The research paper “Fast Computation of Conditional Probabilities in MDPs and Markov Chain Families” by Sebastian Junges, Luko van der Maas (both Radboud University, Nijmegen), Milan Ceska, Filip Macák (both Brno University of Technology), and Tim Quatmann (RWTH) has been accepted for CAV 2026.

The paper introduces a practically efficient method to compute optimal conditional reachability probabilities in MDPs. On acyclic MDPs, the approach decides in linear time, whether the conditional probability exceeds a given threshold. Integration into an abstraction-refinement framework allows analysing millions of Markov chains at once. Experiments on benchmarks from Bayesian network analysis, probabilistic programs, and runtime monitoring show speed-ups up to multiple orders of magnitude compared to existing methods.