改进的基于集合的奇偶博弈符号算法

奇偶对策的有效并行策略改进

Efficient Parallel Strategy Improvement for Parity Games

我们研究解决奇偶博弈的策略改进算法。虽然这些算法已知使用非常少量的迭代来解决奇偶博弈，但实验研究发现，高步骤复杂性导致它们在实践中表现不佳。在本文中，我们试图解决这种情况。算法的每次迭代都必须计算最佳响应，而标准的方法是使用Bellman-Ford算法，我们给出的实验结果表明，一个球员的策略改进显着优于这种技术在实践中。然后，我们研究的最佳方式来实现一个球员的战略改进，我们开发了一个有效的并行算法来执行这项任务，通过减少问题的计算前缀和链表。我们报告这些算法的实验结果，我们发现，该算法的GPU实现显示了显着的加速比单核和多核CPU实现。

Smaller Progress Measures and Separating Automata for Parity Games

Calude et al. have recently shown that parity games can be solved in quasi-polynomial time, a landmark result that has led to a number of approaches with quasi-polynomial complexity. Jurdinski and Lasic have further improved the precise complexity of parity games, especially when the number of priorities is low (logarithmic in the number of positions). Both of these algorithms belong to a class of game solving techniques now often called separating automata: deterministic automata that can be used as witness automata to decide the winner in parity games up to a given number of states and colou…

求解奇偶对策的新确定性算法

New Deterministic Algorithms for Solving Parity Games

我们研究奇偶游戏，其中两个玩家之一控制只有少量的$k$的节点和其他玩家控制的$n-k$的其他节点的游戏。我们的主要结果是一个固定参数的算法，解决了时间$k^{O(\sqrt{k})}\cdot O(n^3)$的二部奇偶游戏，和一般的奇偶游戏的时间$(p+k)^{O(\sqrt{k})} \cdot O(pnm)$，其中$p$是不同的优先级和$m$是边缘的数量。对于所有使用$k = o(n)$的游戏，这改进了Jurdzi{\displaystyle Jurdzi}ski，Paterson和Zwick（SICOMP 2008）以前最快的算法。我们还获得了新的核化结果和一个改进的确定性算法的平均度小的图。

吸引子即一切：多项式时间求解奇偶博弈

Attractors Is All You Need: Parity Games In Polynomial Time

本文提出一种仅移除已确定获胜者区域的新型吸引子算法，以多项式时间求解奇偶博弈并保证找到最小统治域，终结了该问题数十年的研究探索。

Leveraging the Power of Graph Algorithms: Efficient Algorithms for Computer-Aided Verification

The goal of the thesis is to leverage fast graph algorithms and modern algorithmic techniques for problems in model checking and synthesis on graphs, MDPs, and game graphs. The results include symbolic algorithms, a well-known class of algorithms in model checking that trades limited access to the input model for an efficient representation. In particular, we present the following results: Algorithms for game graphs with mean-payoff Büchi objectives and mean-payoff coBüchi objectives which match one of the best running time bounds for mean-payoff objectives. A near-linear time randomized algor…

The Strahler number of a parity game

The Strahler number of a rooted tree is the largest height of a perfect binary tree that is its minor. The Strahler number of a parity game is proposed to be defined as the smallest Strahler number of the tree of any of its attractor decompositions. It is proved that parity games can be solved in quasi-linear space and in time that is polynomial in the number of vertices~$n$ and linear in $({d}/{2k})^k$, where $d$ is the number of priorities and $k$ is the Strahler number. This complexity is quasi-polynomial because the Strahler number is at most logarithmic in the number of vertices. The proo…

Solving Parity Games Using An Automata-Based Algorithm

Parity games are abstract infinite-round games that take an important role in formal verification. In the basic setting, these games are two-player, turn-based, and played under perfect information on directed graphs, whose nodes are labeled with priorities. The winner of a play is determined according to the parities (even or odd) of the minimal priority occurring infinitely often in that play. The problem of finding a winning strategy in parity games is known to be in UPTime $\cap$ CoUPTime and deciding whether a polynomial time solution exists is a long-standing open question. In the last t…

奇偶对策Divide-et-Impera算法的鲁棒指数最坏情况

Robust Exponential Worst Cases for Divide-et-Impera Algorithms for Parity Games

McNaughton-Zielonka divide et impera算法是文献中用于确定奇偶博弈中的获胜者的最简单和最灵活的方法。尽管其理论上的最坏情况下的复杂性和负面声誉作为一个效率低下的算法在实践中，它已被证明是最好的技术之一，为解决这类游戏。此外，它被证明是抵抗下界攻击，甚至超过战略改进的方法，直到最近的一个家庭的游戏，该算法需要指数时间已由弗里德曼提供。对该族的简单分析表明，一个简单的记忆技术可以帮助算法在多项式时间内求解该族。同样的结果也可以通过利用文献中提出的基于支配分解技术的方法来实现。这些意见提出了一个问题，动态规划和游戏分解技术的适当组合，可以改善指数最坏情况下的原始算法。在本文中，我们回答这个问题否定的，通过提供一个强大的指数最坏的情况下，表明没有交织的上述技术可以帮助减轻指数性质的划分等impera方法。

A symmetric attractor-decomposition lifting algorithm for parity games

Progress-measure lifting algorithms for solving parity games have the best worst-case asymptotic runtime, but are limited by their asymmetric nature, and known from the work of Czerwiński et al. (2018) to be subject to a matching quasi-polynomial lower bound inherited from the combinatorics of universal trees. Parys (2019) has developed an ingenious quasi-polynomial McNaughton- Zielonka-style algorithm, and Lehtinen et al. (2019) have improved its worst-case runtime. Jurdziński and Morvan (2020) have recently brought forward a generic attractor-based algorithm, formalizing a second class of qu…

无限对策的线性互补算法

Linear Complementarity Algorithms for Infinite Games

两个旋转算法的性能，由于Lemke和Cottle和Dantzig，研究线性互补问题（LCP）所产生的无限游戏，如奇偶校验，平均奖励，折扣游戏。该算法以前没有在无限博弈的背景下进行过研究，它们提供了经典策略改进算法的替代方案。这两个算法是纯粹的折扣游戏，从而绕过减少从游戏到LCP，从而促进更好地理解的算法时，应用于游戏。一个家庭的奇偶校验游戏，这两个算法在指数时间内运行，表明在最坏的情况下，他们没有更好的表现为奇偶校验，平均奖励，或折扣游戏比他们一般的P-矩阵LCP。

奇偶博弈随机刻面算法的次指数下界

Errata for: A subexponential lower bound for the Random Facet algorithm for Parity Games

在Friedmann、Hansen和Zwick（2011）中，我们声称Kalai、Matousek、Sharir和Welzl的Random-Facet算法执行的旋转步骤的预期数量等于Random-Facet^* 执行的旋转步骤的预期数量，Random-Facet是Random-Facet的一个变体，其随机决策基于一个随机排列。然后我们得到了Random-Facet^* 执行的旋转步骤的预期数量的下限，并声称同样的下限也适用于Random-Facet。不幸的是，Random-Facet和Random-Facet^* 执行的预期步骤数相同的说法是错误的。我们在这里提供了简单的例子，表明这两种算法所执行的步骤的预期数量是不一样的。

奇偶对策的延迟升级策略

A Delayed Promotion Policy for Parity Games

奇偶博弈是图上的两人无限持续时间博弈，在理论计算机科学的各个领域都起着至关重要的作用。在实践中找到有效的算法来解决这些游戏被广泛认为是形式化验证中的核心问题，因为它导致表达时态逻辑的模型检查和可满足性问题的有效解决方案，例如，modal muCalculus。他们的解决方案可以归结为确定游戏的位置集的问题，称为domestic，在每个位置中，玩家可以通过永远留在集合中来迫使获胜。最近，一种新的技术来计算领域，称为优先级提升，已被提出，这是基于准领域的概念，一个宽松的形式的领域，和领域空间。底层框架足够通用，以适应不同的实例化的解决方案的过程中，其正确性是由空间本身的性质。在本文中，我们提出了一个新的这样的实例，称为延迟推广，试图减少可能的指数行为所表现出的原始方法在最坏的情况下。由此产生的程序不仅往往优于原来的优先级提升方法，但到目前为止，没有指数最坏的情况下是已知的。

求解奇偶博弈的拟多项式算法的改进复杂度分析

Improved Complexity Analysis of Quasi-Polynomial Algorithms Solving Parity Games

本研究针对顶点带优先级的奇偶博弈求解问题，基于通用树算法通过细化通用树宽度分析、改用n/2-通用树两项改进，将d=ω(log n)场景下的拟多项式复杂度提升了θ(d²)倍。