Good games for good-for-games automata
Given an automaton , consider the following two games: Game I. At each turn : Adam plays a letter Eve plays a transition over A play is the infinite word and the sequence of transitions Eve wins if either is not in or is an accepting run over in . Game II. At each turn turn : Adam plays a letter Eve plays a transition over Adam plays a pair of transitions and A play is the triple of sequences of runs and Eve wins if either is an accepting run of or both and are not accepting runs of . The problem We know that these two games have the same winner when is a nondeterministic Buchi [1] or coBuchi [2] automaton. Conjecture [1]: These two games are equivalent on nondeterministic parity automata. Does this conjecture hold? Can we find any examples of automata on which these games do not have the same winner, for example using any acceptance condition or extra features like stacks or clocks? Why is it interesting? A positive answer would mean good-for-gameness (which Game I characterises) can be decided in polynomial time for automata with a fixed number of priorities, by solving Game II. It is also a rare example of a problem that we know how to solve for both Buchi and co-Buchi automata, but not for parity automata. [1] Bagnol, Marc, and Denis Kuperberg. "Büchi Good-for-Games Automata Are Efficiently Recognizable." 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. 2018. [2] Boker, U., Kuperberg, D., Lehtinen, K., & Skrzypczak, M. (2020). On Succinctness and Recognisability of Alternating Good-for-Games Automata. arXiv preprint arXiv:2002.07278.
