## Computational challenges in bounded model checking

*Edmund Clarke*, *Daniel Kroening*,
*Joël
Ouaknine*, and *Ofer Strichman*
We describe several observations regarding the completeness and the
complexity of bounded model checking and propose techniques to solve
some of the associated computational challenges. We begin by defining
the completeness threshold (*CT*) problem: for every
finite model *M* and LTL property *φ*, there exists a number
*CT* 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 overapproximation to *CT* for a
general LTL property using Büchi automata, following the Vardi-Wolper
LTL model checking framework. This computation is based on finding the
initialized diameter and initialized recurrence-diameter (the longest
loop-free path from an initial state) of the product automaton. We
show a method for finding a recurrence diameter with a formula of size
*O(klogk)* (or *O(k(logk)*^{2}) in practice), where
*k* is the attempted depth, which is an improvement compared to
the previously known method that requires a formula of size in
*O(k*^{2}). 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.

*International Journal on Software Tools for Technology Transfer*
7(2), 2005. 10 pages.

PDF
© 2005 Springer-Verlag.

Imprint / Data Protection