Fast Computation of Conditional Probabilities in MDPs and Markov Chain Families

TL;DR

This paper introduces a new, efficient method for computing optimal conditional reachability probabilities in MDPs, improving performance and stability over traditional approaches, and enabling large-scale analysis.

Contribution

The authors develop a numerically stable, linear-time threshold decision method for acyclic MDPs and integrate it into a framework for analyzing millions of Markov chains simultaneously.

Findings

Achieved speed-ups up to multiple orders of magnitude on benchmarks.

Method is numerically stable and can decide threshold problems in linear time for acyclic MDPs.

Successfully applied to Bayesian networks, probabilistic programs, and runtime monitoring.

Abstract

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.