Abstract
In this chapter, we describe the theory of LTL model checking using w- automata theory. The relation between model checking algorithms and automata theory allows applying various known results about automata to the automatic verification of programs.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
M. Y. Vardi . An automata-theoretic approach to linear temporal logic. In Logics for Concurrency: Structure versus Automata, pages 238-266. Springer-Verlag, Lecture Notes in Computer Science 1043, 1996.
M.Y . Vardi and P. Wolper . Automata-theoretic techniques for modal logics of programs . In Proc. 16th ACM Symposium on Theory of Computing, pages 446–456, May 1984.
M.Y. Vardi and P. Wolfer. Reasoning about infinite computations.Information and Computation, 115:1–37, 1994.
W. Thomas. Automata on infinite objects. In J. Van Leeuwen, editor, Hand-book of Theoretical Computer Science, volume B, pages 133–191. Eisvier, 1990.
W. Thomas. Languages, automata, and logic. In G. Rozenberg and A. Salo-maa, editors, Handbook of Formal Language Theory, volume III, pages 389–455. Springer-Verlag, New York.
J.R. BÜchi. On a decision method in restricted second order arithmetic. In Proc. Internat. Congr. Logic, Method and Philos. Sei. 1960, pages 1–12, Stanford, 1962. Stanford University Press.
G. J. Holzmann.Design and Validation of Computer Protocols. Prentice Hall Software Series, 1992.
R.P. Kurshan. Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton, New Jersey, 1994
D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi . On the temporal analysis of fairness. ACM Symposium on Principles of Programming Languages, pages 163–173, 1980.
M.O. Rabin and D. Scott. Finite automata and their decision problems. IBM journal of research and development, 3:114–125, 1959.
A.P. Sistla, M.Y. Vardi, and P. Wolper. The complementation problem for BÜchi automata with applications to temporal logic. Theoretical Computer Science, 49:217–237, 1987.
S. Safra. On the complexity of omega-automata. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science, White Plains, October 1988.
R.E. Tarjan. Depth first search and linear graph algorithms.SIAM Journal of Computing 1:146–160, 1972.
C. Courcoubetis, M.Y. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1:275–288, 1992.
R. Gerth, D. Peled, M.Y. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In PS TV 95, Protocol Specification Testing and Verification, pages 3–18, Warsaw, Poland, 1995. Chapman & Hall.
P. Wolper. Temporal logic can be more expressive. In Proceedings of the 22nd IEEE Symposium on Foundations of Computer Science, pages 340–348, Nashville, October 1981.
D. Kozen. Lower bounds for natural proof Systems. In 18th IEEE Symposium on Foundations of Computer Science, pages 254-266, Providence, Rhode Island, 197
A.P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logics. Journal of the ACM, 32:733–749, 1985.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg New York
About this chapter
Cite this chapter
Shukla, S.K. (2000). Model Checking Using Automata Theory. In: Inan, M.K., Kurshan, R.P. (eds) Verification of Digital and Hybrid Systems. NATO ASI Series, vol 170. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-59615-5_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-59615-5_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-64052-0
Online ISBN: 978-3-642-59615-5
eBook Packages: Springer Book Archive