【模型检测学习笔记】10：有限状态迁移系统上的IC3算法

IC3算法全称是Incremental Construction of Inductive Clauses for Indubitable Correctness，可以用来检测迁移系统上的不变性性质。

1 术语约定

1.1 clause和literal

这里逻辑公式（logic formula）一律用合取范式（conjunctive normal form，CNF）来表示，CNF中的每一项是一个clause，每个clause是若干literal的析取，每个literal是一个逻辑变量或者逻辑变量的非，例如下面就是一个CNF：
(a∨¬b)∧(¬a∧b)(a \vee \neg b) \wedge (\neg a \wedge b) (a∨¬b)∧(¬a∧b)

其中的a∨¬ba \vee \neg ba∨¬b和¬a∧b\neg a \wedge b¬a∧b称为clause，而其中出现的aaa、bbb、¬a\neg a¬a、¬b\neg b¬b称为literal。

1.2 有限状态迁移系统

一个有限状态迁移系统（finite state transition system）用一个三元组S=(X,I,T)S=(X,I,T)S=(X,I,T)表达，用XXX表示状态变量的集合，用逻辑公式I(x)I(x)I(x)初始状态集合，用逻辑公式T(X,X′)T(X, X')T(X,X′)表示迁移关系。

用XiX^iXi表示对XXX中的变量迁移iii步的结果，为了简化，用X′X'X′表示迁移一步的，也就是X1X^1X1。类似地，用F′F'F′表示F(X1)F(X^1)F(X1)，即对迁移一步之后的X′X'X′应用逻辑公式FFF的结果。

系统中的一个状态sss是对XXX中的所有变量的一个赋值，每个变量的赋值可以用一个literal来表示，然后整个赋值其实就是这些literal的合取：
s=a∧¬bs = a \wedge \neg b s=a∧¬b

注意，因为sss是literal的合取，所以¬s\neg s¬s是literal的析取，比如以上面的公式为例子，有：
¬s=¬a∨b\neg s = \neg a \vee b ¬s=¬a∨b

所以对表示状态的sss取反得到的¬s\neg s¬s是一个clause。

称sss是一个FFF状态，当有s⊨Fs \models Fs⊨F（其中FFF是一个逻辑公式）。

1.3 inductive generalization

称满足c⇒sc \Rightarrow sc⇒s的一个clause ccc是sss的一个归纳推广（inductive generalization）。

1.4 safety property

在给定的有限状态系统上，如果给出一条逻辑公式，这个逻辑公式在所有的可达状态上都满足，则称这个逻辑公式是一个safety property（其实就是传统意义上的不变性公式）。如果对于给定的（要验证的）safety property，存在一个可达状态不满足这条公式，那么称这个状态是一个坏状态（bad state）。

1.5 inductive assertion

迁移系统上的一个归纳断言（inductive assertion） ，或者叫归纳不变式（inductive invariant），是一个逻辑公式FFF，满足I⇒FI \Rightarrow FI⇒F，并且F∧T⇒F′F \wedge T \Rightarrow F'F∧T⇒F′。前面一条称为初始步（initialization），确保所有的初始状态都满足FFF；后面一条称为归纳步（consecution），确保FFF对于状态迁移是封闭的（closed）。简称FFF是归纳的（inductive）。另外，如果在归纳的过程中出现反例，那么也就是出现了不满足条件的坏状态，称为归纳的反例（counterexample to induction，CTI）。

1.6 inductive strengthening

设PPP是一个safety property，FFF是一个逻辑公式，如果F∧PF \wedge PF∧P是归纳的（也就是满足1.5里那两个条件），那么称FFF是PPP的一个归纳强化（inductive strengthening）。

1.7 inductive relative

设GGG是一个逻辑公式，FFF是一个逻辑公式，如果I⇒FI \Rightarrow FI⇒F和G∧T∧F⇒F′G \wedge T \wedge F \Rightarrow F'G∧T∧F⇒F′都成立，则称FFF对GGG是归纳相对（inductive relative） 的。

2 在有限状态系统上用IC3算法做模型检测

要验证有限状态系统S=(X,I,T)S=(X,I,T)S=(X,I,T)上的safety property PPP是否是成立的，IC3算法生成一个PPP的inductive strengthening公式FFF，它能够覆盖掉所有的初始状态。

只要存在PPP的这样一个inductive strengthening公式FFF，就能够证明PPP是一个safety property，因为：

由于归纳性质，F∧PF \wedge PF∧P对系统SSS的迁移TTT是封闭的，也就是在迁移过程中这个F∧PF \wedge PF∧P一直满足，所以迁移过程不会到达一个¬P\neg P¬P状态。
在构造的时候就让F∧PF \wedge PF∧P对系统SSS的所有初始状态都是满足的了。

2.1 顶层函数

下面是IC3算法的顶层函数的伪代码，第2行是对归纳过程中的初始步（0-step）和第一个归纳步（1-step）用SAT求解器验证一下，PPP如果是一个safety property，那么对所有的初始状态和下一步的状态都必须得是成立的，如果一开始PPP就不成立了，那那么就直接返回False了。

bool prove():if unsat(I -> P) or unsat(I /\ T -> P): return FalseF[0] := I, F[1] := P, k := 1while True:if not extendFrontier(): return FalsepropagateClauses()if F[i] = F[i + 1] for some 1 <= i <= k: return Truek := k + 1

Inductive strengthening其实就是把要证明的不变性性质PPP通过合取一个公式FFF，给它强化成模型中的一个归纳不变式F∧PF \wedge PF∧P。IC3算法会维持归纳不变式的序列F0,...,FkF_0,...,F_kF0,...,Fk（注意这里虽然都是用字母F，但是这个带下标的其实是F∧PF \wedge PF∧P迁移到每个状态上之后的那个式子），文章里称序列里的每一项FiF_iFi是一个frame，那么FiF_iFi就代表了归纳过程中可达状态的一种over-approximation。初始时候F0=IF_0 = IF0=I，F1=PF_1 = PF1=P，然后主循环会一直执行来不断扩充这个序列，并保持下面的性质一直满足：
(P1)I⇒F0(P2)Fi⇒Fi+1for0≤i≤k(P3)Fi⇒Pfor0≤i≤k(P4)Fi∧T⇒Fi+1for0≤i≤k\begin{aligned} (P_1) \ \ \ \ & I \Rightarrow F_0 \ \ \ \ \ \ \ & \\ (P_2) \ \ \ \ & F_i \Rightarrow F_{i+1} \ \ \ \ \ \ \ & for \ \ 0 \leq i \leq k \\ (P_3) \ \ \ \ & F_i \Rightarrow P \ \ \ \ \ \ \ & for \ \ 0 \leq i \leq k \\ (P_4) \ \ \ \ & F_i \wedge T \Rightarrow F_{i+1} \ \ \ \ \ \ \ & for \ \ 0 \leq i \leq k \end{aligned} (P1) (P2) (P3) (P4) I⇒F0 Fi⇒Fi+1 Fi⇒P Fi∧T⇒Fi+1 for 0≤i≤kfor 0≤i≤kfor 0≤i≤k

思考一：序列初始化时候F0=IF_0 = IF0=I和F1=PF_1 = PF1=P满足上面的四个条件吗？

答：满足，因为F[0] := I所以P1:I⇒F0P_1: I \Rightarrow F_0P1:I⇒F0成立。因为用SAT求解器做过了I -> P的检查，并且F[1] := P，所以P2:Fi⇒Fi+1P_2:F_i \Rightarrow F_{i+1}P2:Fi⇒Fi+1和P3:Fi⇒PP_3:F_i \Rightarrow PP3:Fi⇒P成立。因为用SAT求解器做过了I /\ T -> P的检查，所以P4:Fi∧T⇒Fi+1P_4:F_i \wedge T \Rightarrow F_{i+1}P4:Fi∧T⇒Fi+1成立。

思考二：为什么关注的是上面这四条性质？

答：试想已经找出了一个序列F0,...,Fi,Fi+1,...,FkF_0,...,F_i,F_{i+1},...,F_kF0,...,Fi,Fi+1,...,Fk，其中的每个frame都满足上面的四条性质，并且有Fi=Fi+1F_i = F_{i+1}Fi=Fi+1。那其实就已经达到了一个不动点，原文是『FiF_iFi is closed under the transition relation』，由P4P_4P4和Fi=Fi+1F_i = F_{i+1}Fi=Fi+1知FiF_iFi对迁移关系TTT是封闭的。又由P1P1P1和P2P2P2知I⇒FiI \Rightarrow F_iI⇒Fi，所以FiF_iFi是一个归纳不变式。又由P3P_3P3知Fi∧PF_i \wedge PFi∧P也是一个归纳不变式（其实这里Fi∧P=FiF_i \wedge P = F_iFi∧P=Fi），所以FiF_iFi是对PPP的一个归纳强化，也就证明了PPP是一个safety property，这就能够理解上面伪代码里面第7行返回True的逻辑了。

思考三：为什么循环一定可以终止？

答：根据P2P_2P2，以及第7行程序的判断相等就退出，知道这个frame序列一定是单调增强的，又因为这个是一个有限状态系统，所以最多#state+1\#state + 1#state+1步就可以终止。

综上所述，P1P_1P1到P4P_4P4这四条约束可以保证算法的正确性。

Theorem 1. Given a ﬁnite state transition system S and a formula P, IC3 terminates and returns true if and only if P is a safety property of S.

2.2 extendFrontier过程

这个过程就是已经有了满足上面P1..P4P_1..P_4P1..P4的序列F0..FkF_0..F_kF0..Fk，去找构造F0..Fk+1F_0..F_{k+1}F0..Fk+1的过程。这里要注意，因为P1..P4P_1..P_4P1..P4是有相邻的两个frame的关系的，所以每次其实是去重新构造整个序列，而不是能够直接找到一个Fk+1F_{k+1}Fk+1添加上去。

bool extendFrontier():F[k + 1] := Pwhile sat(F[k] /\ T /\ !P'): try:s := predecessor of !P extracted from SAT witnessremoveCTI(s)except Counterexample:return Falsereturn True

首先，添加一个新的Fi+1=PF_{i+1} = PFi+1=P进来，然后就是想要调整这个新的序列，使得性质P1..P4P_1..P_4P1..P4仍然在序列的每个frame上都满足。显然P1P_1P1是不受影响的，P3P_3P3根据定义在构造的时候就是满足的，由于调整的过程是给P0...PiP_0...P_iP0...Pi添加上一个clause，所以P2P_2P2也是不受影响的，所以关键就是要保持P4P_4P4在FkF_kFk上成立，也就是要让Fk∧T⇒Fk+1′F_k \wedge T \Rightarrow F_{k+1}'Fk∧T⇒Fk+1′。

假设这个蕴含式能保持，那么新的序列就也是满足这四条性质，这个extendFrontier()就可以返回了，没有其它的功能。

假设这个蕴含式不能保持，又因为这个Fk+1′F_{k+1}'Fk+1′就是P′P'P′，那也就是说用SAT求解器求解Fk∧T∧¬P′F_k \wedge T \wedge \neg P'Fk∧T∧¬P′是能成立的，也就是说满足FkF_kFk的状态存在能一步到达满足¬P\neg P¬P状态的，记为sss（它就是一个CTI），那么为了构造P4P_4P4成立，就把这个sss从FkF_kFk里面删除，并且保证P1P_1P1、P2P_2P2、P3P_3P3仍旧是满足的，这个删除过程就是伪代码里的removeCTI(s)。

2.3 removeCTI过程

在IC3构造序列的过程中，在FkF_kFk处出现一个CTI状态sss可能是两种原因导致的：

sss是从初始状态III可达的
目前还没有发现sss其实是不可达的

如果是第一种情况，那确实可以证明PPP这个性质是不满足的，因为确实存在从III到¬P\neg P¬P状态的path。但是如果是第二种情况，那就不能这样断定了。所以需要通过扩充帧序列，来尝试把sss从FkF_kFk中排除，从而尝试证明sss其实是不可达的，记这个证明义务（proof obligation） 为⟨s,k⟩\langle s, k \rangle⟨s,k⟩。

void removeCTI(s : state)states ={<s, k>}while states not empty:<q, i> = pop element of states that minimizes iif sat(F[0] /\ T /\ !q /\ q'):raise Counterexample//至此，q至少inductive relative于F[0]j := maximal j with not sat(F[j] /\ T /\ !q /\ q')c := inductiveGeneralization(!q)for l from 0 to j + 1:F[l] := F[l] /\ cif j >= i - 1:break // 证明义务满足w := witness for sat(F[j + 1] /\ T /\ !q /\ q')t := predecessor of q extracted from wstates := states U <t, j + 1>// <t, j + 1>可能无法表出<q, i>，继续检查states := states U <q, i>

IC3维护了整个证明义务的集合，集合中的每个条目⟨q,i⟩\langle q, i \rangle⟨q,i⟩的语义是接下来想要从frame FiF_iFi中把状态sss消除掉。为了完成这一点，要检查¬q\neg q¬q是inductive relative于F0..Fi−1F_0..F_{i-1}F0..Fi−1的。如果这个关系建立了，那么就可以挑选一个满足¬q⇒c\neg q \Rightarrow c¬q⇒c的ccc合取到F0..FiF_0..F_iF0..Fi的每一个frame里，这样就把qqq从FiF_iFi里面消除了。

一种简单的选法是选择c=¬qc = \neg qc=¬q，但是仅仅把一个状态qqq消除掉可能是不充分的，所以IC3算法是选择¬q\neg q¬q的一个（最小的）inductive generalization来作为ccc，这样就不仅把qqq消除掉了，还把类似qqq的状态（原文是q-like）也消除掉了。

在上面的伪代码程序里，考虑每次对证明义务⟨q,i⟩\langle q, i \rangle⟨q,i⟩，目的是要把qqq从FiF_iFi里消除掉。先要检查一下¬q\neg q¬q是不是inductive relative于F0F_0F0的。如果不是，那么就存在一个初始状态能够到达qqq状态，使得¬P\neg P¬P成立，所以就说明PPP不是一个safety property，可以直接返回了（在这个程序里是从异常退出）。反之，就找到一个最大的jjj满足¬q\neg q¬qinductive relative于FjF_jFj。因为先对F0F_0F0做了检查，所以这个jjj一定是存在的（至少也是0）。

接下来，就可以把¬q\neg q¬q的一个inductive generalization合取到F0..Fj+1F_0..F_{j+1}F0..Fj+1的每一个frame上（就是前面说的ccc）。如果j≥i−1j \geq i - 1j≥i−1，那么F0..Fj+1F_0..F_{j+1}F0..Fj+1这个序列其实就是F0..FiF_0..F_iF0..Fi，所以就完成目标了。反之，就是在归纳步（consecution）上失败了。也就是说jjj的下一项j+1j+1j+1满足Fj+1∧T∧¬q∧q′F_{j+1} \wedge T \wedge \neg q \wedge q'Fj+1∧T∧¬q∧q′用SAT求解器求解的结果是满足的，并且给出了一个witness（我理解的就是让这个逻辑公式为真的一组变量赋值）。这个witness揭露了一个Fj+1F_{j+1}Fj+1状态ttt（也就是t⊨Fj+1t \models F_{j+1}t⊨Fj+1），并且ttt是qqq的一个前置状态（predecessor）。至此，为了证明qqq是不可达的，就要证明ttt是不可达的，因此就构造一个新的证明义务⟨t,j+1⟩\langle t, j+1 \rangle⟨t,j+1⟩，加入到证明义务集合里去，然后继续这个循环。

在之后的某次循环就把⟨t,j+1⟩\langle t, j+1 \rangle⟨t,j+1⟩这个证明义务解出来了（或者从raise那里给出反例并退出），然后还是要去考虑本来要解决的证明义务——⟨q,i⟩\langle q, i \rangle⟨q,i⟩，所以这个证明义务也要加回到证明义务集合里，在未来解决了⟨t,j+1⟩\langle t, j+1 \rangle⟨t,j+1⟩之后继续考察⟨q,i⟩\langle q, i \rangle⟨q,i⟩。注意，这个过程不会造成无限循环，因为如果再次处理到⟨q,i⟩\langle q, i \rangle⟨q,i⟩这个证明义务，SAT求解器对Fj+1∧T∧¬q∧q′F_{j+1} \wedge T \wedge \neg q \wedge q'Fj+1∧T∧¬q∧q′的求解结果就不会再给出重复的ttt了，因为⟨t,j+1⟩\langle t, j+1 \rangle⟨t,j+1⟩在这之前的某个循环已经解决掉了，也就是ttt不会再包含在Fj+1F_{j+1}Fj+1里了。所以要么⟨q,i⟩\langle q, i \rangle⟨q,i⟩被解决，要么就给出一个新的前置状态（predecessor），而不会出现已经解决过的ttt。

思考一：为什么循环一定可以终止？

因为选择证明义务的时候避免了和后面的证明义务出现循环依赖，见伪代码的第4行，每次是在证明义务集合states里选择iii最小的一个证明义务⟨q,i⟩\langle q, i \rangle⟨q,i⟩。

思考二：为什么算法是正确的？基于前面2.1节的讨论，这个思考其实是在关注这样一个问题：为什么这个算法过程中可以保持P1P_1P1到P4P_4P4这四条约束？

P1P_1P1是保持的，因为没有一个III状态（⊨I\models I⊨I的状态）被从F0F_0F0里消除掉，这是因为每个加入到F0F_0F0中的clause ccc对F0F_0F0都是inductive relative的（这个地方需要再思考一下）。

P2P_2P2是保持的，因为每次拿到ccc都会合取到F0..FiF_0..F_iF0..Fi这个序列的每一个frame上，显然是不破坏P2P_2P2的。

P3P_3P3是保持的，因为F0..FiF_0..F_iF0..Fi这个序列的每一个frame只会不断加强（restricted），都是去不断合取clause，不会变弱，所以既然本来Fi⇒PF_i \Rightarrow PFi⇒P，现在FiF_iFi加强之后也能⇒P\Rightarrow P⇒P。

P4P_4P4是被强制构造出来的，因为伪代码的第14、15行会把前置状态（predecessor）找出来，然后以证明义务的形式加到证明义务集合里，再在未来的某次循环时候把这个predecessor（其形式就是一个clause）的取反的inductive generalization合取到每个frame上（见伪代码的9、10、11行），直到找不到新的predecessor，这时候性质P4P_4P4最终一定是满足的。

2.4 propagateClauses过程

为了稳定地精化frame序列，这个过程会把FiF_iFi中的某些clause加入到Fi+1F_{i+1}Fi+1中，每次检查FiF_iFi中的每个clause ccc，看ccc是否是inductive relative于FiF_iFi的，如果是，那么就不存在满足FiF_iFi的状态能够下一步到达满足¬c\neg c¬c的状态（因为归纳相对的定义限制了Fi∧T∧c⇒c′F_i \wedge T \wedge c \Rightarrow c'Fi∧T∧c⇒c′），所以就证明了¬c\neg c¬c的状态在i+1i + 1i+1步以内是不可达的，因此ccc就能够被加入到Fi+1F_{i+1}Fi+1中来精化Fi+1F_{i+1}Fi+1的这种over-approximation。

void propagateClauses()for i = 1 to k:for each clause c in F[i]:// 等价于not sat(F[i] /\ c /\ T /\ !c')if not sat(F[i] /\ T /\ !c'):F[i + 1] := F[i + 1] /\ c

不过这种方式还不是最强的精化办法，因为这种方法里是一个一个clause单独考虑的，完全可能存在两个clause c1,c2∈Fic_1, c_2 \in F_ic1,c2∈Fi，两个一起的时候c1∧c2c_1 \wedge c_2c1∧c2是inductive relative于FiF_iFi的，但是单独某一个拎出来都不是inductive relative于FiF_iFi的。所以可以计算一下FiF_iFi的一个最大clause集合，使得它能够inductive relative于FiF_iFi，把这样一个clause集合加入到Fi+1F_{i+1}Fi+1里面。