Büchi 自动机

为什么到达一次不够 ​

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

识别“字母 $a$ 无限多次出现”只需两个状态。令初态 $q_0$ 非接受、$q_a$ 接受，并定义

在输入 $(abb{)}^{\omega }=abbabb\cdots$ 上，运行每三步回到一次 $q_a$，故接受；在 $a{b}^{\omega }=abbb\cdots$ 上只在首字母后访问一次 $q_a$，随后永远留在 $q_0$，故拒绝。到达接受态一次与无限多次访问的差别可以直接从这两条运行复核。

相反，“最终永远只有 $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 搜索不必预先生成全图；可以在探索转移的同时寻找接受环。但算法仍须区分“看见接受节点”和“证明从它可回到接受区域”。

自动机论验证接口 ​

$\omega$-正则语言公理库ω-正则语言Omega-regular language · ω-regular language · Regular language of infinite words由 Büchi 等价自动机形式识别的无限字语言，以及其有限前缀与无限重复结构。可定义为 Büchi 自动机所接受的无限词语言。LTL 模型检查常把否定规格转换为 Büchi 自动机，再与系统取同步积；积中的接受运行代表系统存在一条违反规格的无限路径。

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

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

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