馬占有，李健祥，李召愷，郭 昊

(北方民族大學(xué) 計(jì)算機(jī)科學(xué)與工程學(xué)院 寧夏 銀川 750021)

0 引言

模型檢測(cè)(model checking)[1]作為一種高效的形式化驗(yàn)證方法，由于其自動(dòng)驗(yàn)證的優(yōu)點(diǎn)，廣泛應(yīng)用于計(jì)算機(jī)軟硬件的正確性與安全性驗(yàn)證[2-5]。模型檢測(cè)技術(shù)的基本思想是將現(xiàn)實(shí)中的系統(tǒng)抽象為狀態(tài)遷移系統(tǒng)模型，通過特定的時(shí)序邏輯[6-7]描述系統(tǒng)的性質(zhì)，例如計(jì)算樹邏輯(computation tree logic, CTL)[8-10]，并采用對(duì)應(yīng)的模型檢測(cè)算法驗(yàn)證系統(tǒng)模型是否滿足相應(yīng)的性質(zhì)。若滿足，驗(yàn)證通過；若不滿足，則給出反例。傳統(tǒng)的模型檢測(cè)方法起初是為了驗(yàn)證系統(tǒng)中定性屬性而設(shè)計(jì)的，例如安全性與活性。然而，許多復(fù)雜的系統(tǒng)具有隨機(jī)性、非可加性等定量特征[11-12]，無法通過經(jīng)典模型檢測(cè)方法驗(yàn)證。因此，定量的模型檢測(cè)方法引起了學(xué)術(shù)界與工業(yè)界的重視。

在模糊理論基礎(chǔ)上，將可能性測(cè)度理論[13]與模型檢測(cè)方法結(jié)合，文獻(xiàn)[14-18]提出了可能性計(jì)算樹邏輯模型檢測(cè)方法。該方法以可能性Kripke結(jié)構(gòu)或廣義可能性Kripke結(jié)構(gòu)作為系統(tǒng)模型，兩種模型的主要區(qū)別是可能性Kripke結(jié)構(gòu)要求狀態(tài)轉(zhuǎn)移關(guān)系中必須存在可能性為1的轉(zhuǎn)移，而廣義可能性Kripke結(jié)構(gòu)則不要求。在此基礎(chǔ)上，我們提出了基于決策過程的廣義可能性計(jì)算樹邏輯模型檢測(cè)方法[15]，主要用于具有非確定性與信息不完備性系統(tǒng)的驗(yàn)證。該方法的主要特點(diǎn)是引入了決策過程，以廣義可能性決策過程作為模型(generalized possibilistic decision processes, GPDP)[16]，廣義可能性計(jì)算樹邏輯(generalized possibilistic CTL, GPoCTL)[17-18]描述系統(tǒng)的性質(zhì)，最終通過算法將模型檢測(cè)問題[19-21]轉(zhuǎn)換為復(fù)雜度較低的模糊矩陣合成運(yùn)算。

在實(shí)際的系統(tǒng)設(shè)計(jì)中，系統(tǒng)產(chǎn)生的成本開銷、能耗[22]等也是我們需要重視的問題。例如，在醫(yī)療專家系統(tǒng)中，除治療效果外，我們還關(guān)心每種治療方案所產(chǎn)生的費(fèi)用，從而能夠選取性價(jià)比最高的診療方案。在工程管理中，要考慮到花費(fèi)的人力資源、財(cái)力、時(shí)間成本等諸多因素，并綜合分析出最優(yōu)方案[23]。廣義可能性決策過程模型雖然能夠?qū)哂胁煌陚湫畔⒌姆谴_定性系統(tǒng)進(jìn)行建模，但無法刻畫這類系統(tǒng)所產(chǎn)生的成本開銷、能耗等量化特征。為解決此類問題，我們?cè)趶V義可能性決策過程模型的基礎(chǔ)上增加了成本約束，在進(jìn)行動(dòng)作的非確定選擇時(shí)會(huì)產(chǎn)生相應(yīng)的成本開銷，從而能夠?qū)ο到y(tǒng)的實(shí)際成本進(jìn)行分析，豐富了GPoCTL模型檢測(cè)的應(yīng)用場(chǎng)景。

針對(duì)需要考慮成本開銷的非確定系統(tǒng)，本文首先引入帶成本的廣義可能性決策過程模型，接著給出此模型下GPoCTL的語法及語義，最后研究帶成本的GPoCTL模型檢測(cè)算法。此外，我們還將給出此模型在病人診療專家系統(tǒng)中的應(yīng)用。

1 預(yù)備知識(shí)

本文用到了一些模糊數(shù)學(xué)的運(yùn)算符號(hào)，下面給出其定義。

定義1[21]設(shè)X為普通集合，集合X上模糊集合滿足映射A:X→[0,1],A也稱為模糊集合A的隸屬度函數(shù)，對(duì)x∈X,A(x)稱為x屬于模糊集A的隸屬度。

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

定義2[21]設(shè)A,B∈F(X)，A與B的并A∪B、交A∩B、補(bǔ)Ac的隸屬函數(shù)定義為

本文是對(duì)廣義可能性決策過程進(jìn)行擴(kuò)展得到帶成本的廣義可能性決策過程，下面給出廣義可能性決策過程的定義。

定義3[15]廣義可能性決策過程(generalized possibilistic decision processes, GPDPs)由六元組M=(S,Act,p,I,AP,L)定義，其中：

1)S是可數(shù)非空狀態(tài)集合;

2)Act是動(dòng)作集;

3)p:S×Act×S→[0,1]是可能性轉(zhuǎn)移分布，對(duì)于任意s∈S,α∈Act，存在狀態(tài)t∈S，使P(s,α,t)>0;

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

5)AP是原子命題集合;

6)L:S×AP→[0,1]是標(biāo)簽函數(shù)，L(s,a)表示原子命題a在狀態(tài)s上成立的真值。

2 帶成本的廣義可能性決策過程

對(duì)GPDP六元組進(jìn)行擴(kuò)展，增加成本函數(shù)，從而得到帶成本的廣義可能性決策過程，其形式化定義如下。

定義4帶成本的廣義可能性決策過程(generalized possibilistic decision processes with costs, CGPDP)是一個(gè)七元組Mc=(S,Act,p,I,AP,L,C)，其中：

1)S是可數(shù)非空狀態(tài)集合;

2)Act是動(dòng)作集;

3)p:S×Act×S→[0,1]是可能性轉(zhuǎn)移分布，對(duì)于任意s∈S,α∈Act，存在狀態(tài)t∈S，使P(s,α,t)>0;

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

5)AP是原子命題集合;

6)L:S×AP→[0,1]是標(biāo)簽函數(shù)，L(s,a)表示原子命題a在狀態(tài)s上成立的真值。

7)C:S×Act→N(N為自然數(shù)集)是成本函數(shù)，對(duì)于任意s∈S,α∈Act，產(chǎn)生成本C(s,α)。

若動(dòng)作集與原子命題集均有窮，則稱Mc為有窮CGPDP。若存在一狀態(tài)t∈S，使得p(s,α,t)>0，則稱α在狀態(tài)s上是可激活的，Act(s)表示s所有可激活的動(dòng)作集合。

對(duì)于π=s0α0s1α1s2…∈(S×Act)ω，集合F?S，當(dāng)π能夠最終訪問F中所包含的任意狀態(tài)時(shí)，該路徑到達(dá)F的累積成本為

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

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

注1給定集合A、B，A×B表示集合A與B的笛卡爾積。

圖1 CGPDP模型實(shí)例(4狀態(tài))Figure 1 CGPDP model example (4 states)

對(duì)于路徑π=s0αs1βs2αs2…，第3步的瞬時(shí)成本C(s2,α)=120，前3步累積成本為

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

C(s2,α)=420。

對(duì)于集合F={s2,s3}，π到達(dá)F的累積成本為

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

由例1可以看出，CGPDP中的狀態(tài)可以選擇多個(gè)動(dòng)作。如s1在轉(zhuǎn)移時(shí)可選擇動(dòng)作α或β，這種選擇是非確定的。為消除CGPDP中狀態(tài)對(duì)動(dòng)作的非確定性選擇，我們引入調(diào)度。

定義5給定一個(gè)有窮的CGPDPMc=(S,Act,p,I,AP,L,C)，定義函數(shù)Adv:S→Act為Mc的調(diào)度。對(duì)任意s∈S，有Adv(s)∈Act(s)。

定義6設(shè)Mc=(S,Act,p,I,AP,L,C)是有窮的CGPDP，定義函數(shù)rAdv:S→[0,1]為

rAdv(s)是在調(diào)度Adv下，從狀態(tài)s出發(fā)的最大可能性。文獻(xiàn)[15]的定理1已經(jīng)給出了rAdv(s)的計(jì)算過程，此處直接引用。

定義8給定有窮的CGPDPMc，則函數(shù)GPo:PathsAdv(Mc)→[0,1]定義為

對(duì)于任意集合F?PathsAdv(Mc)，有GPo(F)=∨{GPo(π)|π∈F}，即可擴(kuò)展為函數(shù)GPo:2PathsAdv(Mc)→[0,1]，稱為集合2PathsAdv(Mc)上的廣義可能性測(cè)度。

3 期望成本

引入調(diào)度Adv后，CGPDP中任意狀態(tài)s在Adv下的轉(zhuǎn)移動(dòng)作α得以確定。由s出發(fā)不斷通過Adv確定的動(dòng)作發(fā)生轉(zhuǎn)移，從而產(chǎn)生路徑集合PathsAdv(s)。為定量刻畫這些路徑所產(chǎn)生的成本，結(jié)合廣義可能性模型檢測(cè)中的理論，我們引入了期望成本這一概念。CGPDP中的期望成本主要包括瞬時(shí)期望成本、累積期望成本與可達(dá)期望成本。

定義9給定有窮CGPDPMc，在調(diào)度Adv下，PathsAdv(s)中所有路徑在第k步瞬時(shí)成本cost[=k]的期望值，稱為從s出發(fā)第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是到達(dá)F的所有路徑長(zhǎng)度的最大值。帶成本的廣義可能性決策過程計(jì)算樹邏輯模型檢測(cè)問題首先考慮的是滿足公式的可能性，然后再計(jì)算期望成本。在計(jì)算可能性時(shí)，本文使用有窮路徑的可能性來計(jì)算無窮路徑的可能性，故考慮成本時(shí)，也只考慮有窮路徑的期望成本，即只考慮一次或有限次的自環(huán)。

4 帶成本廣義可能性計(jì)算樹邏輯

定義12(GPoCTL語法) GPoCTL狀態(tài)公式定義為

其中：φ是路徑公式；a∈AP。(=k)、(≤k)、(Φ)分別表示第k步瞬時(shí)期望成本公式、前k步累積期望成本公式和可達(dá)期望成本公式。

GPoCTL路徑公式

其中：Φ、Φ1、Φ2是狀態(tài)公式；O、∪、◇、□分別表示“下一個(gè)”、“直到”、“最終”、“總是”。

定義13(GPoCTL語義)

設(shè)Mc=(S,Act,p,I,AP,L,C)是一個(gè)有窮的CGPDP，‖Φ‖:S→[0,1]是S的模糊子集，對(duì)于帶成本的GPoCTL，其狀態(tài)公式Φ的語義定義為

‖true‖(s)=1，

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

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

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

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

對(duì)于路徑公式φ，對(duì)應(yīng)于Mc上語義為‖φ‖:PathsAdv(Mc)→[0,1]，歸納定義為

5 帶成本GPoCTL模型檢測(cè)算法

帶成本的GPoCTL模型檢測(cè)問題描述為：給定CGPDPMc、Mc中的狀態(tài)s及GPoCTL狀態(tài)公式Φ，計(jì)算‖Φ‖(s)的值。對(duì)于狀態(tài)公式Φ=true,Φ=a,Φ=Φ1∧Φ2,Φ=Φ，可直接由語義給出相應(yīng)的模型檢測(cè)算法。對(duì)于GPo(φ)算子，引入文獻(xiàn)[15]中的算法，包括算法1和算法2。對(duì)于第k步瞬時(shí)期望成本公式(=k)，前k步累積期望成本公式(≤k)，可達(dá)期望成本公式(Φ)，將分別給出它們對(duì)應(yīng)的模型檢測(cè)算法。

算法1不動(dòng)點(diǎn)算法

Require: 不動(dòng)點(diǎn)函數(shù)f

Ensure: 不動(dòng)點(diǎn)x

procedureFixPoint(x,f)

x′=f(x)

whilex≠x′ do

x=x′

x′=f(x)

end while

returnx

end procedure

算法2主要采用模糊矩陣合成運(yùn)算方式來計(jì)算路徑公式的廣義可能性。

算法2計(jì)算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給出了瞬時(shí)期望成本的迭代計(jì)算形式，依此可得到瞬時(shí)期望成本算子(=k)的遞歸求解算法，具體步驟詳見算法3。

算法3計(jì)算(=k)的算法

Require: CGPDPMc和步數(shù)k

Ensure:Mc中任意狀態(tài)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)是一個(gè)有窮的CGPDP，對(duì)任意s∈S，有

證明

依據(jù)定理2，算法4給出累積期望成本算法。

算法4計(jì)算(≤k)的算法

Require: CGPDPMc和步數(shù)k

Ensure:Mc中任意狀態(tài)s，(≤k)的值

procedureExKsteps(s,k)

ifk=0 then

return 0

end if

end procedure

定理3給定有窮的CGPDPMc，對(duì)任意s∈S，若GPo(s|=◇Sat(Φ))>0且s?Sat(Φ)，則有：

證明

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

依據(jù)定理3，算法5給出可達(dá)期望成本算法。

算法5計(jì)算(Φ)的算法

Require: CPDPMc和狀態(tài)公式Φ

Ensure:Mc中任意狀態(tài)s，(Φ)的值

procedureExPhi(s)

end procedure

依據(jù)算法1～5，算法6給出了帶成本的GPoCTL模型檢測(cè)算法。

算法6帶成本的GPoCTL模型檢測(cè)算法

Require: CGPDPMc和狀態(tài)公式Φ

Ensure:Mc中任意狀態(tài)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

上述算法的時(shí)間復(fù)雜度與文獻(xiàn)[15]中的計(jì)算方法相同，下面進(jìn)行算法的時(shí)間復(fù)雜度分析。

在所有調(diào)度Adv下，可以在|Φ|步遞歸計(jì)算出‖Φ‖(s)的值，這里|Φ|表示公式Φ的子公式數(shù)，其遞歸定義如下。

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

在GPoCTL模型檢測(cè)算法中，公式Φ=a|Φ1∧Φ2|Φ|GPo(OΦ)計(jì)算‖Φ‖(s)的時(shí)間只與CPDPMc的大小和公式Φ的長(zhǎng)度有關(guān)，公式Φ=(=k)|(≤k)計(jì)算‖Φ‖(s)的時(shí)間只與CPDPMc的大小、公式Φ的長(zhǎng)度和k的大小有關(guān)。而計(jì)算公式Φ=GPo(Φ1∪Φ2)|GPo(◇Φ)的時(shí)間主要取決于計(jì)算PAdv的轉(zhuǎn)移閉包的時(shí)間。采用文獻(xiàn)[24]的算法來計(jì)算其時(shí)間復(fù)雜度為O(n2logn)，其中n=|S|。公式Φ=GPo(□Φ)|(◇Φ)的時(shí)間主要取決于迭代時(shí)間和矩陣合成運(yùn)算時(shí)間，參照文獻(xiàn)[15]的迭代分析，可知迭代計(jì)算時(shí)間是O(|S|3)。綜上所述，通過定理4給定GPoCTL模型檢測(cè)算法的時(shí)間復(fù)雜度。

定理4(帶成本的GPoCTL模型檢測(cè)算法的時(shí)間復(fù)雜度) 給定有窮的CGPDPMc和帶成本的GPoCTL公式Φ、步數(shù)k、Mc|=Φ的時(shí)間復(fù)雜度為O(size(Mf)·poly(S)·|Φ|·k)，其中：size(Mf)是模型的大小；poly(S)是n的多項(xiàng)式函數(shù)；|Φ|是公式的長(zhǎng)度；k是步數(shù)。

6 實(shí)例應(yīng)用

本文在文獻(xiàn)[15]患者診療的專家系統(tǒng)的基礎(chǔ)上增加了成本回饋，用以說明帶成本GPoCTL模型檢測(cè)算法的實(shí)際應(yīng)用。通過CGPDPMc=(S,Act,p,I,AP,L,C)來對(duì)整個(gè)診療過程進(jìn)行建模。s0、s1、s2表示患者的健康狀態(tài)，原子命題集合AP={P,G,E}表示患者的健康狀況為P(差)、G(一般)、E(好)。專家對(duì)于患者健康狀況的判斷是主觀的，因此通過給三者賦予模糊值，表示患者的健康程度。三位專家的專業(yè)背景與經(jīng)驗(yàn)存在差異，他們針對(duì)患者狀況采取的診療方案也不盡相同，分別用動(dòng)作α、β、γ表示。當(dāng)狀態(tài)si激活某個(gè)動(dòng)作αi時(shí)，會(huì)產(chǎn)生成本回饋C(si,αi)，表示該方案的治療費(fèi)用。Mc可通過圖2描述。初始分布I及α、β、γ的可能性轉(zhuǎn)移矩陣為

圖2 患者診療過程CGPDP模型Figure 2 Treatment process of patients modeled by CGPDP

根據(jù)算法6，調(diào)度Adv取最大值，其過程是優(yōu)先考慮治愈病人的最大可能性，在此基礎(chǔ)上計(jì)算期望成本。同理，Adv取最小值則是考慮在治愈的最小可能性基礎(chǔ)上計(jì)算期望成本。

1)Adv取最大值，調(diào)用ExKstep(s2,6)迭代計(jì)算6次，最終計(jì)算得到從s2出發(fā)第6步的最大可能性瞬時(shí)期望成本‖(=6)‖max(s2)=230。再令A(yù)dv取最小值，調(diào)用ExKstep(s2,6)迭代計(jì)算6次，最終計(jì)算得到最小可能性瞬時(shí)期望成本‖(=6)‖min(s2)=11.76。說明在狀態(tài)Adv，醫(yī)生采用3種治療方案治療6次后，第6次治療的最大可能性期望費(fèi)用為230，最小可能性期望費(fèi)用為11.76。

2)Adv取最大值，調(diào)用ExKsteps(s0,6)迭代計(jì)算6次，最終得到從s0出發(fā)前6步的最大可能性累積期望成本‖(≤6)‖max(s0)=1 082.4。再令A(yù)dv取最小值，調(diào)用ExKsteps(s0,6)迭代計(jì)算6次，最終計(jì)算得到從s0出發(fā)前6步的最小可能性累積期望成本‖(≤6)‖min(s0)=111.3。說明在狀態(tài)‖E‖(s0)=0，醫(yī)生采用3種治療方案治療6次后，6次治療的累積最大可能性期望費(fèi)用為1 082.4，最小可能性期望費(fèi)用為111.3。

3) 由‖E‖(s0)=0，‖E‖(s1)=0.6，‖E‖(s2)=0.9，得Sat(E)={s1,s2}。Adv取最大值，迭代調(diào)用ExPhi(s0)，得到從s0出發(fā)，最終到達(dá)Sat(E)的最大可能性可達(dá)期望成本‖(E)‖max(s0)=432。再令A(yù)dv取最小值，迭代調(diào)用ExPhi(s0)，計(jì)算得到從狀態(tài)s0出發(fā)，最終到達(dá)Sat(E)的最小可能性可達(dá)期望成本‖(E)‖min(s0)=101.4。說明在狀態(tài)s0，醫(yī)生采用3種治療方案治療多次后，病人最終健康狀況為“好”的最大可能性期望費(fèi)用為432，最小可能性期望費(fèi)用為101.4。

7 結(jié)束語

為解決GPoCTL模型檢測(cè)中的成本問題，本文提出了帶成本的GPoCTL模型檢測(cè)方法。引入了帶成本的廣義可能性決策過程模型并在此基礎(chǔ)上給出了期望成本，進(jìn)而擴(kuò)展得到帶成本GPoCTL，增強(qiáng)了原有邏輯的表達(dá)能力。接著通過證明期望算子滿足迭代計(jì)算形式，從而擴(kuò)展了帶成本的GPoCTL模型檢測(cè)算法，最后通過實(shí)例說明其實(shí)際應(yīng)用。