Emptiness Of Alternating Tree Automata Using Games With Imperfect Information

Abstract

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.