A Parity Game Tale of Two Counters
arXiv:1807.10210 · doi:10.4204/EPTCS.305.8
Abstract
Parity games are simple infinite games played on finite graphs with a winning condition that is expressive enough to capture nested least and greatest fixpoints. Through their tight relationship to the modal mu-calculus, they are used in practice for the model-checking and synthesis problems of the mu-calculus and related temporal logics like LTL and CTL. Solving parity games is a compelling complexity theoretic problem, as the problem lies in the intersection of UP and co-UP and is believed to admit a polynomial-time solution, motivating researchers to either find such a solution or to find superpolynomial lower bounds for existing algorithms to improve the understanding of parity games. We present a parameterized parity game called the Two Counters game, which provides an exponential lower bound for a wide range of attractor-based parity game solving algorithms. We are the first to provide an exponential lower bound to priority promotion with the delayed promotion policy, and the first to provide such a lower bound to tangle learning.
arXiv commentIn Proceedings GandALF 2019, arXiv:1909.05979
References in corpus (10)
- Succinct progress measures for solving parity games
- Oink: an Implementation and Evaluation of Modern Parity Game Solvers
- Attracting Tangles to Solve Parity Games
- An Exponential Lower Bound for the Latest Deterministic Strategy Iteration Algorithms
- Non-oblivious Strategy Improvement
- The Fixpoint-Iteration Algorithm for Parity Games
- Zielonka's Recursive Algorithm: dull, weak and solitaire games and tighter bounds
- Robust Exponential Worst Cases for Divide-et-Impera Algorithms for Parity Games
- A Delayed Promotion Policy for Parity Games
- Simple Fixpoint Iteration To Solve Parity Games