Faster Game Solving by Fixpoint Acceleration
Daniel Hausmann
TL;DR
This work tackles solving parity games by exploiting cycle-free DAG sub-structures to accelerate fixpoint computation. It introduces a DAG-attractor framework that restricts the fixpoint domain to non-DAG nodes, enabling large-step solving with complexity improvements driven by $m=|V'|$ and the number of priorities $k$, including a quasipolynomial bound via universal trees. Additionally, the paper extends to Emerson-Lei objectives through an economic LAR reduction that preserves DAG structure, yielding equivalent parity games $P(G)$ where the same acceleration applies. The combined approach offers faster, symbolically solvable game-solving methods with potential impact on model checking and satisfiability tasks. Overall, the method narrows the solution domain and increases convergence speed, while the LAR extension broadens applicability to richer objective classes.
Abstract
We propose a method for solving parity games with acyclic (DAG) sub-structures by computing nested fixpoints of a DAG attractor function that lives over the non-DAG parts of the game, thereby restricting the domain of the involved fixpoint operators. Intuitively, this corresponds to accelerating fixpoint computation by inlining cycle-free parts during the solution of parity games, leading to earlier convergence. We also present an economic later-appearance-record construction that takes Emerson-Lei games to parity games, and show that it preserves DAG sub-structures; it follows that the proposed method can be used also for the accelerated solution of Emerson-Lei games.