Muller 自动机与最近出现记录

只有有限次出现的状态，最终会被反复出现的状态挤到排列后面。若无限出现集合有k个元素，过了一段有限前缀后，它们恰占据前k格，后面的格子不再动。

在这些活跃格中，最久没出现的那个元素也必须再次出现，于是位置k*会被无限次命中。更深的位置只命中有限次，更浅位置的命中又被赋予更大的优先级。因此长期最小优先级正好来自整块Inf集合，检查这块集合是否在F即可。

LAR不是猜测“最后一次坏事已经过去”。它确定地更新最近顺序，让无限次命中的最深位置在运行极限中提供证据。额外记忆正是集合条件转换为奇偶条件公理库奇偶自动机Parity automaton · Deterministic parity automaton用无限重复的最小优先级决定接受，明确确定/非确定量词、有限前缀和min-even约定。所付出的代价。

三状态接受族 ​

令Q={a,b,c}，字母也是a、b、c，任何状态读字母x都转到状态x。取

所以$(ab{)}^{\omega }$与$(bc{)}^{\omega }$接受，$(abc{)}^{\omega }$拒绝；$a^{\omega }$也拒绝，因为{a}不在F。这里状态名与字母名相同只是便于手算，定义本身并不要求二者相同。

从初始排列abc计算$(bc{)}^{\omega }$：

之后最后两行反复，最小无限优先级是2，接受。第二行曾输出更小的奇数1，但它只出现有限次，不改变最终结论。

对$(ab{)}^{\omega }$，排列最终在abc、bac之间交替，每次命中第2位并输出2。对$(abc{)}^{\omega }$，在每个状态都反复出现后，每次命中第3位，前缀集始终为{a,b,c}，输出1并拒绝。三种判断与原Muller条件一致。

转换正确性的两个关键步骤 ​

设I=Inf(ρ)，k*=|I|。Q有限，所以所有Q∖I元素都有最后一次出现；再等I中的每个元素至少出现一次，排列前k*格便恰好是I，且以后保持这个集合。

位置k必须无限次被命中。若从某刻起再也不命中它，移到前面的都来自更浅位置，第k格的元素就一直停在那里、再未出现，违背它属于I。因此最大无限命中位置恰为k*。

每次足够晚命中k时，Sₖ=I；更深命中只有有限次，更浅命中的两种优先级都大于k*对应的两种优先级。于是最小无限优先级偶，当且仅当I∈F。这完成逐运行等价；确定机器的唯一运行也就保持整个语言。

初始排列与空集合 ​

初始排列中尚未真正见过的状态先后次序没有语义意义，但只影响有限暂态。上述证明等到所有无限出现状态都访问过一次，自动消去这份任意性，因此不需要给每个初始排列另猜一套接受条件。

有限非空Q中的无限运行总有I≠∅。把∅列入或移出F不会影响语言；不过死路仍不是无限运行，不能借“允许空Inf”让一条提前停止的路径接受。

若只显式存(π,c)，状态数至多 $2n\cdot n!$，优先级范围0到2n−1；原状态已经由π首项确定，不必额外再乘n。用数组移动元素和构造Sₖ需O(n)操作，检查Sₖ∈F的成本另计。

若F以显式集合列表输入，其本身可含2ⁿ个成员。可以用位向量和索引表加速成员测试，但不能只报告n!排列，而把读取、保存接受族的成本当作零。若F用逻辑公式或其他紧凑表示，成员判断也须按该表示分析。

Büchi公理库Büchi 自动机Büchi automaton · Nondeterministic Büchi automaton · NBA在无限字上运行，并以接受状态被无限多次访问作为接受条件的有限状态自动机。接受只问Inf是否碰到F；Muller能对完整Inf集合提出更细的允许/禁止组合。LAR表明这些组合仍可由有限优先级机器实现，但一般需要增加记忆，不能保证在原图上仅换颜色就足够。

单元终点会要求用同一个最终周期字核对原接受族与LAR优先级，检查“有限前缀产生的奇数”和“无限反复产生的奇数”是否被正确区分。