Strategy Synthesis for Markov Decision Processes and Branching-Time Logics

BRÁZDIL, Tomáš a Vojtěch FOREJT. Strategy Synthesis for Markov Decision Processes and Branching-Time Logics. Luís Caires, Vasco Thudichum Vasconcelos (Eds.). In Proceedings of 18th International Conference on Concurrency Theory (CONCUR 2007). Berlin Heidelberg New York: Springer, 2007, s. 428-444. ISBN 978-3-540-74406-1.

Základní údaje

Originální název

Strategy Synthesis for Markov Decision Processes and Branching-Time Logics

Název česky

Syntéza strategií pro Markovovy rozhodovací procesy a logiky větvícího času

Autoři

BRÁZDIL, Tomáš a Vojtěch FOREJT
Luís Caires, Vasco Thudichum Vasconcelos (Eds.).

Vydání

Berlin Heidelberg New York, Proceedings of 18th International Conference on Concurrency Theory (CONCUR 2007), od s. 428-444, 17 s. 2007

Nakladatel

Springer

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/07:00022548

Organizační jednotka

Fakulta informatiky

ISBN

978-3-540-74406-1

UT WoS

000251195900029

Klíčová slova anglicky

Markov decision processes; branching-time logics

Štítky

branching-time logics, Markov decision processes

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

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.

Česky

Předmětem zkoumání jsou konečné hry jednoho a půl hráče (Markovovy rozhodovací procesy), ve kterých je vítězná podmínka zadána pomocí formule logiky větvícího času qPECTL*, což je rozšíření kvalitativní PCTL*. Zkoumáme rozhodnutelnost a složitost problému existence vítězné strategie v těchto hrách. Popíšeme fragment detPECTL*, pro který je tento problém rozhodnutelný v exponenciálním čase a také ukážeme, že vítěznou strategii lze nalézt v exponenciálním čase, pokud tato existuje. Navíc ukážeme, že každou formuli qPECTL* lze převést na formuli detPECTL*, která je ekvivalentní na všech konečných Markovových řetězcích. Tím dostaneme rozhodnutelnost problému existence konečněpaměťové strategie pro qPECTL*. Přímým důsledkem je rozhodnutelnost problému existence konečněpaměťové strategie pro qPCTL*. Také ukážeme, že pro qPCTL je stejný problém řešitelný v exponenciálním čase. V závěru článku se zabýváme vyjadřovací silou konečně pamětových strategií vzhledem k formulím logiky qPCTL.

---

Návaznosti

1M0545, projekt VaV

Název: Institut Teoretické Informatiky Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky