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

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

Thumbnail 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

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)


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
  • Temporal logic
  • fairness
  • expressiveness
  • branching-time


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


  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:
  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:
  3. M. Ben-Ari, A. Pnueli, and Z. Manna. The temporal logic of branching time. Acta Inf., 20(3):207–226, September 1983. URL:
  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:
  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:
  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:
  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:
  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:
  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:
  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:
  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:
  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:
  15. N. Markey. Temporal logics. Course notes, Master Parisien de Recherche en Informatique, Paris, France, 2013. URL:
  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:
  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:
  18. A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logics. J. ACM, 32(3):733-749, 1985. URL:
  19. P. Wolper. The tableau method for temporal logic: An overview. Logique Et Analyse, 28(110-111):119-136, 1985. Google Scholar