Robust Probabilistic Model Checking with Continuous Reward Domains

TL;DR

The paper tackles the limitation of probabilistic model checking that focuses on expected values by introducing a moment-matching framework that uses mixtures of Erlang distributions to approximate the full distribution of cumulative rewards in discrete-time Markov chains. By deriving higher-order moments via the moment generating function and solving a truncated Stieltjes moment problem with a maximum-entropy objective, it achieves bounded approximation error while preserving distributional characteristics. This enables robust, distribution-focused model checking for chance constraints such as $\Pr(X \le r^*) \ge \alpha$, compatible with both continuous and discrete reward spaces without discretization. Theoretical results justify the Erlang-based approximations through discrete-phase-type representations and continuous Erlangization, and empirical evaluations demonstrate accurate, scalable performance across PRISM-inspired benchmarks, including challenging continuous-reward cases like UAV energy and Future Investor.

Abstract

Probabilistic model checking traditionally verifies properties on the expected value of a measure of interest. This restriction may fail to capture the quality of service of a significant proportion of a system's runs, especially when the probability distribution of the measure of interest is poorly represented by its expected value due to heavy-tail behaviors or multiple modalities. Recent works inspired by distributional reinforcement learning use discrete histograms to approximate integer reward distribution, but they struggle with continuous reward space and present challenges in balancing accuracy and scalability. We propose a novel method for handling both continuous and discrete reward distributions in Discrete Time Markov Chains using moment matching with Erlang mixtures. By analytically deriving higher-order moments through Moment Generating Functions, our method approximates the reward distribution with theoretically bounded error while preserving the statistical properties of the true distribution. This detailed distributional insight enables the formulation and robust model checking of quality properties based on the entire reward distribution function, rather than restricting to its expected value. We include a theoretical foundation ensuring bounded approximation errors, along with an experimental evaluation demonstrating our method's accuracy and scalability in practical model-checking problems.

Figures (6)

• Figure 1: UAV flight process with states $\{s_0, s_1, s_2, s_3, s_4\}$ representing Takeoff, Stable Flight, Maneuvering, Descent, and Landing, respectively. Transition probabilities and rewards are shown on the edges in the form of $p$/$\underline{r}$. The cumulative reward distribution at $s_0$ is illustrated using the expected value (grey), probability histogram estimation (light blue), and true simulated distribution points (green), highlighting the different levels of information provided by various methods on the same distribution.
• Figure 2: Cantelli Bound's Coarseness in Model Checking
• Figure 3: PDF and CDF for discrete reward space subjects (figure 1 of 2)
• Figure 4: PDF and CDF for discrete reward space subjects (figure 2 of 2)
• Figure 5: PDF and CDF for continuous reward space subjects

Theorems & Definitions (6)

• Theorem 4.1: Approximation of Cumulative Reward by Discrete Phase-Type (DPH) Distribution
• proof
• Theorem 4.2: Continuous Approximation of DPH by Erlangization
• proof
• Theorem 4.3: Mixture of Erlang Distributions Approximation
• proof