Reachability in recursive Markov decision processes

DOI10.1016/j.ic.2007.09.002zbMath1145.91011OpenAlexW2101561362MaRDI QIDQ924718

Vojtěch Forejt, Tomáš Brázdil, Antonín Kučera, Václav Brožek

Publication date: 19 May 2008

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2007.09.002

zbMATH Keywords

Markov decision processesStochastic gamesTemporal logics

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Stochastic games, stochastic differential games (91A15)

Related Items (11)

Hyperplane separation technique for multidimensional mean-payoff games ⋮ Polynomial Time Algorithms for Branching Markov Decision Processes and Probabilistic Min(Max) Polynomial Bellman Equations ⋮ Greatest fixed points of probabilistic min/max polynomial equations, and reachability for branching Markov decision processes ⋮ Determinacy and optimal strategies in infinite-state stochastic reachability games ⋮ Branching-time model-checking of probabilistic pushdown automata ⋮ Recursive stochastic games with positive rewards ⋮ Bounded Verification of Reachability of Probabilistic Hybrid Systems ⋮ Analyzing probabilistic pushdown automata ⋮ Regularity in PDA Games Revisited ⋮ Qualitative reachability in stochastic BPA games ⋮ Unnamed Item

Uses Software

• PRISM

Cites Work

• Unnamed Item
• Unnamed Item
• Optimal control of diffusion processes with reflection
• A logic for reasoning about time and reliability
• Pushdown processes: Games and model-checking
• Model checking LTL with regular valuations for pushdown systems
• Model checking of probabilistic and nondeterministic systems
• Efficient Qualitative Analysis of Classes of Recursive Markov Decision Processes and Simple Stochastic Games
• STACS 2005
• Automata, Languages and Programming
• Handbook of Markov decision processes. Methods and applications
• Reachability analysis of pushdown automata: Application to model-checking

This page was built for publication: Reachability in recursive Markov decision processes