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
(47)- Verification of general Markov decision processes by approximate similarity relations and policy refinement
- Deep reinforcement learning with temporal logics
- Probabilistic guarantees for safe deep reinforcement learning
- Probabilistic black-box reachability checking (extended version)
- Automated verification and synthesis of stochastic hybrid systems: a survey
- Comparison of algorithms for simple stochastic games
- Automatic verification of concurrent stochastic systems
- Multi-cost bounded tradeoff analysis in MDP
- Exact quantitative probabilistic model checking through rational search
- Global PAC bounds for learning discrete time Markov chains
- Interval iteration algorithm for MDPs and IMDPs
- Value iteration for simple stochastic games: stopping criterion and learning algorithm
- Statistical approximation of optimal schedulers for probabilistic timed automata
- Polynomial-time verification of PCTL properties of MDPs with convex uncertainties
- Model checking probabilistic systems
- Reachability in MDPs: refining convergence of value iteration
- Marimba: a tool for verifying properties of hidden Markov models
- Learning-based mean-payoff optimization in an unknown MDP under omega-regular constraints
- Comparison of algorithms for simple stochastic games
- Task-aware verifiable RNN-based policies for partially observable Markov decision processes
- Scenario-based verification of uncertain MDPs
- Good-for-MDPs automata for probabilistic analysis and reinforcement learning
- Farkas certificates and minimal witnesses for probabilistic reachability constraints
- scientific article; zbMATH DE number 7559459 (Why is no real title available?)
- scientific article; zbMATH DE number 7559496 (Why is no real title available?)
- Of cores: a partial-exploration framework for Markov decision processes
- Verification of general Markov decision processes by approximate similarity relations and policy refinement
- Of cores: a partial-exploration framework for Markov decision processes
- Model Checking for Safe Navigation Among Humans
- Certified reinforcement learning with logic guidance
- Optimistic and topological value iteration for simple stochastic games
- Verification of Indefinite-Horizon POMDPs
- Abstraction-Refinement for Hierarchical Probabilistic Models
- PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP
- Bayes-Adaptive Planning for Data-Efficient Verification of Uncertain Markov Decision Processes
- A practitioner's guide to MDP model checking algorithms
- Correct approximation of stationary distributions
- Robust almost-sure reachability in multi-environment MDPs
- Under-approximating expected total rewards in POMDPs
- Correct probabilistic model checking with floating-point arithmetic
- Entropic risk for turn-based stochastic games
- PAC statistical model checking of mean payoff in discrete- and continuous-time MDP
- Efficient constraint generation for stochastic shortest path problems
- Average reward reinforcement learning for omega-regular and mean-payoff objectives
- On piecewise affine reachability with Bellman operators
- Safe learning for near-optimal scheduling
- Model checking finite-horizon Markov chains with probabilistic inference
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)
