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 Fp and Gq.
Proceedings of CAV 11, LNCS 6806, 2011. 16 pages.
PDF
© 2011
Springer-Verlag.