Distributional Probabilistic Model Checking

Summary

This partial ingest is based on the abstract, setup, algorithm sections, experiments, conclusion, and appendix statements in the extracted PDF text. The paper extends Probabilistic Model Checking from expected reward/cost queries to distributional reward queries over DTMCs and MDPs. The target quantity is the full distribution of cumulative reward or cost until a co-safe Linear Temporal Logic formula is satisfied, so downstream analysis can ask for expected value, variance, mode, VaR, CVaR, or other distributional summaries.

The paper’s main wiki role is to connect temporal-logic model checking, risk-sensitive planning, and distributional RL-style value distributions in a formal verification setting.

Key Claims

• Expected reward can hide high-cost, low-probability outcomes and multimodal reward/cost behavior, so verification sometimes needs the full reward distribution rather than a scalar expectation.
• For DTMCs, the authors compute a finite approximation of the full reward distribution to a user-specified precision by graph analysis followed by forward distribution generation.
• For MDPs, they propose risk-neutral and risk-sensitive Distributional Value Iteration methods that maintain value distributions per state and optimize either expected cumulative reward or CVaR.
• For CVaR, memoryless policies are generally insufficient; the method uses a product MDP with a discretized slack/risk-budget variable and shows convergence toward the continuous-budget optimum as the discretization is refined.
• Experiments in a PRISM extension show the approach can handle large benchmark DTMCs/MDPs, but risk-sensitive DVI is much more expensive because the slack variable enlarges the product state space.

Methods / Formalism

• A DTMC distributional query has the form

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

where r is a reward structure, f is a distributional property such as E, Var, VaR, or CVaR, and \psi is co-safe LTL.

• An MDP distributional optimization query has the form

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

where f is specialized in the paper to expected value or CVaR and opt is min or max.

• The semantics use a random variable X^{r,\psi} for cumulative reward until the shortest good prefix of \psi; if the path never satisfies \psi, the value is \infty.
• Co-safe LTL is reduced to reachability by building a DFA for good prefixes and forming a DTMC-DFA or MDP-DFA product.
• The DTMC algorithm tracks probabilities over (state, accumulated_reward) pairs, separates bottom SCCs that cannot reach the target, and stops when the remaining finite/infinite mass uncertainty is below epsilon.
• Risk-neutral DVI replaces scalar Bellman values with projected categorical or quantile distributions and chooses actions minimizing expected value.
• Risk-sensitive DVI uses the dual representation of CVaR and an augmented state space S x B, where B is a finite grid of slack/risk-budget values.
• The denser formal payload is summarized in Distributional Queries and DVI.

Evidence / Experiments

• The prototype extends the PRISM explicit-state engine.
• Case studies include betting, deep sea treasure, obstacle, UAV, energy, and standard DTMC benchmarks from the PRISM suite.
• Risk-neutral DVI generally recovers the same expected-value policy as classical value iteration while also producing a distribution that supports additional summaries.
• Risk-sensitive DVI yields lower CVaR policies, at substantially higher runtime due to the slack-variable product.
• Forward DTMC distribution generation is often fast and gives a more precise policy-evaluation distribution, but it becomes expensive when the reward distribution has large support.
• Increasing the number of categorical/quantile atoms improves approximation quality, while increasing slack-budget atoms improves CVaR policy quality at a direct computational cost.

Connections

• Extends the Temporal Logic cluster by making co-safe LTL specifications the stopping condition for distributional reward analysis.
• Provides a primary source for Probabilistic Model Checking and Distributional Value Iteration in this vault.
• Connects to Safe Reinforcement Learning because risk-sensitive policies can avoid low-probability, high-cost trajectories that expected-value objectives accept.
• Connects to Decision Theory through CVaR and risk-sensitive optimization.
• Connects to Probability and Statistics because the central object is the full distribution of a trajectory-level random variable.
• Related to Jamroga2026 - Towards Probabilistic Strategic Timed CTL because both enrich temporal reasoning with probabilistic guarantees, but this paper is distributional and reward-centric rather than strategic and coalition-centric.
• Related to Vinzent2026 - Probabilistic Safety Verification of Neural Policies via Predicate Abstraction because both use probabilistic verification for policy/system assurance, though this paper assumes explicit DTMC/MDP models.

Open Questions

• How sensitive are the resulting policies to the chosen categorical/quantile representation when the reward distribution has heavy tails?
• Can the distributional query language be extended cleanly to multi-objective or multi-agent settings without making the state explosion worse than the underlying product constructions?
• What guarantees survive when the DTMC/MDP model is learned rather than supplied exactly?
• How should these distributional verification outputs be exposed to an RL training loop: as constraints, diagnostics, shields, or objective shaping?

Citation

Elsayed-Aly, I., Parker, D., and Feng, L. (2024). Distributional probabilistic model checking. In Proceedings of the 16th NASA Formal Methods Symposium (NFM 2024). arXiv:2309.05584.