Büchi Good-for-Games Automata Are Efficiently Recognizable

Authors Marc Bagnol, Denis Kuperberg

Thumbnail PDF


  • Filesize: 0.5 MB
  • 14 pages

Document Identifiers

Author Details

Marc Bagnol
  • LIP, École Normale Supérieure, Lyon, France
Denis Kuperberg
  • CNRS, LIP, École Normale Supérieure, Lyon, France

Cite AsGet BibTex

Marc Bagnol and Denis Kuperberg. Büchi Good-for-Games Automata Are Efficiently Recognizable. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 16:1-16:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Good-for-Games (GFG) automata offer a compromise between deterministic and nondeterministic automata. They can resolve nondeterministic choices in a step-by-step fashion, without needing any information about the remaining suffix of the word. These automata can be used to solve games with omega-regular conditions, and in particular were introduced as a tool to solve Church's synthesis problem. We focus here on the problem of recognizing Büchi GFG automata, that we call Büchi GFGness problem: given a nondeterministic Büchi automaton, is it GFG? We show that this problem can be decided in P, and more precisely in O(n^4m^2|Sigma|^2), where n is the number of states, m the number of transitions and |Sigma| is the size of the alphabet. We conjecture that a very similar algorithm solves the problem in polynomial time for any fixed parity acceptance condition.

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
  • Theory of computation → Formal languages and automata theory
  • Büchi
  • automata
  • games
  • polynomial time
  • nondeterminism


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


  1. Udi Boker, Denis Kuperberg, Orna Kupferman, and Michał Skrzypczak. Nondeterminism in the Presence of a Diverse or Unknown Future. In Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II, pages 89-100, 2013. Google Scholar
  2. Udi Boker, Orna Kupferman, and Michał Skrzypczak. How Deterministic are Good-For-Games Automata? In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2017, December 11-15, 2017, Kanpur, India, pages 18:1-18:14, 2017. Google Scholar
  3. J. Richard Buchi and Lawrence H. Landweber. Solving Sequential Conditions by Finite-State Strategies. Transactions of the American Mathematical Society, 138:295-311, 1969. Google Scholar
  4. Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasipolynomial time. In Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2017, Montreal, QC, Canada, June 19-23, 2017, pages 252-263, 2017. Google Scholar
  5. Alonzo Church. Application of Recursive Arithmetic to the Problem of Circuit Synthesis. Journal of Symbolic Logic, 28(4):289-290, 1963. Google Scholar
  6. Thomas Colcombet. The theory of stabilisation monoids and regular cost functions. In Automata, languages and programming. Part II, volume 5556 of Lecture Notes in Comput. Sci., pages 139-150, Berlin, 2009. Springer. Google Scholar
  7. Thomas Colcombet. Forms of Determinism for Automata (Invited Talk). In 29th International Symposium on Theoretical Aspects of Computer Science, STACS 2012, February 29th - March 3rd, 2012, Paris, France, pages 1-23, 2012. Google Scholar
  8. E. Allen Emerson and Charanjit S. Jutla. Tree Automata, Mu-Calculus and Determinacy (Extended Abstract). In 32nd Annual Symposium on Foundations of Computer Science, San Juan, Puerto Rico, 1-4 October 1991, pages 368-377, 1991. Google Scholar
  9. Kousha Etessami. A Hierarchy of Polynomial-Time Computable Simulations for Automata. In CONCUR 2002 - Concurrency Theory, 13th International Conference, Brno, Czech Republic, August 20-23, 2002, Proceedings, pages 131-144, 2002. Google Scholar
  10. Thomas A. Henzinger and Nir Piterman. Solving Games Without Determinization. In Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings, pages 395-410, 2006. Google Scholar
  11. Marcin Jurdziński. Small Progress Measures for Solving Parity Games. In Horst Reichel and Sophie Tison, editors, STACS 2000, pages 290-301, Berlin, Heidelberg, 2000. Springer Berlin Heidelberg. Google Scholar
  12. Nils Klarlund. Progress Measures, Immediate Determinacy, and a Subset Construction for Tree Automata. Ann. Pure Appl. Logic, 69(2-3):243-268, 1994. Google Scholar
  13. Joachim Klein, David Müller, Christel Baier, and Sascha Klüppelholz. Are Good-for-Games Automata Good for Probabilistic Model Checking? In Language and Automata Theory and Applications - 8th International Conference, LATA 2014, Madrid, Spain, March 10-14, 2014. Proceedings, pages 453-465, 2014. Google Scholar
  14. Denis Kuperberg and Anirban Majumdar. Width of Non-deterministic Automata. In 35th Symposium on Theoretical Aspects of Computer Science, STACS 2018, February 28 to March 3, 2018, Caen, France, pages 47:1-47:14, 2018. Google Scholar
  15. Denis Kuperberg and Michał Skrzypczak. On Determinisation of Good-for-Games Automata. In Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, pages 299-310, 2015. Google Scholar
  16. Robert McNaughton. Infinite games played on finite graphs. Annals of Pure and Applied Logic, 65(2):149-184, 1993. Google Scholar
  17. Sven Schewe. Solving parity games in big steps. Journal of Computer and System Sciences, 84:243-262, 2017. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail