The Fixpoint-Iteration Algorithm for Parity Games
The Fixpoint-Iteration Algorithm for Parity Games
复制标题
DOI：
10.4204/eptcs.161.12
复制
发表时间：
2014-01-01
影响因子：
--
通讯作者：
Lange, Martin
中科院分区：
文献类型：
--
作者：
Bruse, Florian;Falk, Michael;Lange, Martin
众所周知，模态μ演算的模型检测问题归结为解决奇偶博弈的问题，反之亦然。后者是实现的Walukiewicz公式，满足了一个节点在平价游戏如果玩家0赢得了游戏从这个节点。因此，他们定义了她的获胜区域，并且任何模态μ演算的模型检查算法，适当地专用于Walukiewicz公式，产生了一个解决奇偶博弈的算法。在本文中，我们研究的效果，采用最直接的μ演算模型检测算法：不动点迭代。这也是为数不多的算法之一，如果不是唯一的一个，最初不是为奇偶博弈解决而设计的。虽然一项实证研究很快表明，这并不能产生一个在实践中运行良好的算法，但从理论上讲，这是有趣的，原因有两个：首先，它在几乎所有游戏家族上都是指数级的，这些游戏家族被设计为非常特定的算法的下限，这表明不动点迭代与所有这些算法都有联系。其次，不动点迭代不计算位置获胜策略。请注意，Walukiewicz公式只定义了获胜区域;为了使该算法计算获胜策略，还需要一些额外的工作。我们表明，这些是特殊的指数空间的战略，我们称之为最终位置，我们展示了如何位置的，可以从他们中提取。
It is known that the model checking problem for the modal mu-calculus reduces to the problem of solving a parity game and vice-versa. The latter is realised by the Walukiewicz formulas which are satisfied by a node in a parity game iff player 0 wins the game from this node. Thus, they define her winning region, and any model checking algorithm for the modal mu-calculus, suitably specialised to the Walukiewicz formulas, yields an algorithm for solving parity games. In this paper we study the effect of employing the most straight-forward mu-calculus model checking algorithm: fixpoint iteration. This is also one of the few algorithms, if not the only one, that were not originally devised for parity game solving already. While an empirical study quickly shows that this does not yield an algorithm that works well in practice, it is interesting from a theoretical point for two reasons: first, it is exponential on virtually all families of games that were designed as lower bounds for very particular algorithms suggesting that fixpoint iteration is connected to all those. Second, fixpoint iteration does not compute positional winning strategies. Note that the Walukiewicz formulas only define winning regions; some additional work is needed in order to make this algorithm compute winning strategies. We show that these are particular exponential-space strategies which we call eventually-positional, and we show how positional ones can be extracted from them.