Skip to content

Software Quality

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, 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 and formal methods.

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)1.
  • Storm — 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)2.

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 — 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 — the sampling-based mode of the dual-engine checker.
  • 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; 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)3, carried into probabilistic verification (Younes and Simmons 2006)4 and later generalized (Li et al. 2014)5. The SPRT bounds the false-accept / false-reject rate, so the sampling error is quantified rather than assumed: bounded, not eliminated.

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 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 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

References

  1. Kwiatkowska, Marta, Gethin Norman, and David Parker. 2011. "PRISM 4.0: Verification of Probabilistic Real-time Systems." 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. ↩

  2. Dehnert, Christian, Sebastian Junges, Joost-Pieter Katoen, and Matthias Volk. 2017. "A Storm is Coming: A Modern Probabilistic Model Checker." 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. ↩

  3. Wald, Abraham. 1945. "Sequential Tests of Statistical Hypotheses." Annals of Mathematical Statistics 16 (2): 117–86. https://doi.org/10.1214/aoms/1177731118. ↩

  4. Younes, Håkan L. S., and Reid G. Simmons. 2006. "Statistical Probabilistic Model Checking with a Focus on Time-Bounded Properties." Information and Computation 204 (9): 1368–409. https://doi.org/10.1016/j.ic.2006.05.002. ↩

  5. Li, Xiaoou, Jingchen Liu, and Zhiliang Ying. 2014. "Generalized Sequential Probability Ratio Test for Separate Families of Hypotheses." Sequential Analysis 33 (4): 539–63. https://doi.org/10.1080/07474946.2014.961861. ↩