Probabilistic Model Checking

Definition

Probabilistic model checking verifies quantitative properties of stochastic transition models such as DTMCs and MDPs. Instead of asking only whether all executions satisfy a temporal property, it asks for probabilities, rewards, costs, or policies associated with temporal specifications.

Why It Matters

Many learning, robotics, and distributed systems have uncertainty in transitions or nondeterminism in choices. Probabilistic model checking gives a way to state and compute formal guarantees about those systems, including safety probabilities and risk-sensitive cost summaries.

Formalism / Key Objects

• DTMCs model probabilistic transitions without controllable choices.
• MDPs model both probabilistic transitions and nondeterministic or policy-resolved action choices.
• Temporal specifications can be written in logics such as Linear Temporal Logic, PCTL-like logics, or richer strategic logics.
• Reward queries attach costs or rewards to states/actions. In Elsayed-Aly2024 - Distributional Probabilistic Model Checking, a distributional query has the form

$$R_{=?}^{f(r)}[\psi ],$$

where f can be a distributional property such as expectation, variance, VaR, or CVaR.

• PCIS-style safety predecessors ask for states from which some policy can keep an MDP inside a safe set with probability at least 1-epsilon over a finite horizon.
• Explainable shielding computes finite-horizon state/action risk values such as risk(s,a,h) <= epsilon to decide which actions a probabilistic shield should permit.
• Sound reachability algorithms such as Sound Value Iteration maintain lower and upper probability bounds, for example with x_k(s)=Pr_s(\Diamond_{\le k}G) and y_k(s)=Pr_s(\Box_{\le k}S?), so unbounded reachability estimates can be certified before being used by a shield.
• pMDP-style compositional RL models can treat subsystem success probabilities as parameters and verify whether a high-level meta-policy reaches a goal with probability at least 1-delta.

Connections

• Distributional Value Iteration extends value iteration so MDP model checking can optimize over full reward distributions.
• Distributional Queries and DVI stores the heavier reward-distribution query semantics and DVI construction.
• Sound Value Iteration provides scalar reachability and expected-reward bounds when ordinary value iteration would only give a one-sided or heuristic approximation.
• Probabilistic Shielding consumes these conservative probability bounds to enforce unsafe-reachability thresholds during RL.
• PCIS Safety Predecessor stores the heavier safety-predecessor recursion for PCIS-style probability guarantees.
• Predicate Abstraction can reduce rich policy or system models into finite probabilistic models suitable for verification.
• Probabilistic Strategic Timed CTL combines probabilistic model checking with strategic and timed reasoning.
• Runtime Verification monitors concrete traces; probabilistic model checking usually reasons over a model before or alongside execution.
• Probabilistic Controlled Invariant Sets use similar MDP probability guarantees, but package the result as a runtime safe set and action filter for learning.
• Explainable Shielding uses probabilistic model-checking risk results as the target for compact safety explanations.
• Compositional Reinforcement Learning can use probabilistic reachability models to lift local subsystem success guarantees into system-level claims.

Common Confusions

• Probabilistic model checking is not just simulation. It explores a formal model numerically or symbolically to compute guarantees.
• A probability guarantee is only as meaningful as the model and abstraction assumptions behind it.
• Expected reward is only one quantitative query; distributional and tail-risk queries can reveal failures hidden by expectations.

Key Sources

• Elsayed-Aly2024 - Distributional Probabilistic Model Checking
• Neary2022 - Verifiable and Compositional Reinforcement Learning Systems
• Quatmann2018 - Sound Value Iteration
• HamelDeLeCourt2025 - Probabilistic Shielding for Safe Reinforcement Learning
• Rieder2025 - Explainably Safe Reinforcement Learning
• Hashimoto2026 - Data-Driven Synthesis of Probabilistic Controlled Invariant Sets for Linear MDPs
• Jamroga2026 - Towards Probabilistic Strategic Timed CTL
• Vinzent2026 - Probabilistic Safety Verification of Neural Policies via Predicate Abstraction