Alternating Automata Semantic Constructions for the Bounded Model Checking of Regular Linear Temporal Logic

Abstract—We present two algorithms for bounded model checking of Regular Linear Temporal Logic (RLTL) specifica-tions. 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 paper we present the first study on bounded model checking RLTL specifications by providing two semantic trans-lations from RLTL into SAT: one based on non-deterministic Büchi 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. Keywords-temporal logic; formal verification; formal meth-ods; model checking; regular linear temporal logic; bounded model checking I