论文标题
平价游戏和嵌套fixpoint的通用算法
Universal Algorithms for Parity Games and Nested Fixpoints
论文作者
论文摘要
赋予了用于解决平等游戏的吸引子分解元算象，它概括了经典的McNaughton-Zielonka算法及其最近由于Parys而引起的准级 - 多项式变体（2019），以及Lehtinen，Schewe，Schewe和Wojtczak（2019）。所研究和利用的中心概念是多米尼亚在平等游戏中的吸引子分解以及描述吸引子分解的诱导结构的有序树。通用算法在将合适的通用树作为输入时，将McNaughton-Zielonka，Parys和Lehtinen-Schewe-Wojtczak算法作为特殊情况。主要技术结果为这些算法提供了统一的正确性和结构见解。适当地将通用算法用于奇偶校验游戏来固定点游戏，可以通过有限的完整晶格来计算嵌套的fixpoints。可以象征性地实现平等游戏和嵌套固定点的通用算法。它显示了如何使用$ O（\ lg d）$象征空间复杂性来完成，从而改善了Chatterjee，dvoDi光，Henzinger和Svozil（2018）在Prication Games中获得的$ O（d \ lg n）$象征空间的复杂性，其中$ n $是$ n $ n $ d $ d $ distical nistical nistical and and difters parity n数字。
An attractor decomposition meta-algorithm for solving parity games is given that generalises the classic McNaughton-Zielonka algorithm and its recent quasi-polynomial variants due to Parys (2019), and to Lehtinen, Schewe, and Wojtczak (2019). The central concepts studied and exploited are attractor decompositions of dominia in parity games and the ordered trees that describe the inductive structure of attractor decompositions. The universal algorithm yields McNaughton-Zielonka, Parys, and Lehtinen-Schewe-Wojtczak algorithms as special cases when suitable universal trees are given to it as inputs. The main technical results provide a unified proof of correctness and structural insights into those algorithms. Suitably adapting the universal algorithm for parity games to fixpoint games gives a quasi-polynomial time algorithm to compute nested fixpoints over finite complete lattices. The universal algorithms for parity games and nested fixpoints can be implemented symbolically. It is shown how this can be done with $O(\lg d)$ symbolic space complexity, improving the $O(d \lg n)$ symbolic space complexity achieved by Chatterjee, Dvořák, Henzinger, and Svozil (2018) for parity games, where $n$ is the number of vertices and $d$ is the number of distinct priorities in a parity game.
