Bounded model checking (BMC) is an effective algorithmic method for the verification of finite state systems against temporal specifications expressed in some linear temporal logic, typically LTL. The basis of BMC consists on encoding the existence of a counterexample trace of bounded description into a satisfiability formula, and proceed incrementally increasing the bound if a counterexample is not found.

In spite of its wide acceptance, LTL has limited expressivity, so some important ω-regular properties cannot be expressed in LTL. RLTL is a temporal logic that overcome this expressivity limitation by fusing LTL with regular expressions, extending the expressive power of LTL to all ω-regular languages.

In this talk, I will present the first study on bounded model checking RLTL specifications by providing two semantic translations from RLTL into SAT: one based on non-deterministic Bühi automata, and a more efficient one based on alternating hesitant automata, in both cases with a symbolic transition representation. Both encodings require a number of variables linear in the number of states, and generate SAT formulas of linear size with respect to the unrolling bound. This implies that the SAT formula generated from the alternating automaton is exponentially more succinct than the classical non-determinsitic construction.