ω-正则语言

无限字语言 ​

对有限字母表 $\mathrm{\Sigma }$，无限字集合记作 ${\mathrm{\Sigma }}^{\omega }$。语言 $L\subseteq {\mathrm{\Sigma }}^{\omega }$ 称为 $\omega$-正则语言，若存在Büchi 自动机公理库Büchi 自动机Büchi automaton · Nondeterministic Büchi automaton · NBA在无限字上运行，并以接受状态被无限多次访问作为接受条件的有限状态自动机。 $\mathcal{A}$ 使

$$L=L_{\omega }(\mathcal{A}).$$

等价刻画还包括 nondeterministic Muller automata、deterministic parity automata 与 monadic second-order logic over $(\mathbb{N},<)$。接受装置不同，但描述的是同一语言类。

有限字正则语言公理库正则语言Regular language能被某个有限自动机识别的形式语言。属于 ${\mathrm{\Sigma }}^{\ast }$，$\omega$-正则语言属于 ${\mathrm{\Sigma }}^{\omega }$。二者共享有限状态本质，却不能把无限字当作“特别长但最终读完”的有限字。

$U{V}^{\omega }$ 结构 ​

每个 $\omega$-正则语言可以写成有限并

$$L=\bigcup _{i=1}^m{U}_i{V}_i^{\omega },$$

其中 $U_i,V_i\subseteq {\mathrm{\Sigma }}^{\ast }$ 是正则语言，且通常排除 $\epsilon \in V_i$。$U_i$ 描述进入长期区域的有限前缀，$V_i^{\omega }$ 描述无限拼接的循环块。

这个表达不是说语言中的每个字从某处起重复同一个固定有限块。$V_i^{\omega }$ 可每轮选择 $V_i$ 中不同的字，只要无限拼接；最终周期字只是在非空性证明中提供一个见证。

例如“$a$ 无限多次出现”可写成

$$(a+b{)}^{\ast }(a(a+b{)}^{\ast }{)}^{\omega },$$

直观上每个无限阶段都要再次包含一个 $a$。若只写 $(a+b{)}^{\ast }a$，那是有限字语言，无法约束无限后缀。

闭包与补集 ​

$\omega$-正则语言对并、交、补闭合。并可用非确定初始选择，交可用积自动机配合适当接受条件；补集需要确定化或专门构造，不能简单翻转 Büchi 接受集合。

投影也保持该类：把扩展字母表上的辅助命题存在量化掉，可由非确定自动机猜测被隐藏分量。这使逻辑公式中的存在二阶变量与自动机非确定性相接。

闭包存在不表示构造代价低。Büchi 补集和 determinization 可能导致显著状态增长；使用“正则类闭合”时仍应报告算法复杂度。

安全、活性与边界行为 ​

许多常见时序性质是 $\omega$-正则的。$G\mathrm{\neg }bad$ 排除含坏前缀的字；$GFgrant$ 要求授权无限出现；$FGstable$ 要求最终永久稳定。

安全语言可由其有限坏前缀刻画，而一般活性语言的任意有限前缀都仍可延伸成满足字。二者的交织仍可能是 $\omega$-正则，但非空与包含算法要处理完整无限接受条件。

“$a$ 与 $b$ 的出现次数始终精确相等”需要无界计数，通常不是 $\omega$-正则。有限状态可记有限余数或有界差，不能精确保存任意大的计数差。

从逻辑到自动机 ​

每个 LTL 公式定义一个 $\omega$-正则语言。公式到 Büchi 自动机的标准转换在公式大小上可能指数增长；反方向，Büchi 可表达的全部 $\omega$-正则语言严格超过 LTL，只用 LTL 不能定义所有有限状态无限字性质。

模型检查时，系统路径标记语言与否定规格语言取交。交集非空给出违反行为；若只检查有限前缀语言，会漏掉“最终永不响应”这类没有单个有限坏点的 liveness 反例。

概率、时间和数据值可把字母表或接受语义扩展出去。称一个性质 $\omega$-正则之前，应明确观察字母表有限，或说明符号自动机怎样有限表示无限数据谓词。

包含与等价问题 ​

语言包含 $L_1\subseteq L_2$ 可转成 $L_1\cap \overline{L_2}=\varnothing$，因而组合补集、交与 Büchi 非空性。语言等价需检查两个方向包含。这个判定链说明闭包性质不仅是分类结论，也给出算法接口；其中补集构造可能成为主要复杂度来源，不能把最后一次线性 SCC 搜索当作整个算法成本。

无限字的有限前缀集合相同也不保证语言相同。“最终全是 $a$”与“$a$ 无限多次”允许的每个有限前缀都可继续，却对许多完整无限字判断不同。只做 prefix sampling 无法判定一般 $\omega$-语言等价。

参考资料

• Wolfgang Thomas, “Automata on Infinite Objects,” in Handbook of Theoretical Computer Science, Vol. B, Elsevier, 1990, Ch. 4。
• Dominique Perrin and Jean-Éric Pin, Infinite Words, Elsevier, 2004, Chs. 1–3。
• Christel Baier and Joost-Pieter Katoen, Principles of Model Checking, MIT Press, 2008, Ch. 4。