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．上限假设解决奇偶博弈是容易处理的，金边解决方案将是找到解决奇偶博弈的多项式时间算法。第二个最佳上限是建立 FPTAS 算法，其中优先级数量是参数。进一步有趣的问题是改善对优先级数量的依赖，对于具有 n 个状态和 p 个优先级的奇偶游戏，优先级数量先前已从 n^p 通过 n^(p/2) 改进到 n^(p/3)，并改进已知的次指数界，目前为 n^\sqrt(n)。本项下的另一个研究分支是估计具有未知复杂度的已知算法的复杂度。1b。下界假设奇偶游戏不易处理，找到超多项式下界将是金边解决方案。然而，没有可用的非平凡多项式界限，也没有基于下限的证明，例如在强指数时间假设上，可以为难处理性证明提供一个起点。1c。将 2 玩家奇偶校验与均值、贴现和简单随机博弈联系起来。从奇偶校验通过平均收益和贴现收益到简单随机博弈，有一个简单的多项式时间减少。后者的多项式时间相当于所有这些游戏的 2.5 个玩家（2 个敌对玩家和一个随机玩家）版本。我们将研究其他方向的减少。 2．描述可以有效解决的平价博弈和支付博弈的类别。已知可以在多项式时间内解决平价博弈的许多不同情况。这主要包括优先级有限的游戏，也包括任一玩家的节点数量有限的游戏（尤其是单人游戏）以及具有简单结构的竞技场的游戏，例如有界树宽度、DAG 宽度、派系宽度、凯利宽度，或纠缠。我们将进一步研究具有较弱限制的限制类图，例如局部有界树宽、排除次要图和无处稠密图，并将这种分析扩展到支付博弈。我们还将进一步研究基于使用多项式算法的部分求解器组合，该算法仅求解奇偶博弈的子类，目的是定义可以在多项式时间内求解的越来越大的博弈类。 3．开发具有良好性能的解决平价和支付游戏的算法。为了实现这一目标，我们利用前两个工作包的见解来开发具有良好性能的进一步算法，特别是策略改进算法。我们将关注的另一个方面是研究解决奇偶游戏的分布式算法，利用 GPU 的能力来解决奇偶游戏和支付游戏。4。开发解决奇偶游戏和支付游戏的快速算法。最后，我们将在模型检查和综合工具中实现最有前途的算法。