一句话：提出带量词正则表达式 EREQ，以符号导数做增量式量词消去，替代自动机确定化并高效判定 wMSO。
弱一元二阶逻辑（wMSO）是刻画正则性质的基础工具，其传统判定过程将公式翻译为有限自动机，虽可判定但最坏情形复杂度为非初等；近三十年前的 MONA 表明，经过精心优化的自动机构造在实践中仍可高效判定该逻辑。本文从代数视角重新审视 wMSO，提出带量词的正则表达式 EREQ，不再依赖自动机确定化，而是以符号导数为核心做增量式量词消去，从而给出一种组合式、符号化的替代方案。作者给出了 wMSO 到 EREQ 的线性时间翻译以及 EREQ 上基于导数的判定过程，并在 Lean 证明助手中机器化验证了翻译与导数构造的正确性。最后用 Rust 实现该方案，在 MONA 的经典基准集上评估，性能与当前最先进工具相当，显示了基于导数的方法在高效判定过程中的潜力。
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.
@article{paperbot3755,
title = {EREQ: Regular Expressions with Quantifiers and Incremental Quantifier Elimination},
author = {Ekaterina Zhuchko and Ian Erik Varatalu and Margus Veanes and Nikolaj Bjørner},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808349}
}