"Springer-Verlag" . "14330" . "452659" . "[5D27CC9F5079]" . "Strategy Synthesis for Markov Decision Processes and Branching-Time Logics"@en . "Br\u00E1zdil, Tom\u00E1\u0161" . "Proceedings of 18th International Conference on Concurrency Theory (CONCUR 2007)" . . . "Strategy Synthesis for Markov Decision Processes and Branching-Time Logics" . "978-3-540-74406-1" . "Lisabon" . . . "P(1M0545)" . . "17"^^ . . "2007-01-01+01:00"^^ . . . "2"^^ . "Strategy Synthesis for Markov Decision Processes and Branching-Time Logics"@en . . "RIV/00216224:14330/07:00022548!RIV10-MSM-14330___" . "2"^^ . "Markov decision processes; branching-time logics"@en . "Strategy Synthesis for Markov Decision Processes and Branching-Time Logics" . . "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." . "Berlin Heidelberg New York" . . "Forejt, Vojt\u011Bch" . . . "RIV/00216224:14330/07:00022548" . "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."@en . . . .