Oxford logo
[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]
Downloads:  pdf pdf (192 KB)  bib 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.