# 模型检验与时序逻辑

对计算机系统的正确性进行验证有很多好处，尤其是对于安全性要求较高的及系统，这其实也适用于商业关键系统。

***形式化验证方法(Formal verification)*** 在近几年被工业界大量使用，形式化验证技巧被认为由三个部分组成：

- 一个模型系统框架，通常为某种描述语言

- 一个规范语言用来描述待验证的形式

- 一个验证方法用来确定系统的描述是否符合规范

根据验证方法可以分类为：

- 基于证明(proof-based) / 基于模型(model-based): 在基于证明的方法中，模型系统描述为一个公式的集合` $\Gamma$ `，而规范是另外一个公式` $\phi$ `。验证方法为找到一个证明，使得` $\Gamma \vdash \phi$ `成立；在基于模型的方法中，模型系统为一个模型` $\mathcal{M}$ `，规范为一个公式` $\phi$ `，验证方法为计算模型是否满足` $\phi$ `（即` $\mathcal{M} \models \phi$ `）。

- 自动化程度(degree of automation) ： 根据自动化程度可以对形式化验证方法进行分类，最极端的是完全自动和完全手动的。但许多计算机辅助技术是居于两者之间。

- 完全验证(full-verification) / 性质验证(property-verification) : 规范由可能描述系统的单个性质，或者描述其全部行为，往往后者验证起来很昂贵。

- 应用领域(intended domain of application) : 例如硬件或者软件，顺序的还是并行的，反应式还是终止的等。

> 补充： 反应式系统指的式根据环境做出反应且不会终止，例如操作系统，嵌入式系统以及计算机硬件

- 开发前(pre-development) / 开发后(post-development) : 在开发工程的早期阶段进行验证具有很大的优势，因为在生产周期的早期阶段，捕获错误的纠正成本更低。

我们介绍一种验证方法为 ***模型检验(model checking)***， 根据上述的分类，模型检验式一种自动化的，基于模型，性质验证的方法。它通常被期望应用于并行的反应式系统。

模型检验基于时序逻辑，即一个公式在一个模型中并不是恒为真或假；在时序逻辑中的模型包含几个状态，一个公式在某些状态中为真，另一些状态为假。

在模型检验中，模型` $\mathcal{M}$ `为 ***转移系统(transition systems)*** ，性质为时序逻辑中的公式` $\phi$ `。为了验证一个系统满足某个性质，我们需要做：

- 使用模型检验器的描述语言模型化系统，形成一个模型` $\mathcal{M}$ `

- 使用模型检验器的规范语言编码性质，形成一个时序逻辑公式` $\phi$ `

- 根据输入的` $\mathcal{M},\phi$ `运行模型检验器

最终模型检验器输出“是”(如果` $\mathcal{M} \models \phi$ `)或者“否”。对于后者，大多的模型检验器还会产生一个系统行为追踪，用来追溯失败原因。


## 线性时序逻辑 LTL

### LTL 语法

***线性时序逻辑(Linear-time Temporal Logic, LTL)*** 有如下的语法（以BNF形式给出）： 

```math
\phi ::= \top \ | \ \bot \ | \ p \ | \ (\neg \phi) \ | \ (\phi \wedge \phi) \ | \ (\phi \vee \phi) \ | \ (\phi \rightarrow \phi) \ | \\ (X \phi) \ | \ (F \phi) \ | \ (G \phi) \ | \ (\phi U \phi) \ | \ (\phi W \phi) \ | \ (\phi R \phi) 
```

其中` $p$ `是原子，第一行定义我们已经比较熟悉；第二行是时序逻辑特有的连接词，` $X$ `表示“接下来的状态是”；` $F$ `表示“未来的某个状态是”；` $G$ `表示“未来所有状态是”；` $U$ `表示“直到（前者）结束后状态变为（后者）”；` $R$ `表示“在到达（前者）状态前（后者）成立 或者 （后者）始终成立”；` $W$ `表示“直到（前者）结束后状态变为（后者） 或者 （后者）始终成立”

> 在笔记来源的教材中，分别称` $U,R,W$ `为“直到(until)”，“释放(release)”，“弱-直到(weak-until)”；此处描述不甚清晰，读者可以移步下文的语义部分

> 补充：为了减少括号，根据传统时序逻辑的优先级为： 一元连接词(` $\neg,X,F,G$ `)，` $U$ ` ，` $R$ ` ，` $\wedge$ `和` $\vee$ `，最后是` $\rightarrow$ `。

### LTL 语义

下面给出LTL的模型（即转移系统）：

一个转移系统` $\mathcal{M} = （S,\rightarrow,L）$ `是一组状态` $S$ `、转移关系` $\rightarrow$ `（使得对于每个` $s \in S$ `，总有某个` $s' \in S$ `满足` $s \rightarrow s'$ `）以及一个标记函数` $L : S \rightarrow \mathcal{P}(Atoms)$ `。

> 注意： 这里` $s \rightarrow s'$ ` 意味着系统中没有状态会进入到“死锁”状态

在一个模型` $\mathcal{M} = (S,\rightarrow,L)$ `中，***路径(path)*** 是一个` $S$ `中无限的状态序列` $s_1,s_2,s_3,...$ `，对于每个` $i \ge 1$ `，有` $s_i \rightarrow s_{i + 1}$ `。我们将路径写为` $s_1 \rightarrow s_2 \rightarrow ...$ `。

特别的，我们` $\pi^i$ `表示从` $s^i$ `开始的后缀，即` $\pi^i = s_3 \rightarrow s_4 \rightarrow ....$ `。

> 补充： 或者` $\pi^i(n) = \pi(i + n)$ `

通过将状态系统延展为路径，我们可以很清晰看到模型的执行过程。

令` $\mathcal{M} = (S,\rightarrow,L)$ `为一个模型，并且` $\pi = s_1 \rightarrow ...$ `为一个` $\mathcal{M}$ `的一个路径。那么路径` $\pi$ `是否满足LTL公式由满足性关系` $\models$ `定义：

1 . ` $\pi \models \top$ `

2 . ` $\pi \not \models \bot$ `

3 . ` $\pi \models p$ ` iff ` $p \in L(s_1)$ `

4 . ` $\pi \models \neg \phi$ ` iff ` $\pi \not \models \phi$ ` 

5 . ` $\pi \models \phi_1 \wedge \phi_2$ ` iff ` $\pi \models \phi_1$ ` and ` $\pi \models \phi_2$ `

6 . ` $\pi \models \phi_1 \vee \phi_2$ ` iff ` $\pi \models \phi_1$ ` or ` $\pi \models \phi_2$ `

7 . ` $\pi \models \phi_1 \rightarrow \phi_2$ ` iff 当` $\phi \models \phi_1$ `成立时，` $\pi \models \phi_2$ ` 成立

8 . ` $\pi \models X \phi$ ` iff ` $\pi^2 \models \phi$ `

9 . ` $\phi \models G \phi$ ` iff 对于任意的` $i \ge 1$ `，有` $\pi^i \models \phi$ `

10 . ` $\pi \models F \phi$ ` iff 存在某个` $i \ge 1$ `使得` $\pi^i \models \phi$ `

11 . ` $\pi \models \phi U \psi$ ` iff 存在某个` $i \ge 1$ `使得` $\pi^i \models \psi$ `且对任意的` $j = 1,...,i-1$ `，有` $\pi^j \models \phi$ `

12 . ` $\pi \models \phi W \psi$ ` iff 或者存在某个` $i \ge 1$ `使得` $\pi^i \models \psi$ `且对于任意的` $j = 1,...,i-1$ `我们有` $\pi^j \models \phi$ `;或者对于任意的` $k \ge 1$ `我们有` $\pi^k \models \phi$ `

13 . ` $\pi \models \phi R \psi$ ` iff 或者存在某个` $i \ge 1$ `使得` $\pi^i \models \phi$ `且对任意的` $j = 1,...,i$ `我们有` $\pi^j \models \psi$ `;或者对任意的` $k \ge 1$ `我们有` $\pi^k \models \psi$ `

假设` $\mathcal{M} = (S,\rightarrow,L)$ `是一个模型，` $s \in S$ `，且` $\phi$ `是一个LTL公式。` $\mathcal{M},s \models \phi$ `表示如果对于` $\mathcal{M}$ `的任意以` $s$ `开始的可执行路径` $\pi$ `，我们有` $\pi \models \phi$ `；` $\mathcal{M} \models \phi$ `表示对于任意的路径` $\pi$ `，有` $\pi \models \phi$ `;` $\ \models \phi$ `表示对于任意的模型` $\mathcal{M}$ `，有` $\mathcal{M} \models \phi$ `。


### LTL公式的等价关系

如果对于任意的模型` $\mathcal{M}$ `和所有` $\mathcal{M}$ `中的路径` $\pi$ `有` $\pi \models \phi$ `当且仅当` $\pi \models \psi$ `，我们称两个LTL公式` $\phi$ `和` $\psi$ `（语义）等价，写作` $\phi \equiv \psi$ `。

我们已经知道命题逻辑中的等价关系，下面给出LTL特有的等价关系：

` $F$ `和` $G$ `是对偶的，` $X$ `与其自身是对偶的：

- ` $\neg G \phi \equiv F \neg \phi$ `

- ` $\neg F \phi \equiv G \neg \phi$ `

- ` $\neg X \phi \equiv X \neg \phi$ `

` $U$ `和` $R$ `是对偶的：

- ` $\neg (\phi U \psi) \equiv \neg \phi R \neg \psi$ `

- ` $\neg (\phi R \psi) \equiv \neg \phi U \neg \psi$ `

另外，` $F$ `和` $G$ `分别关于` $\vee$ `和` $\wedge$ `是分配的，即：

- ` $F (\phi \vee \psi) \equiv F \phi \vee F \psi$ `

- ` $G (\phi \wedge \psi) \equiv G \phi \wedge G \psi$ `

“直到”与“弱直到”是具有关联性的，` $U$ `可以看作` $W$ `附加了“终止必须出现的限制”的条件：

- ` $\phi U \psi \equiv \phi W \psi \wedge F \psi$ `

或者说，` $W$ `是` $U$ `放宽了“终止可以永远不出现”的条件：

- ` $\phi W \psi \equiv \phi U \psi \vee G \phi$ `

` $W$ `和` $R$ `在表述上也有一定的近似，可以将其使用等价关系联系起来：

- ` $\phi W \psi \equiv \psi R (\phi \vee \psi)$ `

- ` $\phi R \psi \equiv \psi W (\phi \wedge \psi)$ `

### LTL 连接词充分集合

LTL 连接词充分集合指的是集合内的连接词可以表达全部公式，而无需冗余的连接词。在命题逻辑中，如` $\{\bot,\wedge,\neg\}$ `、` $\{\vee,\rightarrow,\top\}$ `等都是连接词充分集合。

在LTL中，` $X$ `与其他连接词完全正交，因此在充分集合中必须含有` $X$ `，我们给出三个完备集合` $\{U,X\}、\{R,X\}、\{W,X\}$ `。

- 对于` $\{U,X\}$ `，` $R$ `和` $W$ `可以被` $U$ `定义，即` $\phi R \psi \equiv \neg (\neg \phi U \neg \psi)$ `和` $\phi W \psi \equiv \psi R (\phi \vee \psi)$ `（后者需要进一步使用前者化归）

- 对于` $\{R,X\}$ `，` $U$ `和` $W$ `可以被` $R$ `定义，即` $\phi U \psi \equiv \neg (\neg \phi U \neg \psi)$ `和` $\phi W \psi \equiv \psi R (\phi \vee \psi)$ `

- 对于` $\{W,X\}$ `，` $R$ `和` $U$ `可以被` $W$ `定义，即` $\phi R \psi \equiv \psi W (\phi \wedge \psi)$ `和` $\phi U \psi \equiv \neg (\neg \psi R \neg \psi)$ `（后者需要进一步使用前者化归）

**定理** 等价关系` $\phi U \psi \equiv \neg (\neg \psi U (\neg \phi \wedge \neg \psi)) \wedge F \psi$ `成立对任意的LTL公式` $\phi$ `和` $\psi$ `。

> 提示： 实际上，右侧使用等价替换后记为` $(\phi W \psi) \wedge \psi$ `，即“弱直到”加强了终止出现的条件，也就是“直到”

### LTL 模型检验：系统，工具与性质 

## 计算树逻辑 CTL

在LTL中，我们知道LTL公式依赖于路径计算，我们定义一个系统的状态满足一个LTL公式，如果从该状态出发的所有路径都满足这个公式。因此LTL隐式地在路径上使用了全称量化。这也导致了对于存在性路径我们无法通过LTL进行表示。

***计算树逻辑(Computation Tree Logic, CTL)*** 允许对路径显式使用量词。在CTL中除了LTL中特有连接词` $U,F,G,X$ `外，还增加了` $A,E$ `分别表示“全部路径”和“存在一个路径”。

### CTL 语法

CTL公式的BNF形式如下：

```math
\phi ::= &\bot \ | \ \top \ | \ p \ | \ (\neg \phi) \ | \ (\phi \wedge \phi) \ | \ (\phi \vee \phi) \ | \ (\phi \rightarrow \phi) \ | \\& A X \phi \ | \ EX \phi \ | \ AF \phi \ | \ EF \phi \ | \ AG \phi \ | \ EG \phi \ | \ A [\phi U \phi] \ | \ E [\phi U \phi]    
```

> CTL 连接词的集合优先级与命题逻辑和谓词逻辑比较相似，首先一元连接词结合最紧密(` $\neg,AG,EG,AF,EF,AX,EX$ `)，其次是` $\wedge,\vee$ `，最后是` $\rightarrow,AU,EU$ `

值得注意的是，CTL语法中的量词与谓词逻辑中量词行为并不完全类似，在定义中， ` $A$ `和` $E$ `后必须跟随` $G,F,X,U$ `其中之一.这也表示CTL也不允许直接嵌套路径连接词，例如不能存在` $F G p$ `;同时也不允许对路径使用布尔连接词，例如` $A [F p \vee F q]$ `是不合法的。

> 提示： 我们后面将介绍CTL的加强版CTL*，其去除了CTL的诸多限制

### CTL 语义

令` $\mathcal{M} = (S,\rightarrow,L)$ `是CTL的一个模型，` $s$ `在` $S$ `中，` $\phi$ `是一个CTL公式。则CTL语义由如下结构归纳定义：

1 . ` $\mathcal{M}, s \models \top $ ` 以及 ` $\mathcal{M},s \not \models \bot$ `

2 . ` $\mathcal{M},s \models p$ ` iff ` $p \in L(s)$ `

3 . ` $\mathcal{M},s \models \neg \phi$ ` iff ` $\mathcal{M},s \not \models \phi$ `

4 . ` $\mathcal{M},s \models \phi_1 \wedge \phi_2$ ` iff ` $\mathcal{M},s \models \phi_1$ ` 且 ` $\mathcal{M},s \models \phi_2$ `

5 . ` $\mathcal{M},s \models \phi_1 \vee \phi_2$ ` iff ` $\mathcal{M},s \models \phi_1$ `或者` $\mathcal{M},s \models \phi_2$ `

6 . ` $\mathcal{M},s \models \phi_1 \rightarrow \phi_2$ `iff ` $\mathcal{M},s \not \models \phi_1$ `或者` $\mathcal{M},s \models \phi_2$ `

7 . ` $\mathcal{M},s \models AX \phi$ `iff 对于任意的` $s_1$ `满足` $s \rightarrow s_1$ `，我们有` $\mathcal{M},s_1 \models \phi$ ` （即对于任意的下一个状态，满足` $\phi$ `）

8 . ` $\mathcal{M},s \models EX \phi$ `iff 对于某个` $s_1$ `满足` $s \rightarrow s_1$ `，我们有` $\mathcal{M},s_1 \models \phi$ ` （即存在某个下一个状态，满足` $\phi$ `）

9 . ` $\mathcal{M},s \models AG \phi$ `iff对于每个路径` $s_1 \rightarrow s_2 \rightarrow s_3 \rightarrow ...$ `，其中沿途的` $s_i$ `均与` $s$ `相等，我们有` $\mathcal{M},s_i \models \phi$ `

10 . ` $\mathcal{M},s \models EG \phi$ `iff存在一个路径` $s_1 \rightarrow s_2 \rightarrow s_3 \rightarrow ...$ `，其中沿途的` $s_i$ `均与` $s$ `相等，我们有` $\mathcal{M},s_i \models \phi$ `

11 . ` $\mathcal{M},s \models AF \phi$ `iff对于任意的路径` $s_1 \rightarrow s_2 \rightarrow s_3 \rightarrow ...$ `，其中` $s_1$ `与` $s$ `相等，且存在一个` $s_i$ `使得` $\mathcal{M},s_i \models \phi$ `

12 . ` $\mathcal{M},s \models EF \phi$ `iff存在一个路径` $s_1 \rightarrow s_2 \rightarrow s_3 \rightarrow ...$ `，其中` $s_1$ `与` $s$ `相等，且对某个沿途的` $s_i$ `有` $\mathcal{M},s_i \models \phi$ `

13 . ` $\mathcal{M},s \models A[\phi_1 U \phi_2]$ `iff对于任意的路径` $s_1 \rightarrow s_2 \rightarrow s_3 \rightarrow ...$ `，其中` $s_1$ `与` $s$ `相等，且这个路径满足` $\phi_1 U \phi_2$ `

14 . ` $\mathcal{M},s \models E[\phi_1 U \phi_2]$ `iff存在一个路径` $s_1 \rightarrow s_2 \rightarrow s_3 \rightarrow ...$ `，其中` $s_1$ `与` $s$ `相等，且这条路径满足` $\phi_1 U \phi_2$ `


### CTL 公式的等价关系

对于两个CTL公式` $\phi$ `和` $\psi$ `，如果任意模型下的任意状态满足其中之一必然满足其中的另一个，则称他们语义等价，写作` $\phi \equiv \psi$ `。

本节给出一些重要的CTL等价公式:

```math 
& \neg AF \phi \equiv EG \neg \phi  \\ 
& \neg EF \phi \equiv AG \neg \phi \\ 
& \neg AX \phi \equiv EX \neg \phi 
```

以及 

```math 
& AF \phi \equiv A [\top U \phi] \\ 
& EF \phi \equiv E [\top U \phi]
```

### CTL 连接词充分集合

**定理** 一个CTL的时序连接词集合是充分的，当且仅当，这个集合至少包含了` $\{AX,EX\}$ `其中之一，以及` $\{EG,AF,AU\}$ `其中之一和` $EU$ `。

我们给出其中之一的充分集合` $\{AU,EU,AX\}$ `并展示其他的连接词如何化归到这些连接词上：

```math
& A[\phi R \psi] = \neg E [\neg \phi U \neg \psi] \\ 
& E[\phi R \psi] = \neg A [\neg \phi U \neg \psi] \\ 
& A[\phi W \psi] = A [\psi R (\phi \vee \psi)] \\ 
& E[\phi W \psi] = E [\psi R (\phi \vee \psi)]
```

读者可以自行通过定义验证这些等式。

## CTL* 和 LTL与CTL的表达力

在CTL中，其允许对路径使用量词，因而其表达力比LTL更强，然而它不允许像LTL一样通过一个公式选择一系列路径。例如对于任意有` $p$ `的路径，也会有` $q$ `在LTL中可以写为` $F p \rightarrow F q$ `，但在CTL中由于每一个时序连接词必须与量词绑定的限制，并不能表达这个内容。

为此，我们提出CTL*，其将CTL中的限制解除，以便获得更强大的表达力。

下面给出CTL*语法：

- 状态公式

```math 
\phi ::= \top \ | \ p \ | \ (\neg \phi) \ | \ (\phi \wedge \phi) \ | \ A[\alpha] \ | \ E[\alpha]
```
其中` $p$ `式任意原子公式，` $\alpha$ `式任意的路径公式。

- 路径公式

```math 
\alpha ::= \phi \ | \ (\neg \alpha) \ | \ (\alpha \wedge \alpha) \ | \ (\alpha U \alpha) \ | \ (G \alpha) \ | \ (G \alpha) \ | \ (F \alpha) \ | \ (X \alpha) 
```

其中` $\phi$ `式任意的状态公式。

> 补充： 这个定义很有趣，因为其第一次展示了一种特殊但不失常见的递归方式--相互递归，它们的定义需要相互调用，递归的基础情形是` $p$ `和` $\top$ `。

### CTL时序公式中的布尔连接词

在前面讨论CTL中，我们提到了CTL的两大限制，一是不允许使用布尔连接词；二是不允许嵌套路径公式。然而对于前者，我们仍然有办法将其转化为CTL的合法公式。

例如在CTL*中的公式` $E [ F p \wedge F q]$ `可以转化为` $EF [p \wedge EF q] \vee EF [q \wedge EF p]$ `；如果我们有` $F p \wedge F q$ `，那么要么` $p$ `在` $q$ `之前出现，要么` $q$ `在` $p$ `之前出现，这对应了CTL公式中析取的两部分。