Rabin Games and Colourful Universal Trees

TL;DR

The paper tackles solving Rabin and Streett games on graphs with $n$ vertices, $m$ edges, and $k$ colours, and achieves a significant improvement by presenting a lifting-based algorithm that operates on colourful universal trees. The core idea is to characterise winning states via colourful trees and progress measures, and then construct universal colourful trees that can embed all relevant instances, enabling succinct representations and efficient navigation. The main results show a running time of $ ilde{O}(m n (k!)^{1+o(1)})$ and space $O(n k \log k \log n)$, improving over the prior $(k!)^{2+o(1)}$-dependent approaches while maintaining polynomial space. This work connects Rabin measures to universal-tree techniques from parity games, offers explicit lifting procedures, and discusses potential symbolic and synthesis-related extensions, illustrating a path toward faster reactive synthesis for omega-regular specifications.

Abstract

We provide an algorithm to solve Rabin and Streett games over graphs with $n$ vertices, $m$ edges, and $k$ colours that runs in $\tilde{O}\left(mn(k!)^{1+o(1)} \right)$ time and $O(nk\log k \log n)$ space, where $\tilde{O}$ hides poly-logarithmic factors. Our algorithm is an improvement by a super quadratic dependence on $k!$ from the currently best known run time of $O\left(mn^2(k!)^{2+o(1)}\right)$, obtained by converting a Rabin game into a parity game, while simultaneously improving its exponential space requirement. Our main technical ingredient is a characterisation of progress measures for Rabin games using \emph{colourful trees} and a combinatorial construction of succinctly-represented, universal colourful trees. Colourful universal trees are generalisations of universal trees used by Jurdziński and Lazić (2017) to solve parity games, as well as of Rabin progress measures of Klarlund and Kozen (1991). Our algorithm for Rabin games is a progress measure lifting algorithm where the lifting is performed on succinct, colourful, universal trees.