Document Open Access Logo

Full Characterisation of Extended CTL*

Authors Massimo Benerecetti , Laura Bozzelli , Fabio Mogavero , Adriano Peron

PDF

File

Thumbnail PDF
PDF
LIPIcs.TIME.2024.18.pdf
  • Filesize: 0.86 MB
  • 18 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Tree languages
Keywords
  • Branching-Time Temporal Logics
  • Monadic Chain Logic
  • Tree Automata

Metrics

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

Abstract

The precise identification of the expressive power of logic languages used in formal methods for specifying and verifying run-time properties of critical systems is a fundamental task and characterisation theorems play a crucial role as model-theoretic tools in this regard. While a clear picture of the expressive power of linear-time temporal logics in terms of word automata and predicate logics has long been established, a complete mapping of the corresponding relationships for branching-time temporal logics has proven to be a more elusive task over the past four decades with few scattered results. Only recently, an automata-theoretic characterisation of both CTL* and its full-ω-regular extension ECTL* has been provided in terms of Symmetric Hesitant Tree Automata (HTA), with and without a suitable counter-freeness restriction on their linear behaviours. These two temporal logics also correspond to the bisimulation-invariant semantic fragments of Monadic Path Logic (MPL) and Monadic Chain Logic (MCL), respectively. Additionally, it has been proven that the counting extensions of CTL* and ECTL*, namely CCTL* and CECTL*, enjoy equivalent graded versions of the HTAs for the corresponding non-counting logics. However, while Moller and Rabinovich have proved CCTL* to be equivalent to full MPL, thus filling the gap for the standard branching-time logic, no similar result has been given for CECTL*. This work completes the picture, by proving the expressive equivalence of CECTL* and full MCL, by means of a composition theorem for the latter logic. This also indirectly establishes the equivalence between HTAs and their first-order extensions HFTAs, as originally introduced by Walukiewicz.

Cite As Get BibTex

Massimo Benerecetti, Laura Bozzelli, Fabio Mogavero, and Adriano Peron. Full Characterisation of Extended CTL*. In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.TIME.2024.18

Author Details

Massimo Benerecetti
  • Università di Napoli Federico II, Italy
Laura Bozzelli
  • Università di Napoli Federico II, Italy
Fabio Mogavero
  • Università di Napoli Federico II, Italy
Adriano Peron
  • Università di Trieste, Italy

Funding

Indam GNCS 2024 project "Certificazione, Monitoraggio, ed Interpretabilità in Sistemi di Intelligenza Artificiale". M. Benerecetti, F. Mogavero, and A. Peron are members of the Gruppo Nazionale Calcolo Scientifico-Istituto Nazionale di Alta Matematica (GNCS-INdAM).

References

  1. A. Arnold and D. Niwiński. Fixed Point Characterization of Weak Monadic Logic Definable Sets of Trees. In Tree Automata and Languages, pages 159-188. North-Holland, 1992. 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. IEEECS, 2023. Google Scholar
  3. M. Benerecetti, L. Bozzelli, F. Mogavero, and A. Peron. Automata-Theoretic Characterisations of Branching-Time Temporal Logics. In ICALP'24, LIPIcs 297, pages 128:1-20. Leibniz-Zentrum fuer Informatik, 2024. Google Scholar
  4. M. Benerecetti, F. Mogavero, and A. Murano. Substructure Temporal Logic. In LICS'13, pages 368-377. IEEECS, 2013. Google Scholar
  5. M. Benerecetti, F. Mogavero, and A. Murano. Reasoning About Substructures and Games. TOCL, 16(3):25:1-46, 2015. Google Scholar
  6. U. Boker, K. Lehtinen, and S. Sickert. On the Translation of Automata to Linear Temporal Logic. In FOSSACS'22, LNCS 13242, pages 140-160. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99253-8_8.
  7. J.R. Büchi. Weak Second-Order Arithmetic and Finite Automata. MLQ, 6(1-6):66-92, 1960. Google Scholar
  8. 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
  9. 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
  10. Y. Choueka. Theories of Automata on ω-Tapes: A Simplified Approach. JCSS, 8(2):117-141, 1974. Google Scholar
  11. E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach. In POPL'83, pages 117-126. ACM, 1983. Google Scholar
  12. E.A. Emerson and E.M. Clarke. Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. In LP'81, LNCS 131, pages 52-71. Springer, 1982. Google Scholar
  13. E.A. Emerson and J.Y. Halpern. "Sometimes" and "Not Never" Revisited: On Branching Versus Linear Time. In POPL'83, pages 127-140. ACM, 1983. Google Scholar
  14. 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
  15. S. Feferman and R. Vaught. The First-Order Properties of Products of Algebraic Systems. FM, 47(1):57-103, 1959. Google Scholar
  16. K. Fine. In So Many Possible Worlds. NDJFL, 13:516-520, 1972. URL: https://doi.org/10.1305/NDJFL/1093890715.
  17. M.J. Fischer and R.E. Ladner. Propositional Dynamic Logic of Regular Programs. JCSS, 18(2):194-211, 1979. URL: https://doi.org/10.1016/0022-0000(79)90046-1.
  18. G. De Giacomo and M.Y. Vardi. Linear Temporal Logic and Linear Dynamic Logic on Finite Traces. In IJCAI'13, pages 854-860. IJCAI' & AAAI Press, 2013. Google Scholar
  19. Y. Gurevich. Modest Theory of Short Chains. I. JSL, 44(4):481-490, 1979. URL: https://doi.org/10.2307/2273287.
  20. Y. Gurevich. Monadic Second-Order Theories. In Model-Theoretical Logics, pages 479-506. Springer, 1985. Google Scholar
  21. Y. Gurevich and S. Shelah. Modest Theory of Short Chains. II. JSL, 44(4):491-502, 1979. URL: https://doi.org/10.2307/2273288.
  22. Y. Gurevich and S. Shelah. Rabin’s Uniformization Problem. JSL, 48(4):1105-1119, 1979. Google Scholar
  23. Y. Gurevich and S. Shelah. The Decision Problem for Branching Time Logic. JSL, 50(3):668-681, 1985. URL: https://doi.org/10.2307/2274321.
  24. 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.
  25. D. Janin. A Contribution to Formal Methods: Games, Logic and Automata. Habilitation thesis, Université Bordeaux I, Bordeaux, France, 2005. Google Scholar
  26. D. Janin and G. Lenzi. On the Relationship Between Monadic and Weak Monadic Second Order Logic on Arbitrary Trees, with Applications to the mu-Calculus. FI, 61(3-4):247-265, 2004. URL: http://content.iospress.com/articles/fundamenta-informaticae/fi61-3-4-04.
  27. 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.
  28. H.W. Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, University of California, Los Angeles, CA, USA, 1968. Google Scholar
  29. D. Kozen. Results on the Propositional muCalculus. TCS, 27(3):333-354, 1983. URL: https://doi.org/10.1016/0304-3975(82)90125-6.
  30. 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.
  31. 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
  32. O. Maler and A. Pnueli. On the Cascaded Decomposition of Automata, its Complexity, and its Application to Logic. Unpublished, 1995. Google Scholar
  33. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer, 1992. Google Scholar
  34. Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems - Safety. Springer, 1995. Google Scholar
  35. 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.
  36. R. McNaughton and S. Papert. Counter-Free Automata. MIT Press, 1971. Google Scholar
  37. F. Moller and A.M. Rabinovich. On the Expressive Power of CTL*. In LICS'99, pages 360-368. IEEECS, 1999. Google Scholar
  38. 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.
  39. 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.
  40. A. Pnueli. The Temporal Logic of Programs. In FOCS'77, pages 46-57. IEEECS, 1977. Google Scholar
  41. A. Pnueli. The Temporal Semantics of Concurrent Programs. TCS, 13:45-60, 1981. URL: https://doi.org/10.1016/0304-3975(81)90110-9.
  42. S. Safra. On the Complexity of ω-Automata. In FOCS'88, pages 319-327. IEEECS, 1988. Google Scholar
  43. S. Shelah. The Monadic Theory of Order. AM, 102(3):379-419, 1975. Google Scholar
  44. W. Thomas. Star-Free Regular Sets of ω-Sequences. IC, 42(2):148-156, 1979. Google Scholar
  45. W. Thomas. A Combinatorial Approach to the Theory of ω-Automata. IC, 48(3):261-283, 1981. Google Scholar
  46. W. Thomas. Logical Aspects in the Study of Tree Languages. In CAAP'84, pages 31-50. CUP, 1984. Google Scholar
  47. W. Thomas. On Chain Logic, Path Logic, and First-Order Logic over Infinite Trees. In LICS'87, pages 245-256. IEEECS, 1987. Google Scholar
  48. W. Thomas. Automata on Infinite Objects. In Handbook of Theoretical Computer Science (vol. B), pages 133-191. MIT Press, 1990. Google Scholar
  49. J. van Benthem. Modal Correspondence Theory. PhD thesis, University of Amsterdam, Amsterdam, Netherlands, 1977. Google Scholar
  50. M.Y. Vardi and P. Wolper. Yet Another Process Logic. In LP'83, LNCS 164, pages 501-512. Springer, 1984. Google Scholar
  51. I. Walukiewicz. Monadic Second Order Logic on Tree-Like Structures. TCS, 275(1-2):311-346, 2002. URL: https://doi.org/10.1016/S0304-3975(01)00185-2.
  52. 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.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact