Qualitative Determinacy and Decidability of Stochastic Games with Signals

We consider the standard model of finite two person zero sum stochastic games with signals. We are interested in the existence of almost surely winning or positively winning strategies, under reachability, safety, Buchi or co-Buchi winning objectives. We prove two qualitative determinacy results. First, in a reachability game either player 1 can achieve almost-surely the reachability objective, or player 2 can ensure surely the complementary safety objective, or both players have positively winning strategies. Second, in a Buchi game if player 1 cannot achieve almost-surely the Buchi objective, then player 2 can ensure positively the complementary co-Buchi objective. We prove that players only need strategies with finite memory, whose sizes range from no memory at all to doubly-exponential number of states, with matching lower bounds. Together with the qualitative determinacy results, we also provide fix point algorithms for deciding which player has an almost surely winning or a positively winning strategy and for computing the finite memory strategy. Complexity ranges from EXPTIME to 2-EXPTIME with matching lower bounds, and better complexity can be achieved for some special cases where one of the players is better informed than her opponent.