Winning Cores in Parity Games

TL;DR

This paper introduces winning cores in parity games and presents a polynomial-time approximation algorithm that improves solving efficiency and accuracy over existing methods, with promising experimental results.

Contribution

It proposes the novel concept of winning cores and develops a new approximation algorithm that outperforms current algorithms in solving parity games.

Findings

Algorithm significantly outperforms existing methods on benchmarks.

Winning core contains all fatal attractors, aiding in game analysis.

Experimental results show high quality of approximation and faster running times.

Abstract

We introduce the novel notion of winning cores in parity games and develop a deterministic polynomial-time under-approximation algorithm for solving parity games based on winning core approximation. Underlying this algorithm are a number properties about winning cores which are interesting in their own right. In particular, we show that the winning core and the winning region for a player in a parity game are equivalently empty. Moreover, the winning core contains all fatal attractors but is not necessarily a dominion itself. Experimental results are very positive both with respect to quality of approximation and running time. It outperforms existing state-of-the-art algorithms significantly on most benchmarks.