Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Distributional Probabilistic Model Checking

Ingy Elsayed-Aly, David Parker, Lu Feng

TL;DR

This work extends probabilistic model checking to reason about full reward distributions in DTMCs and MDPS by introducing distributional queries and distributional value iteration. It supports both risk-neutral and risk-sensitive objectives, notably CVaR, and uses forward distribution generation for DTMCs alongside categorical and quantile distribution representations. The risk-neutral and CVaR DVI algorithms are implemented as PRISM extensions and validated on sizeable benchmarks, demonstrating accurate distributions and scalable performance. This distributional capability enables risk-aware verification and controller synthesis for safety-critical systems where tail behavior and variability matter beyond the mean.

Abstract

Probabilistic model checking can provide formal guarantees on the behavior of stochastic models relating to a wide range of quantitative properties, such as runtime, energy consumption or cost. But decision making is typically with respect to the expected value of these quantities, which can mask important aspects of the full probability distribution such as the possibility of high-risk, low-probability events or multimodalities. We propose a distributional extension of probabilistic model checking, applicable to discrete-time Markov chains (DTMCs) and Markov decision processes (MDPs). We formulate distributional queries, which can reason about a variety of distributional measures, such as variance, value-at-risk or conditional value-at-risk, for the accumulation of reward until a co-safe linear temporal logic formula is satisfied. For DTMCs, we propose a method to compute the full distribution to an arbitrary level of precision, based on a graph analysis and forward analysis of the model. For MDPs, we approximate the optimal policy with respect to expected value or conditional value-at-risk using distributional value iteration. We implement our techniques and investigate their performance and scalability across a range of benchmark models. Experimental results demonstrate that our techniques can be successfully applied to check various distributional properties of large probabilistic models.

Distributional Probabilistic Model Checking

TL;DR

This work extends probabilistic model checking to reason about full reward distributions in DTMCs and MDPS by introducing distributional queries and distributional value iteration. It supports both risk-neutral and risk-sensitive objectives, notably CVaR, and uses forward distribution generation for DTMCs alongside categorical and quantile distribution representations. The risk-neutral and CVaR DVI algorithms are implemented as PRISM extensions and validated on sizeable benchmarks, demonstrating accurate distributions and scalable performance. This distributional capability enables risk-aware verification and controller synthesis for safety-critical systems where tail behavior and variability matter beyond the mean.

Abstract

Probabilistic model checking can provide formal guarantees on the behavior of stochastic models relating to a wide range of quantitative properties, such as runtime, energy consumption or cost. But decision making is typically with respect to the expected value of these quantities, which can mask important aspects of the full probability distribution such as the possibility of high-risk, low-probability events or multimodalities. We propose a distributional extension of probabilistic model checking, applicable to discrete-time Markov chains (DTMCs) and Markov decision processes (MDPs). We formulate distributional queries, which can reason about a variety of distributional measures, such as variance, value-at-risk or conditional value-at-risk, for the accumulation of reward until a co-safe linear temporal logic formula is satisfied. For DTMCs, we propose a method to compute the full distribution to an arbitrary level of precision, based on a graph analysis and forward analysis of the model. For MDPs, we approximate the optimal policy with respect to expected value or conditional value-at-risk using distributional value iteration. We implement our techniques and investigate their performance and scalability across a range of benchmark models. Experimental results demonstrate that our techniques can be successfully applied to check various distributional properties of large probabilistic models.
Paper Structure (14 sections, 2 theorems, 4 equations, 4 figures, 2 tables, 3 algorithms)

This paper contains 14 sections, 2 theorems, 4 equations, 4 figures, 2 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. Related Work
  3. Background
  4. Random Variables and Probability Distributions
  5. Markov Chains and Markov Decision Processes
  6. Distributional Probabilistic Model Checking
  7. Distributional Model Checking Algorithms
  8. Forward Distribution Generation for DTMCs
  9. Risk-Neutral Distributional Value Iteration for MDPs
  10. Risk-Sensitive Distributional Value Iteration for MDPs
  11. Experiments
  12. Case Studies
  13. Results Analysis
  14. Conclusion

Key Result

lemma thmcounterlemma

Let $[x]^+$ denote the function that is 0 if $x<0$, and $x$ otherwise. Given a random variable $X$ over the probability space $(\Omega, {\mathcal{F}}, \Pr)$, it holds that: and the minimum-point is given by $b^* = {\mathsf{VaR}_{\alpha}}(X)$. $\sqcap$$\sqcup$=0

Figures (4)

  • Figure 1: An example distribution with its categorical and quantile representations.
  • Figure 2: The "mud & nails" example. Left: Map of the terrain to navigate, with two policies that minimize expected cost and conditional value-at-risk to visit $g_1$ and then $g_2$. Right: The corresponding distributions over cost.
  • Figure 3: Varying the numbers of atoms for distributional representations.
  • Figure 4: Results for varying the numbers of atoms in risk-sensitive DVI.

Theorems & Definitions (9)

  • definition thmcounterdefinition: Categorical representation
  • definition thmcounterdefinition: Quantile representation
  • definition thmcounterdefinition: DTMC
  • definition thmcounterdefinition: MDP
  • definition thmcounterdefinition: Reward structure
  • definition thmcounterdefinition: Distributional query
  • definition thmcounterdefinition: Distributional optimization query
  • lemma thmcounterlemma: Dual Representation of ${\mathsf{CVaR}_{}}$ bauerle2011markovrockafellar2002conditional
  • lemma thmcounterlemma