Rabin 与 Streett 接受条件

Rabin可以给运行多条可选的长期接受理由，选中一对兑现即可。Streett则是一张全部都要履行的条件清单；但若某项前件只出现有限次，该项以后便没有无限要求。

强公平/compassion公理库公平性约束Fairness constraint · Weak fairness · Strong fairness以弱公平、强公平等条件排除持续忽略可执行动作的不合理无限执行。常有Streett形式：某动作若无限次使能，就须无限次执行。这里新增的是自动机接受对及其对偶，而不是重新定义强公平。还要注意，一项Streett公平义务不逐个匹配每次请求的响应；有限次发生且最后未回答的请求，可能不违反这份无限频率条件。

同一组集合对不是同一语义 ​

取Q含r₁、g₁、r₂、g₂，使用两对 $E_i=\{r_i\},F_i=\{g_i\}$。每个无限周期中写出的状态都依次重复，计算如下：

因此“Rabin存在一对”并不是把Streett的“每一对”机械替成“某一对”。括号内的逻辑结构也不同：一个是Fin∧Inf，一个是Inf⇒Inf。

逐式求补，为什么要交换坐标 ​

使用命题逻辑公理库命题逻辑Propositional logic · Propositional calculus研究命题如何通过逻辑联结词组合以及公式在真值赋值下何时成立。的德摩根律，

同理 $\mathrm{\neg }S(E_i,F_i{)}_i=R(F_i,E_i{)}_i$。在本页固定约定下，取补同时交换Rabin/Streett与每对的两个坐标，不能只换接受条件名称。

例如单对E={r}、F={g}，运行$g^{\omega }$满足R(E,F)。它不满足补条件S(F,E)，因为g无限而r不无限；若错误使用S(E,F)，前件r不无限，反而也接受。

条件对偶与自动机语言对偶 ​

确定完整自动机每个字有唯一运行，因此上述对偶可直接给出语言补。非确定自动机则不同：设一个字可以选择进入只含g的环，也可以进入只含r的环。第一条运行满足R(E,F)，第二条满足它的运行补S(F,E)；两台非确定机器仍都接受这个字。

语言补要求没有任何原接受运行，涉及存在量词变成全称。确定化或交替对偶能够处理这一层，而单纯变换接受对不能。

无限频率不等于逐请求响应 ​

若状态r只出现一次，此后永远在不含g的中性状态t，Streett(r,g)仍成立，因为Inf(r)为假；响应规格G(r→Fg)却失败。把响应要求编译成Streett前，通常需要增加一个pending状态，记住尚未兑现的请求，让永久欠账变成持续的接受义务。

Büchi公理库Büchi 自动机Büchi automaton · Nondeterministic Büchi automaton · NBA在无限字上运行，并以接受状态被无限多次访问作为接受条件的有限状态自动机。要求Inf(F)，可写成单对Rabin(∅,F)，也可写成Streett(Q,F)。co-Büchi要求Fin(B)，则可用Rabin(B,Q)或Streett(B,∅)表达。这里利用每条无限运行在有限Q中必无限访问Q。

min-even奇偶条件也能写成Rabin：对每个偶数e，取 $E_e=\{q:\mathrm{\Omega }(q)<e\}$、$F_e=\{q:\mathrm{\Omega }(q)=e\}$。存在一对成立，恰好表示某个偶数e无限出现且所有更小优先级只有限出现。

Safra确定化公理库Safra 的 Büchi 确定化Safra determinization · Safra tree construction以命名有序树记录非确定Büchi的接受进展，用持续存在且无限变绿的节点构造确定Rabin自动机。中，一对分别记录“某名字的树节点缺席”与“该节点完成一轮接受进展”。Rabin的Fin/Inf组合因此能表达同一份持续存在的进展证据，而不只是“某些时刻总能找到一个看起来不错的分支”。