基于模糊測(cè)度的模糊分支時(shí)態(tài)邏輯模型檢測(cè)*

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

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

1 引言

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

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

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

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

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

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

定義1[20,21]設(shè)X是經(jīng)典集合,X上的模糊集合A是X到[0,1]的一個(gè)映射,也被稱為模糊集合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的交、并、補(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的交、并、補(bǔ)定義如下:

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。

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

3 模糊決策過(guò)程

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

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

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

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

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

(4)I:S→[0,1]為初始分布函數(shù),對(duì)于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。

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

定義6[10]設(shè)Mf=(S,Act,P,I,AP,L)為一有窮FDP,定義函數(shù)Adv:S→2Act是Mf的調(diào)度。對(duì)任意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)。

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

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

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

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

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

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

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

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

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

定義9(FCTL*狀態(tài)公式語(yǔ)義) 設(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],對(duì)于狀態(tài)公式Φ,其在Mf上的語(yǔ)義是‖Φ‖:S→[0,1],歸納定義如下:對(duì)于任意的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*路徑公式語(yǔ)義) 設(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…,對(duì)于路徑公式φ在Mf上語(yǔ)義是‖φ‖: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 模糊分支時(shí)態(tài)邏輯模型檢測(cè)算法

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

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

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

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

(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*模型檢測(cè)算法,為表達(dá)方便使用Adv表示最大可能性調(diào)度或最小可能性調(diào)度。算法中Sub(Φ)是Φ的子式的集合,|Φ|是Φ的極大真子式個(gè)數(shù)。

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

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

6 實(shí)例說(shuō)明

醫(yī)療專家系統(tǒng)是一種通過(guò)收集和分析大量醫(yī)學(xué)數(shù)據(jù)協(xié)助醫(yī)護(hù)人員進(jìn)行診斷并給出治療建議的計(jì)算機(jī)系統(tǒng)。本文采用文獻(xiàn)[10,19]中的醫(yī)療專家治療系統(tǒng)對(duì)FCTL*模型檢測(cè)算法進(jìn)行說(shuō)明。圖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)對(duì)病人的治療過(guò)程進(jìn)行建模,其中,S={S0,S1,S2},Act={α,β,γ},為了對(duì)病人的狀態(tài)進(jìn)行標(biāo)記,設(shè)AP={B,G,F}。對(duì)于病人的3種身體狀況,不同專家對(duì)此有不同的看法,因此,本文賦予一個(gè)模糊值來(lái)表示身體狀況的健康程度。例如,L(S1,F)=0.7表示在狀態(tài)S1上身體狀況為“好”的程度是0.7;用P(S1,α,S2)=0.8表示醫(yī)生采用α治療方案對(duì)病人進(jìn)行治療后,病人的身體狀態(tài)從狀態(tài)S1到S2的可能性是0.8。

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

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

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

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

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

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

DF°Pmax=

由此可得:

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

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

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

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

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

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

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)度時(shí):

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)=

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

7 結(jié)束語(yǔ)

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