# Probabilistic model checking Probabilistic model checking computes how likely a system is to meet a requirement, rather than whether it can fail at all. The system is modeled as a discrete- or continuous-time Markov chain, or a Markov decision process, whose transitions carry genuine probabilities. The properties are numeric bounds: does the chain miss its deadline with probability under 0.01, does the protocol deliver within the bound at least 99% of the time, does the expected energy to completion stay within budget? It comes in two modes. The **exact** engine enumerates the reachable state space and computes the true probability by solving the underlying equations (PRISM, Storm). **Statistical model checking (SMC)** instead simulates the model many times and applies a hypothesis test to the runs, trading the exact answer for the number of runs the budget allows on a model far too large to enumerate. The randomness in both modes is the *model's own*: transition probabilities declared in the model and sampled from it. That is what separates probabilistic model checking from [statistical / sampling testing](https://quality.stereobooster.com/statistical-testing.md), whose variation comes from a real, unmodelable system. And because it reasons over a formal model rather than the implementation, it shares the formal family's caveat: a verdict about a model the code diverges from is not a verdict about the code. For the qualitative (non-probabilistic) sibling and the wider family see [model checking](https://quality.stereobooster.com/model-checking.md) and [formal methods](https://quality.stereobooster.com/formal.md). ## Exact probabilistic model checking The exact engine builds the model's reachable state space and computes the probability of a temporal property directly: for a PCTL or CSL formula like `P<0.01 [ F deadline_missed ]` it solves a linear system (discrete-time chains) or a set of differential equations (continuous time), and for Markov decision processes it optimizes over the adversary's choices. The answer is the *true* probability, so the verdict carries no sampling error. - **PRISM** — the reference checker for DTMCs, CTMCs, MDPs and probabilistic timed automata (Kwiatkowska et al. 2011)[^kwiatkowska2011]. - **[Storm](https://www.stormchecker.org/)** — a modern checker with a modular solver setup and a Python API; it analyzes discrete- and continuous-time Markov chains and MDPs and consumes PRISM and JANI models, dynamic fault trees, and generalized stochastic Petri nets (Dehnert et al. 2017)[^dehnert2017]. Exact analysis gives the stronger guarantee whenever the state space fits in memory. ## What the statistical mode catches - **Probabilistic property violations beyond exact reach.** "P(deadline missed) exceeds the bound" on a model whose state space is too large for the exact engine. - **Quantitative timing and performance properties.** Expected response time, probability of buffer overflow, energy budgets on timed and priced automata: questions an exact checker cannot always express but a simulator measures directly. - **Rare-but-bounded failure rates.** With the right sampling scheme, the probability of a rare violation is estimated to a stated confidence rather than proved. What SMC does **not** give: the *exact* probability, or a guarantee that holds for *every* trace. Its verdict is statistical: bounded error rates over the runs sampled, so a rare event below the sampling resolution can be missed. ## Statistical model checking tools - **[UPPAAL-SMC](https://uppaal.org/)** — the statistical engine of the UPPAAL real-time-systems toolset; simulates networks of stochastic timed automata and tests probabilistic and expected-value properties. - The **statistical engine in [PRISM](https://www.prismmodelchecker.org/)** — the sampling-based mode of the dual-engine checker. - **[PLASMA Lab](https://project.inria.fr/plasma-lab/)** — a standalone statistical model checker with pluggable simulators and rare-event sampling. ## When to use, when not **Use:** - When the model carries genuine probabilities (failure rates, timing jitter, message-loss rates) and the question is quantitative ("how often", not "ever"). - When the state space is too large for the exact engine. SMC's cost scales with the number of runs, not the size of the state space. - For rare-event probabilities, paired with an importance-sampling scheme that the tool supports. **Don't:** - When the state space is small enough to enumerate. Use the exact engine (PRISM, Storm) instead. - For non-probabilistic safety properties. A property that must hold on *every* trace is the job of exhaustive [model checking](https://quality.stereobooster.com/model-checking.md); sampling can only ever say "not observed in *N* runs." - As a check on the implementation. SMC verifies the model; pair it with property-based or differential testing of the code on the same surface. ## Evidence The technical case is mathematical, not empirical: SMC's verdict is decided by the sequential probability ratio test (Wald 1945)[^wald1945], carried into probabilistic verification (Younes and Simmons 2006)[^younes2006] and later generalized (Li et al. 2014)[^li2014]. The SPRT bounds the false-accept / false-reject rate, so the sampling error is quantified rather than assumed: bounded, not eliminated. ## Related **Looks alike — Statistical testing vs statistical model checking** Both sample many runs and make a statistical decision, which makes them look like the same method — but they sample different things. Statistical model checking samples a *model* whose probabilities you know and can simulate; [statistical testing](https://quality.stereobooster.com/statistical-testing.md) samples a *real system* whose randomness you can't model, only observe. **Model checking vs probabilistic model checking** Both check whether a property holds over a system's state space; they differ in the *kind* of property and model. [Model checking](https://quality.stereobooster.com/model-checking.md) checks a *boolean* temporal or safety property over a state-transition model: it holds, or there is a counterexample. Probabilistic model checking generalizes this to a *stochastic* model (a Markov chain or MDP) and a *quantitative* property, computing the probability that it holds, either exactly (PRISM, Storm) or by sampling for state spaces too large to enumerate. ## Classification - **Quality dimensions:** Reliability, Performance (checks quantitative timing properties — expected response time, energy budgets on priced automata). - **Area:** Stochastic and real-time protocols, continuous-time Markov chains, Markov decision processes, cyber-physical and biological models; any system with a probabilistic specification too large to verify exactly. - **Guarantee:** Empirical, Exhaustive (exact). ## Referenced by - [Quality dimensions](https://quality.stereobooster.com/quality-dimensions.md) · Quality dimensions - [Guarantee](https://quality.stereobooster.com/guarantee.md) · The axes - [Oracle](https://quality.stereobooster.com/oracle.md) · The axes - [State machines and statecharts](https://quality.stereobooster.com/state-machines.md) · Methods - [Statistical and sampling testing](https://quality.stereobooster.com/statistical-testing.md) · Methods - [Verifying safety-critical systems](https://quality.stereobooster.com/safety.md) · Methods - [How AI fits into software quality](https://quality.stereobooster.com/ai.md) · AI ## References [^kwiatkowska2011]: Kwiatkowska, Marta, Gethin Norman, and David Parker. 2011. "[PRISM 4.0: Verification of Probabilistic Real-time Systems](https://inria.hal.science/hal-00648035/document)." *Computer Aided Verification (CAV 2011)*, Lecture notes in computer science, vol. 6806: 585–91. [https://doi.org/10.1007/978-3-642-22110-1\\\_47](https://doi.org/10.1007/978-3-642-22110-1\_47). [^dehnert2017]: Dehnert, Christian, Sebastian Junges, Joost-Pieter Katoen, and Matthias Volk. 2017. "[A Storm is Coming: A Modern Probabilistic Model Checker](https://arxiv.org/pdf/1702.04311)." *Computer Aided Verification (CAV 2017)*, Lecture notes in computer science, vol. 10427: 592–600. [https://doi.org/10.1007/978-3-319-63390-9\\\_31](https://doi.org/10.1007/978-3-319-63390-9\_31). [^wald1945]: Wald, Abraham. 1945. "[Sequential Tests of Statistical Hypotheses](https://projecteuclid.org/journals/annals-of-mathematical-statistics/volume-16/issue-2/Sequential-Tests-of-Statistical-Hypotheses/10.1214/aoms/1177731118.pdf)." *Annals of Mathematical Statistics* 16 (2): 117–86. . [^younes2006]: Younes, Håkan L. S., and Reid G. Simmons. 2006. "[Statistical Probabilistic Model Checking with a Focus on Time-Bounded Properties](http://www.cs.cmu.edu/~lorens/papers/tmp/prob_model_checking.pdf)." *Information and Computation* 204 (9): 1368–409. . [^li2014]: Li, Xiaoou, Jingchen Liu, and Zhiliang Ying. 2014. "[Generalized Sequential Probability Ratio Test for Separate Families of Hypotheses](https://pmc.ncbi.nlm.nih.gov/articles/PMC4941833/)." *Sequential Analysis* 33 (4): 539–63. . ## Acronyms - CSL — continuous stochastic logic - CTMC — continuous-time Markov chain - DTMC — discrete-time Markov chain - MDP — Markov decision process - PCTL — probabilistic computation tree logic - SMC — statistical model checking - SPRT — sequential probability ratio test