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: |