Sciweavers

Share
CADE
2007
Springer

Encodings of Bounded LTL Model Checking in Effectively Propositional Logic

12 years 7 days ago
Encodings of Bounded LTL Model Checking in Effectively Propositional Logic
We present an encoding that is able to specify LTL bounded model checking problems within the Bernays-Sch?onfinkel fragment of first-order logic. This fragment, which also corresponds to the category of effectively propositional problems (EPR) of the CASC system competitions, allows a natural and succinct representation of both a software/hardware system and the property that one wants to verify. The encoding for the transition system produces a formula whose size is linear with respect to its original description in common component description languages used in the field (e.g. smv format) preserving its modularity and hierarchical structure. Likewise, the LTL property is encoded in a formula of linear size with respect to the input formula, plus an additional component, with a size of O(log k) where k is the bound, that represents the execution flow of the system. The encoding of bounded model checking problems by effectively propositional formulae is the main contribution of this pa...
Andrei Voronkov, Juan Antonio Navarro Pérez
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2007
Where CADE
Authors Andrei Voronkov, Juan Antonio Navarro Pérez
Comments (0)
books