Document Open Access Logo

Automata-Theoretic Characterisations of Branching-Time Temporal Logics

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

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2024.128.pdf
  • Filesize: 0.85 MB
  • 20 pages

Document Identifiers

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

M. Benerecetti, F. Mogavero, and A. Peron are members of the Gruppo Nazionale Calcolo Scientifico-Istituto Nazionale di Alta Matematica (GNCS-INdAM). This work has been partially supported by the GNCS 2024 project "Certificazione, monitoraggio, ed interpretabilità in sistemi di intelligenza artificiale".

Cite AsGet BibTex

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). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 128:1-128:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ICALP.2024.128

Abstract

Characterisations theorems serve as important tools in model theory and can be used to assess and compare the expressive power of temporal languages used for the specification and verification of properties in formal methods. While complete connections have been established for the linear-time case between temporal logics, predicate logics, algebraic models, and automata, the situation in the branching-time case remains considerably more fragmented. In this work, we provide an automata-theoretic characterisation of some important branching-time temporal logics, namely CTL* and ECTL* interpreted on arbitrary-branching trees, by identifying two variants of Hesitant Tree Automata that are proved equivalent to those logics. The characterisations also apply to Monadic Path Logic and the bisimulation-invariant fragment of Monadic Chain Logic, again interpreted over trees. These results widen the characterisation landscape of the branching-time case and solve a forty-year-old open question.

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 Second-Order Logics
  • Tree Automata

Metrics

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

Related Versions

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. C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2008. Google Scholar
  3. 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
  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. M. Bojańczyk. The Finite Graph Problem for Two-Way Alternating Automata. TCS, 3(298):511-528, 2003. Google Scholar
  7. U. Boker and Y. Shaulian. Automaton-Based Criteria for Membership in CTL. In LICS'18, pages 155-164. ACM, 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. F. Carreiro, A. Facchini, Y. Venema, and F. Zanasi. Weak MSO: Automata and Expressiveness Modulo Bisimilarity. In CSL'14 & LICS'14, pages 27:1-27. ACM, 2014. Google Scholar
  12. F. Carreiro, A. Facchini, Y. Venema, and F. Zanasi. The Power of the Weak. TOCL, 21(2):15:1-47, 2020. Google Scholar
  13. F. Carreiro, A. Facchini, Y. Venema, and F. Zanasi. Model Theory of Monadic Predicate Logic with the Infinity Quantifier. AML, 61(3-4):465-502, 2022. Google Scholar
  14. Y. Choueka. Theories of Automata on ω-Tapes: A Simplified Approach. JCSS, 8(2):117-141, 1974. Google Scholar
  15. A. Church. Logic, Arithmetics, and Automata. In ICM'62, pages 23-35, 1963. Google Scholar
  16. 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
  17. E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. TOPLAS, 8(2):244-263, 1986. Google Scholar
  18. E.M. Clarke, O. Grumberg, and D.A. Peled. Model Checking. MIT Press, 2002. Google Scholar
  19. V. Diekert and P. Gastin. First-Order Definable Languages. In Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas], volume 2 of Texts in Logic and Games, pages 261-306. Amsterdam University Press, 2008. Google Scholar
  20. C.C. Elgot. Decision Problems of Finite Automata Design and Related Arithmetics. TAMS, 98:21-51, 1961. Google Scholar
  21. 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
  22. E.A. Emerson and E.M. Clarke. Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons. SCP, 2(3):241-266, 1982. Google Scholar
  23. 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
  24. E.A. Emerson and J.Y. Halpern. Decision Procedures and Expressiveness in the Temporal Logic of Branching Time. JCSS, 30(1):1-24, 1985. Google Scholar
  25. 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
  26. E.A. Emerson and C.S. Jutla. Tree Automata, muCalculus, and Determinacy. In FOCS'91, pages 368-377. IEEECS, 1991. Google Scholar
  27. E.A. Emerson, C.S. Jutla, and A.P. Sistla. On Model Checking for the muCalculus and its Fragments. TCS, 258(1-2):491-522, 2001. Google Scholar
  28. A. Facchini, Y. Venema, and F. Zanasi. A Characterization Theorem for the Alternation-Free Fragment of the Modal μ-Calculus. In LICS'13, pages 478-487. IEEECS, 2013. Google Scholar
  29. K. Fine. In So Many Possible Worlds. NDJFL, 13:516-520, 1972. Google Scholar
  30. M.J. Fischer and R.E. Ladner. Propositional Dynamic Logic of Regular Programs. JCSS, 18(2):194-211, 1979. Google Scholar
  31. D.M. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the Temporal Basis of Fairness. In POPL'80, pages 163-173. ACM, 1980. Google Scholar
  32. 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
  33. Y. Gurevich and S. Shelah. The Decision Problem for Branching Time Logic. JSL, 50(3):668-681, 1985. Google Scholar
  34. 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. Google Scholar
  35. D. Harel, D. Kozen, and J. Tiuryn. Dynamic Logic. MIT Press, 2000. Google Scholar
  36. D. Janin. A Contribution to Formal Methods: Games, Logic and Automata. Habilitation thesis, Université Bordeaux I, Bordeaux, France, 2005. Google Scholar
  37. 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. Google Scholar
  38. 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. Google Scholar
  39. H.W. Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, University of California, Los Angeles, CA, USA, 1968. Google Scholar
  40. R.M. Keller. Formal Verification of Parallel Programs. CACM, 19(7):371-384, 1976. Google Scholar
  41. S.C. Kleene. Representation of Events in Nerve Nets and Finite Automata. In Automata Studies, pages 3-42. Princeton University Press, 1956. Google Scholar
  42. D. Kozen. Results on the Propositional muCalculus. TCS, 27(3):333-354, 1983. Google Scholar
  43. S.A. Kripke. Semantical Considerations on Modal Logic. APF, 16:83-94, 1963. Google Scholar
  44. O. Kupferman, U. Sattler, and M.Y. Vardi. The Complexity of the Graded muCalculus. In CADE'02, LNCS 2392, pages 423-437. Springer, 2002. Google Scholar
  45. O. Kupferman and M.Y. Vardi. Freedom, Weakness, and Determinism: From Linear-Time to Branching-Time. In LICS'98, pages 81-92. IEEECS, 1998. Google Scholar
  46. O. Kupferman and M.Y. Vardi. Weak Alternating Automata are not That Weak. TOCL, 2(3):408-429, 2001. Google Scholar
  47. O. Kupferman, M.Y. Vardi, and P. Wolper. An Automata Theoretic Approach to Branching-Time Model Checking. JACM, 47(2):312-360, 2000. Google Scholar
  48. R.E. Ladner. Application of Model Theoretic Games to Discrete Linear Orders and Finite Automata. IC, 33(4):281-303, 1977. Google Scholar
  49. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer, 1992. Google Scholar
  50. Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems - Safety. Springer, 1995. Google Scholar
  51. R. McNaughton. Testing and Generating Infinite Sequences by a Finite Automaton. IC, 9(5):521-530, 1966. Google Scholar
  52. R. McNaughton and S. Papert. Counter-Free Automata. MIT Press, 1971. Google Scholar
  53. S. Miyano and T. Hayashi. Alternating Finite Automata on ω-Words. TCS, 32(3):321-330, 1984. Google Scholar
  54. F. Moller and A.M. Rabinovich. On the Expressive Power of CTL*. In LICS'99, pages 360-368. IEEECS, 1999. Google Scholar
  55. F. Moller and A.M. Rabinovich. Counting on CTL*: On the Expressive Power of Monadic Path Logic. IC, 184(1):147-159, 2003. Google Scholar
  56. E.F. Moore. Gedanken-Experiments on Sequential Machines. In Automata Studies, pages 129-154. Princeton University Press, 1956. Google Scholar
  57. A. Nerode. Linear Automaton Transformations. PAMS, 9(4):541-544, 195. Google Scholar
  58. D. Perrin. Recent Results on Automata and Infinite Words. In MFCS'84, LNCS 176, pages 134-148. Springer, 1984. Google Scholar
  59. D. Perrin and J. Pin. First-Order Logic and Star-Free Sets. JCSS, 32(3):393-406, 1986. Google Scholar
  60. D. Perrin and J. Pin. Infinite Words. Pure and Applied Mathematics. Elsevier, 2004. Google Scholar
  61. A. Pnueli. The Temporal Logic of Programs. In FOCS'77, pages 46-57. IEEECS, 1977. Google Scholar
  62. A. Pnueli. The Temporal Semantics of Concurrent Programs. TCS, 13:45-60, 1981. Google Scholar
  63. A. Pnueli and R. Rosner. On the Synthesis of a Reactive Module. In POPL'89, pages 179-190. ACM, 1989. Google Scholar
  64. M.O. Rabin. Decidability of Second-Order Theories and Automata on Infinite Trees. TAMS, 141:1-35, 1969. Google Scholar
  65. 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
  66. M.O. Rabin and D.S. Scott. Finite Automata and their Decision Problems. IBMJRD, 3:115-125, 1959. Google Scholar
  67. A. Rabinovich. A Proof of Kamp’s Theorem. In CSL'12, LIPIcs 16, pages 516-527. Leibniz-Zentrum fuer Informatik, 2012. Google Scholar
  68. A. Rabinovich. A Proof of Kamp’s Theorem. LMCS, 10(1):1-16, 2014. Google Scholar
  69. R. Rosner. Modular Synthesis of Reactive Systems. PhD thesis, Weizmann Institute of Science, Rehovot, Israel, 1992. Google Scholar
  70. M.P. Schützenberger. On Finite Monoids Having Only Trivial Subgroups. IC, 8(2):190-194, 1965. Google Scholar
  71. W. Thomas. Star-Free Regular Sets of ω-Sequences. IC, 42(2):148-156, 1979. Google Scholar
  72. W. Thomas. A Combinatorial Approach to the Theory of ω-Automata. IC, 48(3):261-283, 1981. Google Scholar
  73. W. Thomas. Logical Aspects in the Study of Tree Languages. In CAAP'84, pages 31-50. CUP, 1984. Google Scholar
  74. W. Thomas. On Chain Logic, Path Logic, and First-Order Logic over Infinite Trees. In LICS'87, pages 245-256. IEEECS, 1987. Google Scholar
  75. W. Thomas. Automata on Infinite Objects. In Handbook of Theoretical Computer Science (vol. B), pages 133-191. MIT Press, 1990. Google Scholar
  76. B.A. Trakhtenbrot. Finite Automata and the Logic of One-Place Predicates. AMST, 59:23-55, 1966. Google Scholar
  77. J. van Benthem. Modal Correspondence Theory. PhD thesis, University of Amsterdam, Amsterdam, Netherlands, 1977. Google Scholar
  78. M.Y. Vardi. Reasoning about The Past with Two-Way Automata. In ICALP'98, LNCS 1443, pages 628-641. Springer, 1998. Google Scholar
  79. M.Y. Vardi and L.J. Stockmeyer. Improved Upper and Lower Bounds for Modal Logics of Programs: Preliminary Report. In STOC'85, pages 240-251. ACM, 1985. Google Scholar
  80. M.Y. Vardi and P. Wolper. Yet Another Process Logic. In LP'83, LNCS 164, pages 501-512. Springer, 1984. Google Scholar
  81. M.Y. Vardi and P. Wolper. Automata-Theoretic Techniques for Modal Logics of Programs. JCSS, 32(2):183-221, 1986. Google Scholar
  82. I. Walukiewicz. Monadic Second Order Logic on Tree-Like Structures. TCS, 275(1-2):311-346, 2002. Google Scholar
  83. A. Weinert and M. Zimmermann. Visibly Linear Dynamic Logic. TCS, 747:100-117, 2018. Google Scholar
  84. P. Wolper. Temporal Logic Can Be More Expressive. IC, 56(1-2):72-99, 1983. 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