Strategy Synthesis for Markov Decision Processes and Branching-Time Logics
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F07%3A00022548" target="_blank" >RIV/00216224:14330/07:00022548 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
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
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
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)
Others
Publication year
2007
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Proceedings of 18th International Conference on Concurrency Theory (CONCUR 2007)
ISBN
978-3-540-74406-1
ISSN
—
e-ISSN
—
Number of pages
17
Pages from-to
—
Publisher name
Springer
Place of publication
Berlin Heidelberg New York
Event location
Lisabon
Event date
Jan 1, 2007
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—