# Accelerated Model Checking of Parametric Markov Chains

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 15 May 2018.

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

- [Fine-Tuning the Odds in Bayesian Networks](https://mlsanity.com/paper/2105.14371/) (2021)
- [PAC Approximation and DIRECT Optimization for Parametric Markov Models](https://mlsanity.com/paper/2608.02184/) (2026)

## Abstract (arXiv)

Parametric Markov chains occur quite naturally in various applications: they can be used for a conservative analysis of probabilistic systems (no matter how the parameter is chosen, the system works to specification); they can be used to find optimal settings for a parameter; they can be used to visualise the influence of system parameters; and they can be used to make it easy to adjust the analysis for the case that parameters change. Unfortunately, these advancements come at a cost: parametric model checking is---or rather was---often slow. To make the analysis of parametric Markov models scale, we need three ingredients: clever algorithms, the right data structure, and good engineering. Clever algorithms are often the main (or sole) selling point; and we face the trouble that this paper focuses on -- the latter ingredients to efficient model checking. Consequently, our easiest claim to fame is in the speed-up we have often realised when comparing to the state of the art.