Symbolic automata are finite state automata that support potentially infinite alphabets, such as the set of rational numbers, generally applied to regular expressions/languages over finite words. In symbolic automata (or automata modulo theories), an alphabet is represented by an effective Boolean algebra, supported by a decision procedure for satisfiability. Regular languages over infinite words (so called $\omega$-regular languages) have a rich history paralleling that of regular languages over finite words, with well known applications to model checking via B\"uchi automata and temporal logics. We generalize symbolic automata to support $\omega$-regular languages via symbolic 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 $A$, $NBW_A$. In particular, we define: (1) alternating B\"uchi automata modulo $A$, $ABW_A$ as well (non-alternating) non-deterministic B\"uchi automata modulo $A$, $NBW_A$; (2) an alternation elimination algorithm that incrementally constructs an $NBW_A$ from an $ABW_A$, and can also be used for constructing the product of two $NBW_A$'s; (3) a definition of linear temporal logic (LTL) modulo $A$ that generalizes Vardi's construction of alternating B\"uchi automata from LTL, using (2) to go from LTL modulo $A$ to $NBW_A$ via $ABW_A$. Finally, we present a combination of LTL modulo $A$ with extended regular expressions modulo $A$ 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 symbolic transition terms.

翻译：符号自动机是支持潜在无限字母表（如有理数集）的有限状态自动机，通常应用于有限词上的正则表达式/语言。在符号自动机（或称模理论自动机）中，字母表由有效布尔代数表示，并通过可满足性判定过程支持。无限词上的正则语言（即$ω$-正则语言）与有限词正则语言有着同样悠久的历史，并通过Büchi自动机和时序逻辑在模型检验中具有广泛应用。我们通过符号迁移项和符号导数，将符号自动机推广至支持$ω$-正则语言，在统一框架下融合了多种经典自动机与逻辑，提供了支持模$A$符号模型检验$NBW_A$的全部必要组件。具体而言，我们定义了：(1) 模$A$的交替Büchi自动机$ABW_A$及（非交替的）非确定性Büchi自动机$NBW_A$；(2) 一种交替消除算法，可从$ABW_A$增量式构造$NBW_A$，并可用于构建两个$NBW_A$的乘积；(3) 模$A$的线性时序逻辑（LTL）定义，该定义推广了从LTL构造交替Büchi自动机的Vardi构造方法，通过(2)从模$A$的LTL经由$ABW_A$转换至$NBW_A$。最后，我们提出模$A$的LTL与模$A$的扩展正则表达式的组合，该组合推广了属性规范语言（PSL）。我们的组合支持正则表达式补集运算——该运算在PSL中不受支持，但可通过符号迁移项自然实现。