# Parameter Synthesis for Markov Models: Faster Than Ever

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

## Key facts

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

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

- [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)
- [Abstraction-Refinement for Hierarchical Probabilistic Models](https://mlsanity.com/paper/2206.02653/) (2022)
- [Fine-Tuning the Odds in Bayesian Networks](https://mlsanity.com/paper/2105.14371/) (2021)
- [Inductive Synthesis for Probabilistic Programs Reaches New Horizons](https://mlsanity.com/paper/2101.12683/) (2021)
- [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)
- [Finding an ε-close Variation of Parameters in Bayesian Networks](https://mlsanity.com/paper/2305.10051/) (2023)
- [Robustness Analysis of POMDP Policies to Observation Perturbations](https://mlsanity.com/paper/2604.21256/) (2026)
- [PAC Approximation and DIRECT Optimization for Parametric Markov Models](https://mlsanity.com/paper/2608.02184/) (2026)
- [Supermartingale Certificates for Parametric MDPs](https://mlsanity.com/paper/2609.12715/) (2026)

## Abstract (arXiv)

We propose a simple technique for verifying probabilistic models whose transition probabilities are parametric. The key is to replace parametric transitions by nondeterministic choices of extremal values. Analysing the resulting parameter-free model using off-the-shelf means yields (refinable) lower and upper bounds on probabilities of regions in the parameter space. The technique outperforms the existing analysis of parametric Markov chains by several orders of magnitude regarding both run-time and scalability. Its beauty is its applicability to various probabilistic models. It in particular provides the first sound and feasible method for performing parameter synthesis of Markov decision processes.