## On the magnitude of completeness thresholds in
bounded model checking

*Daniel Bundala*, *Joël
Ouaknine*, and *James Worrell*
Bounded model checking (BMC) is a highly successful bug-finding method
that examines paths of bounded length for violations of a given
regular or ω-regular specification. A *completeness
threshold* for a given model *M* and specification φ is a
bound *k* such that, if no counterexample to φ of
length *k* or less can be found in *M*, then *M* in fact
satisfies φ. The quest for 'small' completeness thresholds in
BMC goes back to the very inception of the technique, over a decade
ago, and remains a topic of active research.
For a fixed specification, completeness thresholds are typically
expressed in terms of key attributes of the models under
consideration, such as their diameter (length of the longest shortest
path) and especially their *recurrence diameter* (length of the
longest loop-free path). A recent research paper identified a large
class of LTL specifications having completeness thresholds
*linear* in the models' recurrence diameter [7]. However, the
authors left open the question of whether linearity is in general even
decidable.
In the present paper, we settle the problem in the affirmative, by
showing that the linearity problem for both regular and
ω-regular specifications (provided as automata and Buchi
automata respectively) is PSPACE-complete.
Moreover, we establish the following dichotomies: for regular
specifications, completeness thresholds are either linear or
exponential, whereas for ω-regular specifications, completeness
thresholds are either linear or at least quadratic.

*Proceedings of LICS 12*, 2012. 10 pages.

PDF
© 2012 IEEE Computer Society Press.

Imprint / Data Protection