Parity Games Played on Transition Graphs of One-Counter Processes
Parity Games Played on Transition Graphs of One-Counter Processes
复制标题
在单柜台进程的转换图上玩的奇偶游戏
DOI：
10.1007/11690634_23
复制
发表时间：
2006
影响因子：
0.5
通讯作者：
O. Serre
中科院分区：
文献类型：
--
作者：
O. Serre
我们考虑在特殊下推图上进行的奇偶游戏，即由单计数器过程生成的奇偶游戏。对于下推图上的奇偶游戏，从[23]可知，决定获胜者是一个 ExpTime 完全问题。该结果的一个重要推论是下推过程的 μ 微积分模型检查问题是 ExpTime 完备的。由于单计数器过程是下推过程的特例，因此，在单计数器过程的转换图上进行的奇偶游戏中决定获胜者可以在 ExpTime 中实现。然而，[23] 的 ExpTime-hardness 下限的证明不能适应这种情况。因此，一个自然的问题是在这种特殊情况下是否可以改进 ExpTime 上限。在本文中，我们采用[11,4]中的技术并为此问题提供了 PSpace 上限和 DP-hard 下界。我们还给出了这个结果的两个重要后果。首先，我们改进了针对 μ 微积分的模型检查单计数器过程已知的最佳上限。其次，我们展示了如何使用这些游戏来解决具有获胜条件的下推游戏，这些获胜条件是控制状态上的奇偶条件与堆栈高度上的条件的布尔组合。
We consider parity games played on special pushdown graphs, namely those generated by one-counter processes. For parity games on pushdown graphs, it is known from [23] that deciding the winner is an ExpTime-complete problem. An important corollary of this result is that the μ-calculus model checking problem for pushdown processes is ExpTime-complete. As one-counter processes are special cases of pushdown processes, it follows that deciding the winner in a parity game played on the transition graph of a one-counter process can be achieved in ExpTime. Nevertheless the proof for the ExpTime-hardness lower bound of [23] cannot be adapted to that case. Therefore, a natural question is whether the ExpTime upper bound can be improved in this special case. In this paper, we adapt techniques from [11,4] and provide a PSpace upper bound and a DP-hard lower bound for this problem. We also give two important consequences of this result. First, we improve the best upper bound known for model-checking one-counter processes against μ-calculus. Second, we show how these games can be used to solve pushdown games with winning conditions that are Boolean combinations of a parity condition on the control states with conditions on the stack height.