A New One-Pass Tableau Calculus for PLTL

  • Stefan Schwendimann
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1397)


The paper presents a one-pass tableau calculus PLTL T for the propositional linear time logic PLTL. The calculus is correct and complete and unlike in previous decision methods, there is no second phase that checks for the fulfillment of the so-called eventuality formulae. This second phase is performed locally and is incorporated into the rules of the calculus. Derivations in PLTL T are cyclic trees rather than cyclic graphs. When used as a basis for a decision procedure, it has the advantage that only one branch needs to be kept in memory at any one time. It may thus be a suitable starting point for the development of a parallel decision method for PLTL.


Temporal Logic Decision Procedure Linear Temporal Logic Propositional Variable Local Consistency 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    M. Browne, E. Clarke, D. Dill, and B. Mishra. Automatic verification of sequential circuits using temporal logic. IEEE Transactions on Computers, 35:1035–1044, December 1986.zbMATHCrossRefGoogle Scholar
  2. 2.
    C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. Memory-efifcient algorithms for the verification of temporal properties. In Formal Methods in System Design, volume 1, pages 275–288, 1992.CrossRefGoogle Scholar
  3. 3.
    M. D’Agostino, D. Gabbay, R. Hähnle, and J. Posegga, editors. Handbook of Tableau Methods, chapter Tableau Methods for Modal and Temporal Logics. Kluwer, to appear. (currently available as technical report TR-ARP-15-95, Australian National University (ANU)).Google Scholar
  4. 4.
    E. Emerson. Temporal and modal logic. In J. v. Leeuwen, editor, Handbook of Theoretical Computer Science. Volume B, pages 995–1072. Elsevier, 1990.Google Scholar
  5. 5.
    M.J. Fischer and R.L. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18:194–211, 1979.zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    M. Fitting. Proof Methods for Modal and Intuitionistic Logics. Reidel, Dordrecht, 1983.zbMATHGoogle Scholar
  7. 7.
    R. Gerth, D. Peled, M. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In P. Dembinski and M. Sredniawa, editors, Protocol Specification Testing and Verification, volume XV, pages 3–18. Chapman & Hall, 1996.Google Scholar
  8. 8.
    R. Goré. Cut-free Sequent and Tableau Systems for Propositional Normal Modal Logic. PhD thesis, Computer Laboratory, University of Cambridge, England, 1992.Google Scholar
  9. 9.
    G. Gough. Decision procedures for temporal logic. Technical Report UMCS-89-10-1, Department of Computer Science, University of Manchester, 1989.Google Scholar
  10. 10.
    A. Heuerding, G. Jäger, S. Schwendimann, and M. Seyfried. Propositional logics on the computer. In P. Baumgartner, R. Hähnle, and J. Posegga, editors, Theorem Proving with Analytic Tableaux and Related Methods, LNCS 918, pages 310–323, 1995.Google Scholar
  11. 11.
    A. Heuerding, M. Seyfried, and H. Zimmermann. Efficient loop-check for backward proof search in some non-classical propositional logics. In P. Miglioli, U. Moscato, D. Mundici, and M. Ornaghi, editors, Tableaux 96, LNCS 1071, pages 210–225, 1996.Google Scholar
  12. 12.
    Y. Kesten, Z. Manna, H. McGuire, and A. Pnueli. A decision algorithm for full propositional temporal logic. In Computer Aided Verification, LNCS 697, pages 4–35. Springer, 1993.Google Scholar
  13. 13.
    Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer Verlag, 1991.Google Scholar
  14. 14.
    K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.Google Scholar
  15. 15.
    A. Sistla and E. Clarke. The complexity of propositional linear temporal logic. Journal of the Association for Computing Machinery, 32(3):733–749, 1985.zbMATHMathSciNetGoogle Scholar
  16. 16.
    R. Tarjan. Depth first search and linear graph algorithms. SIAM Journal Computing, 1(2):146–160, 1972.zbMATHCrossRefMathSciNetGoogle Scholar
  17. 17.
    P. Wolper. The tableau method for temporal logic: an overview. Logique et Analyse, 110–111:119–136, 1985.MathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Stefan Schwendimann
    • 1
  1. 1.Institut für Informatik und angewandte MathematikUniversity of BerneBern

Personalised recommendations