# Parameter Synthesis in Markov Models: A Gentle Survey

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

## Key facts

- Cited by 10 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 14 Jul 2022.

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

- [Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet](https://mlsanity.com/paper/2411.11451/) (2024)
- [Imprecise Probabilities Meet Partial Observability: Game Semantics for Robust POMDPs](https://mlsanity.com/paper/2405.04941/) (2024)
- [Efficient Sensitivity Analysis for Parametric Robust Markov Chains](https://mlsanity.com/paper/2305.01473/) (2023)
- [What should be observed for optimal reward in POMDPs?](https://mlsanity.com/paper/2405.10768/) (2024)
- [Data-Efficient Safe Policy Improvement Using Parametric Structure](https://mlsanity.com/paper/2507.15532/) (2025)
- [MM Algorithms to Estimate Parameters in Continuous-time Markov Chains](https://mlsanity.com/paper/2302.08588/) (2023)
- [Scaling Observation-aware Planning in Uncertain Domains](https://mlsanity.com/paper/2605.22364/) (2026)
- [Tensor Probabilistic Model Checking of Finite-Horizon Markov Chains (Extended Version)](https://mlsanity.com/paper/2608.00374/) (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)

This paper surveys the analysis of parametric Markov models whose transitions are labelled with functions over a finite set of parameters. These models are symbolic representations of uncountable many concrete probabilistic models, each obtained by instantiating the parameters. We consider various analysis problems for a given logical specification varphi: do all parameter instantiations within a given region of parameter values satisfy varphi?, which instantiations satisfy varphi and which ones do not?, and how can all such instantiations be characterised, either exactly or approximately? We address theoretical complexity results and describe the main ideas underlying state-of-the-art algorithms that established an impressive leap over the last decade enabling the fully automated analysis of models with millions of states and thousands of parameters.