Reachability in recursive Markov decision processes
type: Item
instance of: scholarly article
title: Reachability in recursive Markov decision processes
zbMATH Open document ID: 1145.91011
author: Tomáš Brázdil
author: Václav Brožek
author: Vojtech Forejt
author: Antonin Kučera
published in: Information and Computation
publication date: 2008-05-19T00:00:00Z
review text: A class of infinite-state Markov decision processes generated by stateless pushdown automata is considered. This class corresponds to 1 1/2-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)\). It is shown 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 and Yannakakis which says that the qualitative termination for 1-exit RMDPs (which exactly correspond to our 1 1/2-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, the EXPTIME-completeness of the model-checking problem is obtained for 1 1/2-player BPA games and qualitative PCTL formulae.
reviewed by: Giacomo Bonanno
Mathematics Subject Classification ID: 91A15
Mathematics Subject Classification ID: 68Q45
zbMATH DE Number: 5276410
zbMATH Keywords: Markov decision processes
zbMATH Keywords: Temporal logics
zbMATH Keywords: Stochastic games
describes a project that uses: PRISM
MaRDI profile type: Publication
full work available at URL: j.ic.2007.09.002
OpenAlex ID: W2101561362
cites work: Q5137353
cites work: Model checking of probabilistic and nondeterministic systems
cites work: Reachability analysis of pushdown automata: Application to model-checking
cites work: STACS 2005
cites work: Model checking LTL with regular valuations for pushdown systems
cites work: Automata, Languages and Programming
cites work: Efficient Qualitative Analysis of Classes of Recursive Markov Decision Processes and Simple Stochastic Games
cites work: Handbook of Markov decision processes. Methods and applications
cites work: Q5538132
cites work: A logic for reasoning about time and reliability
cites work: Optimal control of diffusion processes with reflection
cites work: Pushdown processes: Games and model-checking
DOI: 10.1016/J.IC.2007.09.002
description: scientific article; zbMATH DE number 5276410