In *Proceedings of the 33rd International Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS 2013)*, volume 24, of *LIPIcs*, pages 299-311, 2013. Schloss Dagstuhl - Leibniz-Zentrum für Informatik.

abstract bibtex

abstract bibtex

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.

@inproceedings{FPS13, keywords={perso}, title = {Emptiness Of Alternating Tree Automata Using Games With Imperfect Information}, author = {Nathanaël Fijalkow and Sophie Pinchinat and Olivier Serre}, year={2013}, booktitle = {Proceedings of the 33rd International Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS 2013)}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, series = {LIPIcs}, volume = {24}, pages = {299-311}, 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.}, fulltexturl = {https://hal.inria.fr/hal-01260682}, }

Downloads: 0