Fast Computation of Conditional Probabilities in MDPs and Markov Chain Families

Technical Summary: Fast Computation of Conditional Probabilities in MDPs and Markov Chain Families

Problem Statement
The paper addresses the challenge of computing optimal conditional reachability probabilities in Markov Decision Processes (MDPs). While conditional reachability on Markov Chains (MCs) is tractable via Bayes' theorem, extending this to MDPs is difficult because the optimal policy for the numerator (reaching both goal $G$ and evidence $E$) and the denominator (reaching evidence $E$) are generally different. The standard state-of-the-art approach, the "restart method" (Baier et al. [7]), reduces the problem to a standard reachability query by rewiring transitions from states that cannot reach $E$ back to the initial state. However, this transformation introduces cycles even in originally acyclic MDPs, creating "challenging" instances that are notoriously difficult for standard solvers like value iteration and often lead to numerical instability or poor performance.

Methodology
The authors propose an alternative method rooted in multi-objective model checking and total reward queries, avoiding the introduction of cycles. The core approach involves three main steps:

1. Threshold Decision via Total Reward:
   To decide if $\Pr^{\max}_M(\diamond G \mid \diamond E) \le \lambda$, the authors utilize a key observation derived from Bayes' law:
   $$\max_{\sigma} \Pr_\sigma(\diamond G \mid \diamond E) \le \lambda \iff \max_{\sigma \in \Sigma_{M,E}} \left( \Pr_\sigma(\diamond G \cap \diamond E) - \lambda \cdot \Pr_\sigma(\diamond E) \right) \le 0$$
   This transforms the conditional problem into maximizing a linear combination of two reachability probabilities. This expression is reformulated as an expected total reward problem. A reward function $R_\lambda$ is defined such that reaching states in $E$ yields a reward based on the probability of subsequently reaching $G$, and reaching states in $G$ yields a reward based on the probability of subsequently reaching $E$.

2. Preprocessing and Initial Component Elimination:
   To ensure the total reward query is well-defined and solvable, the authors preprocess the MDP:

   • States in $G \cup E$ are made absorbing.
   • A set of terminal states $T$ is defined (states in $E$ and states in $G$ that can reach $E$).
   • Crucially, the algorithm identifies an "initial component" ($CI$) consisting of states from which $T$ cannot be reached with positive probability under some policies. These states are eliminated by constructing a new MDP ($\tilde{M}$) where transitions exiting $CI$ are explicitly modeled. This ensures that all policies in the new MDP reach $T$ with positive probability, allowing standard total reward algorithms (like value iteration or linear programming) to be applied without issues regarding undefined conditional probabilities.

3. Optimization via Bisection:
   To compute the optimal value (Problem 2), the threshold decision procedure is embedded within a bisection algorithm. The authors introduce several optimizations:

   • Exact Computation: Using Stern-Brocot tree traversal to find rational numbers with minimal denominators.
   • Policy Tracking: If the same policy induces the optimal value for both the lower and upper bounds of the bisection interval, the exact optimal value can be computed immediately without further iterations.
   • Advanced Bounds: Using pre-computed reachability probabilities for $E$ to tighten the bounds of the bisection search.

4. Integration with Abstraction-Refinement (Colored MDPs):
   The method is extended to analyze families of Markov Chains represented as Colored MDPs (where policies must be color-consistent). The authors adapt the abstraction-refinement framework [3] to handle conditional properties. They note that standard heuristics for refinement (based on visit counts) are not directly applicable; instead, they employ a backward refinement strategy focusing on the distance from the initial state.

Key Contributions

• New Algorithm: A numerically stable, cycle-free reduction of conditional reachability in MDPs to total reward queries.
• Complexity: For acyclic MDPs, the threshold problem can be decided in linear time ($O(\|M\|)$), a significant improvement over the restart method which introduces cycles.
• Policy Extraction: A technique to extract optimal policies for conditional properties, which are not necessarily memoryless, enabling integration into abstraction-refinement loops.
• Scalability: The ability to analyze millions of Markov Chains simultaneously via Colored MDPs and abstraction-refinement.

Results
The authors implemented their approach in the Storm model checker and evaluated it against the restart method on 318 benchmarks from Bayesian networks, probabilistic programs, and runtime monitoring.

• Performance: The new method ("treat") achieves speed-ups of multiple orders of magnitude compared to the restart method, particularly on acyclic benchmarks and those with large initial components.
• Accuracy: The restart method frequently fails to converge or produces significant numerical errors on standard benchmarks. The new method provides accurate results in both floating-point and exact arithmetic.
• Colored MDPs: In the context of Colored MDPs, the new method significantly outperforms the restart method, solving benchmarks that previously timed out.
• Runtime Monitoring: In runtime monitoring experiments, the new approach reduces average evaluation times from seconds to sub-second levels, making it viable for learning and deploying monitors.

Significance
The paper claims to provide a "significant step forward" in computing conditional probabilities on MDPs. By moving away from the restart method's cyclic reductions, the authors enable efficient, stable, and exact analysis of conditional reachability. This makes it feasible to apply conditional reasoning to complex systems modeled as MDPs, including those with uncertain parameters (Bayesian networks) and large families of configurations (Colored MDPs). The work bridges the gap between theoretical multi-objective model checking and practical, high-performance verification tools.