Faster Solutions of Rabin and Streett Games

Abstract

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 <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">k+1</sup> 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. 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 <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">k+1</sup> k!) and space O(n <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">k+1</sup> k!). These results improve on the current bounds of O(mn <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">2k</sup> k!) time in the case of direct (symbolic) solution or O(m(nk <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">2</sup> k!) <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">k</sup> ) in the case of reduction to parity games