A New One-Pass Tableau Calculus for PLTL
- 264 Downloads
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.
KeywordsTemporal Logic Decision Procedure Linear Temporal Logic Propositional Variable Local Consistency
Unable to display preview. Download preview PDF.
- 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.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
- 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.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.G. Gough. Decision procedures for temporal logic. Technical Report UMCS-89-10-1, Department of Computer Science, University of Manchester, 1989.Google Scholar
- 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.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.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.Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer Verlag, 1991.Google Scholar
- 14.K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.Google Scholar