INTERLEAVE: A Faster Symbolic Algorithm for Maximal End Component Decomposition
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916853576630272 |
|---|---|
| author | Bansal, Suguman Singh, Ramneet |
| author_facet | Bansal, Suguman Singh, Ramneet |
| contents | 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 19 more benchmarks (out of 379) than the closest previous algorithm. On the 149 benchmarks that prior approaches can solve, we demonstrate a 3.81x average speedup in runtime. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_20748 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | INTERLEAVE: A Faster Symbolic Algorithm for Maximal End Component Decomposition Bansal, Suguman Singh, Ramneet Logic in Computer Science Formal Languages and Automata Theory Programming Languages D.3.1; F.3.1; F.4.0 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 19 more benchmarks (out of 379) than the closest previous algorithm. On the 149 benchmarks that prior approaches can solve, we demonstrate a 3.81x average speedup in runtime. |
| title | INTERLEAVE: A Faster Symbolic Algorithm for Maximal End Component Decomposition |
| topic | Logic in Computer Science Formal Languages and Automata Theory Programming Languages D.3.1; F.3.1; F.4.0 |
| url | https://arxiv.org/abs/2505.20748 |