Succinct progress measures for solving parity games
arXiv:1702.05051 · doi:10.1109/LICS.2017.8005092
Abstract
The recent breakthrough paper by Calude et al. has given the first algorithm for solving parity games in quasi-polynomial time, where previously the best algorithms were mildly subexponential. We devise an alternative quasi-polynomial time algorithm based on progress measures, which allows us to reduce the space required from quasi-polynomial to nearly linear. Our key technical tools are a novel concept of ordered tree coding, and a succinct tree coding result that we prove using bounded adaptive multi-counters, both of which are interesting in their own right.
References in corpus (1)
Cited by in corpus (16)
- Succinct progress measures for solving parity games
- Oink: an Implementation and Evaluation of Modern Parity Game Solvers
- Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games
- A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games
- Games on Graphs: From Logic and Automata to Algorithms
- Robust Exponential Worst Cases for Divide-et-Impera Algorithms for Parity Games
- Simple Fixpoint Iteration To Solve Parity Games
- A Comparison of BDD-Based Parity Game Solvers
- Parity games and universal graphs
- A Parity Game Tale of Two Counters
- Finite-state Strategies in Delay Games
- Smaller Progress Measures and Separating Automata for Parity Games
- The Theory of Universal Graphs for Infinite Duration Games
- An Objective Improvement Approach to Solving Discounted Payoff Games
- Complexity results for modal logic with recursion via translations and tableaux
- New Algorithms for Combinations of Objectives using Separating Automata