基于模糊決策過程的模糊計(jì)算樹邏輯模型檢測*

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

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

1 引言

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

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

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

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

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

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

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

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

定義2[22]設(shè)A,B∈F(X)，A與B的并(A∪B)、交(A∩B)、補(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]設(shè)X=(xij)m×n,Y=(yij)m×n為m行n列的模糊矩陣，如果對(duì)于任意i,j，都有xij=yij，則稱模糊矩陣X和Y相等，記為X=Y。如果對(duì)于任意i,j，都有xij≤yij，則稱模糊矩陣X包含于模糊矩陣Y，記為X?Y。

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

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

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

Xc=(1-xij)m×n。

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

X°Y=(zij)m×l

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

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

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

本文將模糊決策過程轉(zhuǎn)化為模糊Kripke結(jié)構(gòu)，從而可以使用模糊Kripke結(jié)構(gòu)已有的成果來研究模糊決策過程，在這里給出模糊Kripke結(jié)構(gòu)的定義。

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

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

(2)P:S×S→[0,1]是模糊轉(zhuǎn)移函數(shù)，對(duì)于任意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]是模糊標(biāo)簽函數(shù)，L(s,p)表示原子命題p在狀態(tài)s上的可能性真值。

3 模糊決策過程

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

4 模糊計(jì)算樹邏輯

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

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

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

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

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

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

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

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

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

同時(shí)根據(jù)上述幾個(gè)公式，可以推導(dǎo)出下列幾個(gè)常用邏輯公式：

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

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

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

‖true‖(s)=1

(1)

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

(2)

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

(3)

(4)

(5)

(6)

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

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

(7)

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

(8)

5 模糊計(jì)算樹邏輯模型檢測

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

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

‖?max○Φ‖(s)=

(Pαmax°PΦ)(s)

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

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

(9)

‖?min○Φ‖(s)=

(Pαmin°PΦ)(s)

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

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

(10)

‖?max○Φ‖(s)=

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

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

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

(11)

‖?min○Φ‖(s)=

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

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

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

(12)

由以上推導(dǎo)，得出定理1。

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

‖?○Φ‖=PAdv°PΦ

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

對(duì)于路徑公式φ=○Φ，將其代入狀態(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進(jìn)行計(jì)算。

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

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

‖?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‖的矩陣計(jì)算形式如式(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‖的矩陣計(jì)算形式如式(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‖的計(jì)算公式如式(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‖的計(jì)算公式如式(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)

由以上推導(dǎo)，得出定理2。

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

‖?Φ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

對(duì)于路徑公式φ=Φ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進(jìn)行計(jì)算。

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

‖?maxB∪E‖(s0)=0.5說明在狀態(tài)s0，病人的健康狀態(tài)為“差”，醫(yī)生使用3種治療方案經(jīng)過多次治療，取得最好治療效果時(shí)，病人的健康狀態(tài)變?yōu)椤昂谩钡目赡苄宰畲鬄?.5。‖?minB∪E‖(s0)=0.3說明在狀態(tài)s0，病人的健康狀態(tài)為“差”，醫(yī)生使用3種治療方案經(jīng)過多次治療，取得最好治療效果時(shí)，病人的健康狀態(tài)變?yōu)椤昂谩钡目赡苄宰钚?.3。‖?maxB∪E‖(s0)=0.2說明在狀態(tài)s0，病人的健康狀態(tài)為“差”，醫(yī)生使用3種治療方案經(jīng)過多次治療，取得最差治療效果時(shí)，病人的健康狀態(tài)變?yōu)椤昂谩钡目赡苄宰畲鬄?.2。‖?minB∪E‖(s0)=0.2說明在狀態(tài)s0，病人的健康狀態(tài)為“差”，醫(yī)生使用3種治療方案經(jīng)過多次治療，取得最差治療效果時(shí)，病人的健康狀態(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模型檢測算法是基于模糊矩陣運(yùn)算的，相比于文獻(xiàn)[18]中的不動(dòng)點(diǎn)方法，具有簡單明了、可讀性較強(qiáng)、效率高等優(yōu)勢，下面對(duì)本文所提出的算法進(jìn)行復(fù)雜度分析。

在所有調(diào)度Adv下，可以在|Φ|步遞歸計(jì)算出‖Φ‖(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,Φ=Φ計(jì)算‖Φ‖(s)的時(shí)間復(fù)雜度只與FDPMf的大小和公式Φ的長度有關(guān)，而計(jì)算公式Φ=?φ,Φ=?φ的時(shí)間取決于計(jì)算模糊矩陣PAdv的轉(zhuǎn)移閉包的時(shí)間。本文采用文獻(xiàn)[23]的算法來計(jì)算其時(shí)間復(fù)雜度為O(w2logw)，其中w=|S|。綜上所述，本文通過定理3給定FCTL模型檢測算法的時(shí)間復(fù)雜度。

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

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

6 結(jié)束語

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