Static Analysis of Parity Games: Alternating Reachability Under Parity
Static Analysis of Parity Games: Alternating Reachability Under Parity
复制标题
平价博弈的静态分析：平价下的交替可达性
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Nir Piterman
中科院分区：
文献类型：
--
作者：
M. Huth;Jim Huan;Nir Piterman
众所周知，解决奇偶博弈相当于多项式时间，相当于模式微积分的模型检验。能否在多项式时间内求解奇偶对策或模型检验模微积分公式一直是一个悬而未决的问题。最近研究这个问题的方法是设计部分解算器，这是一种在多项式时间内运行的算法，可能只解决对等游戏的部分问题。尽管事实证明，这种部分求解器可以完全解决许多实际基准问题，但这种部分求解器的设计有些特别，限制了对这种方法潜力的深入了解。我们在这里的意思是通过一种新的博弈形式，在同等条件下交替可达性，为更深层次的分析提供这样坚实的基础。我们证明了这些对策的确定性，并利用这种确定性为每个局中人定义了一个与对等对策的大小成线性关系的高度有序区域上的单调不动点，使得在其最大不动点上的所有结点都被该局中人赢得。通过理论和实验工作，我们证明了这种最大不动点及其计算导致了在多项式时间内运行的部分求解器。这些局部解算器基于已建立的静态分析原理，比现有工作中研究的部分解算器更有效。
It is well understood that solving parity games is equivalent, upi¾?to polynomial time, to model checking of the modal mu-calculus. It is a long-standing open problem whether solving parity games or model checking modal mu-calculus formulas can be done in polynomial time. Ai¾?recent approach to studying this problem has been the design of partial solvers, algorithms that run in polynomial time and that may only solve parts of a parity game. Although it was shown that such partial solvers can completely solve many practical benchmarks, the design of such partial solvers was somewhat ad hoc, limiting a deeper understanding of the potential of that approach. We here mean to provide such robust foundations for deeper analysis through a new form of game, alternating reachability under parity. We prove the determinacy of these games and use this determinacy to define, for each player, a monotone fixed point over an ordered domain of height linear in the size of the parity game such that all nodes in its greatest fixed point are won by said player in the parity game. We show, through theoretical and experimental work, that such greatest fixed points and their computation leads to partial solvers that run in polynomial time. These partial solvers are based on established principles of static analysis and are more effective than partial solvers studied in extant work.
DOI：
10.1007/3-540-45931-6
发表时间：
2002-04
期刊：
--
影响因子：
--
作者：
M. Nielsen;Uffe Engberg
通讯作者：
M. Nielsen;Uffe Engberg