Document Open Access Logo

On the Size of Good-For-Games Rabin Automata and Its Link with the Memory in Muller Games

Authors Antonio Casares , Thomas Colcombet , Karoliina Lehtinen

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2022.117.pdf
  • Filesize: 0.94 MB
  • 20 pages

Document Identifiers

Author Details

Antonio Casares
  • LaBRI, Université de Bordeaux, France
Thomas Colcombet
  • CNRS, IRIF, Université Paris Cité, France
Karoliina Lehtinen
  • CNRS, Aix-Marseille Université, Université de Toulon, LIS, France

Funding

  • Colcombet, Thomas: ANR Delta and Duall

Acknowledgements

We would like to thank Marthe Bonamy and Pierre Charbit for their help with graph theory.

Cite AsGet BibTex

Antonio Casares, Thomas Colcombet, and Karoliina Lehtinen. On the Size of Good-For-Games Rabin Automata and Its Link with the Memory in Muller Games. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 117:1-117:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ICALP.2022.117

Abstract

In this paper, we look at good-for-games Rabin automata that recognise a Muller language (a language that is entirely characterised by the set of letters that appear infinitely often in each word). We establish that minimal such automata are exactly of the same size as the minimal memory required for winning Muller games that have this language as their winning condition. We show how to effectively construct such minimal automata. Finally, we establish that these automata can be exponentially more succinct than equivalent deterministic ones, thus proving as a consequence that chromatic memory for winning a Muller game can be exponentially larger than unconstrained memory.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
Keywords
  • Infinite duration games
  • Muller games
  • Rabin conditions
  • omega-regular languages
  • memory in games
  • good-for-games automata

Metrics

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

Related Versions

References

  1. Bader Abu Radi and Orna Kupferman. Minimizing GFG transition-based automata. In ICALP, volume 132, pages 100:1-100:16, 2019. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.100.
  2. Tomáš Babiak, František Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Křetínský, David Müller, David Parker, and Jan Strejček. The Hanoi omega-automata format. In CAV, pages 479-486, 2015. Google Scholar
  3. Marc Bagnol and Denis Kuperberg. Büchi good-for-games automata are efficiently recognizable. In FSTTCS, page 16, 2018. Google Scholar
  4. Udi Boker, Denis Kuperberg, Karoliina Lehtinen, and Michal Skrzypczak. On succinctness and recognisability of alternating good-for-games automata. CoRR, abs/2002.07278, 2020. URL: http://arxiv.org/abs/2002.07278.
  5. Udi Boker and Karoliina Lehtinen. History determinism vs. good for gameness in quantitative automata, 2021. URL: http://arxiv.org/abs/2110.14238.
  6. Udi Boker and Karoliina Lehtinen. Token games and history-deterministic quantitative-automata, 2022. To appear in proceedings of FoSSaCS'22. URL: http://arxiv.org/abs/2110.14308.
  7. Patricia Bouyer, Mickael Randour, and Pierre Vandenhove. Characterizing omega-regularity through finite-memory determinacy of games on infinite graphs. CoRR, abs/2110.01276, 2021. URL: http://arxiv.org/abs/2110.01276.
  8. Patricia Bouyer, Stéphane Le Roux, Youssouf Oualhadj, Mickael Randour, and Pierre Vandenhove. Games where you can play optimally with arena-independent finite memory. In CONCUR, volume 171, pages 24:1-24:22, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.24.
  9. J. Richard Büchi. Using determinancy of games to eliminate quantifiers. In FCT, volume 56 of Lecture Notes in Computer Science, pages 367-378. Springer, 1977. URL: https://doi.org/10.1007/3-540-08442-8_104.
  10. 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.
  11. Antonio Casares, Thomas Colcombet, and Nathanaël Fijalkow. Optimal transformations of games and automata using Muller conditions. In ICALP, volume 198, pages 123:1-123:14, 2021. URL: https://doi.org/10.4230/LIPIcs.ICALP.2021.123.
  12. Thomas Colcombet. The theory of stabilisation monoids and regular cost functions. In ICALP, pages 139-150, 2009. URL: https://doi.org/10.1007/978-3-642-02930-1_12.
  13. Thomas Colcombet and Damian Niwiński. On the positional determinacy of edge-labeled games. Theoretical Computer Science, 352(1):190-196, 2006. URL: https://doi.org/10.1016/j.tcs.2005.10.046.
  14. Thomas Colcombet and Konrad Zdanowski. A tight lower bound for determinization of transition labeled Büchi automata. In ICALP, pages 151-162, 2009. URL: https://doi.org/10.1007/978-3-642-02930-1_13.
  15. 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.
  16. E. Allen Emerson and Charanjit S. Jutla. Tree automata, mu-calculus and determinacy (extended abstract). In FOCS, pages 368-377, 1991. URL: https://doi.org/10.1109/SFCS.1991.185392.
  17. Hugo Gimbert and Wieslaw Zielonka. Games where you can play optimally without any memory. In CONCUR, volume 3653, pages 428-442, 2005. URL: https://doi.org/10.1007/11539452_33.
  18. Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann. A Bit of Nondeterminism Makes Pushdown Automata Expressive and Succinct. In MFCS, volume 202, pages 53:1-53:20, 2021. URL: https://doi.org/10.4230/LIPIcs.MFCS.2021.53.
  19. Yuri Gurevich and Leo Harrington. Trees, automata, and games. In STOC, pages 60-65, 1982. URL: https://doi.org/10.1145/800070.802177.
  20. Thomas A. Henzinger and Nir Piterman. Solving games without determinization. In Computer Science Logic, pages 395-410, 2006. Google Scholar
  21. Florian Horn. Random fruits on the zielonka tree. In STACS, volume 3, pages 541-552, 2009. URL: https://doi.org/10.4230/LIPIcs.STACS.2009.1848.
  22. Nils Klarlund. Progress measures, immediate determinacy, and a subset construction for tree automata. Annals of Pure and Applied Logic, 69(2):243-268, 1994. URL: https://doi.org/10.1016/0168-0072(94)90086-8.
  23. Eryk Kopczyński. Half-positional determinacy of infinite games. In ICALP, pages 336-347, 2006. URL: https://doi.org/10.1007/11787006_29.
  24. Eryk Kopczyński. Half-positional Determinacy of Infite Games. Phd thesis, University of Warsaw, 2008. Google Scholar
  25. Alexander Kozachinskiy. State complexity of chromatic memory in infinite-duration games. CoRR, abs/2201.09297, 2022. URL: http://arxiv.org/abs/2201.09297.
  26. Jan Křetínský, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger. Index appearance record for transforming Rabin automata into parity automata. In TACAS, pages 443-460, 2017. URL: https://doi.org/10.1007/978-3-662-54577-5_26.
  27. 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.
  28. Karoliina Lehtinen and Martin Zimmermann. Good-for-games ω-pushdown automata. In LICS, pages 689-702, 2020. URL: https://doi.org/10.1145/3373718.3394737.
  29. Christof Löding and Anton Pirogov. Determinization of Büchi automata: Unifying the approaches of Safra and Muller-Schupp. In ICALP, pages 120:1-120:13, 2019. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.120.
  30. Michael Luttenberger, Philipp J. Meyer, and Salomon Sickert. Practical synthesis of reactive systems from LTL specifications via parity games. Acta Informatica, pages 3-36, 2020. URL: https://doi.org/10.1007/s00236-019-00349-3.
  31. Christof Löding. Optimal bounds for transformations of ω-automata. In FSTTCS, pages 97-109, 1999. URL: https://doi.org/10.1007/3-540-46691-6_8.
  32. Robert McNaughton. Testing and generating infinite sequences by a finite automaton. Information and control, 9:521-530, 1966. Google Scholar
  33. Philipp Meyer and Salomon Sickert. On the optimal and practical conversion of Emerson-Lei automata into parity automata. Personal Communication, 2021. Google Scholar
  34. Max Michel. Complementation is more difficult with automata on infinite words. CNET, Paris, 15, 1988. Google Scholar
  35. Dhruv Mubayi and Vojtech Rödl. Specified intersections. Transactions of the American Mathematical Society, 366(1):491-504, 2014. URL: http://www.jstor.org/stable/23813142.
  36. David E. Muller and Paul E. Schupp. Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra. Theor. Comput. Sci., 141(1–2):69-107, 1995. URL: https://doi.org/10.1016/0304-3975(94)00214-4.
  37. Nir Piterman. From nondeterministic Büchi and Streett automata to deterministic parity automata. In LICS, pages 255-264, 2006. URL: https://doi.org/10.1109/LICS.2006.28.
  38. 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.
  39. Schmuel Safra. On the complexity of ω-automata. In FOCS, pages 319-327, 1988. URL: https://doi.org/10.1109/SFCS.1988.21948.
  40. Sven Schewe. Tighter bounds for the determinisation of Büchi automata. In FoSSaCS, pages 167-181, 2009. URL: https://doi.org/10.1007/978-3-642-00596-1_13.
  41. 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.
  42. Sven Schewe. Minimising Good-For-Games automata is NP-complete. In FSTTCS, volume 182, pages 56:1-56:13, 2020. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2020.56.
  43. 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.
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