Stochastic games with branching-time winning objectives

We consider stochastic turn-based games where the winning objectives are given by formulae of the branching-time logic PCTL. These games are generally not determined and winning strategies may require memory and/or randomization. Our main results concern history-dependent strategies. In particular, we show that the problem whether there exists a history-dependent winning strategy in 1 1/2 -player games is highly undecidable, even for objectives formulated in the L(F-=5/8, F-=1,F-> 0,G(=1)) fragment of PCTL. On the other hand, we show that the problem becomes decidable (and in fact EXPTIME-complete) for the L(F-=1, F-> 0, G(=1)) fragment of PCTL, where winning strategies require only finite memory. This result is tight in the sense that winning strategies for L(F-=1, F-> 0, G(=1), G(> 0)) objectives may already require infinite memory.