Linear Completeness Thresholds for Bounded Model Checking
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 a recent 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 (no
"until") 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.
Collaborators: Daniel Kroening,
Joël Ouaknine, James Worrell (all Oxford), Ofer Strichman (Technion)