李 丹，李永明

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

廣義可能性計算樹邏輯和計算樹邏輯的關(guān)系*

李 丹，李永明+

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

Abstract:Generalized possibilistic computation tree logic(GPoCTL)plays an important role in model checking with uncertainty,there is still further research in its expressiveness.In order to study the expressiveness of GPoCTL,this paper discusses the relationship between GPoCTL and computation tree logic(CTL)with respect to their expressiveness.Firstly,this paper defines interval generalized possibilistic computation tree logic(IGPoCTL),and gives the definition of the equivalence between IGPoCTL formulae and CTL formulae,and proves that CTL is a proper subclass of IGPoCTL.Because IGPoCTL is obviously a simple crispness of GPoCTL,CTL can be regarded as a proper subclass of GPoCTL.Besides,this paper gives the definition ofα-equivalence between IGPoCTL formulae and CTL formulae and gets some more general results.

Key words:computation tree logic;generalized possibilistic computation tree logic;interval generalized possibilistic computation tree logic;expressiveness

廣義可能性計算樹邏輯（generalized possibilistic computation tree logic，GPoCTL）在不確定性模型檢測中扮演著非常重要的角色，但其表達(dá)能力還尚未研究全面。為此，討論了GPoCTL與計算樹邏輯（computation tree logic，CTL）表達(dá)能力之間的關(guān)系。首先定義了區(qū)間廣義可能性計算樹邏輯（interval generalized pos-sibilistic computation tree logic，IGPoCTL），并給出了IGPoCTL公式和CTL公式等價的定義。然后證明了CTL是IGPoCTL的一個真子類，因為IGPoCTL是GPoCTL的一種簡單分明化形式，則CTL可看作GPoCTL的一個真子類。此外，還給出了IGPoCTL公式和CTL公式α-等價的定義，并得出了一些更一般的結(jié)果。

計算樹邏輯；廣義可能性計算樹邏輯；區(qū)間廣義可能性計算樹邏輯；表達(dá)能力

1 引言

模型檢測[1-4]是一種形式化的自動驗證技術(shù)，它主要由以下3步組成：（1）抽象出系統(tǒng)的數(shù)學(xué)模型；（2）對需要驗證的屬性進(jìn)行形式化描述；（3）通過模型檢測算法來驗證系統(tǒng)是否滿足該屬性，若滿足，則返回“是”；若不滿足，將會給出一個反例。模型檢測現(xiàn)已被廣泛地應(yīng)用于計算機系統(tǒng)的設(shè)計和分析中[5-6]。

1986年Hart和Sharir[7]提出了將概率理論應(yīng)用到系統(tǒng)的模型檢測中；Baier和Katoen[2]在此基礎(chǔ)上，介紹了以馬爾科夫鏈為模型的基于概率測度的模型檢測。隨后，一些學(xué)者提出在狀態(tài)模型中引入更多的量化信息，如在模型中引入統(tǒng)計信息[8]或者多值信息[9-10]，以及在狀態(tài)中引入時間信息[2]。1965年Zadeh提出了模糊集理論[11-13]，并引入可能性測度的概念。李永明等人率先將可能性測度與模型檢測結(jié)合，提出了基于可能性測度的模型檢測[14-17]；但它具有極大的局限性，為了解決更一般的不確定性問題，又進(jìn)一步提出了基于廣義可能性測度的模型檢測[18-19]，目前該理論還在不斷完善中。

模型檢測需要將系統(tǒng)屬性形式化地描述為不同的邏輯公式。對于這些邏輯公式，它們的表達(dá)能力不同，采用表達(dá)能力強的邏輯公式能夠拓廣模型檢測的適用范圍。然而，對于廣義可能性計算樹邏輯（generalized possibilistic computation tree logic，GPoCTL）的表達(dá)能力的研究尚不全面，文獻(xiàn)[19]比較了GPoCTL和可能性計算樹邏輯（possibilistic computation tree logic，PoCTL）的表達(dá)能力，并得出GPoCTL的表達(dá)能力強于PoCTL。本文定義了IGPoCTL，并比較了IGPoCTL和CTL的表達(dá)能力。

本文組織結(jié)構(gòu)如下：第2章介紹了一些基本概念；第3章比較了IGPoCTL和CTL的表達(dá)能力；第4章總結(jié)全文。

2 預(yù)備知識

本章給出經(jīng)典計算樹邏輯和基于廣義可能性測度下計算樹邏輯的概念，包括Kripke結(jié)構(gòu)、CTL的語構(gòu)和語義、廣義可能性Kripke結(jié)構(gòu)和GPoCTL的語構(gòu)和語義等。

定義1[2]一個Kripke結(jié)構(gòu)（Kripke structure，KS)M=(S,→,I,AP,L)是一個五元組，其中：

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

（2）→?S×S是狀態(tài)轉(zhuǎn)移關(guān)系，并且要求→是全關(guān)系，即對任意s∈S,存在t∈S,使得(s,t)∈→;

（3）I?S是初始狀態(tài)的集合；

（4）AP是原子命題的集合；

（5）L:S→2AP是狀態(tài)的標(biāo)簽函數(shù)，表明每個狀態(tài)s所滿足的原子命題的集合。

定義2[2]（CTL的語構(gòu)）CTL狀態(tài)公式按照如下規(guī)則定義：

其中，φ是CTL路徑公式，a∈AP。

CTL路徑公式按照如下規(guī)則定義：

其中，Φ、Φ1和Φ2是CTL狀態(tài)公式。

定義3[2]（CTL的語義）設(shè)M=(S,→,I,AP,L)是一個KS，a∈AP,s∈S,Φ1和Φ2是CTL狀態(tài)公式，φ是CTL路徑公式，π=s0s1s2…是M中的任意一條路徑，對任意的i≥0,記π[i]=si。則狀態(tài)公式的滿足關(guān)系定義為：

路徑公式的滿足關(guān)系定義為：

定義4[2]對于a∈AP,存在范式（existential normal form，ENF）的CTL狀態(tài)公式定義如下：

定義5[19]一個廣義可能性Kripke結(jié)構(gòu)（generalized possibilistic Kripke structure，GPKS）M=(S,P,I,AP,L)是一個五元組，其中：

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

（2）P:S×S→[0,1]是可能性轉(zhuǎn)移分布函數(shù)；

（3）I:S→[0,1]是可能性初始分布函數(shù)；

（4）AP是原子命題的集合；

（5）L:S×AP→[0,1]是可能性標(biāo)簽函數(shù)，若a∈AP,s∈S,則L(s,a)表示狀態(tài)s滿足原子命題a的可能程度。

若S和AP都是有限的，則M是有限的GPKS。

進(jìn)一步，對任意的E?Paths(M),定義PoM(E)=∨{PoM(π)|π∈E},則可得擴張映射PoM:2Paths(M)→[0,1],并明的，即L:S×AP→{0,1}，則M為GPKS[15-16]，并稱M是正規(guī)的。這里，∨和∧分別表示實數(shù)的上下確界。

（2)對于GPKSM，從狀態(tài)s出發(fā)的一條路徑可以用一組無限的狀態(tài)序列來表示，即s0s1s2…,其中s0=s,以及?i≥0,都有P(si,si+1)＞0;從狀態(tài)s出發(fā)的一條有限路徑可以用一組有限的狀態(tài)序列來表示，即s0s1s2…sn,其中s0=s,n≥0,以及對任意的0≤i≤n-1,有P(si,si+1)＞0。Paths(s)是從狀態(tài)s出發(fā)的所有路徑所組成的集合；而Pathsfin(s)是從狀態(tài)s出發(fā)的所有有限路徑所組成的集合。Paths(M)是M中所有路徑所組成的集合；而Pathsfin(M)是M中所有有限路徑所組成的集合。

定義6[19]設(shè)M是一個GPKS，定義映射PoM:Paths(M)→[0,1]，對任意的π=s0s1s2…∈Paths(M),有稱PoM是Ω=2Paths(M)上的廣義可能性測度。若M是明確的，則PoM可簡記為Po。

注2可能性測度[15]除了滿足以上條件外，還需滿足Po(Paths(M))=1。

定義7[19]（GPoCTL的語構(gòu)）GPoCTL狀態(tài)公式按如下規(guī)則定義：

其中，a∈AP，φ是GPoCTL路徑公式。

GPoCTL路徑公式按如下規(guī)則定義：

其中，Φ、Φ1和Φ2是GPoCTL狀態(tài)公式，且n∈N。

定義8[19]（GPoCTL的語義）設(shè)M=(S,P,I,AP,L)是一個GPKS，a∈AP,s∈S,Φ和Ψ是GPoCTL狀態(tài)公式，φ是GPoCTL路徑公式。狀態(tài)公式Φ的語義是一個模糊集||Φ||:S→[0,1]，遞歸定義如下：

對于π∈Paths(M),路徑公式φ的語義是一個模糊集||φ||:Paths(M)→[0,1]，遞歸定義如下：

路徑公式?Φ（“最終”）定義為?Φ=true?Φ,其語義為：

3 IGPoCTL與CTL表達(dá)能力的比較

首先定義了IGPoCTL，并給出IGPoCTL公式和CTL公式等價的定義，然后比較了IGPoCTL和CTL的表達(dá)能力。此外，還給出了IGPoCTL公式和CTL公式等價的另一種定義。

定義9（IGPoCTL的語構(gòu)）IGPoCTL狀態(tài)公式按照如下規(guī)則定義：

其中，a∈AP,φ是IGPoCTL路徑公式，J?[0,1]是一個區(qū)間。

IGPoCTL路徑公式按照如下規(guī)則定義：

其中，Φ、Φ1和Φ2是IGPoCTL狀態(tài)公式，且n∈N。

定義10（IGPoCTL的語義）假設(shè)M=(S,P,I,AP,L)是一個GPKS，a∈AP,J?[0,1]是一個區(qū)間，s∈S,Φ1和Φ2是IGPoCTL狀態(tài)公式，φ是IGPoCTL路徑公式，π=s0s1s2…是M中的任意一條路徑，對任意的i≥0,記π[i]=si,則狀態(tài)公式的滿足關(guān)系定義為：

路徑公式的滿足關(guān)系定義為：

3.1 IGPoCTL公式和CTL公式等價的定義

定義11設(shè)M是一個有限的GPKS，S是狀態(tài)空間，Φ是IGPoCTL狀態(tài)公式，則狀態(tài)公式Φ的滿足集為。若M是明確的，則SatM(Φ)也可以簡記為Sat(Φ)。

定義12設(shè)Φ1和Φ2是兩個IGPoCTL狀態(tài)公式，如果對任意的有限GPKSM,都有Sat(Φ1)=Sat(Φ2),則稱Φ1和Φ2是等價的，記作Φ1≡Φ2。

定義13設(shè)Φ是IGPoCTL狀態(tài)公式，Ψ是CTL狀態(tài)公式，如果對任意的有限GPKSM=(S,P,I,AP,L),都有SatM(Φ)=SatTS(M)(Ψ)，則稱Φ和Ψ是等價的，記作Φ≡Ψ。其中，TS(M)=(S,→,I′,AP,L′),?s,s′∈S,s→s′當(dāng)且僅當(dāng)P(s,s′)＞0;s∈I′當(dāng)且僅當(dāng)I(s)＞0;?a∈AP,a∈L′(s)當(dāng)且僅當(dāng)L(s,a)＞0。明顯地，PathsM(s)=PathsTS(M)(s),下面都會記作Paths(s)。

定義14 ENF形式的CTL狀態(tài)公式Φ的長度記為[Φ]，表示Φ中子公式的個數(shù)，定義如下：

定理1設(shè)p∈[0,1]，φ是任意的IGPoCTL路徑公式，則Po＜p(φ)≡?Po≥p(φ)。

證明 設(shè)p∈[0,1],對任意的有限GPKSM=(S,P,I,AP,L)，有：

3.2 CTL是IGPoCTL的子類

定理2[2]對任意的CTL公式，都存在一個ENF形式的CTL公式與其等價。

定理3對任意ENF形式的CTL公式Φ，都存在一個IGPoCTL公式Φ′與其等價，即Φ≡Φ′。

證明 設(shè)M是任意一個有限的GPKS，通過對公式Φ的長度進(jìn)行歸納來證明：

（1）Φ=true，取Φ′=true。

（2）Φ=a,取Φ′=a＞0。下證a≡a＞0。因為sTS(M)a當(dāng)且僅當(dāng)a∈L′(s),當(dāng)且僅當(dāng)L(s,a)＞0,當(dāng)且僅當(dāng)sMa＞0,所以a≡a＞0。

（3）Φ=?φ，其中φ=○Φ|?Φ|□Φ|Φ1?Φ2，由歸納假設(shè)，存在IGPoCTL狀態(tài)公式Φ1′和Φ2′，使得Φ1≡Φ1′,Φ2≡Φ2′。取Φ′=Po＞0(φ′)，其中，φ′=○Φ′|?Φ′|□Φ′|Φ1′?Φ2′。下證?φ≡Po＞0(φ′)。即需要證明SatTS(M)(?φ)=SatM(Po＞0(φ′))。其中,SatTS(M)(?φ)={s|?π∈Paths(s),πφ},SatM(Po＞0(φ′))={s|Po(sφ′)＞0},而Po(sφ′)=∨{PoMs(π)|π∈Paths(s),πφ′}。

假設(shè)s∈SatTS(M)(?φ)，則在TS(M)中，存在路徑π,使得π∈Paths(s)且πφ。因為M是有限的，相應(yīng)地，在M中有PoMs(π)＞0和πφ′,從而∨{PoMs(π)|π∈Paths(s),πφ′}＞0,即Po(sφ′)＞0，則s∈SatM(Po＞0(φ′)),所以SatTS(M)(?φ)?SatM(Po＞0(φ′))。

假設(shè)s∈SatM(Po＞0(φ′)),則s滿足Po(sφ′)＞0，即∨{PoMs(π)|π∈Paths(s),πφ′}＞0.因為M是有限的，則存在路徑π,使得π∈Paths(s),PoMs(π)＞0和πφ′。相應(yīng)地，在TS(M)中，有π∈Paths(s)和πφ，則s∈SatTS(M)(?φ)，所以SatM(Po＞0(φ′))?SatTS(M)(?φ)。

綜上所述，SatTS(M)(?φ)=SatM(Po＞0(φ′)),則?φ≡Po＞0(φ′)。

（4）Φ=Φ1∧Φ2。由歸納假設(shè)，存在IGPoCTL狀態(tài)公式Φ1′和Φ2′,使得Φ1≡Φ1′,Φ2≡Φ2′。取Φ′=Φ1′∧Φ2′。下證Φ1∧Φ2≡Φ1′∧Φ2′。因為sTS(M)Φ1∧Φ2當(dāng)且僅當(dāng)sTS(M)Φ1且sTS(M)Φ2,當(dāng)且僅當(dāng)sMΦ1′且sMΦ2′，當(dāng)且僅當(dāng)sMΦ1′∧Φ2′,所以Φ1∧Φ2≡Φ1′∧Φ2′。

（5）Φ=?Φ1。由歸納假設(shè)，存在IGPoCTL狀態(tài)公式Φ1′,使得Φ1≡Φ1′,取Φ′=?Φ1′。下證?Φ1≡?Φ1′。因為sTS(M)?Φ1當(dāng)且僅當(dāng)sTS(M)Φ1,當(dāng)且僅當(dāng)sMΦ1′,當(dāng)且僅當(dāng)sM?Φ1′,所以?Φ1≡?Φ1′。

綜上所述，對任意ENF形式的CTL公式Φ，都存在一個IGPoCTL公式Φ′與其等價。

注3若CTL路徑公式φ中還含有存在量詞?，則與其等價的IGPoCTL公式都需將其變?yōu)镻o＞0的形式。

例1如下ENF形式的CTL公式：?(?○(?(a??○b))∧??a∧?a)，其中a,b∈AP，存在與其等價的IGPoCTL公式，具體如下：

由定理3，可得如下等價式（若CTL狀態(tài)公式是Φ，則與其等價的IGPoCTL狀態(tài)公式記作Φ′）。

命題1如下具有存在量詞?的CTL狀態(tài)公式等價于相應(yīng)的IGPoCTL狀態(tài)公式：

命題2如下具有任意量詞?的CTL狀態(tài)公式等價于相應(yīng)的IGPoCTL狀態(tài)公式：

注4在上述推論中，有的式子在無限的GPKS中不成立。下面舉出命題2（1）的一個反例。假設(shè)命題2（1）對任意的無限GPKSM=(S,P,I,AP,L)都滿足，即?s∈S,要么s滿足?○Φ和Po=0(○?Φ′)，要么都不滿足。取Φ=a∈AP。如圖1，通過計算可得Po(s0○?a＞0)=∨{PoMs0(π)|π∈Paths(s0),π○?a＞0}=0,則s0∈SatM(Po=0(○?a＞0))。但是s0ts1s2…○?a＞0，則s0?SatTS(M)(?○a)。從而可得SatM(Po=0(○?a＞0))≠SatTS(M)(?○a),即?○a?Po=0(○?a＞0)。

結(jié)合定理2和定理3，可得如下定理。

定理4對任意的CTL公式，都存在一個IGPoCTL公式與其等價。

定理4說明：CTL是IGPoCTL的子類。

3.3 CTL是IGPoCTL的一個真子類

定理5不存在CTL公式與IGPoCTL公式Po=1(○a＞0)等價。

證明 假設(shè)存在CTL公式Φ,使得Φ≡Po=1(○a＞0)。圖2和圖3是兩個有限的GPKSM1和M2。對M1而言，Po(s0○a＞0)=∨{Po

M1s0(π)|π○a＞0}=Po(s0s1s3ω)=1;對M2而言，Po(s0○a＞0)=Po(s0s1s3ω)=0.8。因此，s0∈SatM1(Po=1(○a＞0)),而s0?SatM2(Po=1(○a＞0)),則可得：

Fig.1 An infinite GPKSM圖1 無限的GPKSM

因為Φ是一個CTL公式，且TS(M1)=TS(M2)，則

但假設(shè)Φ≡Po=1(○a＞0)，即對任意的有限 GPKSM，都有SatTS(M)(Φ)=SatM(Po=1(○a＞0))成立。則對M1，有SatTS(M1)(Φ)=SatM1(Po=1(○a＞0));對M2,有SatTS(M2)(Φ)=SatM2(Po=1(○a＞0))。結(jié)合等式（2），則有：

Fig.2 Afinite GPKSM1圖2 有限的GPKSM1

Fig.3 Afinite GPKSM2圖3 有限的GPKSM2

由上可知，等式（1）和等式（3）存在矛盾，故假設(shè)不成立，即不存在CTL公式與IGPoCTL公式Po=1(○a＞0)等價。

由定理4和定理5可得：CTL是IGPoCTL的一個真子類，因為IGPoCTL是GPoCTL的一種簡單分明化形式，則CTL可看作GPoCTL的一個真子類。

采用和定理5類似的證明方法可以得到如下定理。

定理6不存在CTL公式與IGPoCTL公式Po＜1(○a＞0)等價。

定理7不存在CTL公式與IGPoCTL公式Po=1(?a＞0)等價。

定理8不存在CTL公式與IGPoCTL公式Po=1(□a＞0)等價。

定理9不存在CTL公式與IGPoCTL公式Po＜1(a＞0?b＞0)等價。

定理10不存在CTL公式與IGPoCTL公式a=1和a＜1等價。

3.4 IGPoCTL公式和CTL公式等價的另一種定義

定義15設(shè)Φ是IGPoCTL狀態(tài)公式，Ψ是CTL狀態(tài)公式，α∈(0,1]，如果對任意的有限GPKSM=(S,P,I,AP,L),都有SatM(Φ)=SatTSα(M)(Ψ)，則稱Φ和Ψ是α-等價的，記作Φ≡αΨ。其中，TSα(M)=(S,→α,Iα,AP,Lα)，?s,s′∈S，s→αs′當(dāng)且僅當(dāng)P(s,s′)≥α;s∈Iα當(dāng)且僅當(dāng)I(s)≥α;?a∈AP,a∈Lα(s)當(dāng)且僅當(dāng)L(s,a)≥α。明顯地，PathsM(s)=PathsTSα(M)(s),下面都會記作Paths(s)。

命題3設(shè)α∈(0,1]，對任意的CTL公式都存在一個IGPoCTL公式與其α-等價。

例2對于例1中的CTL公式，存在與其α-等價的IGPoCTL公式，具體如下：

命題4設(shè)α∈(0,1]，如下具有存在量詞?的CTL狀態(tài)公式α-等價于相應(yīng)的IGPoCTL狀態(tài)公式：

命題6設(shè)α∈(0,1]，不存在CTL公式與IGPoCTL公式a=0.5α-等價。

由命題3和命題6可得：設(shè)α∈(0,1],在α-等價的情況下，CTL是IGPoCTL的一個真子類。

注5若采用3.2節(jié)中的等價定義，根據(jù)定理3有?φ≡Po＞0(φ′)。可知：當(dāng)某一事件的可能性大于0時，則與該事件相對應(yīng)的事件存在。若采用1-等價，則會出現(xiàn)這種情況：當(dāng)某一事件的可能性大于0時，并不意味著與該事件相對應(yīng)的事件存在。例如：對于圖3，有Po(s0○a=1)=0＜1,則s0Po=1(○a=1)。根據(jù)命題 4（1），若取α=1（即采用1-等價），則能推出s0?○a。但顯然有s0?○a。

命題5設(shè)α∈(0,1]，如下具有任意量詞?的CTL狀態(tài)公式α-等價于相應(yīng)的IGPoCTL狀態(tài)公式：

4 總結(jié)

本文定義了IGPoCTL，給出了IGPoCTL公式和CTL公式等價的定義，證明了對任意的CTL公式都存在與其等價的IGPoCTL公式，但對任意的IGPoCTL公式不一定都存在與其等價的CTL公式，即CTL是IGPoCTL的一個真子類。最后給出了IGPoCTL公式和CTL公式α-等價的定義，并得出了更一般的結(jié)果。本文結(jié)論進(jìn)一步揭示了GPoCTL的表達(dá)能力。

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

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

[3]Clark E M,Grumberg O,Long D E.Model checking and abstraction[J].ACM Transactions on Programming Languages and Systems,1994,16(5):1512-1542.

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

[5]Cao Yongzhi,Ying Mingsheng.Observability and decentralized control of fuzzy discrete event systems[J].IEEE Transactions on Fuzzy Systems,2006,14(2):202-216.

[6]Clarke E M,Emerson E A,Sistla A P.Automatic verification of finite state concurrent systems using temporal logic specifications[J].ACM Transactions on Programming Languages and Systems,1986,8(2):244-263.

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

[8]Fischer D,Gr?del E,Kaiser ?.Model checking games for the quantitativeμ-calculus[J].Theory of Computing Systems,2010,47(3):696-719.

[9]Chechik M,Devereux B,Easterbrook S,et al.Multi-valued symbolic model-checking[J].ACM Transactions on Software Engineering and Methodology,2003,12(4):371-408.

[10]Lei Lihui,Duan Zhenhua.An extended deterministic finite automata based on possibility measure[J].Journal of Software,2007,18(12):2980-2990.

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

[12]Klir G J,Folger T A.Fuzzy sets,uncertainty and information[M].Englewood Cliffs,USA:Prentice Hall,1988.

[13]Dubois D J.Fuzzy sets and systems:theory and application[M].New York:Academic Press,1980.

[14]Li Yongming.Analysis of fuzzy systems[M].Beijing:Science Press,2005.

[15]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.

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

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

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

[19]Li Yongming,Ma Zhanyou.Quantitative computation tree logic model checking based on generalized possibility measures[J].IEEE Transactions on Fuzzy Systems,2015,23(6):2034-2047.

附中文參考文獻(xiàn)：

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

[10]雷麗暉,段振華.一種基于擴展有限自動機驗證組合Web服務(wù)的方法[J].軟件學(xué)報,2007,18(12):2980-2990.

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

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

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

Relationship Between Generalized Possibilistic Computation Tree Logic and Computation Tree Logic*

LI Dan,LI Yongming+
College of Computer Science,Shaanxi Normal University,Xi'an 710119,China

A

TP301.2

+Corresponding author:E-mail:liyongm@snnu.edu.cn

LI Dan,LI Yongming.Relationship between generalized possibilistic computation tree logic and computation tree logic.Journal of Frontiers of Computer Science and Technology,2017,11(10)：1681-1688.

ISSN 1673-9418 CODEN JKYTA8

Journal of Frontiers of Computer Science and Technology

1673-9418/2017/11(10)-1681-08

10.3778/j.issn.1673-9418.1607030

E-mail:fcst@vip.163.com

http://www.ceaj.org

Tel:+86-10-89056056

*The National Natural Science Foundation of China under Grant Nos.11271237,61228305(國家自然科學(xué)基金).

Received 2016-06,Accepted 2016-08.

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

LI Dan was born in 1991.She is an M.S.candidate at Shaanxi Normal University.Her research interest is model checking.

李丹（1991—），女，山西平陸人，陜西師范大學(xué)碩士研究生，主要研究領(lǐng)域為模型檢測。

LI Yongming was born in 1966.He received 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 logic and quantum computing,etc.

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