Büchi 自动机

无限字上的接受条件 ​

非确定性 Büchi 自动机写作

$$\mathcal{A}=(Q,\mathrm{\Sigma },\delta ,Q_0,F),$$

其中 $Q$ 是有限状态集，$\mathrm{\Sigma }$ 是字母表，$Q_0\subseteq Q$ 是初始状态集，$F\subseteq Q$ 是接受状态集，转移函数 $\delta :Q\times \mathrm{\Sigma }\to 2^Q$。

输入是无限字公理库序列Sequence以自然数为定义域的函数。 $w=a_0{a}_1{a}_2\cdots \in {\mathrm{\Sigma }}^{\omega }$。运行是状态序列

$$\rho =q_0{q}_1{q}_2\cdots ,q_0\in Q_0,q_{i+1}\in \delta (q_i,a_i).$$

令 $\mathrm{Inf}(\rho )$ 为运行中无限多次出现的状态集合。运行接受当且仅当

$$\mathrm{Inf}(\rho )\cap F\ne \varnothing .$$

自动机接受 $w$，若存在至少一条接受运行。非确定选择是存在量词，不是给转移随机分配概率。

为什么到达一次不够 ​

若接受条件只要求曾经到达 $F$，自动机只能表达一个有限前缀事件；在无限字上，之后永远违背目标也仍会被接受。Büchi 条件要求接受状态反复出现，从而描述 recurrence。

构造识别“字母 $a$ 无限多次出现”的自动机：状态 $q_a$ 为接受态，读到 $a$ 转入 $q_a$，读到其他字母转入非接受态 $q_b$。输入

$$abbbababb\cdots$$

只要持续出现 $a$，运行就无限次访问 $q_a$；若某个位置后全是 $b$，即使早期访问过 $q_a$，仍不接受。

相反，“最终永远只有 $b$”也可由非确定 Büchi 自动机识别：它猜测最后一个 $a$ 已过去，进入一个只接受 $b$ 的接受循环。若猜得过早又看到 $a$，该运行失败；存在一次正确猜测即可接受。

与有限自动机的差异 ​

NFA公理库非确定性有限自动机Nondeterministic finite automaton · NFA转移可同时给出多个后继状态的有限状态机。在有限字末端查看当前状态是否接受；Büchi 输入没有末端，只能用运行中无限重复的集合定义接受。把 NFA 的“读完后位于 $F$”照搬到无限字没有意义。

两者都只有有限状态，却有不同的确定化性质。每个 NFA 可无指数以外障碍地确定化为 DFA；并非每个 nondeterministic Büchi automaton 都有等价 deterministic Büchi automaton。确定化需要更强的 Rabin、Muller 或 parity 接受条件。

补集也因此更微妙。把 $F$ 换成 $Q\setminus F$ 不会得到语言补：一条运行可能同时无限访问两类状态，而非确定存在量词还需整体对偶化。

lasso 与非空性 ​

有限 Büchi 自动机若语言非空，就存在最终周期字 $u{v}^{\omega }$ 被接受。对应运行由有限 stem 到达一个可达 SCC，再在其中循环，并且循环访问接受状态。

因此非空性可归约为：是否存在从初态可达、且包含接受状态和循环的强连通区域。一个接受状态若可达却没有返回自身的路径，不足以形成无限接受运行。

on-the-fly 搜索不必预先生成全图；可以在探索转移的同时寻找接受环。但算法仍须区分“看见接受节点”和“证明从它可回到接受区域”。

自动机论验证接口 ​

LTL 模型检查常把否定规格转换为 Büchi 自动机，再与系统取同步积。积中的接受运行代表系统存在一条违反规格的无限路径。

系统公平性、generalized Büchi 多接受集合和 transition-based acceptance 会改变判空条件。generalized Büchi 要求每个接受集合都无限访问，不能只命中其中任意一个。

Büchi 自动机只表达 $\omega$-regular 行为。带无界计数匹配或精确数据约束的无限语言可能超出该类，需要 pushdown、counter 或数据自动机。

运行非确定性还会影响“拒绝”的证明：一个字被拒绝，必须说明所有可能运行都没有无限访问接受集，而不是展示一条失败运行。实现判空时通常在自动机状态图上整体搜索接受 SCC，避免逐一枚举无限多运行；把某次启发式选择走入死路当作拒绝结论，会混淆存在接受运行的量词。

参考资料

• J. Richard Büchi, “On a Decision Method in Restricted Second Order Arithmetic,” Proceedings of the International Congress on Logic, Methodology and Philosophy of Science, Stanford University Press, 1962, pp. 1–11。
• Wolfgang Thomas, “Automata on Infinite Objects,” in Handbook of Theoretical Computer Science, Vol. B, Elsevier, 1990, Ch. 4。
• Christel Baier and Joost-Pieter Katoen, Principles of Model Checking, MIT Press, 2008, Ch. 4。