论文标题
可折叠的下降奇偶校验游戏
Collapsible Pushdown Parity Games
论文作者
论文摘要
本文研究了无限图表上基于折叠图的两种竞争对手完美信息的平均游戏,即可折叠式下降自动机产生的游戏。研究这些游戏的主要动机来自可折叠的下降自动机和高阶递归方案的联系,这两种模型均用于产生无限树。我们的主要结果是确定此类游戏的可决定性,并为获胜区和获胜策略提供有效的代表。因此,此处获得的结果提供了所有必要的工具,以深入研究由可折叠的下降自动机/递归方案产生的树木的逻辑特性。
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.