| |
VOLUME 2, ISSUE 5, PAPER 5
|
Linear Encodings of Bounded LTL Model Checking
|
©Armin Biere, Johannes Kepler University
©Keijo Heljanko, Helsinki University of Technology
©Tommi Junttila, Helsinki University of Technology
©Timo Latvala, University of Illinois at Urbana-Champaign
©Viktor Schuppan, Computer Systems Institute, ETH Zentrum
|
Abstract
We consider the problem of bounded model checking (BMC) for linear temporal
logic (LTL). We present several efficient encodings that have size linear in
the bound. Furthermore, we show how the encodings can be extended to LTL with
past operators (PLTL). The generalised encoding is still of linear size, but
cannot detect minimal length counterexamples. By using the virtual unrolling
technique minimal length counterexamples can be captured, however, the size of
the encoding is quadratic in the specification. We also extend virtual
unrolling to Buchi automata, enabling them to accept minimal length
counterexamples.
Our BMC encodings can be made incremental in order to benefit from
incremental SAT technology. With fairly small modifications the incremental
encoding can be further enhanced with a termination check, allowing us to prove
properties with BMC. Experiments clearly show that our new encodings improve
performance of BMC considerably, particularly in the case of the incremental
encoding, and that they are very competitive for finding bugs. An analysis of
the liveness-to-safety transformation reveals many similarities to the BMC
encodings in this paper. Using the liveness-to-safety translation with
BDD-based invariant checking results in an efficient method to find shortest
counterexamples that complements the BMC-based approach.
|
Publication date: November 15, 2006
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-2(5:5)2006
Hit Counts: 5138 |
 Creative Commons | |
