In automata-theoretic model checking we compose the design under verification with a Büchi automaton that accepts traces violating the specification. 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 algorithms were developed during the 1990s. Both explicit and symbolic implementations, 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. The conference talk also reviews the reduction of the theory to practice and outlines areas that require further research. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Vardi, M. Y. (2007). Linear-time model checking: Automata theory in practice. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4783 LNCS, pp. 5–10). Springer Verlag. https://doi.org/10.1007/978-3-540-76336-9_2
Mendeley helps you to discover research relevant for your work.