Distributional Queries and DVI

Context

Elsayed-Aly2024 - Distributional Probabilistic Model Checking extends reward-based probabilistic model checking from scalar expectations to full reward/cost distributions. The key move is to evaluate or optimize a trajectory-level random variable: accumulated reward until a co-safe LTL formula has a good prefix.

Formal Statement

For a DTMC, a distributional query is written

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

where r is a reward structure, f is a distributional property such as expectation, variance, mode, VaR, or CVaR, and \psi is a co-safe LTL formula.

For an MDP, a distributional optimization query is written

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

where opt is min or max; the paper focuses on f equal to expectation or CVaR.

The semantic random variable has the form

$$X^{r,\psi }(\omega )=\{\begin{array}{ll}r(\omega ,k_{\psi }-1)& \text{if }\omega \models \psi ,\\ \infty & \text{otherwise,}\end{array}$$

where k_\psi is the length of the shortest good prefix for \psi.

For CVaR, the paper uses the dual representation

$${\mathrm{CVaR}}_{\alpha }(X)=\underset{b\in \mathbb{R}}{\min }\left(b+\frac{1}{1-\alpha }\mathbb{E}([X-b{]}^{+})\right),$$

with the minimizer at VaR_alpha(X).

Derivation / Construction

• Compile the co-safe LTL formula \psi into a DFA A_\psi for good prefixes.
• Build a product DTMC or MDP with state space S x Q, reducing satisfaction of \psi to reachability of accepting automaton states.
• For DTMCs, compute a distribution over (state, accumulated_reward) pairs. The algorithm separates bottom SCCs that cannot reach the target, keeps probability mass for +\infty, and terminates when the remaining uncertainty is at most epsilon.
• The finite approximation hat_mu satisfies the paper’s pointwise/truncation guarantee: for each finite or infinite support value i, mu(i) <= hat_mu(i) <= mu(i)+epsilon, and omitted tail mass is bounded by epsilon.
• For risk-neutral MDP optimization, maintain a value distribution mu_s for each state and apply the distributional Bellman update

$$\eta (s,a)=\mathrm{proj}\left(r(s,a)+\sum _{s^{\prime }}P(s,a,s^{\prime }){\mu }_{s^{\prime }}\right).$$

The policy chooses the action minimizing the expected value of eta(s,a).

• For risk-sensitive CVaR optimization, augment the MDP with a finite grid B of slack/risk-budget values. The action criterion minimizes E([X-b]^+) on the augmented state (s,b), and the best initial budget is selected after convergence.
• If the slack grid has stride varsigma_n, the paper states that the CVaR gap induced by discretization is O(varsigma_n) and vanishes as |B| increases.

Implications

• Distributional model checking can expose tail-risk and multimodality that expected reward hides.
• Co-safe temporal specifications make the stopping condition trace-based without requiring infinite-horizon reward accumulation.
• Approximate categorical or quantile representations are computationally necessary for DVI, but representation coarseness can affect both metric accuracy and policy quality.
• A useful workflow is to synthesize an MDP policy with DVI, then evaluate the induced DTMC with the more precise forward distribution algorithm.

Links

• Source: Elsayed-Aly2024 - Distributional Probabilistic Model Checking
• Concepts: Probabilistic Model Checking, Distributional Value Iteration, Linear Temporal Logic, Safe Reinforcement Learning