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

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

1 引言

模型檢測(Model Checking)[1]是一種自動的形式化驗證方法，主要由3部分組成，一是對待檢測的系統(tǒng)進行建模，二是使用時序邏輯語言對屬性進行形式化描述，三是使用模型檢測算法驗證系統(tǒng)模型是否滿足屬性。經(jīng)典的模型檢測[2]強調(diào)的是系統(tǒng)行為的絕對正確性，如果滿足屬性，則返回滿足，如果不滿足屬性，則返回一個反例。經(jīng)典模型檢測是一種定性的驗證方式。

目前，越來越多的復雜計算機系統(tǒng)具有隨機性、不確定性和不一致性等特征，為了處理復雜系統(tǒng)的驗證問題，定量模型檢測受到了學術界和工業(yè)界的關注。概率模型檢測[3]主要處理由隨機過程產(chǎn)生的不確定性系統(tǒng)的模型檢測問題，其目標是：針對定量概率規(guī)范，確定概率系統(tǒng)的準確性。多值模型檢測[4]主要處理包含不完全或者不一致信息的系統(tǒng)的模型檢測問題。模糊模型檢測主要處理包含數(shù)據(jù)表述不確定性的系統(tǒng)的模型檢測問題，其更關注于系統(tǒng)在屬性上的真值。

模糊模型檢測是在模糊集合理論基礎上提出的模型檢測方法。Li等[5,6]等結合可能性測度和模糊理論提出的可能性模型檢測[5,7 - 10]和廣義可能性模型檢測[6,11 - 15]，在計算過程中，到達狀態(tài)之后的路徑的柱集的可能性也參與了計算，而這些計算在大部分系統(tǒng)中是可以被忽略的。Pan等[16,17]利用模糊Kripke結構建模，模糊計算樹邏輯描述屬性，來進行模糊模型檢測研究。范艷煥等[18]利用不確定型模糊Kripke結構建模，模糊計算樹邏輯描述屬性，通過不動點的方法研究模糊模型檢測算法。文獻[19]使用模糊模型檢測替代小區(qū)間映射技術對模糊控制系統(tǒng)的行為正確性進行統(tǒng)計評估。文獻[20]使用模糊模型檢測對模糊轉換系統(tǒng)進行穩(wěn)態(tài)分析。

相對于迭代運算而言，矩陣運算具有簡單明了、可讀性較強和高效等優(yōu)勢[6]，故本文參考文獻[18]中的不確定型模糊Kripke結構，引入模糊決策過程FDP(Fuzzy Decision Processes)對復雜非確定性模糊系統(tǒng)建模，使用模糊計算樹邏輯描述待驗證系統(tǒng)的屬性，將基于模糊決策過程的模糊模型檢測問題轉換為矩陣的合成運算，并給出了相應的算法，同時也對算法的復雜性進行了分析。

2 預備知識

本節(jié)將介紹模糊集合、模糊集合運算和模糊矩陣運算和閉包等預備知識。詳細內(nèi)容可參考文獻[21,22]。

定義1[22]設X為普通集合，集合X上的模糊集合(Fuzzy Set)是一個映射A:X→[0,1],也稱為模糊集合A的隸屬度函數(shù)，對x∈X，A(x) 稱為x屬于模糊集A的隸屬度。

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

定義2[22]設A,B∈F(X)，A與B的并(A∪B)、交(A∩B)、補(Ac)的隸屬度函數(shù)分別定義為：

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

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

Ac(x)=1-A(x)。

定義3[22]設X=(xij)m×n,Y=(yij)m×n為m行n列的模糊矩陣，如果對于任意i,j，都有xij=yij，則稱模糊矩陣X和Y相等，記為X=Y。如果對于任意i,j，都有xij≤yij，則稱模糊矩陣X包含于模糊矩陣Y，記為X?Y。

模糊矩陣X和Y的并、交和補定義為：

X∪Y=(xij∨yij)m×n;

X∩Y=(xij∧yij)m×n;

Xc=(1-xij)m×n。

定義4[22]設X=(xij)m×n為m行n列的模糊矩陣，Y=(yij)n×l為n行l(wèi)列的模糊矩陣，則模糊矩陣X和Y的內(nèi)積定義為：

X°Y=(zij)m×l

對于模糊矩陣X,Y和Z，內(nèi)積運算具有如下運算律：

結合律:(X°Y)°Z=X°(Y°Z)；

分配律:(X∪Y)°Z=(X°Z)∪(Y°Z)。

本文將模糊決策過程轉化為模糊Kripke結構，從而可以使用模糊Kripke結構已有的成果來研究模糊決策過程，在這里給出模糊Kripke結構的定義。

定義5[16]模糊Kripke結構FKS(Fuzzy Kripke Structure)是一個五元組K=(S,P,I,AP,L)，其中

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

(2)P:S×S→[0,1]是模糊轉移函數(shù)，對于任意s∈S，存在狀態(tài)t∈S，使P(s,t)>0；

(3)I:S→[0,1]是模糊初始分布函數(shù)，I(s)表示初態(tài)是狀態(tài)s的可能性真值；

(4)AP是原子命題集合；

(5)L:S×AP→[0,1]是模糊標簽函數(shù)，L(s,p)表示原子命題p在狀態(tài)s上的可能性真值。

3 模糊決策過程

Figure 1 Medical expert system(3 experts)圖1 醫(yī)療專家系統(tǒng)(3專家)

多專家組成的專家系統(tǒng)雖然較為復雜，但是可以避免單純由某一個專家進行全程治療這一情況所帶來的主觀性和片面性。為了描述這種復雜的系統(tǒng)，本文參考文獻[18]的不確定型模糊Kripke結構，引入模糊決策過程模型，對此類復雜模糊系統(tǒng)建模，研究相應的模型檢測問題。

定義6模糊決策過程FDP是一個六元組Mf=(S,Act,P,I,AP,L)，其中:

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

(2)Act是動作集；

(3)P:S×Act×S→[0,1]是模糊轉移函數(shù)，對于任意s∈S，α∈Act，存在狀態(tài)t∈S，使P(s,α,t)>0；

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

(5)AP是原子命題集合;

(6)L:S×AP→[0,1]是模糊標簽函數(shù),對于任意s∈S，a∈AP，L(s,a)表示原子命題a在狀態(tài)s上的可能性真值。

若狀態(tài)集S、動作集Act和原子命題集AP均有窮，則稱Mf為有窮FDP。若存在一狀態(tài)t∈S，使得P(s,α,t)>0，則稱α在狀態(tài)s上是可激活的，Act(s)表示狀態(tài)s所有可激活的動作集合。

為了解決FDP中動作的不確定性問題，本文引入調(diào)度的概念，通過調(diào)度可以將FDP轉換為FKS。

定義7給定一個有窮FDPMf=(S,Act,P,I,AP,L)，定義函數(shù)Adv:S→Act為Mf的調(diào)度。對于任意s∈S，有Adv(s)∈Act(s)。

利用調(diào)度Adv可以誘導出FKS。在調(diào)度Adv下，F(xiàn)KS可以描述FDP的行為動作，即FKS中的路徑是FDP中對應的Adv路徑。FDP中的轉移P(s,α,t)轉換為：Adv誘導出的FKS中的PAdv(s,t)。

例2對于圖1所示FDP模型，當調(diào)度函數(shù)為Adv(s0)=α，Adv(s1)=β,Adv(s2)=γ時，模型轉變?yōu)閳D2所示模型，該模型實際上是一個FKS。

Figure 2 FDP for determining scheduling圖2 確定調(diào)度的FDP

例3圖1d的FDP中，動作α下的狀態(tài)轉移可能性矩陣Pα、動作β下的狀態(tài)轉移可能性矩陣Pβ、動作γ下的狀態(tài)轉移可能性矩陣Pγ、最大可能性轉移矩陣Pαmax、最小可能性轉移矩陣Pαmin分別如下所示：

最大可能性轉移矩陣Pαmax和最小可能性轉移矩陣Pαmin下，圖1d所示的FDP模型轉換為如圖3所示的FKS。

Figure 3 FDP with the maximum and minimum possibility transfer matrices圖3 轉移矩陣為最大、最小可能性轉移矩陣的FDP

4 模糊計算樹邏輯

本文使用模糊計算樹邏輯FCTL(Fuzzy Computation Tree Logic)來描述有窮的FDP的性質(zhì)。FCTL由狀態(tài)公式和路徑公式構成，下面給出FCTL的語法和在FDP上的語義解釋。

定義8(FCTL語法) FCTL狀態(tài)公式遞歸定義如下所示：

Φ::=true|a|Φ1∧Φ2|Φ|?φ|?φ,其中φ是路徑公式，a∈AP。

FCTL路徑公式：φ::=○Φ|Φ1∪Φ2,其中Φ、Φ1和Φ2是狀態(tài)公式。

在給出這些公式的語義之前，先給出上述公式的直觀含義。

?φ表示 “存在一條路徑滿足φ”。

?φ表示 “所有路徑都滿足φ”。

○Φ表示 “在路徑上，第2個狀態(tài)滿足Φ”。

Φ1∪Φ2表示 “在路徑上，有一些狀態(tài)滿足Φ2，同時在這些狀態(tài)之前的所有狀態(tài)都滿足Φ1”。

同時根據(jù)上述幾個公式，可以推導出下列幾個常用邏輯公式：

◇Φ=true∪Φ,表示 “在路徑上，最終會有狀態(tài)滿足Φ”。

□Φ=(true∪Φ),表示“在路徑上，所有狀態(tài)一直滿足Φ”。

定義9(FCTL語義) 設Mf=(S,Act,P,I,AP,L)是一個有窮FDP，‖Φ‖:S→[0,1]是S的模糊子集，對于FCTL狀態(tài)公式Φ的語義遞歸定義如下所示：

‖true‖(s)=1

(1)

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

(2)

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

(3)

(4)

(5)

(6)

給定一個FDPMf，調(diào)度Adv，對任意π∈PathsAdv(s)，路徑公式φ的語義是： ‖φ‖:PathsAdv(Mf)→[0,1]表示在調(diào)度Adv的作用下，路徑π滿足公式φ的可能性，其語義遞歸定義如下所示：

‖○Φ‖(π)=PAdv(s0,s1)∧‖Φ‖(s1)

(7)

‖Φ1‖(sk)∧PAdv(sj-1,sj)∧‖Φ2‖(sj))

(8)

5 模糊計算樹邏輯模型檢測

模糊計算樹邏輯模型檢測問題描述為：給定一個FDPMf，Mf中的狀態(tài)s和FCTL狀態(tài)公式Φ，計算‖Φ‖(s)的值。對于狀態(tài)公式Φ=a，Φ=Φ1∧Φ2和Φ=Φ，‖Φ‖(s)可分別由式(2)～式(4)得出。對于Φ=?φ和Φ=?φ，一般要計算狀態(tài)s滿足狀態(tài)公式Φ的最大可能性和最小可能性，理論上必須計算出所有調(diào)度下‖Φ‖(s)的值，然后再計算出狀態(tài)s滿足公式Φ的最大可能性和最小可能性。在本節(jié)FCTL模型檢測算法中，將其轉換為模糊矩陣相乘。用‖Φ‖max(s)和‖Φ‖min(s)分別表示狀態(tài)s滿足公式Φ的最大可能性和最小可能性。通過調(diào)度，本文將FDP中求最大可能性和最小可能性的模型檢測問題，轉換為求最大可能性轉移矩陣和最小可能性轉移矩陣構成的相應FKS上的模型檢測問題，解決了FDP中動作的不確定性問題。下面分別給出路徑公式φ=○Φ和φ=Φ1∪Φ2分別對應的‖Φ‖max(s)和‖Φ‖min(s)計算方法。

(1)對于φ=○Φ，最大值‖Φ‖max(s)和最小值‖Φ‖min(s)的計算過程分別如下所示：

‖?max○Φ‖(s)=

(Pαmax°PΦ)(s)

對于狀態(tài)公式Φ，PΦ表示|S|×1的模糊矩陣，對于任意s,PΦ(s)=‖Φ‖(s)，從而得到‖?max○Φ‖的矩陣計算形式如式(9)所示:

‖?max○Φ‖=Pαmax°PΦ

(9)

‖?min○Φ‖(s)=

(Pαmin°PΦ)(s)

從而得到‖?min○Φ‖的矩陣計算形式如式(10)所示:

‖?min○Φ‖=Pαmin°PΦ

(10)

‖?max○Φ‖(s)=

((Pαmax°DΦ)c°E)c(s)

對于狀態(tài)公式Φ，DΦ表示|S|×|S|的對角模糊矩陣，對于任意s,t，當s=t時DΦ(s,t)=‖Φ‖(s)，否則DΦ(s,t)=0。E是一個全1的|S|×1的模糊矩陣，從而得到‖?max○Φ‖的矩陣計算形式如式(11)所示:

‖?max○Φ‖=((Pαmax°DΦ)c°E)c

(11)

‖?min○Φ‖(s)=

((Pαmin°DΦ)c°E)c(s)

從而得到‖?min○Φ‖的矩陣計算形式如式(12)所示:

‖?min○Φ‖=((Pαmin°DΦ)c°E)c

(12)

由以上推導，得出定理1。

定理1給定一個FDPMf，Mf中的狀態(tài)s和FCTL狀態(tài)公式Φ，當Adv為max或min時:

‖?○Φ‖=PAdv°PΦ

‖?○Φ‖=((PAdv°DΦ)c°E)c

對于路徑公式φ=○Φ，將其代入狀態(tài)公式Φ=?φ，得‖Φ‖max(s)=‖?φ‖max(s)=‖?max○Φ‖(s),‖Φmin(s)‖=‖?φ‖min(s)=‖?min○Φ‖(s);將其代入狀態(tài)公式Φ=?φ，得‖Φ‖max(s)=‖?φ‖max(s)=‖?max○Φ‖(s),‖Φ‖min(s)=‖?φ‖min(s)=‖?min○Φ‖(s)，即可按定理1進行計算。

例4對于圖1所示模型，根據(jù)式(9)～式(12)可計算出滿足公式Φ的真值，部分結果及說明如下： ‖?max○E‖(s0)=0.5說明在狀態(tài)s0，醫(yī)生使用3種治療方案治療1次，取得最好治療效果時，病人身體情況變?yōu)椤昂谩钡目赡苄宰畲鬄?.5。‖?min○E‖(s0)=0.3說明在狀態(tài)s0，醫(yī)生使用3種治療方案治療1次，取得最好治療效果時，病人身體情況變?yōu)椤昂谩钡目赡苄宰钚?.3。‖?max○N‖(s0)=0.3說明在狀態(tài)s0，醫(yī)生使用3種治療方案治療1次，取得最差治療效果時，病人身體情況變?yōu)椤罢！钡目赡苄宰畲鬄?.3?！?min○N‖(s0)=0.1說明在狀態(tài)s0，醫(yī)生使用3種治療方案治療1次，取得最差治療效果時，病人身體情況變?yōu)椤罢！钡目赡苄宰钚?.1。

(2)對于φ=Φ1∪Φ2，最大值‖Φ‖max(s)和最小值‖Φ‖min(s)的計算過程分別如下所示：

‖?maxΦ1∪Φ2‖(s)=

Pmax(tj-1,tj)∧‖Φ2‖(tj)))=

‖Φ2‖(tj)))=

(Pαmax(tj-1,tj)∧‖Φ2‖(tj))))=

‖Φ2‖(tj)))=

((DΦ1°Pαmax)*°PΦ2)(s)

得到‖?maxΦ1∪Φ2‖的矩陣計算形式如式(13)所示：

‖?maxΦ1∪Φ2‖=(DΦ1°Pαmax)*°PΦ2

(13)

‖?minΦ1∪Φ2‖(s)=

Pmin(tj-1,tj)∧‖Φ2‖(tj)))=

‖Φ2‖(tj))))=

(Pαmin(tj-1,tj)∧‖Φ2‖(tj))))=

‖Φ2‖(tj)))=

((DΦ1°Pαmin)*°PΦ2)(s)

得到‖?minΦ1∪Φ2‖的矩陣計算形式如式(14)所示:

‖?minΦ1∪Φ2‖=(DΦ1°Pαmin)*°PΦ2

(14)

‖?maxΦ1∪Φ2‖(s)=

Pmax(tk-1,tk)∧‖Φ1‖(tk)∧

Pmax(tj-1,tj)∧‖Φ2‖(tj)))=

(Pαmax(tm,tm+1)∧‖Φ1‖(tk))∧

(Pαmax(tk,tk+1)∧‖Φ2‖(tj))))=

(‖Φ1‖(s)∧Pαmax(tk,tk+1))∧‖Φ2‖(tj)))=

Pαmax(tk,tk+1))∧‖Φ2‖(tj)))=

‖Φ2‖(s)∨{DS-[DS-

((DΦ1°Pαmax)c°DS)c°((DS°(DΦ1°

Pαmax)c)c)*°DΦ2]°E}(s)=

‖Φ2‖(s)∨([((DΦ1°Pαmax)c°DS)c°

((DS°(DΦ1°Pαmax)c)c)*°DΦ2]c°E)c(s)=

(PΦ2∪([((DΦ1°Pαmax)c°DS)c°

((DS°(DΦ1°Pαmax)c)c)*°DΦ2]c°E)c)(s)

其中:

DS表示|S|×|S|的全1模糊矩陣。從而得到‖?maxΦ1∪Φ2‖的計算公式如式(15)所示:

‖?maxΦ1∪Φ2‖=PΦ2∪([((DΦ1°Pαmax)c°

DS)c°((DS°(DΦ1°Pαmax)c)c)*°DΦ2]c°E)c

(15)

‖?minΦ1∪Φ2‖(s)=

Pmin(tj-1,tj)∧‖Φ2‖(tj)))=

P(tj-1,αj-1,tj)∧‖Φ2‖(tj))))=

(Pαmin(tj-1,tj)∧‖Φ2‖(tj))))=

‖Φ2‖(tj)))=

‖Φ2‖(tj)))=

(PΦ2∪([((DΦ1°Pαmin)c°DS)c°((DS°

(DΦ1°Pαmin)c)c)*°DΦ2]c°E)c)(s)

得到‖?minΦ1∪Φ2‖的計算公式如式(16)所示:

‖?minΦ1∪Φ2‖=PΦ2∪([((DΦ1°Pαmin)c°

DS)c°((DS°(DΦ1°Pαmin)c)c)*°DΦ2]c°E)c

(16)

由以上推導，得出定理2。

定理2給定一個FDPMf，Mf中的狀態(tài)s和FCTL狀態(tài)公式Φ，當Adv為max或min時：

‖?Φ1∪Φ2‖=(DΦ1°PAdv)*°PΦ2

‖?Φ1∪Φ2‖=PΦ2∪([((DΦ1°PAdv)c°

DS)c°((DS°(DΦ1°PAdv)c)c)*°DΦ2]c°E)c

對于路徑公式φ=Φ1∪Φ2，將其代入狀態(tài)公式Φ=?φ，得‖Φ‖max(s)=‖?φ‖max(s)=‖?maxΦ1∪Φ2‖(s),‖Φ‖min(s)=‖?φ‖min(s)=‖?minΦ1∪Φ2‖(s);將其代入狀態(tài)公式Φ=?φ，得‖Φ‖max(s)=‖?φ‖max(s)=‖?maxΦ1∪Φ2‖(s),‖Φ‖mmin(s)=‖?φ‖min(s)=‖?minΦ1∪Φ2‖(s)，即可按定理2進行計算。

例5對于圖1所示模型，根據(jù)式(13)～式(16)可計算出滿足公式Φ的真值，部分結果及說明如下：

‖?maxB∪E‖(s0)=0.5說明在狀態(tài)s0，病人的健康狀態(tài)為“差”，醫(yī)生使用3種治療方案經(jīng)過多次治療，取得最好治療效果時，病人的健康狀態(tài)變?yōu)椤昂谩钡目赡苄宰畲鬄?.5。‖?minB∪E‖(s0)=0.3說明在狀態(tài)s0，病人的健康狀態(tài)為“差”，醫(yī)生使用3種治療方案經(jīng)過多次治療，取得最好治療效果時，病人的健康狀態(tài)變?yōu)椤昂谩钡目赡苄宰钚?.3?！?maxB∪E‖(s0)=0.2說明在狀態(tài)s0，病人的健康狀態(tài)為“差”，醫(yī)生使用3種治療方案經(jīng)過多次治療，取得最差治療效果時，病人的健康狀態(tài)變?yōu)椤昂谩钡目赡苄宰畲鬄?.2?！?minB∪E‖(s0)=0.2說明在狀態(tài)s0，病人的健康狀態(tài)為“差”，醫(yī)生使用3種治療方案經(jīng)過多次治療，取得最差治療效果時，病人的健康狀態(tài)變?yōu)椤昂谩钡目赡苄宰钚?.2。

根據(jù)式(1)～式(16)，本文給出具體的FCTL模型檢測算法。

算法1FCTL模型檢測算法

輸入:FDPMf和FCTL公式Φ。

輸出:Mf滿足公式Φ的可能性真值。

ProcedureFCTLCheck(Φ)

CaseΦ

truereturn(1)s∈S;

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

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

?○ΦreturnPAdv°PΦ;

?○Φreturn((PAdv°DΦ)c°E)c;

?Φ1∪Φ2return(DΦ1°PAdv)*°PΦ2;

?Φ1∪Φ2returnPΦ2∪([((DΦ1°PAdv)c°DS)c°((DS°(DΦ1°PAdv)c)c)*°DΦ2]c°E)c

EndCase

EndProcedure

本文所提出的FCTL模型檢測算法是基于模糊矩陣運算的，相比于文獻[18]中的不動點方法，具有簡單明了、可讀性較強、效率高等優(yōu)勢，下面對本文所提出的算法進行復雜度分析。

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

如果Φ∈AP∪{true}，則|Φ|=1；

|Φ1∧Φ2|=|Φ1|+|Φ2|+1；

|?○Φ|=|Φ|+1；

|?○Φ|=|Φ|+1；

|?Φ1∪Φ2|=|Φ1|+|Φ2|+1；

|?Φ1∪Φ2|=|Φ1|+|Φ2|+1。

在FCTL模型檢測算法中，公式Φ=true,Φ=a,Φ=Φ1∧Φ2,Φ=Φ計算‖Φ‖(s)的時間復雜度只與FDPMf的大小和公式Φ的長度有關，而計算公式Φ=?φ,Φ=?φ的時間取決于計算模糊矩陣PAdv的轉移閉包的時間。本文采用文獻[23]的算法來計算其時間復雜度為O(w2logw)，其中w=|S|。綜上所述，本文通過定理3給定FCTL模型檢測算法的時間復雜度。

定理3(FCTL模型檢測算法的時間復雜度)

給定一個有窮FDPMf和一個FCTL公式Φ，計算Mf滿足Φ的可能性的時間復雜度為O(size(Mf)·poly(S)·|Φ|)，其中size(Mf)是模型的大小，poly(S)是|S|的多項式函數(shù)，|Φ|是公式的長度。

6 結束語

為了研究模糊決策過程中的模型檢測問題，本文使用FDP對系統(tǒng)建模，使用FCTL對屬性進行描述，推導出模糊計算樹邏輯模型檢測的計算方法，并給出了相應的算法，分析了算法的時間復雜度。文中以一個醫(yī)療專家系統(tǒng)為例說明了FCTL模型檢測在實際中的應用。