# Scenario-Based Verification of Uncertain MDPs

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 24 Dec 2019.

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

- [Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet](https://mlsanity.com/paper/2411.11451/) (2024)
- [Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise](https://mlsanity.com/paper/2110.12662/) (2021)
- [Distributionally Robust Statistical Verification with Imprecise Neural Networks](https://mlsanity.com/paper/2308.14815/) (2023)
- [Convex Optimization for Parameter Synthesis in MDPs](https://mlsanity.com/paper/2107.00108/) (2021)
- [Multi-Objective Controller Synthesis with Uncertain Human Preferences](https://mlsanity.com/paper/2105.04662/) (2021)
- [Data-driven Abstractions with Probabilistic Guarantees for Linear PETC Systems](https://mlsanity.com/paper/2203.05522/) (2022)

## Abstract (arXiv)

We consider Markov decision processes (MDPs) in which the transition probabilities and rewards belong to an uncertainty set parametrized by a collection of random variables. The probability distributions for these random parameters are unknown. The problem is to compute the probability to satisfy a temporal logic specification within any MDP that corresponds to a sample from these unknown distributions. In general, this problem is undecidable, and we resort to techniques from so-called scenario optimization. Based on a finite number of samples of the uncertain parameters, each of which induces an MDP, the proposed method estimates the probability of satisfying the specification by solving a finite-dimensional convex optimization problem. The number of samples required to obtain a high confidence on this estimate is independent from the number of states and the number of random parameters. Experiments on a large set of benchmarks show that a few thousand samples suffice to obtain high-quality confidence bounds with a high probability.