Emptiness Of Alternating Tree Automata Using Games With Imperfect Information. Fijalkow, N., Pinchinat, S., & Serre, O. 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   
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