Automata-Theoretic Model Checking Revisited

Abstract

In automata-theoretic model checking we compose the design under verification with a Büchi automaton that accepts traces violating the specifica-tion. We then use graph algorithms to search for a counterexample trace. The basic theory of this approach was worked out in the 1980s, and the basic algo-rithms were developed during the 1990s. Both explicit and symbolic implemen-tations, such as SPIN and and SMV, are widely used. It turns out, however, that there are still many gaps in our understanding of the algorithmic issues involved in automata-theoretic model checking. This paper covers the fundamentals of automata-theoretic model checking, review recent progress, and outlines areas that require further research.