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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

INTERLEAVE: A Faster Symbolic Algorithm for Maximal End Component Decomposition

  • Suguman Bansal,
  • Ramneet Singh

摘要

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.