INTERLEAVE: A Faster Symbolic Algorithm for Maximal End Component Decomposition

Abstract 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 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 on the standardized Quantitative Verification Benchmark Set demonstrates that it solves $\textbf{19}$ 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}$ 3.81 × average speedup in runtime.