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(mnk+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 raning 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(nk+1k!)
and space O(nk+1k!). These results improve on the
current bounds of O(mn2kk!) time in the case of direct
(symbolic) solution or O(m(nk2k!)k) in the case
of reduction to parity games.
PDF