Reachability in recursive Markov decision processes
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.
- A logic for reasoning about time and reliability
- Automata, Languages and Programming
- Efficient Qualitative Analysis of Classes of Recursive Markov Decision Processes and Simple Stochastic Games
- Handbook of Markov decision processes. Methods and applications
- scientific article; zbMATH DE number 7280017 (Why is no real title available?)
- scientific article; zbMATH DE number 3249395 (Why is no real title available?)
- Model checking LTL with regular valuations for pushdown systems
- Model checking of probabilistic and nondeterministic systems
- Optimal control of diffusion processes with reflection
- Pushdown processes: Games and model-checking
- Reachability analysis of pushdown automata: Application to model-checking
- STACS 2005
- The complexity of graph-based reductions for reachability in Markov decision processes
- Reachability and safety objectives in Markov decision processes on long but finite horizons
- Analyzing probabilistic pushdown automata
- Hyperplane separation technique for multidimensional mean-payoff games
- Reachability analysis of uncertain systems using bounded-parameter Markov decision processes
- Recursive stochastic games with positive rewards
- Qualitative analysis of VASS-induced MDPs
- Nested Reachability Approximation for Discrete-Time Markov Chains with Univariate Parameters
- Strategy Synthesis for Markov Decision Processes and Branching-Time Logics
- Forward Recursion for Markov Decision Processes with Skip-Free-to-the-Right Transitions, Part I: Theory and Algorithm
- Determinacy and optimal strategies in infinite-state stochastic reachability games
- Branching-time model-checking of probabilistic pushdown automata
- scientific article; zbMATH DE number 1786649 (Why is no real title available?)
- Reachability problems for Markov chains
- scientific article; zbMATH DE number 7561608 (Why is no real title available?)
- Polynomial time algorithms for branching Markov decision processes and probabilistic min(max) polynomial Bellman equations
- Expected termination time in BPA games
- Regularity in PDA games revisited
- Qualitative reachability in stochastic BPA games
- Reachability in Recursive Markov Decision Processes
- Bounded Verification of Reachability of Probabilistic Hybrid Systems
- Qualitative reachability in stochastic BPA games
- Enforcing almost-sure reachability in POMDPs
This page was built for publication: Reachability in recursive Markov decision processes
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q924718)
