Transition System(变迁系统) 与 TLA+

概述

本文章是根据法国国立高等电力技术、电子学、计算机、水力学与电信学校 (E.N.S.E.E.I.H.T.) 第八学期课程“Système de Transition”总结而来的课程笔记。碍于本人学识有限，部分叙述难免存在纰漏，请读者注意甄别。

参考：

• 系统分析与验证 - Campsisgrandiflora的博客
• 《 Introduction to TLA 》- Lesie Lamport

变迁系统

在计算机科学和控制理论中，“变迁系统”用数学的方法描述离散系统的行为。变迁系统主要由“状态”和状态之间的“状态迁移”组成。 有标号的变迁系统可以从已定义的标签集合中选择相应标签来标记状态迁移，而且相同的标签可能被应用在多个状态迁移上。 变迁系统也可以是无标记的，此时也可以认为标签集合中只有单一标签元素，从而省略了状态迁移上的标签记号。

变迁系统在数学定义上和有向图一致，但与有限状态自动机有一定不同。

变迁系统的特点有：

• 系统状态的集合不一定是有限的或可数的；
• 状态迁移的集合不一定是有限的或可数的；
• 变迁系统并不需要给出“开始”状态或“最终”状态；
• 变迁系统可以表示为有向图，有限状态自动机则不能。

资料来源于维基百科：变迁系统

TLA+

形式化验证

形式化验证技术想要解决的核心问题是：软件总是可能存在 Bug 的，而测试始终无法涵盖所有可能性，特别是对于并发系统及分布式系统来说，就算单元测试达到了 100% 分支覆盖率，也不能肯定的说这个系统在线程安全，一致性等方面不会出问题。那如何更好的来验证我们的程序是否符合预期呢？

形式化验证就旨在使用严谨的数学证明方法来证明某一算法是正确的。

TLA+

Temporal Logic of Actions **+**是由Leslie Lamport开发的一种【形式化验证语言】。它用于设计、建模、记录和验证程序，尤其是并发系统和分布式系统。TLA +被描述为可完全测试的伪代码，其用途类似于为软件系统绘制蓝图。

由于 TLA+ 写的代码并不是用来实际运行的，故一般将其代码称为模型（Model）而非程序（Program）。

学习资源

1. Learn TLA+
2. L. Lamport 关于TLA+的视频
3. 其他资源

第一部分：Transition System

定义

变迁系统

Transition System在计算机科学中通常用作描述系统行为的模型，它是一种有向图，节点代表状态，边代表着状态的转化。

状态（state）描述了系统在其行为的特定时刻的一些信息。
例如，交通灯的状态指示灯的当前颜色。类似地，顺序计算机程序的状态指示所有程序变量的当前值，以及指示要执行的下一个程序语句的程序计数器的当前值。

转变（transition）指定系统如何从一种状态演变为另一种状态。
对交通信号灯来说，转换表示从一种颜色切换到另一种颜色。而对于顺序程序，转换通常对应于语句的执行，并且可能涉及某些变量和程序计数器的更改。

下面给出一种Transition System（TS）的定义

变迁系统是一个三元组$⟨S,I,R⟩$:

• $S$ 是状态集。包含 终结状态 和 非终结状态
• $I \subseteq S$ 是一个 初始状态
• $R \subseteq S \times S$ 是状态对之间的（转换）关系。$(s,s') \in R$ 表示系统从状态 $s$ 到状态$s'$ 的转换。我们假定 $s$ 表示现在时刻的状态集合， $s$ 中的变量称为现态， $s'$ 表示发生转变之后的状态集合， $s'$ 中的变量称为次态。

例：

$S = {S_0, S_1, S_2, S_3,S_4}$

$I = {S_0}$

$R = \{(S_0,S_0), (S_0,S_1), (S_0,S_2), (S_2,S_3), (S_3,S_4), (S_4,S_3)\}$

直接后继（Direct Successors）

定义为：

$Post(s,α)=\{s'∈S | s\xrightarrow{α}s' \}$

就是指状态$s$执行动作$α$之后能达到的状态的集合

如果α为任意动作，可以记为：

$Post(s)=\bigcup_{α∈Act}Post(s,α)$

直接前任（Direct Predecessors）

$Pre(s, α) =\{s'∈S|s'\xrightarrow{α}s\}$

指通过执行动作α之后能达到状态s的状态集合

同理，α如果为任意动作，则记为：

$Pre(s)=\bigcup_{α∈Act}Pre(s,α)$

用图来表示前任和后继的话就是这样子的：

终止状态

对于TS模型来说，终止状态就是指没有后继状态的状态，即$Post(s)=\varnothing$

串行程序的终止状态代表着程序的终止。

对于并行程序来说，我们一般不考虑它的终止状态，因为并行程序大都要求持续运行下去。

确定性TS（Deterministic Transition System）

如果

$|S_{0}|≤1\;and\;|Post(s,α)|≤1$

那么这个TS就可以称为动作确定的TS

如果

$|S_{0}|≤1\;and\;|Post(s,α)\cap \{s'∈S|L(s')=A\}|≤1(A∈2^{AP})$

那么这个TS就可以称为AP确定的TS

序列（Séquence）

$S$ 是状态集：

• $S^*$ 是 $S$ 上的有限序列集；
• $S^w$ 是 $S$ 上的无限数据集；
• $\sigma _i$ 是序列 $\sigma$ 从 0 开始的第 $i$个元素。
• 序列 $S$ 用以下形式表示：$⟨s1 → s2 → ...⟩$
• $⟨⟩$ 表示空序列；

对于一个有限序列$\sigma$ ：

• $\sigma^*$ 是由任意的 $\sigma $ 重复产生的有限序列集。
• $\sigma^+ \triangleq \sigma^* \backslash \{ ⟨⟩ \}$
• $\sigma^w$ 是由任意的 $\sigma $ 重复产生的无限序列集。

迹（trace）

有限轨迹（Traces finies）

令 $⟨S, I, R⟩$ 是一个变迁系统。我们称有限迹为有限序列$\sigma \in S^*$ 使得

• $\sigma = ⟨s_0 → s_1 → ... → s_{n-1} → s_n ⟩$

• $\forall i \in [0 ... n[:(s_i, s_{i-1}) \in R$

最大有限轨迹（Traces finies maximales）

当有限轨迹$⟨s_0 → s_1 → ... → s_{n-1} → s_n ⟩ \in S^*$ 时，我们称它是最大的。$s_n$没有后继状态，即$\forall s \in S:(s_n, s) \notin R$

无限轨迹（Trace infinies）

令 $⟨S, I, R⟩$ 是一个变迁系统，并且$s_0 \in S$。我们称从 $s_0$开始到元素 $tr \in S^w$ 的无限序列为

• $tr = ⟨s_0 → s_1 → s_2 → ... ⟩$

• $\forall i \in \mathbb{N}:(s_i, s_{i+1}) \in R$

来自状态的轨迹（Traces issues d’un état）

令 $⟨S, I, R⟩$ 是一个变迁系统，并且$s \in S$。

• $Traces(s) $ 是从状态$s$ 开始的最大无限或有限轨迹的集合。

执行（Exécutions）

令 $⟨S, I, R⟩$ 是一个变迁系统，

一次执行片段 $σ = ⟨s_0 →…⟩ $ 是满足 $s_0 ∈ I $ 的最大无限或有限轨迹（如果是有限执行片段，那么它结束于终止状态，或者该片段是一个无限执行片段）。

• $Exec(S)$ 是 $S = \bigcup_{s_0 \in I} Traces(s_0)$ 的执行集。
• 如果 $I = ∅$，则我们有一个（也是唯一一个）空执行$ ⟨⟩$。
• 如果一个初始、有限执行片段的终止状态为s，那么s称为可达的(reachable)，直观来说，可达表示从初始状态开始能够到达某个状态。我们把所有的可达状态记为Reach(TS)

练习一

例一

$s_0 → s_0 → s_2 → s_3$ 是一段非最大的有限轨迹。

1. $Traces(s_1) = ⟨s_1⟩$
2. $Traces(s_3) = ⟨(s_3 → s_4)^w⟩$
3. $Traces(s_2) = ⟨s_2 → (s_3 → s_4)^w⟩$
4. $Traces(s_0) = ⟨{s_0}^w⟩, ⟨{s_0}^+ → s_1⟩, ⟨s_0 → s_2 → (s_3 → s_4)^w⟩$
5. $Exec(S) = Traces(s_0)$

例二

1. $Traces(s_2) = ⟨s_2 → s_4⟩, ⟨(s_2 → s_3 → s_0 → s_1)^w⟩, ⟨(s_2 → s_3 → s_0 → s_1)^* → s_2 → s_4⟩$
2. $Traces(s_0) = ⟨(s_0 → s_1 → s_2 → s_3⟩^w, ⟨s_0 → s_1 → (s_2 → s_3 → s_0 → s_1)^* → s_2 → s_4⟩$
3. $Exec(S) = Traces(s_0)$

例三

1. $Traces(s_2) = ⟨(s_2 → s_3)^w⟩, ⟨(s_2 → s_3)^* → s_2 → s_4⟩$
2. $Traces(s_0) = ⟨(s_0 → (s_2 → s_3)^w⟩, ⟨(s_0 → (s_2 → s_3)^* → s_2 → s_4⟩$
3. $Traces(s_1) = ⟨(s_1 → (s_3 → s_2)^w⟩, ⟨(s_1 → (s_3 → s_2)^+ → s_4⟩$
4. $Exec(S) = Traces(s_0) \cup Traces(s_1)$

可访问状态（Etats accessibles）

令 $⟨S, I, R⟩$ 是一个变迁系统。

• $s ∈ S$ 是一个可访问状态 $\triangleq $ 有一个通过 $s$ 的执行（或等价的，有一个以 $s$ 结尾的执行前缀）;
• $Acc(S)$ 是 $S$ 的可访问状态集。

执行图（Graphe des Exécutions）

令 $⟨S, I, R⟩$ 是一个变迁系统。

执行图是有向图，其中：

• 顶点集是 $Acc(S)$；
• 有向边的集合是 $R$，仅限于可访问状态。

因此它是$ ⟨S ∩ Acc(S), R ∩ (Acc(S) × Acc(S))⟩ $ 的图。

被标记的变迁系统（Systeme de Transitions étiqueté ）

被标记的变迁系统 是一个五元组$⟨S、I、R、L、Etiq⟩$：

• $S$：状态集。
• $I ⊆ S$：初始状态集。
• $R ⊆ S × S$：状态对之间的转换关系。
• $L$：标签集。
• $Etiq$：将标签与每个转换(transition) 相关联的函数：$Etiq ∈ R → L$。带

被标记的变迁系统 非常接近自动机。但是没有 terminal state + infinity execution。

被标记的变迁系统 $⟨S, I, R, L, Etiq⟩$ 等价于由如下定义的 未标记系统$⟨S', I', R'⟩$ ：

• $S' = (L \cup \{ \epsilon \}) \times S$
• $I' = \{ \epsilon \} \times I$
• $R' = \{ ( ⟨I,s⟩, ⟨I',s'⟩ )| (s, s') \in R \land I' = Etiq(s,s')\}$

转换(transition) $s_1 \xrightarrow{a} s_2 $ 可变成 $ ⟨_,s_1⟩ \to ⟨a,s_2⟩$，其中 _ 是任何标签。

可变为

变迁系统 不等于 自动机

• 转换没有标签：Pas d’étiquette sur les transitions (ou comme si)
• 转换不是由环境引起的：Une transition n’est pas causée par l’environnement
• 没有终结状态：Pas d’états terminaux
• 可能有许多的有限状态：Nombre d’états infini possible
• 可能有无限的执行：Exécution infinie possible

表示形式

显式的表示

在执行图(Graphe d’exécution) 中显式地给出，例如以图像形式或通过顶点和边的集合。仅适用于状态和转换数量有限的变迁系统。

隐式的表示

基于变量的变迁系统的三元组$ ⟨V, Init,Trans⟩ $ 中，

• $V = \{ v_1, ..., v_n\}$：有限的的变量集；
• $Init(v_1, ..., v_n)$ ：定义初始状态并与变量 $v_i$ 相关的谓词（系数）
• $Trans(v_1, ..., v_n, {v_1}', ..., {v_n}')$：谓词定义转换，涉及表示当前状态的变量 $v_i$ 和表示后续状态的变量 ${v_i}'$。

示例

有界计数器

i = 0;
while (i < N) {
	i = i+1;
}

1. 在显式的表示中，$N = 5$:

$⟨(0, 1, 2, 3, 4, 5), \{ 0\}, \{ (0,1), (1,2), (2,3), (3,4), (4,5)\}⟩$

​ 执行图(Graphe d’exécution)为

$0 \to 1 \to 2 \to 3 \to 4 \to5$

2. 隐式的表示为：

• $V \triangleq i \in \mathbb{N}$
• $Init \triangleq i = 0$
• $Trans \triangleq i < N \land i' = i+1$ 或 $Trans \triangleq i' \leq N \land i'-i=1$

循环计数器

i = 0;
while (true) {
	i = (i+1) % N;
}

1. 在显式的表示中，$N = 4$:

$⟨(0, 1, 2, 3, 4), \{ 0\}, \{ (0,1), (1,2), (2,3), (3,4), (4,0)\}⟩$

​ 执行图(Graphe d’exécution)为

2. 隐式的表示为：

• $V \triangleq i \in \mathbb{N}$
• $Init \triangleq i = 0$
• $Trans \triangleq i’ = (i+1) \mod N $

振荡整数

i = 0;
while (true) {
		i > 0 -> i = i - 1;
	or
  	i < N -> i = i + 1;
}

1. 在显式的表示中，$N = 5$:

$⟨(0, 1, 2, 3, 4, 5), \{ 0\}, \{ (0,1), (1,2), (2,3), (3,4), (4,5), (5,4), (4,3), (3,2), (2,1)\}⟩$

​ 执行图(Graphe d’exécution)为

2. 隐式的表示为：

• $V \triangleq i \in \mathbb{N}$
• $Init \triangleq i = 0$
• $Trans \triangleq (i > 0 \land i’=i-1) \lor (i < N \land i’=i+1) $ 或 $Trans \triangleq \left| i' -i \right| = 1 \land 0 \leq i' \leq N$

表示形式所对应的变迁系统

对于符号描述$⟨V, Init,Trans⟩$，对应的变迁系统是$⟨S, I, R⟩$，其中：

• $S = \prod_{i \in 1..n} D_i$ ，其中$D_1,...,D_n$ 是变量 $v_1, ..., v_n$ 的域（类型）
• $I = \{ (v_1,...,v_n) | Init(v_1, ..., v_n)\}$
• $R = \{ ((v_1, ..., v_n),({v_1}', ..., {v_n}')) | Trans(v_1, ..., v_n,{v_1}', ..., {v_n}')\}$

状态谓词（Prédicat d’état）

状态谓词是与隐式表示的系统的（状态）变量有关的谓词。

状态谓词可以看作是 S 的一部分的特征函数。

转换谓词（Prédicat de transition）

转换谓词是与已启动和未启动（状态）变量相关的谓词。

转换谓词可以看作是 $S × S$ 子集的特征函数。

实例：谓词

$V \triangleq n \in \mathbb{N} $

$Init \triangleq -5 \leq n \leq 5$

$Trans \triangleq n \neq 1 \land ((n' = n/2 \land n \equiv 0[2]) \lor (n' = (3n+1)/2 \land n \equiv 1[2]))$

• Prédicat d’état : $ Init, n < 20 $

• Prédicat de transition : $Trans, n' − n > 3$

属性

阻塞（Blocage）

死锁（Interblocage）

一个系统有一个死锁 $\triangleq$ 存在一个可访问的状态，没有关系 R 的后继。等效地，如果执行（execution）有限，系统就会出现死锁。

对于建模经典顺序程序的系统，死锁相当于终止。

可复位（Réinitialisable）

一个系统可以从任何可访问的状态重置 $\triangleq$ 有一个有限轨迹导致一个初始状态。

这个属性意味着在任何时候，都有一系列的转换（transitions）返回到系统的初始状态，从而重新启动。 这样的系统只有无限的执行。

重复（Bégaiement）

重复状态 $\triangleq$ 状态有一个循环：$(s,s) ∈ R$。

一个重复变迁系统 $\triangleq$ 任何状态都有一个到自身的循环：$Id ⊆ R$。

用处

1. 我们可以在 $s_0$ 中停留任意时间后进入 $s_1$。

2. 无限的执行：在无重复系统中，任何没有后继者的状态都有一个独特的后继者：它自己。
3. 终止状态时（或死锁）$... \to s_i$ 就相当于 $... \to {s_i}^w$
4. 可以组成几个变迁系统。

组合

自由组合

变迁系统 $⟨V,I,T⟩$ 由带有重复的 $⟨V_1, I_1,T_1⟩$ 和 $⟨V_2, I_2, T_2⟩ $ 组成， 其中：

• $V \triangleq V_1 \cup V_2$ ：变量$V_1$和$V_2$的并集
• $I \triangleq I_1 \land I_2$ ：每个子系统都从它的一个初始状态开始
• $ T \triangleq T_1 ∧ T_2 $ ：每个子系统都根据其转换（transition）演变

由于 $T_1$ 和 $T_2$ 中有循环的状态，因此 $T_1 ∧ T_2$ 意味着我们可以单独执行 $T_1$ 的转换和 $T_2$ 的循环，反之亦然，甚至可以与 $T_2$ 同时执行 $T_1$。

例：

$\left( \begin{matrix} V_1 \triangleq i \in \mathbb{N}\\ I_1 \triangleq i = 0 \\ T_1 \triangleq \begin{cases} i'=i+1\\ \lor \ i'=i\\ \end{cases}\\ \end{matrix} \right) \otimes \left( \begin{matrix} V_2 \triangleq j \in \mathbb{N}\\ I_2 \triangleq j = 0 \\ T_2 \triangleq \begin{cases} j'=j+1\\ \lor \ j'=j\\ \end{cases}\\ \end{matrix} \right) \to \left( \begin{matrix} V \triangleq i,j \in \mathbb{N}\\ I \triangleq i=0 \land j=0\\ T \triangleq \begin{cases} i'=i+1 \land j' = j\\ \lor \ (i'=i \land j'=j+1)\\ \lor \ (i'=i+1 \land j'=j+1)\\ \lor \ (i'=i \land j'=j) \end{cases}\\ \end{matrix} \right)$

严格同步的组合

变迁系统 $⟨S,I,R,L⟩$ 由标记为 $⟨S_1,I_1,R_1,L_1⟩$ 和 $⟨S_2,I_2,R_2,L_2⟩$ 严格同步地组成， 其中：

• $S \triangleq S_1 \times S_2$ ：状态对
• $I \triangleq I_1 \times I_2$ ：每个子系统都从它的一个初始状态开始
• $R \triangleq \{ ((s_1, s_2), ({s_1}', {s_2}')) | (s_1, {s_1}') \in R_1 \land (s_2, {s_2}') \in R_2 \land Etiq((s_1, {s_1}')) = Etiq((s_2, {s_2}')) \}$ ：这两个子系统严格根据带有相同标签转换
• $ L \triangleq L_1 \cap L_2 $

例：

1. Synchronizé strict avec LIFO 2 éléments (pile)

​ Donne：

2. Synchronizé strict avec FIFO 2 éléments (file)

​ Donne:

​

Synchronisé ouvert 的组合

变迁系统 $⟨S,I,R,L⟩$ 由标记为 $⟨S_1,I_1,R_1,L_1⟩$ 和 $⟨S_2,I_2,R_2,L_2⟩$ 同步地组成， 其中：

• $S \triangleq S_1 \times S_2$ ：状态对

• $I \triangleq I_1 \times I_2$ ：每个子系统都从它的一个初始状态开始

• $R \triangleq \begin{cases} ((s_1, s_2), ({s_1}', {s_2}')) | (s_1, {s_1}') \in R_1 \land (s_2, {s_2}') \in R_2 \land Etiq((s_1, {s_1}')) = Etiq((s_2, {s_2}'))\\ ((s_1, s_2), ({s_1}', {s_2})) | (s_1, {s_1}') \in R_1 \land Etiq((s_1, {s_1}')) \notin L_2\\ ((s_1, s_2), ({s_1}, {s_2}')) | (s_2, {s_2}') \in R_2 \land Etiq((s_2, {s_2}')) \notin L_1 \end{cases}$

• $ L \triangleq L_1 \cap L_2 $

例：

Synchronizé strict avec LIFO 2 éléments (pile)

Donne：

• strict：

• ouvert

  

第二部分：Action

在《概述》中，我们提到Temporal Logic of Actions +是由Leslie Lamport开发的一种【形式化验证语言】。

本章我们会简单介绍这种语言。

规约 Specification

规约的结构

一个TLA+的Model里应该包含的元素有：

• 常数 Constant
• 变量 Variable（状态 = 变量的值）
• Init. State 由状态谓词定义的一组初始状态
• 动作 Action = 连接两个状态的转换谓词：
  1. 当前状态，未启动的变量
  2. 到达状态，主要变量
• 由动作的析取构造的过渡谓词（≈无限重复动作）

例：

---------------- MODULE example ----------------
EXTENDS Naturals
VARIABLE x

\* 初始状态 Init是初始化谓词（initial predicate）
Init == x \in 0..2				\* 等价于x属于自然数 并且 0 <= x < 3

\* 动作
Plus == x'=x+1
Sub == x>0 /\ x'=x-1
Next == Plus \/ Sub				\* Next是Next-state动作（action）
Spec == Init /\ [] [ Next ]_<<x>>		

上述规约语言等价于下述变迁系统

• $V \triangleq x \in \mathbb{N}$
• $I \triangleq 0 \le x \le 2$
• $R \triangleq \begin{cases} x' = x+1\\ \lor x>0 \land x'=x-1\\ \lor x'=x \end{cases}$

常量 Constantes

• 显式常量：0、1、true、false、“string”
• 命名常量：$_{CONSTANT} \ N$，通常伴随着属性：$_{ASSUME}\ N \in Nat \land N \ge 2$

表达式 Expression

一切可以公理化的东西：

• 逻辑表达式：$¬， ∧， ∨， ∀x ∈ S:p(x)， ∃x ∈ S:p(x)$
• 算术表达式：$+，-，>，...$
• 集合表达式： $∈$，$∪$，$∩$，$⊂$，$\{e1, e2, . . . , en\}$，$n..m$，$\{x ∈ S : p(x)\}$，$\{f (x) : x ∈ S\}$，$_{UNION}\ S$，$_{SUBSET} \ S$
• $_{IF}$ … $_{THEN}$ … $_{ELSE}$ …
• 从 X 到 Y 的函数
• 元组、序列等

集合运算符 Operateurs ensemblistes

• $\{e_1, ...,e_n\}$ ： 扩展成集合
• $n ..m$ ： $i \in Nat : n \le i \le m$
• $\{ x \in S : p(x)\}$ ：S 中满足性质 p 的元素集合
  • 例1，${ n \in 1…10 : n%2=0} = {2,4,6,8,10} $
  • 例2，${ n \in Nat : n%2=1} = {所有的奇数} $
• ${ f(x) :x \in S} $ ：所有$f(x)$ 的值的集合
  • 例1，${ 2*n: n \in 1…5} = {2,4,6,8,10} $
  • 例2，${2*n+1 : n \in Nat} = {所有的奇数} $
• $_{UNION}\ S$ ：S 的元素的并集
  • $_{UNION} \{ \{ 1,2\}, \{ 3,4\}\} = \{ 1,2,3,4\}$
• $_{SUBSET}\ S$：S的所有子集的集合
  • $_{SUBSET} \{ 1,2\} = \{ \{\}, \{1\}, \{ 2\}, \{ 1,2\}\}$

动作 Action

操作符 Action Operators

• $e'$ : The value of e in the final state of a step (迭代器中e的更新值)
• $[A]_e$ : $[A ∨ (e' = e)]$
• $⟨A⟩_e$ : $[A ∧ (e' \ne e)]$
• $_{ENABLE} \ A$ : [An A step is possible]
• $_{UNCHANGED}\ E$ : $[e' = e]$
• $A · B$ : [Composition of actions]

动作 = 转换谓词 = 包含常量、变量和引发变量的布尔表达式。

动作 不等于 任务

• $\begin{aligned} & x'=x+1\\ & \equiv x'-x=1\\ & \equiv x=x'-1\\ & \equiv (x>1 \land x'/x=1 \land x'\%x=1) \lor (1=x \land 2=x') \lor (x=0 \land x' \in \{y \in Nat:y+1=2*y\})\\ \end{aligned}$

• Other types of actions:

  • $x' > x$ 或 $x' ∈ \{x + 1, x + 2, x + 3\}$（不确定性）
  • $x' ∈ \{y ∈ \mathbb{N}: ∃z ∈ N: z ∗ y = x ∧ z \% 2 = 0\}$（不可评估）
  • $x' = y ∧ y' = x$（多个变量）

由连词组成的动作

1. 仅与起始状态有关的状态谓词
2. 确定性转移谓词 $var' = . . .$ 或 非确定性转移谓词 $var' ∈ ...$

例：$x < 10 ∧ x' = x + 1$，而不是 $x′ = x + 1 ∧ x' < 11$ 或 $x′ - x = 1 ∧ x' < 11$

重复（Bégaiement）

Bégaiement

$[\mathcal{A}]_f \triangleq \mathcal{A} ∨ f' = f$ ，其中 $f$ 是变量元组。

示例：

$\begin{aligned} {[x'=x+1]_{⟨x,y⟩}} & = {(x'=x+1 ∨ (⟨x, y⟩'=⟨x,y⟩))} \\ & = {(x'= x+1 ∨ (x'=x ∧ y'=y))} \\ \end{aligned}$

Non Bégaiement

$[\mathcal{A}]_f \triangleq \mathcal{A} ∨ f' \ne f$ ，其中 $f$ 是变量元组。

无约束变量 Variables non contraintes

$\begin{aligned} {(x′=x+1)} & = {(x'=x+1 \land y'= 任何值 )} \\ & \ne {(x'=x+1 \land y'=y)} \\ \end{aligned}$

UNCHANGED

$_{UNCHANGED}\ e \triangleq e' = e$

---------------- MODULE AlternatingBit ----------------
EXTENDS Naturals
CONSTANT Data
VARIABLE val, ready, ack
-------------------------------------------------------
\* 初始状态 Init是初始化谓词（initial predicate）
Init == /\ val \in Data
		/\ ready \in {0,1}
		/\ ack = ready
		
Send == /\ ready = ack
		/\ val' \in Data
		/\ ready' = 1 - ready
		/\ UNCHANGED ack
		
Receive == /\ ready # ac k
		/\ ack' = 1 - ack
		/\ UNCHANGED <<val, ready>>
-------------------------------------------------------
Next == Send \/ Receive				\* Next是Next-state动作（action）
Spec == Init /\ [] [ Next ]_<<val, ready, ack>>		
=========================================================

函数 Function

“映射(mapping) ”意义上的函数，对应：

• $X \to Y$ : 从 X 到 Y 的一组函数。
• $f \in [X \to Y]$ : X 在 Y 中的 f 函数
• $f[x]$ : x 处的 f 值。

一个函数就是一个值。
一个包含函数的变量可以改变它的值⇒“函数改变”。

符号的定义 Definition of symbol

$f[x \in Nat]$ : 关于x的表达式。例 : $Inc[x \in Nat] \triangleq x+1$

值的定义 Definition of value

$[x \in S \mapsto expr]$. 例 : $x \in 1..4 \mapsto 2*x$

表 Table

函数 $t ∈ [X → Y ]$ 其中 X 是整数区间。

定义域 Domain

$_{DOMAIN}\ f$ : f 的定义域

值域 Codomaine

$Codomain(f) \triangleq \{ f[x]:x \in _{DOMAIN}f\}$

EXCEPT

$[a \ _{EXCEPT}\ ![i] =v] \triangleq [j\in _{DOMAIN} \ a \mapsto _{IF}\ j=i\ _{THEN}\ v\ _{ELSE}\ a[j]]$

例：$[a' = a \ _{EXCEPT}\ ![2] =8] \not\equiv (a[2]' =8)$

IncF

IncF 是数学意义上的函数定义，等价于 $IncF \triangleq [x ∈ Nat \mapsto x + 1]$

• 它的定义域：$_{DOMAIN}\ IncF$
• 它的值域：$ {IncF[x] : x ∈ _{DOMAIN}IncF}$
• $IncF \in [X \mapsto Y]$

IncO

IncO 是运算符(Operator) 的定义

• 写因式分解：类似于一个宏，其文本可以替换
• 没有定义域 和 值域
• $IncO ∈ [X → Y ]$ 没有意义

记录 Record

记录是 $[X → Y]$ 的函数，其中 X 是一组字符串。

简写作：
$["qwerty" \mapsto 1, "asdfgh" \mapsto 2] = [qwerty \mapsto 1,asdfgh \mapsto 2]$$

$rec["qwerty"] = rec.qwerty$

递归定义 Définition récursive

定义（函数或运算符）时，可以给出递归定义：

• 函数：$fact[n \in Nat] \triangleq _{IF}\ n=0\ _{THEN}\ 1\ _{ELSE}\ n*fact(n-1)$
• 运算符：$fact(n) \triangleq _{IF}\ n=0\ _{THEN}\ 1\ _{ELSE}\ n*fact(n-1)$

从理论上讲，必须证明这些定义的有效性。

n元组 n-Tuple

符号：⟨a, b, c⟩。

• n元组是定义域函数= $\{1,. . .,n\} :⟨a, b, c⟩[3] = c$
• 用于表示关系：$\{⟨x, y⟩ ∈ X × Y: R(x, y)\}$。示例：$\{⟨a, b⟩ ∈ Nat × Nat:a=2*b\}$。

序列 Sequence

$\begin{aligned} Seq(T) & \triangleq _{UNION} \{[1..n → T]: n ∈ Nat\}\\ & \triangleq 包含 T 的有限序列集 \end{aligned}$

运算符：$Len(s)$，$s ◦ t$（连接），$Append(s,e)$，$Head(s)$，$Tail(s)$。

局部定义 Local Definition

$LET$

• 表达式： $_{LET}\ v \triangleq e\ _{IN}\ f$

  等效于表达式 $f$，其中所有的符号 $v$ 的都被 $e$ 替换。例子：$_{LET}\ i \triangleq g(x)\ _{IN}\ f (i)≡ f (g(x))$

例：

$Pythagore(x, y, z) \triangleq _{LET}\ square(n) \triangleq n∗n\ _{IN}\ square(x) + square(y) = square(z)$

选择 CHOOSE

• $_{CHOOSE}\ x \in S:p$ ：确定性任意选择集合 S 中满足谓词 p 的元素。

• $max[S \in _{SUBSET}\ Nat] \triangleq\ _{CHOOSE}\ m \in S:(\forall p \in S : m \ge p)$

对于集合 S 和属性 p，选择的元素在所有执行过程中始终相同。 它不是一个随机选择器，它在每次调用时都给出一个不同的元素。所以$_{CHOOSE}\ x \in S:p = _{CHOOSE}\ x \in S:p$。

规约

• $(x =\ _{CHOOSE}\ n : n ∈ Nat) ∧ \Box [x'=_{CHOOSE}\ n : n ∈ Nat]_{⟨x⟩}$

  有一个独特的执行：$ x = c → x = c → …$其中 c 是一个不确定的整数（由选择指定）。

• $(x ∈ Nat) ∧ \Box [x' ∈ Nat]_{⟨x⟩}$

  有无限次执行，其中一些在每个状态中 x 是不同的，另一些在 x 是恒定的，另一些在 x 中循环

第三部分：线性时间属性(LT Properties)

刻画线性时间属性(LT Properties)

因为线性时间属性（LT Properties）是TS中迹的要求，所以在原子命题（AP）上的线性时间属性是$S^{w}$
的子集。$S^{w}$表示的是AP中命题的无限级联的集合

如果AP={a,b}，那么$(2^{AP})^{w}$ 可以表示为

$\{\{a\}\{a,b\}\varnothing ...，\{b\}\{a\}\varnothing\varnothing...，...\}$

类似该集合中的元素，由无限个字符级联在一起组成的序列称为无限字(infinite word)，无限字可以表示为:

$W=A_{0}A_{1}A_{2}...$

当这个序列是有限时，便称为有限字(finite word)，有限字可以表示为:

$W=A_{0}A_{1}A_{2}...A_{n}$

因为TS不考虑终止状态，所以也就无需使用有限字。

如果一个TS满足线性时间属性P，那么就表明：

$TS \vDash P\text{ 当且仅当}Traces(TS) ⊆ P$

我个人的理解是线性时间属性P刻画了AP上能够出现的原子命题序列，而迹表示的是系统在AP上出现的原子命题序列，如果系统的迹是P的子集，那么肯定这个系统就满足了线性时间属性P。

刻画基于信号量互斥系统的属性

一说到信号量和互斥，再次搬出这个例子：

在这里，$AP=\{crit_1, crit_2\}$，这个系统中的约束有一条：

“Always at most one process is in its critical section”

就是最多有一个进程能够进入临界区

用形式化的语言描述就是：

$P_{mutex} = 一个无限字的集合\{A_0A_1A_2...\} 且满足对于所有0\le i,\{crit_1, crit_2\} \nsubseteq A_{i}$

这就完成对系统属性的刻画，描述一下就是对于这个TS的运行轨迹来说不存在$\{crit_1, crit2\}$满足条件的情况。

所以无限字可以是类似$\{crit_1\}\{crit_2\}\{crit_1\}\{crit_2\}…$或者$\varnothing\varnothing\varnothing\varnothing\varnothing…$反正就是不能出现$\{crit_1, crit2\}$这个元素。

那么再问一个问题，上面的那个TS系统满足这个$P_{mutex}$ 性质嘛？

• Yes，因为从图上看不存在$\{crit_1, crit2\}$以满足了我们定义的互斥性性质。

刻画无饥饿(starvation freedom)系统的属性

不存在饥饿的系统要求满足条件:

“A process that wants to enter the critical section is eventually able to do so”

如果一个进程想要进入临界区，那么它最终总是能够进入临界区。

这一次让$AP=\{crit_1,wait_1,crit_2,wait_2\}$

用形式化的语言描述为LT性质就是：

$P_{nostarve} = 一个无限字的集合\{A_0A_1A_2...\} \\ 满足(\overset{\infty}∃ j.\;wait_{i}∈A_{j})\Rightarrow (\overset{\infty}∃ j.\;crit_{i}∈A_{j})\; for\;each\;i∈\{1,2\}$

其中 $\overset{\infty}∃$ 代表无限多

描述一下就是当一个进程进入等待状态后，之后肯定会进入临界区

那么基于信号量的互斥系统满足无饥饿性质嘛？no，如果是这样一条迹:$\varnothing\{wait_2\}\{wait_1,wait_2\}\{crit_1,wait_2\}\{wait_2\}\{wait_1,wait_2\}\{crit_1,wait_2\}...$，那么进程2将永远的不能进入临界区。

不变性(Invariants)

事实上，上述（互斥与无死锁）安全性是一种特殊的性质：不变性。不变性是LT属性，由状态的条件$Φ$给出，并且要求$Φ$对所有可达到的状态保持不变。不变性是安全性的一种，也就是安全性的子集。

如果在AP上的线性属性$P_{inv}$是不变性，那么它具有如下形式：

$P_{inv}=\{A_{0}A_{1}A_{2}... ∈ (2^{AP})^{w} | ∀j \ge 0. A_{j} \vDash Φ \}$

其中$Φ$AP上的逻辑命题公式，$Φ$ 被称为$P_{inv}$ 的不变条件。

让我们回想一下先前的基于信号量的互斥系统，在那个系统中$Φ=\lnot crit1\vee \lnot crit2$, 保证crit1和crit2不能同时为真。

$Invariants \triangleq \forall crit_1,crit_2 \; Value:Chosen(crit_1) \land Chosen(crit_2) \quad \Rightarrow \quad crit_1 = crit_2$

设TS是一个没有终止状态的转换系统，那么有：

• $TS\vDash P_{inv}$
  • $iff\; trace(\pi)∈ P_{inv}\; for\; all\; paths\;\pi \; in\; TS$
  • $iff\; L(s)\vDash Φ\; for\; all\; states\;s\;that\;belong\; to\; a\;path\; of\;TS$
  • $iff\; L(s)\vDash Φ\; for\; all\; states\;s∈Reach(TS)$

注意上面的最后一个式子，我们将TS能否满足不变性，转换成为了所有可达状态是否满足不变性这一问题。基于此我们可以设计检验不变性的算法。

我们该如何检验一个系统是否满足了不变性呢？

我们只要遍历系统的每个状态，从初始状态开始，利用深度优先(Dfs)或者广度优先(Bfs)算法，检查每一个可达状态是否满足$Φ$，只要找到一个可达状态不满足$Φ$，那么系统就不满足不变性，如果我们遍历所有状态发现均满足$Φ$，那么系统就满足不变性。

安全性(safety)

上面我们可以看到，不变性可以被视为状态属性，并且可以通过考虑可达状态来检查。但是安全性不能仅考虑可达状态来验证，而是需要对有限路径片段提出要求。

个人理解，不变性的要求是满足所有可达状态满足要求，而安全性是要求所有的系统上出现的有限路径片段满足要求，从这个角度来看，不变性就是安全性的一种特例，如果安全性要求的有限路径片段的长度为1的话，那就变成了不变性要求。

我们考虑一个自动取款机（ATM）的例子，ATM机的要求是，只有在提供了正确的个人识别码（PIN）后，才能从自动取款机中取款。这个属性不是不变量，因为它不是一个单纯的状态属性。但是，它是一种安全性，例如

$"提供正确的PIN","取款",...$

这样的路径片段是满足安全性的，但如果出现

$"提供错误的PIN","取款"...$

这样的路径片段是是不满足安全性的，我们可以看到，一旦出现了这样"坏(bad)"的片段，不管后面如何都是不满足安全性的，我们引入前缀、坏前缀等概念来帮助我们定义安全性。

安全性通常被描述为“不会发生不好的事情”(nothing bad should happen)

安全性的例子

• 互斥性是一种典型的安全性，它要求在临界区最终只有一个进程存在，bad thing指的是在临界区存在两个或两个以上的进程，这种坏事要求永远不会发生
• 无死锁性(deadlock freedom)是另一个典型的安全属性。在哲学家问题中，发生死锁的特征是所有哲学家都拿起了一把筷子，并且正在等待拿起第二把筷子，这种坏的（或unwanted，即不必要的）情况要求永远都不会发生。

安全性定义为

$对于所有的\sigma∈(2^{AP})^w\setminus P_{safe}存在一个\sigma的有限前缀\hat{\sigma}满足 \\ P_{safe}\cap\{\sigma'∈(2^{AP})^w|\hat{\sigma}是\sigma'的有限前缀\}=\varnothing$

解释一下，对于所有的无限字$\sigma=A_{0}A_{1}A_{2}...\in(2^{AP})^w\setminus P_{safe}$ ，存在$\sigma$的有限前缀 $\hat{\sigma}=A_{0}A_{1}…A_{n} $
，使得以 $\hat{\sigma}$ 有限前缀起始的字$A_{0}A_{1}...A_{n}B_{n+1}B_{n+2}...$ 不属于$P_{safe}$。

有限字 $\hat{\sigma}=A_{0}A_{1}...A_{n}$ 被称为$P_{safe}$ 的坏前缀(bad prefix)，符号表示为 $BadPref(P_{safe})$ 。

如果 $\hat{\sigma} $被称为 $P_{safe}$ 的最小坏前缀(minimal bad prefix)，那么就是说 $\hat{\sigma}$ 中没有比 $\hat{\sigma} $ 长度更小的坏前缀，符号表示为$MinBadPref(P_{safe})$。

对于一个TS系统满足安全性，那么当且仅当：

• $TS\models P_{safe}$
• $iff\; trace(TS)\subseteq P_{safe}$
• $iff\; trace_{fin}(TS) \cap BadPref=\varnothing$
• $iff\; trace_{fin}(TS) \cap MinBadPref=\varnothing$

以红绿灯系统为例，它拥有一个属性

each red phase should be immediately preceded by a yellow phase
只有在黄灯亮了之后红灯才能亮

AP定义为$\{red,yellow\}$，用形式化的符号表述为：

$一个无限字的集合\{A_{0}A_{1}A_{2}...\}\; 对于所有i>0满足red∈A_{i},yellow∈A_{i-1}$

类似于$\varnothing\varnothing\{red\}$，$\varnothing\{red\}$ 都是最小坏前缀，因为 $\{red\}$之前没有出现 $\{yellow\}$

而类似于$\{yellow\}\{yellow\}\{red\}\{red\}\varnothing\{red\}$是坏前缀而不是最小坏前缀，因为存在比它更小的坏前缀 $\{yellow\}\{yellow\}\{red\}\{red\}$

活性(liveness)

安全性规定“不好的事情永远不会发生”，一个算法可以很容易地实现一个安全性，只要检验一下看看会不会出现不好的情况。但是这很多时候是不需要的，有时候没有必要保证永远不会发生不好的事情，为此需要一些其他属性来补充。这样的属性称为"活性(liveness)"属性。可以说，活性表示**“好事”将会发生**(something good will happen)

活性的例子

• “每个进程最终都会进入临界区”
• “每个哲学家将会无限经常次吃到饭”

从上面的定义中我们就可以知道，对于活性的判断和安全性完全不同，因为安全性只要有一个坏前缀就可以驳倒安全性，不论后面的序列如何。而活性需要考虑未来无限路径中需要满足的特性。

如果 $P_{live}$ 是AP上上的活性，那么无论何时：p$ref(P_{live})=(2^{AP})^{*}$ 被称为活性，那么每个在AP上的有限字都能够扩展成为 $P_{live}$ 中的无限字

活性 vs 安全性

• 活性和安全性是不相交的嘛？

  是的

• 所有线性时间属性都是活性或者安全性嘛？

  不是

• 有哪些既不是安全性也不是活性的例子？

  例如：“机器在提供三次雪碧之后，会无限次提供啤酒”

  这个例子由两个部分组成，一个是“提供三次雪碧之后”，这是一个安全属性，我们给出一个坏前缀，提供一次雪碧后提供啤酒，另一部分是“无限次提供啤酒”，这是一个活性属性。所以这种包含了安全性和活性的特性，既不属于安全性也不属于活性。

• 是否所有的线性时间属性都可以表示为安全性和活性的交集？

  是的

  根据分解定理(Decomposition theorem)

  对于任何AP上的线性时间属性P，存在安全性$P_{safe}$ 和活性 $P_{live}$ 使得

  $P=P_{safe}\cap P_{live}$

• 线性时间属性的分类（注：不变性是包含在安全性里面，中间那块黄色的区域既是安全性又是活性，代表的含义是True）

  

第四部分：Fairness

系统的一个重要方面是公平性，公平性排除了被认为是不现实(unrealistic)的无限行为，并且这一步通常是建立活性属性所必需的。

我们通过在并发系统中经常遇到的一个问题来说明公平的概念：

现有一个并发系统N，有进程 $P_{1},P_{2}...P_{N}$，它们在有需要时就会请求服务，但是现在只有一个服务进程名叫Server会为这些进程提供服务，现在Server采用如下策略：

1. 从P1开始检查，如果P1请求了服务，那么就为P1提供服务;
2. 如果P1没有请求，那么就检查下一个进程P2，直到检查完毕，然后从头开始检查…

我们可以想见，如果P1一直请求服务，那么Server会为P1无限次提供服务，而剩下的进程都会陷入无限等待的过程，这对除P1外的进程来说是是不公平(unfair)的，这种行为就属于不现实的无限行为。

为了获得由TS建模的并行系统的行为的真实描述，我们需要一种另一种形式的LT属性，来解决TS中不确定性决策的问题。

于是，为了排除上述不现实的行为，我们需要添加公平性约束(Fairness Constraints)，而公平的执行或者轨迹(execute or trace)就是满足了某些公平性约束。

公平性约束 Contraintes d’équité

公平性约束指定在程序的任何执行中必须经常无限地访问（或执行）某些状态（某些转换）。

通常，公平性约束用于将程序或其环境约束为**活性（liveness）**，而不涉及有关这些约束的实际实现的细节。

公平约束通过消除不尊重公平约束的执行来减少合法执行的集合。

循环状态集 （Ensemble recurrent d’etats）

令 $⟨S, I, R⟩$ 是一个变迁系统，且$\sigma = \langle s_0 \to ... \rangle$是一段执行。状态集$P$在$\sigma$ 中是循环的，当

• 情况1：$\sigma$是无限的：$\forall i \in \mathbb{N} : ∃ j \ge i : s_j \in P$ （$P在\sigma中出现无限次$）
• 情况2：$\sigma$是有限的：$\sigma$的最终状态在$P$里

$Inf_S(P,\sigma)$ ：$P$是在$\sigma$中的循环状态集

循环转换集（Ensemble recurrent de transitions）

令 $⟨S, I, R⟩$ 是一个变迁系统，且$\sigma = \langle s_0 \to ... \rangle$是一段执行。转换集$Q$在$\sigma$ 中是循环的，当

• 情况1：$\sigma$是无限的：$\forall i \in \mathbb{N} : ∃ j \ge i : s_j \to s_{j+1} \in Q$ （$Q在\sigma中出现无限次$）
• 情况2：$\sigma$是有限的：$\sigma$的最终转换在$Q$里

$Inf_T(Q,\sigma)$ ：$Q$是在$\sigma$中的循环状态集

例（循环状态）：

• $s_1 \; is\;recurrent\;in\;⟨(s_0 → s_1 → s_3)^ω⟩$

• $s_1 \; is\;recurrent\;in\;⟨(s_0 → s_1 → s_3 \to s_0 \to s_2 \to s_3)^ω⟩$

• $s_1 \; is\;NOT\;recurrent\;in\;⟨(s_0 → s_1 → s_3)^* \to (s_0 \to s_2 \to s_3)^ω⟩$

  个人理解，这里在说循环状态时有两个判断标准：

  1. 当这段执行是无限的时，该状态应该在这段无限执行内；
  2. 当这段执行是有限的时，该状态应该是这段有限执行的最终状态。

  下列循环转换可类比于循环状态

• $s_1 \to s_3 \; is\;recurrent\;in\;⟨(s_0 → s_1 → s_3 \to s_0 \to s_2 \to s_3)^ω⟩$

• $s_1 \to s_3 \; is\;NOT\;recurrent\;in\;⟨(s_0 → s_1 → s_3)^* \to (s_0 \to s_2 \to s_3)^ω⟩$

关于状态的公平性

简单公平性

令 $⟨S, I, R⟩$ 是一个变迁系统，如果$ F ⊆ S $ 是一组公平的状态，那么任何执行 $σ$ 必须满足循环状态集 $Inf_S (F, σ)$。

例：

$Exec(S) = ⟨{s_0}^ω⟩,⟨{s_0}^+ \to s_1⟩,⟨{s_0}^+ \to s_2 \to (s_3 \to s_4) ^w⟩,⟨{s_0}^+ \to s_2 \to (s_3 \to s_4) ^+ \to s_5⟩$

• 满足 $\{s_0\}$ 简单公平性的执行是：$⟨{s_0}^ω⟩$
• 满足 $\{s_1, s_4\}$ 简单公平性的执行是：$⟨{s_0}^+ \to s_1⟩,⟨{s_0}^+ \to s_2 \to (s_3 \to s_4) ^w⟩$
• 满足 $\{s_1, s_5\}$ 简单公平性的执行是：$⟨{s_0}^+ \to s_1⟩,⟨{s_0}^+ \to s_2 \to (s_3 \to s_4) ^+ \to s_5⟩$

满足 $\{s_0, s_1\}$ 简单公平性意味着分别满足$\{s_0\}$ 和 $\{s_1\}$ 的简单公平性

多重公平性

令 $⟨S, I, R⟩$ 是一个变迁系统，给定一个可枚举的集合，可由一组整数$ J = {0, 1, 2,…}$，公平集 $\{F_i\}i ∈ J$。

任何执行 $σ$ 必须满足 $∀i ∈ J : Inf_S (F_i, σ)$。

例：

$Exec(S) = ⟨{s_0}^ω⟩,⟨{s_0}^+ \to {s_1}^w⟩,⟨({s_0}^+ \to {s_1}^+)^w⟩,⟨({s_0}^+ \to {s_1}^+)^* \to {s_0}^+ \to {s_1}^w⟩$

• 满足 $\{s_0\}$ 简单公平性的执行是：$⟨{s_0}^ω⟩, ⟨({s_0}^+ \to {s_1}^+)^w⟩$
• 满足 $\{s_0, s_1\}$ 简单公平性的执行是：$Exec(S)$
• 满足 $\{s_0\}\{s_1\}$ 多重公平性的执行是：$⟨({s_0}^+ \to {s_1}^+)^w⟩$

满足 $\{s_0\}\{s_1\}$ 多重公平性意味着同时满足$\{s_0\}$ 和 $\{s_1\}$ 的简单公平性

有限多重公平性 ↔ 简单公平性

1. 简单情况：$J$ 是有限的。 $|J|$ 是 $J$ 的基数(cardinalite)。

   下面的简单公平性系统$⟨S', I', R'⟩$ 是等价的（执行的平等投影到 S）：

   • $S' = S \times J$
   • $I' = I \times \{0\}$
   • $\begin{aligned} R' = &\{ (⟨s,j⟩,⟨s',j+1 \mod |J|⟩) | (s,s') \in R \land s \in F_j\}\\ &∪ \{(⟨s, j⟩,⟨s', j⟩) |(s,s') ∈ R ∧ s \notin F_j \} \end{aligned}$
   • 简单公平状态$F' = F_0 \times \{0\}$

   例：

   带有多重公平性$F_0 = \{s_0\}$，$ F_1 ={s_1}$ 的ST系统与下述带有简单公平性$\{(s_0,0)\}$的ST系统等价：

   

2. 一般情况（J 可能无限）。

   下面的简单公平性系统$⟨S', I', R'⟩$ 是等价的（执行的平等投影到 S）：

   • $S' = S \times J \times J$

   • $I' = I \times \{0\} \times \{0\}$

   • $\begin{aligned} R' = &\{ (⟨s,i,i⟩,⟨s',i⊕1,0⟩) | (s,s') \in R \land s \in F_j\}\\ &∪ \{(⟨s,i,j⟩,⟨s',i,j+1⟩) | j < i \land (s,s') \in R \land s \in F_j\} \\&∪ \{(⟨s,i,j⟩,⟨s',i,j⟩) |(s,s') ∈ R ∧ s \notin F_j \} \end{aligned}$

   • 简单公平状态$F' = F_0 \times J \times \{0\}$

     注：$ i⊕1 \triangleq \begin{cases} i+1;(if;J是无限的) \ i+1 \mod |J| ;(else)\end{cases}$

在公平执行中，计数器 i、j 形成一个三角形：$⟨(0, 0) → (1, 0) → (1, 1) → (2, 0) → (2, 1) → (2, 2) → (3, 0) → ...⟩$

例：带有多重公平性$F_0 = \{s_0\}$，$ F_1 ={s_1}$ 的ST系统与下述带有简单公平性$\{(s_0,0,0)\}$，$\{(s_0,1,0)\}$的ST系统等价：

条件公平性

令 $⟨S, I, R⟩$ 是一个变迁系统，我们有两个集合 F 和 G。

任何执行 σ 必须满足 $Inf_S (F, σ) ⇒ Inf_S (G, σ)$。如果 $F$ 在 $σ$ 中循环，则 $G$ 必须在 $σ$ 中循环。

例：

$Exec(S) = ⟨{s_0}^ω⟩,⟨{s_0}^+ \to s_1⟩,⟨{s_0}^+ \to s_2 \to (s_3 \to s_4) ^w⟩,⟨{s_0}^+ \to s_2 \to (s_3 \to s_4) ^+ \to s_5⟩$

• 满足 ${s_0} ⇒ {s_5} $ 简单公平性的执行是：$⟨{s_0}^+ \to s_1⟩,⟨{s_0}^+ \to s_2 \to (s_3 \to s_4) ^w⟩,⟨{s_0}^+ \to s_2 \to (s_3 \to s_4) ^+ \to s_5⟩$
• 满足 ${s_3} ⇒ {s_4} $ 简单公平性的执行是：$Exec(S)$

满足 $\{s_3\} ⇒ \{s_4\}$ 条件公平性意味着什么？

关于转换的公平性

基于动作的公平性约束

如何表述这类公平性约束？这里采用基于动作 $\mathcal{A}$ (action)的观点.

---

弱可能性 ( $WF$ )：

我们说，一个 TLA 的 Action 动作 $\mathcal{A}$ 在状态 $s$ 下是“使能的” 或者“可触发的”(Enabled)，当且仅当系统的行为序列中可能存在着一个状态 $t$ 是 $s$ 的一个下一个后续状态，即 $⟨上一个状态\;s, 下一个状态\;t⟩$，并且这个二元组可以满足 $\mathcal{A}⟨s\to t⟩$ 这个动作规范。

$WF_f(\mathcal{A})$ 表示一个这样的系统行为：如果存在这样的一个 TLA 动 作 $\mathcal{A} ∧ (f' \neq f)$，一旦变成是“使能的”、“可触发的”，就保持着， 并且永远是“使能的”，“可触发的”，我们认为，那么这个系统就会出现无限多次（Infinitely Many) 的 $\mathcal{A} ∧ (f' \neq f)$ 步骤。换言之， 如果一旦出现一个 Action 动作的可能性并且一直保持着这种系统会执行这个动作的可能性，那么就一定会出现和发生，或者说，被执行无限多次。

强可能性 ( $SF$ )：

TLA 规约另外也定义了强公平性 (Strong Fairness) $SF_f (\mathcal{A})$，其中 $f$ 是一个状态函数，$\mathcal{A}$ 是一个 TLA 动作范式。 强公平性范式表示，如果 $\mathcal{A} ∧ (f' \neq f)$ 在一个无限的系统行为里存在着无限频繁多次的可能性，那么 $\mathcal{A} ∧ (f' \neq f)$ 就一定会出现无限多次。如果一个动作范式在某个时间点变得永远可能，那么 也满足“无限经常”的条件。因此，强公平性 $SF_f(\mathcal{A})$ 中蕴含了 $WF_f(\mathcal{A})$

个人理解：

• 在弱可能性 $WF_f(\mathcal{A})$ 中，$\mathcal{A}$ 满足 $⟨上一个状态\;s, 下一个状态\;t⟩$ 的二元组，即 $s \to t$。当 TLA 处于当前状态 $s$ 时，动作 $\mathcal{A}$ 是 “Enable”，则该动作 $\mathcal{A}$ 一定会发生（被执行无限多次）。
• 在强可能性 $SF_f(\mathcal{A})$ 中，$\mathcal{A}$ 满足 $⟨上一个状态\;s, 下一个状态\;t⟩$ 的二元组，即 $s \to t$。当 TLA 处于当前状态 $s$ 时，动作 $\mathcal{A}$ 是 “Enable”，则该动作 $\mathcal{A}$ 可能会发生（存在被执行无限多次的可能性）。

---

公平属性是 前提条件 施加在系统上以排除不切实际的痕迹。

• 无条件公平的形式是**“每个过程都会无休止地轮流使用”**。
• 强公平性 (SF) 的形式是**“如果无限频繁地启用它，则每个过程都将无限次地轮流运行”**。
• 弱公平性 (WF) 的形式是**“如果从某个特定点连续进行，则每个过程都会无限制地轮流转动”**。

之前我们看到了，LTL公式可以用来描述两进程互斥问题的公平性属性，现在我们将它推广到一般的公平性问题

设 $\phi$ 和 $\psi$ 是命题公式：

• 无条件的公平性：$\Box\Diamond\psi$
• 强公平性：$\Box\Diamond\phi\rightarrow\Box\Diamond\psi$
• 弱公平性：$\Diamond\Box\phi\rightarrow\Box\Diamond\psi$

对于公平性假设fair和LTL公式 $\phi$，我们有如下结论

$s\vDash_{fair}\phi \\ \text{当且仅当 对于所有的π∈Paths(s),如果}π\vDash fair，那么π\vDash\phi \\ \text{当且仅当 }s\vDash (fair\rightarrow\phi)$

其实这里想要表达的意思是，如果我们有了一套算法或者说流程可以验证TS系统是否满足LTL公式，那么我们可以用相同的流程步骤来检测在加入公平性约束的情况下，TS系统是否满足LTL公式。

对于一个没有终止状态的$TS=⟨S,I,R⟩$，$ \alpha ⊆ Act$，TS上的无限执行片段$ρ =s{0}\xrightarrow{α{0}} s{1}\xrightarrow{α{1}}…$，公平约束具有三种：

1. 如果$\rho$是无条件公平性（unconditionally A-fair），那么无论何时

   $\text{if }\overset{∞}∃ j\ge 0,a_{j}∈A.$

   无条件A-fair的含义是，无论在什么情况下，A中的动作总能无限经常次执行。

2. 如果$\rho$是强公平性（strongly A-fair），那么无论何时

   $(\overset{∞}∃ j.Act(s_{j}\cap A\ne ∅)\Rightarrow(\text{if }\overset{∞}∃ j\ge 0,a_{j}∈A)$

   strongly A-fair的含义是，存在无限经常次A为enabled时，A中动作将会无限经常次执行。

3. 如果$\rho$是弱公平性（weakly A-fair），那么无论何时

   $(\overset{∞}\forall j.Act(s_{j}\cap A\ne ∅)\Rightarrow(\text{if }\overset{∞}∃ j\ge 0,a_{j}∈A)$

   weakly A-fair的含义是，从某个时刻起，A将会为enabled，从而A中动作将会无限经常次执行。

strong和weak引入了enabled这个概念，

strongly A-fair要求在enable的片段中动作能够无限经常次执行，而在not enabled的片段中没有规定

weakly A-fair则是，不管之前如何，如果在某一个时间点之后，动作持续一直enabled，那么在这片段中动作要求能够无限经常次执行。

从上面的定义中我们可以容易得到

$\text{unconditionally A-fair}\Rightarrow \text{strongly A-fair}\Rightarrow \text{weakly A-fair}$

第五部分：$LTL$

时间逻辑TL（Temporal Logic）

时间逻辑TL：用以表达与系统执行相关的属性。不能表达没有明确的转换关系，没有初始状态的概念。

TL逻辑定义为：

• 一种语法：经典逻辑运算符加上时间运算符来谈论未来和过去。
• 语义：对象域（称为模型），我们将在其上测试公式的有效性，以及运算符的解释。

线性时间逻辑LTL（Linear Temporal Logic）

LTL模型

LTL 公式总是与系统的给定迹 $σ$ 相关：迹构成该逻辑的模型。

注意：我们经常说即时而不是状态，以指定迹 $σ$ 的元素。

LTL语法

• $s$：表示s在当前时刻成立，在轨迹表现为在第一个位置成立
• $\neg P$
• $P \lor Q$
• $P \land Q$
• $\bigcirc P$：表示P在下一个时刻成立，在轨迹表现为第二个位置成立
• $\Box P$：表示P总是(always)成立，即在全部的时刻都成立，在轨迹上表现为每个位置都成立，$\Box P=\lnot \Diamond \lnot P$
• $\Diamond P$：表示的是P最终(eventually)能够成立，在轨迹上表现为，在某一个时刻的时候P成立，$\Diamond P = \lnot \Box \lnot P$ : $P$ 不永远为假 $\to$ 存在 $P$ 为真（在这个序列的某个点上 $F$ 为真，哪个点我不关心）
• $\Diamond \Box P$：表示在某一个点之后 $F$ 永远为真。
• $\Box \Diamond P$：表示存在无穷多个点 $F$ 为真。有一个执行序列 $Exec$，任给一个迹 $\sigma$，总要包含一个 $F$ 为真。
• $P \mathcal{U} Q$：表示直到Q成立前，P一直成立
• $P \rightsquigarrow Q$：表示当P成立时，Q一会后也成立。如果 $P$ 在某个点上为真了，那么 $Q$一定在后面的某个点上为真

最小的运算符

最小的运算符是$\bigcirc P$ 和 $P \mathcal{U}Q$：

• $\Diamond P \triangleq True \; \mathcal{U} P$
• $\Box P \triangleq \neg \Diamond \neg P$
• $P \rightsquigarrow Q \triangleq \Box (P ⇒ \Diamond Q)$

替代语法

我们可以使用另一种语法：

• $\Box ↔ G$（Globally）
• $\Diamond ↔ F$（Finally）
• $\bigcirc↔ X$（Next）

互补运算符

运算符 wating-for（或 unless 或 weak-less）: Q 可能最终为真，同时 P 仍然为真

$P\; \mathcal{W}\;Q \triangleq \Box P ∨ P \mathcal{U}Q$

释放运算符

$P \; \mathcal{R} \; Q \triangleq Q \mathcal{U}(P ∧ Q)$Q : 保持为真，直到 P 变为真。

过去式运算符

• $\ominus P$：previous : P 在前一个瞬间为真
• $\boxminus P$：has-always-been : P 一直是真实的直到当前时刻
• $ \diamond P$：once : P 在过去是真的
• $P\; \mathcal{S}\;Q$：since : 自 Q 过去一直为真，而 P 自上次出现 Q 以来一直为真
• $P\; \mathcal{B}\;Q$：back-to : P 自上次出现 Q 以来为真，或者如果 Q 从未为真，则自初始时刻起为真

LTL语义

我们用 $(σ, i)$ 表示后缀为 $⟨s_i → s_i+1 → ...⟩$ 的迹 $σ = ⟨s0 → s1 → ...⟩$

系统验证

系统 $S$ 验证（valid）公式 $F$ 当且仅当 $S$ 的所有执行从初始时刻验证它：

$\frac{\forall σ \in Exec(S):(σ,0) \models F}{S \models F}$

$P\land Q$

$(\sigma,i) \models P \land Q$ 当且仅当$(\sigma ,i) \models P$ 并且 $(\sigma ,i) \models Q$

$\frac{(\sigma,i) \models P\qquad(\sigma,i) \models Q}{(\sigma,i) \models P \land Q}$

$P\lor Q$

$(\sigma,i) \models P \land Q$ 当且仅当$(\sigma ,i) \models P$ 或者 $(\sigma ,i) \models Q$

$\frac{(\sigma,i) \models P}{(\sigma,i) \models P \lor Q} \qquad \frac{(\sigma,i) \models Q}{(\sigma,i) \models P \lor Q}$

$\neg P$

$\frac{\neg (\sigma,i) \models P}{(\sigma,i) \models \neg P}$

$s$

$\frac{\sigma_i=s}{(\sigma,i) \models s}$

$\bigcirc P$

$(\sigma,i) \models \bigcirc P$ 当且仅当对使$suffix(\sigma,1) = \sigma_{1},\sigma_{2},\sigma_{3}...\models P$

$\frac{(\sigma,i+1) \models P}{(\sigma,i) \models \bigcirc P}$

$P\;\mathcal{U}\;Q$

$(\sigma,i) \models P\;\mathcal{U}\;Q$ 存在 $j \ge 0$ 使得 $suffix(\sigma,j)=\sigma_{j},\sigma_{j+1},\sigma_{j+2}...\models Q$ 且 $suffix(\sigma,i)=\sigma_{i}, \sigma_{i+1}, \sigma_{i+2}...\models P$ ，$0\le i\lt 1$

$\frac{\{∃ k \ge 0:(\sigma,i+k) \models Q\} \land \{ \forall k',0 \le k' \le k:(\sigma, i+k')\models P\} } {(\sigma,i) \models P \mathcal{U} Q}$

$\Diamond P$

$(\sigma,i) \models \Diamond P$ 当且仅当存在 $i \ge 0$使得 $\sigma_{j},\sigma_{j+1},\sigma_{j+2}...\models P$

$\frac{∃k \ge 0 :(\sigma ,i+k) \models P}{(\sigma,i) \models \Diamond P}$

$\Box P$

$(\sigma,i) \models \Box P$ 当且仅当对所有 $i \ge 0$使得 $\sigma_{j},\sigma_{j+1},\sigma_{j+2}...\models P$

$\frac{\forall k \ge 0 :(\sigma ,i+k) \models P}{(\sigma,i) \models \Box P}$

$P \rightsquigarrow Q$

$\frac{\{\forall k \ge 0 :(\sigma ,i+k) \models P \} \Rightarrow \{∃ k' \ge k :(\sigma ,i+k') \models Q\} } { (\sigma,i) \models P \rightsquigarrow Q}$

简化为纯逻辑

线性时序逻辑具有这样的表达能力，以至于它可以准确地表示根据转换系统描述的任何操作规范，因此：

• 检查变迁系统 M 是否具有时间属性 $F_{\mathcal{S}pec}$：

$\mathcal{M} \models F_{\mathcal{S}pec}$

• 相当于确定以下各项的有效性：

  $F_{\mathcal{M}} ⇒ F_{\mathcal{S}pec}$

  其中 $F_{\mathcal{M}}$ 是一个公式，准确地表示模型 ${\mathcal{M}}$ 的执行（即它的初始状态、它的转换、它的公平性约束）。

例题（考试必考）

例1

	无公平性	简单公平性($s_1,s_2$)
$s_0 \land \bigcirc s_0$	$n (s_0→{s_1}^ω) $	n
$s_0 \land \bigcirc (s_0 \lor s_1)$	o	o
$\Box (s_0 ⇒ \bigcirc s_0)$	$n (s_0→{s_1}^ω) $	n
$\Box (s_0 ⇒ \bigcirc (s_0 \lor s_1)$	o	o
$\Box (s_0 ⇒ \bigcirc s_1)$	o	o
$\Diamond (s_0 ⇒ \bigcirc s_1)$	$n ({s_0}^ω) $	o
$\Box s_0$	$n (s_0→{s_1}^ω) $	n
$\Diamond \neg s_0$	$n ({s_0}^ω) $	o
$\Diamond \Box s_0$	$n ({s_0}^ω) $	o
$s_0 \mathcal{W} s_1$	o	o
$s_0 \mathcal{U} s_1$	$n ({s_0}^ω) $	o

例2

$Exec(S) = ⟨s_0 \to {s_1}^w⟩, ⟨(s_0 \to {s_1}^+)^w⟩, ⟨(s_0 \to {s_1}^+)^+ \to {s_2}^w⟩$

	无公平性	$\mathcal{W_{eak}F_{airness}}(s_1,s_2)$	$\mathcal{S_{trong}F_{airness}}(s_1,s_2)$
$\Box \Diamond \neg s_1$	$n (s_0→{s_1}^ω) $	o	o
$\Box (s_1 ⇒ \Diamond s_2)$	$n (s_0→{s_1}^ω) $	$n ((s_0→s_1)^ω) $	o
$\Diamond \Box (s_1 \lor s_2)$	$n ((s_0→s_1)^ω) $	n	o
$\Box (s_1 \mathcal{U} s_2)$	$n (s_0→…) $	n	n
$\Box (s_0 ⇒ s_0 \mathcal{U} s_1)$	o	o	o
$\Box(s_0 \mathcal{U} (s_1 \lor s_2))$	o	o	o
$\Box (s_1 ⇒ s_1 \mathcal{U} s_2)$	$n (s_0→{s_1}^ω) $	$n ((s_0→s_1)^ω) $	$n (s0→s1→s0→s1→s2^ω) $
$\Diamond (s_1 \mathcal{U} s_2)$	$n (s_0→{s_1}^ω) $	$n ((s_0→s_1)^ω) $	o
$\Diamond (s_1 \mathcal{W} s_2)$	$n ((s_0→s_1)^ω) $	n	o
$\Box \Diamond (s_1 \mathcal{U} (s_0 \lor s_2))$	$n (s_0→{s_1}^ω) $	o	o

个人理解：以例1中的第一行 $\Box \Diamond \neg s_1 $ 为例，可以将其视为一个条件，意为在该条件下是否满足“无公平性” 和 “$WF(s_1,s_2)$”：

$\Box \Diamond \neg s_1 $ 意为 “对于所有迹，最终都会不出现 $s_1$” ，此时我们需要找出有否所有的迹都符合该条件。

1. 对于“无公平性”：由图可见存在一个迹 $\sigma = ⟨s_0 \to {s_1}^w⟩$ ，并不符合$\Box \Diamond \neg s_1 $ ，所以为n(means no)。

2. 对于“$WF(s_1, s_2)$”：在转换 $s_0 \to s_1$ 下，条件 $\Box \Diamond \neg s_1 $ 并总是成立

3. 对于“$SF(s_1, s_2)$”：在转换 $s_0 \to s_1$ 下，条件 $\Box \Diamond \neg s_1 $ 并会成立

时间逻辑TL属性

安全性

没有什么不好的事情发生（详见第三部分）= 在执行的有限前缀上无效的属性：

• $\Box P$, $\Box (P ⇒ \Box P)$, $P \mathcal{W} Q$, …

活性

美好的事情终会发生 = 始终可以通过扩展运行前缀来验证的属性：

• $\Diamond P$, $P \rightsquigarrow Q$, …

活性与安全性的组合属性

一些活性与安全性的组合属性，例如

• $P \mathcal{U} Q$, $\Box P \land \Diamond Q$, …
• Reponse: $\Box \Diamond P$
• Persistance: $\Diamond \Box P$

不变性

指定系统可达状态的超集（详见第三部分：

$\mathcal{S} \models \Box P$

其中 P 是状态谓词。

稳定性

指定情况发生时的稳定性：

$\mathcal{S} \models \Box(P ⇒ \Box P)$

其中 P 是状态谓词

可能性

指定在某个执行中可能达到满足 $P$ 的某个状态：

• 对于任意 $P$ 是不可能的，但对于 $P$ 是一个状态谓词：

  $\mathcal{S} \nvDash \Box \neg P$

  请注意否定性：$\neg \Box P = \Diamond \neg P$ 但是 $\mathcal{S} \nvDash \Box P \nRightarrow \mathcal{S} \models \Diamond \neg P$

否定性

• 对于 $σ$ 执行：$σ \models ¬P ≡ σ \nvDash P$

• 对于 $\mathcal{S}$ 系统： $\mathcal{S} \models ¬P ⇒ \mathcal{S} \nvDash P$ , 但不是等价的！

  $\mathcal{S} \nvDash P$ 表示至少有一次执行使 Q 无效（ $¬Q$ 有效），但并非所有执行都如此。

  在 LTL 中，我们可以有$ S \nvDash Q ∧ S \nvDash ¬Q$ :

  $$ \frac { {s_0}^+ → {s_1}^w \nvDash \Box s_0}{\mathcal{S} \nvDash \Box s_0} \qquad \frac { {s_0}^w \nvDash \Diamond \neg s_0}{\mathcal{S} \nvDash \Diamond \neg s_0} $$

无限经常

指定 $P$ 在任何执行中都无限地经常为真：

$\mathcal{S} \models \Box \Diamond P$

最终总是

指定 $P$ 最终保持绝对真：

$\mathcal{S} \models \Diamond \Box P$

LTL公式的性质

对偶率(Duality laws)

$\lnot\Box\phi\equiv\Diamond\lnot\phi \\ \lnot\Diamond\phi\equiv\Box\lnot\phi \\ \lnot\bigcirc\phi\equiv\bigcirc\lnot\phi$

幂等律(Idempotence laws)

$\Box\Box\phi\equiv\Box\phi \\ \Diamond\Diamond\phi\equiv\Diamond\phi \\ \phi U(\phi U\psi)\equiv\phi U\psi \\ (\phi U\psi)U\psi\equiv\phi U\psi$

吸收率(Absorption laws)

$\Diamond\Box\Diamond\phi\equiv\Box\Diamond\phi \\ \Box\Diamond\Box\phi\equiv\Diamond\Box\phi$

分配律(Distributive laws)

$\bigcirc(\phi U\psi)\equiv (\bigcirc\phi)U(\bigcirc\psi) \\ \Diamond(\phi \vee\psi)\equiv (\Diamond\phi)\vee(\Diamond\psi) \\ \Box(\phi\wedge\psi)\equiv\Box\phi\wedge\Box\psi$

扩展率(Expansion laws)

$\phi U\psi\equiv\psi\vee(\phi\wedge\bigcirc(\phi U\psi)) \\ \Diamond\phi\equiv\phi\vee\bigcirc\Diamond\phi \\ \Box\phi\equiv\phi\wedge\bigcirc\Box\phi$

扩展率是非常重要的一条性质，之后的LTL模型检测都会基于此。

特别是这个第一条公式，我个人感觉其实它的意思就是基于当前项然后向后走了一步，就拿 $\phi \mathcal{U}\psi$ 来说，它代表 $\psi$ 成立前 $\phi$ 一直成立，

1. 首先看扩展出来的第一个 $\psi$ ，如果当前项是 $\psi$ 那么就代表到达了公式成立的条件，后面的也就可以不用管了；
2. 然后再看第二项 $\phi\wedge\bigcirc(\phi U\psi)$ 如果当前项是 $\phi$ 还没有达到公式成立的条件，那么如果公式成立，对于下一步来说肯定是满足 $\phi \mathcal{U}\psi$ 的。

用公式来表示LT性质

公平性

例如我们可以用它来表示两进程互斥问题中的公平性：

• 无条件的公平性：$\Box \Diamond crit_{i}$
• 强公平性：$\Box \Diamond wait_{i}\rightarrow \Box \Diamond crit_{i}$
• 弱公平性：$\Diamond\Box wait_{i}\rightarrow \Box \Diamond crit_{i}$

Weak until

前面介绍的until操作，它是一种比较强的限制，而weak until操作（或者称为unless）定义为:

$\phi W\psi=(\phi U\psi)\vee\Box\phi ϕWψ=(ϕUψ)∨□ϕ$

也就是说 $\phi \mathcal{W} \psi$ 表示为 $\phi \mathcal{U} \psi$ 成立或者 $\Box\phi$ 成立

weak until和until操作是对偶的，具体表现为：

$\lnot(\phi \mathcal{U}\psi)=(\phi \wedge\lnot\psi)\mathcal{W}(\lnot\phi\wedge\lnot\psi) \\ \lnot(\phi \mathcal{W}\psi)=(\phi \wedge\lnot\psi)\mathcal{U}(\lnot\phi\wedge\lnot\psi)$

weak until和until两者的表达能力是相同的，两者之间可以互换

$\phi \mathcal{U} \psi=(\phi \mathcal{W} \psi)\wedge\lnot\Box\lnot\psi$

也可以用它来表示一些其他属性：

可达性

简单可达性

$\Diamond\psi$

带条件的可达性

$\phi \mathcal{U} \psi$

安全性中的不变性

$\Box\phi$

活性

$\Box(\phi\Rightarrow\Diamond\psi)$

LTL公式的一些例子

Client / Server

Server

指定系统（扮演服务器的角色）总是响应（Q）给定的请求（P）：

$\mathcal{S} \models \Box (P ⇒ \Diamond Q)$

通常称为lead-to：

$\mathcal{S} \models P \rightsquigarrow Q$

Client

指定来自系统（扮演客户端的角色）的请求 P 只要没有有利的响应 Q 就稳定：

$\mathcal{S} \models \Box (P ⇒ P \mathcal{W} Q)$

互斥问题

两个进程不能同时进入临界区：

$\Box(\lnot crit_{1}\vee \lnot crit_{2}) \\ OR \qquad \Box(\forall i,j \in 0..N-1: state[i]=crit \;\land\;state[j]=crit \quad \Rightarrow \quad i=j )$

无饥饿

两个进程可以无限经常次访问临界区：

$(\Box\Diamond w_{1}\Rightarrow\Box\Diamond c_{1})\wedge(\Box\Diamond w_{2}\Rightarrow\Box\Diamond c_{2})\\ OR \qquad \forall i \in 0..N-1:state[i]=waiting \;\rightsquigarrow\; state[i]=crit$

火车轨道通行问题

$\Box(train\_is\_near\rightarrow gate\_is\_close)$

进程通信

$\Box(request\rightarrow \Diamond response)$

第六部分：$TLA^+$

$TLA+$ 逻辑

$TLA+$ 是一种状态机思维，只要初始是正确的，规则是正确的，那么结果就一定是正确的。不管系统经历了怎样的运行路径。（类似于数学归纳法）

逻辑表达式

带有 $\Box$ , $\Diamond$ , $\rightsquigarrow$的 LTL 表达式和引发变量 + 量词 $∀$，$∃$。

没有 $\mathcal{U}$，也没有 $\mathcal{W}$，但是：

• $\Box (p ⇒ (p \mathcal{W}q)) = \Box (p ⇒ (p' \lor q))$
• $\Box (p ⇒ (p \mathcal{U}q)) = \Box (p ⇒ (p' \lor q)) \land \Box(p ⇒ \Diamond q)$

公平性

ENABLE

$_{ENABLE} \mathcal{A}$ 是在状态 $s$ 中为真的状态函数，当且仅当存在通过动作 $\mathcal{A}$ 从 $s$ 可访问的状态 t。

弱/强公平

• $\mathcal{WF}_e(\mathcal{A}) \triangleq \Box \Diamond \neg (_{ENABLE} ⟨\mathcal{A}⟩_e) \lor \Box \Diamond ⟨\mathcal{A}⟩_e$

  如果 $\mathcal{A}$ 是持续可触发的，它将被触发。

• $\mathcal{SF}_e(\mathcal{A}) \triangleq \Diamond \Box \neg (_{ENABLE} ⟨\mathcal{A}⟩_e) \lor \Box \Diamond ⟨\mathcal{A}⟩_e$

  如果 A 是无限频繁可触发的，它将被触发。

TLA+ 规范的形式

通常，TLA+ 规范是一系列谓词的连词(conjonction)：

$\mathcal{I} \land \Box [\mathcal{N}]_v \land \mathcal{E}$

• $\mathcal{I}$ = 描述初始状态的状态谓词；
• $\mathcal{N}$ = 动作 $A_1 ∨ A_2 ∨ A_3 ∨… $的分解(disjonction)；
• $\mathcal{E}$ = 行动公平性约束的合取(conjonction)：$\mathcal{WF}_v(\mathcal{A}_1) \land \mathcal{WF}_v(\mathcal{A}_3) \land ...$

规约的细化

如果 $P_c ⇒ P_a$，则一个具体的规约 $P_c$ 细化（raffine）一个抽象的规约 $P_a$：$P_c$ 所做的一切在 $P_a$ 中都是可能的。

这意味着如果 $P_a \models P$ 满足 LTL 属性，则 $P_c \models P$ 也满足LTL属性。

例1

-----------------module somme1----------------
EXTENDS Naturals
CONSTANT N
VARIABLE res

TypeInvariant == res \in Nat
Init == res = 0
Next == res′ = ((N + 1) * N) / 2
Spec == Init ∧ [][Next]_res /\ WF_res (Next)

当 $N = 3$ 时的执行图:

例2

----------------- module somme2 ----------------
EXTENDS Naturals
CONSTANT N
VARIABLE res, acc, disp

TypeInvariant == res \in Nat
		/\ acc \in Nat
		/\ disp \in SUBSET 1..N
Init == res = 0
	/\ acc = 0
	/\ disp = 1..N
Next == \/ \E i \in disp : acc' = acc + i /\ disp' = disp \ {i}
					/\ UNCHANGED res
	\/ disp = {} /\ res' = acc /\ UNCHANGED res
Spec == Init ∧ [][Next]_<<res, disp, acc>> /\ WF_<<res, disp, acc>> (Next)

当 $N = 3$ 时的执行图:


分解：引入中间转换

---------------- module somme2_raffine_somme1 ----------------
EXTENDS somme2
Orig == INSTANCE somme1
Raffinement == Orig ! Spec
THEOREM Spec => Orig ! Spec

例3

----------------- module somme3 ----------------
EXTENDS Naturals
CONSTANT N
VARIABLE res, acc, i

TypeInvariant == res \in Nat
		/\ acc \in Nat
		/\ i \in 1..N
Init == res = 0
	/\ acc = 0
	/\ i = N
Next == \/ i > 0 /\ acc' = acc + i /\ i' = i - 1 /\ UNCHANGED res
	\/ i = 0 /\ res' = acc /\ UNCHANGED <<i, res>>
Spec == Init ∧ [][Next]_<<res, i, acc>> /\ WF_<<res, i, acc>> (Next)

当 $N = 3$ 时的执行图:

减少非确定性 + 表示变化（数据细化） $disp = 1..i$

---------------- module somme3_raffine_somme2 ----------------
EXTENDS somme3
dispMapping == 1..i
Orig == INSTANCE somme2 WITH disp <- dispMapping
Raffinement == Orig ! Spec
THEOREM Spec => Orig ! Spec

公理证明

简单时序逻辑

$\frac{F 在命题逻辑中可证明}{\Box F} \;STL1$

意义：

$\frac{}{\Box F ⇒ F} \;STL2$

$\frac{}{\Box \Box F = \Box G} \;STL3$

$\frac{F ⇒ G}{\Box F ⇒ \Box G} \;STL4$

$\frac{}{\Box (F \land G) = (\Box F) \land (\Box G)} \;STL5$

$\frac{}{ (\Diamond \Box F) \land (\Diamond \Box G) = \Diamond \Box (F \land G)} \;STL6$

不变性

$\frac{P \land (v' = v) ⇒ P'}{\Box P = P \land \Box [P ⇒ P']_v} \;TLA1$

$\frac{P \land [\mathcal{A}]_{v1} ⇒ Q \land [\mathcal{B}]_{v2}}{\Box P \land \Box [\mathcal{A}]_{v1} ⇒ \Box Q \land \Box[\mathcal{B}]_{v2}} \;TLA2$

$\frac{I \land [\mathcal{N}]_{v} ⇒ I'}{I \land \Box[\mathcal{N}]_{v} ⇒ \Box I} \;INV1$

$\frac{}{\Box I ⇒ (\Box[\mathcal{N}]_{v} = \Box [\mathcal{N} \land I \land I']_v)} \;INV2$

活性

$\frac{\begin{aligned} P \land [\mathcal{N}]_v ⇒ (P' \lor Q') \\ P \land ⟨\mathcal{N} \land \mathcal{A}⟩_v ⇒ Q' \\ P ⇒ _{ENABLE} ⟨\mathcal{A}⟩_v\end{aligned}}{\Box [\mathcal{N}]_v) \land WF_v(\mathcal{A}) ⇒ (P \rightsquigarrow Q)} \;WF1$

$\frac{\begin{aligned} P \land [\mathcal{N}]_v ⇒ (P' \lor Q') \\ P \land ⟨\mathcal{N} \land \mathcal{A}⟩_v ⇒ Q' \\ \Box P \land \Box [\mathcal{N}]_v \land \Box F ⇒ \Diamond _{ENABLE} ⟨\mathcal{A}⟩_v\end{aligned}}{\Box [\mathcal{N}]_v) \land SF_v(\mathcal{A}) \land \Box F ⇒ (P \rightsquigarrow Q)} \;WF1$

推导规则

$\frac{\Box(P ⇒ \Box P) \land \Diamond P}{\Diamond \Box P} \;LDSTBL$

$\frac{P \rightsquigarrow Q \land Q \rightsquigarrow R}{P \rightsquigarrow R} \;TRANS$

$\frac{\forall m \in W : P(m) \rightsquigarrow Q}{(∃ m \in W : P(m)) \rightsquigarrow Q} \;INFDIJ$

模型检查

原则：构建执行图并研究属性。

• $\Box P$，其中 $P$ 是一个状态谓词（没有初始变量）：随着状态的构建。
• $\Box P (v,v')$，其中 $P(v,v')$ 是一个转换谓词（具有带素变量和非素数变量的非时间谓词）：计算转换时。
• 活跃度 $\Diamond P$ , $P \rightsquigarrow Q$ , … ：一旦建立了图，寻找一个尊重公平约束并使属性无效的循环。

复杂度

让系统 $\mathcal{S} = ⟨S, I, R⟩$ 的状态数$|S|$ 和 LTL的 $\mathcal{F}$ 公式的大小$|F|$（时间运算符的数量）。

验证 $\mathcal{S} \models \mathcal{F}$ 的时间（和空间）复杂度为

$O(|S| × 2^{|F|})$

TLC检查器

TLC 模型检查器可以检查：

1. 带有保护的动作的规约；

2. 没有初始变量的不变量 $\Box P$，其中 P 是状态谓词；

3. 带有素变量（prime variables ）和重复（begaiement）的纯安全公式 $\Box [P]_v$ , 其中 P 是转换谓词；

4. $P \rightsquigarrow Q$ , 其中 P 和 Q 是状态谓词（没有素变量）；

5. 将 $\Box$、$\Diamond $ 组合在一起的公式，没有带底数的变量。

   注意：系统和公式的状态空间必须是有限的：例如任何有界量化。

第七部分：$CTL$

在前面我们已经介绍了线性属性，为了方便地去描述这个线性属性，我们又介绍了线性时序逻辑，本节要介绍一种新的逻辑计算树逻辑（CTL），这种逻辑可以描述LTL不能描述的部分。

如果用文氏图来表示的话就是：

---

让我们先来回想一下LTL之所以称为线性的，是因为时间的定性概念是基于路径的，并且被视为线性的：在每个时刻只有唯一的一个可能的后继状态，因此每个时刻都有一个唯一的可能的未来。 从技术上讲，这是基于以下事实：LTL公式的解释是根据路径（即状态序列）定义的。

但是路径本身可能存在着分支，例如在一个TS系统中，一个状态也许有着多个后继状态，从这个角度来看这种解释是基于状态分支的。我们想到，某些时候在一个状态的所有可能计算都满足某个条件，或者有些时候一个状态的部分可能计算满足某个条件，为了表述这些个性质，我们加入$\forall$ 和 $∃$ 符号。

LTL描述的从某个状态开始所有的路径情况，例如$s \models \Box(x\le 20)$，它表示对于从s开始的所有路径都满足 $x\le 20$

而CTL描述的是从某个状态开始的所有或部分路径情况

例如$s\models \forall\Box(x\le 20)$,它表示对于从s开始的所有路径都满足$x\le 20$ , 而 $s\models∃\Box(x\le 20)$表示对于从s开始的某些路径满足$x\le 20$

线性时间 vs 分支时间

	linear time	branching time
行为behavior	path-based:trace(s)	state-based:computation tree of s
时间逻辑temporal logic	LTL path formulas	CTL state formulas
模型检测	$PSPACE-complete O(size(TS)·2^{\mid\phi\mid})$	$PTIME O(size(TS)·\mid\phi\mid)$
公平性	可以直接表示	需要额外的技术

执行集 vs 执行树

• 执行集：$Exec(S) = ⟨({s_0}^+ → s_1 → s_2)^∗ → {s_0}^ω⟩,⟨({s_0}^+ → s_1 → s_2)^ω⟩,⟨({s_0}^+ → s_1 → s_2)^+ → s_3^ω⟩$

• 执行树：

  

计算树逻辑CTL

模型描述

CTL 公式始终与系统的给定状态 s 相关，迹 Trace(s) 源自该状态。S 的状态构成了这个逻辑的模型。

与 LTL 的区别（从句法上讲）在于迹量词的时间运算符的出现。

CTL 语义

CTL状态公式的语义

$ s\models a$

当且仅当 $a∈L_(s)$

$\frac{}{s \models a}$

$s\models P \land Q$

当且仅当 $s\models P$ 并且 $s\models Q$

$\frac{s \models P \qquad s \models Q}{s \models P \land Q}$

$s \models P \lor Q$

当且仅当 $s \models P$ 或者 $s \models Q$

$\frac{s \models P}{s \models P \lor Q} \qquad \frac{s \models Q}{s \models P \lor Q}$

$s\nvDash \neg P$

当且仅当 $ s\models P$

$\frac{s \models P}{s \nvDash \neg P}$

$s\models ∃ φ$

当且仅当 $\pi\vDash\phi$ 对于某些从s开始的路径成立

$s\models \forall φ$

当且仅当 $\pi\vDash\phi$ 对于所有从s开始的路径成立

CTL路径公式的语义

• $\pi\vDash\bigcirc P$ 当且仅当 $\pi[1]=P$
• $\pi\vDash P \mathcal{U} Q$ 当且仅当存在 $j\ge0$ 使得 $s_{j}\vDash Q$ 且对于 $0\le k\lt j,\pi[k]\vDash P$

CTL在TS上的语义

对于一个CTL公式 $\phi$，它的可满足集合(satisfaction set) $Sat(\phi)$ 定义为 :

$Sat(\phi)=\{s\in S | s\vDash \phi\}$

说白了就是一些满足CTL公式$\phi$的状态的集合

如果我们说一个TS满足CTL公式 $\phi$ , 那么当且仅当公式 $\phi$ 在所有的初始状态上成立，用公式表示为：

$TS\vDash\phi\text{ 当且仅当 }S_{0}\subseteq Sat(\phi) \text{ 当且仅当 }\forall s_{0}\in S_{0}.s_{0}\vDash\phi$

上面的 $S_{0}$ 就是初始状态的集合

全称量词 : 从 s 开始的任何轨迹（对于 s 状态）

提醒：对于迹 $\sigma$，$\sigma_i$ 是从 0 开始的 $\sigma$ 的第 i 个元素，对于状态 s，Traces(s) 是来自 s 的迹线集合）

$s \models \forall \bigcirc P$

P 在下一瞬间为真

$\frac{\forall \sigma \in Traces(S) :a_1 \models P}{s \models \forall \bigcirc P}$

$s \models \forall \Box P$

P 在每个状态下始终为真

$\frac{\forall \sigma \in Traces(S) : \forall i \ge 0 :a_i \models P}{s \models \forall \Box P}$

$s \models \forall \Diamond P$

P 最终为真（未来）

$\frac{\forall \sigma \in Traces(S) : ∃ i \ge 0 :a_i \models P}{s \models \forall \Diamond P}$

$s \models P\;\forall\;\mathcal{U}\;Q$

P 最终为真，同时 P 仍然为真

$\frac{\forall \sigma \in Traces(S) : ∃ j \ge 0 :a_j \models Q \land \forall i < j : \sigma_i \models P}{s \models P\;\forall\;\mathcal{U}\;Q}$

存在量词 : 从 s 开始的至少一条迹线（对于 s 状态）

$s \models ∃ \bigcirc P$

P 在下一瞬间为真

$\frac{∃ \sigma \in Traces(S) :a_1 \models P}{s \models ∃ \bigcirc P}$

$s \models ∃ \Box P$

P 在每个状态下始终为真

$\frac{∃ \sigma \in Traces(S) : \forall i \ge 0 :a_i \models P}{s \models ∃ \Box P}$

$s \models ∃ \Diamond P$

P 最终为真（未来）

$\frac{∃ \sigma \in Traces(S) : ∃ i \ge 0 :a_i \models P}{s \models ∃ \Diamond P}$

$s \models P\;∃\;\mathcal{U}\;Q$

Q 最终为真，同时 P 仍然为真

$\frac{∃ \sigma \in Traces(S) : ∃ j \ge 0 :a_j \models Q \land \forall i < j : \sigma_i \models P}{s \models P\;∃\;\mathcal{U}\;Q}$

$\forall \bigcirc$，$∃ \bigcirc$ 图解

$\forall \Box$，$∃ \Box$ 图解

$\forall \Diamond$，$∃ \Diamond$ 图解

$\forall \mathcal{U}$，$∃ \mathcal{U}$ 图解

CTL 语法

最小运算符

$\{ \forall \bigcirc , \forall \mathcal{U}, ∃ \mathcal{U}\} \lor \{ ∃ \bigcirc , ∃ \Box, ∃ \mathcal{U}\} \lor \{ ∃ \diamond , ∃ \mathcal{U}, ∃ \bigcirc \}$

• $∃ \bigcirc P \triangleq \neg \forall \neg P$
• $\forall \Diamond P \triangleq True \; \forall \mathcal{U} P$
• $∃ \Diamond P \triangleq True \; ∃ \mathcal{U} P$
• $\forall \Box P \triangleq \neg ∃ \Diamond \neg P$
• $∃ \Box P \triangleq \neg \forall \Diamond \neg P$

替代语法

• $∀ ↔ A$ (all)
• $∃ ↔ E$ (exists)
• $\Box ↔ G$ (globally)
• $\Diamond ↔ F$ (finally)
• $\bigcirc ↔ X$ (next)
• $\mathcal{U} ↔ U$ (until)

互补运算符

• $P∃ \mathcal{W}Q \triangleq ∃ \Box P \lor P ∃ \mathcal{U} Q$
• $P\forall \mathcal{W}Q $ 不等于 $ \forall \Box P \lor P \forall \mathcal{U} Q$；$P\forall \mathcal{W}Q \triangleq \neg (\neg Q ∃ \mathcal{U} (\neg P \land \neg Q))$

否定性

与 LTL 不同，对于任何 CTL 属性，我们有：

$S \models F，或\; S \models \neg F， 或\; S \nvDash F ≡ S \models ¬F。$

公式的否定$ ∀, ∃, \Box, \Diamond$

对基于 $ ∀, ∃, \Box, \Diamond$ 的公式的求反只需将每个运算符反转为对偶即可。

例：

• $¬(∀ \Diamond ∃ \Box p) = ∃\Box ∀\Diamond ¬p$

• $(∀\Diamond ¬s_0 ⇒ ∀\Diamond s_3) = (∃\Box s_0 ∨ ∀\Diamond s_3) \qquad 因为 (p ⇒ q) = (¬p ∨ q)$

定点定义

一旦定义了 $∃\bigcirc$ 和 $∀\bigcirc$，每个操作符就是最小的点

其归纳定义：

• $∀ \Box f = f ∧ ∀ \bigcirc ∀ \Box f$

• $∃ \Box f = f ∧ ∃ \bigcirc ∃ \Box f$

• $∀ \Diamond f = f ∨ ∀ \bigcirc ∀ \Diamond \Box f$

• $∃ \Diamond f = f ∨ ∃ \bigcirc ∃ \Diamond \Box f$

• $f ∀ \mathcal{U} g = g ∨ (f ∧ ∀\bigcirc (f ∀ \mathcal{U} g))$

• $f ∃ \mathcal{U} g = g ∨ (f ∧ ∃\bigcirc (f ∃ \mathcal{U} g))$

  （对于实现模型检查器特别有用）

第八部分：$LTL \; vs \; CTL$

LTL和CTL的等价

由之前的一张图我们看到，CTL和LTL有部分的表达是有交集的，这部分既可以用LTL表达，又可以用CTL表达，那么如何形式化地定义等价这个概念呢？

如果一个LTL公式 $φ$ 和一个CTL公式 $\Phi$ 是等价的（记为 $φ\equiv\Phi$），那么当且仅当，对于AP上的TS来说

$TS\vDash φ\Leftrightarrow TS\vDash\Phi$

例如有这些个公式是等价的

CTL公式 $\Phi$	LTL公式 $φ$
$a$	$a$
$ \forall\bigcirc a$	$\bigcirc a$
$\forall(a\mathcal{U}b)$	$a\mathcal{U}b$
$\forall\Box a$	$\Box a$
$\forall\Diamond a$	$\Diamond a$
$\forall(a\mathcal{W}b)$	$a\mathcal{W}b$
$\forall\Box\forall\Diamond a$	$\Box\Diamond a$

LTL和CTL各自能表达的部分

由上面的文氏图我们知道，LTL和CTL的表达能力并不完全等价，因为存在着只要有各自能够表达的部分

某些LTL公式不能表示成CTL公式，例如

• $\Diamond\Box a$
• $\Diamond(a\land\bigcirc a)$

某些CTL公式不能表示成LTL公式，例如

• $\forall\Diamond\forall\Box a$
• $ \forall\Diamond(a\land\forall\bigcirc a)$
• $\forall\Box\exist\Diamond a$

不等价案例

$\Diamond(a\wedge\bigcirc a)$ 与 $ \forall\Diamond(a\wedge\forall\bigcirc a)$ 不等价

例如下面这张图：

我们可以看到它能表示LTL公式 $ \Diamond(a\land\bigcirc a)$，但是不能表示CTL公式$\forall\Diamond(a\land\forall\bigcirc a)$，因为看到 $S_{0},S_{3}$这条路径，对于用CTL表示的 $\forall\Diamond(a\wedge\forall\bigcirc a)$ 来说，从 $S_{0}$ 的角度看，它不满足所有的下一个状态 $a$ 成立。

再看另一个例子，$\Diamond\Box a$ 和 $\forall\Diamond\forall\Box a$ 不等价

就如下图所示

它能够表示LTL公式 $\Diamond\Box a$，但是不能表示CTL公式 $\forall\Diamond\forall\Box a$，我们把它的计算树画出来

我们看到最左边的那条路径，也就是说如果走的路径为 $S_{0}S_{0}S_{0}S_{0}S_{0}S_{0}...$ S 那么就会有一条路径不满足$\forall\Diamond\forall\Box a$。

模型检测的复杂度

LTL模型检测的时间复杂度为

$O(|TS|·2^{|\phi|})$

CTL模型检测的时间复杂度为

$O(|TS|·|\phi|)$