TY - GEN
T1 - Emptiness of alternating tree automata using games with imperfect information
AU - Fijalkow, Nathanaël
AU - Pinchinat, Sophie
AU - Serre, Olivier
N1 - Publisher Copyright:
© Nathanaël Fijalkow, Sophie Pinchinat, and Olivier Serre.
PY - 2013/12/1
Y1 - 2013/12/1
N2 - We consider the emptiness problem for alternating tree automata, with two acceptance semantics: classical (all branches are accepted) and qualitative (almost all branches are accepted). For the classical semantics, the usual technique to tackle this problem relies on a Simulation Theorem which constructs an equivalent non-deterministic automaton from the original alternating one, and then checks emptiness by a reduction to a two-player perfect information game. However, for the qualitative semantics, no simulation of alternation by means of non-determinism is known. We give an alternative technique to decide the emptiness problem of alternating tree automata, that does not rely on a Simulation Theorem. Indeed, we directly reduce the emptiness problem to solving an imperfect information two-player parity game. Our new approach can successfully be applied to both semantics, and yields decidability results with optimal complexity; for the qualitative semantics, the key ingredient in the proof is a positionality result for stochastic games played over infinite graphs.
AB - We consider the emptiness problem for alternating tree automata, with two acceptance semantics: classical (all branches are accepted) and qualitative (almost all branches are accepted). For the classical semantics, the usual technique to tackle this problem relies on a Simulation Theorem which constructs an equivalent non-deterministic automaton from the original alternating one, and then checks emptiness by a reduction to a two-player perfect information game. However, for the qualitative semantics, no simulation of alternation by means of non-determinism is known. We give an alternative technique to decide the emptiness problem of alternating tree automata, that does not rely on a Simulation Theorem. Indeed, we directly reduce the emptiness problem to solving an imperfect information two-player parity game. Our new approach can successfully be applied to both semantics, and yields decidability results with optimal complexity; for the qualitative semantics, the key ingredient in the proof is a positionality result for stochastic games played over infinite graphs.
KW - Alternating automata
KW - Emptiness checking
KW - Imperfect information games
KW - Two-player games
U2 - 10.4230/LIPIcs.FSTTCS.2013.299
DO - 10.4230/LIPIcs.FSTTCS.2013.299
M3 - Conference contribution
AN - SCOPUS:84907553162
T3 - Leibniz International Proceedings in Informatics, LIPIcs
SP - 299
EP - 311
BT - Leibniz International Proceedings in Informatics, LIPIcs
A2 - Seth, Anil
A2 - Vishnoi, Nisheeth K.
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 33rd International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2013
Y2 - 12 December 2013 through 14 December 2013
ER -