. "10"^^ . . "Ku\u010Dera, Anton\u00EDn" . "4"^^ . . "14330" . "4"^^ . . . "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.5-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."@en . "21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, Washington, USA, Proceedings" . "Bro\u017Eek, V\u00E1clav" . "RIV/00216224:14330/06:00017108" . . . "Br\u00E1zdil, Tom\u00E1\u0161" . . . "2006-08-12+02:00"^^ . "Stochastic games; branching-time temporal logics"@en . . . "501652" . . . . "RIV/00216224:14330/06:00017108!RIV10-MSM-14330___" . . "P(1M0545), Z(MSM0021622419)" . "0-7695-2631-4" . . "Los Alamitos, California" . "Forejt, Vojt\u011Bch" . "Stochastic Games with Branching-Time Winning Objectives" . "Stochastic Games with Branching-Time Winning Objectives"@en . . . "IEEE Computer Society" . "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.5-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." . "Stochastic Games with Branching-Time Winning Objectives"@en . . "Stochastic Games with Branching-Time Winning Objectives" . "Seattle, Washington, USA" . "[FDD58DF532FB]" . .