【模型检测学习笔记】6：线性时序性质(Linear-time Properties)

为方便，线性时序性质（linear-time properties）后续均简称LT性质。

在系统分析中，描述线性时序行为（linear-time behavior）可以是基于动作的（action-based approach），也可以是基于状态的（state-based approach），本章主要学习的是基于状态的（但在学习公平性时用动作描述），也就可以在TS中刻意忽略转移过程中的具体动作，而只考虑前后状态。

1 前置知识

1.1 路径(path)与状态图

TS可以表示成状态图(V,E)(V,E)(V,E)的形式，其中状态就是其结点V=SV=SV=S，边就是状态到状态的转移关系E={(s,s′)∈S×S′∣s′∈Post(s)}E=\{(s,s') \in S \times S' \ | \ s' \in Post(s)\}E={(s,s′)∈S×S′ ∣ s′∈Post(s)}。这里Post(s)Post(s)Post(s)是从状态sss的所有直接后继状态的集合，相关内容见笔记3中的定义。

约定，将无限长的path记为π\piπ等小写字母，而将有限长的path记为π^\hat{\pi}π^等头戴^的小写字母。从状态sss出发的所有path记为Paths(s)Paths(s)Paths(s)，所有有限长的path记为Pathsfin(s)Paths_{fin}(s)Pathsfin(s)。

1.2 迹(traces)

一个TS系统可以用一系列trace来描述其行为轨迹，具体是，迹被定义为一串接连到达的状态sis_isi的标签函数L(si)L(s_i)L(si)的序列。因为L∈2APL \in 2^{AP}L∈2AP，所以迹上的每个元素也是APAPAP的子集。

例如，状态图上的一系列接连的转移是一个path：
s0⟶α1s1⟶α2s2...s_0 \stackrel{\alpha_1}{\longrightarrow} s_1 \stackrel{\alpha_2}{\longrightarrow} s_2 ...s0⟶α1s1⟶α2s2...

这可以简记为：
s0s1s2...s_0 s_1 s_2...s0s1s2...

对其中每个结点对应的状态用标签函数映射到2AP2^{AP}2AP上，得到的就是一个迹(trace)：
L(s0)L(s1)L(s2)...L(s_0) L(s_1) L(s_2) ...L(s0)L(s1)L(s2)...

具体地，这个迹可能是这样的形式：
{a}{a,b}ϕ...\{a\} \ \{a,b\} \ \phi \ ...{a} {a,b} ϕ ...

其中a,b∈APa,b \in APa,b∈AP。

约定，用trace()trace()trace()表示对path（如π\piπ），或者path的集合中的每个元素（如π∈Π\pi \in \Piπ∈Π）取迹。对每个path而言，无限长的path得到无限长的迹，有限长的path得到有限长的迹。

从path集合得到trace集合：
trace(Π)={trace(π)∣π∈Π}trace(\Pi)=\{trace(\pi) \ | \ \pi \in \Pi\}trace(Π)={trace(π) ∣ π∈Π}

约定，用Traces()Traces()Traces()表示从状态（如sss），或者从TS中的每个初始状态（如s∈IfromTSs \in I \ from \ TSs∈I from TS）出发的所有迹的集合。用Tracesfin()Traces_{fin}()Tracesfin()表示只取有限长度的那些迹组成集合。

从sss出发的所有path的trace：
Traces(s)=trace(Paths(s))Traces(s)=trace(Paths(s))Traces(s)=trace(Paths(s))
从TS的初始状态出发的所有path的trace：
Traces(TS)=⋃s∈ITraces(s)Traces(TS)=\bigcup_{s \in I} Traces(s)Traces(TS)=s∈I⋃Traces(s)
从sss出发的所有有限长path的trace：
Tracesfin(s)=trace(Pathsfin(s))Traces_{fin}(s)=trace(Paths_{fin}(s))Tracesfin(s)=trace(Pathsfin(s))
从TS的初始状态出发的所有有限长path的trace：
Tracesfin(TS)=⋃s∈ITracesfin(s)Traces_{fin}(TS)=\bigcup_{s \in I} Traces_{fin}(s)Tracesfin(TS)=s∈I⋃Tracesfin(s)

1.3 无限字和有限字

举例来说，如原子命题集合AP={a,b}AP=\{a,b\}AP={a,b}，则2AP2^{AP}2AP是APAPAP的幂集：
2AP={ϕ,{a},{b},{a,b}}2^{AP}=\{\phi,\{a\},\{b\},\{a,b\}\}2AP={ϕ,{a},{b},{a,b}}

那么(2AP)ω(2^{AP})^{\omega}(2AP)ω表示以2AP2^{AP}2AP中元素为字母构成的所有无限长的字的集合，称为2AP2^{AP}2AP上的无限字集合。也就是说，这个集合是这样一种形式：
(2AP)ω={ϕ{b}{a}...,{a,b}{a,b}{a}...,...}\begin{aligned} (2^{AP})^{\omega} = & \{ \\ & \phi \ \{b\} \ \{a\} \ ... \ ,\\ & \{a,b\} \ \{a,b\} \ \{a\} \ ... \ ,\\ & ... \\ & \} \\ \end{aligned} (2AP)ω={ϕ {b} {a} ... ,{a,b} {a,b} {a} ... ,...}

同理可定义2AP2^{AP}2AP上的有限字集合，其形式如下：
(2AP)∗={ϕ,{a},{b},{a,b},ϕϕ,ϕ{a},...}\begin{aligned} (2^{AP})^{*} = & \{ \\ & \phi \ ,\\ & \{a\} \ ,\\ & \{b\} \ ,\\ & \{a,b\} \ ,\\ & \phi \ \phi \ ,\\ & \phi \ \{a\} \ ,\\ & ... \\ & \} \\ \end{aligned} (2AP)∗={ϕ ,{a} ,{b} ,{a,b} ,ϕ ϕ ,ϕ {a} ,...}

注意，无限字和无限字集合不是一个概念，无限字集合中的每个元素都是无限字，无限字指用无限多个字母组成的序列，在这里，幂集2AP2^{AP}2AP中的每个元素都是一个字母（例如{a,b}\{a,b\}{a,b}）。

无限字集合和有限字集合中的元素数目都是无限多的。

2 LT性质

以两进程并发，并带有一个互斥信号量控制的例子为例：

它们并发后转为TS，结果如下：

每个状态都是由之前两PG的Loc和互斥信号量y的取值组成（见笔记5PG向TS的转换），其中红色和蓝色分别表示两个进程的Loc，n表示在非临界区，w表示想要进入临界区，c表示正处在临界区。

2.1 一般描述

LT性质可用无限字集合的子集来表示，即P⊆(2AP)ωP \subseteq (2^{AP})^{\omega}P⊆(2AP)ω。

一个TS满足P，记为TS⊨PTS \models PTS⊨P，当且仅当从其初始状态出发的所有trace都在PPP中，即Traces(TS)⊆PTraces(TS) \subseteq PTraces(TS)⊆P。

例如，取原子命题集合AP={crit1,crit2}AP=\{crit_1,crit_2\}AP={crit1,crit2}，这之中的两个命题分别表示两进程P1P1P1和P2P2P2处在访问临界资源状态。则【永远至多只有一个进程进入临界资源】这一LT性质可表示为：
Pmutex=无限字A0A1A2..的集合,保证对所有i≥0有{crit1,crit2}⊈AiP_{mutex}=无限字A_0A_1A_2..的集合,保证对所有i \geq0有\{crit_1,crit_2\} \nsubseteq A_iPmutex=无限字A0A1A2..的集合,保证对所有i≥0有{crit1,crit2}⊈Ai

也就是说，像{crit1}{crit2}{crit1}...\{crit_1\} \ \{crit_2\} \ \{crit_1\} ...{crit1} {crit2} {crit1}...这样的trace是合法的，但是不会在trace中出现{crit1,crit2}\{crit_1,crit_2\}{crit1,crit2}这一项，见上一张图中没有同时存在c1和c2的状态。

2.2 无饥饿性(starvation freedom)

无饥饿性（PnostarveP_{nostarve}Pnostarve）表示，一个想访问临界资源的进程最终一定能访问到临界资源。

在上面的例子中，取原子命题AP={wait1,crit1,wait2,crit2}AP=\{wait_1,crit_1,wait_2,crit_2\}AP={wait1,crit1,wait2,crit2}，注意这里和2.1中的例子的取法不一样，因为那里只关注“处在临界区”，而这里还要关注“想要进入临界区”。则“无饥饿性”可以表达为满足如下条件的无限字A0A1A2..A_0A_1A_2..A0A1A2..的集合PnostarveP_{nostarve}Pnostarve：
(∃∞j.waiti∈Aj)⇒(∃∞j.criti∈Aj)foreachi∈{1,2}(\exists^\infty j. wait_i \in A_j)\Rightarrow (\exists^\infty j. crit_i \in A_j) \ for \ each \ i\in\{1,2\}(∃∞j.waiti∈Aj)⇒(∃∞j.criti∈Aj) for each i∈{1,2}

也就是说，对每个进程i，若无限经常次存在j，使得waiti∈Ajwait_i \in A_jwaiti∈Aj，那么就无限经常次存在j，使得criti∈Ajcrit_i \in A_jcriti∈Aj。也即“无限经常次想要最终会导致无限经常次获得”，这就是无饥饿性。

前面的例子不满足无饥饿性，如下图中标注的无限trace，进程2无限经常此waitwaitwait，却始终无法进入临界区：

2.3 两TS的trace集合与LT性质的关系

假设TSTSTS和TS′TS'TS′是同一APAPAP上的两transition system，那么，其trace集合可能特别地存在包含关系和等价关系。

包含关系意在说明一系统扩张了另一系统的实现，而等价关系则指出两确定性的系统是一致的。

2.3.1 包含关系

Traces(TS)⊆Traces(TS′)Traces(TS) \subseteq Traces(TS')Traces(TS)⊆Traces(TS′)当且仅当对任意LT性质P，有TS′⊨P→TS⊨PTS' \models P \to TS \models PTS′⊨P→TS⊨P。

这可以由TS满足LT性质的定义直观得到，即右边意为Traces(TS′)⊆P→Traces(TS)⊆PTraces(TS') \subseteq P \to Traces(TS) \subseteq PTraces(TS′)⊆P→Traces(TS)⊆P。

2.3.2 等价关系

Traces(TS)=Traces(TS′)Traces(TS)=Traces(TS')Traces(TS)=Traces(TS′)当且仅当它们总是满足相同的LT性质。也即对任意LT性质P，有TS′⊨P↔TS⊨PTS' \models P \leftrightarrow TS \models PTS′⊨P↔TS⊨P（双蕴含）。

这可由双向的2.3.1得到，两个trace集合互相包含，也就是等价的。

2.4 不变性(invariants)

不变性（PinvP_{inv}Pinv）表示，TS的所有可达状态都满足某一不变性条件Φ\PhiΦ。

用LT性质的形式表达，不变性可表示为这样的无限字集合，每个无限字上的每个字母（也即APAPAP的子集）总是满足一不变性条件（实为命题逻辑公式）Φ\PhiΦ：
Pinv={A0A1A2..∈(2AP)ω∣∀j≥0.Aj⊨Φ}P_{inv}=\{A_0A_1A_2.. \in (2^{AP})^{\omega} \ | \ \forall j \geq 0. \ A_j \models \Phi\}Pinv={A0A1A2..∈(2AP)ω ∣ ∀j≥0. Aj⊨Φ}

说TS⊨PinvTS \models P_{inv}TS⊨Pinv，即TS满足某一不变性性质PinvP_{inv}Pinv，实则是和下面三个命题是等价的：

对TS的所有无限长的路径π\piπ，有trace(π)∈Pinvtrace(\pi) \in P_{inv}trace(π)∈Pinv
对TS的所有路径上的所有状态sss，有L(s)⊨ΦL(s) \models \PhiL(s)⊨Φ
对TS的所有可达状态s∈Reach(TS)s \in Reach(TS)s∈Reach(TS)，有L(s)⊨ΦL(s) \models \PhiL(s)⊨Φ

显然，不变性性质只有一个不变性条件Φ\PhiΦ是可定制的，也就是一个Φ\PhiΦ即可决定整个不变性性质。对不变性的检查只需搜索（如DFS）整个TS的图结构，看看每个结点状态是不是都满足Φ\PhiΦ（这是由上面的命题3知道的），而不需要真的找出所有的无限path。

2.5 安全性(safety properties)

2.5.1 简述

仅在和security properties一词不会发生混淆的语境，可将其直接翻译成安全性。

安全性（PsafeP_{safe}Psafe）是不变性的超集，也就是说所有的不变性都属于安全性。和不变性不同的那部分在于，安全性不一定都能像不变性那样通过检查所有的可达状态来检验，而往往是基于有限的path片段的约束，安全性涉及一个坏前缀（bad prefix）的概念。

若将安全性表示为LT性质PsafeP_{safe}Psafe，它一定是一个无限字的集合，那么从无限字全集(2AP)ω(2^{AP})^{\omega}(2AP)ω中将其去掉，所得到的一系列无限字即σ∈(2AP)ω∖Psafe\sigma \in (2^{AP})^{\omega} \setminus P_{safe}σ∈(2AP)ω∖Psafe，每个无限字σ\sigmaσ的所有前缀σ^\hat{\sigma}σ^都是坏前缀（是有限字），从这些坏前缀拓展出的所有无限字都不在安全性中：
Psafe∩{σ′∈(2AP)ω∣σ^是σ′的前缀}=ϕP_{safe} \cap \{ \sigma' \in (2^{AP})^{\omega} \ | \ \hat{\sigma}是\sigma'的前缀\} = \phiPsafe∩{σ′∈(2AP)ω ∣ σ^是σ′的前缀}=ϕ

安全性的形式定义比较复杂，但是其表达的意义是很直观的。也就是说系统表示成TS以后，其一系列执行的状态片段里都不能出现特定形式的片段，这个“特定形式”也就是用坏前缀σ^\hat{\sigma}σ^来表达的安全性属性。

因为坏前缀的形式可以多种多样，很多时候需要用繁杂的命题来书写约束，而没办法写成像2.4中表达不变性那样的单纯的命题逻辑公式。

安全性PsafetyP_{safety}Psafety的所有坏前缀组成的集合记为BadPref(Psafety)BadPref(P_{safety})BadPref(Psafety)，对每个坏前缀总能找到一个最小坏前缀，从最小坏前缀扩展出的所有有限字都是坏前缀。

2.5.2 例子

例如，交通灯的【红灯紧跟在黄灯出现以后】，写为：
对所有无限字σ=A0A1..,(red∈Ai)→((i>0)and(yellow∈Ai−1))对所有无限字\sigma = A_0A_1.., \ (red \in A_i) \to ((i>0) \ and \ (yellow \in A_{i-1}))对所有无限字σ=A0A1.., (red∈Ai)→((i>0) and (yellow∈Ai−1))

又如，饮料机的“在任一时刻iii，有效投币总量不少于已分发的总饮料数”，写为：
对所有无限字σ=A0A1..,∣{0≤j≤i∣pay∈Aj}∣≥∣{0≤j≤i∣drink∈Aj}∣对所有无限字\sigma = A_0A_1.., \ |\{0\leq j \leq i \ | \ pay \in A_j\}|\geq|\{0\leq j \leq i \ | \ drink \in A_j\}|对所有无限字σ=A0A1.., ∣{0≤j≤i ∣ pay∈Aj}∣≥∣{0≤j≤i ∣ drink∈Aj}∣

在交通灯的例子中，如"ϕϕ{red}\phi \ \phi \ \{red\}ϕ ϕ {red}“和”{red}\{red\}{red}“都是最小坏前缀，而”{yellow}{yellow}{red}{red}ϕ{red}\{yellow\} \ \{yellow\} \ \{red\} \ \{red\} \ \phi \ \{red\}{yellow} {yellow} {red} {red} ϕ {red}“虽是一个坏前缀，但不是最小坏前缀，因为它还可以缩小为”{yellow}{yellow}{red}{red}\{yellow\} \ \{yellow\} \ \{red\} \ \{red\}{yellow} {yellow} {red} {red}"。

2.5.3 安全性的有限trace集表示

一个TS满足某安全性PsafeP_{safe}Psafe，当且仅当TS的有限trace集和安全性的坏前缀集不相交：
TS⊨Psafe↔(Tracesfin(TS)∩BadPref(Psafe)=ϕ)TS \models P_{safe} \leftrightarrow (Traces_{fin}(TS) \ \cap \ BadPref(P_{safe}) = \phi)TS⊨Psafe↔(Tracesfin(TS) ∩ BadPref(Psafe)=ϕ)

2.6 LT性质的闭包(closure)

定义pref(σ)pref(\sigma)pref(σ)为无限字σ\sigmaσ的所有有限前缀集合：
pref(σ)={σ^∈(2AP)∗∣σ^是σ的有限前缀}pref(\sigma) = \{ \hat{\sigma} \in (2^{AP})^* \ | \ \hat\sigma 是\sigma的有限前缀\}pref(σ)={σ^∈(2AP)∗ ∣ σ^是σ的有限前缀}

例如，取σ=A0A1..\sigma=A_0A_1..σ=A0A1..则pref(σ)={ϵ,A0,A0A1,..}pref(\sigma)=\{\epsilon,A_0,A_0A_1,..\}pref(σ)={ϵ,A0,A0A1,..}。

还可以定义LT性质PPP的前缀，为其中所有无限字的前缀集合的并集：
pref(P)=⋃α∈Ppref(σ)pref(P)=\bigcup_{\alpha \in P}pref(\sigma)pref(P)=α∈P⋃pref(σ)

那么，LT性质PPP的闭包定义为前缀都在pref(P)pref(P)pref(P)中的那些无限字的集合（得到的还是一个LT性质）：
closure(P)={σ∈(2AP)ω∣pref(σ)⊆pref(P)}closure(P)=\{\sigma \in (2^{AP})^{\omega} \ | \ pref(\sigma) \subseteq pref(P)\}closure(P)={σ∈(2AP)ω ∣ pref(σ)⊆pref(P)}

也就是说，PPP的闭包是那些前缀也是PPP的前缀的无限字的集合。反过来看，PPP的闭包中的无限字不会以不是PPP的前缀的有限字为前缀。

使用闭包可以判定一个LT性质是不是安全性。一个LT性质是安全性，当且仅当其闭包是其本身：
closure(P)=Pclosure(P) = Pclosure(P)=P

2.7 活性(liveness)

活性（PliveP_{live}Plive）相比安全性而言，其表达的是在无限时间上的性质。安全性表达“坏的事情不会出现”，而活性则表达“期望的事情最终一定会出现”。

相比安全性，活性只能在无限时间上判定真伪，所以它不会移除任何有限字，其前缀集合就是整个有限字集合：
pref(Plive)=(2AP)∗pref(P_{live})=(2^{AP})^*pref(Plive)=(2AP)∗

活性可以分为三种：

EventuallyEventuallyEventually：如【每个进程最终都能访问临界资源】
RepeatedeventuallyRepeated \ eventuallyRepeated eventually：如【每个进程最终都能无限经常次访问临界资源】
StarvationfreedomStarvation \ freedomStarvation freedom：如【每个想要访问临界资源的进程最终都能访问临界资源】

注意，pref(Plive)=(2AP)∗pref(P_{live})=(2^{AP})^*pref(Plive)=(2AP)∗等价于closure(Plive)=(2AP)ωclosure(P_{live})=(2^{AP})^{\omega}closure(Plive)=(2AP)ω。

2.8 非安全性也非活性的例子

若定义LT性质为P⊂(2AP)ωP \subset (2^{AP})^{\omega}P⊂(2AP)ω，则安全性和活性是不相交的。

若定义LT性质为P⊆(2AP)ωP \subseteq (2^{AP})^{\omega}P⊆(2AP)ω，则仅有(2AP)ω(2^{AP})^{\omega}(2AP)ω既是安全性又是活性。这可由“安全性的闭包是其自身，而活性的闭包是整个无限字”来验证。

并非所有LT性质都是安全性或者活性，但总能表示成一个安全性和一个活性的合取形式。

例如【一个机器初始吐出三瓶雪碧，接下来可以无限经常次地吐出啤酒】，这一用自然语言描述的性质。仅看前半句是安全性（因为能用坏前缀表述，如前三个至少有一个是啤酒，那么就是一个坏前缀）；仅看后半句是活性（注意，无限经常次吐出啤酒，并非是仅允许吐出啤酒，任何有限序列都无法说明是不是无限经常次吐出啤酒，这部分是活性）。

2.9 分解定理(decomposition theorem)

任何一个LT性质总能分解成安全性和活性的交集：
P=Psafe∩PliveP=P_{safe} \cap P_{live}P=Psafe∩Plive

一般地，因为闭包的闭包仍是自身（一定是安全性），总可以将其按闭包分解出来：
P=closure(P)∩(P∪((2AP)ω∖closure(P)))P=closure(P) \ \cap \ (P \cup ((2^{AP})^{\omega} \setminus closure(P)))P=closure(P) ∩ (P∪((2AP)ω∖closure(P)))

更加一般地，所分解出的安全性是闭包的超集，而活性则是右半部分的子集：
Psafe⊇closure(P)Plive⊆(P∪((2AP)ω∖closure(P)))\begin{aligned} P_{safe} & \supseteq closure(P) \\ P_{live} & \subseteq (P \cup ((2^{AP})^{\omega} \setminus closure(P))) \end{aligned} PsafePlive⊇closure(P)⊆(P∪((2AP)ω∖closure(P)))

2.10 基于动作的公平性(fairness)

公平性可以用于去除那些不合实际(unrealistic) 的系统行为，公平性有时是建立活性性质的必要手段。例如，对两个红绿灯进程的interleaving：
TS=TrLight1∣∣∣TrLight2TS=TrLight_1 \ ||| \ TrLight_2TS=TrLight1 ∣∣∣ TrLight2

给定一个活性性质的自然语言描述为【每个红绿灯都无限经常次处在绿灯状态】，那么下面这个trace在TS中，却不满足那条活性：
{red1,red2}{green1,red2}{red1,red2}{green1,red2}...\{red_1,red_2\} \ \{green_1,red_2\} \ \{red_1,red_2\} \ \{green_1,red_2\} \ ...{red1,red2} {green1,red2} {red1,red2} {green1,red2} ...

这个例子可以看出unrealistic这一词的精髓。这个模型本身没有问题，但这条trace是不合实际的，因为实际中并不会有某一个红绿灯的切换频率是无穷大的，以至于在无限长的trace中另一个红绿灯的切换都未被记录。

注意，trace中有多少元素和时间尺度无关，只和系统的状态转换的次数有关。假如两个红绿灯，一个切换频率是无穷大，另一个切换频率是40秒，那么无论多长的trace都没法表达完40秒(甚至1秒或者0.0…1秒)。

公平性的引入即是为了排除此类不现实的trace，也就在模型检验阶段避免了相应的不现实执行的验证（后面会讨论排除得过多和过少的问题）。

公平性可以分为三种，无条件的、强的、弱的。对一个没有终止状态的TS，存在若干无限的执行片段，每个都可记为s0→α0s1→α1...s_0\xrightarrow[]{\alpha_0}s_1\xrightarrow[]{\alpha_1}...s0α0s1α1...，则可以用动作的子集A⊆ActA \subseteq ActA⊆Act定义三类公平性：

UnconditionalA−fairUnconditional \ A-fairUnconditional A−fair：AAA中存在无条件无限经常次执行的动作。
true⟹∀k≥0.∃j≥k.αj∈Atrue \Longrightarrow \forall k \geq 0. \ \exists j \geq k. \ \alpha_j \in Atrue⟹∀k≥0. ∃j≥k. αj∈A
因为是无条件的，所以⇒\Rightarrow⇒左边是truetruetrue，右边完全是在诠释【AAA中存在无限经常次执行的动作】，即对trace中的动作序列的任一位置kkk，总能在其后找到一个位置jjj，该位置的动作αj∈A\alpha_j \in Aαj∈A。
StronglyA−fairStrongly \ A-fairStrongly A−fair：若AAA中存在无限经常次使能（想做）的动作，那么AAA中存在无限经常次执行的动作。
(∀k≥0.∃j≥k.Act(sj)∩A≠ϕ)⟹∀k≥0.∃j≥k.αj∈A(\forall k \geq 0. \ \exists j \geq k. \ Act(s_j) \cap A \neq \phi) \Longrightarrow \forall k \geq 0. \ \exists j \geq k. \ \alpha_j \in A(∀k≥0. ∃j≥k. Act(sj)∩A=ϕ)⟹∀k≥0. ∃j≥k. αj∈A
右边是不变的。整体上表示，对trace中的状态序列的任一位置kkk，若总能在其后找到一个位置jjj，使得状态sjs_jsj的所有直接动作Act(sj)Act(s_j)Act(sj)中存在AAA中的动作，也即Act(sj)∩A≠ϕAct(s_j) \cap A \neq \phiAct(sj)∩A=ϕ（至此即表示无限经常次使能），那么AAA中一定存在无限经常次执行的动作（⇒\Rightarrow⇒右边）。
WeaklyA−fairWeakly \ A-fairWeakly A−fair：若从某位置开始，不断有AAA中的动作使能，那么AAA中存在无限经常次执行的动作。
(∃k≥0.∀j≥k.Act(sj)∩A≠ϕ)⟹∀k≥0.∃j≥k.αj∈A(\exists k \geq 0. \ \forall j \geq k. \ Act(s_j) \cap A \neq \phi) \Longrightarrow \forall k \geq 0. \ \exists j \geq k. \ \alpha_j \in A(∃k≥0. ∀j≥k. Act(sj)∩A=ϕ)⟹∀k≥0. ∃j≥k. αj∈A
右边是不变的。整体上表示，从trace中的状态序列的某一位置kkk开始，若其后的所有位置jjj，对应的状态sjs_jsj的所有直接动作Act(sj)Act(s_j)Act(sj)中总是存在AAA中的动作，也即Act(sj)∩A≠ϕAct(s_j) \cap A \neq \phiAct(sj)∩A=ϕ（至此即表示从某一位置之后不断使能），那么AAA中一定存在无限经常次执行的动作（⇒\Rightarrow⇒右边）。

在下图标注的执行中，取A={enter1,enter2}A=\{enter_1,enter_2\}A={enter1,enter2}，可见AAA中的动作enter1enter_1enter1和enter2enter_2enter2都无限经常次使能，最终enter2∈Aenter2\in Aenter2∈A无限经常次执行了，所以这个trace是满足stronglyA−fairstrongly \ A-fairstrongly A−fair的。

这里留下一点个人猜想：虽然听起来有点违背事实，可以证明在任意的动作集合A∈ActA \in ActA∈Act下无条件的公平性和强公平性是等价的。
因为如果AAA中某些动作无限经常次执行，那么这些动作一定无限经常次使能。所以可以从无条件公平推出强公平。这个还能说明，不存在仅有enter1无限经常次使能而导致enter2无限经常次执行的情况，因为无限经常次执行的动作一定也在无限经常次使能里面。

在下图标注的执行中，取A={req2}A=\{req_2\}A={req2}，可见AAA中的动作req2req_2req2从k=0k=0k=0之后就不断使能，但AAA中没有无限经常次执行的动作，所以这个trace不满足weaklyA−fairweakly \ A-fairweakly A−fair。

注意，【不断使能】是接下来每个状态都要使能，比【无限经常次使能】更苛刻。

但还需注意，因为定义弱公平性时先说明了存在一个起始点kkk，所以强公平性和弱公平性无法比较哪个更严格。倘若指定了弱公平性里的起始点k=0k=0k=0，这时就可以比较了，它要比强公平性的条件更严格。这在字面上好似很矛盾，实际上没有什么问题，可以类比着看，无条件公平性中的条件truetruetrue是最宽松的条件。

2.11 公平性对path的过度去除和去除不足

公平性的引入就是为了去除不合理的path，但是当去除得太多（约束过强）或者去除得太少（约束过弱）时，验证结果导出的true和false和真实的合理的模型的true和false有一定的不确定关系，实际上这里也就是一个很普通的集合问题。

约束过强时，去除的path太多，实际验证使用的path是合理path的子集：

所以当验证出错时，能说明合理path对应的模型是有问题的。但验证通过时却不能说明合理path对应的模型没有问题。
约束过弱时，去除的path太少，实际验证使用的path是合理path的超集：

所以当验证通过时，能说明合理path对应的模型是正确的。但验证出错时却不能说明合理path对应的模型有错误。

2.12 公平性假设(fairness assumptions)

公平性假设F\mathcal{F}F将无条件公平、强公平性、弱公平性分属成三个集合，表示为三元组：
F=(Fucond,Fstrong,Fweak)\mathcal{F=(F_{ucond},F_{strong},F_{weak})}F=(Fucond,Fstrong,Fweak)

其中的每个元素Fxxx\mathcal{F_{xxx}}Fxxx是该类公平性属性的集合。如Fucond={fucond1,fucond2,...}\mathcal{F_{ucond}=\{f_{ucond_1},f_{ucond_2},...\}}Fucond={fucond1,fucond2,...}，对之中的每个fucondi⊆Actf_{ucond_i} \subseteq Actfucondi⊆Act。类似地，可知Fucond,Fstrong,Fweak⊆2AP\mathcal{F_{ucond},F_{strong},F_{weak}}\subseteq 2^{AP}Fucond,Fstrong,Fweak⊆2AP。

称一个执行片段ρ\rhoρ满足公平性假设F\mathcal{F}F，也即称它是F−fair\mathcal{F}-fairF−fair的，意为：

对所有A∈FucondA \in \mathcal{F_{ucond}}A∈Fucond，执行片段ρ\rhoρ是unconditionallyA−fairunconditionally \ A-fairunconditionally A−fair的
对所有A∈FstrongA \in \mathcal{F_{strong}}A∈Fstrong，执行片段ρ\rhoρ是stronglyA−fairstrongly \ A-fairstrongly A−fair的
对所有A∈FweakA \in \mathcal{F_{weak}}A∈Fweak，执行片段ρ\rhoρ是weaklyA−fairweakly \ A-fairweakly A−fair

例如，取2.10中第一个例子的执行：

当F=(ϕ,{{enter1,enter2}},ϕ)\mathcal{F=(\phi,\{\{enter_1,enter_2\}\},\phi)}F=(ϕ,{{enter1,enter2}},ϕ)，也就是说没有Fucond\mathcal{F_{ucond}}Fucond和Fweak\mathcal{F_{weak}}Fweak，而且Fstrong\mathcal{F_{strong}}Fstrong里也只有一个公平性性质fstrong1={enter1,enter2}f_{strong_1}=\{enter_1,enter_2\}fstrong1={enter1,enter2}，这个公平性假设和2.10第一个例子给出的强公平性性质是完全一样的。所以图上的执行是满足这个公平性性质F\mathcal{F}F的。

又如，还是上面这个执行，但是将上面的例子Fstrong\mathcal{F_{strong}}Fstrong里唯一的公平性性质里的动作拿出来，拆成两个，得到：
F′=(ϕ,{{enter1},{enter2}},ϕ)\mathcal{F'=(\phi,\{\{enter_1\},\{enter_2\}\},\phi)}F′=(ϕ,{{enter1},{enter2}},ϕ)

显然，这个执行对fstrong2={enter2}f_{strong_2}=\{enter_2\}fstrong2={enter2}是满足强公平性的，但是对fstrong1={enter1}f_{strong_1}=\{enter_1\}fstrong1={enter1}是不满足的，所以对整个公平性性质F′\mathcal{F'}F′也是不满足的。

又如，取2.10中第二个例子的执行：

对上个例子的F′\mathcal{F'}F′加入两个弱公平性属性：
F′′=(ϕ,{{enter1},{enter2}},{{req1},{req2}})\mathcal{F''=(\phi,\{\{enter_1\},\{enter_2\}\},\{\{req_1\},\{req_2\}\})}F′′=(ϕ,{{enter1},{enter2}},{{req1},{req2}})

考察上图中的执行是否满足F′′\mathcal{F''}F′′中的每个公平性属性：

fstrong1={enter1}f_{strong_1}=\{enter_1\}fstrong1={enter1}是满足的，因为enter1enter_1enter1无限经常次使能且无限经常次进入了
fstrong2={enter2}f_{strong_2}=\{enter_2\}fstrong2={enter2}是满足的，因为其中的全部动作即仅enter2enter_2enter2没有无限经常次使能（所以也不用看有没有无限经常次执行了）
fweak1={req1}f_{weak_1}=\{req_1\}fweak1={req1}是满足的，因为对于其中的全部动作即仅req1req_1req1而言，在状态序列上找不到一个位置kkk使得在这之后的所有状态都有req1req_1req1不断使能（所以也不用看有没有无限经常次执行了）
fweak2={req2}f_{weak_2}=\{req_2\}fweak2={req2}是不满足的，见2.10的第二个例子。

综上，上图中的执行不满足公平性假设F′′\mathcal{F''}F′′。

2.13 TS被公平性假设F\mathcal{F}F约束后满足LT性质P

将公平性整合为公平性假设后，拿整个公平性假设来作为性质约束模型，以去除模型中不切实际的那些trace。前面说的都是执行片段ρ\rhoρ满足公平性假设F\mathcal{F}F，这里要将其拓展到path π\piπ，再拓展到trace σ\sigmaσ上。

称形如s0→s1...s_0 \to s_1...s0→s1...是F−fair\mathcal{F}-fairF−fair的，仅当存在与之对应位置状态相同的执行序列s0→α0s1→α1...s_0\xrightarrow[]{\alpha_0}s_1\xrightarrow[]{\alpha_1}...s0α0s1α1...。

记FairPathsF(s)FairPaths_{\mathcal{F}}(s)FairPathsF(s)为从状态sss出发的所有F−fair\mathcal{F}-fairF−fair的path的集合。

记FairPathsF(TS)FairPaths_{\mathcal{F}}(TS)FairPathsF(TS)为⋃s∈IFairPathsF(s)\bigcup_{s \in I} FairPaths_{\mathcal{F}}(s)⋃s∈IFairPathsF(s)，即从所有初始状态出发的所有F−fair\mathcal{F}-fairF−fair的path的集合。

称F−fair\mathcal{F}-fairF−fair的path π\piπ的对应trace，即σ=trace(π)\sigma=trace(\pi)σ=trace(π)也是F−fair\mathcal{F}-fairF−fair的。

直接对上面的FairPathsFairPathsFairPaths取trace，得到从某状态出发的所有F−fair\mathcal{F}-fairF−fair的trace，以及整个TS的F−fair\mathcal{F}-fairF−fair的trace：
FairTracesF(s)=trace(FairPathsF(s))FairTracesF(TS)=trace(FairPathsF(TS))\begin{aligned} FairTraces_{\mathcal{F}}(s)&=trace(FairPaths_{\mathcal{F}}(s)) \\ FairTraces_{\mathcal{F}}(TS)&=trace(FairPaths_{\mathcal{F}}(TS)) \end{aligned} FairTracesF(s)FairTracesF(TS)=trace(FairPathsF(s))=trace(FairPathsF(TS))

前面学了，说一个TS满足LT性质P，即TS⊨PTS \models PTS⊨P，当且仅当其trace集合是PPP的子集，即Traces(TS)⊆PTraces(TS)\subseteq PTraces(TS)⊆P。

引入公平性假设后，称TS被公平性假设F\mathcal{F}F约束后满足LT性质P，只需考虑TS中的那些被公平性假设约束后的trace集合是P的子集即可，记为：
TS⊨FPiffFairTracesF(TS)⊆PTS \models_{\mathcal{F}} P \ \ \ iff \ \ \ FairTraces_{\mathcal{F}}(TS) \subseteq PTS⊨FP iff FairTracesF(TS)⊆P

例如，对本篇全文采用的互斥信号量的例子（见2开头），在2.12中考察了三个公平性假设。若针对这个例子，给出一个LT性质【每个进程都能无限经常次进入临界区】记为P，用2.12中的F′\mathcal{F'}F′约束是不满足P的，即TS⊭F′PTS \nvDash_{\mathcal{F'}}PTS⊭F′P，但是用F′′\mathcal{F''}F′′约束后就是满足P的了，即TS⊨F′′PTS \vDash_{\mathcal{F''}}PTS⊨F′′P。

因为公平性假设F\mathcal{F}F的约束是在无限trace上的，而安全性是在有限trace上的，所以一个TS用公平性约束与否不会影响其是否满足某个安全性性质：
TS⊨PsafeiffTS⊨FPsafeTS \vDash P_{safe} \ \ \ iff \ \ \ TS \vDash_{\mathcal{F}} P_{safe}TS⊨Psafe iff TS⊨FPsafe

相对地，活性是在无限trace上的，一个TS用公平性约束，无法保证约束后的TS对某活性性质的满足性仍保持。