Document Open Access Logo

Layered Automata: A Canonical Model for Automata over Infinite Words

Authors Antonio Casares , Christof Löding , Igor Walukiewicz

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.24.pdf
  • Filesize: 1.15 MB
  • 26 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Omega automata
  • history determinism
  • canonical automata

Metrics

Abstract

We introduce layered automata, a subclass of alternating parity automata that generalises deterministic automata. Assuming a consistency property, these automata are history deterministic and 0-1 probabilistic. We show that every omega-regular language is recognised by a unique minimal consistent layered automaton, and that this canonical form can be computed in polynomial time from every layered or deterministic automaton. We further establish that, for layered automata, both consistency checking and inclusion testing can be performed in polynomial time. Much like deterministic finite automata, minimal consistent layered automata admit a characterisation based on congruences.

Cite As Get BibTex

Antonio Casares, Christof Löding, and Igor Walukiewicz. Layered Automata: A Canonical Model for Automata over Infinite Words. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 24:1-24:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.24

Author Details

Antonio Casares
  • University of Kaiserslautern-Landau, Germany
Christof Löding
  • RWTH Aachen University, Germany
Igor Walukiewicz
  • CNRS, Bordeaux University, Talence, France

Funding

  • Casares, Antonio: Partially supported by Deutsche Forschungsgemeinschaft (grant number 522843867) and European Research Council (grant number 101089343). Part of this work was done while Casares was at the University of Warsaw, Poland, supported by the Polish National Science Centre (NCN) grant "Polynomial finite state computation" (2022/46/A/ST6/00072).
  • Löding, Christof: supported by DFG grant LO 1174/7-1.

Acknowledgements

We thank Thomas Colcombet, Keya Prakash and Pierre Ohlmann for interesting discussions on the subject.

References

  1. Bader Abu Radi and Rüdiger Ehlers. Characterizing the polynomial-time minimizable ω-automata. CoRR, abs/2504.20553, 2025. URL: https://doi.org/10.48550/arXiv.2504.20553.
  2. Bader Abu Radi and Orna Kupferman. Minimization and canonization of GFG transition-based automata. Logical Methods in Computer Science, Volume 18, Issue 3:7587, 2022. URL: https://doi.org/10.46298/lmcs-18(3:16)2022.
  3. Dana Angluin and Dana Fisman. Learning regular omega languages. Theor. Comput. Sci., 650:57-72, 2016. URL: https://doi.org/10.1016/J.TCS.2016.07.031.
  4. André Arnold. A syntactic congruence for rational omega-languages. Theor. Comput. Sci., 39:333-335, 1985. URL: https://doi.org/10.1016/0304-3975(85)90148-3.
  5. Guy Avni and Orna Kupferman. Stochastization of weighted automata. In Mathematical Foundations of Computer Science 2015 - 40th International Symposium, MFCS 2015, Milan, Italy, August 24-28, 2015, Proceedings, Part I, volume 9234 of Lecture Notes in Computer Science, pages 89-102. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-48057-1_7.
  6. Christel Baier, Marcus Grösser, and Nathalie Bertrand. Probabilistic ω-automata. J. ACM, 59(1), 2012. URL: https://doi.org/10.1145/2108242.2108243.
  7. León Bohn and Christof Löding. Constructing deterministic parity automata from positive and negative examples. TheoretiCS, 3, 2024. URL: https://doi.org/10.46298/THEORETICS.24.17.
  8. Udi Boker, Denis Kuperberg, Karoliina Lehtinen, and Michal Skrzypczak. On the succinctness of alternating parity good-for-games automata. In Nitin Saxena and Sunil Simon, editors, FSTTCS, volume 182 of LIPIcs, pages 41:1-41:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2020.41.
  9. Udi Boker and Karoliina Lehtinen. Good for games automata: From nondeterminism to alternation. In Wan J. Fokkink and Rob van Glabbeek, editors, CONCUR, volume 140 of LIPIcs, pages 19:1-19:16, 2019. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.19.
  10. J. Richard Büchi. On a decision method in restricted second order arithmetic. Proc. Internat. Congr. on Logic, Methodology and Philosophy of Science, pages 1-11, 1962. Google Scholar
  11. Antonio Casares. On the minimisation of transition-based Rabin automata and the chromatic memory requirements of Muller conditions. In CSL, volume 216, pages 12:1-12:17, 2022. URL: https://doi.org/10.4230/LIPIcs.CSL.2022.12.
  12. Antonio Casares, Thomas Colcombet, Nathanaël Fijalkow, and Karoliina Lehtinen. From Muller to parity and Rabin automata: Optimal transformations preserving (history) determinism. TheoretiCS, 3, 2024. URL: https://doi.org/10.46298/THEORETICS.24.12.
  13. Antonio Casares, Christof Löding, and Igor Walukiewicz. Layered automata: A canonical model for automata over infinite words, 2026. URL: https://doi.org/10.48550/arXiv.2601.15940.
  14. Antonio Casares and Pierre Ohlmann. Positional ω-regular languages. In LICS, pages 21:1-21:14. ACM, 2024. URL: https://doi.org/10.1145/3661814.3662087.
  15. Ashok K. Chandra, Dexter C. Kozen, and Larry J. Stockmeyer. Alternation. J. ACM, 28(1):114-133, January 1981. URL: https://doi.org/10.1145/322234.322243.
  16. E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244-263, 1986. URL: https://doi.org/10.1145/5397.5399.
  17. Thomas Colcombet. Fonctions régulières de coût. Habilitation (hdr), Université Paris Diderot – Paris 7, 2013. Google Scholar
  18. Thomas Colcombet and Christof Löding. The non-deterministic Mostowski hierarchy and distance-parity automata. In Automata, Languages and Programming, 35th International Colloquium, ICALP 2008, volume 5126 of Lecture Notes in Computer Science, pages 398-409. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-70583-3_33.
  19. Stefan Dziembowski, Marcin Jurdziński, and Igor Walukiewicz. How much memory is needed to win infinite games? In LICS, pages 99-110, 1997. URL: https://doi.org/10.1109/LICS.1997.614939.
  20. Rüdiger Ehlers. Rerailing automata. CoRR, abs/2503.08438, 2025. URL: https://doi.org/10.48550/arXiv.2503.08438.
  21. Rüdiger Ehlers and Ayrat Khalimov. Fully Generalized Reactivity(1) Synthesis. In Bernd Finkbeiner and Laura Kovács, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 14570, pages 83-102. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57246-3_6.
  22. Rüdiger Ehlers and Ayrat Khalimov. A Naturally-Colored Translation from LTL to Parity and COCOA, 2024. URL: https://doi.org/10.48550/arXiv.2410.01021.
  23. Rüdiger Ehlers and Sven Schewe. Natural Colors of Infinite Words. LIPIcs, Volume 250, FSTTCS 2022, 250:36:1-36:17, 2022. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2022.36.
  24. Nathanaël Fijalkow, C. Aiswarya, Guy Avni, Nathalie Bertrand, Patricia Bouyer, Romain Brenguier, Arnaud Carayol, Antonio Casares, John Fearnley, Paul Gastin, Hugo Gimbert, Thomas A. Henzinger, Florian Horn, Rasmus Ibsen-Jensen, Nicolas Markey, Benjamin Monmege, Petr Novotný, Pierre Ohlmann, Mickael Randour, Ocan Sankur, Sylvain Schmitz, Olivier Serre, Mateusz Skomra, Nathalie Sznajder, and Pierre Vandenhove. Games on graphs: From logic and automata to algorithms, 2025. To appear in Cambridge University Press. URL: https://arxiv.org/abs/2305.10546.
  25. Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtczak. Good-for-mdps automata for probabilistic analysis and reinforcement learning. In Armin Biere and David Parker, editors, TACAS, volume 12078 of Lecture Notes in Computer Science, pages 306-323, 2020. URL: https://doi.org/10.1007/978-3-030-45190-5_17.
  26. Thomas A. Henzinger and Nir Piterman. Solving games without determinization. In Computer Science Logic, pages 395-410, 2006. URL: https://doi.org/10.1007/11874683_26.
  27. Thomas A. Henzinger, Keya Prakash, and K. S. Thejaswini. Resolving nondeterminism with randomness. In Pawel Gawrychowski, Filip Mazowiecki, and Michal Skrzypczak, editors, MFCS, volume 345 of LIPIcs, pages 57:1-57:18, 2025. URL: https://doi.org/10.4230/LIPIcs.MFCS.2025.57.
  28. Markus Holzer and Barbara König. On deterministic finite automata and syntactic monoid size. In Developments in Language Theory, DLT 2002, volume 2450 of Lecture Notes in Computer Science, pages 258-269. Springer, 2002. URL: https://doi.org/10.1007/3-540-45005-X_22.
  29. Olivier Idir and Karoliina Lehtinen. Using games and universal trees to characterise the nondeterministic index of tree languages. In 52nd International Colloquium on Automata, Languages, and Programming, ICALP 2025, volume 334 of LIPIcs, pages 160:1-160:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.ICALP.2025.160.
  30. Nils Klarlund. A homomorphism concepts for omega-regularity. In Computer Science Logic, 8th International Workshop, CSL '94, Kazimierz, Poland, September 25-30, 1994, Selected Papers, volume 933 of Lecture Notes in Computer Science, pages 471-485. Springer, 1994. URL: https://doi.org/10.1007/BFb0022276.
  31. Nils Klarlund, Anders Møller, and Michael I. Schwartzbach. MONA implementation secrets. Int. J. Found. Comput. Sci., 13(4):571-586, 2002. URL: https://doi.org/10.1142/S012905410200128X.
  32. Denis Kuperberg and Michał Skrzypczak. On determinisation of good-for-games automata. In ICALP, pages 299-310, 2015. URL: https://doi.org/10.1007/978-3-662-47666-6_24.
  33. Orna Kupferman. Automata theory and model checking. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 107-151. Springer International Publishing, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_4.
  34. Orna Kupferman, Shmuel Safra, and Moshe Y. Vardi. Relating word and tree automata. In LICS, pages 322-332, 1996. URL: https://doi.org/10.1109/LICS.1996.561360.
  35. Christof Löding and Igor Walukiewicz. Minimal history-deterministic co-Büchi automata: Congruences and passive learning. In LICS, pages 431-443. IEEE, 2025. URL: https://doi.org/10.1109/LICS65433.2025.00039.
  36. Oded Maler and Ludwig Staiger. On syntactic congruences for ω-languages. Theoretical Computer Science, 183(1):93-112, 1997. Formal Language Theory. URL: https://doi.org/10.1016/S0304-3975(96)00312-X.
  37. Zohar Manna and Amir Pnueli. A hierarchy of temporal properties. In Cynthia Dwork, editor, PODC, pages 377-410. ACM, 1990. URL: https://doi.org/10.1145/93385.93442.
  38. Donald A. Martin. Borel determinacy. Annals of Mathematics, 102(2):363-371, 1975. Google Scholar
  39. Soumyajit Paul, David Purser, Sven Schewe, Qiyi Tang, Patrick Totzke, and Di-De Yen. Resolving nondeterminism by chance. In Patricia Bouyer and Jaco van de Pol, editors, CONCUR, volume 348 of LIPIcs, pages 32:1-32:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2025.32.
  40. Dominique Perrin and Jean-Éric Pin. Semigroups and automata on infinite words. In Semigroups, formal languages and groups (York, 1993), volume 933, pages 49-72. Kluwer Acad. Publ., 1995. Google Scholar
  41. Amir Pnueli and Roni Rosner. On the synthesis of a reactive module. In POPL, pages 179-190, 1989. URL: https://doi.org/10.1145/75277.75293.
  42. Sven Schewe. Beyond hyper-minimisation - minimising DBAs and DPAs is NP-complete. In FSTTCS, volume 8, pages 400-411, 2010. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2010.400.
  43. Thomas Wilke. An Eilenberg theorem for infinity-languages. In ICALP, volume 510, pages 588-599, 1991. URL: https://doi.org/10.1007/3-540-54233-7_166.
  44. Wiesław Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science, 200(1-2):135-183, 1998. URL: https://doi.org/10.1016/S0304-3975(98)00009-7.
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