Document Open Access Logo

One-Pass Context-Based Tableaux Systems for CTL and ECTL

Authors Alex Abuin , Alexander Bolotov , Montserrat Hermo , Paqui Lucio

PDF
Thumbnail PDF

File

LIPIcs.TIME.2020.14.pdf
  • Filesize: 0.67 MB
  • 20 pages

Document Identifiers

Author Details

Alex Abuin
  • Ikerlan Technology Research Centre, Basque Research and Technology Alliance (BRTA), Arrasate-Mondragón Gipuzkoa, Spain
Alexander Bolotov
  • University of Westminster, London, UK
Montserrat Hermo
  • University of the Basque Country, San Sebastián, Spain
Paqui Lucio
  • University of the Basque Country, San Sebastián, Spain

Funding

  • Bolotov, Alexander: This author has been supported by the European Union (FEDER funds) under grant TIN2017-86727-C2-2-R, and by the University of the Basque Country under Project LoRea GIU18-182.
  • Hermo, Montserrat: This author has been supported by the European Union (FEDER funds) under grant TIN2017-86727-C2-2-R, and by the University of the Basque Country under Project LoRea GIU18-182.
  • Lucio, Paqui: This author has been supported by the European Union (FEDER funds) under grant TIN2017-86727-C2-2-R, and by the University of the Basque Country under Project LoRea GIU18-182.

Cite AsGet BibTex

Alex Abuin, Alexander Bolotov, Montserrat Hermo, and Paqui Lucio. One-Pass Context-Based Tableaux Systems for CTL and ECTL. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.TIME.2020.14

Abstract

When building tableau for temporal logic formulae, applying a two-pass construction, we first check the validity of the given tableaux input by creating a tableau graph, and then, in the second "pass", we check if all the eventualities are satisfied. In one-pass tableaux checking the validity of the input does not require these auxiliary constructions. This paper continues the development of one-pass tableau method for temporal logics introducing tree-style one-pass tableau systems for Computation Tree Logic (CTL) and shows how this can be extended to capture Extended CTL (ECTL). A distinctive feature here is the utilisation, for the core tableau construction, of the concept of a context of an eventuality which forces its earliest fulfilment. Relevant algorithms for obtaining a systematic tableau for these branching-time logics are also defined. We prove the soundness and completeness of the method. With these developments of a tree-shaped one-pass tableau for CTL and ECTL, we have formalisms which are well suited for the automation and are amenable for the implementation, and for the formulation of dual sequent calculi. This brings us one step closer to the application of one-pass context-based tableaux in certified model checking for a variety of CTL-type branching-time logics.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • Temporal logic
  • fairness
  • expressiveness
  • branching-time

Metrics

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

References

  1. P. Abate, R. Goré, and F. Widmann. One-pass tableaux for computation tree logic. In N. Dershowitz and A. Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, pages 32-46, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-75560-9_5.
  2. A. Abuin, A. Bolotov, U. Díaz-de-Cerio, M. Hermo, and P. Lucio. Towards certified model checking for PLTL using one-pass tableaux. In Johann Gamper, Sophie Pinchinat, and Guido Sciavicco, editors, 26th International Symposium on Temporal Representation and Reasoning, TIME 2019, October 16-19, 2019, Málaga, Spain, volume 147 of LIPIcs, pages 12:1-12:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.TIME.2019.12.
  3. M. Ben-Ari, A. Pnueli, and Z. Manna. The temporal logic of branching time. Acta Inf., 20(3):207–226, September 1983. URL: https://doi.org/10.1007/BF01257083.
  4. A. Bolotov, M. Hermo, and P. Lucio. Branching-time logic ECTL# and its tree-style one-pass tableau: Extending fairness expressibility of ECTL+. Theoretical Computer Science, 813:428-451, 2020. URL: https://doi.org/10.1016/j.tcs.2020.02.015.
  5. J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142-170, 1992. URL: https://doi.org/10.1016/0890-5401(92)90017-A.
  6. E. M. Clarke and E. A. Emerson. Using Branching Time Temporal Logic to Synthesise Synchronisation Skeletons. Science of Computer Programming, pages 241-266, 1982. URL: https://doi.org/10.1016/0167-6423(83)90017-5.
  7. E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst., 8(2):244-263, 1986. URL: https://doi.org/10.1145/567067.567080.
  8. E. A. Emerson. Temporal and modal logic. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science (Vol. B), pages 995-1072. MIT Press, Cambridge, USA, 1990. Google Scholar
  9. E. A. Emerson and J. Y. Halpern. Decision procedures and expressiveness in the temporal logic of branching time. Journal of Computer and System Sciences, 30(1):1-24, 1985. URL: https://doi.org/10.1016/0022-0000(85)90001-7.
  10. E. A. Emerson and J. Y. Halpern. Sometimes and not never revisited: On branching versus linear time temporal logic. J. ACM, 33(1):151-178, 1986. URL: https://doi.org/10.1145/4904.4999.
  11. J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro, and F. Orejas. Dual systems of tableaux and sequents for PLTL. Journal of Logic and Algebraic Programming, 78(8):701-722, 2009. URL: https://doi.org/10.1016/j.jlap.2009.05.001.
  12. R. Goré. And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL. In Stéphane Demri, Deepak Kapur, and Christoph Weidenbach, editors, Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings, volume 8562 of Lecture Notes in Computer Science, pages 26-45. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08587-6_3.
  13. R. Goré. Tableau methods for modal and temporal logics. In Marcello D'Agostino, Dov M. Dov Gabbay, Reiner Hähnle, and Joachim Posegga, editors, Handbook of Tableau Methods, pages 297-396. Springer, Netherlands, Dordrecht, 1999. Google Scholar
  14. R. Kashima. An axiomatization of ECTL. J. Log. Comput., 24(1):117-133, 2014. URL: https://doi.org/10.1093/logcom/ext005.
  15. N. Markey. Temporal logics. Course notes, Master Parisien de Recherche en Informatique, Paris, France, 2013. URL: http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/NM-coursTL13.pdf.
  16. A. Mebsout and C. Tinelli. Proof certificates for SMT-based model checkers for infinite-state systems. In Proceedings of the 16th Conference on Formal Methods in Computer-Aided Design, FMCAD '16, pages 117-124, 2016. URL: https://doi.org/10.1109/FMCAD.2016.7886669.
  17. Stefan Schwendimann. A new one-pass tableau calculus for pltl. In International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pages 277-291. Springer, 1998. URL: https://doi.org/10.1007/3-540-69778-0_28.
  18. A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logics. J. ACM, 32(3):733-749, 1985. URL: https://doi.org/10.1145/3828.3837.
  19. P. Wolper. The tableau method for temporal logic: An overview. Logique Et Analyse, 28(110-111):119-136, 1985. 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