# Parameter Synthesis for Markov Models: Covering the Parameter Space

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

## Key facts

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

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

- [Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet](https://mlsanity.com/paper/2411.11451/) (2024)
- [Convex Optimization for Parameter Synthesis in MDPs](https://mlsanity.com/paper/2107.00108/) (2021)
- [Verifiable Reinforcement Learning Systems via Compositionality](https://mlsanity.com/paper/2309.06420/) (2023)
- [What should be observed for optimal reward in POMDPs?](https://mlsanity.com/paper/2405.10768/) (2024)
- [Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation](https://mlsanity.com/paper/2511.06341/) (2025)
- [Formal Verification of Markov Processes with Learned Parameters](https://mlsanity.com/paper/2501.15767/) (2025)
- [Best-Effort Policies for Robust Markov Decision Processes](https://mlsanity.com/paper/2508.07790/) (2025)
- [Robust Parameter Learning for Uncertain MDPs](https://mlsanity.com/paper/2605.01339/) (2026)
- [Adversarial Robustness Verification and Attack Synthesis in Stochastic Systems](https://mlsanity.com/paper/2110.02125/) (2021)
- [A Multifidelity Sim-to-Real Pipeline for Verifiable and Compositional Reinforcement Learning](https://mlsanity.com/paper/2312.01249/) (2023)
- [Robustness Analysis of POMDP Policies to Observation Perturbations](https://mlsanity.com/paper/2604.21256/) (2026)
- [Tensor Probabilistic Model Checking of Finite-Horizon Markov Chains (Extended Version)](https://mlsanity.com/paper/2608.00374/) (2026)
- [Supermartingale Certificates for Parametric MDPs](https://mlsanity.com/paper/2609.12715/) (2026)
- [Bellman-Certified Rounding for Sparse Policy Deployment in MDPs](https://mlsanity.com/paper/2610.00325/) (2026)

## Abstract (arXiv)

Markov chain analysis is a key technique in formal verification. A practical obstacle is that all probabilities in Markov models need to be known. However, system quantities such as failure rates or packet loss ratios, etc. are often not -- or only partially -- known. This motivates considering parametric models with transitions labeled with functions over parameters. Whereas traditional Markov chain analysis relies on a single, fixed set of probabilities, analysing parametric Markov models focuses on synthesising parameter values that establish a given safety or performance specification varphi. Examples are: what component failure rates ensure the probability of a system breakdown to be below 0.00000001?, or which failure rates maximise the performance, for instance the throughput, of the system? This paper presents various analysis algorithms for parametric discrete-time Markov chains and Markov decision processes. We focus on three problems: (a) do all parameter values within a given region satisfy varphi?, (b) which regions satisfy varphi and which ones do not?, and (c) an approximate version of (b) focusing on covering a large fraction of all possible parameter values. We give a detailed account of the various algorithms, present a software tool realising these techniques, and report on an extensive experimental evaluation on benchmarks that span a wide range of applications.