Sciweavers

ENTCS
2007

A Compact Linear Translation for Bounded Model Checking

13 years 3 months ago
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
Paul B. Jackson, Daniel Sheridan
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2007
Where ENTCS
Authors Paul B. Jackson, Daniel Sheridan
Comments (0)