Abstract
We present a tableau-based algorithm for obtaining an automaton from a temporal logic formula. The algorithm is geared towards being used in model checking in an “on-the-fly” fashion, that is the automaton can be constructed simultaneously with, and guided by, the generation of the model. In particular, it is possible to detect that a property does not hold by only constructing part of the model and of the automaton. The algorithm can also be used to check the validity of a temporal logic assertion. Although the general problem is PSPACE-complete, experiments show that our algorithm performs quite well on the temporal formulas typically encountered in verification. While basing linear-time temporal logic model-checking upon a transformation to automata is not new, the details of how to do this efficiently, and in “on-the-fly” fashion have never been given.
The work of this author was supported by the Esprit BRA action REACT and by the Belgian Incentive Program “Information Technology” — Computer Science of the future, initiated by the Belgian State — Prime Minister’s Office — Science Policy Office. The scientific responsibility is assumed by its authors.
Chapter PDF
References
Y. Choueka, Theories of automata on w-Tapes: a simplified approach, Journal of Computer and System Science 8 (1974), 117–141.
G. Bhat, R. Cleaveland, O. Grumberg, Efficient on-the-fly model checking for CTL*, Proceedings of the 10th Symposium on Logic in Computer Science, 1995, San Diego, CA, To appear.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L.Dill, J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, 98 (1992), 142–170.
C. Courcoubetis, M. Vardi, P. Wolper, M Yannakakis, Memory-efficient algorithms for the verification of temporal properties, Formal methods in system design 1 (1992) 275–288.
O. Coudert, C. Berthet, J.C. Madre, Verification of synchronous sequential machines based on symbolic execution, Automatic Verification Methods for Finite State Systems, Grenoble, France, LNCS 407, Springer—Verlag, 1989, 365–373.
G.J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall, 1992.
Y. Kesten, Z. Manna, H. McGuire, A. Pnueli, A decision algorithm for full propositional temporal logic, CAV’93, Elounda, Greece, LNCS 697, Springer—Verlag, 97–109.
O. Lichtenstein, A. Pnueli, Checking that finite-state concurrent programs satisfy their linear specification, 11th ACM POPL, 1984, 97–107.
A. Pnueli, The temporal logic of programs, Proceedings of the 18th IEEE Symposium on Foundation of Computer Science, 1977, 46–57.
A. P. Sistla, E. M. Clarke, The Complexity of propositional linear temporal logics, Journal of the ACM, 32 (1985), 733–749.
W. Thomas, Automata on infinite objects, Handbook of theoretical computer science, 1990, 165–191.
M.Y. Vardi, R. Wolper, An automata-theoretic approach to automatic program verification, Proceedings of the 1st Symposium on Logic in Computer Science, 1986, Cambridge, England, 322–331.
M.Y. Vardi, R Wolper, Reasoning about infinite computations, Information and Computation, 115 (1994), 1–37.
R Wolper, Temporal logic can be more expressive, Information and Control, 56 (1983), 72–99.
R Wolper, The tableau method for temporal logic: an overview, Logique et Analyse, 110–111 (1985), 119–136.
R Wolper, M.Y. Vardi, A.P. Sistla, Reasoning about infinite computation paths, Proceedings of 24th IEEE symposium on foundation of computer science, Tuscan, 1983, 185–194.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1996 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Gerth, R., Peled, D., Vardi, M.Y., Wolper, P. (1996). Simple On-the-fly Automatic Verification of Linear Temporal Logic. In: Dembiński, P., Średniawa, M. (eds) Protocol Specification, Testing and Verification XV. PSTV 1995. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-34892-6_1
Download citation
DOI: https://doi.org/10.1007/978-0-387-34892-6_1
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2925-1
Online ISBN: 978-0-387-34892-6
eBook Packages: Springer Book Archive