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

  • R. Gerth
  • D. Peled
  • M. Y. Vardi
  • P. Wolper
Part of the IFIP Advances in Information and Communication Technology book series (IFIPAICT)


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.


Automatic Verification Linear Temporal Logic Büchi Automata Concurrency Specification 


  1. [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. [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. [3]
    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.MathSciNetCrossRefzbMATHGoogle Scholar
  4. [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. [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. [6]
    G.J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall, 1992.Google Scholar
  7. [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. [8]
    O. Lichtenstein, A. Pnueli, Checking that finite-state concurrent programs satisfy their linear specification, 11th ACM POPL, 1984, 97–107.Google Scholar
  9. [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. [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. [11]
    W. Thomas, Automata on infinite objects, Handbook of theoretical computer science, 1990, 165–191.Google Scholar
  12. [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. [13]
    M.Y. Vardi, R Wolper, Reasoning about infinite computations, Information and Computation, 115 (1994), 1–37.MathSciNetCrossRefzbMATHGoogle Scholar
  14. [14]
    R Wolper, Temporal logic can be more expressive, Information and Control, 56 (1983), 72–99.MathSciNetCrossRefzbMATHGoogle Scholar
  15. [15]
    R Wolper, The tableau method for temporal logic: an overview, Logique et Analyse, 110–111 (1985), 119–136.MathSciNetGoogle Scholar
  16. [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

Copyright information

© IFIP International Federation for Information Processing 1996

Authors and Affiliations

  • R. Gerth
    • 1
  • D. Peled
    • 2
  • M. Y. Vardi
    • 3
  • P. Wolper
    • 4
  1. 1.Technical University EindhovenEindhovenThe Netherlands
  2. 2.ATamp;T Bell LaboratoriesMurray HillUSA
  3. 3.Department of Computer ScienceRice UniversityHoustonUSA
  4. 4.Institut MontefioreUniversité de LiègeLiègeBelgium

Personalised recommendations