奇偶自动机

较小的优先级有更强的长期裁决权，但必须无限出现才有资格裁决。一次访问优先级0不会永久赦免后面永不兑现的义务；同样，有限次访问优先级1也不必导致拒绝。

两优先级已经包含熟悉的特例。对Büchi接受集公理库Büchi 自动机Büchi automaton · Nondeterministic Büchi automaton · NBA在无限字上运行，并以接受状态被无限多次访问作为接受条件的有限状态自动机。F，给F优先级0、其他状态1，便要求F无限出现。若希望坏状态B最终不再出现，则给B优先级1、其余状态2：坏状态无限出现时1胜出，只有有限次时最终由2接受。

多个优先级允许交叠的“除非更强事件反复发生，否则仍应满足下一层”条件。它不是把所有偶数状态简单并成一个Büchi集合；奇数与偶数的相对次序参与语义。

三优先级的完整小自动机 ​

令Σ={a,b,c}，状态qₐ、qᵦ、q𝚌分别表示刚读过哪一个字母，初态qᵦ。无论当前在哪，读a转qₐ，读b转qᵦ，读c转q𝚌。优先级为

它接受的性质是：“a无限出现，或者最终永远只有b。”若a无限出现，0决定接受；若a仅有限出现，就需要c也仅有限出现，才能让2成为长期最小值。

状态数有限不表示完整输入最终周期；这里只挑最终周期字，让判定能用一个有限周期核算。

min-even与max-even的翻译 ​

一些文献检查无限出现的最大优先级。不能直接拿同一组数字换“min”为“max”：循环{1,2}在min-even下拒绝，在max-even下接受。

若想等价变换，选一个不小于全部旧优先级的偶数D，令 ${\mathrm{\Omega }}^{\prime }(q)=D-\mathrm{\Omega }(q)$。最大旧优先级对应最小新优先级，且减去偶数保持奇偶性。因此max-even(Ω)与min-even(Ω′)等价。若D为奇数，胜负反而会被翻转。

运行取补不总是语言取补 ​

对确定完整自动机，把每个优先级加1，唯一运行的最小无限优先级奇偶翻转，得到语言补集。完整性重要：原机若在某个字上无运行，加1以后仍无运行，就不会接受这个本应在补集里的字。

非确定模式下，加1只交换每条运行的接受与拒绝。原来是“存在接受运行”，补集应是“所有运行都拒绝”；改号后却变成“存在原来的拒绝运行”。一个字同时有一条好运行和一条坏运行时，两台非确定自动机都可能接受它。

确定与非确定奇偶自动机都能表示全部ω-正则语言公理库ω-正则语言Omega-regular language · ω-regular language · Regular language of infinite words由 Büchi 等价自动机形式识别的无限字语言，以及其有限前缀与无限重复结构。，但转换可能增加状态。能够确定地跟踪输入，是后续控制器综合公理库LTL 控制器综合LTL synthesis · LTL reactive synthesis · LTL realizability固定输入输出回合与环境假设，将LTL确定监控器展开为奇偶博弈，并把获胜位置策略提取为在线控制器。把环境选择与机器状态对应起来的重要接口，不意味着每个非确定Büchi图直接重新染色就能完成确定化。

奇偶条件只由Inf状态集决定。Rabin/Streett条件公理库Rabin 与 Streett 接受条件Rabin acceptance · Streett acceptance · Rabin–Streett duality以有限/无限访问集合对表达存在与全称长期义务，逐项推导Rabin和Streett取补时的坐标交换。把长期要求组织成集合对，Muller条件公理库Muller 自动机与最近出现记录Muller automaton · Latest appearance record · LAR construction用最近出现排列记录无限重复状态集合，将确定Muller接受条件转换为带有限记忆的奇偶条件。直接列允许的Inf集合；它们的表达能力和实际状态/接受条件大小需要分别比较。

给定最终周期输入$u{v}^{\omega }$（其中 $v\ne \epsilon$），在确定自动机上应跟踪“自动机状态、周期内位置”的有限积，直到整个积状态重复，再检查重复段的优先级。仅看输入周期v第一次经过的状态可能仍处在自动机的暂态，不能跳过这一步。