广义可能性计算树逻辑模型检测中的成本分析

马占有，李健祥，李召恺，郭 昊

(北方民族大学 计算机科学与工程学院 宁夏 银川 750021)

0 引言

模型检测(model checking)[1]作为一种高效的形式化验证方法，由于其自动验证的优点，广泛应用于计算机软硬件的正确性与安全性验证[2-5]。模型检测技术的基本思想是将现实中的系统抽象为状态迁移系统模型，通过特定的时序逻辑[6-7]描述系统的性质，例如计算树逻辑(computation tree logic, CTL)[8-10]，并采用对应的模型检测算法验证系统模型是否满足相应的性质。若满足，验证通过；若不满足，则给出反例。传统的模型检测方法起初是为了验证系统中定性属性而设计的，例如安全性与活性。然而，许多复杂的系统具有随机性、非可加性等定量特征[11-12]，无法通过经典模型检测方法验证。因此，定量的模型检测方法引起了学术界与工业界的重视。

在模糊理论基础上，将可能性测度理论[13]与模型检测方法结合，文献[14-18]提出了可能性计算树逻辑模型检测方法。该方法以可能性Kripke结构或广义可能性Kripke结构作为系统模型，两种模型的主要区别是可能性Kripke结构要求状态转移关系中必须存在可能性为1的转移，而广义可能性Kripke结构则不要求。在此基础上，我们提出了基于决策过程的广义可能性计算树逻辑模型检测方法[15]，主要用于具有非确定性与信息不完备性系统的验证。该方法的主要特点是引入了决策过程，以广义可能性决策过程作为模型(generalized possibilistic decision processes, GPDP)[16]，广义可能性计算树逻辑(generalized possibilistic CTL, GPoCTL)[17-18]描述系统的性质，最终通过算法将模型检测问题[19-21]转换为复杂度较低的模糊矩阵合成运算。

在实际的系统设计中，系统产生的成本开销、能耗[22]等也是我们需要重视的问题。例如，在医疗专家系统中，除治疗效果外，我们还关心每种治疗方案所产生的费用，从而能够选取性价比最高的诊疗方案。在工程管理中，要考虑到花费的人力资源、财力、时间成本等诸多因素，并综合分析出最优方案[23]。广义可能性决策过程模型虽然能够对具有不完备信息的非确定性系统进行建模，但无法刻画这类系统所产生的成本开销、能耗等量化特征。为解决此类问题，我们在广义可能性决策过程模型的基础上增加了成本约束，在进行动作的非确定选择时会产生相应的成本开销，从而能够对系统的实际成本进行分析，丰富了GPoCTL模型检测的应用场景。

针对需要考虑成本开销的非确定系统，本文首先引入带成本的广义可能性决策过程模型，接着给出此模型下GPoCTL的语法及语义，最后研究带成本的GPoCTL模型检测算法。此外，我们还将给出此模型在病人诊疗专家系统中的应用。

1 预备知识

本文用到了一些模糊数学的运算符号，下面给出其定义。

定义1[21]设X为普通集合，集合X上模糊集合满足映射A:X→[0,1],A也称为模糊集合A的隶属度函数，对x∈X,A(x)称为x属于模糊集A的隶属度。

用F(X)表示X上模糊集合的全体，即F(X)={A|A:X→[0,1]}。

定义2[21]设A,B∈F(X)，A与B的并A∪B、交A∩B、补Ac的隶属函数定义为

本文是对广义可能性决策过程进行扩展得到带成本的广义可能性决策过程，下面给出广义可能性决策过程的定义。

定义3[15]广义可能性决策过程(generalized possibilistic decision processes, GPDPs)由六元组M=(S,Act,p,I,AP,L)定义，其中：

1)S是可数非空状态集合;

2)Act是动作集;

3)p:S×Act×S→[0,1]是可能性转移分布，对于任意s∈S,α∈Act，存在状态t∈S，使P(s,α,t)>0;

4)I:S→[0,1]是可能性初始分布函数;

5)AP是原子命题集合;

6)L:S×AP→[0,1]是标签函数，L(s,a)表示原子命题a在状态s上成立的真值。

2 带成本的广义可能性决策过程

对GPDP六元组进行扩展，增加成本函数，从而得到带成本的广义可能性决策过程，其形式化定义如下。

定义4带成本的广义可能性决策过程(generalized possibilistic decision processes with costs, CGPDP)是一个七元组Mc=(S,Act,p,I,AP,L,C)，其中：

1)S是可数非空状态集合;

2)Act是动作集;

3)p:S×Act×S→[0,1]是可能性转移分布，对于任意s∈S,α∈Act，存在状态t∈S，使P(s,α,t)>0;

4)I:S→[0,1]是可能性初始分布函数;

5)AP是原子命题集合;

6)L:S×AP→[0,1]是标签函数，L(s,a)表示原子命题a在状态s上成立的真值。

7)C:S×Act→N(N为自然数集)是成本函数，对于任意s∈S,α∈Act，产生成本C(s,α)。

若动作集与原子命题集均有穷，则称Mc为有穷CGPDP。若存在一状态t∈S，使得p(s,α,t)>0，则称α在状态s上是可激活的，Act(s)表示s所有可激活的动作集合。

对于π=s0α0s1α1s2…∈(S×Act)ω，集合F⊆S，当π能够最终访问F中所包含的任意状态时，该路径到达F的累积成本为

cost[◇F](π)=cost[≤n](π)，

其中：sn∈F且s0,…,sn-1∉F。

注1给定集合A、B，A×B表示集合A与B的笛卡尔积。

图1 CGPDP模型实例(4状态)Figure 1 CGPDP model example (4 states)

对于路径π=s0αs1βs2αs2…，第3步的瞬时成本C(s2,α)=120，前3步累积成本为

cost[≤3](π)=C(s0,α)+C(s1,β)+

C(s2,α)=420。

对于集合F={s2,s3}，π到达F的累积成本为

cost[◇F](π)=C(s0,α)+C(s1,β)=300。

由例1可以看出，CGPDP中的状态可以选择多个动作。如s1在转移时可选择动作α或β，这种选择是非确定的。为消除CGPDP中状态对动作的非确定性选择，我们引入调度。

定义5给定一个有穷的CGPDPMc=(S,Act,p,I,AP,L,C)，定义函数Adv:S→Act为Mc的调度。对任意s∈S，有Adv(s)∈Act(s)。

定义6设Mc=(S,Act,p,I,AP,L,C)是有穷的CGPDP，定义函数rAdv:S→[0,1]为

rAdv(s)是在调度Adv下，从状态s出发的最大可能性。文献[15]的定理1已经给出了rAdv(s)的计算过程，此处直接引用。

定义8给定有穷的CGPDPMc，则函数GPo:PathsAdv(Mc)→[0,1]定义为

对于任意集合F⊆PathsAdv(Mc)，有GPo(F)=∨{GPo(π)|π∈F}，即可扩展为函数GPo:2PathsAdv(Mc)→[0,1]，称为集合2PathsAdv(Mc)上的广义可能性测度。

3 期望成本

引入调度Adv后，CGPDP中任意状态s在Adv下的转移动作α得以确定。由s出发不断通过Adv确定的动作发生转移，从而产生路径集合PathsAdv(s)。为定量刻画这些路径所产生的成本，结合广义可能性模型检测中的理论，我们引入了期望成本这一概念。CGPDP中的期望成本主要包括瞬时期望成本、累积期望成本与可达期望成本。

定义9给定有穷CGPDPMc，在调度Adv下，PathsAdv(s)中所有路径在第k步瞬时成本cost[=k]的期望值，称为从s出发第k步的期望成本，递归定义为

若k=1，则

若k>1，则

若k=1，则

若k>1，则

其中：S′={s∈S|GPo(s|=◇F)>0且s∉F}。

若GPo(s|=◇F)>0且s∉F，则

n是到达F的所有路径长度的最大值。带成本的广义可能性决策过程计算树逻辑模型检测问题首先考虑的是满足公式的可能性，然后再计算期望成本。在计算可能性时，本文使用有穷路径的可能性来计算无穷路径的可能性，故考虑成本时，也只考虑有穷路径的期望成本，即只考虑一次或有限次的自环。

4 带成本广义可能性计算树逻辑

定义12(GPoCTL语法) GPoCTL状态公式定义为

其中：φ是路径公式；a∈AP。(=k)、(≤k)、(Φ)分别表示第k步瞬时期望成本公式、前k步累积期望成本公式和可达期望成本公式。

GPoCTL路径公式

其中：Φ、Φ1、Φ2是状态公式；O、∪、◇、□分别表示“下一个”、“直到”、“最终”、“总是”。

定义13(GPoCTL语义)

设Mc=(S,Act,p,I,AP,L,C)是一个有穷的CGPDP，‖Φ‖:S→[0,1]是S的模糊子集，对于带成本的GPoCTL，其状态公式Φ的语义定义为

‖true‖(s)=1，

‖a‖(s)=L(s,a)，

‖Φ1∧Φ2‖(s)=‖Φ1‖(s)∧‖Φ2‖(s)，

‖GPo(φ)‖(s)=GPo(s|=φ)，

其中：Sat(Φ)={s∈S|‖Φ‖(s)>0}。

对于路径公式φ，对应于Mc上语义为‖φ‖:PathsAdv(Mc)→[0,1]，归纳定义为

5 带成本GPoCTL模型检测算法

带成本的GPoCTL模型检测问题描述为：给定CGPDPMc、Mc中的状态s及GPoCTL状态公式Φ，计算‖Φ‖(s)的值。对于状态公式Φ=true,Φ=a,Φ=Φ1∧Φ2,Φ=Φ，可直接由语义给出相应的模型检测算法。对于GPo(φ)算子，引入文献[15]中的算法，包括算法1和算法2。对于第k步瞬时期望成本公式(=k)，前k步累积期望成本公式(≤k)，可达期望成本公式(Φ)，将分别给出它们对应的模型检测算法。

算法1不动点算法

Require: 不动点函数f

Ensure: 不动点x

procedureFixPoint(x,f)

x′=f(x)

whilex≠x′ do

x=x′

x′=f(x)

end while

returnx

end procedure

算法2主要采用模糊矩阵合成运算方式来计算路径公式的广义可能性。

算法2计算GPo(φ)的算法

Require: 路径公式φ和CGPDPMc

Ensure:GPo(φ)的值

procedureGPoCTl(φ)

caseφ

OΦreturnPAdv∘DΦ∘RAdv

Φ1∪Φ2return (DΦ1∘PAdv)*DΦ2∘RAdv

□ΦreturnFixPoint((1)s∈S,fΦ)

end case

end procedure

定义6给出了瞬时期望成本的迭代计算形式，依此可得到瞬时期望成本算子(=k)的递归求解算法，具体步骤详见算法3。

算法3计算(=k)的算法

Require: CGPDPMc和步数k

Ensure:Mc中任意状态s，(=k)的值

procedureExKstep(s,k)

ifk=0 then

return 0

end if

ifk=1 then

end if

end procedure

定理2给定Mc=(S,Act,p,I,AP,L,C)是一个有穷的CGPDP，对任意s∈S，有

证明

依据定理2，算法4给出累积期望成本算法。

算法4计算(≤k)的算法

Require: CGPDPMc和步数k

Ensure:Mc中任意状态s，(≤k)的值

procedureExKsteps(s,k)

ifk=0 then

return 0

end if

end procedure

定理3给定有穷的CGPDPMc，对任意s∈S，若GPo(s|=◇Sat(Φ))>0且s∉Sat(Φ)，则有：

证明

其中：S′={s∉Sat(Φ)|GPo(s|=◇Sat(Φ))>0}。

依据定理3，算法5给出可达期望成本算法。

算法5计算(Φ)的算法

Require: CPDPMc和状态公式Φ

Ensure:Mc中任意状态s，(Φ)的值

procedureExPhi(s)

end procedure

依据算法1～5，算法6给出了带成本的GPoCTL模型检测算法。

算法6带成本的GPoCTL模型检测算法

Require: CGPDPMc和状态公式Φ

Ensure:Mc中任意状态s，‖Φ‖(s)的值

procedureGPoCTLCheck(Φ)

caseΦ

true return (1)s∈S

a∈APreturn (‖a‖(s))s∈S

Φ1∧Φ2return (‖Φ1‖(s)∧‖Φ2‖(s))s∈S

GPo(φ)returnGPoCal(φ)

end case

end procedure

上述算法的时间复杂度与文献[15]中的计算方法相同，下面进行算法的时间复杂度分析。

在所有调度Adv下，可以在|Φ|步递归计算出‖Φ‖(s)的值，这里|Φ|表示公式Φ的子公式数，其递归定义如下。

若Φ=a或Φ=true，则|Φ|=1。

在GPoCTL模型检测算法中，公式Φ=a|Φ1∧Φ2|Φ|GPo(OΦ)计算‖Φ‖(s)的时间只与CPDPMc的大小和公式Φ的长度有关，公式Φ=(=k)|(≤k)计算‖Φ‖(s)的时间只与CPDPMc的大小、公式Φ的长度和k的大小有关。而计算公式Φ=GPo(Φ1∪Φ2)|GPo(◇Φ)的时间主要取决于计算PAdv的转移闭包的时间。采用文献[24]的算法来计算其时间复杂度为O(n2logn)，其中n=|S|。公式Φ=GPo(□Φ)|(◇Φ)的时间主要取决于迭代时间和矩阵合成运算时间，参照文献[15]的迭代分析，可知迭代计算时间是O(|S|3)。综上所述，通过定理4给定GPoCTL模型检测算法的时间复杂度。

定理4(带成本的GPoCTL模型检测算法的时间复杂度) 给定有穷的CGPDPMc和带成本的GPoCTL公式Φ、步数k、Mc|=Φ的时间复杂度为O(size(Mf)·poly(S)·|Φ|·k)，其中：size(Mf)是模型的大小；poly(S)是n的多项式函数；|Φ|是公式的长度；k是步数。

6 实例应用

本文在文献[15]患者诊疗的专家系统的基础上增加了成本回馈，用以说明带成本GPoCTL模型检测算法的实际应用。通过CGPDPMc=(S,Act,p,I,AP,L,C)来对整个诊疗过程进行建模。s0、s1、s2表示患者的健康状态，原子命题集合AP={P,G,E}表示患者的健康状况为P(差)、G(一般)、E(好)。专家对于患者健康状况的判断是主观的，因此通过给三者赋予模糊值，表示患者的健康程度。三位专家的专业背景与经验存在差异，他们针对患者状况采取的诊疗方案也不尽相同，分别用动作α、β、γ表示。当状态si激活某个动作αi时，会产生成本回馈C(si,αi)，表示该方案的治疗费用。Mc可通过图2描述。初始分布I及α、β、γ的可能性转移矩阵为

图2 患者诊疗过程CGPDP模型Figure 2 Treatment process of patients modeled by CGPDP

根据算法6，调度Adv取最大值，其过程是优先考虑治愈病人的最大可能性，在此基础上计算期望成本。同理，Adv取最小值则是考虑在治愈的最小可能性基础上计算期望成本。

1)Adv取最大值，调用ExKstep(s2,6)迭代计算6次，最终计算得到从s2出发第6步的最大可能性瞬时期望成本‖(=6)‖max(s2)=230。再令Adv取最小值，调用ExKstep(s2,6)迭代计算6次，最终计算得到最小可能性瞬时期望成本‖(=6)‖min(s2)=11.76。说明在状态Adv，医生采用3种治疗方案治疗6次后，第6次治疗的最大可能性期望费用为230，最小可能性期望费用为11.76。

2)Adv取最大值，调用ExKsteps(s0,6)迭代计算6次，最终得到从s0出发前6步的最大可能性累积期望成本‖(≤6)‖max(s0)=1 082.4。再令Adv取最小值，调用ExKsteps(s0,6)迭代计算6次，最终计算得到从s0出发前6步的最小可能性累积期望成本‖(≤6)‖min(s0)=111.3。说明在状态‖E‖(s0)=0，医生采用3种治疗方案治疗6次后，6次治疗的累积最大可能性期望费用为1 082.4，最小可能性期望费用为111.3。

3) 由‖E‖(s0)=0，‖E‖(s1)=0.6，‖E‖(s2)=0.9，得Sat(E)={s1,s2}。Adv取最大值，迭代调用ExPhi(s0)，得到从s0出发，最终到达Sat(E)的最大可能性可达期望成本‖(E)‖max(s0)=432。再令Adv取最小值，迭代调用ExPhi(s0)，计算得到从状态s0出发，最终到达Sat(E)的最小可能性可达期望成本‖(E)‖min(s0)=101.4。说明在状态s0，医生采用3种治疗方案治疗多次后，病人最终健康状况为“好”的最大可能性期望费用为432，最小可能性期望费用为101.4。

7 结束语

为解决GPoCTL模型检测中的成本问题，本文提出了带成本的GPoCTL模型检测方法。引入了带成本的广义可能性决策过程模型并在此基础上给出了期望成本，进而扩展得到带成本GPoCTL，增强了原有逻辑的表达能力。接着通过证明期望算子满足迭代计算形式，从而扩展了带成本的GPoCTL模型检测算法，最后通过实例说明其实际应用。