模型检验^[1-2]是受到学术界和工业界广泛认可的一种自动形式验证技术，用于判断计算机系统的正确行为属性，且能够保障计算机系统在不同开发阶段^[3]需要满足的各类正确性需求。

在模型检验中，通常使用Kripke结构进行建模，用以描述系统行为^[4]，使用计算树逻辑 (computation tree logic，简称 CTL)^[5]刻画需要验证的性质，最后通过模型检验算法进行验证。在经典的模型检验中，如果模型不满足待检验的性质规约，算法通常会给出一个反例，表明所验证的系统存在一部分行为违反性质规约^[6-12]。尽管模型检验的方法已经大量应用于复杂系统的验证，但这些方法大都存在一个严重限制，就是它们只能验证系统规范的正确性，而当验证失败时并不能进行相应的修复。

在模型修复的研究中，很多是采用自动修复方法。例如，Buccafurri等^[6]提出了一种将人工智能和模型检验相结合的模型修复算法，该算法可以识别并发系统的错误，且为系统提供可能的修复方法。Zhang等^[7]将模型修复思想运用到线性时态逻辑(linear temporal logic, 简称LTL)模型检验中，并进一步提出了基于“可容许”模型的修复算法^[10]，对计算树逻辑的模型修复问题进行了深入研究。Carrillo等^[10]在以往的模型修复中增添了“保护”的概念，并提出了对应的算法，解决了CTL的模型修复问题。与以上方法不同的是，Attie等^[11]提出了另外一种模型修复算法。该算法采用了子模型修复，在只考虑删除状态和迁移的前提下，构造一个布尔公式，然后用SAT求解器进行修复。此外，还有许多有关模型自动修复的研究^[13-14]。

由以上研究可知，验证失败的模型经过一系列修复手段（如删除大量失败路径）后，失去了与原模型相似的结构，而这意味着在修复操作后系统行为会发生重大变化。鉴于此，提出一种模型修复方法，在修复过程中保留原模型中尽可能多的信息。

首先，基于极小模型修复思想^[10]，给出2种对原模型影响相对最小的原子修复操作，通过经典模型检验中的不动点思想^[15]对模型修复问题进行初步讨论；其次，在极小模型修复的基础上，结合图算法的某些性质^[16]给出了状态保留的模型修复理论和算法。此外，由于基于CTL的极小模型修复是NP问题^[9]，将模型修复的范围进行缩小，在CTL的一个子集ECTL上进行研究讨论，从而使状态保留的修复算法时间复杂度得以降低到多项式时间。

1.   模型修复的不动点思想

在模型检验中，通常使用Kripke结构对系统进行建模^[17-18]。基于原子命题集合AP的Kripke结构是一个三元组$M = \left( {S,R,L} \right)$，其中：$S$是一个非空有限状态集合；$R \subseteq S \times S$表示迁移函数，且$R$是total的^[19]，即任意状态存在后继；$L:S \to {2^{{\text{AP}}}}$表示状态标签函数，每个状态对应一组原子命题。

在$M$中，称一个无限的状态序列${s_0}{s_1}{s_2} \cdot \cdot \cdot$为状态$s$的一条路径$\pi$，其中$s = {s_0}$，且对于任意的$i \geqslant 0$，$\left( {{s_i},{s_{i + 1}}} \right) \in R$。此外，常用$\pi (j)$表示路径$\pi$中第$j + 1$个状态，其中$j \in {\bf{N}}$。给定状态$s \in S$，约定使用${\text{RS(}}s{\text{)}}$表示状态$s$的所有可达状态集合,${\text{Post(}}s{\text{)}}$表示所有状态$s'$的集合，其中$s' \in S$，且$(s,s') \in R$。同样地，${\text{Pre(}}s{\text{)}}$表示所有状态${s^*}$的集合，其中${s^*} \in S$，且$({s^*},s) \in R$。

给定$M = \left( {S,R,L} \right)$是一个Kripke结构，${s_0} \in S$，${s_0}$为初始状态，$\varphi$表示可满足的CTL公式。在模型检验的过程中，若模型$M$满足公式$\varphi$^[20]，则记作$\left( {M,{s_0}} \right) \vdash \varphi$；否则，需要对$M$进行修复，构成新的模型$M'$，使得模型$M'$满足公式$\varphi$。在此过程中，期望修复后的模型能保留原模型中尽可能多的元素，因此，结合极小模型修复的思想选择了对模型影响最小的2种修复操作。

定义1　设$M = \left( {S,R,L} \right)$是一个Kripke结构，$\varphi$是一个CTL命题公式，$s,s' \in S$。$M$上的原子修复操作定义为${\rm{ChangeLabel}}(M,s,\varphi )$，用于修改状态$s$上的标签函数，使得$\left( {M,s} \right) \vdash \phi$；${\rm{AddRlt}}(M,s,s')$，在状态$s$和$s'$之间增加一条迁移，使得$R' = R \cup \left\{ {(s,s')} \right\}$。

上述2种原子修复操作都是赋值操作，因此，其时间复杂度都是$O(1)$。

模型修复是模型检验问题的拓展，自然地，首先考虑的是模型检验的过程，并尝试由此得出修复验证后失败模型的方法。在经典的模型检验中，对于CTL中部分逻辑算子的检验需要反复迭代，直至被标记为成功或者失败，在检验模型的过程中，搜寻判断出需要被修复的路径以及状态，从而调用2种原子修复操作，以达到模型修复的目的。

以下给出Kripke结构中关于时态逻辑算子$EG$的不动点修复算法。

算法1　${\text{FixpointRepairEG}}\left( {M,{s_0},EG\phi } \right)。$

输入：Kripke结构$M$，CTL公式$EG\varphi$，其中$M = \left( {S,R,L} \right)$，${s_0} \in S$且$\left( {M,{s_0}} \right) \nvdash EG\phi。$

输出：修复后的Kripke结构$M'$，其中$M' = \left( S', R',L' \right)$，${s_0}' \in S'$且$\left( {M',{s_0}'} \right) \vdash EG\phi。$

1. if $\left( {M,{s_0}} \right) \nvdash \phi$ then

2. 　$M' \leftarrow {\rm{ChangeLabel}}(M,{s_0},\varphi )$

3. else

4.　 ${\text{W}} \leftarrow {\text{SAT}}\left( {EG\varphi } \right)$//调用标签算法

5. 　if $X \ne \varnothing$ then

6. 　　任取$s \in X$

7. 　　$M' \leftarrow {\text{ADDRlt}}(M',{s_0},s)$//添加迁移

8. 　else

9. 　　$Y \leftarrow {\text{Stack}}\left( {{s_0}} \right)$//初始化栈Y,${s_0}$为栈首

10. 　　$X \leftarrow {\text{NIL}}$//初始化栈X

11. 　　while $X \ne Y$ do

12. 　　　$X \leftarrow Y$

13. 　　　if for all$s \in {\text{Post}}\left( {X.{\text{top}}} \right)$,$s \nvdash \phi$ then

14. 　　　　任取$s \in {\text{Post}}\left( {X.{\text{top}}} \right)$

15. 　　　　$M' \leftarrow {\text{Changelabel}}(M',s,\varphi )$

16. 　　　else 选择$s \in {\text{Post}}\left( {X.{\text{top}}} \right) \wedge s \vdash \phi$

17. 　　　　$Y \leftarrow Y \cup \left\{ s \right\}$

18. if $\left( {M',{s_0}'} \right) \vdash EG\phi$ then

19. 　　return $M'$

20. else ${\text{FixpointRepairEG}}\left( {M',{s_0}',EG\phi } \right)。$

算法1是针对CTL逻辑算子$EG\phi$在Kripke结构中的修复。需要说明的是，算法输入的CTL公式$EG\varphi$是可满足的，且公式中的$\phi$为基于原子命题${\rm{AP}}$和逻辑联结词组成的命题公式。算法运行时判断模型的初始状态${s_0}$是否满足命题公式$\phi$，若不满足，则实施状态修复。

根据定义1的修复操作，算法提供了修复模型的2个思路，首先调用经典的模型检验算法求解满足公式$EG\phi$的状态集合(为表述方便，后文将此类集合统称为满足集，公式$\varphi$的满足集记为${\text{SAT}}\left( \phi \right)$)，通过在初始状态和满足集中元素间添加迁移的方法完成修复。当模型中不存在满足集时，算法将由初始状态出发，通过不动点思想迭代构造出模型中的一条完整的路径，在迭代的同时对路径上每个状态进行判断修复，从而完成公式修复。算法1第11~17行运行过程中，使用2个栈结构对修复路径中的状态进行搜索并存储，当入栈元素为重复状态时，表明算法已构造出一条完整路径，且该路径上所有状态皆满足算法要求，此时循环结束。值得一提的是，因Kripke结构是total的，算法1第13行在遍历栈顶元素的后继状态时不会为空。

与经典的模型检验算法所需的复杂度$O\left( \left| \varphi \right| \cdot \left( {\left| S \right| + \left| R \right|} \right) \right)$相比，不动点修复算法所添加的判断语句以及修复操作并不会影响算法整体复杂度。算法1第11~17行的while循环复杂度为$O\left( {\left| S \right| + \left| R \right|} \right)$。因此，不动点修复算法的总时间复杂度为$O\left( {\left| \varphi \right| \cdot \left( {\left| S \right| + \left| R \right|} \right)} \right)$。

命题1　给定一个Kripke结构$M$，CTL公式$EG\varphi$，其中$M = \left( {S,R,L} \right)$，${s_0} \in S$，且$\left( {M,{s_0}} \right) \nvdash EG\phi$。算法1终止时，返回一个满足公式$EG\varphi$的修复模型$M' = \left( S', R',L' \right)$。

证明　算法通过2部分进行修复工作。第1部分，首先调用了标签算法，搜索满足公式$EG\varphi$的状态集合并将其作为满足集，当满足集不为空时，任取集合中一元素$s$，可知$s \in S$，且$s \vdash EG\phi$，在初始状态及其之间增添一条迁移$\left( {{s_0},s} \right)$，构造路径$\pi = \left[ {{s_0}, \cdot \cdot \cdot } \right]$，其中${s_0} \in S$为初始状态，且$\left( {M',{s_0}} \right) \vDash EG\phi$。此时算法返回模型$M'$，修复完成。当满足集为空时，算法1执行第2部分。因为模型存在有限个状态且任一状态出度不为零，故遍历状态后必能构造出一条完整路径，则2个栈总能相等，此时while循环结束，且栈中存储路径$\pi = \left[ {{s_0}, \cdot \cdot \cdot } \right]$，其中${s_0} \in S$为初始状态，且$\left( {M',{s_0}} \right) \vdash EG\phi$。

综上所述，算法1必会终止，且返回的修复模型$M'$会满足公式$EG\varphi$。

2   保留可达状态的路径修复理论

不动点修复算法是基于经典的模型检验方法改造而来，在完成修复工作的前提下存在一些不足，例如在修复算子$EG$的算法中，路径的选择过于随机，可能导致状态修复代价过大的情况；此外，处于多条路径中的同一状态可能被重复进行修复操作，尽管这些操作不会影响算法输出结果，但同样会造成较大的计算资源浪费。

基于上述原因，结合极小代价修复的思想，提出了保留可达状态的路径修复算法，对不动点修复进行改进。对于同一个模型，选择不同的修复手段，可能得到不同的修复模型，因此找到其中修复代价最小的模型是修复算法所追求的效果。首先定义衡量模型间修复代价的数值，称其为“距离”，用于衡量修复模型与原模型之间的差别。

定义2　设$M = \left( {S,R,L} \right)$，$M' = \left( {S',R',L'} \right)$是2个Kripke结构，它们之间的距离$d\left( {M,M'} \right)$定义为$d\left( {M,M'} \right) = \left| {S' - S} \right| + \left| {R' - R} \right| + \left| {\left\{ {s \in S'|L\left( s \right) \ne L'\left( s \right)} \right\}} \right|$。

根据修复模型与原模型之间的距离可定义模型间的近似性。

定义3　设$M = \left( {S,R,L} \right)$是一个Kripke结构，${M_1} = \left( {{S_1},{R_1},{L_1}} \right)$和${M_2} = \left( {{S_2},{R_2},{L_2}} \right)$都是$M$经过若干原子修复操作后得到的修复模型。若${\text{dis}}(M,{M_1}) \leqslant {\text{dis}} (M,{M_2})$，则称相较于${M_2}$，${M_1}$更接近于$M$，记为${M_1}{ \leqslant _M}{M_2}$。此外，若${M_1}{ \leqslant _M}{M_2}$且${M_2}{ \nleqslant _M}{M_1}$，则称${M_1}$比${M_2}$真接近于$M$，记为${M_1}{ \lt _M}{M_2}$。

定义3确保在不同的修复模型中能够找到与$M$距离最小，即修复代价最小的修复模型，简称为极小代价修复模型。以下给出${ \leqslant _M}$的性质，以保证极小代价修复模型的存在。

命题2　设集合$A$是$M$经过若干原子修复操作后得到的模型所构成的集合，${ \leqslant _M}$是集合$A$上的偏序关系。

证明　根据定义2，可证得${ \leqslant _M}$具有自反性和反对称性。

设$M = \left( {S,R,L} \right)$是一个Kripke结构，${M_1}$、${M_2}$和${M_3}$都是$M$经过一系列原子修复操作得到的修复模型，且${M_1}{ \leqslant _M}{M_2}$，${M_2}{ \leqslant _M}{M_3}$。由定义2可知，

通过定义3可得$d(M,{M_1}) \leqslant d(M,{M_3})$，即${M_1}{ \leqslant _M}{M_3}$，所以${ \leqslant _M}$具有传递性。因此，${ \leqslant _M}$是集合$A$上的偏序关系。

在模型修复过程中，为了保留原模型尽可能多的信息，采取如下措施：首先，针对模型修复时可能存在的修复操作，选择对原模型影响最小的2种修复操作，即增加一条迁移和修改某状态的标签函数；其次，通过极小代价修复的概念保证修复模型与原模型之间的差距最小；最后，缩小修复公式的范围，使得能够用较低复杂度的算法解决极小代价修复的问题。

在这些工作的基础上，对保留原模型中“尽可能多的信息”做出了具体尝试，选择保留原模型中尽可能多的原状态。该思想在定义1对于模型间距离的定义中可以得到体现。在衡量2个模型间差异时，通过修复操作分为2类进行讨论：1)模型间迁移数目的差异；2)模型间状态的差异。因2种修复操作皆对状态数目不造成影响，故衡量2个模型间状态差异便取决于拥有不同标签函数的相同状态数。不难看出，在修复原模型的过程中，修改状态标签并不会影响原模型中的状态数，下面给出的定理将证明修复过程中迁移关系的增添不会影响原模型中的状态数。

引理1 　设$M = \left( {S,{s_0},R,L} \right)$是一个Kripke结构，$\phi$是一个CTL公式，且$\left( {M,{s_0}} \right) \nvdash \varphi$，$M' = \left( {S',{s_{\text{0}}}',R',L'} \right)$是$M$经过某些原子修复操作得到的极小代价修复模型。若$s \in S$，且状态$s$从初始状态${s_0}$不可达，则状态$s \in S'$。

证明　使用反证法。假设经过修复得到$M'$后，状态$s \notin S'$，即在修复过程中存在修复操作删除了状态$s$。尽管算法选择的2种原子修复操作都不具有删除某状态的功能，但为方便证明，假设$M$存在另一个极小代价修复模型$M'' = \left( {S'',{s_0}'',R'',L''} \right)$，其中$S'' = S' \cup \left\{ s \right\}$。根据定义1，不难计算出$d(M,M'){ \leqslant _M}d(M,M'')$，即相较于$M'$，$M''$对于模型的修复代价更小。因此，$M'$并非极小代价修复，与假设矛盾，从而证得命题成立。

定理1　设$M = \left( {S,{s_0},R,L} \right)$是一个Kripke结构，$\phi$是一个CTL公式，且$\left( {M,{s_0}} \right) \nvdash \varphi$，$M' = \left( {S',{s_{\text{0}}}',R',L'} \right)$是$M$经过定义1中2种原子修复操作得到的极小代价修复模型，则$\left| S \right| = \left| {S'} \right|$。

证明　要证明修复操作不会影响状态数，可根据状态$s$是否由初始状态可达进行分类讨论。

1）若状态$s$从初始状态可达，显然修复操作对这类状态不造成影响；

2）若状态$s$从初始状态不可达，由引理1可知，状态$s$一定存在修复模型中。

至此，可以证得算法中的2种原子修复操作都不会影响原模型中的状态数。因此，极小代价修复可以完整表示。以下给出状态保留修复的定义。

定义4　设$M = \left( {S,{s_0},R,L} \right)$是一个Kripke结构，$\phi$是一个CTL公式，且$\left( {M,{s_0}} \right) \nvDash \varphi$，$M' = \left( {S',{s_{\text{0}}}',R',L'} \right)$是$M$经过某些原子修复操作得到的修复模型。若要$M'$是$M$的一个状态保留修复模型，则须满足：

1）$\left( {M',{s_0}'} \right) \vdash \varphi$；

2）不存在另外一个修复模型$M''$，使得$\left( {M'',{s_0}''} \right) \vdash \varphi$，且$M''{ \lt _M}M'$。

得出状态保留修复的定义是算法成功的基础，然而，判断基于Kripke结构的修复模型是否为极小代价修复是NP完全问题。为了降低修复算法的复杂度，对CTL公式的修复范围进行了约束，在它的一个子集上讨论极小代价修复问题。

定义5　在CTL公式中划分出一个子集，称这些公式为易处理的CTL公式，记为ECTL，其归纳定义如下：

1）公式$AX\phi 、EX\phi 、AG\phi 、EG\phi 、AF\phi 、EF\phi 、A(\phi U\varphi )$以及$E(\phi U\varphi )$是ECTL公式，其中$\phi 、\varphi$都是命题公式；

2）若${\psi _1}、{\psi _2}$是ECTL公式，则${\psi _1} \wedge {\psi _2}、{\psi _1} \vee {\psi _2}$也是ECTL公式。

3   保留可达状态的路径修复算法

以下给出具体的算法，用于解决ECTL上的状态保留修复问题。

算法2　${\text{ModelRepair}}\left( {M,s,\varphi } \right)。$

输入：Kripke结构$M$，CTL公式$\phi$，状态$s$，其中$M = \left( {S,R,L} \right)$，$s \in S$，且$\left( {M,s} \right) \nvdash \varphi。$

输出：修复后的Kripke结构$M'$，其中$M' = \left( S', R',L' \right)$，$s' \in S'$，且$\left( {M',s'} \right) \vdash \varphi。$

1.switch ($\phi$):

2. 　ase $p$，其中$p \in {\text{AP}}$:${\text{ChangeLabel}}(M,s,p)$

3. 　case ${\varphi _{\text{1}}} \vee {\varphi _{\text{2}}}$，其中${\varphi _{\text{1}}}、{\varphi _{\text{2}}}$是ECTL：

4. 　　${M_1} \leftarrow {\text{ModeRepair}}\left( {M,s,{\varphi _1}} \right)$

5.　　 ${M_2} \leftarrow {\text{ModeRepair}}\left( {M,s,{\varphi _2}} \right)$

6. 　　$M' \leftarrow$${M_1}$和${M_2}$中修复代价较小的模型

7. 　　return $M'$

8.　 case ${\varphi _{\text{1}}} \wedge {\varphi _{\text{2}}}$,其中${\varphi _{\text{1}}}、{\varphi _{\text{2}}}$是ECTL:

9. 　　$M' \leftarrow {\text{ModeRepair}}\left( {M,s,{\varphi _1}} \right)$

10. 　　$M' \leftarrow {\text{ModeRepair}}\left( {M,s,{\varphi _2}} \right)$

11. 　　return $M'$

12. 　case $EX\phi$:$X \leftarrow {\text{SAT}}\left( \phi \right)$

13. 　　if $X \ne \varnothing$ then

14. 　　　任取$s \in X$

15. 　　　$M' \leftarrow {\text{ADDRlt}}(M,{s_0},s)$

16. 　　else 任取$s \in {\text{Post}}\left( {{s_0}} \right)$

17. 　　　$M' \leftarrow {\text{ChangeLabel}}\left( {M,s,\phi } \right)$

18. 　　return $M'$

19. 　case $AX\phi$: for all $s \in {\text{Post}}\left( {{s_0}} \right)$

20. 　　　if $\left( {M,s} \right) \nvdash \phi$ then

21. 　　　　$M' \leftarrow {\text{ChangeLabel}}\left( {M,s,\phi } \right)$

22. 　　　return $M'$

23. 　case $EG\phi$:${\text{RepairEG}}\left( {M,{s_0},EG\phi } \right)$

24. 　case $AG\phi$:${\text{RepairAG}}\left( {M,{s_0},AG\phi } \right)$

25. 　case$E\left( {{\phi _1}U{\phi _2}} \right)$:${\text{RepairEU}}\left( {M,{s_0},E\left( {\phi U\varphi } \right)} \right)$

26. case $A\left( {{\phi _1}U{\phi _2}} \right)$:${\text{RepairAU}}\left( {M,{s_0},A\left( {\phi U\varphi } \right)} \right)$

27. case $EF\phi$:${\text{RepairEF}}\left( {M,{s_0},EF\phi } \right)$

28. case $AF\phi$:${\text{RepairAF}}\left( {M,{s_0},AF\phi } \right)。$

给定一个Kripke结构$M$和ECTL公式$\phi$，根据公式$\phi$的语法结构进行分类修复。

1)原子命题的修复直接调用状态标签修复操作；

2)若修复的ECTL公式是${\psi _1} \vee {\psi _2}$，则对${\psi _1}$、${\psi _2}$分别进行状态保留修复，返回其中修复代价较小的模型；

3)若修复的ECTL公式是${\psi _1} \wedge {\psi _2}$，则依次对${\psi _1}$、${\psi _2}$进行极大状态保留修复；

4)若修复的ECTL公式是$EX\phi$，则首先搜寻模型中是否存在满足命题公式$\phi$的状态$s$，若存在，则在初始状态与其之间添加一条迁移，否则对初始状态的一个后继状态实施标签修复；

5)若修复的ECTL公式是$AX\phi$，则对初始状态的所有后继状态实施标签修复；

6)其余的ECTL公式修复将在下文进行具体展现。

定理 2　给定一个Kripke结构$M$，CTL公式$EG\varphi$，其中$M = \left( {S,R,L} \right)$，${s_0} \in S$，且$\left( {M,{s_0}} \right) \nvDash EG\varphi$。状态保留修复算法${\text{ModelRepair}}\left( {M,s,\varphi } \right)$的时间复杂度是$O({(|S| + |R|)^2} \times |\varphi {|^2} \times {2^{\left| \varphi \right|}})$。特别地，若$\varphi$是原子命题，则算法复杂度为$O((|S| + |R|) \times |\varphi |)$。

证明　经典的模型检验算法时间复杂度是$O((|S| + |R|) \times |\varphi |)$，假设修复公式中的$\varphi$都是原子命题，则相较于模型检验，各函数无须在修复过程中进行多余的循环，因此，若$\varphi$是原子命题，则算法${\text{ModelRepair}} \left( {M,s,\varphi } \right)$复杂度为$O((|S| + |R|) \times |\varphi |)$。

当命题公式$\varphi$中不存在公式嵌套时，命题公式$\varphi$的修复需要对所有子公式进行检索，故时间复杂度为$O({2^{|\varphi |}})$，且重复于每轮验证算法。而算法中任一函数的修复都需多次调用模型检验算法，最坏情况下，所有状态和迁移都需要调用一次，故该过程时间复杂度为$O({(|S| + |R|)^2} \times |\varphi | \times {2^{|\varphi |}})$。最后考虑公式嵌套的情况，如${\varphi _{\text{1}}} \vee {\varphi _{\text{2}}}$或${\varphi _{\text{1}}} \wedge {\varphi _{\text{2}}}$，其中${\varphi _{\text{1}}}、{\varphi _{\text{2}}}$都是ECTL公式，则在上述情况下需要调用$\left| \varphi \right|$次公式$\varphi$的修复算法。

综上所述，状态保留修复算法${\text{ModelRepair}} \left( {M,s,\varphi } \right)$的最坏情况下的时间复杂度为$O({(|S| + |R|)^2} \times |\varphi {|^2} \times {2^{\left| \varphi \right|}})$。

根据德摩根律和等价关系式可知，CTL公式间存在等价关系，且可以通过基础的CTL公式进行转换。因此，不必给出所有ECTL公式的修复算法，结合算法2，给出3个算法以解决状态保留的模型修复工作。

算法3　${\text{RepairEG}}\left( {M,{s_0},EG\phi } \right)。$

输入：Kripke结构$M$，CTL公式$EG\varphi$，其中$M = \left( {S,R,L} \right)$，${s_0} \in S$，且$\left( {M,{s_0}} \right) \nvdash EG\phi。$

输出：Kripke结构$M$，CTL公式$EG\varphi$，其中$M = \left( {S,R,L} \right)$，${s_0} \in S$，且$\left( {M,{s_0}} \right) \vdash EG\phi。$

1. if $\left( {M,{s_0}} \right) \nvdash \phi$ then

2. 　　$M' \leftarrow {\text{ChangeLabel}}(M,{s_0},\varphi )$

3. 　else

4. 　　for each $s \in S$//初始化

5. 　　　$s.{\text{color}} \leftarrow {\text{white}}$

6. 　　　$s.{\pi} \leftarrow {\text{NIL}}$

7. 　　　if $\left( {M,s} \right) \nvdash \phi$ then

8. 　　　　$s.{{w}} \leftarrow 1$//判断状态是否需要修复

9. 　　　else $s.{\text{w}} \leftarrow 0$

10. 　　${\text{flag}} \leftarrow 0$，${\text{min}} \leftarrow \infty$

11. 　　${\text{path}} \leftarrow {\text{FindPath}}\left( {M,{s_0}} \right)$

12. 　　最后一个加入${\text{path}}$的状态记为${s^*}$

13. 　　if ${s^*} \vdash \phi$ then

14. 　　　$M' \leftarrow {\text{ADDRlt}}(M',{s_0}',{s^*})$

15. 　　else

16. 　　　for all $s' \in {\text{path}} \wedge s' \nvdash \phi$

17. 　　　　$M' \leftarrow {\text{ChangeLabel}}\left( {M,s',\phi } \right)$

18. 　if $\left( {M',{s_0}'} \right) \vdash EG\phi$ then

19. 　　　return $M'$

20. 　else ${\text{RepairEG}}\left( {M',{s_0}',EG\phi } \right)。$

算法4　${\text{FindPath}}\left( {M,u} \right)。$

输入：Kripke结构$M = \left( {S,R,L} \right)$，状态$u$，$u \in S。$

输出:$M$中一条以状态$u$为起始的路径path，且该路径上需要修复的状态数极少。

1.$u.{\text{color}} \leftarrow {\text{black}}$

2. 　for each $v \in {\text{Post}}\left( u \right)$

3. 　　$v.{\pi} \leftarrow u$

4. 　　if $v.{\text{color}} = {\text{white}}$ then

5. 　　　${\text{path}} \leftarrow {\text{FindPath}}\left( {M,v} \right)$

6. 　　else

7. 　　　根据父节点信息反向构造出路径${\text{pat}}{{\text{h}}^*}$

8. 　　　${\text{flag}} \leftarrow \displaystyle \sum\limits_{s \in {\text{path}}} {s.{{w}}}$

9. 　　　if ${\text{flag}} \lt {\text{min}}$ then

10. 　　　　${\text{min}} \leftarrow {\text{flag}}$

11. 　　　　${\text{path}} \leftarrow {\text{pat}}{{\text{h}}^{\text{*}}}$

12. 　　　　$v.{\text{color}} \leftarrow {\text{white}}$

13. 　　　　$u.{\text{color}} \leftarrow {\text{white}}$

14. 　　return ${\text{path}}。$

算法3是对ECTL公式中$EG\varphi$的状态保留修复，首先对模型中的初始状态进行判断，若初始状态不满足命题公式$\phi$，则对其进行修复，否则对模型中状态进行初始化。初始化操作包括给模型中每个状态$v$赋值$v.{\text{color}}$、$v.{\pi}$以及$v.{{w}}$，分别记录状态$v$的公式满足性，前驱以及需要修复与否。不难看出，对于$EG\varphi$的修复思路来自深度优先搜索，算法初始化辅助亦借鉴了图算法中的深度优先搜索。通过算法4计算出修复代价最小的一条路径，即一条以初始状态为起点的路径，其路径上需要修复的状态数最少。算法3第13~17行将这条路径的修复工作分为2种情况：若最后加入路径的状态${s^*}$满足公式$\varphi$，则在初始状态及状态${s^*}$间增添一条迁移；否则依次修复路径上需要修改标签的状态。

算法4用于计算模型中修复代价最小的路径。其思想与深度优先搜索算法类似，所有初始状态为白色，遍历时修改为黑色。算法4由初始状态出发，搜索后继结点的过程中记录当前遍历路径的修复代价，即算法4第8行。当探索到回路时，表明已探索到一条完整路径，此时将已探索完毕的状态恢复为白色，使其能被其他路径再次探索。算法3中变量${\text{flag}}$用于存储每次遍历路径的修复代价，每次与${\text{min}}$进行比较，保证算法找出修复代价最小的路径。

算法5　${\text{RepairAF}}\left( {M,{s_0},AF\phi } \right)。$

输入：Kripke结构$M$，CTL公式$AF\varphi$，其中$M = \left( {S,R,L} \right)$，${s_0} \in S$，且$\left( {M,{s_0}} \right) \nvdash AF\phi。$

输出：修复后的Kripke结构$M'$，其中$M' = \left( S', R',L' \right)$，${s_0}' \in S'$，且$\left( {M',{s_0}'} \right) \vdash AF\phi。$

1. if for all $s \in S$,$\left( {M,s} \right) \nvdash \phi$

2. let ${s^*} \in S \wedge {s^*} \in {\text{RS}}\left( {{s_0}} \right)$ //${\text{RS}}\left( t \right)$表示状态$t$可达的状态集合

3. $M' \leftarrow {\text{ChangeLabel}}(M,{s^*},\varphi )$

4. else

5. for all $s \in S$

6. $s.{\text{count}} \leftarrow \left| {{\rm{Post}}\left( s \right)} \right|$//$s$的后继数

7. $s.{\text{color}} \leftarrow {\text{white}}$

8. $X \leftarrow {\text{NIL}}$

9. $Y \leftarrow {\text{SAT}}\left( \phi \right)$

10. for all $s \in Y$

11. $s{\text{.color}} \leftarrow {\text{black}}$

12. while $Y \ne \varnothing$ do //不动点迭代

13. $X \leftarrow Y$

14. 任取$s' \in Y$

15. $Y \leftarrow Y\backslash \left\{ {s'} \right\}$

16. for all $s \in {\text{Pre}}\left( {s'} \right)$//结点满足公式，则其所有前驱结点权重减1

17. $s.{\text{count}} \leftarrow s.{\text{count}} - 1$

18. if $s.{\text{count}} = 0$ then

19. $Y \leftarrow Y \cup \left\{ s \right\}$，$X \leftarrow X \cup \left\{ s \right\}$

20. $s.{\text{color}} \leftarrow {\text{black}}$

21. for all $s \in {\text{Post}}\left( {{s_0}} \right)$

22. if $s.{\text{color}} = {\text{white}}$ then

23. let $s' \in X$

24. $M' \leftarrow {\text{ADDRlt}}(M,s,s')$

25. if $\left( {M',{s_0}'} \right) \vdash AF\phi$ then

26. return $M'$

27.else ${{\rm{Repair}}} {\text{AF}}\left( {M',{s_0}',AF\phi } \right)。$

算法5是对ECTL公式中$AF\varphi$的状态保留修复。首先若模型中不存在满足公式$\varphi$的状态，则任取一个状态进行标签修复，否则对模型进行初始化。将所有状态初始标记为白色，记录每个状态的后继数为$s.{\text{count}}$，之后通过不动点迭代检验模型，同时如算法5第16~20行操作，使得所有满足公式$AF\varphi$的状态都被标记为黑色。最后检索初始状态所有的后继状态，对仍被标记为白色的状态实施修复。

算法6　${\text{RepairEU}}\left( {M,{s_0},E\left( {\phi U\varphi } \right)} \right)。$

输入：Kripke结构$M$，CTL公式$E\left( {\varphi U\phi } \right)$，其中$M = \left( {S,R,L} \right)$，${s_0} \in S$，且$\left( {M,{s_0}} \right) \nvdash E\left( {\phi U\varphi } \right)。$

输出：修复后的Kripke结构$M'$，其中$M' = \left( {S',R',L'} \right)$，${s_0}' \in S'$，且$\left( {M',{s_0}'} \right) \vdash E\left( {\phi U\varphi } \right)。$

1. if $\left( {M,{s_0}} \right) \nvdash \phi$ then

2. $M' \leftarrow {\text{ChangeLabel}}(M,{s_0},\varphi )$

3.else if for all $s \in S$，$\left( {M,s} \right) \nvdash \varphi$

4. let ${s^*} \in S \wedge {s^*} \in {\text{RS}}\left( {{s_0}} \right)$

5. $M' \leftarrow {\text{ChangeLabel}}(M,{s^*},\phi )$

6.else

7. $X \leftarrow {\text{SAT}}\left( {E\left( {\varphi U\phi } \right)} \right)$

8. 任取$s \in X$

9. $M' \leftarrow {\text{ADDRlt}}(M,{s_0},s)$

10.if $\left( {M',{s_0}'} \right) \vdash E\left( {\phi U\varphi } \right)$ then

11. return $M'$

12.else ${\text{RepairEU}}\left( {M',{s_0}',E\left( {\phi U\varphi } \right)} \right)。$

算法6是对ECTL公式中$E\left( {\varphi U\phi } \right)$的状态保留修复，首先检验初始状态是否满足公式$\varphi$，以及模型中是否存在满足公式$\phi$的状态，并做出对应的修复操作。其次通过标签算法找出满足公式$E\left( {\varphi U\phi } \right)$的状态集，算法6第3~5行的判断操作保证了此状态集必不为空。接下来进行的修复操作，在满足公式$E\left( {\varphi U\phi } \right)$的状态中随机挑选一个状态，在初始状态与其之间添加一条迁移。

4.   结束语

研究了基于Kripke结构的CTL模型检验的修复问题，在极小修复的基础上提出状态保留修复的理论与算法。首先，为了降低算法时间复杂度，限制了CTL公式修复的范围，在其一个子集上讨论修复问题。其次，通过不动点理论迭代地搜寻模型中的失败路径，并进行修复，以此构造$AF$的修复算法，同时结合DFS算法的性质构造$EG$修复算法。最后，给出算法正确性以及时间复杂度证明，保证了本算法能以多项式时间复杂度解决状态保留的模型修复问题。