Strategy Synthesis for Markov Decision Processes and Branching-Time Logics

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F07%3A00025651" target="_blank" >RIV/00216224:14330/07:00025651 - isvavai.cz</a>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Strategy Synthesis for Markov Decision Processes and Branching-Time Logics

Original language description

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 existenceof 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 expo

Czech name

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

Czech description

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.

Type

O - Miscellaneous

CEP classification

IN - Informatics

OECD FORD branch

—

Project

<a href="/en/project/1M0545" target="_blank" >1M0545: Institute for Theoretical Computer Science</a><br>

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year

2007

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů