魚先鋒，李 超，李永明

1.商洛學(xué)院 數(shù)學(xué)與計算機應(yīng)用學(xué)院，陜西 商洛 726000 2.陜西師范大學(xué) 計算機科學(xué)學(xué)院，西安 710062

直覺模糊測度的計算樹邏輯*

魚先鋒1+，李 超1，李永明2

1.商洛學(xué)院 數(shù)學(xué)與計算機應(yīng)用學(xué)院，陜西 商洛 726000 2.陜西師范大學(xué) 計算機科學(xué)學(xué)院，西安 710062

直覺模糊Kripke結(jié)構(gòu)；直覺模糊測度；直覺模糊計算樹邏輯；模型檢測

1 引言

模型檢測[1-5]作為一種形式化自動驗證技術(shù)，自1981年由Clarke、Emerson等人提出之后，在計算機軟硬件設(shè)計與可靠性分析、通信協(xié)議、安全協(xié)議等正確性分析方面獲得了成功的應(yīng)用。經(jīng)典模型檢測技術(shù)主要驗證系統(tǒng)定性性質(zhì)，近些年來，許多學(xué)者注重系統(tǒng)定量性質(zhì)的驗證，提出了量化模型檢測技術(shù)，包括概率模型檢測[6-7]、可能性模型檢測[8-14]等。這些量化模型檢測技術(shù)在驗證不確定環(huán)境下系統(tǒng)量化性質(zhì)方面有著各自的特點。概率模型檢測用于驗證系統(tǒng)轉(zhuǎn)移在確定概率分布情況下的性質(zhì)?？赡苄阅Ｐ蜋z測用以驗證系統(tǒng)轉(zhuǎn)移具有模糊不確定的性質(zhì)，比概率模型檢測表現(xiàn)力要強。直覺模糊集[15]是模糊集[16]的推廣，可以更客觀自然地表示對象間不確定的隸屬關(guān)系和非隸屬關(guān)系。因此研究基于直覺模糊測度的模型檢測理論與技術(shù)有著重要的理論和現(xiàn)實意義。本文將在直覺模糊模型檢測方面做些初步探索工作。

2 直覺模糊集與直覺模糊Kripke結(jié)構(gòu)

定義1（intuitionistic fuzzy structure，IFS）[15]設(shè) X是一個給定的論域，稱 A={＜x,μA(x),vA(x)＞|x∈X}為 X上的IFS，其中，μA(x):X→I,vA(x):X→I，且 0≤μA(x)+vA(x)≤1(?x∈X)。 μA(x)表示 x對 A的隸屬程度，vA(x)表示x對A的非隸屬程度。X上的所有IFS記為IFS(x)。稱πA(x)=1-μA(x)-vA(x)為x對 A的猶豫度。X中x對A的隸屬度與非隸屬度所組成序?qū)?μA(x),vA(x))稱為直覺模糊數(shù)。因此，可以將X上的IFSA看作直覺模糊數(shù)的集合，即可記A={(μA(x),vA(x))|x∈X}。

定義2（直覺模糊關(guān)系的合成）[17]設(shè) P=(μPij,γPij)n×n和 Q=(μQij,γQij)n×n為直覺模糊矩陣，若 R=P°Q=(μij,γij)n×n,則稱R是P和Q的合成矩陣，這里

定義3（直覺模糊數(shù)的序）對任意兩個直覺模糊數(shù) a=(μ1,λ1),b=(μ2,λ2) ，，若 μ1=μ2且λ1=λ2，則稱直覺模糊數(shù)a等于b，記作a=b；否則：

（1）若d＞0，則稱a大于b，記作a＞b；

（2）若d＜0，則稱a小于b，記作a＜b。

若 μ1=μ2且 λ1=λ2，則稱直覺模糊數(shù)a等于b是很自然的。若 μ1＞μ2，λ1≤λ2，此時 a＞b也是自然的，但若出現(xiàn) μ1＞μ2，λ1＞λ2這種情況，就不好刻畫 a 與 b的大小了。比如，a=(0.8,0.1)，b=(0.7,0.05)。這種情況下考慮隸屬度比值與非隸屬度比值的差異情況，即即d＞0，說明隸屬度的差異較大，對直覺模糊數(shù)的大小區(qū)別做主要貢獻，故認為a＞b是合理的。同理定義3中關(guān)于a＜b的定義也是合理的。

定義 4（intuitionistic fuzzy Kripke structure，IFKS）一個直覺模糊Kripke結(jié)構(gòu)（IFKS）是一個五元組，表示為M=(S,P,I,AP,L)，其中：

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

（2）P:S×S→[0,1]2是直覺模糊轉(zhuǎn)移函數(shù)，滿足對于每個狀態(tài)s都有成立；一般的?s,s′∈S,P(s,s′)=(μ,γ)，這里 (μ,γ)∈[0,1]2是一個直覺模糊數(shù)。其中 μ刻畫了從狀態(tài)s遷移到狀態(tài)s′的可達度，γ刻畫了從狀態(tài)s遷移到狀態(tài)s′的不可達度，π=1-μ-γ刻畫了從狀態(tài)s遷移到狀態(tài)s′的猶豫程度。

（3）I:S→[0,1]2是初始可能性分配函數(shù)，使得

（4）AP是一組原子命題之集。

（5）L:S→2AP是標記函數(shù)，即在每個狀態(tài)下都有一個賦值(AP的子集)。

如果S和AP是有窮的，則稱M為有窮的直覺模糊Kripke結(jié)構(gòu)。

注意1這里假設(shè) AP=S和L(s)={s}，對X?[0,1]，集合X的最小上界和最大下界分別用∨X和∧X表示。所有滿足I(s)＞0的狀態(tài)s被定義為初始狀態(tài)。對于狀態(tài)s和T?S，P(s,T)表示從狀態(tài)s出發(fā)經(jīng)過一步轉(zhuǎn)移到達T中的某些狀態(tài)t的可達度，表示為。

例1如圖1所示為一個IFKSM=(S,P,I,AP,L)的圖形表示，圖中圓圈代表狀態(tài)，箭頭代表轉(zhuǎn)移，箭頭上的數(shù)字表示一個狀態(tài)轉(zhuǎn)移到另一個狀態(tài)的可達度。其中 S={s0,s1,s2,s3}，I(s0)=(1,0)，即初始狀態(tài)是 s0，L(s0)={s0}，L(s1)={s1}，L(s2)={s2},L(s3)={s3}，P(s0,s1)=(1,0)，P(s0,s2)=(0.2,0.6)，P(s1,s2)=(1,0)，P(s1,s3)=(0.9,0.06)，P(s2,s1)=(0.7,0.1)，P(s2,s3)=(1,0)，P(s3,s3)=(1,0)。通常用矩陣(P(s,t))s,t∈S表示直覺模糊轉(zhuǎn)移函數(shù)P:S×S→[0,1]2，稱其為直覺模糊轉(zhuǎn)移矩陣。該IFKS的直覺模糊轉(zhuǎn)移矩陣為(按順序 s0＜s1＜s2＜s3表示第1、2、3、4行和列)：

Fig.1 IFKS M has 4 states圖1 四狀態(tài)的IFKS M

對于IFKSM，無窮狀態(tài)序列π=s0s1s2…∈Sw表示M中的無窮路徑，其中對于所有的i∈N，滿足P(si,si+1)＞0。用Paths(M)表示M中無窮路徑集合。Pathsfin(M)表示M中所有有窮路徑集合，有窮路徑形如 s0s1…sn(n∈N)，對于 0≤i＜n，P(si,si+1)＞(0,1)。Paths(s)表示M中從狀態(tài)s出發(fā)的無窮路徑集合。Pathsfin(s)表示M中從狀態(tài)s出發(fā)的有窮路徑集合，形如s0s1…sn，其中 s0=s。

M中的狀態(tài)和狀態(tài)集合的前驅(qū)（記為Pre）、后繼（記為Post）的定義如下：

3 直覺模糊Kripke結(jié)構(gòu)上的直覺模糊測度

實際上，上述直覺模糊測度滿足以下定理2的3個條件，從而稱IFPM為Ω上的直覺模糊測度是合理的。另外，在不發(fā)生歧義的情況下，IFPM簡寫為IFP。

定理1設(shè)M是一個IFKS，則有窮路徑擴展的無窮路徑的直覺模糊測度表示為：

特別地，

證明 因為Cyl(s0s1…sn)=?{π∈Sw|s0s1…sn∈Pref(π)}，則有 IFP(Cyl(s0s1…sn))=∨{Po(π)|s0s1…sn∈Pref(π)}=

在文章后續(xù)，用IFP(s0s1…sn)來表示。

定理2直覺模糊測度IFP滿足以下3個性質(zhì)：

（1）IFP(?)=(0,1)，IFP(Paths(M))=(1,0)；

（2）如果 Ai∈Ω ，i∈N ，則；

（3）如果 A?B，A，B∈Ω，則IFP(A)≤IFP(B)。但一般的，下列性質(zhì)未必是成立的：

（4）如果 A1?A2?…為下降列，則

證明 （1）①因為 IFP(?)= ∨{IFP(π)|π∈?}=(0,1)，所以 IFP(?)=(0,1)。)，所以 IFP，根據(jù)定理1可知 IFP(Paths(M))=。又因為對于，所以 IFP(Paths(M))=(1,0)。

（2）因為

所以性質(zhì)（2）成立。

（3）因為 A?B，根據(jù)性質(zhì)（2）可得：

進而推出IFP(A)≤IFP(B)。

Fig.2 IFKSMhas 2 states圖2 二狀態(tài)的IFKS M

定義7M=(S,P,I,AP,L)為IFKS，P是關(guān)于狀態(tài)s的直覺模糊傳遞分布。?s∈S,T?S，P(s,T)表示經(jīng)s一步轉(zhuǎn)移至T的直覺模糊測度，即?s,t∈S，P的傳遞閉包P+定義為：

注意2?s,t∈S，在IFKSM=(S,P,I,AP,L)中必然存在有窮路徑使得其中s0=s,sn=t。因此P的傳遞閉包P+還可以表示成。其中 Pk+1=Pk°P ，這里°為定義2給出的直覺模糊矩陣合成運算，即maxmin復(fù)合運算。

下面引入函數(shù)r(s)方便描述本文后續(xù)結(jié)果。

定義8 M=(S,P,I,AP,L)為IFKS，r:S→[0,1]2，?s∈

下面給出r(s)的一種形式化計算方法。

定理3 M=(S,P,I,AP,L)為IFKS，假設(shè) n=|S|是有窮的，則?s∈S，有：

證明 分兩步證明：

（2）因為 P+(s,t)∧P+(t,t)=P(s1,s2)∧…∧P(si,t)∧P(t,t1)∧P(t1,t2)∧…∧P(tr,t)，其中 s1=s，si,t,tr∈S，i,r∈N，所以對M中的任一無窮路徑π+=s1s2…si(tt1…trt)ω，有：

由π+的任意性可得，

綜合（1）、（2）知定理3成立。 □

注意3定理3計算r(s)的時間主要取決于計算直覺模糊關(guān)系矩陣P的傳遞閉包P+，所以時間復(fù)雜度為O(n2lbn)[18]。

4 直覺模糊計算樹邏輯及其性質(zhì)

直覺模糊計算樹邏輯（intuitionistic fuzzy computation tree logic，IFPCTL）是建立在IFKS上的一種計算樹邏輯。和經(jīng)典計算樹邏輯（computation tree logic，CTL）公式一樣，IFPCTL公式也包含狀態(tài)公式和路徑公式。不同的是IFPCTL不再使用路徑量詞?、?，而用 IFPJ(φ)代替。這里 φ 是路徑公式，J?[0,1]2，J表示公式φ的直覺模糊上界和下界。?s∈IFKS M，s╞IFPJ(φ)表明IFP(Paths(s))?J。定量性是指到達壞狀態(tài)的IFP足夠小，或者到達好狀態(tài)的IFP很大，超過給定值。定性性是定量性的一個特例，它要求所有轉(zhuǎn)移的IFP不是(0,1)就是(1,0)。

定義9定量的IFPCTL語構(gòu)定義如下。

IFPCTL的狀態(tài)公式：

其中，a∈AP；?、?1、?2是IFPCTL狀態(tài)公式；φ是IFPCTL路徑公式；J?[0,1]2。 IFP≤(0.5,0.25)(φ)表示IFP[(0,1),(0.5,0.25)](φ)。

IFPCTL的路徑公式：

其中 ?、?1、?2是IFPCTL狀態(tài)公式，n∈N 。

定義10M=(S,P,I,AP,L)為IFKS，?s∈S，a∈AP,?1、?2是IFPCTL狀態(tài)公式，φ是IFPCTL路徑公式，則IFPCTL滿足的關(guān)系為：

（1）s╞IFPJ(φ)當且僅當IFP(s╞φ)∈J，其中IFP(s╞φ)=IFP({π∈Path(s)|π╞φ})；

（2）π╞?1?≤n?2當且僅當?0≤j≤n，π[j]╞?2且?0≤k＜j,π[k]╞?1。

特別的：

（1）π╞??當且僅當?j≥0,π[j]╞?；

（2）π╞□?當且僅當?j≥0,π[j]╞?；

（3）π╞?1W?2當且僅當 π╞?1??2或 π╞□?1。

其他滿足關(guān)系與經(jīng)典的CTL公式滿足關(guān)系相同，詳見文獻[19]。

定義11 ?、ψ為IFPCTL狀態(tài)公式，記Sat(?)={s|s∈S,s╞?}，稱?與ψ等價，記作?≡ψ，當且僅當Sat(?)=Sat(ψ)。

定理 4 IFP＞(0,1)(○IFP＞(0,1)(??))≡ IFP＞(0,1)(?IFP＞(0,1)(○?))。

證明 先證 Sat(IFP＞(0,1)(○IFP＞(0,1)(??)))?Sat(IFP＞(0,1)(?IFP＞(0,1)(○?)))，?s∈ Sat(IFP＞(0,1)(○IFP＞(0,1)(??)))，即：

則s有直接后繼頂點t0，滿足t0╞IFP＞(0,1)(??)。這樣就存在從 t0出發(fā)，到達 tn∈Sat(?)的路徑 t0t1…tn。其中，tn-1╞IFP＞(0,1)(○?)，這樣就得到路徑st0t1…tn-1，滿足s╞IFP＞(0,1)(?IFP＞(0,1)(○?))。因此，s∈Sat(IFP＞(0,1)(? IFP＞(0,1)(○?))),也就有：

再 證 Sat(IFP＞(0,1)(? IFP＞(0,1)(○?)))? Sat(IFP＞(0,1)(○IFP＞(0,1)(??)))，?s∈Sat(IFP＞(0,1)(?IFP＞(0,1)(○?)))，即：

則存在路徑s0s1…sn,其中s=s0，sn╞IFP＞(0,1)(○?)。這樣sn必有一直接后繼t，且t╞?。這樣就得到路徑s1s2…snt使得s1╞IFP＞(0,1)(??)，由于s1為s0的一個后繼，故有s╞IFP＞(0,1)(○IFP＞(0,1)(??))。因此，s∈Sat(IFP＞(0,1)(○IFP＞(0,1)(? ?)))，也就有：

綜上 Sat(IFP＞(0,1)(○IFP＞(0,1)(??)))=

Sat(IFP＞(0,1)(? IFP＞(0,1)(○?)))

由定義10知：

IFP＞(0,1)(○IFP＞(0,1)(? ?))≡IFP＞(0,1)(?IFP＞(0,1)(○?)) □

定義12定性的IFPCTL的語構(gòu)遞歸定義如下。

IFPCTL的狀態(tài)公式：

其中，a∈AP；?、?1、?2是IFPCTL狀態(tài)公式；φ是IFPCTL路徑公式。

IFPCTL的路徑公式：

其中?、?1、?2是IFPCTL狀態(tài)公式，n∈N。

定義13 ?、ψ為IFPCTL或PoCTL（possibilistic computation tree logic）或CTL，稱 ? 等價于 ψ ，記作 ?≡ψ，當且僅當 Sat(?)=Sat(ψ)。

注意4定義12指出若滿足給定的IFPCTL，PoCTL和CTL的狀態(tài)之集相同，就可以稱所滿足的公式是等價的，這使得IFKS、PoKS和KS間的模擬刻畫成為可能。

定理5以下IFPCTL、PoCTL和CTL公式等價：

（1）IFP＞(0,1)(?a)≡PO＞0(?a)≡??a

（2）IFP＞(0,1)(○a)≡ PO＞0(○a)≡ ?○a

（3）IFP＞(0,1)(□a)≡ PO＞0(□a)≡?□a

（4）IFP＞(0,1)(a?b)≡PO＞0(a?b)≡?(a?b)

（5）IFP＞(0,1)(aWb)≡PO＞0(aWb)≡?(aWb)

證明（1）先證IFP＞(0,1)(?a)≡??a。設(shè)s╞IFP＞(0,1)(?a)，則IFP(s╞?a)＞(0,1)。因此{π|π∈Path(s),π╞?a}≠?，故s╞??a。另一方面設(shè)s╞??a，則存在路徑s0s1…si…，其中s=s0且?si使得si╞a。因此IFP(s╞?a)≥IFP((s0s1…si…)╞?a)＞(0,1)，從而s╞IFP＞(0,1)(?a)。綜 上 IFP＞(0,1)(?a)≡??a 。再 證 PO＞0(?a)≡??a，與 IFP＞(0,1)(?a)≡??a的證明方法一樣，不再累述。所以 IFP＞(0,1)(?a)≡PO＞0(?a)≡??a。

（2）、（3）的證明與（1）類似。

（4）先證明IFP＞(0,1)(a?b)≡?(a?b)。假設(shè)s╞IFP＞(0,1)(a?b)，則IFP(s╞(a?b))＞(0,1)。因此{π|π∈Path(s),π╞(a?b)}≠?，故s╞?(a?b)。另一方面設(shè)s╞?(a?b)，則存在有窮路徑s0s1…sn，其中s=s0且si╞a(i=0,1,…,n-1)，sn╞b。因此IFP(s╞(a?b))≥IFP((s0s1…sn)╞(a?b))＞(0,1)，從而s╞IFP＞(0,1)(a?b)。綜上IFP＞(0,1)(a?b)≡?(a?b)。再證 PO＞0(a?b)≡?(a?b)，與 IFP＞(0,1)(a?b)≡?(a?b)的證明方法一樣，不再累述。因此IFP＞(0,1)(a?b)≡PO＞0(a?b)≡?(a?b)。

（5）先證明IFP＞(0,1)(aWb)≡?(aWb)。假設(shè)s╞IFP＞(0,1)(aWb)，則IFP(s╞(aWb))＞(0,1)。因此{π|π∈Path(s),π╞(aWb)}≠?，故s╞?(aWb)。假設(shè)s╞?(aWb)，則存在有窮路徑s0s1…sn，其中s=s0且si╞a(i=0,1,…,n-1)，sn╞b；或存在路徑s0′s1′…，其中s′=s0′且?i≥0,si′╞a。因此IFP(s╞(aWb))≥IFP(s0s1…sn)∨IFP(s0′s1′…)＞(0,1)，從而s╞IFP＞(0,1)(aWb)。綜上IFP＞(0,1)(aWb)≡?(aWb)。再證 PO＞0(aWb)≡?(aWb)，與 IFP＞(0,1)(aWb)≡?(aWb)的證明方法一樣，不再累述。 □

定理6以下IFPCTL和PoCTL公式等價：

（1）IFP=(1,0)(? a)≡ PO=1(? a)

（2）IFP=(1,0)(□a)≡ PO=1(□a)

（3）IFP=(1,0)(○a)≡ PO=1(○a)

（4）IFP=(1,0)(a?b)≡PO=1(a?b)

（5）IFP=(1,0)(aWb)≡ PO=1(aWb)

直覺模糊測度的非隸屬度為“0”，它就退化成對應(yīng)的可能測度了，因此定理6成立是顯然的。

定理7以下IFPCTL和CTL公式不等價：

（1）IFP=(1,0)(?a)???a

（2）IFP=(1,0)(□a)??□a

（3）IFP=(1,0)(○a)??○a

（4）IFP=(1,0)(a?b)??(a?b)

（5）IFP=(1,0)(aWb)??(aWb)

假設(shè)?既是IFPCTL也是CTL，則Sat(IFP=(1,0)(?))={s|s∈S,IFP(path(s))=(1,0)}，考慮 s∈Sat(IFP=(1,0)(?))，存在從 s出發(fā)的路徑 s10s11…，s20s21…，…sk0sk2…，其中s=s10=s20=…=sk0，k∈N。因為(si0si1…╞?)，所以 s∈Sat(IFP=(1,0)(?))，必須且只需?0≤i≤k，使得 IFP(si0si1…╞?)=(1,0)。而 s∈Sat(??)要求?0≤i≤k，使得 IFP(si0si1…╞?)=(1,0)，顯然 Sat(??)?Sat(IFP=(1,0)(?))。

因此一般情況下IFP=(1,0)(?)≡??。對于定理7中的結(jié)論很容易給出反例來證明它們。

5 小結(jié)

本文建立了IFKS模型（定義4），提出了直覺模糊測度空間理論（定義6），討論了IFKS的一系列性質(zhì)（定理1、定理2）。定義了IFKS中任一路徑的直覺模糊測度以及從任一狀態(tài)出發(fā)的路徑簇的直覺模糊測度。提出了路徑轉(zhuǎn)移矩陣P及其傳遞閉包P+的概念（定義7），給出了通過計算路徑轉(zhuǎn)移矩陣傳遞閉包計算路徑IFP的算法（定理3），分析了算法的復(fù)雜度。提出了直覺模糊計算樹邏輯（IFPCTL）理論（定義9、定義13），討論了一組IFPCTL、PoCTL和CTL公式的等價性（定理4、定理5）。給出了一組等價的IFPCTL和PoCTL公式（定理6），以及一組不等價的IFPCTL和CTL公式（定理7）。這些性質(zhì)是IFPCTL、PoCTL和CTL模擬刻畫的基礎(chǔ)，也是直覺模糊測度模型檢測的基礎(chǔ)。

[1]Clake E,Grumberg O,Peled D.Model checking[M].Cambridge,USA:MIT Press,1999.

[2]Lin Huimin,Zhang Wenhui.Model checking:theories,techniques and applications[J].Acta Electronica Sinica,2002,30(12A):1907-1912.

[3]Baier C,Katoen J P.Principles of model checking[M].Cambridge,USA:MIT Press,2007.

[4]Rozier K Y.Linear temporal logic symbolic model checking[J].Computer Science Review,2011,5(2):163-203.

[5]Yu Xianfeng,Lei Lihui,Li Yongming.Modeling and verification of batch system[J].Computer Science,2011,38(4):257-259.

[6]Hart S,Sharir M.Probabilistic propositional temporal logics[J].Information and Control,1986,70(2/3):97-155.

[7]Hansson H.Time and probability in formal design of distributed systems[M].New York:Elsevier Science Inc,1994.

[8]Xue Yan,Lei Hongxuan,Li Yongming.Computation tree logic based on possibility measure[J].Computer Engineering and Science,2011,33(9):70-75.

[9]Xue Yan,Lei Hongxuan,Li Yongming.Possibilistic Kripke structure decision processes[C]//Proceedings of the 2012 Conference on Quantitative Logic and Soft Computing,Xi'an,China,May 12-15,2012.Singapore:World Scientific Publishing Company,2012:295-302.

[10]Li Yongming,Li Lijun.Model-checking of linear-time properties based on possibility measure[J].IEEE Transactions on Fuzzy Systems,2013,21(5):842-854.

[11]Deng Hui,Xue Yan,Li Yali,et al.Computation tree logic CTL*based on possibility measure and possibilistic bisimulation[J].Computer Science,2012,39(10):258-263.

[12]Li Yali,Li Yongming.Some properties of computation tree logic under possibility measure[J].Journal of Shaanxi Normal University:Natural Science Edition,2013,41(6):6-11.

[13]Li Yongming.Two methods for possibilistic linear temporal logic model checking[J].Journal of Shaanxi Normal University:Natural Science Edition,2014,42(6):21-25.

[14]Ma Zhanyou,Li Yongming.Model checking of reachability problem based on possibility measure[J].Fuzzy Systems and Mathematics,2014,28(6):88-97.

[15]Atanassov K T.Intuitionistic fuzzy sets[J].Fuzzy Sets and System,1986,20(1):87-96.

[16]Zadeh L A.Fuzzy sets[J].Information and Control,1965,8(3):338-353.

[17]Zhao Faxin,Ma Zongmin,Yan Li.Fuzzy clustering based on vague relations[C]//LNCS 4223:Proceedings of the 3rd International Conference on Fuzzy Systems and Knowledge Discovery,Xi'an,China,Sep 24-28,2006.Berlin,Heidelberg:Springer,2006:79-88.

[18]Garmendia L,González R C,López V,et al.An algorithmto compute the transitive closure,a transitive approximation and a transitive opening of a fuzzy proximity[J].Mathware and Soft Computing,2009,16(2):175-191.

[19]Baier C,Katoen J P.Principles of model checking[M].Cambridge,USA:MIT Press,2007.

附中文參考文獻:

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

[5]魚先鋒,雷麗暉,李永明.單道批處理系統(tǒng)的建模與驗證[J].計算機科學(xué),2011,38(4):257-259.

[8]薛艷,雷紅軒,李永明.基于可能性測度的計算樹邏輯[J].計算機工程與科學(xué),2011,33(9):70-75.

[11]鄧輝,薛艷,李亞利,等.基于可能性測度的計算樹邏輯CTL*與可能性互模擬[J].計算機科學(xué),2012,39(10):258-263.

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

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

[14]馬占有,李永明.基于廣義可能性測度的可達性問題的模型檢測[J].模糊系統(tǒng)與數(shù)學(xué),2014,28(6):88-97.

YU Xianfeng was born in 1984.He is an M.S.candidate and lecturer at Shangluo University.His research interest includes model checking and fuzzy system analysis,etc.

魚先鋒（1984—），男，陜西商州人，商洛學(xué)院碩士研究生、講師，主要研究領(lǐng)域為模型檢測，模糊系統(tǒng)分析等。

LI Chao was born in 1965.He is a professor at Shangluo University.His research interest includes model checking and fuzzy system analysis,etc.

李超（1965—），男，陜西鎮(zhèn)安人，商洛學(xué)院教授，主要研究領(lǐng)域為模型檢測，模糊系統(tǒng)分析等。

Computation Tree Logic Based on Intuitionistic Fuzzy Measure*

YU Xianfeng1+,LI Chao1,LI Yongming2
1.Institute of Mathematics and ComputerApplication,Shangluo University,Shangluo,Shaanxi 726000,China 2.School of Computer Science,Shaanxi Normal University,Xi'an 710062,China

This paper establishes the intuitionistic fuzzy Kripke structure(IFKS)model,proposes the intuitionistic fuzzy measure theory based on IFKS,and expounds a series of properties of IFKS.Then,this paper proves that the intuitionistic fuzzy probability(IFP)of every path in an IFKS is the infimum of the IFP of the initial state and every translation in the path,and the IFP of those paths that start from the same initial state is the supremum of their IFP.This paper also defines the transfer matrix of pathPand its transitive closureP+,gives an algorithm which can be used for calculatingP+,and analyzes the complexity of the algorithm.After that,this paper builds the intuitionistic fuzzy computation tree logic(IFPCTL)theory,and discusses the equivalence of a set of formula about IFPCTL,possibilistic computation tree logic(PoCTL)and computation tree logic(CTL).Finally,this paper gives a set of equivalent formula about IFPCTL and PoCTL,and a set of inequitable formula about IFPCTL and CTL at the same time.

intuitionistic fuzzy Kripke structure;intuitionistic fuzzy probability;intuitionistic fuzzy computation tree logic;model checking

the Ph.D.degree from Sichuan University in 1996.Now he is a professor and Ph.D.supervisor at Shaanxi Normal University,and the senior member of CCF.His research interests include intelligent computing,fuzzy system analysis,quantum information and quantum logic,etc.

2016-06, Accepted 2016-08.

A

TP301.2

+Corresponding author:E-mail:pioneer.369@163.com

YU Xianfeng,LI Chao,LI Yongming.Computation tree logic based on intuitionistic fuzzy measure.Journal of Frontiers of Computer Science and Technology,2017,11(9)：1523-1530.

10.3778/j.issn.1673-9418.1606020

*The National Natural Science Foundation of China under Grant No.61228305(國家自然科學(xué)基金);the Special Research Foundation of Department of Education of Shaanxi Province under Grant No.2015JK0605(陜西省教育廳專項科研計劃項目);the Science Foundation of Shangluo University under Grant No.15SKY001(商洛學(xué)院科研項目).

CNKI網(wǎng)絡(luò)優(yōu)先出版: 2016-08-19, http://www.cnki.net/kcms/detail/11.5602.TP.20160819.0932.002.html

摘 要：建立了直覺模糊Kripke結(jié)構(gòu)（intuitionistic fuzzy Kripke structure，IFKS）模型，提出了基于直覺模糊Kripke結(jié)構(gòu)的直覺模糊測度空間理論，闡述了IFKS的一系列性質(zhì)。證明了任一路徑轉(zhuǎn)移的直覺模糊可達度（intuitionistic fuzzy probability，IFP）為初始狀態(tài)的直覺模糊測度與各轉(zhuǎn)移的IFP所取下確界，任一狀態(tài)出發(fā)的所有路徑上路徑轉(zhuǎn)移的IFP為所有路徑可達度的上確界。給出了路徑轉(zhuǎn)移矩陣P及其傳遞閉包P+的概念，給出了通過計算路徑轉(zhuǎn)移矩陣傳遞閉包，計算路徑可達度的算法，并分析了算法的復(fù)雜度。提出了直覺模糊計算樹邏輯（intuitionistic fuzzy computation tree logic，IFPCTL）理論，討論了一組IFPCTL、可能測度計算樹邏輯（possibilistic computation tree logic，PoCTL）和經(jīng)典計算樹邏輯（computation tree logic，CTL）公式的等價性。最后給出了一組等價的IFPCTL和PoCTL公式以及一組不等價的IFPCTL和CTL公式。

李永明（1966—），男，陜西大荔人，1996年于四川大學(xué)獲得博士學(xué)位，1999年于西北工業(yè)大學(xué)博士后流動站出站，現(xiàn)為陜西師范大學(xué)教授、博士生導(dǎo)師，CCF高級會員，主要研究領(lǐng)域為計算智能，模糊系統(tǒng)分析，量子計算與量子邏輯等。