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.

QAV:

Home

People

Projects

Publications