"RIV/00216224:14330/07:00022548" . . . "452660" . "Strategy Synthesis for Markov Decision Processes and Branching-Time Logics" . "P\u0159edm\u011Btem zkoum\u00E1n\u00ED jsou kone\u010Dn\u00E9 hry jednoho a p\u016Fl hr\u00E1\u010De (Markovovy rozhodovac\u00ED procesy), ve kter\u00FDch je v\u00EDt\u011Bzn\u00E1 podm\u00EDnka zad\u00E1na pomoc\u00ED formule logiky v\u011Btv\u00EDc\u00EDho \u010Dasu qPECTL*, co\u017E je roz\u0161\u00ED\u0159en\u00ED kvalitativn\u00ED PCTL*. Zkoum\u00E1me rozhodnutelnost a slo\u017Eitost probl\u00E9mu existence v\u00EDt\u011Bzn\u00E9 strategie v t\u011Bchto hr\u00E1ch. Pop\u00ED\u0161eme fragment detPECTL*, pro kter\u00FD je tento probl\u00E9m rozhodnuteln\u00FD v exponenci\u00E1ln\u00EDm \u010Dase a tak\u00E9 uk\u00E1\u017Eeme, \u017Ee v\u00EDt\u011Bznou strategii lze nal\u00E9zt v exponenci\u00E1ln\u00EDm \u010Dase, pokud tato existuje. Nav\u00EDc uk\u00E1\u017Eeme, \u017Ee ka\u017Edou formuli qPECTL* lze p\u0159ev\u00E9st na formuli detPECTL*, kter\u00E1 je ekvivalentn\u00ED na v\u0161ech kone\u010Dn\u00FDch Markovov\u00FDch \u0159et\u011Bzc\u00EDch. T\u00EDm dostaneme rozhodnutelnost probl\u00E9mu existence kone\u010Dn\u011Bpam\u011B\u0165ov\u00E9 strategie pro qPECTL*. P\u0159\u00EDm\u00FDm d\u016Fsledkem je rozhodnutelnost probl\u00E9mu existence kone\u010Dn\u011Bpam\u011B\u0165ov\u00E9 strategie pro qPCTL*. Tak\u00E9 uk\u00E1\u017Eeme, \u017Ee pro qPCTL je stejn\u00FD probl\u00E9m \u0159e\u0161iteln\u00FD v exponenci\u00E1ln\u00EDm \u010Dase. V z\u00E1v\u011Bru \u010Dl\u00E1nku se zab\u00FDv\u00E1me vyjad\u0159ovac\u00ED silou kone\u010Dn\u011B pam\u011Btov\u00FDch strategi\u00ED vzhledem k formul\u00EDm logiky qPCTL."@cs . "428-444" . "14330" . "Strategy Synthesis for Markov Decision Processes and Branching-Time Logics"@en . . . "Br\u00E1zdil, Tom\u00E1\u0161" . . . "0302-9743" . "DE - Spolkov\u00E1 republika N\u011Bmecko" . . "[6F54E2F01403]" . "Synt\u00E9za strategi\u00ED pro Markovovy rozhodovac\u00ED procesy a logiky v\u011Btv\u00EDc\u00EDho \u010Dasu"@cs . "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"@en . "Summer" . "P(1M0545)" . "RIV/00216224:14330/07:00022548!RIV08-MSM-14330___" . "17"^^ . . "2"^^ . . "2"^^ . . "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" . "Strategy Synthesis for Markov Decision Processes and Branching-Time Logics"@en . . . "Forejt, Vojt\u011Bch" . "Markov decision processes; branching-time logics"@en . . "Lecture Notes in Computer Science" . "4703" . . "Synt\u00E9za strategi\u00ED pro Markovovy rozhodovac\u00ED procesy a logiky v\u011Btv\u00EDc\u00EDho \u010Dasu"@cs . "Strategy Synthesis for Markov Decision Processes and Branching-Time Logics" . .