一句话：将符号自动机从有限字推广到 ω-正则语言，统一交替/非确定 Büchi 自动机与 LTL、PSL 的模理论框架。
符号自动机是支持无限字母表（由带可满足性判定的有效布尔代数 𝒜 表示）的有限状态自动机，此前仅适用于有限字上的正则语言。本文借助转移项与符号导数，将其推广到无限字 ω-正则语言：定义模 𝒜 的交替与非确定 Büchi 自动机（ABW𝒜、NBW𝒜）；给出交替消除算法 Æ，可从 ABW𝒜 增量构造 NBW𝒜，并用于构造两个 NBW𝒜 的乘积；定义模 𝒜 的线性时序逻辑 LTL⟨𝒜⟩，推广 Vardi 的 LTL 到交替 Büchi 自动机构造，经 ABW𝒜 得到 NBW𝒜；提出 RLTL⟨𝒜⟩，将 LTL⟨𝒜⟩ 与模 𝒜 的扩展正则表达式结合以推广 PSL，并自然支持 PSL 缺失的 regex complement。最后在 Lean 证明助手中形式化语义并机器验证主要派生定理的正确性。
Symbolic automata are finite state automata that support potentially infinite alphabets, such as the set of rational numbers, generally applied to regular expressions and languages over finite words. In symbolic automata (or automata modulo 𝒜), an alphabet is represented by an effective Boolean algebra 𝒜, supported by a decision procedure for satisfiability. Regular languages over infinite words (so called ω -regular languages) have a rich history paralleling that of regular languages over finite words, with well known applications to model checking via Büchi automata and temporal logics. We generalize symbolic automata to support ω -regular languages via transition terms and symbolic derivatives , bringing together a variety of classic automata and logics in a unified framework that provides all the necessary ingredients to support symbolic model checking modulo 𝒜. In particular, we define: (1) alternating Büchi automata modulo 𝒜( AB W 𝒜 ) as well (non-alternating) nondeterministic Büchi automata modulo 𝒜( NB W 𝒜 );(2) an alternation elimination algorithm Æ that incrementally constructs an NB W 𝒜 from an AB W 𝒜 , and can also be used for constructing the product of two NB W 𝒜 ; (3) a definition of linear temporal logic modulo 𝒜, LTL ⟨𝒜⟩, that generalizes Vardi's construction of alternating Büchi automata from LTL, using (2) to go from LTL modulo 𝒜 to NB W 𝒜 via AB W 𝒜 . Finally, we present RLTL ⟨ 𝒜 ⟩, a combination of LTL ⟨ 𝒜 ⟩ with extended regular expressions modulo 𝒜 that generalizes the Property Specification Language (PSL). Our combination allows regex complement , that is not supported in PSL but can be supported naturally by using transition terms. We formalize the semantics of RLTL ⟨ 𝒜 ⟩ using the Lean proof assistant and formally establish correctness of the main derivation theorem.
@article{VeanesBEZ25,
title = {Symbolic Automata: Omega-Regularity Modulo Theories},
author = {Margus Veanes and Thomas Ball and Gabriel Ebner and Ekaterina Zhuchko},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704838}
}