Safra 的 Büchi 确定化

步骤1在每个节点标签上复用子集构造公理库DFA–NFA 等价定理DFA–NFA equivalence · Subset construction每个 NFA 都能以当前可能状态集为一个 DFA 状态，从而在有限字上保持语言不变。的后继取并更新；在有限字上，这个集合摘要已经足够，因为读完就能判断终点。Büchi还要证明同一条无限运行反复经过F；每一步“有某个分支刚到F”可能来自互不相接的一批短命分支。

Safra父标签维护候选运行，孩子把已取得一段接受进展的候选分组保存。若孩子们已经覆盖父标签中的全部候选，父节点变绿并清空下层记录，重新开始下一轮进展。绿色是一次完成记录，不是永久接受标志。

同胞去重优先保留较老分组，使候选不能在越来越年轻的组之间无穷逃避。树的深度和节点数有限，再配合稳定名字，才能从反复的局部进展抽出一条真正的无限接受运行。

相同子集序列，却有不同接受结果 ​

取Q={p,f}，初态p，F={f}，转移为

在 $a^{\omega }$ 和 $b^{\omega }$ 上，普通子集序列都是{p}、{p,f}、{p,f}、…。前者可进入f后永留f，因而接受；后者每个进入f的分支都会在下一个b死去，唯一能无限继续的p分支从不接受。因此只给子集{p,f}标“包含F”会把两者误判相同。

逐字计算命名与绿色 ​

本例n=2，名字池1到5。用“1:{p,f} / 2:{f}”表示根及其唯一孩子，星号表示本次绿色。

在 $a^{\omega }$ 上，名字2最终永久存在且无限变绿，Rabin第2对成功。在 $b^{\omega }$ 上，根1一直存在却从不变绿；孩子2、3反复缺席，也不产生绿色，所以没有成功的接受对。

名字池不是给运行分支永久编号。有限池会复用名字，但Rabin的Fin(Eᵢ)要求在某个后缀以后这个名字再也不缺席，因而排除“无限多个不同短命节点恰好都叫i”的伪证据。

两向正确性靠哪些证据 ​

先设某名字v最终一直存在，并在无限多个时刻变绿。两次相邻绿色之间，v的孩子从接触F的候选开始积累，最终覆盖v的整个当前标签。因此后一绿色时刻标签中的每个候选，都可从前一绿色标签沿输入段走来，途中经过F。

不能随意为每段选一条路径后就假定它们首尾相接。应把这些有限候选路径按共同端点连接成分层、有限分支的选择树。每个足够长层次都有可接续见证，每个有限输入区间只产生有限多个候选片段，各深度的可接续选择形成有限分支的前缀树公理库树Tree连通且无圈的有限简单无向图，也就是任意两点之间只有一条简单路径的图。。它有任意深的节点，由该接口中的 König 引理存在无限链；这条链在每个绿色区间都经过F，所以给原机一条Büchi接受运行。

反过来，跟踪一条原机接受运行q₀q₁…。在每棵Safra树中，选择标签仍包含当前q的最深节点。同胞去重只会把它转交给更老的同胞，新的同胞永远添加在右侧。若它无限返回某个持续存在的节点，每次经过F后又从后代回到该节点，便要求该节点不断进行绿色重置。

若当前层次没有这样的无限返回，经过有限次向老同胞迁移后，跟踪点最终落入更深的一条持续分组。这个分析可逐层重复，但稳定树深度至多n，不能无限下沉。因此总有一个最终不再消失的节点无限变绿。Rabin条件恰好把这两个要求同时记录。

为什么稳定树至多n个节点？父标签严格大于孩子标签之并，所以每个节点可选一个只属于自己、没有落入任何孩子的状态。不同同胞分支互不相交，祖先选的状态也不在后代中，这给树节点到Q的单射。

树形、O(n)个名字的分配、同胞次序与标签可以用 $2^{O(n\log n)}$ 种组合编码：每个原状态只需指定它出现链上的最深节点，祖先标签随之确定。输出有O(n)个Rabin对。不能把每个标签都当成完全独立子集，忽略树的不相交与包含约束后再误报这个标准状态界。

给定一棵树及一个字母，用n位集合直接执行后继、同胞去重与重置，可取O(n³)的保守单步时间、O(n²)位标签存储界。完整确定自动机的显式构造还要乘上可达树状态数及字母表大小，不能把“单步是多项式”当成整体确定化多项式。

确定Rabin自动机随后可转换到奇偶接受，为控制器综合提供确定监控器。本页不加入Piterman紧凑重命名的奇偶优化，也不把本算法与同名的Safra分布式终止检测混为一项协议。