Solving Parity Games in Theory and Practice

从理论和实践中解决平价博弈

基本信息

批准号：
EP/P020909/1
负责人：
Sven Schewe
金额：
$ 52.13万
依托单位：
University of Liverpool
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2017
资助国家：
英国
起止时间：
2017 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FP020909%2F1
关键词：
Solving Parity Games Theory Practice

项目摘要

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.

平价游戏是一个有趣的问题类别，因为它们易于说明，并且被证明可以抵抗无数尝试对其复杂性进行分类的尝试。同时，用于解决平等游戏的算法在模型检查，满意度检查和合成中起着至关重要的作用。在本项目中，我们将实现上述目标。1。确定或缩小解决平等和回报游戏的复杂性。基本的开放问题是P。我们将在两个方向上进行均等游戏的成员资格，试图改善已知的上限和下限，并研究不同类型的奇偶校验和回报游戏之间的关系。1A.1A。上范围是解决平等游戏是可以解决的，金布里姆解决方案将是找到用于解决平等游戏的多项式时间算法。第二最佳上限是建立FPTA算法，其中优先级是参数。进一步的有趣问题是改善了对优先级的依赖，这些优先级以前从n^p到n^（p/2）提高了具有N个州和P优先级的平等游戏的N^（p/3），并改善了已知的n^\ sqrt（n）的n^\ sqrt（n）的n^\ sqrt界限。较低的范围认为，平均游戏是无法处理的，找到超级多项式下限将是金色的解决方案。但是，没有可用的非平凡多项式界限，也没有基于下限的证据，例如在强烈的指数时间假设上，可以为棘手的证明提供一个起点1c。将2个球员均等与均值，打折和简单的随机游戏联系起来。从平均值到平均收益和简单随机游戏的折扣回报，有一个简单的多项式时间减少。后者是所有这些游戏的2.5播放器（2个对抗玩家和一个随机玩家）的多项式时间。我们将研究其他方向的减少。2。描述可以有效解决的奇偶校验和回报游戏的类别。许多不同的情况可以在多项式时间内解决平价游戏。这是一个重要的游戏，包括具有一定优先级的游戏，以及具有有限数量的玩家节点（尤其是一个玩家游戏）的游戏和具有简单结构的竞技场的游戏，例如有限的树宽，dag宽度，dag宽度，clique宽度，凯利（Kelly）宽度，凯利（Kelly图形，并将此分析扩展到收益游戏。我们还将基于使用多项式算法的部分求解器的组合进行进一步的研究，该算法仅解决平等游戏的子类，目的是定义越来越大的游戏类别的游戏，这些游戏可以在多项式时间内解决。3。为了开发算法以良好的性能解决奇偶校验和回报游戏。要实现这一目标，我们使用前两个工作包的见解来开发具有良好性能的进一步算法，尤其是策略改进算法。我们将重点关注的另一个方面是研究用于解决平等游戏的分布式算法，利用GPU来解决平等和回报游戏的力量4。为了开发用于解决奇偶校验和回报游戏的快速算法。在本文中，我们将实施模型检查和合成工具中最有希望的算法。