模型检验与时序逻辑

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

形式化验证方法(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形式给出）：

\[\begin{split}\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) \end{split}\]

其中\(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形式如下：

\[\begin{split}\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] \end{split}\]

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等价公式:

\[\begin{split}& \neg AF \phi \equiv EG \neg \phi \\ & \neg EF \phi \equiv AG \neg \phi \\ & \neg AX \phi \equiv EX \neg \phi \end{split}\]

以及

\[\begin{split}& AF \phi \equiv A [\top U \phi] \\ & EF \phi \equiv E [\top U \phi]\end{split}\]

CTL 连接词充分集合

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

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

\[\begin{split}& 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)]\end{split}\]

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

CTL* 和 LTL与CTL的表达力

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

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

下面给出CTL*语法：

  • 状态公式

\[\phi ::= \top \ | \ p \ | \ (\neg \phi) \ | \ (\phi \wedge \phi) \ | \ A[\alpha] \ | \ E[\alpha]\]

其中\(p\)式任意原子公式，\(\alpha\)式任意的路径公式。

  • 路径公式

\[\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公式中析取的两部分。