On the Minimisation of Transition-Based Rabin Automata and the Chromatic Memory Requirements of Muller Conditions

Author Antonio Casares

Thumbnail PDF


  • Filesize: 0.84 MB
  • 17 pages

Document Identifiers

Author Details

Antonio Casares
  • LaBRI, Université de Bordeaux, France


I would like to thank Alexandre Blanché for pointing me to the chromatic number problem. I also want to thank Bader Abu Radi, Thomas Colcombet, Nathanaël Fijalkow, Orna Kupferman, Karoliina Lehtinen and Nir Piterman for interesting discussions on the minimisation of transition-based automata, a problem introduced to us by Orna Kupferman. Finally, I warmly thank Thomas Colcombet, Nathanaël Fijalkow and Igor Walukiewicz for their help in the preparation of this paper. This work was done while the author was participating in the program Theoretical Foundations of Computer Systems at the Simons Institute for the Theory of Computing.

Cite AsGet BibTex

Antonio Casares. On the Minimisation of Transition-Based Rabin Automata and the Chromatic Memory Requirements of Muller Conditions. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


In this paper, we relate the problem of determining the chromatic memory requirements of Muller conditions with the minimisation of transition-based Rabin automata. Our first contribution is a proof of the NP-completeness of the minimisation of transition-based Rabin automata. Our second contribution concerns the memory requirements of games over graphs using Muller conditions. A memory structure is a finite state machine that implements a strategy and is updated after reading the edges of the game; the special case of chromatic memories being those structures whose update function only consider the colours of the edges. We prove that the minimal amount of chromatic memory required in games using a given Muller condition is exactly the size of a minimal Rabin automaton recognising this condition. Combining these two results, we deduce that finding the chromatic memory requirements of a Muller condition is NP-complete. This characterisation also allows us to prove that chromatic memories cannot be optimal in general, disproving a conjecture by Kopczyński.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
  • Automata on Infinite Words
  • Games on Graphs
  • Arena-Independent Memory
  • Complexity


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


  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. Bader Abu Radi and Orna Kupferman. Canonicity in GFG and transition-based automata. In GandALF, volume 326, pages 199-215, 2020. URL: https://doi.org/10.4204/EPTCS.326.13.
  3. 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 of LIPIcs, pages 24:1-24:22, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.24.
  4. Olivier Carton and Ramón Maceiras. Computing the Rabin index of a parity automaton. RAIRO, pages 495-506, 1999. URL: https://doi.org/10.1051/ita:1999129.
  5. Antonio Casares. On the minimisation of transition-based Rabin automata and the chromatic memory requirements of Muller conditions. CoRR, abs/2105.12009, 2021. URL: http://arxiv.org/abs/2105.12009.
  6. 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.
  7. Edmund M. Clarke, I. A. Draghicescu, and Robert P. Kurshan. A unified approch for showing language inclusion and equivalence between various types of omega-automata. Inf. Process. Lett., 46(6):301-308, 1993. URL: https://doi.org/10.1016/0020-0190(93)90069-L.
  8. 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.
  9. Thomas Colcombet, Nathanaël Fijalkow, and Florian Horn. Playing safe. In FSTTCS, volume 29, pages 379-390, 2014. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2014.379.
  10. 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.
  11. 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.
  12. 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.
  13. Dimitra Giannakopoulou and Flavio Lerda. From states to transitions: Improving translation of ltl formulae to Büchi automata. In FORTE, pages 308-326, 2002. Google Scholar
  14. Hugo Gimbert and Wieslaw Zielonka. Games where you can play optimally without any memory. In CONCUR, volume 3653 of Lecture Notes in Computer Science, pages 428-442, 2005. URL: https://doi.org/10.1007/11539452_33.
  15. John E. Hopcroft. An n log n algorithm for minimizing states in a finite automaton. Technical report, Stanford University, 1971. URL: https://doi.org/10.5555/891883.
  16. Richard M. Karp. Reducibility among Combinatorial Problems, pages 85-103. The IBM Research Symposia Series. Springer US, 1972. URL: https://doi.org/10.1007/978-1-4684-2001-2_9.
  17. 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.
  18. Eryk Kopczyński. Half-positional determinacy of infinite games. In ICALP, pages 336-347, 2006. URL: https://doi.org/10.1007/11787006_29.
  19. Eryk Kopczyński. Half-positional determinacy of infite games. PhD Thesis. University of Warsaw, 2008. Google Scholar
  20. Christof Löding. Efficient minimization of deterministic weak omega-automata. Inf. Process. Lett., 79(3):105-109, 2001. URL: https://doi.org/10.1016/S0020-0190(00)00183-6.
  21. Philipp Meyer and Salomon Sickert. On the optimal and practical conversion of Emerson-Lei automata into parity automata. Personal Communication, 2021. Google Scholar
  22. 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.
  23. 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.
  24. Schmuel Safra. On the complexity of ω-automata. In FOCS, pages 319-327, 1988. URL: https://doi.org/10.1109/SFCS.1988.21948.
  25. 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.
  26. Sven Schewe. Beyond hyper-minimisation - minimising DBAs and DPAs is NP-complete. In FSTTCS, volume 8 of LIPIcs, pages 400-411, 2010. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2010.400.
  27. 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.
  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. 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.