Document Open Access Logo

Arbitrary-Arity Tree Automata for QCTL

Authors François Laroussinie , Nicolas Markey

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2025.28.pdf
  • Filesize: 1.21 MB
  • 20 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Model-checking
  • Verification
  • Automata theory
  • Quantified CTL

Metrics

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

Abstract

We introduce a new class of automata (which we coin EU-automata) running on infinite trees of arbitrary (finite) arity. We develop and study several algorithms to perform classical operations (union, intersection, complement, projection, alternation removal) for those automata, and precisely characterise their complexities. We also develop algorithms for solving membership and emptiness for the languages of trees accepted by EU-automata. We then use EU-automata to obtain several algorithmic and expressiveness results for the temporal logics QCTL and QCTL* (which extends CTL and CTL* with quantification over atomic propositions) and for MSO.

Cite As Get BibTex

François Laroussinie and Nicolas Markey. Arbitrary-Arity Tree Automata for QCTL. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CONCUR.2025.28

Author Details

François Laroussinie
  • IRIF, Université Paris Cité, France
Nicolas Markey
  • IRISA – Inria, CNRS, Univ. Rennes 1, France

Acknowledgements

We thank Igor Walukiewicz for answering our questions on MSO-automata, and the reviewers for their careful reading and constructive comments.

References

  1. Orna Bernholtz and Orna Grumberg. Branching time temporal logic and 𝒜 m o r p ℋ O u s tree automata. In Eike Best, editor, Proceedings of the 4th International Conference on Concurrency Theory (CONCUR'93), volume 715 of Lecture Notes in Computer Science, pages 262-277. Springer-Verlag, 1993. Google Scholar
  2. Orna Bernholtz, Moshe Y. Vardi, and Pierre Wolper. An automata-theoretic approach to branching-time model checking (extended abstract). In David L. Dill, editor, Proceedings of the 6th International Conference on Computer Aided Verification (CAV'94), volume 818 of Lecture Notes in Computer Science, pages 142-155. Springer-Verlag, 1994. URL: https://doi.org/10.1007/3-540-58179-0_50.
  3. Mikołaj Bojańczyk. Tree-walking automata. In Carlos Martín-Vide, Friedrich Otto, and Henning Fernau, editors, Revised Papers of the 2nd International Conference on Language and Automata Theory and Applications (LATA'08), volume 5196 of Lecture Notes in Computer Science, pages 1-2. Springer-Verlag, 2008. URL: https://doi.org/10.1007/978-3-540-88282-4_1.
  4. Julius R. Büchi. On a decision method in restricted second order arithmetic. In Ernest Nagel, Patrick Suppes, and Alfred Tarski, editors, Proceedings of the 1960 International Congress on Logic, Methodology and Philosophy of Science (LMPS'60), pages 1-11. Stanford University Press, 1962. Google Scholar
  5. Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasipolynomial time. In Hamed Hatami and Pierre McKenzie, editors, Proceedings of the 49th Annual ACM Symposium on the Theory of Computing (STOC'17), pages 252-263. ACM Press, 2017. URL: https://doi.org/10.1145/3055399.305540.
  6. Hubert Comon, Max Dauchet, Rémi Gilleron, Florent Jacquemard, Denis Lugiez, Christof Löding, Sophie Tison, and Marc Tommasi. Tree automata techniques and applications. Technical Report hal-03367725, H.A.L., 2008. Google Scholar
  7. Arnaud Da Costa, François Laroussinie, and Nicolas Markey. Quantified CTL: Expressiveness and model checking. In Maciej Koutny and Irek Ulidowski, editors, Proceedings of the 23rd International Conference on Concurrency Theory (CONCUR'12), volume 7454 of Lecture Notes in Computer Science, pages 177-192. Springer-Verlag, 2012. URL: https://doi.org/10.1007/978-3-642-32940-1_14.
  8. Calvin C. Elgot. Decision problems of finite automata design and related arithmetics. Transactions of the American Mathematical Society, 98(1):21-51, 1961. URL: https://doi.org/10.2307/1993511.
  9. E. Allen Emerson and Charanjit S. Jutla. Tree automata, mu-calculus and determinacy. In Proceedings of the 32nd Annual Symposium on Foundations of Computer Science (FOCS'91), pages 368-377. IEEE Comp. Soc. Press, 1991. URL: https://doi.org/10.1109/SFCS.1991.185392.
  10. E. Allen Emerson and A. Prasad Sistla. Deciding full branching time logic. Information and Control, 61(3):175-201, 1984. URL: https://doi.org/10.1016/S0019-9958(84)80047-9.
  11. Tim French. Decidability of quantified propositional branching time logics. In Markus Stumptner, Dan Corbett, and Mike Brooks, editors, Proceedings of the 14th Australian Joint Conference on Artificial Intelligence (AJCAI'01), volume 2256 of Lecture Notes in Computer Science, pages 165-176. Springer-Verlag, 2001. URL: https://doi.org/10.1007/3-540-45656-2_15.
  12. Tim French. Bisimulation Quantifiers for Modal Logics. PhD thesis, School of Computer Science & Software Engineering, University of Western Australia, 2006. Google Scholar
  13. David Janin and Igor Walukiewicz. Automata for the modal μ-calculus and related results. In Jirí Wiedermann and Petr Hájek, editors, Proceedings of the 20th International Symposium on Mathematical Foundations of Computer Science (MFCS'95), volume 969 of Lecture Notes in Computer Science, pages 552-562. Springer-Verlag, 1995. URL: https://doi.org/10.1007/3-540-60246-1_160.
  14. Orna Kupferman. Augmenting branching temporal logics with existential quantification over atomic propositions. In Pierre Wolper, editor, Proceedings of the 7th International Conference on Computer Aided Verification (CAV'95), volume 939 of Lecture Notes in Computer Science, pages 325-338. Springer-Verlag, 1995. URL: https://doi.org/10.1007/3-540-60045-0_60.
  15. Orna Kupferman, Parthasarathy Madhusudan, P. S. Thiagarajan, and Moshe Y. Vardi. Open systems in reactive environments: Control and synthesis. In Catuscia Palamidessi, editor, Proceedings of the 11th International Conference on Concurrency Theory (CONCUR'00), volume 1877 of Lecture Notes in Computer Science, pages 92-107. Springer-Verlag, 2000. URL: https://doi.org/10.1007/3-540-44618-4_9.
  16. Orna Kupferman and Moshe Y. Vardi. Π₂∩Σ₂ ≡ AFMC. In Jos C. M. Baeten, Jan Karel Lenstra, Joachim Parrow, and Gerhard J. Woeginger, editors, Proceedings of the 30th International Colloquium on Automata, Languages and Programming (ICALP'03), volume 2719 of Lecture Notes in Computer Science, pages 697-713. Springer-Verlag, 2003. Google Scholar
  17. François Laroussinie and Nicolas Markey. Arbitrary-arity tree automata and QCTL, 2024. URL: https://doi.org/10.48550/arXiv.2410.18799.
  18. François Laroussinie and Nicolas Markey. Quantified CTL: expressiveness and complexity. Logical Methods in Computer Science, 10(4), 2014. URL: https://doi.org/10.2168/LMCS-10(4:17)2014.
  19. François Laroussinie, Nicolas Markey, and Philippe Schnoebelen. Temporal logic with forgettable past. In Proceedings of the 17th Annual Symposium on Logic in Computer Science (LICS'02), pages 383-392. IEEE Comp. Soc. Press, 2002. URL: https://doi.org/10.1109/LICS.2002.1029846.
  20. Christof Löding. Automata on infinite trees. In Jean-Éric Pin, editor, Handbook of automata theory, volume 1, chapter 8, pages 265-302. EMS Press, 2021. URL: https://doi.org/10.4171/AUTOMATA-1/8.
  21. Robert McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9(6):521-530, 1966. URL: https://doi.org/10.1016/S0019-9958(66)80013-X.
  22. David E. Muller and Paul E. Schupp. Alternating automata on infinite objects, determinacy and Rabin’s theorem. In Maurice Nivat and Dominique Perrin, editors, Automata on Infinite Words - École de Printemps d'Informatique Théorique (EPIT'84), volume 192 of Lecture Notes in Computer Science, pages 99-107. Springer-Verlag, 1985. URL: https://doi.org/10.1007/3-540-15641-0_27.
  23. Michael O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society, 141:1-35, 1969. Google Scholar
  24. A. Prasad Sistla, Moshe Y. Vardi, and Pierre Wolper. The complementation problem for Büchi automata, with applications to temporal logic. In Wilfried Brauer, editor, Proceedings of the 12th International Colloquium on Automata, Languages and Programming (ICALP'85), volume 194 of Lecture Notes in Computer Science, pages 465-474. Springer-Verlag, 1985. Google Scholar
  25. Wolfgang Thomas. Languages, automata and logics. In Grzegorz Rozenberg and Arto Salomaa, editors, Handbook of Formal Languages, volume 3, pages 389-455. Springer-Verlag, 1997. Google Scholar
  26. Boris A. Trakhtenbrot. Finite automata and the logic of one-place predicates. Siberskii Matematicheskii Zhurnal, 3(1):103-131, 1962. Google Scholar
  27. Moshe Y. Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the 1st Annual Symposium on Logic in Computer Science (LICS'86), pages 332-344. IEEE Comp. Soc. Press, 1986. Google Scholar
  28. Moshe Y. Vardi and Pierre Wolper. Automata theoretic techniques for modal logics of programs. Journal of Computer and System Sciences, 32(2):183-221, 1986. URL: https://doi.org/10.1016/0022-0000(86)90026-7.
  29. Igor Walukiewicz. Monadic second order logic on tree-like structures. In Claude Puech and Rüdiger Reischuk, editors, Proceedings of the 13th Symposium on Theoretical Aspects of Computer Science (STACS'96), volume 1046 of Lecture Notes in Computer Science, pages 401-413. Springer-Verlag, 1996. URL: https://doi.org/10.1007/3-540-60922-9_33.
  30. Igor Walukiewicz. Monadic second order logic on tree-like structures. Theoretical Computer Science, 275(1-2):311-346, 2002. URL: https://doi.org/10.1016/S0304-3975(01)00185-2.
  31. Thomas Wilke. CTL^+ is exponentially more succinct than CTL. In C. Pandu Rangan, Venkatesh Raman, and R. Ramanujam, editors, Proceedings of the 19th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'99), volume 1738 of Lecture Notes in Computer Science, pages 110-121. Springer-Verlag, 1999. URL: https://doi.org/10.1007/3-540-46691-6_9.
  32. Thomas Wilke. Alternating tree automata, parity games, and modal μ-calculus. Bulletin of the Belgian Mathematical Society - Simon Stevin, 8(2):359-391, 2001. Google Scholar
  33. Fabio Zanasi. Expressiveness of monadic second-order logics on infinite trees of arbitrary branching degrees. Master’s thesis, Amsterdam University, the Netherlands, 2012. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact