Current browse context:
cs.DS
Change to browse by:
References & Citations
Computer Science > Data Structures and Algorithms
Title: Universal Algorithms for Parity Games and Nested Fixpoints
(Submitted on 13 Jan 2020 (v1), last revised 29 Aug 2022 (this version, v2))
Abstract: 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\v{r}\'{a}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.
Submission history
From: Rémi Morvan [view email][v1] Mon, 13 Jan 2020 15:19:05 GMT (210kb,D)
[v2] Mon, 29 Aug 2022 09:08:49 GMT (132kb,D)
Link back to: arXiv, form interface, contact.