Improving the Encoding of LTL Model Checking into SAT

Bounded Model Checking (BMC) is a technique for encoding an LTL model checking problem into a problem of propositional satisfiability. Since the seminal paper by [Biere et al.'99], the research on BMC has been primarily directed at achieving higher efficiency for solving reachability properties. In this paper, we tackle the problem of improving BMC encodings for the full class of LTL properties. We start noticing some properties of the encoding of [Biere et al.'99], and we exploit them to define improvements that make the resulting boolean formulas smaller or simpler to solve.