Detailed Information on Publication Record
2008
Reachability in Recursive Markov Decision Processes
BRÁZDIL, Tomáš, Václav BROŽEK, Vojtěch FOREJT and Antonín KUČERABasic information
Original name
Reachability in Recursive Markov Decision Processes
Name in Czech
Dosažitelnost v rekurzivních Markovových rozhodovacích procesech
Authors
BRÁZDIL, Tomáš (203 Czech Republic), Václav BROŽEK (203 Czech Republic), Vojtěch FOREJT (203 Czech Republic) and Antonín KUČERA (203 Czech Republic, guarantor)
Edition
Information and Computation, Elsevier, 2008, 0890-5401
Other information
Language
English
Type of outcome
Článek v odborném periodiku
Field of Study
10201 Computer sciences, information science, bioinformatics
Country of publisher
United States of America
Confidentiality degree
není předmětem státního či obchodního tajemství
Impact factor
Impact factor: 1.504
RIV identification code
RIV/00216224:14330/08:00024683
Organization unit
Faculty of Informatics
UT WoS
000256002800003
Keywords in English
Markov decision processes; temporal logics; reachability
Tags
International impact, Reviewed
Změněno: 22/5/2009 15:14, prof. RNDr. Antonín Kučera, Ph.D.
V originále
We consider a class of infinite-state Markov decision processes generated by stateless pushdown automata. This class corresponds to 1.5-player games over graphs generated by BPA systems or (equivalently) 1-exit recursive state machines. An extended reachability objective is specified by two sets S and T of safe and terminal stack configurations, where the membership to S and T depends just on the top-of-the-stack symbol. The question is whether there is a suitable strategy such that the probability of hitting a terminal configuration by a path leading only through safe configurations is equal to (or different from) a given x in {0,1}. We show that the qualitative extended reachability problem is decidable in polynomial time, and that the set of all configurations for which there is a winning strategy is effectively regular. More precisely, this set can be represented by a deterministic finite-state automaton with a fixed number of control states. This result is a generalization of a recent theorem by Etessami & Yannakakis which says that the qualitative termination for 1-exit RMDPs (which exactly correspond to our 1.5-player BPA games) is decidable in polynomial time. Interestingly, the properties of winning strategies for the extended reachability objectives are quite different from the ones for termination, and new observations are needed to obtain the result. As an application, we derive the EXPTIME-completeness of the model-checking problem for 1.5-player BPA games and qualitative PCTL formulae.
In Czech
V článku se zkoumá třída nekonečně-stavových Markovových rozhodovacích procesů generovaná zásobníkovými automaty bez stavové jednotky. Tato třída odpovídá hrám s 1.5 hráči nad grafy generovanými BPA systémy nebo (ekvivalentně) rekuzivními stavovými automaty s jedním exitem. Rozšířený problém dosažitelnosti je dán dvěma množinami S a T bezpečných a koncových stavů, kde příslušnost do S a T závisí pouza na symbolu na vrcholu zásobníku. V článku se zkoumá algortimická rozhodnutelnost a složitost otázky existence vhodné strategie, která zajistí, že pravděpodobnost dosažení koncového stavu přes bezpečné stavy je rovna danému x z množiny {0,1}. Je ukázáno, že tato otázka je algoritmicky rozhodnutelná v polynomiálním čase, a že množina všech konfigurací, pro které vhodná strategie existuje, je efektivně regulární.
Links
| GD102/05/H050, research and development project |
| ||
| MSM0021622419, plan (intention) |
| ||
| 1M0545, research and development project |
|