Stochastic Games with Branching-Time Winning Objectives

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BRÁZDIL Tomáš BROŽEK Václav FOREJT Vojtěch KUČERA Antonín

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

Faculty of Informatics

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:

You are running an old browser version. We recommend updating your browser to its latest version.