Solving Parity Games in Theory and Practice

对等游戏是一个耐人寻味的问题类别，因为它们很容易陈述，而且已经被证明抵抗了无数次对其复杂性进行分类的尝试。同时，奇偶博弈的求解算法在模型检验、可满足性检验和综合中起着至关重要的作用。在本项目中，我们将实现上述目标如下。我们将从两个方向进行研究，试图改进已知的上下界，并研究不同类型的对等对策与支付对策之间的关系。上界假设求解平价对策是容易的，金边解将是找到求解平价对策的多项式时间算法。第二个最好的上限是建立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.