
doi: 10.1109/lics.2012.27
Bounded model checking (BMC) is a highly successful bug-finding method that examines paths of bounded length for violations of a given regular or omega-regular specification. A completeness threshold for a given model M and specification phi is a bound k such that, if no counterexample to phi of length k or less can be found in M, then M in fact satisfies phi. 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. 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 omega-regular specifications (provided as automata and Buechi automata respectively is PSPACE-complete. Moreover, we establish the following dichotomies: for regular specifications, completeness thresholds are either linear or exponential, whereas for omega-regular specifications, completeness thresholds are either linear or at least quadratic.
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 2 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
