# Accelerating Parametric Probabilistic Verification

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 13 Dec 2013.

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

- [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)
- [Scalable Stochastic Parametric Verification with Stochastic Variational Smoothed Model Checking](https://mlsanity.com/paper/2205.05398/) (2022)
- [PAC Approximation and DIRECT Optimization for Parametric Markov Models](https://mlsanity.com/paper/2608.02184/) (2026)
- [Leveraging System-Level Observations to Inform Bayesian Learning of Model Parameters for Quantitative Verification](https://mlsanity.com/paper/2608.03489/) (2026)
- [Supermartingale Certificates for Parametric MDPs](https://mlsanity.com/paper/2609.12715/) (2026)

## Abstract (arXiv)

We present a novel method for computing reachability probabilities of parametric discrete-time Markov chains whose transition probabilities are fractions of polynomials over a set of parameters. Our algorithm is based on two key ingredients: a graph decomposition into strongly connected subgraphs combined with a novel factorization strategy for polynomials. Experimental evaluations show that these approaches can lead to a speed-up of up to several orders of magnitude in comparison to existing approaches