# Verification of Markov Decision Processes using Learning Algorithms

arXiv: https://arxiv.org/abs/1402.2967 · HTML: https://mlsanity.com/paper/1402.2967/

## Key facts

- Cited by 39 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 10 Feb 2014.

## Built on by (most cited first, 30 of 39)

- [Multi-Agent Reinforcement Learning with Temporal Logic Specifications](https://mlsanity.com/paper/2102.00582/) (2021)
- [DeepLTL: Learning to Efficiently Satisfy Complex LTL Specifications for Multi-Task RL](https://mlsanity.com/paper/2410.04631/) (2024)
- [Policy Optimization with Linear Temporal Logic Constraints](https://mlsanity.com/paper/2206.09546/) (2022)
- [COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking](https://mlsanity.com/paper/2209.07133/) (2022)
- [On the (In)Tractability of Reinforcement Learning for LTL Objectives](https://mlsanity.com/paper/2111.12679/) (2021)
- [Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet](https://mlsanity.com/paper/2411.11451/) (2024)
- [Reinforcement Learning with LTL and ω-Regular Objectives via Optimality-Preserving Translation to Average Rewards](https://mlsanity.com/paper/2410.12175/) (2024)
- [A PAC Learning Algorithm for LTL and Omega-regular Objectives in MDPs](https://mlsanity.com/paper/2310.12248/) (2023)
- [Safety-Oriented Pruning and Interpretation of Reinforcement Learning Policies](https://mlsanity.com/paper/2409.10218/) (2024)
- [Abstraction-Refinement for Hierarchical Probabilistic Models](https://mlsanity.com/paper/2206.02653/) (2022)
- [Model-Free Learning of Safe yet Effective Controllers](https://mlsanity.com/paper/2103.14600/) (2021)
- [Under-Approximating Expected Total Rewards in POMDPs](https://mlsanity.com/paper/2201.08772/) (2022)
- [What Are the Odds? Improving the foundations of Statistical Model Checking](https://mlsanity.com/paper/2404.05424/) (2024)
- [Sample-Efficient Reinforcement Learning with Temporal Logic Objectives: Leveraging the Task Specification to Guide Exploration](https://mlsanity.com/paper/2410.12136/) (2024)
- [1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization](https://mlsanity.com/paper/2410.18293/) (2024)
- [PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP](https://mlsanity.com/paper/2206.01465/) (2022)
- [Playing Games with your PET: Extending the Partial Exploration Tool to Stochastic Games](https://mlsanity.com/paper/2405.03885/) (2024)
- [Learning Optimal Strategies for Temporal Tasks in Stochastic Games](https://mlsanity.com/paper/2102.04307/) (2021)
- [Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives](https://mlsanity.com/paper/2304.09930/) (2023)
- [Mission-driven Exploration for Accelerated Deep Reinforcement Learning with Temporal Logic Task Specifications](https://mlsanity.com/paper/2311.17059/) (2023)
- [On the Uniqueness of Solution for the Bellman Equation of LTL Objectives](https://mlsanity.com/paper/2404.05074/) (2024)
- [Dual-Objective Reinforcement Learning with Novel Hamilton-Jacobi-Bellman Formulations](https://mlsanity.com/paper/2506.16016/) (2025)
- [Reinforcement Learning Based Temporal Logic Control with Soft Constraints Using Limit-deterministic Generalized Buchi Automata](https://mlsanity.com/paper/2101.10284/) (2021)
- [Graph-Based Reductions for Parametric and Weighted MDPs](https://mlsanity.com/paper/2305.05739/) (2023)
- [Co-Activation Graph Analysis of Safety-Verified and Explainable Deep Reinforcement Learning Policies](https://mlsanity.com/paper/2501.03142/) (2025)
- [Semantically Labelled Automata for Multi-Task Reinforcement Learning with LTL Instructions](https://mlsanity.com/paper/2602.06746/) (2026)
- [Strategy Synthesis in Markov Decision Processes Under Limited Sampling Access](https://mlsanity.com/paper/2303.12718/) (2023)
- [Probabilistic Black-Box Checking via Active MDP Learning](https://mlsanity.com/paper/2308.07930/) (2023)
- [Accelerated Learning with Linear Temporal Logic using Differentiable Simulation](https://mlsanity.com/paper/2506.01167/) (2025)
- [Mini-Batch Robustness Verification of Deep Neural Networks](https://mlsanity.com/paper/2508.15454/) (2025)

## Abstract (arXiv)

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.