Skip to main content
SpringerLink
Log in

Towards a CTL* Tableau

  • Conference paper
FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2005)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3821))

Abstract

We present a sound, complete and relatively straightforward tableau method for deciding valid formulas in the propositional version of the bundled (or suffix and fusion closed) computation tree logic BCTL*. This proves that BCTL* is decidable. It is also moderately useful to have a tableau available for a reasonably expressive branching time temporal logic. However, the main interest in this should be that it leads us closer to being able to devise a tableau-based technique for theorem-proving in the important full computational tree logic CTL*.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Burgess, J.P.: Logic and time. J. Symbolic Logic 44, 566–582 (1979)

    Article  MATH  MathSciNet  Google Scholar 

  2. Burgess, J.P.: Decidability for Branching Time. Studia Logica 39, 203–218 (1980)

    Article  MATH  MathSciNet  Google Scholar 

  3. Clarke, E., Emerson, E.: Synthesis of synchronization skeletons for branching time temporal logic. In: Proc. IBM Workshop on Logic of Programs, Yorktown Heights, NY, pp. 52–71. Springer, Berlin (1981)

    Google Scholar 

  4. Clarke, E., Emerson, E., Sistla, A.: Automatic verification of finite state concurrent system using temporal logic specifications: a practical approach. In: Proc. 10th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 117–126 (1983)

    Google Scholar 

  5. Emerson, E., Clarke, E.C.: Using branching time temporal logic to synthesise synchronisation skeletons. Sci. of Computer Programming 2 (1982)

    Google Scholar 

  6. Emerson, E., Halpern, J.: Decision procedures and expressiveness in the temporal logic of branching time. J. Comp and Sys. Sci 30(1), 1–24 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  7. Emerson, E., Jutla, C.: Complexity of tree automata and modal logics of programs. In: Proceedings of 29th IEEE Foundations of Computer Science, IEEE, Los Alamitos (1988)

    Google Scholar 

  8. Emerson, E., Sistla, A.: Deciding full branching time logic. Information and Control 61, 175–201 (1984)

    Article  MATH  MathSciNet  Google Scholar 

  9. Emerson, E.: Alternative semantics for temporal logics. Theoretical Computer Science 26, 121–130 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  10. Emerson, E.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, Elsevier, Amsterdam (1990)

    Google Scholar 

  11. Fitting, M.: Proof methods for modal and intuitionistic logics. Reidel, Boston (1983)

    MATH  Google Scholar 

  12. Goré, R.: Tableau methods for modal and temporal logics. In: D’Agostino, M., Gabbay, D., Hähnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, pp. 297–396. Kluwer Academic Publishers, Dordrecht (1999)

    Google Scholar 

  13. Gough, G.: Decision procedures for temporal logics. Technical Report UMCS-89- 10-1, Department of Computer Science, University of Manchester (1989)

    Google Scholar 

  14. Hodkinson, I., Wolter, F., Zakharyaschev, M.: Decidable and undecidable fragments of first-order branching temporal logics. In: LICS 2002, Proceedings of 17th Annual IEEE Symp. Logic in Computer Science, pp. 393–402. IEEE Computer Society Press, Los Alamitos (2002)

    Chapter  Google Scholar 

  15. Hughes, G., Cresswell, M.: An Introduction to Modal Logic. Methuen, London (1968)

    MATH  Google Scholar 

  16. Pnueli, A., Kesten, Y.: A deductive proof system for CTL*. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 24–40. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  17. Pnueli, A.: The temporal logic of programs. In: Proceedings of 18th Symp. on Foundations of Computer Science, pp. 46–57. Providence, RI (1977)

    Google Scholar 

  18. Reynolds, M., Dixon, C.: Theorem-proving for discrete temporal logic. In: Fisher, M., Gabbay, D., Vila, L. (eds.) Handbook of Temporal Reasoning in Artificial Intelligence, pp. 279–314. Elsevier, Amsterdam (2005)

    Chapter  Google Scholar 

  19. Reynolds, M.: An axiomatization of full computation tree logic. J. Symbolic Logic 66(3), 1011–1057 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  20. Reynolds, M.: An axiomatization of PCTL*. Information and Computation 201, 72–119 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  21. Schwendimann, S.: A new one-pass tableau calculus for PLTL. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol. 1397, pp. 277–291. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  22. Sprenger, C.: Deductive Local Model Checking. PhD thesis, Swiss Federal Institute of Technology, Lausanne, Switzerland (2000)

    Google Scholar 

  23. Stirling, C.: Modal and temporal logics. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science, vol. 2, pp. 477–563. OUP (1992)

    Google Scholar 

  24. Vardi, M., Stockmeyer, L.: Improved upper and lower bounds for modal logics of programs. In: 17th ACM Symp. on Theory of Computing, Proceedings, pp. 240–251. ACM Press, New York (1985)

    Google Scholar 

  25. Wolper, P.: The tableau method for temporal logic: an overview. Logique et Analyse 28, 110–111 (1985)

    MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. The University of Western Australia, Perth, Australia

    Mark Reynolds

Authors
  1. Mark Reynolds
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. National Institute of Advanced Studies, Indian Institute of Science Campus, 560012, Bangalore, India

    Sundar Sarukkai

  2. Department of Comp. Sc. & Engg., Indian Institute of Technology Delhi, 110016, New Delhi, India

    Sandeep Sen

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Reynolds, M. (2005). Towards a CTL* Tableau. In: Sarukkai, S., Sen, S. (eds) FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2005. Lecture Notes in Computer Science, vol 3821. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11590156_31

Download citation

  • DOI: https://doi.org/10.1007/11590156_31

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-30495-1

  • Online ISBN: 978-3-540-32419-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation