Verification of Markov decision processes using learning algorithms
From MaRDI portal
Abstract: We present a general framework for applying machine-learning algorithms to the verification of Markov decision processes (MDPs). The primary goal of these techniques is to improve performance by avoiding an exhaustive exploration of the state space. Our framework focuses on probabilistic reachability, which is a core property for verification, and is illustrated through two distinct instantiations. The first assumes that full knowledge of the MDP is available, and performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP, and yields probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. The latter is the first extension of statistical model-checking for unbounded properties in MDPs. In contrast with other related approaches, we do not restrict our attention to time-bounded (finite-horizon) or discounted properties, nor assume any particular properties of the MDP. We also show how our techniques extend to LTL objectives. We present experimental results showing the performance of our framework on several examples.
Recommendations
- Scenario-based verification of uncertain MDPs
- A game-based abstraction-refinement framework for Markov decision processes
- Polynomial-time verification of PCTL properties of MDPs with convex uncertainties
- Learning deterministic probabilistic automata from a model checking perspective
- \(L^\ast\)-based learning of Markov decision processes (extended version)
Cited in
(45)- Of cores: a partial-exploration framework for Markov decision processes
- Comparison of algorithms for simple stochastic games
- Model checking finite-horizon Markov chains with probabilistic inference
- Safe learning for near-optimal scheduling
- Comparison of algorithms for simple stochastic games
- Probabilistic guarantees for safe deep reinforcement learning
- Global PAC bounds for learning discrete time Markov chains
- Verification of Indefinite-Horizon POMDPs
- Robust almost-sure reachability in multi-environment MDPs
- Reachability in MDPs: refining convergence of value iteration
- Optimistic and topological value iteration for simple stochastic games
- Statistical approximation of optimal schedulers for probabilistic timed automata
- Model checking probabilistic systems
- Model Checking for Safe Navigation Among Humans
- Deep reinforcement learning with temporal logics
- Learning-based mean-payoff optimization in an unknown MDP under omega-regular constraints
- Scenario-based verification of uncertain MDPs
- Farkas certificates and minimal witnesses for probabilistic reachability constraints
- Good-for-MDPs automata for probabilistic analysis and reinforcement learning
- Automatic verification of concurrent stochastic systems
- Automated verification and synthesis of stochastic hybrid systems: a survey
- Efficient constraint generation for stochastic shortest path problems
- Interval iteration algorithm for MDPs and IMDPs
- Of cores: a partial-exploration framework for Markov decision processes
- Multi-cost bounded tradeoff analysis in MDP
- Abstraction-Refinement for Hierarchical Probabilistic Models
- Polynomial-time verification of PCTL properties of MDPs with convex uncertainties
- Verification of general Markov decision processes by approximate similarity relations and policy refinement
- PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP
- Value iteration for simple stochastic games: stopping criterion and learning algorithm
- Bayes-Adaptive Planning for Data-Efficient Verification of Uncertain Markov Decision Processes
- Entropic risk for turn-based stochastic games
- Exact quantitative probabilistic model checking through rational search
- Verification of general Markov decision processes by approximate similarity relations and policy refinement
- A practitioner's guide to MDP model checking algorithms
- Correct approximation of stationary distributions
- Correct probabilistic model checking with floating-point arithmetic
- Under-approximating expected total rewards in POMDPs
- Marimba: a tool for verifying properties of hidden Markov models
- Certified reinforcement learning with logic guidance
- scientific article; zbMATH DE number 7559459 (Why is no real title available?)
- scientific article; zbMATH DE number 7559496 (Why is no real title available?)
- PAC statistical model checking of mean payoff in discrete- and continuous-time MDP
- Task-aware verifiable RNN-based policies for partially observable Markov decision processes
- Probabilistic black-box reachability checking (extended version)
This page was built for publication: Verification of Markov decision processes using learning algorithms
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3457782)
