鄧楠軼，張興興，李永明

(陜西師范大學(xué) 計(jì)算機(jī)科學(xué)學(xué)院，陜西 西安710119)

廣義可能性計(jì)算樹邏輯的不動(dòng)點(diǎn)語義

鄧楠軼，張興興，李永明*

(陜西師范大學(xué) 計(jì)算機(jī)科學(xué)學(xué)院，陜西 西安710119)

計(jì)算樹邏輯的不動(dòng)點(diǎn)語義在其對(duì)應(yīng)的符號(hào)模型檢測(cè)方法中具有重要意義。給出廣義可能性計(jì)算樹邏輯的不動(dòng)點(diǎn)語義解釋，并利用歸納法證明此不動(dòng)點(diǎn)為最大或最小不動(dòng)點(diǎn)。結(jié)論表明,廣義可能性計(jì)算樹邏輯的不動(dòng)點(diǎn)語義具有不同于經(jīng)典情形的形式。

廣義可能性測(cè)度；計(jì)算樹邏輯；不動(dòng)點(diǎn)語義；模型檢測(cè)

21世紀(jì)的信息技術(shù)革命愈演愈烈，隨著計(jì)算機(jī)軟硬件系統(tǒng)日趨復(fù)雜，如何保證其正確性成為系統(tǒng)設(shè)計(jì)者和應(yīng)用者不得不關(guān)心的問題。為此提出的諸多驗(yàn)證理論和方法中，模型檢測(cè)[1-4]因其自動(dòng)化程度高而引人注目。模型檢測(cè)是一種形式化的自動(dòng)驗(yàn)證技術(shù)，其基本思想是：對(duì)狀態(tài)空間進(jìn)行窮舉搜索從而驗(yàn)證系統(tǒng)是否滿足其設(shè)計(jì)規(guī)范。模型檢測(cè)的一般步驟是：(1)抽象出系統(tǒng)的數(shù)學(xué)模型；(2)給出能夠描述該系統(tǒng)性質(zhì)的語言；(3)用模型檢測(cè)算法進(jìn)行驗(yàn)證。如果構(gòu)造的模型滿足系統(tǒng)的性質(zhì)則返回“成功”，否則返回“失敗”，并給出反例。

經(jīng)典的模型檢測(cè)已廣泛應(yīng)用于軟硬件系統(tǒng)的正確性驗(yàn)證，但隨著系統(tǒng)日益復(fù)雜，在驗(yàn)證過程中不可避免會(huì)出現(xiàn)一些不確定的信息，而系統(tǒng)中這些不確定的信息有可能會(huì)導(dǎo)致非常嚴(yán)重的后果。為了更好地處理這些不確定信息，一些學(xué)者提出了狀態(tài)遷移模型的量化擴(kuò)展，比如在狀態(tài)中加入時(shí)間[1]，或者在模型中考慮概率[1]、可能性[5]、多值[6-7]或者統(tǒng)計(jì)信息[8]。本文關(guān)注李永明等提出的可能性測(cè)度下的計(jì)算樹邏輯的模型檢測(cè)方法[9-15]。

符號(hào)模型檢測(cè)是1987年由McMillan提出的,其基本原理是將系統(tǒng)的狀態(tài)轉(zhuǎn)換關(guān)系用邏輯公式表示。二叉圖(Binary Decision Diagram)是用以表示邏輯公式的重要手段，OBDD(Order Binary Decision Diagram)作為布爾公式的一個(gè)規(guī)范的表示形式，比一般的傳統(tǒng)公式如析取公式及合取公式能夠更加緊湊地表示狀態(tài)轉(zhuǎn)換關(guān)系，以降低系統(tǒng)模型所需的內(nèi)存空間。換言之，它避免了對(duì)系統(tǒng)狀態(tài)的傳統(tǒng)表示從而解決狀態(tài)爆炸問題。符號(hào)模型檢測(cè)的基礎(chǔ)是對(duì)時(shí)序邏輯符的不動(dòng)點(diǎn)語義解釋。本文主要是系統(tǒng)地給出了廣義可能性計(jì)算樹邏輯的不動(dòng)點(diǎn)語義。

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

本節(jié)介紹本文用到的一些基本概念，廣義可能性Kripke結(jié)構(gòu)及相應(yīng)的廣義可能性計(jì)算樹邏輯。

1.1 廣義可能性Kripke結(jié)構(gòu)(Generalized Possibilistic Kripke Structure ,GPKS)

定義1[13]一個(gè)GPKS是一個(gè)五元組M(S,P,I,AP,L)，其中

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

(2)P:S×S→[0,1]是可能性轉(zhuǎn)移函數(shù)，滿足對(duì)任意狀態(tài)s，存在狀態(tài)t，使得P(s,t)>0；

(3)I:S→[0,1]是可能性初始分布，滿足存在狀態(tài)s，使得I(s)>0；

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

(5)L:S→[0,1]AP是可能性標(biāo)簽函數(shù)，將s映射到AP的模糊子集，表示AP在狀態(tài)s成立的可能性。其中[0,1]AP表示集合AP到單位區(qū)間[0,1]上的函數(shù)全體構(gòu)成的集合。

若S和AP是有窮的，則稱M是有窮的GPKS。

(2) 可能性轉(zhuǎn)移函數(shù)P:S×S→[0,1]可以表示成一個(gè)模糊矩陣P，P=(P(s,t))s,t∈S。P也稱為M的模糊轉(zhuǎn)移矩陣。

(3)I(s)>0的狀態(tài)稱為初始狀態(tài)。設(shè)s、t∈S，P的傳遞閉包P+定義如下：P+(s,t)=∨{P(s0,s1)∧…∧P(sk-1,sk)|s0=s,sk=t,sk-1∈S,k≥1}。

1.2 廣義可能性測(cè)度

定理1[13]Po是Ω=2Paths(M)上的廣義可能性測(cè)度，其滿足如下條件：

(1) Po(?)=0；

注2可能性測(cè)度[5]除了滿足條件(1)和(2)外，還需滿足條件Po(Paths(M))=1。

因?yàn)楸疚目紤]的GPKSM是有窮的，所以rp(s)可以計(jì)算出來，接下來給出一種計(jì)算方法。

Po(Cyl(s0…sn))=

1.3 廣義可能性計(jì)算樹邏輯(Generalized Possibilistic Computation Tree Logic,GPoCTL)

定義4(GPoCTL的語構(gòu)) GPoCTL的狀態(tài)公式按如下的BNF形式定義：

Φ∶∶=true|a|Φ|Φ∧Ψ|Po(φ)。

其中，a∈AP，Ψ是狀態(tài)公式，φ是路徑公式。

GPoCTL的路徑公式：

φ∶∶=○Φ|Φ∪Ψ|Φ∪≤nΨ|□Φ。

其中，Φ、Ψ是狀態(tài)公式。

定義5(GPoCTL的語義) 設(shè)M是GPKS，s∈S，a∈AP，Φ1、Φ2、Ψ是狀態(tài)公式，φ是路徑公式，那么對(duì)于狀態(tài)公式Φ和狀態(tài)s，其語義解釋是模糊集‖Φ‖:S→[0,1]，遞歸定義如下：

‖true‖(s)=1;

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

‖Φ∧Ψ‖(s)=‖Φ‖(s)∧‖Ψ‖(s);

對(duì)路徑公式φ，π=s0s1…，π[i…]=sisi+1…，π∈Paths(M)，其語義解釋是模糊集‖φ‖:Paths(M)→[0,1]，遞歸定義如下：

‖○Φ‖(π)=P(π[0,],π[1])∧ ‖Φ‖(π[1]);

‖Φ∪Ψ‖(π)=‖Ψ‖(π[0])∨

‖Φ‖(π[k]))∧(P(π[j-1],π[j])∧

‖Ψ‖(π[j])));

‖Φ∪≤nΨ‖(π)=‖Ψ‖(π[0])∨

(P(π[j-1],π[j]∧‖Ψ‖(π[j])));

2 GPoCTL的不動(dòng)點(diǎn)語義

與多值CTL模型檢測(cè)問題[17]類似，GPoCTL的模型檢測(cè)問題可以如下描述：

給定一個(gè)有窮GPKSM，M中的狀態(tài)s，GPoCTL狀態(tài)公式Φ，計(jì)算此狀態(tài)滿足公式的程度‖Φ‖(s)。

可以通過對(duì)公式Φ的長度|Φ|進(jìn)行歸納來計(jì)算‖Φ‖(s)，|Φ|表示Φ的子公式的數(shù)量，定義如下：

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

|Φ∧Ψ|=|Φ|+|Ψ|+1;

|Po(○Φ)|=|Po(□Φ)|=|Φ|+1;

|Po(Φ∪Ψ)|=|Po(Φ∪≤nΨ)|= |Φ|+|Ψ|+1。

當(dāng)Φ=a,Φ,Φ1∧Φ2時(shí)，可以直接用語義解釋的公式來遞歸計(jì)算出‖Φ‖(s)，但當(dāng)Φ=Po(φ)時(shí)，‖Φ‖(s)=Po(s|=φ)，因此現(xiàn)在的重點(diǎn)是如何計(jì)算Po(s|=φ)。由GPoCTL的路徑公式知，需分別解決φ=○Φ、φ=Φ∪≤nΨ、φ=Φ∪Ψ和φ=□Φ時(shí)的情形。

定理4每個(gè)GPoCTL路徑公式都可以刻畫為一個(gè)適當(dāng)函數(shù)的最大或最小不動(dòng)點(diǎn)形式：

‖Po(Φ∪Ψ)‖=μZ.(‖Ψ‖∧rp)∨ (‖Φ‖∧Po(○Z))

(1)

‖Po(◇Φ)‖=μZ.(‖Φ‖∧rp)∨Po(○Z)

(2)

‖Po(□Φ)‖=υZ.(‖Φ‖∧rp)∧Po(○Z)

(3)

其中(1)、(2)式中μZ.f(Z)表示f(Z)的最小不動(dòng)點(diǎn)，(3)式中υZ.f(Z)表示f(Z)的最大不動(dòng)點(diǎn)。

證明(1) 對(duì)任何GPoCTL狀態(tài)公式Φ、Ψ和一個(gè)有窮GPKSM，定義函數(shù)f(Z)=(‖Ψ‖∧rp)∨(‖Φ‖∧‖Po(○Z)‖))，這里‖Po(○Z)‖=P°DZ°rp,DZ是關(guān)于向量Z的對(duì)角矩陣，f(Z)是從S上的可能性分布的集合到它本身的一個(gè)函數(shù)。

令Z0=(0,0…0)T是元素全為0的最小向量。定義Zi+1=f(Zi)，因?yàn)閒是單調(diào)的，如果Z′≥Z″，那么f(Z′)≥f(Z″)，因此有上升鏈Z0≤Z1≤…≤Zi≤Zi+1≤…。

因?yàn)镮m(Φ)[13]是有窮的，f所涉及的運(yùn)算不會(huì)再產(chǎn)生新的元素，所以Zi的集合是有窮集，因此存在k使得Zk+1=Zk，即f(Zk)=Zk。接下來證明Zk是f的最小不動(dòng)點(diǎn)。顯然，如果Z是f的一個(gè)不動(dòng)點(diǎn)，則Z≥Z0。因?yàn)閒是單調(diào)的，則有Z=f(Z)≥Z1，歸納得Z≥Zk，因此Zk是f的最小不動(dòng)點(diǎn)。

令A(yù)=‖Po(Φ∪Ψ)‖，由語義解釋知：

對(duì)任何狀態(tài)s,首先證明A是f的不動(dòng)點(diǎn)：

f(A)(s)=(‖Ψ‖(s)∧rp(s))∨(‖Φ‖(s)∧‖Po(○A)‖(s))=(‖Ψ‖(s)∧rp(s))∨(‖Φ‖(s)∧

rp(sj))=(‖Ψ‖(s)∧rp(s))∨(‖Φ‖(s)∧‖Ψ‖(s1)∧rp(s))∨(‖Φ‖(s)∧

‖Φ‖(sk)∧P(sj-1,sj)∧‖Ψ‖(sj)∧rp(sj))))=(‖Ψ‖(s)∧rp(s))∨(‖Φ‖(s)∧

因此A是f的不動(dòng)點(diǎn)。

其次,要證明A是f的最小不動(dòng)點(diǎn)。假設(shè)Z是f的一個(gè)不動(dòng)點(diǎn)，即Z=(‖Ψ‖∧rp)∨(‖Φ‖∧‖Po(○Z)‖)=(‖Ψ‖∧rp)∨(‖Φ‖∧P°DZ°rp)。令

1) 當(dāng)j=0時(shí)，Z(s)=(‖Ψ‖(s)∧rp(s))∨‖Φ‖(s)，此時(shí)A(s)=(‖Ψ‖(s)∧rp(s))∧‖Φ‖(s)。顯然，Z(s)≥A(s)。

2) 假設(shè)j=n時(shí)成立，即有

Z(s)=(‖Ψ‖(s)∧rp(s))∨(‖Φ‖(s)∧

P(sj-1,sj)∧‖Ψ‖(sj)∧rp(sj))∨

P(sj-1,sj)∧‖Ψ‖(sj)∧rp(sj))=A(s)。

3) 則當(dāng)j=n+1時(shí)，有

Z(s)=(‖Ψ‖(s)∧rp(s))∨(‖Φ‖(s)∧

‖ψ‖(sj)∧rp(sj))∨(‖Φ‖(s)∧

(‖Ψ‖(s)∧rp(s))∨(‖Φ‖(s)∧

‖Ψ‖(sj)∧rp(sj))∨(‖Φ‖(s)∧

‖Ψ‖(sj)∧rp(sj))∨(‖Φ‖(s)∧

(‖Ψ‖(s)∧rp(s))∨(‖Φ‖(s)∧

‖Ψ‖(sj)∧rp(sj))∨(‖Φ‖(s)∧

P(sj-1,sj)∧‖Ψ‖(sj)∧rp(sj))=A(s)

綜上所述，Z≥A。因此，A=‖Po(Φ∪Ψ)‖是f的最小不動(dòng)點(diǎn)。

(2) 因?yàn)椤螃?true∪Φ，而‖true‖∧Z=Z，從而有‖Po(◇Φ)‖=μZ.(‖Φ‖∧rp)∨Po(○Z)。

(3) 對(duì)任何GPoCTL狀態(tài)公式Φ、Ψ和一個(gè)有窮GPKSM，定義函數(shù)f(Z)=‖Φ‖∧‖Po(○Z)‖，這里‖Po(○Z)‖=P°DZ°rp，f(Z)是從s上的可能性分布的集合到它本身的一個(gè)函數(shù)。

令Z0=(1,1…1)T是元素全為1 的最大向量。定義Zi+1=f(Zi)，因?yàn)閒是單調(diào)的，如果Z′≤Z″，那么f(Z′)≤f(Z″)，因此有下降鏈Z0≥Z1≥…≥Zi≥Zi+1≥…。

因?yàn)镮m(Φ)[13]是有窮的，f所涉及的運(yùn)算不會(huì)再產(chǎn)生新的元素，所以Zi的集合是有窮集，因此存在k使得Zk+1=Zk，即f(Zk)=Zk。接下來證明Zk是f的最大不動(dòng)點(diǎn)。顯然，如果Z是f的一個(gè)不動(dòng)點(diǎn)，則Z≤Z0。因?yàn)閒是單調(diào)的，則有Z=f(Z)≤Z1，歸納得Z≤Zk。因此Zk是f的最大不動(dòng)點(diǎn)。

令A(yù)=‖Po(□Φ)‖，由語義解釋知：

因此，A是f的不動(dòng)點(diǎn)。

下面要證A是f的最大不動(dòng)點(diǎn)。假設(shè)Z是f的一個(gè)不動(dòng)點(diǎn)，即Z=(‖Φ‖∧rp)∧‖Po(○Z)‖=(‖Φ‖∧rp)∧P°DZ°rp,則有

因此Z≤A。表明A=‖Po(□Φ)‖是f的最大不動(dòng)點(diǎn)。

綜上所述，定理4得證。

注3與經(jīng)典情形下不動(dòng)點(diǎn)語義[2]相比，上述公式與經(jīng)典不動(dòng)點(diǎn)語義形式類似，但是GPoCTL不動(dòng)點(diǎn)語義形式多交了一個(gè)rp，可見rp在廣義可能性情形下的重要性。

3 算法及其復(fù)雜度分析

在計(jì)算定理4中的不動(dòng)點(diǎn)時(shí)，對(duì)不動(dòng)點(diǎn)函數(shù)f(Z)的第n次迭代可以計(jì)算出從 出發(fā)所有長度為n的路徑滿足Φ的最小或最大上界。因?yàn)闋顟B(tài)空間S是有窮的，所以如果路徑π的長度大于|S|+1，則必然存在一條長度至多為|S|+1的路徑π′，使得‖φ‖(π′)≥‖Φ‖(π)或|φ‖(π′)≤‖φ‖(π)，因此不動(dòng)點(diǎn)的計(jì)算在至多|S|+2次后收斂。因?yàn)椴粍?dòng)點(diǎn)的迭代計(jì)算只涉及取大取小運(yùn)算，所以每次迭代的時(shí)間復(fù)雜度至多為O(|S|2)，因此計(jì)算不動(dòng)點(diǎn)需要O(|S|3)。

定理5(GPoCTL模型檢測(cè)不動(dòng)點(diǎn)算法的時(shí)間復(fù)雜度)

對(duì)于有窮GPKSM，GPoCTL狀態(tài)公式Φ，GPoCTL模型檢測(cè)問題M|=Φ的時(shí)間復(fù)雜度為O(size(M)·poly(|S|)·|Φ|)，size(M)表示模型M的大小，|Φ|表示Φ的子公式的個(gè)數(shù)。相應(yīng)的算法如下給出：

算法1：計(jì)算不動(dòng)點(diǎn)

輸入：狀態(tài)集合S上的可能性分布集合到自身的函數(shù)f。

輸出：f的不動(dòng)點(diǎn)。

Procedure Fixpoint(x,f)

x′←f(x)

whilex≠x′ do

x←x′

x′←f(x)

end while

returnx

End Procedure

算法2：GPoCTL模型檢測(cè)不動(dòng)點(diǎn)算法

輸入：GPKSM和GPoCTL公式Φ。

輸出：M中?s∈S，滿足Φ的程度‖Φ‖(s)。

Procedure GpoCTLCheck(Φ)

caseΦ

true return (1)s∈S

areturn (L(s,a))s∈S

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

Po(○Φ) returnP°DΦ°rp

Po(Φ1∪Φ2)returnFixpoint((0)s∈S,f1)

Po(◇Ф)returnFixpoint((0)s∈S,f2)

Po(□Ф)returnFixpoint((0)s∈S,f3)

Endcase

EndProcedure

其中，P=(P(s,t))s,t∈S，DΦ=diag(‖Φ‖(s))s∈S,rp=P+°D,P+=P∨P2∨P3∨…∨PN,N=|S|,P*=P0∨P+,P0表示N×N的單位矩陣，

f2(Z)=(‖Ψ‖∧rp)∨(‖Φ‖∧P°DZ°rp),

f1(Z)=(‖Φ‖∧rp)∨(P°DZ°rp),

f3(Z)=‖Φ‖∧P°DZ°rp。

注4GPoCTL模型檢測(cè)的不動(dòng)點(diǎn)算法與經(jīng)典CTL模型檢測(cè)的不動(dòng)點(diǎn)算法思想上是一致的，區(qū)別在GPoCTL的不動(dòng)點(diǎn)算法是計(jì)算出具體狀態(tài)公式的取值，而經(jīng)典CTL的不動(dòng)點(diǎn)算法是計(jì)算出狀態(tài)公式的滿足集Sat(Φ)。

5 結(jié)語

本文基于廣義可能性Kripe結(jié)構(gòu)，給出了GPoCTL的不動(dòng)點(diǎn)語義，基于此在對(duì)GPKS模型進(jìn)行驗(yàn)證時(shí)，可以利用不動(dòng)點(diǎn)算法來達(dá)到目的。不動(dòng)點(diǎn)語義完善了現(xiàn)有的廣義可能性模型檢測(cè)理論。

進(jìn)一步的工作為廣義必要性測(cè)度下GPoCTL的模型檢測(cè)不動(dòng)點(diǎn)語義解釋。

[1]BaierC,KatoenJP.Principlesofmodelchecking[M].Cambridge:MITpress, 2008.

[2]ClarkE,GrumbergO,PeledD.ModelChecking[M].Cambridge:TheMITPress,1999.

[3]RozierKY.Lineartemporallogicsymbolicmodelchecking[J].ComputerScienceReview, 2011, 5(2): 163-203.

[4] 林惠民, 張文輝. 模型檢測(cè): 理論, 方法與應(yīng)用[J].電子學(xué)報(bào), 2002, 30(12A): 1907-1912.

[5]LiYongming,LiLijun.Modelcheckingoflinear-timepropertiesbasedonpossibilitymeasure[J].FuzzySystems, 2013, 21(5): 842-854.

[6]ChechikM,DevereuxB,EasterbrookS,etal.Multi-valuedsymbolicmodel-checking[J].ACMTransactionsonSoftwareEngineeringandMethodology, 2003, 12(4): 371-408.

[7]FischerE,GradelE,KaiserL.Modelcheckinggamesforthequantitative-calculus[J].TheoryofComputingSystems,2010(47):696-719.

[8]KwiatkowskaM,NormanG,ParkerD.Stochasticmodelchecking[M]∥Formalmethodsforperformanceevaluation.BerlinHeidelberg:Springer, 2007: 220-270.

[9]ZadehLA.Fuzzysets[J].InformationandControl, 1965, 8(3): 338-353.

[10] 李永明. 模糊系統(tǒng)分析[M].北京：科學(xué)出版社, 2005.

[11] 王熙照. 模糊測(cè)度和模糊積分及在分類技術(shù)中的應(yīng)用[M].北京：科學(xué)出版社, 2008.

[12] Li Yongming, Li Yali, Ma Zhanyou. Computation tree logic model checking based on possibility measures[J].Fuzzy sets and Systems, 2015, 262:44-59.

[13] Li Y, Ma Z. Quantitative computation tree logic model checking based on generalized possibility measures[J].DOI:10.1109/TFUZZ.2015.2396537.

[14] 李亞利，李永明.可能性測(cè)度下計(jì)算樹邏輯的若干性質(zhì)[J].陜西師范大學(xué)學(xué)報(bào):自然科學(xué)版，2013,41(6):6-12.

[15] 李永明.可能LTL模型檢測(cè)的兩種方法[J].陜西師范大學(xué)學(xué)報(bào):自然科學(xué)版，2014，42(6):21-25.

[16] Chechik M, Easterbrook S, Petrovykh V.Model-checking over multi-valued logics[C].Proceedings of FME,2001:72-89.

〔責(zé)任編輯 宋軼文〕

Fixed-point semantics of computation tree logic based on generalized possibility measures

DENG Nanyi, ZHANG Xingxing, LI Yongming*

(School of Computer Science, Shaanxi Normal University,Xi′an 710119, Shaanxi, China)

Fixed-point semantics of computation tree logic plays an important role in symbolic model checking.Fixed-point semantics of generalized possibilistic computation tree logic is presented, then the greatest or least fixed-point is shown by the method of mathematical induction, which is different from the form in classical model checking.

generalized possibility measures;computation tree logic; fixed-point characterization;model checking

68Q45

1672-4291(2015)04-0022-06

10.15983/j.cnki.jsnu.2015.04.145

2014-12-16

國家自然科學(xué)基金(11271237,61228305);高等學(xué)校博士學(xué)科點(diǎn)專項(xiàng)基金(20130202120001)

鄧楠軼，男，碩士研究生，研究方向?yàn)槟Ｐ蜋z測(cè)、信息安全攻防。E-mail:nanyideng@gmail.com

*通信作者:李永明,男,教授,博士生導(dǎo)師。E-mail:liyongm@snnu.edu.cn

TP301.2

A