Reachability in Recursive Markov Decision Processes

BRÁZDIL, Tomáš, Václav BROŽEK, Vojtěch FOREJT a Antonín KUČERA. Reachability in Recursive Markov Decision Processes. C. Baier, H. Hermanns (Eds.). In 17th International Conference on Concurrency Theory. Berlin Heidelberg New York: Springer, 2006, s. 358-374. ISBN 3-540-37376-4.

Základní údaje

Originální název

Reachability in Recursive Markov Decision Processes

Název česky

Dosažitelnost pro Markovovy rozhodovací procesy

Autoři

BRÁZDIL, Tomáš (203 Česká republika), Václav BROŽEK (203 Česká republika), Vojtěch FOREJT (203 Česká republika) a Antonín KUČERA (203 Česká republika, garant)
C. Baier, H. Hermanns (Eds.).

Vydání

Berlin Heidelberg New York, 17th International Conference on Concurrency Theory, od s. 358-374, 17 s. 2006

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í

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/06:00017081

Organizační jednotka

Fakulta informatiky

ISBN

3-540-37376-4

ISSN

UT WoS

000240256100024

Klíčová slova anglicky

Markov decision processes; reachability

Štítky

Markov decision processes, reachability

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

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.

Česky

V článku se zkoumají vlastnosti nekonečně-stavových Markovových rozhodovacích procesů, které jsou generované zásobníkovými procesy bez kontrolních stavů. Tato třída procesů odpovídá hrám s 1.5 hráči nad grafy, které jsou generované BPA systémy. Dokážeme, že kvalitativní problém dosažitelnosti je pro tuto třídu procesů rozhodnutelný v polynomiálním čase. Aplikaci tohoto výsledku prokážeme EXPTIME-úplnost problému platnosti dané kvalitativní PCTL formule v daném stavu daného procesu.

---

Návaznosti

MSM0021622419, záměr	Název: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1M0545, projekt VaV	Název: Institut Teoretické Informatiky Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky