Universal algorithms for parity games and nested fixpoints
From MaRDI portal
(Redirected from Universal algorithms for parity games and nested fixpoints)
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 symbolic space complexity, improving the symbolic space complexity achieved by Chatterjee, Dvov{r}'{a}k, Henzinger, and Svozil (2018) for parity games, where is the number of vertices and is the number of distinct priorities in a parity game.
Recommendations
- Quasipolynomial computation of nested fixpoints
- Universal trees grow inside separating automata: quasi-polynomial lower bounds for parity games
- Parity Games: Zielonka's Algorithm in Quasi-Polynomial Time
- Improved complexity analysis of quasi-polynomial algorithms solving parity games
- A modal \(\mu\) perspective on solving parity games in quasi-polynomial time
Cites work
- A modal \(\mu\) perspective on solving parity games in quasi-polynomial time
- A pseudo-quasi-polynomial algorithm for mean-payoff parity games
- A recursive approach to solving parity games in quasipolynomial time
- A subexponential lower bound for Zadeh's pivoting rule for solving linear programs and games
- Alternating weak automata from universal trees
- Deciding parity games in quasipolynomial time
- Exponential lower bounds for policy iteration
- Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata
- Fast and simple nested fixpoints
- scientific article; zbMATH DE number 1670778 (Why is no real title available?)
- scientific article; zbMATH DE number 5869590 (Why is no real title available?)
- Infinite games on finitely coloured graphs with applications to automata on infinite trees
- Infinite games played on finite graphs
- Lattice-theoretic progress measures and coalgebraic model checking
- Optimal satisfiability checking for arithmetic \(\mu\)-calculi
- Parity Games: Zielonka's Algorithm in Quasi-Polynomial Time
- Practical synthesis of reactive systems from LTL specifications via parity games
- Qualitative concurrent parity games
- Quasipolynomial computation of nested fixpoints
- Quasipolynomial set-based symbolic algorithms for parity games
- Recursive algorithm for parity games requires exponential time
- Subexponential lower bounds for randomized pivoting rules for the simplex algorithm
- Succinct progress measures for solving parity games
- Symbolic model checking: \(10^{20}\) states and beyond
- The mu-calculus and Model Checking
- Universal trees grow inside separating automata: quasi-polynomial lower bounds for parity games
Cited in
(5)
This page was built for publication: Universal algorithms for parity games and nested fixpoints
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6113979)
