# Simple On-the-fly Automatic Verification of Linear Temporal Logic

## 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.

## Keywords

Automatic Verification Linear Temporal Logic Büchi Automata Concurrency Specification## References

- [1]Y. Choueka, Theories of automata on w-Tapes: a simplified approach, Journal of Computer and System Science 8 (1974), 117–141.MathSciNetCrossRefzbMATHGoogle Scholar
- [2]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.Google Scholar
- [3]J.R. Burch, E.M. Clarke, K.L. McMillan, D.L.Dill, J. Hwang, Symbolic model checking: 10
^{20}states and beyond, Information and Computation, 98 (1992), 142–170.MathSciNetCrossRefzbMATHGoogle Scholar - [4]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.CrossRefGoogle Scholar
- [5]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.Google Scholar
- [6]G.J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall, 1992.Google Scholar
- [7]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.Google Scholar
- [8]O. Lichtenstein, A. Pnueli, Checking that finite-state concurrent programs satisfy their linear specification,
*11th*ACM POPL, 1984, 97–107.Google Scholar - [9]A. Pnueli, The temporal logic of programs, Proceedings of the 18th IEEE Symposium on Foundation of Computer Science, 1977, 46–57.Google Scholar
- [10]A. P. Sistla, E. M. Clarke, The Complexity of propositional linear temporal logics, Journal of the ACM, 32 (1985), 733–749.MathSciNetCrossRefzbMATHGoogle Scholar
- [11]W. Thomas, Automata on infinite objects, Handbook of theoretical computer science, 1990, 165–191.Google Scholar
- [12]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.Google Scholar - [13]M.Y. Vardi, R Wolper, Reasoning about infinite computations, Information and Computation, 115 (1994), 1–37.MathSciNetCrossRefzbMATHGoogle Scholar
- [14]R Wolper, Temporal logic can be more expressive, Information and Control, 56 (1983), 72–99.MathSciNetCrossRefzbMATHGoogle Scholar
- [15]R Wolper, The tableau method for temporal logic: an overview, Logique et Analyse, 110–111 (1985), 119–136.MathSciNetGoogle Scholar
- [16]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.Google Scholar