Document Open Access Logo

Optimal Transformations of Games and Automata Using Muller Conditions

Authors Antonio Casares , Thomas Colcombet , Nathanaël Fijalkow

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2021.123.pdf
  • Filesize: 0.77 MB
  • 14 pages

Document Identifiers

Author Details

Antonio Casares
  • LaBRI, Université de Bordeaux, France
Thomas Colcombet
  • CNRS, IRIF, Université de Paris, France
Nathanaël Fijalkow
  • CNRS, LaBRI, Université de Bordeaux, France
  • The Alan Turing Institute of Data Science, London, UK

Funding

  • Colcombet, Thomas: Supported by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No.670624) and the DeLTA ANR project (ANR-16-CE40-0007).

Acknowledgements

We want to thank Philipp Meyer and Salomon Sickert for their comments and for spotting a mistake on a previous version of this paper.

Cite As Get BibTex

Antonio Casares, Thomas Colcombet, and Nathanaël Fijalkow. Optimal Transformations of Games and Automata Using Muller Conditions. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 123:1-123:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ICALP.2021.123

Abstract

We consider the following question: given an automaton or a game with a Muller condition, how can we efficiently construct an equivalent one with a parity condition? There are several examples of such transformations in the literature, including in the determinisation of Büchi automata.
We define a new transformation called the alternating cycle decomposition, inspired and extending Zielonka’s construction. Our transformation operates on transition systems, encompassing both automata and games, and preserves semantic properties through the existence of a locally bijective morphism. We show a strong optimality result: the obtained parity transition system is minimal both in number of states and number of priorities with respect to locally bijective morphisms.
We give two applications: the first is related to the determinisation of Büchi automata, and the second is to give crisp characterisations on the possibility of relabelling automata with different acceptance conditions.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
Keywords
  • Automata over infinite words
  • Omega regular languages
  • Determinisation of automata

Metrics

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

Related Versions

References

  1. Udi Boker, Orna Kupferman, and Avital Steinitz. Parityizing Rabin and Streett. In FSTTCS, pages 412-423, 2010. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2010.412.
  2. Olivier Carton and Ramón Maceiras. Computing the Rabin index of a parity automaton. RAIRO: Theoretical Informatics and Applications, pages 495-506, 1999. URL: https://doi.org/10.1051/ita:1999129.
  3. Olivier Carton and Max Michel. Unambiguous Büchi automata. Theoretical Computer Science, 297(1):37-81, 2003. URL: https://doi.org/10.1016/S0304-3975(02)00618-7.
  4. Antonio Casares, Thomas Colcombet, and Nathanaël Fijalkow. Optimal transformations of Muller conditions. CoRR, abs/2011.13041, 2020. URL: http://arxiv.org/abs/2011.13041.
  5. Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors. Handbook of Model Checking. Springer, Cham, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_2.
  6. 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.
  7. 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.
  8. Javier Esparza, Jan Křetínský, Jean-François Raskin, and Salomon Sickert. From LTL and limit-deterministic Büchi automata to deterministic parity automata. In TACAS, pages 426-442, 2017. URL: https://doi.org/10.1007/978-3-662-54577-5_25.
  9. Yuri Gurevich and Leo Harrington. Trees, automata, and games. In STOC, pages 60-65, 1982. URL: https://doi.org/10.1145/800070.802177.
  10. Thomas Henzinger and Nir Piterman. Solving games without determinization. In CSL, pages 395-410, 2006. URL: https://doi.org/10.1007/11874683_26.
  11. Florian Horn. Explicit Muller games are PTIME. In FSTTCS, pages 235-243, 2008. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2008.1756.
  12. Paul Hunter and Anuj Dawar. Complexity bounds for regular games. In MFCS, pages 495-506, 2005. URL: https://doi.org/10.1007/11549345_43.
  13. 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.
  14. Sriram C. Krishnan, Anuj Puri, and Robert K. Brayton. Structural complexity of omega-automata. In STACS, pages 143-156, 1995. URL: https://doi.org/10.1007/3-540-59042-0_69.
  15. 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.
  16. 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.
  17. Christof Löding. Optimal bounds for transformations of ω-automata. In FSTTCS, page 97–109, 1999. URL: https://doi.org/10.1007/3-540-46691-6_8.
  18. Robert McNaughton. Testing and generating infinite sequences by a finite automaton. Information and control, 9:521-530, 1966. Google Scholar
  19. Philipp Meyer and Salomon Sickert. On the optimal and practical conversion of Emerson-Lei automata into parity automata. Personal Communication, 2021. Google Scholar
  20. Thibaud Michaud and Maximilien Colange. Reactive synthesis from LTL specification with Spot. In SYNT@CAV, 2018. Google Scholar
  21. David Müller and Salomon Sickert. LTL to deterministic Emerson-Lei automata. In GandALF, pages 180-194, 2017. URL: https://doi.org/10.4204/EPTCS.256.13.
  22. Damian Niwiński and Igor Walukiewicz. Relating hierarchies of word and tree automata. In STACS, pages 320-331, 1998. URL: https://doi.org/10.1007/BFb0028571.
  23. 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.
  24. Amir Pnueli and Roni Rosner. On the synthesis of a reactive module. In POPL, page 179–190, 1989. URL: https://doi.org/10.1145/75277.75293.
  25. Schmuel Safra. On the complexity of ω-automata. In FOCS, page 319–327, 1988. URL: https://doi.org/10.1109/SFCS.1988.21948.
  26. 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.
  27. Sven Schewe and Thomas Varghese. Determinising parity automata. In MFCS, pages 486-498, 2014. URL: https://doi.org/10.1007/978-3-662-44522-8_41.
  28. Klaus Wagner. On ω-regular sets. Information and Control, 43(2):123-177, 1979. URL: https://doi.org/10.1016/S0019-9958(79)90653-3.
  29. Thomas Wilke and Haiseung Yoo. Computing the Rabin index of a regular language of infinite words. Information and Computation, pages 61-70, 1996. URL: https://doi.org/10.1006/inco.1996.0082.
  30. 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 About DROPS Imprint Privacy Contact