模糊Kripke結(jié)構(gòu)的子模型修復(fù)算法

王 輝，石鐵柱，錢俊彥，潘海玉

(1.桂林電子科技大學(xué) 廣西可信軟件重點(diǎn)實(shí)驗(yàn)室 廣西 桂林 541004；2.南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院 江蘇 南京 210000)

0 引言

模型檢測(cè)[1]被廣泛運(yùn)用到計(jì)算機(jī)系統(tǒng)、通信協(xié)議等方面的驗(yàn)證中，成為保證計(jì)算機(jī)系統(tǒng)正確性和可靠性[2]的重要手段。隨著計(jì)算機(jī)系統(tǒng)的日益復(fù)雜和龐大，系統(tǒng)中存在的不確定信息使傳統(tǒng)的模型檢測(cè)不能對(duì)這類系統(tǒng)進(jìn)行有效的分析和驗(yàn)證。因此，人們提出了基于模糊邏輯[3-4]的模糊模型檢測(cè)、基于概率理論的概率模型檢測(cè)[5-6]等。

模型檢測(cè)的思想[7]是對(duì)模型的有窮狀態(tài)空間進(jìn)行遍歷，檢測(cè)系統(tǒng)模型是否滿足規(guī)定的性質(zhì)。如果模型不滿足所檢測(cè)的性質(zhì)，算法會(huì)生成一個(gè)反例[8]來(lái)呈現(xiàn)模型中不滿足性質(zhì)規(guī)約的部分，但無(wú)法進(jìn)行自動(dòng)修復(fù)。如果需要修復(fù)系統(tǒng)，常需要設(shè)計(jì)人員進(jìn)行手工分析和調(diào)試，導(dǎo)致效率低下，增加系統(tǒng)成本。

早在1999年，Buccafurri等就注意到模型無(wú)法自動(dòng)修復(fù)這個(gè)問(wèn)題[9]，為此提出了模型修復(fù)這個(gè)概念，并且提出一個(gè)模型修復(fù)算法，能夠自動(dòng)地通過(guò)修復(fù)模型中的結(jié)構(gòu)，使模型滿足性質(zhì)規(guī)約。文獻(xiàn)[10]首次提出了基于“可容許”模型的模型修復(fù)算法，對(duì)CTL檢驗(yàn)的模型修復(fù)問(wèn)題進(jìn)行了深入的研究。Carrillo等[11]更加完美地解決了CTL的模型修復(fù)算法，在以往的模型修復(fù)中增添了“保護(hù)”的概念，并且提出了對(duì)應(yīng)的算法。Attie等[12]提出了另外一種模型修復(fù)算法，該算法采用子模型修復(fù)，在只考慮刪除狀態(tài)和遷移關(guān)系的前提下，構(gòu)造一個(gè)布爾公式，然后用SAT求解器來(lái)進(jìn)行修復(fù)。在概率模型檢測(cè)中，模型修復(fù)問(wèn)題也得到了比較充分的研究[13-14]。

眾所周知，模糊模型檢測(cè)是系統(tǒng)量化驗(yàn)證[15-16]的一個(gè)重要研究方法，是經(jīng)典模型檢測(cè)理論[17]和模糊邏輯思想相結(jié)合而產(chǎn)生的，主要解決模糊系統(tǒng)的驗(yàn)證問(wèn)題。在模糊模型檢測(cè)中，系統(tǒng)被建模為模糊Kripke結(jié)構(gòu)[18](fuzzy Kripke structures，F(xiàn)KS)，系統(tǒng)所需要滿足的性質(zhì)規(guī)約常用模糊計(jì)算樹邏輯(fuzzy computation tree logic，F(xiàn)CTL)公式刻畫。模糊模型檢驗(yàn)已經(jīng)在模糊離散事件系統(tǒng)[19-20]等方面取得了許多研究成果。然而，模型修復(fù)問(wèn)題在模糊模型檢測(cè)中還沒(méi)有得到充分的重視。

文獻(xiàn)[12]研究了CTL模型修復(fù)中的子模型修復(fù)，通過(guò)刪去Kripke結(jié)構(gòu)中的某些狀態(tài)和遷移關(guān)系來(lái)構(gòu)造子模型，從而達(dá)到修復(fù)的目的。本文對(duì)FCTL模型修復(fù)中的子模型修復(fù)問(wèn)題進(jìn)行討論，將FKS中狀態(tài)和模糊遷移的刪去或保留規(guī)約為一個(gè)模糊命題邏輯公式，該模糊命題邏輯公式的可滿足賦值對(duì)應(yīng)著一個(gè)子模型。同時(shí)，本文給出了子模型修復(fù)算法，該算法利用模糊tableaux方法[21]求解模糊命題邏輯公式的可滿足賦值，并且分析了算法的時(shí)間復(fù)雜度，給出算法正確性的證明。本文依據(jù)模糊邏輯的特點(diǎn)，提出帶有模糊屬性的命題公式，將CTL中的子模型修復(fù)方法推廣到FCTL中。

1 子模型修復(fù)

下文出現(xiàn)的模型M、M′和Mi都是指模糊Kripke結(jié)構(gòu)，簡(jiǎn)稱為FKS。

為了便于相關(guān)討論，下面給出FCTL子公式的定義。

定義1給定FCTL公式φ，其子公式集合sub(φ)歸納定義為

sub(p)={p}，p∈AP，

sub(p)={p}，p∈AP，

sub(φ1∨φ2)={φ1∨φ2}∪sub(φ1)∪sub(φ2)，

sub(φ1∧φ2)={φ1∧φ2}∪sub(φ1)∪sub(φ2)，

sub(EXφ)={EXφ}∪sub(φ)，

sub(AXφ)={AXφ}∪sub(φ)，

sub(EGφ)={EGφ}∪sub(φ)，

sub(AGφ)={AGφ}∪sub(φ)，

sub(Eφ1Uφ2)={Eφ1Uφ2}∪sub(φ1)∪sub(φ2)，

sub(Aφ1Uφ2)={Aφ1Uφ2}∪sub(φ1)∪sub(φ2)，

FCTL公式φ的長(zhǎng)度|φ|=|sub(φ)|。

例如，由定義1得，A(p)U(q∨r)的子公式集合為{A(p)U(q∨r),p,p,q∨r,q,r}。

接下來(lái)給出子模型修復(fù)的具體定義。

定義2稱M′=(S′,S′0,R′,AP,V′)是FKS，M′是M的子模型，記為M′M，如果以下條件成立：

1)S′?S,S′0?S0；

2) 對(duì)所有s,s′∈S′,R′(s,s′)=R(s,s′)；

3) 對(duì)于所有的s∈S′,p∈AP,V′(s,p)=V(s,p)，稱M關(guān)于FCTL公式φ和閾值α∈(0,1]是子模型α-可修復(fù)的，如果存在M′M，使得φ(M′,s)≥α。

為了進(jìn)一步研究子模型之間的關(guān)系，我們給出以下定理。

定理1子模型關(guān)系()是一個(gè)偏序關(guān)系。

證明設(shè)Mi=(Si,S0,i,AP,Ri,Vi)，i=1,2,3。

本文將FKS中狀態(tài)和模糊遷移的刪去或保留規(guī)約為一個(gè)模糊命題邏輯公式repair(M,φ,α)，現(xiàn)在給出子模型修復(fù)中該公式的構(gòu)造方法。設(shè)M′=(S′,S′0,R′,AP,V′)是M的子模型，V是repair(M,φ,α)的一個(gè)賦值，用來(lái)計(jì)算修復(fù)后FSK的M′。

定義3如果滿足條件

S′={s:s∈S,V(Xs)=1}，

S′0={s0:s0∈S0,V(Xs0)=1}，

R′={R(s,t):V(Es,t)=1,V(es,t)≥α}，

V′={V(s,p):s∈S′,p∈AP}，

稱M′是repair(M,φ,α)公式在賦值V下的解，記為model(M,V)。

公式的解釋如下。

Xs:設(shè)s∈S,s∈S′當(dāng)且僅當(dāng)V(Xs)=1；

Es,t:設(shè)s∈S,t∈R(s),R′(s,t)>0當(dāng)且僅當(dāng)V(Es,t)=1；

es,t:設(shè)R(s,t)>0,R′(s,t)≥α當(dāng)且僅當(dāng)V(es,t)≥α；

下面給出公式repair(M,φ,α)的構(gòu)造方法和子模型修復(fù)算法SubModel-Repair。在子模型修復(fù)過(guò)程中，首先要保證得到的子模型在它某個(gè)初始狀態(tài)對(duì)FCTL公式是α-可滿足的。然后，給出repair(M,φ,α)中不同子公式的定義。

定義4設(shè)s∈S，t∈R(s)，φ是FCTL公式，閾值α∈(0,1]。repair(M,φ,α)由下面所有命題公式的合取構(gòu)成。

∨s0∈S0Xs0。

(1)

對(duì)所有的s0∈S0，Xs0,φ。

(2)

(3)

(4)

對(duì)所有的p∈AP且V(s,p)≥α，Xs,p。對(duì)所有的p且V(s,p)≤1-α，Xs,p。

(5)

(6)

(7)

∨t∈R(s)(Es,t∧es,t∧Xt,φ1)。

(8)

∧t∈R(s)(Es,t∧es,t∧Xt,φ1)。

(9)

(10)

對(duì)所有的Aφ1Uφ2∈sub(φ)，m≤|S|，

(11)

對(duì)所有的EGφ1∈sub(φ)，m≤|S|，

(12)

對(duì)所有的AGφ1∈sub(φ)，m≤|S|，

(13)

通過(guò)定義4可以構(gòu)造一個(gè)模糊命題邏輯公式φ，該公式由某些模糊命題邏輯公式的合取構(gòu)成，這些命題功能解釋如下：式(1)要求子模型在初始狀態(tài)所對(duì)應(yīng)的公式是可滿足的；式(2)～(4)要求子模型是FKS；式(5)～(13)要求出現(xiàn)的每個(gè)子公式都是α-可滿足的。我們可以用模糊tableaux方法[21]來(lái)求解這個(gè)命題邏輯公式φ。值得一提的是，模糊tableaux方法是命題邏輯公式tableaux方法的擴(kuò)張，可以用來(lái)解決模糊命題邏輯公式的可滿足性。

對(duì)于圖1中子模型，設(shè)FCTL公式φ為AGq，閾值α=0.3。以此為例給出一個(gè)具體的repair(M,φ,α)構(gòu)造出的模糊命題邏輯公式φ。

圖1 子模型示例圖Figure 1 Sub-model example diagram

證明定義4構(gòu)造了一個(gè)模糊命題邏輯公式φ，這個(gè)公式是一系列子公式的合取，通過(guò)每個(gè)子公式的具體構(gòu)造方法，來(lái)分析整個(gè)構(gòu)造過(guò)程的時(shí)間復(fù)雜度。

定義4中式(1)需要遍歷每個(gè)s0∈S0，所以時(shí)間復(fù)雜度是O(|S0|)。同理，式(2)的時(shí)間復(fù)雜度也是O(|S0|)。式(3)需要遍歷每個(gè)s∈S及其所有的后繼狀態(tài)，所以這種情況的時(shí)間復(fù)雜度是O(|S|×d)。式(4)要求遍歷每個(gè)遷移，故時(shí)間復(fù)雜度為O(|R|)。定義4中式(5)要求考慮每個(gè)狀態(tài)上的原子命題的值，因此時(shí)間復(fù)雜度是O(|S|×|AP|)。式(6)和式(7)要求遍歷每個(gè)狀態(tài)和每個(gè)子公式，故得到時(shí)間復(fù)雜度是O(|S|×|φ|)。定義4中式(8)和式(9)需要遍歷每個(gè)子公式、每個(gè)狀態(tài)和對(duì)應(yīng)的后繼狀態(tài)，所以時(shí)間復(fù)雜度是O(|S|×|φ|×d)。式(10)最多需要m次遍歷，其中1≤m≤|S|，每次要求遍歷每個(gè)子公式、每個(gè)狀態(tài)和對(duì)應(yīng)的后繼狀態(tài)，所以時(shí)間復(fù)雜度是O(|S|2×|φ|×d)。同理，式(11)～(13)的時(shí)間復(fù)雜度是O(|S|2×|φ|×d)。

基于以上分析，定義4構(gòu)造φ的時(shí)間復(fù)雜度是O(|S|2×|φ|×d+|S|×|AP|+|R|)。

算法1SubModel-Repair

輸入:FKS的M，α∈(0,1]，F(xiàn)CTL公式φ。

輸出:如果FKS的M可修復(fù)，則返回修復(fù)后的子模型M′，否則返回FALSE。

2) 對(duì)φ使用模糊tableaux方法，可以得到一個(gè)賦值V

3) ifV是一個(gè)可滿足的賦值

4) returnmodel(M,V)

5) return FALSE

定理3設(shè)模糊命題邏輯公式φ運(yùn)行模糊tableaux方法的時(shí)間復(fù)雜度為O(T(|φ|))，則算法的時(shí)間復(fù)雜度為O(|S|2×|φ|×d+|S|×|AP|+|R|×|φ|+T(|φ|))。

證明根據(jù)現(xiàn)有的模糊模型檢測(cè)算法[5]，可知算法第1)步的時(shí)間復(fù)雜度是

O((|R|+|S|log|S|)×|φ|)。

根據(jù)定理2可知，算法第2步的時(shí)間復(fù)雜度是O(|S|2×|φ|×d+|S|×|AP|+|R|+T(|φ|))，整個(gè)算法的時(shí)間復(fù)雜度是O(|S|2×|φ|×d+|S|×|AP|+|R|×|φ|+T(|φ|))。

以下命題用來(lái)闡述repair(M,φ,α)公式的性質(zhì)，這個(gè)性質(zhì)可以用來(lái)證明算法SubModel-Repair的正確性。

證明對(duì)ξ用結(jié)構(gòu)歸納法[22-23]來(lái)證明此命題成立。這里只給出當(dāng)ξ=p,φ1∨φ2,EXφ1,Eφ1Uφ2時(shí)，這幾種情形的具體證明過(guò)程。因?yàn)槠渌樾闻c這些情形的證明類似，故省略它們的證明過(guò)程。

當(dāng)ξ=φ1∨φ2時(shí)，設(shè)V(Xs,ξ)≥α。根據(jù)定義4中的式(6)知，V(Xs,φ1)≥α或V(Xs,φ2)≥α。根據(jù)歸納假設(shè)知，

當(dāng)ξ=EXφ1時(shí)，設(shè)V(Xs,ξ)≥α，即V(Xs,EXφ1)≥α。根據(jù)定義4中式(8)知，

V(∨t∈R(s)(Es,t∧es,t∧Xt,φ1))≥α，

(14)

(15)

同理，此時(shí)V(Es,t)=1，將V(Es,t)=1代入式(15)中，可以得到兩種情形：

1)V(Xs,φ2)≥α；

接下來(lái)分別對(duì)這兩種情形進(jìn)行討論。

通過(guò)上述結(jié)論，可以證明算法是正確的，如果子模型M′是通過(guò)repair(M,φ,α)公式和model(M,V)所確定的，那么子模型M′一定是α-可滿足的。

2 實(shí)例

本節(jié)通過(guò)一個(gè)醫(yī)療診斷和治療[24-25]的例子來(lái)論證我們的結(jié)果，進(jìn)一步闡述我們工作的潛在應(yīng)用價(jià)值。

假設(shè)在某個(gè)地區(qū)出現(xiàn)了一種新的傳染病毒。醫(yī)院決定先會(huì)診，安排一些醫(yī)生制定一個(gè)治療方案。醫(yī)生們對(duì)這個(gè)病毒還沒(méi)有完全地掌握和了解，但是根據(jù)經(jīng)驗(yàn)覺得某些治療手段(比如氧療措施、口服抗病毒的藥物治療、中西醫(yī)結(jié)合治療等)會(huì)對(duì)這種傳染病有較好的療效[26]。下面我們利用一個(gè)FKS的M模型對(duì)這個(gè)治療過(guò)程進(jìn)行建模[27]。

為了方便敘述，我們把治療過(guò)程建模為6個(gè)階段，在圖2中表示為6個(gè)狀態(tài)，即

S={s0,s1,s2,s3,s4,s5}。

醫(yī)生粗略地將病人的身體情況分為三種狀態(tài)“poor”、“normal”和“good”，分別表示病人的身體狀況“較差”、“一般”和“較好”。醫(yī)生在考慮病人的呼吸、心跳、血壓、體溫和白細(xì)胞計(jì)數(shù)等生理特征后，再根據(jù)個(gè)人的經(jīng)驗(yàn)，給出病人身體情況的綜合評(píng)價(jià)。因?yàn)獒t(yī)生要考慮帶有模糊性的不同因素，所以用狀態(tài)上的模糊賦值表示病人身體的綜合情況，具體如何給出模糊綜合評(píng)價(jià)，可以參考文獻(xiàn)[17]，如何給出模糊賦值可以參考文獻(xiàn)[26]。為了方便闡述，本文簡(jiǎn)單給出表1的模糊賦值，表中的數(shù)值表示原子命題在對(duì)應(yīng)狀態(tài)上成立的程度。

圖2 醫(yī)療診斷的FKSFigure 2 The medical diagnosis FKS

表1 模糊賦值函數(shù)表Table 1 Fuzzy valuation function table

通過(guò)一些治療手段后，病人的身體狀況會(huì)有所好轉(zhuǎn)，即FKS當(dāng)前狀態(tài)轉(zhuǎn)移到下一個(gè)狀態(tài)。醫(yī)生通過(guò)他們的經(jīng)驗(yàn)[28]對(duì)狀態(tài)之間轉(zhuǎn)移的可能性進(jìn)行估計(jì)，這些轉(zhuǎn)移可以用一個(gè)矩陣R表示。