# Smart Sampling for Lightweight Verification of Markov Decision Processes

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 7 Sep 2014.

## Built on by (most cited first, 3 of 3)

- [What Are the Odds? Improving the foundations of Statistical Model Checking](https://mlsanity.com/paper/2404.05424/) (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)
- [Probabilistic Black-Box Checking via Active MDP Learning](https://mlsanity.com/paper/2308.07930/) (2023)

## Abstract (arXiv)

Markov decision processes (MDP) are useful to model optimisation problems in concurrent systems. To verify MDPs with efficient Monte Carlo techniques requires that their nondeterminism be resolved by a scheduler. Recent work has introduced the elements of lightweight techniques to sample directly from scheduler space, but finding optimal schedulers by simple sampling may be inefficient. Here we describe "smart" sampling algorithms that can make substantial improvements in performance.