# Efficient Parametric Model Checking Using Domain Knowledge

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

## Key facts

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

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

- [Dependability Analysis of Deep Reinforcement Learning based Robotics and Autonomous Systems through Probabilistic Model Checking](https://mlsanity.com/paper/2109.06523/) (2021)
- [Leveraging System-Level Observations to Inform Bayesian Learning of Model Parameters for Quantitative Verification](https://mlsanity.com/paper/2608.03489/) (2026)

## Abstract (arXiv)

We introduce an efficient parametric model checking (ePMC) method for the analysis of reliability, performance and other quality-of-service (QoS) properties of software systems. ePMC speeds up the analysis of parametric Markov chains modelling the behaviour of software by exploiting domain-specific modelling patterns for the software components. To this end, ePMC precomputes closed-form expressions for key QoS properties of such patterns, and uses these expressions in the analysis of whole-system models. To evaluate ePMC, we show that its application to service-based systems and multi-tier software architectures reduces analysis time by several orders of magnitude compared to current parametric model checking methods.