## Linear completeness thresholds for bounded model checking

*Daniel Kroening*, *Joël
Ouaknine*, *Ofer Strichman*, *Thomas Wahl*, and
*James Worrell*
*Bounded model checking* is a symbolic bug-finding method that
examines paths of bounded length for violations of a given LTL
formula. Its rapid adoption in industry owes much to advances in SAT
technology over the past 10-15 years. More recently, there have been
increasing efforts to apply SAT-based methods to *unbounded*
model checking. One such approach is based on computing a
*completeness threshold*: a bound *k* such that, if no
counterexample of length *k* or less to a given LTL formula is found,
then the formula in fact holds over all infinite paths in the
model. The key challenge lies in determining sufficiently small
completeness thresholds. In this paper, we show that if the Büchi
automaton associated with an LTL formula is *cliquey*, i.e., can
be decomposed into clique-shaped strongly connected components, then
the associated completeness threshold is *linear* in the
recurrence diameter of the Kripke model under consideration. We
moreover establish that all unary temporal logic formulas give rise to
cliquey automata, and observe that this group includes a vast range of
specifications used in practice, considerably strengthening earlier
results, which report manageable thresholds only for elementary
formulas of the form F*p* and G*q*.

*Proceedings of CAV 11*, LNCS 6806, 2011. 16 pages.

PDF
© 2011
Springer-Verlag.

Imprint / Data Protection