Fast Computation of Conditional Probabilities in MDPs and Markov Chain Families
This work provides a practically efficient solution for computing conditional probabilities in MDPs, a problem relevant to verification and analysis of probabilistic systems.
The paper presents a new method for computing optimal conditional reachability probabilities in MDPs that is numerically stable and achieves speed-ups up to multiple orders of magnitude on benchmarks from Bayesian network analysis, probabilistic programs, and runtime monitoring.
Computing optimal conditional reachability probabilities in Markov decision processes (MDPs) is tractable by a reduction to reachability probabilities. Yet, this reduction yields cyclic, challenging MDPs that are often notoriously hard to solve. We present an alternative, practically efficient method to compute optimal conditional reachabilities. This new method is numerically stable, can decide the threshold problem in linear time on acyclic MDPs, and yields performance comparable to standard reachability queries. We also integrate the method in an abstraction-refinement framework to analyse millions of Markov chains at once. We demonstrate the efficacy of the new methods on benchmarks from Bayesian network analysis, probabilistic programs, and runtime monitoring and show speed-ups up to multiple orders of magnitude.