# Scenario-Based Verification of Uncertain Parametric MDPs

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

## Key facts

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

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

- [Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet](https://mlsanity.com/paper/2411.11451/) (2024)
- [Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions](https://mlsanity.com/paper/2301.01526/) (2023)
- [Decision-Making Under Uncertainty: Beyond Probabilities](https://mlsanity.com/paper/2303.05848/) (2023)
- [Certifiably Robust Policies for Uncertain Parametric Environments](https://mlsanity.com/paper/2408.03093/) (2024)
- [Efficient Sensitivity Analysis for Parametric Robust Markov Chains](https://mlsanity.com/paper/2305.01473/) (2023)
- [Efficient Solution and Learning of Robust Factored MDPs](https://mlsanity.com/paper/2508.00707/) (2025)
- [VeRecycle: Reclaiming Guarantees from Probabilistic Certificates for Stochastic Dynamical Systems after Change](https://mlsanity.com/paper/2505.14001/) (2025)
- [PAC Approximation and DIRECT Optimization for Parametric Markov Models](https://mlsanity.com/paper/2608.02184/) (2026)

## Abstract (arXiv)

We consider parametric Markov decision processes (pMDPs) that are augmented with unknown probability distributions over parameter values. The problem is to compute the probability to satisfy a temporal logic specification with any concrete MDP that corresponds to a sample from these distributions. As solving this problem precisely is infeasible, we resort to sampling techniques that exploit the so-called scenario approach. Based on a finite number of samples of the parameters, the proposed method yields high-confidence bounds on the probability of satisfying the specification. The number of samples required to obtain a high confidence on these bounds is independent of the number of states and the number of random parameters. Experiments on a large set of benchmarks show that several thousand samples suffice to obtain tight and high-confidence lower and upper bounds on the satisfaction probability.