INTERLEAVE: A Faster Symbolic Algorithm for Maximal End Component Decomposition
摘要
This paper presents a novel symbolic algorithm for the Maximal End Component (MEC) decomposition of a Markov Decision Process (MDP). The key idea behind our algorithm INTERLEAVE is to interleave the computation of Strongly Connected Components (SCCs) with eager elimination of redundant state-action pairs, rather than performing these computations sequentially as done by existing state-of-the-art algorithms. Even though our approach has the same complexity as prior works, an empirical evaluation of INTERLEAVE on the standardized Quantitative Verification Benchmark Set demonstrates that it solves \(\textbf{19}\) more benchmarks (out of 368) than the closest previous algorithm. On the 149 benchmarks that prior approaches can solve, we demonstrate a \(\mathbf {3.81 \times }\) average speedup in runtime.