Collapsible Pushdown Parity Games
Formal Languages and Automata Theory
2020-10-14 v1 Logic in Computer Science
Abstract
This paper studies a large class of two-player perfect-information turn-based parity games on infinite graphs, namely those generated by collapsible pushdown automata. The main motivation for studying these games comes from the connections from collapsible pushdown automata and higher-order recursion schemes, both models being equi-expressive for generating infinite trees. Our main result is to establish the decidability of such games and to provide an effective representation of the winning region as well as of a winning strategy. Thus, the results obtained here provide all necessary tools for an in-depth study of logical properties of trees generated by collapsible pushdown automata/recursion schemes.
Keywords
Cite
@article{arxiv.2010.06361,
title = {Collapsible Pushdown Parity Games},
author = {Christopher H. Broadbent and Arnaud Carayol and Matthew Hague and Andrzej S. Murawski and C. -H. Luke Ong and Olivier Serre},
journal= {arXiv preprint arXiv:2010.06361},
year = {2020}
}
Comments
51 pages