The Rabin index of parity games

TL;DR

This paper investigates the Rabin index of parity games, providing complexity results, an exponential algorithm for exact computation, and a polynomial-time approximation method with practical effectiveness.

Contribution

It introduces the concept of the Rabin index for parity games, analyzes its computational complexity, and proposes algorithms for exact and approximate computation.

Findings

Deciding Rabin index ≥ k is in PTIME for k=1

Deciding Rabin index ≥ k is NP-hard for fixed k > 1

The exponential algorithm effectively computes the Rabin index, and the polynomial approximation performs well in practice

Abstract

We study the descriptive complexity of parity games by taking into account the coloring of their game graphs whilst ignoring their ownership structure. Colored game graphs are identified if they determine the same winning regions and strategies, for all ownership structures of nodes. The Rabin index of a parity game is the minimum of the maximal color taken over all equivalent coloring functions. We show that deciding whether the Rabin index is at least k is in PTIME for k=1 but NP-hard for all fixed k > 1. We present an EXPTIME algorithm that computes the Rabin index by simplifying its input coloring function. When replacing simple cycle with cycle detection in that algorithm, its output over-approximates the Rabin index in polynomial time. Experimental results show that this approximation yields good values in practice.