Jurdzinski-ing Rabin and Streett

In this paper we give a recursive fixpoint characterization of the winning regions in Rabin and Streett games. We use this characterization in two ways. First, we introduce direct Rabin and Streett ranking that are a sound and complete way to characterize the winning sets in the respective games. By computing directly and explicitly the ranking we can solve such games in time $O(mn^{k+1}kk!)$ and space $O(nk)$ for Rabin and $O(nkk!)$ for Streett where $n$ is the number of states, $m$ the number of transitions, and $k$ the number of pairs in the winning condition. Second, by keeping intermediate values during the fixpoint evaluation, we can solve such games symbolically in time $O(n^{k+1}k!)$ and space $O(n^{k+1}k!)$. These results improve on the current bounds of O(mn^{2k}k!)$time in the case of direct (symbolic) solution or$O(m(nk^2k!)^k)$ in the case of reduction to parity games.