Faster Solutions of Rabin and Streett Games

In this paper we improve the complexity of solving Rabin and Streett games to approximately the square root of previous bounds. 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+1kk!) 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. In order to prove completeness of the ranking method we give a recursive fixpoint characterization of the winning regions in these games. We then show that by keeping intermediate values during the fixpoint evaluation, we can solve such games symbolically in time O(n^k+1k!) and space O(n^k+1k!). These results improve on the current bounds of O(mn^2kk!) time in the case of direct (symbolic) solution or O(m(nk²k!)^k) in the case of reduction to parity games