Winning Regions of Higher-Order Pushdown Games
Winning Regions of Higher-Order Pushdown Games
复制标题
DOI：
10.1109/lics.2008.41
复制
发表时间：
2008-06
期刊：
影响因子：
--
通讯作者：
Arnaud Carayol;M. Hague;A. Meyer;C. Ong;O. Serre
中科院分区：
文献类型：
--
作者：
Arnaud Carayol;M. Hague;A. Meyer;C. Ong;O. Serre
本文考虑由高阶下推自动机定义的奇偶对策。这些自动机通过使用高阶堆栈来推广下推自动机，高阶堆栈是嵌套的“堆栈”结构。用通常的方式将高阶堆栈表示为括号良好的单词，我们表明这些游戏的获胜区域是规则的单词集。此外，可以有效地计算识别该区域的有限自动机。我们工作的一个新奇之处是抽象下推过程，它可以被视为(普通的)下推自动机，但具有无限的堆栈字母表。从我们关于奇偶博弈获胜区域的主要结果出发，我们推导出了高阶下推图的MODAL Mu-Calculus全局模型检查问题的解，以及高阶安全递归方案生成的排序树的解。
In this paper we consider parity games defined by higher-order pushdown automata. These automata generalise pushdown automata by the use of higher-order stacks, which are nested "stack of stacks" structures. Representing higher-order stacks as well-bracketed words in the usual way, we show that the winning regions of these games are regular sets of words. Moreover a finite automaton recognising this region can be effectively computed. A novelty of our work are abstract pushdown processes which can be seen as (ordinary) pushdown automata but with an infinite stack alphabet. We use the device to give a uniform presentation of our results.From our main result on winning regions of parity games we derive a solution to the Modal Mu-Calculus Global Model-Checking Problem for higher-order pushdown graphs as well as for ranked trees generated by higher-order safe recursion schemes.