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 1frac12-player games is highly undecidable, even for objectives formulated in the Lscr(F^=5/8 ,F⁼¹,F^>0,G⁼¹) fragment of PCTL. On the other hand, we show that the problem becomes decidable (and in fact EXPTIME-complete) for the Lscr(F⁼¹,F^>0,G⁼¹) fragment of PCTL, where winning strategies require only finite memory. This result is tight in the sense that winning strategies for Lscr(F⁼¹,F^>0,G⁼¹,G^>0 ) objectives may already require infinite memory