Document Open Access Logo

Deciding the Common Fragment of CTL with past and LTL

Authors Massimo Benerecetti , Dario Della Monica , Angelo Matteo , Fabio Mogavero , Gabriele Puppis

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2026.29.pdf
  • Filesize: 0.83 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Tree languages
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Logic and verification
  • Theory of computation → Automata over infinite objects
Keywords
  • Membership problems
  • tree languages
  • tree logics
  • tree automata
  • Monadic Path Logic
  • CTL^*
  • CTL with past

Metrics

Abstract

A central goal of language theory is to compare formalisms by understanding both their expressive overlaps and their relative expressive power. One particularly challenging question in this direction is the problem of determining the common fragment of two formalisms F₁ and F₂, that is, effectively characterise the class F₁∩ F₂ of properties that can be expressed in both formalisms. This question can be equally phrased as a decision problem: given a property expressed in F₁ or F₂, decide whether the same property can be also expressed in F₁∩ F₂. A question closely related to this is the membership problem, denoted F₁ ↦ F₂, which asks whether a property expressed in F₁ can be also expressed in F₂. These problems become particularly difficult when branching-time formalisms are involved, in general due to the lack of equivalent algebraic characterizations.
In this work, we prove that LTL ∩ PCTL is decidable, where PCTL denotes CTL extended with past operators. We do this by showing that both membership problems, LTL ↦ PCTL and PCTL ↦ LTL, are decidable. The direction PCTL ↦ LTL follows from suitable combinations of known results. The converse direction, LTL ↦ PCTL, requires an automata-theoretic characterisation of PCTL. Specifically, we introduce a new class of automata, called counter-free hesitant weak tree automata (HWT_cf) that capture precisely the expressiveness of PCTL, and that are obtained by combining two orthogonal restrictions on alternating parity tree automata, namely, counter-free hesitancy and weakness. We then prove that, for every word language L defined by an LTL formula, the associated tree language △[L] is recognisable by an HWT_cf if and only if L is recognized by a deterministic Büchi word automaton. Since the latter recognisability problem is known to be decidable, so is the former.
This result advances the longstanding open problem of deciding LTL ∩ CTL. Indeed, that problem can now be reduced to PCTL ↦ CTL, that is, the question of when past operators can be eliminated.

Cite As Get BibTex

Massimo Benerecetti, Dario Della Monica, Angelo Matteo, Fabio Mogavero, and Gabriele Puppis. Deciding the Common Fragment of CTL with past and LTL. In 51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 386, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.MFCS.2026.29

Author Details

Massimo Benerecetti
  • Università degli Studi di Napoli "Federico II", Italy
Dario Della Monica
  • Università degli Studi di Udine, Italy
Angelo Matteo
  • Università degli Studi di Udine, Italy
Fabio Mogavero
  • Università degli Studi di Napoli "Federico II", Italy
Gabriele Puppis
  • Università degli Studi di Udine, Italy

Funding

This work was partially supported by the INdAM-GNCS Project "Neurosymbolic semantic contract for rigorous reachability and certificates in cyber-physical systems (CPS)" (CUP: E53C25002010001), Unione europea-Next Generation EU, Missione 4 Componente 1 (CUP: C63C22000770006), and Unione europea-Next Generation EU, Missione 4 Componente 1 (CUP: D33C22001300002).

References

  1. P. Balbiani and E. Lorini. Ockhamist Propositional Dynamic Logic: a natural link between PDL and CTL. In International Workshop on Logic, Language, Information, and Computation, pages 251-265. Springer, 2013. Google Scholar
  2. M. Benerecetti, L. Bozzelli, F. Mogavero, and A. Peron. Quantifying over Trees in Monadic Second-Order Logic. In LICS'23, pages 1-13. IEEE Computer Society, 2023. Google Scholar
  3. M. Benerecetti, D. Della Monica, A. Matteo, F. Mogavero, and G. Puppis. An Automaton-Based Characterisation of First-Order Logic over Infinite Trees. In GANDALF'25, EPTCS 428, pages 45-61, 2025. Google Scholar
  4. Massimo Benerecetti, Laura Bozzelli, Fabio Mogavero, and Adriano Peron. Automata-Theoretic Characterisations of Branching-Time Temporal Logics. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024), volume 297 of Leibniz International Proceedings in Informatics (LIPIcs), pages 128:1-128:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.ICALP.2024.128.
  5. M. Bojańczyk. The Common Fragment of ACTL and LTL. In FOSSACS'08, LNCS 4962, pages 172-185. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78499-9_13.
  6. Mikołaj Bojańczyk. The common fragment of actl and ltl. In International Conference on Foundations of Software Science and Computational Structures, pages 172-185. Springer, 2008. Google Scholar
  7. U. Boker and Y. Shaulian. Automaton-Based Criteria for Membership in CTL. In LICS'18, pages 155-164. Association for Computing Machinery, 2018. Google Scholar
  8. J.R. Büchi. Weak Second-Order Arithmetic and Finite Automata. MLQ, 6(1-6):66-92, 1960. Google Scholar
  9. J.R. Büchi. On a Decision Method in Restricted Second-Order Arithmetic. In ICLMPS'62, pages 1-11. Stanford University Press, 1962. Google Scholar
  10. J.R. Büchi. On a Decision Method in Restricted Second Order Arithmetic. In Studies in Logic and the Foundations of Mathematics, volume 44, pages 1-11. Elsevier, 1966. Google Scholar
  11. Edward Chang, Zohar Manna, and Amir Pnueli. Characterization of temporal property classes. In International Colloquium on Automata, Languages, and Programming, pages 474-486. Springer, 1992. URL: https://doi.org/10.1007/3-540-55719-9_97.
  12. Y. Choueka. Theories of Automata on ω-Tapes: A Simplified Approach. JCSS, 8(2):117-141, 1974. Google Scholar
  13. E.M. Clarke and I.A. Draghicescu. Expressibility Results for Linear-Time and Branching-Time Logics. In REX'88, LNCS 354, pages 428-437. Springer, 1988. URL: https://doi.org/10.1007/BFb0013029.
  14. Thomas Colcombet, Denis Kuperberg, Christof Löding, and Michael Vanden Boom. Deciding the weak definability of büchi definable tree languages. In CSL, 2013. Google Scholar
  15. Thomas Colcombet and Christof Löding. The non-deterministic mostowski hierarchy and distance-parity automata. In International Colloquium on Automata, Languages, and Programming, pages 398-409. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-70583-3_33.
  16. E.A. Emerson and J.Y. Halpern. "Sometimes" and "Not Never" Revisited: On Branching Versus Linear Time. JACM, 33(1):151-178, 1986. Google Scholar
  17. T. Hafer and W. Thomas. Computation Tree Logic CTL* and Path Quantifiers in the Monadic Theory of the Binary Tree. In ICALP'87, LNCS 267, pages 269-279. Springer, 1987. URL: https://doi.org/10.1007/3-540-18088-5_22.
  18. Olivier Idir and Karoliina Lehtinen. Using games and universal trees to characterise the nondeterministic index of tree languages. arXiv preprint arXiv:2504.16819, 2025. URL: https://doi.org/10.48550/arXiv.2504.16819.
  19. D. Janin and I. Walukiewicz. On the Expressive Completeness of the Propositional mu-Calculus with Respect to Monadic Second Order Logic. In CONCUR'96, LNCS 1119, pages 263-277. Springer, 1996. URL: https://doi.org/10.1007/3-540-61604-7_60.
  20. H.W. Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, University of California, Los Angeles, CA, USA, 1968. Google Scholar
  21. D. Kozen. Results on the Propositional muCalculus. TCS, 27(3):333-354, 1983. URL: https://doi.org/10.1016/0304-3975(82)90125-6.
  22. O. Kupferman and M.Y. Vardi. Weak Alternating Automata and Tree Automata Emptiness. In STOC'98, pages 224-233. Association for Computing Machinery, 1998. Google Scholar
  23. O. Kupferman and M.Y. Vardi. From Linear Time to Branching Time. TOCL, 6(2):273-294, 2005. URL: https://doi.org/10.1145/1055686.1055689.
  24. Orna Kupferman, Shmuel Safra, and Moshe Y Vardi. Relating word and tree automata. Annals of Pure and Applied Logic, 138(1-3):126-146, 2006. URL: https://doi.org/10.1016/j.apal.2005.06.009.
  25. R.E. Ladner. Application of Model Theoretic Games to Discrete Linear Orders and Finite Automata. IC, 33(4):281-303, 1977. URL: https://doi.org/10.1016/S0019-9958(77)90443-0.
  26. François Laroussinie and Ph Schnoebelen. A hierarchy of temporal logics with past. Theoretical Computer Science, 148(2):303-324, 1995. URL: https://doi.org/10.1016/0304-3975(95)00035-U.
  27. H. Läuchli. A Decision Procedure for the Weak Second-Order Theory of Linear Order. In LC'66, volume 50, pages 189-197. North-Holland, 1968. Google Scholar
  28. M. Maidi. The Common Fragment of CTL and LTL. In FOCS'00, pages 643-652. IEEE Computer Society, 2000. URL: https://doi.org/10.1109/SFCS.2000.892332.
  29. R. McNaughton. Testing and Generating Infinite Sequences by a Finite Automaton. IC, 9(5):521-530, 1966. URL: https://doi.org/10.1016/S0019-9958(66)80013-X.
  30. R. McNaughton and S. Papert. Counter-Free Automata. MIT Press, 1971. Google Scholar
  31. F. Moller and A.M. Rabinovich. On the Expressive Power of CTL*. In LICS'99, pages 360-368. IEEE Computer Society, 1999. URL: https://doi.org/10.1109/LICS.1999.782631.
  32. F. Moller and A.M. Rabinovich. Counting on CTL*: On the Expressive Power of Monadic Path Logic. IC, 184(1):147-159, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00104-4.
  33. A.W. Mostowski. Regular Expressions for Infinite Trees and a Standard Form of Automata. In SCT'84, LNCS 208, pages 157-168. Springer, 1984. URL: https://doi.org/10.1007/3-540-16066-3_15.
  34. David E. Muller and Paul E. Schupp. Alternating automata on infinite trees. Theoretical Computer Science, 54:267-276, 1987. URL: https://doi.org/10.1016/0304-3975(87)90133-2.
  35. D.E. Muller, A. Saoudi, and P.E. Schupp. Alternating Automata, the Weak Monadic Theory of Trees and its Complexity. TCS, 97(2):233-244, 1992. URL: https://doi.org/10.1016/0304-3975(92)90076-R.
  36. D. Perrin and J. Pin. First-Order Logic and Star-Free Sets. JCSS, 32(3):393-406, 1986. URL: https://doi.org/10.1016/0022-0000(86)90037-1.
  37. D. Perrin and J. Pin. Infinite Words. Pure and Applied Mathematics. Elsevier, 2004. Google Scholar
  38. Dominique Perrin and Jean-Éric Pin. Semigroups and automata on infinite words. NATO ASI Series C Mathematical and Physical Sciences-Advanced Study Institute, 466:49-72, 1995. Google Scholar
  39. A. Pnueli. The Temporal Logic of Programs. In FOCS'77, pages 46-57. IEEE Computer Society, 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  40. A. Pnueli. The Temporal Semantics of Concurrent Programs. TCS, 13:45-60, 1981. URL: https://doi.org/10.1016/0304-3975(81)90110-9.
  41. A. Prior. Past, Present and Future. Oxford University Press, 1967. Google Scholar
  42. Michael O Rabin. Weakly definable relations and special automata. In Studies in Logic and the Foundations of Mathematics, volume 59, pages 1-23. Elsevier, 1970. Google Scholar
  43. M.O. Rabin. Decidability of Second-Order Theories and Automata on Infinite Trees. TAMS, 141:1-35, 1969. Google Scholar
  44. M.O. Rabin. Weakly Definable Relations and Special Automata. In Studies in Logic and the Foundations of Mathematics, volume 59, pages 1-23. Elsevier, 1970. Google Scholar
  45. M.P. Schützenberger. On Finite Monoids Having Only Trivial Subgroups. IC, 8(2):190-194, 1965. URL: https://doi.org/10.1016/S0019-9958(65)90108-7.
  46. W. Thomas. Logical Aspects in the Study of Tree Languages. In CAAP'84, pages 31-50. Cambridge University Press, 1984. Google Scholar
  47. W. Thomas. Ehrenfeucht Games, the Composition Method, and the Monadic Theory of Ordinal Words. In Structures in Logic and Computer Science: A Selection of Essays in Honor of A. Ehrenfeucht, pages 118-143. Springer, 1997. URL: https://doi.org/10.1007/3-540-63246-8_8.
  48. T. Wilke. Alternating Tree Automata, Parity Games, and Modal muCalculus. BBMS, 8(2):359-391, 2001. Google Scholar
  49. P. Wolper. Temporal Logic Can Be More Expressive. IC, 56(1-2):72-99, 1983. URL: https://doi.org/10.1016/S0019-9958(83)80051-5.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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