公平性约束

间歇使能区分强弱 ​

两个进程竞争锁。进程 P 的 enter 在锁空闲时使能，但进程 Q 每次释放后立刻重新获取，使 P 的动作只在离散瞬间反复使能，从未持续使能。

这条无限执行不违反 P 的弱公平，因为不存在一个后缀让 enter_P 一直使能；它违反强公平，因为 enter_P 无限多次获得机会却从不执行。

若调度器从某时刻起始终把 P 留在 runnable 队列却从不调度，弱公平已经足以排除。例子必须跟踪 enabled 状态，而不能只统计某动作“看起来等了很久”。

公平不是模型自动属性 ​

异步模型允许任意有限延迟，往往也允许某进程永远不被调度。仅因为所有进程在现实操作系统中“通常会运行”，不能在证明里无声删除饥饿路径。

可采纳执行公理库可容许执行Admissible execution满足给定调度、公平性和故障模型约束的执行。会同时约束故障数、消息交付和调度公平。公平性应写成环境或调度器假设；系统算法的保证通常是“对所有满足这些假设的执行”。

若实现运行在没有相应调度保证的平台上，模型内活性证明不适用。相反，安全性质通常对删除路径保持：即使不假设公平，互斥也应对所有执行成立。

justice、compassion 与状态集合 ​

符号模型检查常用 fairness sets。justice 条件给出状态集合 $J_i$，要求路径无限多次访问每个 $J_i$。compassion 对 $(P_i,Q_i)$ 要求：若路径无限多次访问 $P_i$，也必须无限多次访问 $Q_i$。

动作公平可通过增加“动作刚执行”命题编码成状态公平。这个转换会扩展状态，且 enabled/taken 的标记必须准确；漏标使能状态会把不公平路径误判为公平。

多个公平条件取合取。条件越多，保留路径越少，活性越容易成立，也越可能依赖不现实假设。公平假设应最小化并单独审查。

与安全—活性的关系 ​

安全—活性公理库安全性与活性Safety and liveness · Correctness properties把系统正确性分为坏事永不发生与好事最终发生两类性质。分解说明公平性本身通常是对无限行为的 liveness 型限制：任意有限前缀还可以通过未来调度修复，无法仅凭一个有限坏前缀判定永远不公平。

加入公平性可能使“每个请求最终响应”成立，但不会修复“两个进程同时进入临界区”的安全反例。后者一旦发生，即使未来调度完美公平也无法撤销。

公平也不等于概率一事件。随机调度下某动作以概率 $1$ 最终执行，仍可能存在概率零的不公平路径；普通公平语义是集合上的全称筛选，不带概率测度。

验证与反例边界 ​

检查公平前提下的活性时，真正反例必须是合法初始无限路径，满足所有公平假设，同时违反待验证性质。一个持续违反 fairness set 的循环说明该路径不公平，会被前提排除；它不是公平前提下的性质反例。算法必须同时检查否定规格的接受条件和公平条件，单找任意 SCC 不够。

公平性若写得过强，模型检查会“证明”实际上做不到的响应。诊断报告应显示反例是否因不公平被排除，并把 fairness assumptions 与系统 guarantees 分栏呈现。

共享请求系统：弱公平何时可换成 justice ​

取自动机论模型检查公理库自动机论模型检查Automata-theoretic model checking · Automata-based LTL model checking将系统与否定规格 Büchi 自动机同步取积，并以可达接受环判定 LTL 违反行为。中的系统：$r\to w$、$w\to w$、$w\to g$、$g\to r$，初态为 $r$，仅 $r$ 标记 request，仅 $g$ 标记 grant。给 $w\to g$ 命名为动作 serve，其使能谓词恰在 $w$ 成立。taken(serve) 表示所执行的边是 $w\to g$；它不是当前状态上的 grant 命题，二者的等价关系需要从整个路径证明。

系统的无限路径只有两类行为。若 $g$ 从未出现，初态 $r$ 后必永留 $w$；若 $g$ 出现正的有限次，最后一次离开 $g$ 后经过 $r$ 到 $w$，此后必永留 $w$。两种情况都使 serve 持续使能却再不执行，因此违反弱公平。若 $g$ 出现无限次，每次进入 $g$ 都执行 serve，所以 serve 无限执行，弱公平成立。由此，对本系统全部初始无限路径，serve 弱公平与 $GFgrant$ 等价。

现在考虑响应性质 $G(request\to Fgrant)$。无公平限制时的反例 $r{w}^{\omega }$ 被弱公平排除；其余路径无限到达 $g$，从任一请求位置向后都能找到授权，所以在公平路径上性质成立。这是针对给定模型的证明，不是把动作弱公平普遍定义为“授权无限出现”。

一般系统中，serve 可能最终不再使能，此时弱公平的前件为假，即使 grant 从此永不出现也不违反公平；grant 也可能由另一个动作产生。因此用状态集合 $\{grant\}$ 代替 enabled/taken 关系通常会改变允许路径。若还加入绕路 $w\to h\to w$，并使 serve 在 $h$ 禁用，则 $r(wh{)}^{\omega }$ 中 serve 间歇地无限使能、从未执行：它满足弱公平却违反强公平。

多个接受集合必须在同一个循环区域兑现 ​

在上述三态系统中，弱公平已证明可写成 justice $GFgrant$，因此可以在否定规格的积上同时要求两个集合：$F_A=\{R_b,W_b\}$ 记录违反响应规格，$F_J=\{G_z\}$ 记录无限授权。它们是合取要求；取并集只要求无限访问其中任意一个集合，会接受错误路径。

积的三个 SCC 是 $\{R_z,W_z,G_z\}$、$\{R_b\}$ 和 $\{W_b\}$。第一个命中 $F_J$ 却不命中 $F_A$，后两个命中 $F_A$ 却不命中 $F_J$，故没有公平反例。公平筛选发生在无限接受条件上，并没有删除某条单步系统边。

更一般地，广义Büchi 接受条件公理库Büchi 自动机Büchi automaton · Nondeterministic Büchi automaton · NBA在无限字上运行，并以接受状态被无限多次访问作为接受条件的有限状态自动机。要求同一个可达且含正长度循环的强连通分量公理库强连通分量算法Strongly connected components algorithm在线性时间内把有向图划分为互相可达的极大顶点集合。（SCC）命中每个接受集。强连通性保证可以在分量内依次访问各集合的代表并返回入口，形成一个可无限重复的闭合游走。该游走不一定是简单环：例如两只环共用一个中心，一个接受集只在左环，另一个只在右环，就需要重复中心来轮流访问二者。分别在两个不相通的 SCC 命中义务不能拼成一个无限证书。

一般强公平的 $GFenabled(a)\Rightarrow GFtaken(a)$ 属于Streett集合对条件公理库Rabin 与 Streett 接受条件Rabin acceptance · Streett acceptance · Rabin–Streett duality以有限/无限访问集合对表达存在与全称长期义务，逐项推导Rabin和Streett取补时的坐标交换。：前件无限出现才触发后件义务。它不能直接作为一个“每个集合都要命中”的justice条件处理。取补得到某一对“前件无限而后件有限”的Rabin违例时，还要核对该页规定的集合坐标交换。

这类长期频率条件也不同于每次请求都须响应：一个请求只出现一次却永远得不到服务，可能仍满足相应Streett条件。实际验证必须先确定待表达的是动作公平还是逐请求义务，再选择自动机与判空算法。

选择公平对象 ​

公平性可以施加在进程、动作或具体转移上，三者不总等价。一个进程被无限调度，仍可能每次只执行不相关动作；一个动作标签在多个组件中共享，也无法说明究竟哪个实例获服务。证明饥饿自由时，应把公平对象细化到真正承担进展义务的 transition instance，并明确使能谓词在何种原子状态上求值。