Strategy Synthesis for Markov Decision Processes and Branching-Time Logics

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áš FOREJT Vojtěch

Year of publication 2007
Type Article in Proceedings
Conference Proceedings of 18th International Conference on Concurrency Theory (CONCUR 2007)
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords Markov decision processes; branching-time logics
Description We consider a class of finite 1.5-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 exponential 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.
Related projects:

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