eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-12-05
16:1
16:14
10.4230/LIPIcs.FSTTCS.2018.16
article
Büchi Good-for-Games Automata Are Efficiently Recognizable
Bagnol, Marc
1
Kuperberg, Denis
2
LIP, École Normale Supérieure, Lyon, France
CNRS, LIP, École Normale Supérieure, Lyon, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol122-fsttcs2018/LIPIcs.FSTTCS.2018.16/LIPIcs.FSTTCS.2018.16.pdf
Büchi
automata
games
polynomial time
nondeterminism