模糊计算树逻辑的模型检测修复算法

毛兆东， 钱俊彦， 蔡 泳

(桂林电子科技大学 计算机与信息安全学院，广西 桂林 541004)

模型检测[1-2]是一种验证有限状态系统的行为是否具备预期属性的自动验证技术，自提出以来在学术界和工业界产生了巨大的影响，并且已被应用到不同的领域。模型检测的一般过程为：首先对待验证的系统建模，再对待验证的系统属性进行描述，通过模型检测算法验证系统是否满足该属性，若满足，则输出true，否则将给出反例说明模型不满足该属性的原因。

随着计算机系统的复杂性日益增加，系统存在许多不确定性的信息。显然，经典的模型检测方法已经难以准确处理带有大量不确定性信息的系统。为此，人们对经典的模型检测方法进行了扩展。例如，为了对具有随机行为的系统进行定量验证，Hansson等[3]提出了概率计算树逻辑(probabilistic computation tree logic，简称PCTL)的模型检测算法，Baier等[1]提出了基于概率测度的概率模型检测算法。为了解决具有不一致性信息系统的验证问题，文献[4-5]基于多值逻辑对模型检测方法进行扩展，提出了多值模型检测算法。为了解决包含可能性测度量化信息系统的验证问题，文献[6-10]提出了基于可能性测度的模型检测算法。为了解决含有模糊量化信息系统的验证问题，潘海玉等[11]提出了模糊计算树逻辑(fuzzy computation tree logic，简称FCTL)的模型检测算法。

模型检测专注于验证系统是否满足系统属性，当系统不满足属性时无法自动修复系统。由此在模型检测的基础上，Buccafurri等[12]提出了模型检测与自动修复相结合的思想，这引起了研究者的广泛关注。随后，研究者在经典的Kripke结构修复问题的研究上取得了相关的研究成果，如Zhang等[13]提出了经典CTL的修复算法。为了解决CTL在修复过程中所产生的状态空间爆炸问题，Ding等[14]提出了CTL修复的优化算法，Chatzieleftheriou等[15]提出了基于抽象Kripke结构的修复算法。为了克服递归算法在模型修复中遇到的困难，Carrillo等[16]提出了基于“保护”的Kripke结构修复算法。

另一方面，模型检测修复的研究也引入到概率模型中。概率模型修复方法首先在文献[17]被提出。随后，Pathak等[18]提出基于贪心方法的随机模型修复方法。另外，为了解决概率模型的状态空间爆炸的问题，Chatzieleftheriou等[19]提出了抽象概率模型的修复算法。

尽管研究者对经典的Kripke模型修复和概率模型修复的研究工作都取得一定的成果，但关于模糊Kripke结构中模糊计算树逻辑的修复问题至今未引起重视。为此，针对模糊Kripke结构中模糊计算树逻辑的修复问题，提出模糊计算树逻辑的模型检测修复算法。

1 预备知识

定义1(模糊Kripke结构) 原子命题集合P的模糊Kripke结构(fuzzy Kripke structures，简称FKS)是一个四元组K=(S,s0,R,V)，其中：1)S为有限的非空状态集；2)s0∈S为初始状态；3)R:S×S→[0,1]为模糊迁移函数；4)V:S×P→[0,1]为模糊标签函数。对于给定的状态s和原子命题p∈P，V(s,p)表示p在状态s上成立的真值。

在模糊Kripke结构K中，若s=s0，且对于任意的i≥0，R(si,si+1)>0，则称无限的状态序列π=s0s1s2…为状态s的一条路径。从状态s出发的所有路径集合记为Π(s)。对于路径π=s0s1s2…，用π(j)表示π中第j+1个状态，其中j∈Ν。为了方便，将K=(S,s0,R,V)简写为K。

定义2(模糊计算树逻辑的语法) 模糊计算树逻辑(fuzzy computation tree logic，简称FCTL)的语法定义为

∃Gφ|∃φ1Uφ2|∀Xφ|∀Gφ|∀φ1Uφ2,

其中p∈P。

FCTL中的命题逻辑是FCTL的子集，要求FCTL中不能出现时序运算符，如X。

定义3(模糊计算树逻辑的语义) 设s∈S，φ为FCTL，φ在模型K上的语义解释为函数‖φ‖K:S→[0,1]。递归定义如下：

‖true‖K(s)=1,

‖false‖K(s)=0,

‖p‖K(s)=V(s,p),

‖φ1∨φ2‖K(s)=max(‖φ1‖K(s),‖φ2‖K(s)),

‖φ1∧φ2‖K(s)=min(‖φ1‖K(s),‖φ2‖K(s)),

‖φ‖K(π(1))),

R(π(i),π(i+1))),

‖φ‖K(π(1))),

R(π(i),π(i+1))),

‖φ2‖K(π(i))),

其中∨、∧分别表示[0,1]中的取大运算、取小运算。

定义4(α-可满足的FCTL) 设α∈[0,1]，若存在模糊Kripke结构K，满足‖φ‖K(s0)≥α，则称φ是α-可满足的FCTL。

2 FKS的修复问题

模糊Kripke结构的距离是衡量2个模糊Kripke结构之间差异。文献[20]采用标准化Minkowski距离[21]的定义方法，给出了模糊Kripke结构距离的定义。采用Hamming距离[22]的定义方法，给出另一种模糊Kripke结构距离的定义方法。

定义6(模糊Kripke结构的近似性) 设K1和K2分别为K通过某些原子修复操作得到的模糊Kripke结构，若d(K,K1)

3 FCTL模型检测的修复算法

对于模糊Kripke结构K，s∈S，若存在一条从s0出发的路径π，使得s出现在π中，则称s是K中的可达状态。除非特别声明，否则所讨论的模糊Kripke结构中的状态都是可达状态。

为了方便分析算法的时间复杂度，设|φ|和O(K,φ)分别表示FCTLφ的长度和K的模型检测的时间复杂度[11]，其中|φ|递归定义[11]为：

1)若φ∈P∪{true,false}，则|φ|=1；

2)|φ1∨φ2|=|φ1∧φ2|=|φ1|+|φ2|+1；

算法1Update-Prop(K,φ,α,s)输入：模糊Kripke结构K=(S,s0,R,V)，s∈S，阈值α∈[0,1]，α-可满足的FCTL命题逻辑φ，‖φ‖K(s)<α。输出：模糊Kripke结构K1满足‖φ‖K1(s)≥α。

1)将模糊KripkeK1、K2和K3初始化为K；

2)caseφ=p且p∈P；

3)if ‖p‖K(s)<αthen；

4)K1←fInc-Prop(K,s,p,α-‖p‖K(s))；

7)K1←fDec-Prop(K,s,p,α-1+‖p‖K(s))；

8)caseφ=φ1∨φ2且φ1和φ2为α-可满足的FCTL命题逻辑；

9)K2←Update-Prop(K,φ1,α,s)；

10)K3←Update-Prop(K,φ2,α,s)；

11)ifd(K,K2)

12)K1←K2；

13)elseK1←K3；

14)caseφ=φ1∧φ2且φ1和φ2为α-可满足的FCTL命题逻辑；

15)K1←Update-Prop(K,φ1,α,s)；

16)K1←Update-Prop(K1,φ2,α,s)；

17)returnK1。

命题1算法1终止时返回的模糊Kripke结构K1为满足φ的α-极小修复模型。

证明对φ的结构采用数学归纳法证明。

1)当φ=p，其中p∈P时，由算法步骤2)知，算法将执行步骤3)、4)，若‖p‖K(s)<α，则执行步骤4)后，有‖p‖K1(s)=α。此时返回的K1满足：

d(K,K1)=α-‖p‖K(s)，

‖φ‖K1(s)≥α。

若K1不是满足φ的α-极小修复模型，则必然存在K′，使得

d(K,K′)

‖φ‖K′(s)≥α。

因为

‖p‖K(s)+d(K,K′)=

‖p‖K(s)+‖p‖K′(s)-‖p‖K(s)<α，

‖p‖K′(s)<α，这与‖φ‖K′(s)=‖p‖K′(s)≥α矛盾，所以K1是满足φ的α-极小修复模型。

3)当φ=φ1∨φ2，由算法步骤8)知，算法将执行步骤8)～13)。根据归纳假设，K2为满足‖φ1‖K2(s)≥α的α-极小修复模型，K3为满足‖φ2‖K3(s)≥α的α-极小修复模型。由步骤11)～13)知，返回的K1满足‖φ‖K1(s)=‖φ1‖K1(s)∨‖φ2‖K1(s)≥α。若K1不是满足φ的α-极小修复模型，则必然存在一个满足φ的α-极小修复模型K′。根据‖φ‖K′(s)=‖φ1‖K′(s)∨‖φ2‖K′(s)≥α可知，K′也是满足φ1或φ2的α-极小修复模型，这与已知K2是满足φ1的α-极小修复模型和K3是满足φ2的α-极小修复模型矛盾。因此，K1是满足φ的α-极小修复模型。

4)当φ=φ1∧φ2，由算法步骤14)知，算法将执行步骤15)、16)。根据归纳假设，算法执行步骤15)后，K1为满足‖φ1‖K1(s)≥α的α-极小修复模型，算法执行步骤16)后，K1为满足‖φ2‖K1(s)≥α的α-极小修复模型。此时返回的K1满足

‖φ‖K1(s)=‖φ1‖K1(s)∧‖φ2‖K1(s)≥α。若K1不是满足φ的α-极小修复模型，则必然存在一个满足φ的α-极小修复模型K′。根据‖φ‖K′(s)=‖φ1‖K′(s)∧‖φ2‖K′(s)≥α可知，K′是满足φ1的α-极小修复模型，也是满足φ2的α-极小修复模型，与已知K1是满足φ2的α-极小修复模型矛盾。因此，K1是满足φ的α-极小修复模型。

命题2算法1的时间复杂度为O(|φ|(O(K,φ)+(|S|2+|S||P|)))。

证明设T(|φ|)为算法1的时间复杂度。

1)当|φ|≤2，算法执行步骤3)、4)或步骤6)、7)，步骤3)的时间复杂性度为FCTL模型检测的时间复杂度O(K,φ)，步骤4)的时间复杂度为O(1)，步骤6)、7)与步骤3)、4)的时间复杂度相同。

2)当|φ|>2，算法执行步骤9)～13)或步骤15)、16)。设φ1的长度为d|φ|，则φ2的长度为(1-d)|φ|，其中d为φ1的长度与φ的长度的比值。步骤9)的时间复杂度为T(d|φ|)，步骤10)的时间复杂度为T((1-d)|φ|)。由模糊Kripke结构距离的定义知，步骤11)的时间复杂度为O(|S|2+|S||P|)，步骤12)的时间复杂度为O(1)，步骤13)的时间复杂度为O(1)，步骤15)的时间复杂度为T(d|φ|)，步骤16)的时间复杂度为T((1-d)|φ|)。因为步骤9)～13)和步骤15)、16)不可能同时执行，且步骤15)、16)的时间复杂度小于步骤9)～13)的时间复杂度，所以算法的时间复杂度只需考虑步骤9)～13)即可。

根据上述分析，得到以下递推式

设b=O(|S|2+|S||P|)，d≥1-d，0.5≤d<1，有

T(|φ|)=T(d|φ|)+T((1-d)|φ|)+b=

T(d2|φ|)+T(d(1-d)|φ|)+

T(d(1-d)|φ|)+T((1-d)2|φ|)+

|φ|O(K,φ)+b(|φ|-1)=

|φ|O(K,φ)+(|S|2+|S||P|)(|φ|-1)=

|φ|(O(K,φ)+(|S|2+|S||P|))。

因此，可得算法1的时间复杂度为

T(|φ|)=O(|φ|(O(K,φ)+

(|S|2+|S||P|)))。

算法2Update-EX(∃Xφ)。输入：模糊Kripke结构K=(S,s0,R,V)，阈值α∈[0,1]，α-可满足的FCTL ∃Xφ，其中φ为α-可满足的FCTL命题逻辑，‖∃Xφ‖K(s0)<α。输出：模糊Kripke结构K1满足‖∃Xφ‖K1(s0)≥α。

1)将模糊Kripke结构K1和K2初始化为K；

2)Ddis← +∞；

3)for 每个s∈Sdo；

4)if ‖φ‖K(s)<αthen，

K2←Update-Prop(K,φ,α,s)；

5)ifR(s0,s)<αthen，

K2←fInc-Val(K2,s0,s,α-R(s0,s))；

6)ifd(K,K2)

7)K1←K2；

8)Ddis←d(K,K2)；

9)returnK1。

命题3算法2终止时返回的模糊Kripke结构K1为满足∃Xφ的α-极小修复模型，且算法2的时间复杂度为

O(|S||φ|(O(K,φ)+(|S|2+|S||P|)))。

证明首先证明算法的正确性。步骤3)表示循环遍历每个状态s∈S，目的是从所有可能的修复模型中找到极小修复模型。若‖φ‖K(s)<α，则执行步骤4)后，由命题1知，K2为满足φ的α-极小修复模型。若R(s0,s)<α，则执行步骤5)后，R(s0,s)=α，且R(s0,s)的值只能为α，因为当R(s0,s)>α，由FKS间距离的定义知，d(K,K2)的值将会变大，此时状态s满足：

‖φ‖K2(s)≥α，R(s0,s)≥α。

由FCTL∃Xφ的语义知，

‖φ‖K2(π(1)))≥α，

这仅说明找到了一个修复模型K2满足‖∃Xφ‖K2(s0)≥α。执行步骤6)～8)，若d(K,K2)

算法2的时间复杂度分析。步骤1)、2)的时间复杂度为O(1)；步骤3)遍历状态集S中的每个状态，时间复杂度为O(|S|)；步骤4)的时间复杂度取决于Update-Prop操作，由命题1知，时间复杂度为O(|φ|(O(K,φ)+(|S|2+|S||P|)))；步骤5)的时间复杂度为O(1)；由模糊Kripke结构距离的定义知，步骤6)的时间复杂度为O(|S|2+|S||P|)；步骤7)、8)的时间复杂度为O(1)。算法2的时间复杂度为

O(|S||φ|(O(K,φ)+(|S|2+|S||P|)))。

4 结束语

针对模糊计算树逻辑模型检测的修复问题，提出了模糊计算树逻辑的模型检测修复算法。采用分治策略解决FCTL命题逻辑的修复问题，使用Inc-Prop操作和Dec-Prop操作对模糊Kripke结构进行修复，并根据模糊Kripke结构距离的定义，对修复模型进行比较，在多项式时间内返回一个满足FCTL命题逻辑的α-极小修复模型。采用Inc-Val操作和Update-Prop操作解决∃X的修复问题，在多项式时间内返回一个满足∃X的α-极小修复模型。今后将继续研究FCTL中的∀X、∃G、∀G、∃U和∀U的修复问题。