Solving Parity Games in Theory and Practice

奇偶博弈是一个有趣的问题类，因为它们很容易陈述，并且已经被证明能够抵抗无数次对其复杂性进行分类的尝试。同时，求解奇偶博弈的算法在模型检验、可满足性检验和综合中起着至关重要的作用。确定或缩小解决奇偶性和支付博弈的复杂性。基本的开放性问题是奇偶性博弈在P中的成员资格。我们将从两个方向进行研究，试图改进已知的上界和下界，并研究不同类型的奇偶性和支付博弈之间的关系。上限假设解决奇偶博弈是容易的，金边解决方案将是找到一个多项式时间算法来解决奇偶博弈。第二个最佳上限是建立一个FPTAS算法，其中优先级的数量是参数。进一步有趣的问题是改善对优先级数量的依赖性，对于具有n个状态和p个优先级的奇偶博弈，优先级已经从n^p通过n^（p/2）提高到n^（p/3），并改善已知的次指数界，目前为n^\sqrt（n）。在此项目下研究的另一个分支是估计未知复杂度的已知算法的复杂度。下界假设奇偶博弈不容易处理，找到一个超多项式下界将是黄金边缘的解决方案。然而，没有可用的非平凡多项式边界，并且基于例如强指数时间假设的下界的证明可以为棘手的证明提供起点。将两个局中人的奇偶性与平均、折扣和简单随机博弈联系起来。从奇偶性到平均收益和折扣收益到简单随机博弈有一个简单的多项式时间缩减。后者是多项式时间相当于所有这些游戏的2.5玩家（2个对抗玩家和一个随机玩家）版本。我们将研究其他方面的削减。描述一类可以有效求解的奇偶和支付博弈。已知奇偶博弈可以在多项式时间内求解的许多不同情况。这突出地包括具有有限数量优先级的博弈，但也包括具有有限数量节点的博弈（特别是单人游戏）和竞技场具有简单结构的游戏，如有界树宽，DAG宽度，团宽，Kelly宽度或纠缠。我们将进一步研究具有较弱限制的图的限制类，如局部有界树宽，排除子，和无处密集的图，并扩展这种分析支付游戏。我们还将进一步研究基于使用多项式算法的部分求解器的组合，该算法仅解决奇偶游戏的子类，目的是定义可以在多项式时间内解决的越来越大的游戏类。为了实现这个目标，我们使用前两个工作包中的见解来开发具有良好性能的进一步算法，特别是策略改进算法。我们将重点关注的另一个方面是研究解决奇偶博弈的分布式算法，利用GPU的力量解决奇偶和支付博弈。发展快速演算法以解决奇偶性与支付游戏。最后，我们将在模型检查与综合工具中实作最有前途的演算法。

Parity games are an intriguing problem class, because they are simple to state and have proven to be resistant to countless attempts to classify their complexity. At the same time, algorithms for solving parity games play a paramount role in model checking, satisfiability checking, and synthesis.In this project, we will approach the objectives stated above as follows.1. Determine or narrow down the complexity of solving parity and payoff games.The fundamental open question is the membership of parity games in P. We will research in both directions, trying to improve the known upper and lower bounds and studying the relation between different types of parity and payoff games.1a. Upper boundsAssuming that solving parity games is tractable, the gold-brim solution would be to find a polynomial time algorithm for solving parity games. A second best upper bound would be to establish an FPTAS algorithm, where the number of priorities is the parameter. Further interesting questions are improving the dependency on the number of priorities, which have previously improved from n^p through n^(p/2) to n^(p/3) for parity games with n states and p priorities, and to improve the known sub-exponential bounds, which are currently n^\sqrt(n).Another branch of research under this item is to estimate the complexity of known algorithms with unknown complexity.1b. Lower boundsAssuming that parity games are not tractable, finding a super-polynomial lower bound would be the gold-brim solution. However, there are no non-trivial polynomial bounds available, and proofs of lower bounds based, e.g. on the strong exponential time hypothesis, could provide a starting point for an intractability proof.1c. Connecting 2 player parity with mean, discounted, and simple stochastic games.There is a simple polynomial time reduction from parity through mean payoff and discounted payoff to simple stochastic games. The latter are polynomial time equivalent to the 2.5 player (2 antagonistic players and a random player) version of all of these games. We will research reductions in the other directions.2. To describe classes of parity and payoff games that can be solved efficiently.Many different cases where parity games can be solved in polynomial time are known. This prominently includes games with a bounded number of priorities, but also games with a bounded number of nodes of either player (especially one player games) and games with arenas that have a simple structure, such as bounded treewidth, DAG width, clique width, Kelly width, or entanglement.We will further the research on restricted classes of graphs with weaker restrictions, such as local bounded treewidth, excluded minors, and nowhere dense graphs, and extend this analysis to payoff games. We will also further current research on the combination of partial solvers based on using polynomial algorithms that only solve sub-classes of parity games with the aim of defining increasingly larger classes of games that can be solved in polynomial time.3. To develop algorithms for solving parity and payoff games with good performance.To approach this goal, we use the insights from the first two workpackages to develop further algorithms with good performance, especially strategy improvement algorithms. An additional aspect we will focus on is to study distributed algorithms for solving parity games, harnessing the power of GPUs for solving parity and payoff games.4. To develop fast algorithms for solving parity and payoff games.Finally, we will implement the most promising algorithms in model checking and synthesis tools.