Document Open Access Logo

A Cyclic Proof System for Full Computation Tree Logic

Authors Bahareh Afshari, Graham E. Leigh, Guillermo Menéndez Turata

PDF
Thumbnail PDF

File

LIPIcs.CSL.2023.5.pdf
  • Filesize: 0.74 MB
  • 19 pages

Document Identifiers

Author Details

Bahareh Afshari
  • Institute for Logic, Language and Computation, University of Amsterdam, The Netherlands
  • Department of Philosophy, Linguistics and Theory of Science, University of Gothenburg, Sweden
Graham E. Leigh
  • Department of Philosophy, Linguistics and Theory of Science, University of Gothenburg, Sweden
Guillermo Menéndez Turata
  • Institute for Logic, Language and Computation, University of Amsterdam, The Netherlands

Funding

Supported by the Knut and Alice Wallenberg Foundation [2020.0199]; Swedish Research Council [2017-05111, 2016-03502]; and the Dutch Research Council [OCENW.M20.048].

Cite AsGet BibTex

Bahareh Afshari, Graham E. Leigh, and Guillermo Menéndez Turata. A Cyclic Proof System for Full Computation Tree Logic. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CSL.2023.5

Abstract

Full Computation Tree Logic, commonly denoted CTL*, is the extension of Linear Temporal Logic LTL by path quantification for reasoning about branching time. In contrast to traditional Computation Tree Logic CTL, the path quantifiers are not bound to specific linear modalities, resulting in a more expressive language. We present a sound and complete hypersequent calculus for CTL*. The proof system is cyclic in the sense that proofs are finite derivation trees with back-edges. A syntactic success condition on non-axiomatic leaves guarantees soundness. Completeness is established by relating cyclic proofs to a natural ill-founded sequent calculus for the logic.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Proof theory
Keywords
  • Full computation tree logic
  • Hypersequent calculus
  • Cyclic proofs

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Pietro Abate, Rajeev Goré, and Florian Widmann. One-pass tableaux for computation tree logic. In Nachum Dershowitz and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, LPAR 2007, Yerevan, Armenia, October 15-19, 2007, Proceedings, volume 4790 of Lecture Notes in Computer Science, pages 32-46. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-75560-9_5.
  2. Bahareh Afshari, Sebastian Enqvist, and Graham E Leigh. Cyclic proofs for the first-order μ-calculus. Logic Journal of the IGPL, 2022. URL: https://doi.org/10.1093/jigpal/jzac053.
  3. Bahareh Afshari and Graham E. Leigh. Circular proofs for the modal mu-calculus. PAMM, 16(1):893-894, 2016. URL: https://doi.org/10.1002/pamm.201610435.
  4. Bahareh Afshari and Graham E. Leigh. Cut-free completeness for modal mu-calculus. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005088.
  5. Bahareh Afshari and Dominik Wehr. Abstract cyclic proofs. In Agata Ciabattoni, Elaine Pimentel, and Ruy J. G. B. de Queiroz, editors, Logic, Language, Information, and Computation - 28th International Workshop, WoLLIC 2022, Iaşi, Romania, September 20-23, 2022, Proceedings, volume 13468 of Lecture Notes in Computer Science, pages 309-325. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-15298-6_20.
  6. Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. J. ACM, 49(5):672-713, 2002. URL: https://doi.org/10.1145/585265.585270.
  7. Kai Brünnler and Martin Lange. Cut-free sequent systems for temporal logic. J. Log. Algebraic Methods Program., 76(2):216-225, 2008. URL: https://doi.org/10.1016/j.jlap.2008.02.004.
  8. Mads Dam. Translating CTL* into the modal μ-calculus. Tech. rep. ECS-LFCS-90-123, University of Edinburgh, Department of Computer Science, Laboratory for Foundations of Computer Science, 1990. Google Scholar
  9. Anupam Das and Marianna Girlando. Cyclic proofs, hypersequents, and transitive closure logic. In Jasmin Blanchette, Laura Kovács, and Dirk Pattinson, editors, Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings, volume 13385 of Lecture Notes in Computer Science, pages 509-528. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-10769-6_30.
  10. Stéphane Demri, Valentin Goranko, and Martin Lange. Temporal Logics in Computer Science: Finite-State Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. URL: https://doi.org/10.1017/CBO9781139236119.
  11. Sebastian Enqvist. A circular proof system for the hybrid μ-calculus. In Nicola Olivetti, Rineke Verbrugge, Sara Negri, and Gabriel Sandu, editors, 13th Conference on Advances in Modal Logic, AiML 2020, Helsinki, Finland, August 24-28, 2020, pages 169-188. College Publications, 2020. Google Scholar
  12. Oliver Friedmann, Markus Latte, and Martin Lange. A decision procedure for CTL* based on tableaux and automata. In International Joint Conference on Automated Reasoning, pages 331-345. Springer, 2010. Google Scholar
  13. Dov M. Gabbay and Amir Pnueli. A sound and complete deductive system for CTL* verification. Logic Journal of the IGPL, 16(6):499-536, 2008. Google Scholar
  14. Natthapong Jungteerapanich. A tableau system for the modal μ-calculus. In Martin Giese and Arild Waaler, editors, Automated Reasoning with Analytic Tableaux and Related Methods, 18th International Conference, TABLEAUX 2009, Oslo, Norway, July 6-10, 2009. Proceedings, volume 5607 of Lecture Notes in Computer Science, pages 220-234. Springer, 2009. Google Scholar
  15. Ioannis Kokkinis and Thomas Studer. Cyclic proofs for linear temporal logic. Ontos Mathematical Logic, 6:171-192, 2016. Google Scholar
  16. Orna Kupferman and Moshe Y. Vardi. Memoryful branching-time logic. In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings, pages 265-274. IEEE Computer Society, 2006. URL: https://doi.org/10.1109/LICS.2006.34.
  17. Johannes Marti and Yde Venema. A focus system for the alternation-free μ-calculus. In Anupam Das and Sara Negri, editors, Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6-9, 2021, Proceedings, volume 12842 of Lecture Notes in Computer Science, pages 371-388. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-86059-2_22.
  18. Donald A. Martin. Borel determinacy. Annals of Mathematics, 102(2):363-371, 1975. Google Scholar
  19. Faron Moller and Alexander Moshe Rabinovich. Counting on CTL*: On the expressive power of monadic path logic. Inf. Comput., 184(1):147-159, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00104-4.
  20. Damian Niwiński and Igor Walukiewicz. Games for the μ-calculus. Theoretical Computer Science, 163(1-2):99-116, 1996. Google Scholar
  21. Rémi Nollet, Alexis Saurin, and Christine Tasson. PSPACE-Completeness of a thread criterion for circular proofs in linear logic with least and greatest fixed points. In S. Cerrito and A. Popescu, editors, Automated Reasoning with Analytic Tableaux and Related Methods, Lecture Notes in Computer Science, pages 317-334. Springer International Publishing, Cham, 2019. URL: https://doi.org/10.1007/978-3-030-29026-9_18.
  22. Mark Reynolds. An axiomatization of full computation tree logic. The Journal of Symbolic Logic, 66(3):1011-1057, 2001. Google Scholar
  23. Mark Reynolds. An axiomatization of PCTL*. Inf. Comput., 201(1):72-119, 2005. URL: https://doi.org/10.1016/j.ic.2005.03.005.
  24. Mark Reynolds. A tableau for CTL*. In Ana Cavalcanti and Dennis R. Dams, editors, Formal Methods, pages 403-418. Springer Berlin Heidelberg, 2009. Google Scholar
  25. Mark Reynolds. A tableau-based decision procedure for CTL*. Formal aspects of computing, 23(6):739-779, 2011. Google Scholar
  26. Jan Rooduijn. Cyclic hypersequent calculi for some modal logics with the master modality. In Anupam Das and Sara Negri, editors, Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6-9, 2021, Proceedings, volume 12842 of Lecture Notes in Computer Science, pages 354-370. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-86059-2_21.
  27. Jan Rooduijn and Lukas Zenger. An analytic proof system for common knowledge logic over S5. In Proceedings of Advances in Modal Logic (AiML 2022), (to appear). Google Scholar
  28. Ulrike Sattler and Moshe Y. Vardi. The hybrid μ-calculus. In Rajeev Goré, Alexander Leitsch, and Tobias Nipkow, editors, Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings, volume 2083 of Lecture Notes in Computer Science, pages 76-91. Springer, 2001. Google Scholar
  29. Yury Savateev and Daniyar S. Shamkanov. Non-well-founded proofs for the Grzegorczyk modal logic. Rev. Symb. Log., 14(1):22-50, 2021. URL: https://doi.org/10.1017/S1755020319000510.
  30. Colin Stirling. A tableau proof system with names for modal mu-calculus. In Andrei Voronkov and Margarita V. Korovina, editors, HOWARD-60: A Festschrift on the Occasion of Howard Barringer’s 60th Birthday, volume 42 of EPiC Series in Computing, pages 306-318. EasyChair, 2014. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact