# Scalable Verification of Markov Decision Processes

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 14 Oct 2013.

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

- [What Are the Odds? Improving the foundations of Statistical Model Checking](https://mlsanity.com/paper/2404.05424/) (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 concurrent process optimisation problems, but verifying them with numerical methods is often intractable. Existing approximative approaches do not scale well and are limited to memoryless schedulers. Here we present the basis of scalable verification for MDPSs, using an O(1) memory representation of history-dependent schedulers. We thus facilitate scalable learning techniques and the use of massively parallel verification.