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 | |
| Rok publikování | 2007 |
| Druh | Článek ve sborníku |
| Konference | Proceedings of 18th International Conference on Concurrency Theory (CONCUR 2007) |
| Fakulta / Pracoviště MU | |
| Citace | |
| Obor | Informatika |
| Klíčová slova | Markov decision processes; branching-time logics |
| Popis | 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. |
| Související projekty: |