The Rabin index for parity games: reducing complexity via its approximation

We define equivalence relations on coloring functions that forget the ownership structure of parity games. These relations give rise to Rabin indices of parity games. Then we develop algorithms that either compute these Rabin indices in exponential time or over-approximate these Rabin indices in time linear in the number of edges and nodes. Our experimental data on random and non-random games show our over-approximating algorithms often markedly reduce the index of parity games and, on average, do improve the speed of solvers for parity games.

This is joint work with Michael Huth and Nir Piterman.