Title: INTERLEAVE: A Faster Symbolic Algorithm for Maximal End Component Decomposition

Speaker: Ramneet Singh   (bio) (bio)

Ramneet Singh is currently an AI Researcher at Proximal, working on synthetic RL environment generation for post-training of LLMs. Prior to this, he was a Research Fellow at Microsoft Research India, working on AI agents for large-scale software engineering tasks. He acquired a background in formal methods at IIT Delhi and Georgia Tech, where the work being presented was done as part of his Master's Thesis. He loves thinking about how to formally specify system behaviour and believes it has become even more important today.

When: Friday, 11 September 2026 at 1500 hrs (IST)  

Meeting Details: Zoom link, ID: 891 6409 4870, Passcode: 082194

Abstract:
The talk 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.