How Deterministic are Good-For-Games Automata?

Authors Udi Boker, Orna Kupferman, Michal Skrzypczak

Thumbnail PDF


  • Filesize: 0.51 MB
  • 14 pages

Document Identifiers

Author Details

Udi Boker
Orna Kupferman
Michal Skrzypczak

Cite AsGet BibTex

Udi Boker, Orna Kupferman, and Michal Skrzypczak. How Deterministic are Good-For-Games Automata?. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 18:1-18:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


In good for games (GFG) automata, it is possible to resolve nondeterminism in a way that only depends on the past and still accepts all the words in the language. The motivation for GFG automata comes from their adequacy for games and synthesis, wherein general nondeterminism is inappropriate. We continue the ongoing effort of studying the power of nondeterminism in GFG automata. Initial indications have hinted that every GFG automaton embodies a deterministic one. Today we know that this is not the case, and in fact GFG automata may be exponentially more succinct than deterministic ones. We focus on the typeness question, namely the question of whether a GFG automaton with a certain acceptance condition has an equivalent GFG automaton with a weaker acceptance condition on the same structure. Beyond the theoretical interest in studying typeness, its existence implies efficient translations among different acceptance conditions. This practical issue is of special interest in the context of games, where the Büchi and co-Büchi conditions admit memoryless strategies for both players. Typeness is known to hold for deterministic automata and not to hold for general nondeterministic automata. We show that GFG automata enjoy the benefits of typeness, similarly to the case of deterministic automata. In particular, when Rabin or Streett GFG automata have equivalent Büchi or co-Büchi GFG automata, respectively, then such equivalent automata can be defined on a substructure of the original automata. Using our typeness results, we further study the place of GFG automata in between deterministic and nondeterministic ones. Specifically, considering automata complementation, we show that GFG automata lean toward nondeterministic ones, admitting an exponential state blow-up in the complementation of a Streett automaton into a Rabin automaton, as opposed to the constant blow-up in the deterministic case.
  • finite automata on infinite words
  • determinism
  • good-for-games


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


  1. U. Boker. Rabin vs. Streett automata. In Proc. 37th Conf. on Foundations of Software Technology and Theoretical Computer Science, pages 17:1-17:15, 2017. Google Scholar
  2. U. Boker, D. Kuperberg, O. Kupferman, and M. Skrzypczak. Nondeterminism in the presence of a diverse or unknown future. In Proc. 40th Int. Colloq. on Automata, Languages, and Programming, volume 7966 of Lecture Notes in Computer Science, pages 89-100, 2013. Google Scholar
  3. T. Colcombet and C. Löding. Regular cost functions over finite trees. In Proc. 25th IEEE Symp. on Logic in Computer Science, pages 70-79, 2010. Google Scholar
  4. T.A. Henzinger and N. Piterman. Solving games without determinization. In Proc. 15th Annual Conf. of the European Association for Computer Science Logic, volume 4207 of Lecture Notes in Computer Science, pages 394-410. Springer, 2006. Google Scholar
  5. S.C. Krishnan, A. Puri, and R.K. Brayton. Deterministic ω-automata vis-a-vis deterministic Büchi automata. In Algorithms and Computations, volume 834 of Lecture Notes in Computer Science, pages 378-386. Springer, 1994. Google Scholar
  6. D. Kuperberg and M. Skrzypczak. On determinisation of Good-For-Games automata. In Proc. 42nd Int. Colloq. on Automata, Languages, and Programming, pages 299-310, 2015. Google Scholar
  7. O. Kupferman, G. Morgenstern, and A. Murano. Typeness for ω-regular automata. International Journal on the Foundations of Computer Science, 17(4):869-884, 2006. Google Scholar
  8. O. Kupferman, S. Safra, and M.Y. Vardi. Relating word and tree automata. Ann. Pure Appl. Logic, 138(1-3):126-146, 2006. Google Scholar
  9. O. Kupferman and M.Y. Vardi. From linear time to branching time. ACM Transactions on Computational Logic, 6(2):273-294, 2005. Google Scholar
  10. O. Kupferman and M.Y. Vardi. Safraless decision procedures. In Proc. 46th IEEE Symp. on Foundations of Computer Science, pages 531-540, 2005. Google Scholar
  11. L.H. Landweber. Decision problems for ω-automata. Mathematical Systems Theory, 3:376-384, 1969. Google Scholar
  12. G. Morgenstern. Expressiveness results at the bottom of the ω-regular hierarchy. M.Sc. Thesis, The Hebrew University, 2003. Google Scholar
  13. D.E. Muller, A. Saoudi, and P.E. Schupp. Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In Proc. 3rd IEEE Symp. on Logic in Computer Science, pages 422-427, 1988. Google Scholar
  14. D. Niwiński and I. Walukiewicz. Relating hierarchies of word and tree automata. In Proc. 15th Symp. on Theoretical Aspects of Computer Science, volume 1373 of Lecture Notes in Computer Science. Springer, 1998. Google Scholar
  15. M.O. Rabin and D. Scott. Finite automata and their decision problems. IBM Journal of Research and Development, 3:115-125, 1959. Google Scholar
  16. S. Safra. On the complexity of ω-automata. In Proc. 29th IEEE Symp. on Foundations of Computer Science, pages 319-327, 1988. Google Scholar
  17. H. Seidl and D. Niwiński. On distributive fixed-point expressions. Theoretical Informatics and Applications, 33(4-5):427-446, 1999. Google Scholar
  18. W. Thomas. On the synthesis of strategies in infinite games. In E.W. Mayr and C. Puech, editors, Proc. 12th Symp. on Theoretical Aspects of Computer Science, volume 900 of Lecture Notes in Computer Science, pages 1-13. Springer, 1995. Google Scholar
  19. M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1-37, 1994. Google Scholar