An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking

摘要

Bounded model-checking is a technique for finding bugs invery large designs. Bounded model-checking by itself is incomplete: itcan find bugs, but it cannot prove that a system satisfies a specification.A dynamic completeness criterion can allow bounded model-checking toprove properties. A dynamic completeness criterion typically searches fora "beginning" of a bug or bad behavior; if no such "beginning" can befound, we can conclude that no bug exists, and bounded model-checkingcan terminate. Dynamic completeness criteria have been suggested forseveral temporal logics, but most are tied to a specific bounded model-checking encoding, and the ones that are not are based on nondetermin-istic Buchi automata. In this paper we develop a theoretic framework fordynamic completeness criteria based on alternating Buchi automata. Ourcriterion generalizes and explains several existing dynamic completenesscriteria, and is suitable for both linear-time and universal branching-timelogic. We show that using alternating automata rather than nondeter-ministic automata can lead to much smaller completeness thresholds.