← All problems
Unverified

Good games for good-for-games automata

Given an automaton AA, consider the following two games: Game I. At each turn ii: Adam plays a letter aia_i Eve plays a transition rir_i over aia_i A play is the infinite word w=a0a1…w=a_0a_1\ldots and the sequence of transitions r=r0r1…r=r_0r_1\ldots Eve wins if either ww is not in L(A)L(A) or rr is an accepting run over ww in AA. Game II. At each turn turn ii: Adam plays a letter aia_i Eve plays a transition rir_i over aia_i Adam plays a pair of transitions sis_i and tit_i A play is the triple of sequences of runs r=r0r1…,s=s0s1…r=r_0r_1\ldots, s=s_0s_1\ldots and t=t0t1…t=t_0t_1\ldots Eve wins if either rr is an accepting run of AA or both ss and tt are not accepting runs of AA. The problem We know that these two games have the same winner when AA 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.

Coming soon

Organizer

Boyuan Wang portraitBoyuan Wang
Minghan Wang portraitMinghan Wang
Bochao Li portraitBochao Li
Hongwei Hu portraitHongwei Hu