UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

Encodings of bounded LTL model checking in effectively propositional logic

Navarro-Pérez, JA; Voronkov, A; (2007) Encodings of bounded LTL model checking in effectively propositional logic. In: Automated Deduction – CADE-21. 21st International Conference on Automated Deduction Bremen, Germany, July 17-20, 2007 Proceedings. (346 - 361). Springer Berlin Heidelberg Green open access

[img]
Preview
PDF - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
200Kb

Abstract

We present an encoding of LTL bounded model checking problems within the Bernays-Schönfinkel 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 paper. As a side effect, we obtain a rich collection of benchmarks with close links to real-life applications for the automated reasoning community. © Springer-Verlag Berlin Heidelberg 2007.

Type:Book chapter
Title:Encodings of bounded LTL model checking in effectively propositional logic
Event:21st International Conference on Automated Deduction Bremen, Germany, July 17-20, 2007
ISBN:978-3-540-73594-6
Open access status:An open access version is available from UCL Discovery
DOI:10.1007/978-3-540-73595-3_24
Publisher version:http://dx.doi.org/10.1007/978-3-540-73595-3_24
Language:English
Additional information:This is that authors' accepted version of this published article. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-540-73595-3_24
UCL classification:UCL > School of BEAMS > Faculty of Engineering Science > Computer Science

View download statistics for this item

Archive Staff Only: edit this record