## Completeness and complexity of bounded model checking

*Edmund Clarke*, *Daniel Kroening*,
*Joël
Ouaknine*, and *Ofer Strichman*
For every finite model *M* and LTL property *φ*, there
exists a number *CT* (the *Completeness Threshold*) such
that if there is no counterexample to *φ* in *M* of length
*CT* or less, then *M* satisfies *φ*. Finding this
number, if it is sufficiently small, offers a practical method for
making Bounded Model Checking complete. We describe how to compute an
over-approximation to *CT* for a general LTL property using
Büchi automata, following the Vardi-Wolper LTL model checking
framework. Based on the value of *CT*, we prove that the
complexity of standard SAT-based BMC is doubly exponential, and that
consequently there is a complexity gap of an exponent between this
procedure and standard LTL model checking. We discuss ways to bridge
this gap.

The article mainly focuses on observations
regarding bounded model checking rather than on a presentation of new
techniques.

*Proceedings of VMCAI 04*, LNCS 2937, 2004. 12 pages.

PostScript /
PDF
© 2004
Springer-Verlag.

**Note: This paper is superceded by**

E. M. Clarke, D. Kroening, J. Ouaknine, and O. Strichman.
Computational challenges in bounded model checking.
*International Journal on Software Tools for Technology Transfer*
7(2), 2005.

Imprint / Data Protection