A Compact Linear Translation for Bounded Model Checking

We present a syntactic scheme for translating future-time LTL bounded model checking problems into propositional satisfiability problems. The scheme is similar in principle to the Separated Normal Form encoding proposed in [5] and extended to past time in [3]: an initial phase involves putting LTL formulae into a normal form based on linear-time fixpoint characterisations of temporal operators. As with [3] and [7], the size of propositional formulae produced is linear in the model checking bound, but the constant of proportionality appears to be lower. A denotational approach is taken in the presentation which is significantly more rigorous than that in [5] and [3], and which provides an elegant alternative way of viewing fixpoint based translations in [7] and [1]. Key words: Bounded Model Checking, Linear Temporal Logic, Fixpoints, SAT, Denotational Semantics

• Type: Journal
• Year: 2007
• Where: ENTCS
• Authors: Paul B. Jackson, Daniel Sheridan
• Keywords: ENTCS 2007, Normal Form, Propositional Satisfiability Problems, Separated Normal Form