劉子源,馬占有,李 霞,高瀅囡,何娜娜,黃瑞祺

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

1 引言

模型檢測[1-3]是形式化驗證的重要方法,其思想為用狀態(tài)轉(zhuǎn)換系統(tǒng)M表示系統(tǒng)模型的行為,使用邏輯公式F描述系統(tǒng)的性質(zhì),該系統(tǒng)能否滿足此性質(zhì)的模型檢測問題轉(zhuǎn)換為M是否滿足邏輯公式F,若滿足,通過驗證;不滿足,返回一個反例[4]。模型檢測具有自動化驗證的特點,并且以圖論算法、數(shù)據(jù)結(jié)構(gòu)和邏輯等理論作為基礎(chǔ)[1],因此被廣泛用于嵌入式系統(tǒng)、軟件工程和硬件設(shè)計等領(lǐng)域。模型檢測主要包括線性時序邏輯LTL(Liner Temporal Logic)模型檢測和計算樹邏輯CTL(Computation Tree Logic)模型檢測等[5]。LTL和CTL的表達能力是無法比較的,在LTL中某些公式?jīng)]有與之等價的CTL公式;同樣在CTL中某些公式也不存在與之等價的LTL公式。分支時態(tài)邏輯CTL*(Computation Tree Logic*)包含了CTL和LTL兩者的邏輯特性,可以表示CTL和LTL都無法表示的屬性規(guī)約[2],因此,CTL*的表達能力比CTL和LTL更強。CTL*模型檢測算法需要將LTL和CTL的檢測算法進行適當(dāng)組合[1,6]。

經(jīng)典模型檢測是一種定性的驗證方法,對系統(tǒng)行為進行判定,結(jié)果只有正確和錯誤之分。定性模型檢測無法表示和驗證如“系統(tǒng)百分之九十的可能性不會死機”等屬性規(guī)約。為解決上述問題,研究人員提出了定量模型檢測,并受到廣泛關(guān)注。定量模型檢測主要包括概率模型檢測、多值模型檢測和模糊模型檢測等。其中,Hart等[7]提出的概率模型檢測用于解決模型檢測算法中隨機過程所造成的不確定性問題。Chechik等[8,9]提出的多值模型檢測用于處理模型檢測中含有不完全或不一致信息的問題。模糊模型檢測解決了數(shù)據(jù)表述不確定性的系統(tǒng)模型檢測問題[10]。

模糊模型檢測是模糊集合理論與模型檢測結(jié)合的模型檢測方法。Li等[11-15]首先將模糊理論的分支可能性測度與模型檢測進行結(jié)合,提出可能性模型檢測和廣義可能性模型檢測,通過模糊博弈驗證了模糊線性時序邏輯的可實現(xiàn)性。此外,范艷煥等[16]把不確定型模糊Kripke結(jié)構(gòu)作為系統(tǒng)模型,對模糊計算樹邏輯模型檢測問題進行研究,給出了時間復(fù)雜度為對數(shù)多項式時間的改進算法。潘海玉等[17,18]把模糊Kripke結(jié)構(gòu)作為系統(tǒng)模型,使用模糊計算樹邏輯對不同模糊Kripke結(jié)構(gòu)之間的關(guān)系進行研究,為模糊Kripke結(jié)構(gòu)上的模糊計算樹邏輯模型檢測提供了新的方法。李召愷等[10]對模糊計算樹邏輯模型檢測問題進行研究,提出了模糊決策過程FDP (Fuzzy Decision Process)并將其作為系統(tǒng)模型,對模糊計算樹邏輯模型檢測問題進行研究,給出了基于模糊決策過程的模糊計算樹邏輯模型檢測算法。

本文將FDP模型作為系統(tǒng)模型,對模糊分支時態(tài)邏輯FCTL*(Fuzzy Computation Tree Logic*)模型檢測問題進行研究,給出了FCTL*的語法和語義,本文參考文獻[19]中的廣義可能性測度理論,在模糊決策過程中引入模糊測度理論。然后給出FCTL*模型檢測算法,該算法將FCTL*模型檢測問題轉(zhuǎn)化為模糊矩陣的合成運算,其具有高效、可讀性強等優(yōu)勢。最后,對算法的復(fù)雜度進行了分析。

2 預(yù)備知識

本節(jié)介紹模糊集合概念和模糊矩陣運算等。

定義1[20,21]設(shè)X是經(jīng)典集合,X上的模糊集合A是X到[0,1]的一個映射,也被稱為模糊集合A的隸屬度函數(shù),A(x)表示x屬于模糊集合A的隸屬度,其中x∈X。

本文使用F(x)表示X上所有的模糊集合,即F(x)={A|A:X→[0,1]}。

定義2[20,21]設(shè)A,B∈F(x),任意x∈X,A與B的交、并、補的隸屬度函數(shù)定義如下:

(A∩B)(x)=A(x)∧B(x)=min{A(x),B(x)}

(A∪B)(x)=A(x)∨B(x)=max{A(x),B(x)}

Ac(x)=1-A(x)

定義3[21]設(shè)X=(xuv)m× n,Y=(yuv)m× n均為m行n列模糊矩陣,X和Y的交、并、補定義如下:

X∩Y=(xuv∧yuv)m×n

X∪Y=(xuv∨yuv)m×n

Xc=(1-xuv)m×n

定義4[22]設(shè)X=(xuv)m×n是m行n列的模糊矩陣,Y=(yuv)n×l是n行l(wèi)列的模糊矩陣,X和Y的內(nèi)積定義如下:

X°Y=(zuv)m×l

(u=1,…,m;v=1,…,l)

設(shè)P為模糊矩陣,其傳遞閉包[19]定義如下:

P+=P∨P2∨…∨P|S|

其中,S有窮且Pk+1=Pk°P。

對于P,克林閉包P*定義為:P*=P0∨P+,其中P0為恒等矩陣。

3 模糊決策過程

本文采用文獻[10]中提出的模糊決策過程作為模型,并在此基礎(chǔ)上引入模糊測度。

定義5[10]FDP用于復(fù)雜模糊系統(tǒng)模型建模,是一個六元組Mf=(S,Act,P,I,AP,L):

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

(2)Act為動作集;

(3)P:S×Act×S→[0,1]為模糊轉(zhuǎn)移函數(shù),對于s∈S,α∈Act,有t∈S,使P(s,α,t)>0;

(4)I:S→[0,1]為初始分布函數(shù),對于s∈S,I(s)表示初始狀態(tài)是s的可能性真值;

(5)AP是原子命題集;

(6)L:S×AP→[0,1]為模糊標(biāo)簽函數(shù),L(s,a)為命題a在狀態(tài)s上的可能值,其中s∈S,a∈AP。

給定一個FDPMf,則稱s0α0s1α1s2…∈π是從s0出發(fā)的無限路徑當(dāng)且僅當(dāng)對于任意的i有P(si,αi,si+1)>0,其中π表示S上所有無限序列的集合。

定義6[10]設(shè)Mf=(S,Act,P,I,AP,L)為一有窮FDP,定義函數(shù)Adv:S→2Act是Mf的調(diào)度。對任意s∈S,有Adv(s)?Act(s)。

定義7設(shè)Mf=(S,Act,P,I,AP,L)為有窮FDP,Adv是Mf上定義的調(diào)度。定義映射FPoAdv:PathsAdv(Mf)→[0,1]如下:

其中,π=s0α0s1α1s2…∈PathsAdv(Mf)。

對E?PathsAdv(M),定義FPoAdv(E)=∨{FPoAdv(π)|π∈E}可以得到FPoAdv:2PathsAdv(Mf)→[0,1]是Ω=2PathsAdv(Mf)上的模糊測度[22]。

在有窮FDPMf=(S,Act,P,I,AP,L)上定義rAdv:S→[0,1],其中Adv表示調(diào)度,本文考慮最大調(diào)度rmax(s)和最小調(diào)度rmin(s),定義分別如下所示:

4 模糊分支時態(tài)邏輯

FCTL*是CTL*的擴展,FCTL*由狀態(tài)公式和路徑公式構(gòu)成。下面給出FCTL*的語法及語義。

定義8(FCTL*語法) 原子命題集AP上FCTL*狀態(tài)公式的正范式遞歸定義為:

Φ::=true|false|r|a|

其中,r∈[0,1],a∈AP,φ為FCTL*的路徑公式。

FCTL*路徑公式的正范式遞歸定義為:

φ::=true|false|r|a|

定義9(FCTL*狀態(tài)公式語義) 設(shè)Mf=(S,Act,P,I,AP,L)是FDP,其中a∈AP,s∈S,Φ1、Φ2是FCTL*狀態(tài)公式,φ是FCTL*路徑公式,Adv為Mf上定義的調(diào)度,r∈[0,1],對于狀態(tài)公式Φ,其在Mf上的語義是‖Φ‖:S→[0,1],歸納定義如下:對于任意的s∈S,

‖true‖(s)=1

(1)

‖false‖(s)=0

(2)

‖r‖(s)=r

(3)

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

(4)

‖a‖(s)=1-L(s,a)

(5)

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

(6)

(7)

定義10(FCTL*路徑公式語義) 設(shè)Mf=(S,Act,P,I,AP,L)是FDP,其中a∈AP,Adv是Mf上定義的調(diào)度,π=s0α0s1α1s2…∈PathsAdv(Mf),i≥0,s=s0,π[i]=si,πi=siαisi+1…,對于路徑公式φ在Mf上語義是‖φ‖:PathsAdv(Mf)→[0,1],歸納定義如下:

‖true‖(π)=1

(8)

‖false‖(π)=0

(9)

‖r‖(π)=r

(10)

‖a‖(π)=‖a‖(π0)=L(s,a)

(11)

‖a‖(π)=‖a‖(π0)=1-L(s,a)

(12)

‖φ1∧φ2‖(π)=‖φ1‖(π)∧‖φ2‖(π)

(13)

‖○φ‖(π)=‖φ‖(π1)

(14)

‖φ1∪φ2‖(π)=

(15)

5 模糊分支時態(tài)邏輯模型檢測算法

FCTL*模型檢測問題是給定有窮FDPMf及FCTL*狀態(tài)公式Φ,計算Mf中狀態(tài)s滿足Φ的可能性‖Φ‖(s)。FCTL*模型檢測過程是由葉子節(jié)點向根節(jié)點遍歷FCTL*狀態(tài)公式Φ的語法樹,其與FCTL模型檢測算法原理相似。首先找到Φ狀態(tài)極大真子式ψ[1],然后計算Mf中s滿足ψ的可能性‖ψ‖(s),最后計算‖Φ‖(s)。

FCTL*模型檢測過程中,用新原子命題集AP′={a1,a2,…}代替公式Φ中的狀態(tài)極大真子式ψ[1]且新原子命題不會在公式Φ中出現(xiàn)。

對狀態(tài)公式ψ=true,ψ=false,ψ=r,ψ=a,ψ=a,ψ=Φ1∧Φ2。‖ψ‖(s)由式(1)～式(6)可得。

當(dāng)ψ=FPoAdv(φ)時,對一個FDP結(jié)構(gòu),只需要計算Mf中s滿足FCTL*的正規(guī)范型公式FPo(φ)的可能性‖F(xiàn)Po(φ)‖的計算公式。

(1)φ=true。

‖true‖(π))=rmax(s)

(16)

‖true‖(π))=rmin(s)

(17)

(2)φ=false。

(18)

(3)φ=r。

(19)

(20)

(4)φ=a。

L(s,a))=L(s,a)∧rmax(s)

(21)

L(s,a))=L(s,a)∧rmin(s)

(22)

(5)φ=a。

‖

(1-L(s,a)))=(1-L(s,a))∧rmax(s)

(23)

‖

(1-L(s,a)))=(1-L(s,a))∧rmin(s)

(24)

(6)φ=φ1∧φ2。

‖φ2‖(π))=‖F(xiàn)Pomax(φ1)‖(s)∧

‖F(xiàn)Pomax(φ2)‖(s)

(25)

‖φ2‖(π))=‖F(xiàn)Pomin(φ1)‖(s)∧

‖F(xiàn)Pomin(φ2)‖(s)

(26)

(7)φ=○φ。

(Pmax°‖F(xiàn)Pomax(φ)‖)(s)

(27)

(Pmin°‖F(xiàn)Pomin(φ)‖)(s)

(28)

(8)φ=φ1∪φ2。

Pmax(sj-2,sj-1)∧FPomax(πj-1)∧

‖φ1‖(πj-1)∧Pmax(sj-1,sj)∧FPomax(πj)∧

‖F(xiàn)Pomax(φ2)‖)(s)=

((Dφ1°Pmax)*°‖F(xiàn)Pomax(φ2)‖)(s)

(29)

其中,Dφ1=(FPomax(φ1)(s))s∈S。

Pmin(sj-2,sj-1)∧FPomin(πj-1)∧

‖φ1‖(πj-1)∧Pmin(sj-1,sj)∧FPomin(πj)∧

‖F(xiàn)Pomin(φ2)‖)(s)=

((Dφ1°Pmin)*°‖F(xiàn)Pomin(φ2)‖)(s)

(30)

其中,Dφ1=(FPomin(φ1)(s))s∈S。

下面根據(jù)式(1)～式(30)給出基于FDP的FCTL*模型檢測算法,為表達方便使用Adv表示最大可能性調(diào)度或最小可能性調(diào)度。算法中Sub(Φ)是Φ的子式的集合,|Φ|是Φ的極大真子式個數(shù)。

算法1 FCTL*模型檢測算法輸入:FDP Mf和FCTL*狀態(tài)公式Φ。輸出:對于Mf中任意狀態(tài)s和調(diào)度Adv的‖Φ‖(s)。Procedure FCTL*Check(Mf,Φ)Step 1 for all i≤|Φ| doStep 2 for all ψ∈Sub(Φ) with |ψ|=i doStep 3 case ψ true:return(1)s∈S; false:return(0)s∈S; r:return(r)s∈S; a:return(L(s,a))s∈S; a:return(1-L(s,a))s∈S; Φ1∧Φ2 :return (FCTL*Check(Mf,Φ1)∧FCTL*Check(Mf,Φ2))s∈S; FPo(φ): case φ true:return(rAdv(s))s∈S; false:return(0)s∈S; r:return(r∧rAdv(s))s∈S; a:return(L(s,a)∧rAdv(s))s∈S; a:return((1-L(s,a))∧rAdv(s))s∈S; φ1∧φ2:return (FCTL*Check(Mf,FPoAdv(φ1)))s∈S∧ (FCTL*Check(Mf,FPoAdv(φ2)))s∈S; ○φ:return (PAdvFCTL*Check(Mf,FPoAdv(φ)))s∈S; φ1∪φ2:return (((FCTL*Check(Mf,FPoAdv(φ1)))PAdv)s∈S)*(FCTL*Check(Mf,FPoAdv(φ2)))s∈S Endcase;Endcase;Step 4 AP=AP∪{aψ};Step 5 replace ψ with aψ;Step 6 for all ‖ψ‖(s)>0 do L(s)={}∪{};End for End for End forStep 7 return(‖‖(s))s∈S;End Procedure

本文給出的FCTL*模型檢測算法是基于模糊矩陣運算的,下面對上述算法進行復(fù)雜度分析。在FCTL*模型檢測算法中當(dāng)ψ=ture,ψ=false,ψ=r,ψ=a,ψ=a,ψ=Φ1∧Φ2時,其復(fù)雜度與FDPMf大小和ψ的長度有關(guān)。當(dāng)ψ=FPo(φ)時,且在φ=true,φ=false,φ=r,φ=a,φ=a,φ=φ1∧φ2時,復(fù)雜度同樣與FDPMf大小和公式φ的長度有關(guān);當(dāng)φ=○φ時的復(fù)雜度與矩陣相乘有關(guān),所以復(fù)雜度為多項式時間內(nèi)的;φ=φ1∪φ2時的復(fù)雜度和克林閉包的計算有關(guān),采用文獻[23]的計算方式進行計算,可知復(fù)雜度為O(w2logw),w=|S|,其中|S|表示狀態(tài)個數(shù)。

綜上,本文提出的FCTL*模型檢測算法的時間復(fù)雜度主要取決于算法中φ=φ1∪φ2的復(fù)雜度。給定一有窮FDPMf及FCTL*狀態(tài)公式Φ,其模型檢測算法的復(fù)雜度為O(size(Mf)·poly(S)·|Φ|),其中,size(Mf)表示模型的大小,poly(S)表示|S|的多項式函數(shù),|Φ|表示FCTL*狀態(tài)公式的長度。

6 實例說明

醫(yī)療專家系統(tǒng)是一種通過收集和分析大量醫(yī)學(xué)數(shù)據(jù)協(xié)助醫(yī)護人員進行診斷并給出治療建議的計算機系統(tǒng)。本文采用文獻[10,19]中的醫(yī)療專家治療系統(tǒng)對FCTL*模型檢測算法進行說明。圖1是一醫(yī)療專家系統(tǒng),其中有3位專家,每位專家給出不同的治療方案,分別使用α,β,γ表示,圖中圓圈表示該病人的身體狀態(tài),使用S0、S1、S2表示;狀態(tài)中字母表示病人的身體狀況:B(差),G(一般),F(好)。

Figure 1 Medical expert system

多專家組成的專家系統(tǒng)較為復(fù)雜,但是可以避免某位專家全程治療導(dǎo)致的主觀性。本文使用FDPMf=(S,Act,P,I,AP,L)對病人的治療過程進行建模,其中,S={S0,S1,S2},Act={α,β,γ},為了對病人的狀態(tài)進行標(biāo)記,設(shè)AP={B,G,F}。對于病人的3種身體狀況,不同專家對此有不同的看法,因此,本文賦予一個模糊值來表示身體狀況的健康程度。例如,L(S1,F)=0.7表示在狀態(tài)S1上身體狀況為“好”的程度是0.7;用P(S1,α,S2)=0.8表示醫(yī)生采用α治療方案對病人進行治療后,病人的身體狀態(tài)從狀態(tài)S1到S2的可能性是0.8。

根據(jù)圖1醫(yī)療專家系統(tǒng)模型,得出治療方案α、β、γ對應(yīng)的模糊轉(zhuǎn)移矩陣Pα、Pβ、Pγ。B、G、F在狀態(tài)S0、S1、S2對應(yīng)的真值矩陣為PB、PG、PF。

專家結(jié)合3種方案對病人進行持續(xù)7天的治療后,計算病人的身體狀況最終為好(F)且一直保持好(F)的可能性,本文使用公式φ=◇≤7F∧◇□F描述這一性質(zhì)[19]。下面根據(jù)FCTL*模型檢測算法給出該公式的求解過程:

FPoAdv(◇≤7F∧◇□F)(s)=

FPoAdv(◇≤7F)(s)∧FPoAdv(◇□F)(s)=

當(dāng)調(diào)度為最大調(diào)度時:

DF=diag(L(s,F)∧rmax(s))=

DF°Pmax=

由此可得:

FPomax(◇≤7F∧◇□F)(s)=

同理可得當(dāng)調(diào)度為最小調(diào)度時:

由上述計算可知,經(jīng)過7天治療后病人身體狀況為好(F)且一直保持為好(F)的在狀態(tài)S0、S1和S2處最大可能性分別為0.8,0.9和0.9;最小可能性分別為0.2,0.5和0.7。

計算病人身體初始狀況為差(B),專家結(jié)合3種方案經(jīng)過7天治療后,病人的身體狀況最終為好(F)并且最終一直保持身體狀況為好(F)的可能性,本文使用公式Φ=B∧FPo(◇≤7F∧◇□F)來描述這一性質(zhì)。根據(jù)FCTL*模型檢測算法,下面給出該公式的最大可能性和最小可能性求解過程:Φ狀態(tài)極大真子式為ψ1=B,ψ2=FPo(◇≤7F∧◇□F),對應(yīng)的新原子命題集為AP′=AP∪{a1,a2}={B,G,F,a1,a2},公式ψ1=B的最大可能性及最小可能性根據(jù)FCTL*模型檢測算法可得:

公式ψ2=FPo(◇≤7F∧◇□F)的最大可能性及最小可能性在前文已得到:

當(dāng)調(diào)度為最大調(diào)度時:

L(S0)={0.85/B,0.3/G,0.2/F,0.85/a1,0.8/a2},

L(S1)={0.4/B,0.95/G,0.7/F,0.4/a1,0.9/a2},

L(s2)={0.1/B,1/G,0.9/F,0.1/a1,0.9/a2}

當(dāng)調(diào)度為最小調(diào)度時:

L(S0)={0.85/B,0.3/G,0.2/F,0.85/a1,0.2/a2},

L(S1)={0.4/B,0.95/G,0.7/F,0.4/a1,0.5/a2},

L(S2)={0.1/B,1/G,0.9/F,0.1/a1,0.7/a2}

綜上可得:

‖Φ‖max(s)=‖ψ1∧ψ2‖max(s)=

‖ψ1‖max(s)∧‖ψ2‖max(s)=

‖Φ‖min(s)=‖ψ1∧ψ2‖min(s)=

‖ψ1‖min(s)∧‖ψ2‖min(s)=

由上述計算可知,當(dāng)病人身體狀況為差(B)時,專家結(jié)合3種方案經(jīng)過7天治療后,病人身體狀況變好(F)且一直保持好(F)在狀態(tài)S0、S1和S2處最大可能性分別為0.8,0.4和0.1,最小可能性分別為0.2,0.4和0.1。

7 結(jié)束語

針對FCTL*模型檢測問題,本文在FDP的基礎(chǔ)上結(jié)合模糊測度理論給出了FCTL*的語法和語義;設(shè)計了FCTL*的模型檢測算法,該算法將模型檢測問題轉(zhuǎn)化成模糊矩陣的合成運算,并進行復(fù)雜度分析;最后通過醫(yī)療專家系統(tǒng)的實例對算法進行了說明。