Technical Reports
The report FIMU-RS-2006-02
Stochastic Games with Branching-Time Winning Objectives
by
Tomáš Brázdil,
Václav Brožek,
Vojtěch Forejt,
Antonín Kučera,
A full version of the paper presented at LICS 2006. September 2006, 37 pages.
FIMU-RS-2006-02.
Available as Postscript,
PDF.
Abstract:
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.
