"Strategy Synthesis for Markov Decision Processes and Branching-Time Logics" . "[81E0468E9F64]" . "14330" . "Strategy Synthesis for Markov Decision Processes and Branching-Time Logics"@en . "452658" . . "RIV/00216224:14330/07:00025651" . "Br\u00E1zdil, Tom\u00E1\u0161" . "RIV/00216224:14330/07:00025651!RIV10-MSM-14330___" . "2"^^ . "Forejt, Vojt\u011Bch" . "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 . "Markov decision processes; branching-time logics"@en . "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." . . . "Strategy Synthesis for Markov Decision Processes and Branching-Time Logics" . "Strategy Synthesis for Markov Decision Processes and Branching-Time Logics"@en . . . . "P(1M0545)" . . . "2"^^ . . . . . . . .