EREQ: Regular Expressions with Quantifiers and Incremental Quantifier Elimination

Weak monadic second-order logic (wMSO) is a foundational tool for specifying regular properties. Traditional decision procedures for this logic typically translate wMSO formulas into finite automata. Although the logic is decidable, this approach incurs non-elementary complexity in the worst-case. Nearly thirty years ago, the state-of-the-art MONA tool showed that, despite these theoretical limits, wMSO can be decided efficiently in practice through carefully optimized automata constructions. We revisit wMSO from an algebraic perspective by introducing Extended Regular Expressions with Quantifiers (EREQ). Instead of relying on automata determinization, EREQ employs symbolic derivatives to perform incremental quantifier elimination, providing a compositional and symbolic alternative to classical automata-based approaches. We present a linear-time translation of wMSO into EREQ and a derivative-based decision procedure for EREQ. We prove the correctness of the translation and of the derivative construction in the Lean proof assistant. We implement our approach in Rust and evaluate it on a set of established MONA benchmarks, demonstrating competitive performance with state-of-the-art tools. Our results demonstrate the potential of derivative-based methods, opening new avenues for efficient decision procedures in EREQ.