A practitioner's guide to MDP model checking algorithms
From MaRDI portal
Publication:6535370
DOI10.1007/978-3-031-30823-9_24zbMATH Open1543.68212MaRDI QIDQ6535370
Sebastian Junges, Tim Quatmann, Maximilian Weininger, Arnd Hartmanns
Publication date: 13 December 2023
Markov and semi-Markov decision processes (90C40) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Runtime monitors for Markov decision processes
- Performance analysis of probabilistic timed automata using digital clocks
- Parallelizing the dual revised simplex method
- On the article by F. L. Chernous'ko 'Optimization of control and observation processes in dynamic systems under random perturbations'
- The 10,000 facets of MDP model checking
- Comparison of algorithms for simple stochastic games
- Ensuring the reliability of your model checker: interval iteration for Markov decision processes
- Exact quantitative probabilistic model checking through rational search
- Widest paths and global propagation in bounded value iteration for stochastic games
- Optimistic value iteration
- Optimal schedulers vs optimal bases: an approach for efficient exact solving of Markov decision processes
- Interval iteration algorithm for MDPs and IMDPs
- Value iteration for simple stochastic games: stopping criterion and learning algorithm
- Iterative refinement for linear programming
- The Simplex and Policy-Iteration Methods Are Strongly Polynomial for the Markov Decision Problem with a Fixed Discount Rate
- Model Checking Probabilistic Systems
- Sequential Convex Programming for the Efficient Verification of Parametric MDPs
- Reachability in MDPs: Refining Convergence of Value Iteration
- Verification of Markov Decision Processes Using Learning Algorithms
- Value Iteration
- Exponential Lower Bounds for Policy Iteration
- GMRES: A Generalized Minimal Residual Algorithm for Solving Nonsymmetric Linear Systems
- An Analysis of Stochastic Shortest Path Problems
- Pareto Curves for Probabilistic Model Checking
- Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints
- On the Complexity of Value Iteration
- Improving the accuracy of linear programming solvers with iterative refinement
- High-level Counterexamples for Probabilistic Automata
- Sound value iteration
- Optimistic and topological value iteration for simple stochastic games
- Correct probabilistic model checking with floating-point arithmetic
Related Items (1)
This page was built for publication: A practitioner's guide to MDP model checking algorithms
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6535370)
