Regular Expressions with Quantifiers

Ekaterina Zhuchko

Tallinn University of Technology



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