Abstract
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 theory of this approach originated in the 1980s, and the basic algorithms were developed during the 1990s. Both explicit and symbolic implementations, such as SPIN and SMV, are widely used.
Chapter PDF
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Vardi, M.Y. (2009). Automata-Theoretic Model Checking Revisited. In: Chockler, H., Hu, A.J. (eds) Hardware and Software: Verification and Testing. HVC 2008. Lecture Notes in Computer Science, vol 5394. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-01702-5_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-01702-5_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-01701-8
Online ISBN: 978-3-642-01702-5
eBook Packages: Computer ScienceComputer Science (R0)