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\'{n}ski and Lazi\'{c} (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.

翻译：我们提出了一种求解具有$n$个顶点、$m$条边和$k$种颜色的图上的拉宾与斯特里特博弈的算法，该算法运行时间为$\tilde{O}\left(mn(k!)^{1+o(1)} \right)$，空间复杂度为$O(nk\log k \log n)$，其中$\tilde{O}$隐藏了对数多项式因子。与当前最佳运行时间$O\left(mn^2(k!)^{2+o(1)}\right)$（通过将拉宾博弈转化为奇偶博弈得到）相比，我们的算法在$k!$的依赖关系上实现了超二次改进，同时降低了其指数级空间需求。我们的主要技术贡献在于：利用\emph{多彩树}对拉宾博弈的进展度量进行刻画，并通过组合构造方式构建简洁表示的万能多彩树。多彩万能树是Jurdziński与Lazić（2017）用于求解奇偶博弈的万能树、以及Klarlund与Kozen（1991）提出的拉宾进展度量的推广。我们的拉宾博弈算法是一种进展度量提升算法，其中提升操作在简洁的、多彩的万能树上执行。