Rabin games and colourful universal trees

We provide an algorithmto solve Rabin and Streett games over graphs with n vertices,m edges, and k colours that runs in ˜O³mn(k!)1+o(1)´time and O(nk logk logn) space, where ˜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³mn2(k!)2+o(1)´, obtained by converting a Rabin gameinto a parity game,while simultaneously improving its exponential space requirement. Our main technical ingredient is a characterisation of progress measures for Rabin games using colourful trees and a combinatorial construction of succinctlyrepresented, universal colourful trees. Colourful universal trees are generalisations of universal trees used by Jurdzi´nski 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.