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
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.