Publication details
Stochastic Games with Branching-Time Winning Objectives
Authors | |
---|---|
Year of publication | 2006 |
Type | Article in Proceedings |
Conference | 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, Washington, USA, Proceedings |
MU Faculty or unit | |
Citation | |
Field | Informatics |
Keywords | Stochastic games; branching-time temporal logics |
Description | 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. |
Related projects: |