ω-正则语言

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

每个 $\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$。若只写 $(a+b{)}^{\ast }a$，那是有限字语言，无法约束无限后缀。

闭包与补集 ​

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

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

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

安全、活性与边界行为 ​

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

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

一个明确的非 $\omega$-正则例子是 $L=\{a^n{b}^n{c}^{\omega }:n\ge 0\}$。若某个有限 Büchi 自动机识别它，把能接受后缀 $c^{\omega }$ 的状态改作有限字接受态，就能识别 $\{u\in \{a,b{\}}^{\ast }:u{c}^{\omega }\in L\}=\{a^n{b}^n:n\ge 0\}$，与后者非正则矛盾。有限状态可记固定余数或有界差，却不能完成这里任意长两段的精确配对。反之，若字面要求每个单字母前缀中的 $a,b$ 数量都相等，在字母表 $\{a,b\}$ 上根本没有合法无限字，得到的是正则的空语言，不能用作非正则反例。

从逻辑到自动机 ​

每个 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$-语言等价。