交替奇偶字自动机

∨让机器选择一条足够的证明路线，∧要求几份证明同时成立。要验证“后缀既满足A又满足B”，可以直接分叉，分别检查两个目标；不必先把它们手工合并成一个积状态。

“同时”是逻辑义务，不要求两台物理处理器真的同时执行。运行树只是记录各份检查如何展开；同一深度所有副本仍读同一输入位置。有限树自动机公理库有限树自动机Finite tree automaton · Bottom-up tree automaton · NFTA有限有序树上的状态汇总支持确定化、空性和语言差判定；可达闭包寻找有限运行，按节点数的动态规划构造最小反例树，并区分树与共享DAG的大小。则是在读取本来就分叉的有限数据，二者的树来自不同地方：这里输入仍是一条无限字，树来自运行中的逻辑义务；那里输入本身就是树，运行在各输入节点赋状态。

存在一条好分支仍然失败 ​

字母表Σ={a,b}，状态Q={q₀,q₁,q₂,q₃}，优先级分别为2、1、0、1。完整转移为

对 $a^{\omega }$，根选q₁会永远留在优先级1，失败；根选q₂∧q₃时，q₂分支在0上成功，但q₃分支在1上失败。因此不存在接受运行树。找出一条q₂好分支，不足以证明输入被接受。

对 $ab{a}^{\omega }$，根消耗第一个a并选q₁；q₁读到第二个字母b后转q₂，随后永留0，得到接受运行树。注意下标：q₀的转移已经消耗第一个字母，q₁检查的是后缀，不可把它重新从第一个a读起。

true与false怎样处理 ​

若δ(q,a)=true，可选空后继，当前义务在此成功结束。若δ(q,a)=false，没有合法运行树能包含这一步。对δ(q,a)=q₁∧true，可以只产生q₁孩子；对q₁∨true，可以选择空孩子。

允许有限成功分支不改变无限分支的奇偶要求。若转移要求q₁，擅自不给孩子就不满足公式，即使“所有无限分支都接受”在空集上为真，这也不是合法运行。

对偶化同时翻转两种选择 ​

标准交替对偶构造把∧、∨互换，true、false互换，并将每个优先级加1。对偶自动机接受原语言的补集。逻辑层面，外层“存在一种安排使所有分支成功”被交换成“对每种安排，都能指出一个失败分支”；奇偶翻转使同一条无限路径的成功与失败互换。

这一定理的无限部分需要接受博弈的确定性，而不只是有限公式的德摩根律。在固定无限字的接受博弈中，存在方选择∨，对手选择∧的一条待检分支，读字位置持续前进；一般输入产生可能无限的博弈图。对最终周期字，位置可压缩成有限的前缀/周期积，再使用有限奇偶博弈理论。

在上面的 $a^{\omega }$ 例子中，对偶根转移为q₁∧(q₂∨q₃)。对偶q₁优先级2，可以一直成功；右侧选对偶q₃，优先级同为2，也成功，因此对偶接受。对 $ab{a}^{\omega }$，强制存在的q₁分支读b后进入对偶q₂，其优先级为1，故对偶拒绝。两个结果都与原判断相反。

仅有∨时，先按布尔恒等式简化公式，再把原子析取作为非确定后继集合。要使用只接受无限运行的普通奇偶自动机接口，true 转到一个新设的偶优先级吸收状态，false 则不给后继；这样有限成功叶与失败步骤都被正确保留。仅有∧时则要求所有指定后继都通过，形成全称模型；若它也统一采用无限运行，可把 true、false 分别接到偶、奇优先级吸收状态。Büchi公理库Büchi 自动机Büchi automaton · Nondeterministic Büchi automaton · NBA在无限字上运行，并以接受状态被无限多次访问作为接受条件的有限状态自动机。的接受条件也可放进交替模型，但本页选择多优先级条件，以便对偶后仍留在同一类表示中。

交替便于按逻辑公式的∧/∨结构组合检查器，也常用作时序逻辑到自动机之间的紧凑中间层。它没有把“存在接受运行”变成实际控制器可随意调用的预言；控制器是否能在线选择输出，还要另外固定环境输入与行动时机。

显式展开运行树可能指数分叉甚至无限增长，不能从单步公式很短推出判定代价很低。算法常共享同层相同义务，或转成有限图上的博弈/非确定自动机；这种共享与去交替需要各自的正确性和规模分析。