[BF07]
T. Brázdil and V. Forejt.
Strategy Synthesis for Markov Decision Processes and Branching-Time Logics.
In L. Caires and V. T. Vasconcelos (editors), CONCUR 2007 - Concurrency Theory, 18th International Conference,, volume 4703 of Lecture Notes in Computer Science, pages 428-444, Springer.
2007.
[pdf]
[bib]
|
Notes:
The original publication is available at link.springer.com.
|
Abstract.
We consider a class of finite 1½-player games (Markov decision processes) where the winning objectives are specified in the branching-time temporal logic
qPECTL* (an extension of the qualitative PCTL∗). We study decidability and complexity of existence of a winning strategy in these games. We identify a fragment of
qPECTL∗ called detPECTL∗ for which the existence of a winning strategy is decidable in exponential time, and also the winning strategy can be computed in exponential
time (if it exists).
Consequently we show that every formula of qPECTL∗ can be translated to a formula of detPECTL∗ (in exponential time) so that the resulting formula is
equivalent to the original one over finite Markov chains. From this we obtain that for
the whole qPECTL∗, the existence of a winning finite-memory strategy is decidable in
double exponential time. An immediate consequence is that the existence of a winning
finite-memory strategy is decidable for the qualitative fragment of PCTL∗ in triple ex-
ponential time. We also obtain a single exponential upper bound on the same problem
for the qualitative PCTL.
Finally, we study the power of finite-memory strategies with
respect to objectives described in the qualitative PCTL.
|