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.

翻译：在马尔可夫决策过程（MDP）中计算最优条件可达概率可通过归约为可达概率实现。然而，这种归约会产生循环结构复杂且通常极难求解的MDP。我们提出了一种实用的高效替代方法，用于计算最优条件可达概率。该方法数值稳定，能在非循环MDP上以线性时间判定阈值问题，且性能与标准可达查询相当。我们还将该方法集成到抽象精化框架中，用于同时分析数百万条马尔可夫链。通过在贝叶斯网络分析、概率程序及运行时监控等基准测试中的验证，我们展示了新方法的有效性，并实现了高达多个数量级的加速。