Faster Game Solving by Fixpoint Acceleration

TL;DR

This paper introduces a fixpoint acceleration method for solving parity games with DAG sub-structures, improving convergence speed by inlining cycle-free parts, and extends this approach to Emerson-Lei games.

Contribution

It presents a novel fixpoint acceleration technique for parity games with DAG sub-structures and adapts it for Emerson-Lei games, enhancing solution efficiency.

Findings

Accelerates fixpoint computation in parity games.

Preserves DAG sub-structures in Emerson-Lei games.

Enables earlier convergence in game solving.

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.