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 自动机识别。取非接受初态 $q_w$ 与接受态 $q_b$：$q_w$ 在 $a$ 上留在原处，在 $b$ 上可留在原处或转到 $q_b$；$q_b$ 只有 $b$ 自环，没有 $a$ 后继。转入 $q_b$ 就是在猜测最后一个 $a$ 已经过了。

若猜得过早，后面的 $a$ 使这条运行无法继续；若永远不猜，运行一直停在非接受态，也不接受。对只有有限个 $a$ 的字，可以在最后一个 $a$ 后选某个 $b$ 转入接受环；对有无限个 $a$ 的字，任何有限时刻的猜测都会失败。存在量词正是这次构造的关键。

与有限自动机的差异 ​

NFA公理库非确定性有限自动机Nondeterministic finite automaton · NFA以状态集合保留多条候选运行，并在至少一条运行接受时接受输入的有限状态模型。在有限字末端查看当前状态是否接受；Büchi 输入没有末端，只能用运行中无限重复的集合定义接受。把 NFA 的“读完后位于 $F$”照搬到无限字没有意义。

两者都只有有限状态，却有不同的确定化性质。每个NFA都能确定化为DFA；非确定Büchi却未必有等价的确定Büchi表示。允许更一般的Rabin条件公理库Rabin 与 Streett 接受条件Rabin acceptance · Streett acceptance · Rabin–Streett duality以有限/无限访问集合对表达存在与全称长期义务，逐项推导Rabin和Streett取补时的坐标交换。或奇偶条件公理库奇偶自动机Parity automaton · Deterministic parity automaton用无限重复的最小优先级决定接受，明确确定/非确定量词、有限前缀和min-even约定。后，才能为全部ω-正则语言提供确定表示。

Safra构造公理库Safra 的 Büchi 确定化Safra determinization · Safra tree construction以命名有序树记录非确定Büchi的接受进展，用持续存在且无限变绿的节点构造确定Rabin自动机。给出具体机制：可达子集之外再保存有序分组、稳定名字与绿色进展。一棵树上同一个名字最终持续存在且无限变绿，才能把分散的接受迹象串成同一条成功运行；仅要求每轮子集碰到接受集不足以做到这一点。

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

lasso 与非空性 ​

有限 Büchi 自动机若语言非空，就存在最终周期字 $u{v}^{\omega }$ 被接受。对应运行由有限 stem 到达一个可达强连通分量公理库强连通分量算法Strongly connected components algorithm在线性时间内把有向图划分为互相可达的极大顶点集合。（SCC），再在其中循环，并且循环访问接受状态。

因此非空性可归约为：是否存在从初态可达、且包含接受状态和循环的强连通区域。对于只有一个顶点的 SCC，必须另检查有自环；“顶点自身经零步可达”不提供消耗无限输入的循环。对于包含至少两个顶点的 SCC，可从接受点出发经过其他顶点再返回，得到非空闭合游走，其标签就是非空周期 $v$。

这里证明的是至少存在一个最终周期见证，不是说全部接受字都最终周期，也不是说所有接受运行最终只沿一个简单环。有限图允许每次走环时作不同选择，仍可产生非周期输入。

这个判据的必要性可以直接从有限性推出：接受运行中至少有一个接受顶点出现无限次，取两次不同位置的出现便得到非空回返。充分性则由初始路径加上述闭合游走构造：重复游走会无限次访问接受点，其边标签构成最终周期输入。两向构造都使用实际的正长度路径，不能用零步自达替代。

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

从接受运行到对抗策略 ​

自动机的非确定接受只要求存在一条运行。有限 Büchi 博弈公理库安全博弈与反应式综合Safety game · Reactive synthesis · 安全游戏 · 获胜区域 · Controllable predecessor从安全闭包进入有限Büchi博弈，用嵌套吸引域计算反复到达目标的获胜区域，并构造双方位置策略。则把顶点分给控制器和环境，要求存在一个控制策略，使环境的每种选择都无限次访问目标。一个包含接受点的可达环并不足以满足这个量词：环境可能在环上的自己顶点选择永远离开。该页用两层吸引域删除失败区域，以八状态例子逐轮计算，并用保留区的返回秩与删除层的下降秩分别证明双方策略。

自动机论验证接口 ​

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

请求系统的完整积图公理库自动机论模型检查Automata-theoretic model checking · Automata-based LTL model checking将系统与否定规格 Büchi 自动机同步取积，并以可达接受环判定 LTL 违反行为。把这个接口落实为五点七边：否定响应规格的两态自动机在初始请求上分成两支，一个继续等待，另一个进入接受监控。积顶点使用读完当前系统标签后的自动机状态，所以初始积集合须先消费初态标签；本页标准运行中的 $q_0$ 仍是读字前初态，两者只是下标不同。

系统公平性、generalized Büchi 多接受集合和 transition-based acceptance 会改变判空条件。广义 Büchi 要求每个接受集合都无限访问，因而必须在同一个可达循环 SCC 中命中每个集合。可通过强连通路径把各集合代表串成闭合游走，但不一定能找到一条同时访问所有集合的简单环。没有任何接受集合时仍要存在无限运行，有限死路不能作为见证。

对显式普通 Büchi 图的 $N$ 个顶点与 $E$ 条边，SCC 判空为 $O(N+E)$ 时间，物化图存储为 $O(N+E)$。广义版本还需计入接受集成员记录的读入成本；若有 $m$ 个集合和总计 $B$ 条成员记录，可在 SCC 结果上以 $O(N+E+m+B)$ 时间汇总。

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

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