Reachability in recursive Markov decision processes

DOI10.1016/j.ic.2007.09.002zbMath1145.91011MaRDI 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 processes; Stochastic games; Temporal logics

Mathematics Subject Classification ID

68Q45: Formal languages and automata

91A15: Stochastic games, stochastic differential games

Related Items

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

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