Blog

ω-语言

Let $Σ$ be a set of symbols (not necessarily finite). Following the standard definition from formal language theory, $Σ*$ is the set of all finite words over $Σ$. Every finite word has a length, which is a natural number. Given a word w of length n, w can be viewed as a function from the set $\{0,1,...,n−1\} → Σ$, with the value at i giving the symbol at position i. The infinite words, or ω-words, can likewise be viewed as functions from $\mathbb{N}$ to $Σ$. The set of all infinite words over $Σ$ is denoted $Σ^{\omega}$. The set of all finite and infinite words over $Σ$ is sometimes written $Σ^{\infty}$ or $Σ^{\leq \omega}$. —— Wikipedia

简单来说，给定字母表 $Σ$，由其中的所有无限长的字符串构成的集合是 $Σ^{\omega}$，$Σ$ 上的一个 ω-语言就是这一集合的子集。

对比：$\Sigma^*$ 是字母表 $Σ$ 中的所有有限长字符串。

$$ Σ^{\infty} = \Sigma^* \cup \Sigma^{\omega} $$

ω-语言之上的操作（符）

左连接

$KL$，其中 K 是一个只包含有限长度字符串的语言，L 是一个 ω-语言，表示将 K 左连接到 L 上，即对于每个字符串 $k \in K$ 和 $l \in L$ 都有一个新的字符串 $kl \in KL$。

注意右连接生成的东西（$LK$）没有意义，因为 $L$ 已经是一个 ω-语言，其中的字符串是无限长的，在无限长的字符串后面添加有限长的字符串没有意义。

$^\omega$

$L^ω$ 表示将语言 $L$ 中所有的有限字符串“无限重复”得到的语言。

ω-正规语言

如果一个语言能被写作：

$A^ω$，其中 $A$ 是一个正规语言，且不包含空串，或是：
$A\cdot B$，其中 $A$ 是一个正规语言，B 是一个 ω-正规语言
$A \cup B$，其中 $A$ 和 $B$ 都是 ω-正规语言，注意 $\cup$ 只能进行有限次

则该语言就是一个 ω-正规语言。

ω-正则表达式

我们熟悉的 $\cdot$, $|$¹ 和 $*$ 在 ω-语言对应的正则表达式中仍然是我们熟悉的形式和意义。

但是在 ω-正则表达式中，我们还有一个新的操作符 $^{\omega}$，$E^{\omega}$ 代表 $E$ 应当重复无限多次。

例如，一个用来描述二进制的无限循环小数的正则表达式可以表示为：

$$ (0|1)(0|1)*'.'(0|1)(0|1)*((0|1)*)^{\omega} $$

其中最后的 $((0|1)*)^{\omega}$ 这部分就是一个循环节。

Büchi 自动机²

A deterministic Büchi automaton is a tuple A = (Q,Σ,δ,q0,F) that consists of the following components:
Q is a finite set. The elements of Q are called the states of A.
Σ is a finite set called the alphabet of A.
δ: Q × Σ → Q is a function, called the transition function of A.
q0 is an element of Q, called the initial state of A.
F⊆Q is the acceptance condition. A accepts exactly those runs in which at least one of the infinitely often occurring states is in F.
In a (non-deterministic) Büchi automaton, the transition function δ is replaced with a transition relation Δ that returns a set of states, and the single initial state q0 is replaced by a set I of initial states.
—— Wikipedia

基本上，Büchi 自动机和有穷自动机 “长得一样”，唯一的区别在于：

有穷自动机在输入“耗尽”后，要求停止在某一个接受状态才能接受输入的字符串，而 Büchi 自动机则要求输入的字符串要“无限多次地”进入某个接受状态。

注意：Büchi 自动机的确定性和非确定性版本并不等价，确定性 Büchi 自动机的能力严格弱于非确定性版本，而非确定性 Büchi 自动机能识别所有 ω-正则表达式。

例：$(0|1)*0^\omega$ 能被如下非确定 Büchi 自动机识别，但无法被一个确定性的 Büchi 自动机接受。

ω-正则表达式 $\rightarrow$ Büchi 自动机

Inductively，我们需要考虑 3 种情况：

顶层的 ω-正则表达式形如 $A^ω$。这种情况下，$A$ 必然是一个一般的正则表达式，我们可以将其转换为非确定性有限自动机（NFA）。然后，对这个非确定性有限自动机的所有接受状态，添加一条转换箭头到 A 的初始状态的每一个后继，转换箭头上的字符就是初始状态到这个后继的箭头上的字符，如图：

我只画了一个接受状态，但实际上可以有多个接受状态，每个接受状态参考图上的 $a_0$，连回 entry 的每个后继即可。
顶层的 ω-正则表达式形如 $A\cdot B$。这种情况下，$A$ 必然是一般的正则表达式，我们可以将其转换为非确定性有限自动机（NFA），而 $B$ 必定是一个 ω-正则表达式，可以（递归地）用我们目前描述的算法转化为 Büchi 自动机。然后，将 $A$ 的接受状态降级到一般状态，并直接连接到 $B$ 的初始状态的每个后继即可，如图：
顶层的 ω-正则表达式形如 $A | B$。其中 $A$ 和 $B$ 都是 ω-正则表达式，可以（递归地）用我们目前描述的算法转化为 Büchi 自动机。这种情况下把 $A$ 和 $B$ 的初始状态合并即可。

例子

由 Formal Method 的 example exam 提供，我们的课程中 $|$ 写作 $+$。

$$ a(b^ω + cc*ab^ω) $$

顶层形如 $A\cdot B$，其中 $A \rightarrow a$, $B \rightarrow b^ω + cc*ab^ω$。

我们可以先完成 $a$ 部分的 NFA。

A->unexp

继续展开 $b^ω + cc*ab^ω$，顶层是 $+$。

展开成两部分：

a->unexp12

先考虑 $b^\omega$ 的部分，形如 $A^ω$，其中 $A \rightarrow b$，直接展开即可。

a->b*|a->unexp2

$cc*ab^ω$ 的部分，形如 $AB$，其中 $A \rightarrow cc*a$， $B \rightarrow b^\omega$。

a->b*|a->cc*a->unexp2

最后展开 $b^\omega$。

full-expanded

就得到了最终结果。

Büchi 自动机 $\rightarrow$ ω-正则表达式

从前面的 ω-正则表达式 $\rightarrow$ Büchi 自动机的过程中，我们可以感受到，所有 ω-正则表达式：

可能形如 $A^ω$，对应到 Büchi 自动机的图中就是包含接受状态的循环³。
可能形如 $AB$，对应到 Büchi 自动机的图中就是：
- 有一个自起始状态 $q_{start}$ 开始，不含接受状态 $q_{k}$ 的“路径” $q_{start} \to q_{k}$，其中 $q_{k}$ 是一个接受状态。
- $q_{k}$ 在一个循环³中。
可能形如 $A|B$，对应到 Büchi 自动机的图中就是对 $A$ 和 $B$，都至少存在一个包含接受状态的循环。

我们反过来思考，要把 Büchi 自动机转换回 ω-正则表达式，我们只需：

识别出所有包含接受状态 $q_k$ 的循环，并这个子图转换为正则表达式 $L_k$。
识别所有从起始状态 $q_{start}$ 开始，到达（且不重复经过）$q_k$ 的路径，并这个子图转换为正则表达式 $R_{0k}$。
所求的 ω-正则表达式就是 $\Sigma_k^{0\le k<\text{accept state count}}(R_{0k}\cdot L_{k}^ω)$。