朱 曄，袁紅娟,+，錢(qián)俊彥，潘海玉

1.泰州學(xué)院 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，江蘇 泰州 225300

2.桂林電子科技大學(xué) 廣西可信軟件重點(diǎn)實(shí)驗(yàn)室，廣西 桂林 541004

1 引言

模型檢測(cè)[1-3]是一種驗(yàn)證安全攸關(guān)反應(yīng)式系統(tǒng)關(guān)鍵性質(zhì)的自動(dòng)化技術(shù)。其中系統(tǒng)的行為用Kripke結(jié)構(gòu)來(lái)描述，而系統(tǒng)的性質(zhì)則用時(shí)態(tài)邏輯[1-3]公式來(lái)描述，通過(guò)遍歷Kripke結(jié)構(gòu)的狀態(tài)空間來(lái)驗(yàn)證性質(zhì)是否成立。用模型檢測(cè)對(duì)具有模糊不確定性信息的系統(tǒng)進(jìn)行驗(yàn)證，即稱(chēng)為模糊模型檢測(cè)。模糊模型檢測(cè)是經(jīng)典模型檢測(cè)理論的延伸和推廣。近年來(lái)，模糊模型檢測(cè)引起了學(xué)術(shù)界和工業(yè)界的廣泛關(guān)注，并取得了較大的發(fā)展。

模糊模型檢測(cè)技術(shù)首先由加拿大學(xué)者Chechik等人[4]于2003年提出。他們研究了基于De Morgan代數(shù)的計(jì)算樹(shù)邏輯的模型檢測(cè)問(wèn)題并設(shè)計(jì)出模型檢測(cè)工具[5]。以色列學(xué)者Shoham和Grumberg[6]探討了具有相同代數(shù)結(jié)構(gòu)的μ-演算的模型檢測(cè)問(wèn)題。最近，基于抽象和精化思想，Meller、Shoham、Grumberg[7]解決了有限D(zhuǎn)e Morgan代數(shù)的μ-演算的組合模型檢測(cè)問(wèn)題[8]。我國(guó)學(xué)者在模糊模型檢測(cè)問(wèn)題的研究方面做了很多工作。李永明等人[9-11]結(jié)合模糊理論中的可能性測(cè)度及模型檢測(cè)技術(shù)，提出廣義可能性模型檢測(cè)方法。潘海玉等人[12-13]研究了基于任意模糊邏輯的計(jì)算樹(shù)邏輯的模型檢測(cè)問(wèn)題及取值于任意有限格的計(jì)算樹(shù)邏輯的模型檢測(cè)問(wèn)題。

目前的模糊模型檢測(cè)技術(shù)主要適用于模糊封閉式系統(tǒng)的驗(yàn)證，即模糊系統(tǒng)的行為由系統(tǒng)本身的當(dāng)前狀態(tài)決定，與系統(tǒng)的工作環(huán)境無(wú)關(guān)。為了對(duì)模糊開(kāi)放系統(tǒng)使用模糊模型檢測(cè)技術(shù)，即模糊系統(tǒng)的行為不僅受到系統(tǒng)內(nèi)部狀態(tài)的制約，同時(shí)受到外部環(huán)境交互的影響。文獻(xiàn)[14]將Rlur等人提出的并發(fā)博弈結(jié)構(gòu)CGS（concurrent game structure）和它的規(guī)范語(yǔ)言交互時(shí)態(tài)邏輯ATL[15]（alternating-time temporal logic）推廣到模糊情形下，用不動(dòng)點(diǎn)迭代算法解決所獲得的邏輯的模型檢測(cè)問(wèn)題。值得一提的是，ATL已經(jīng)被用于多智能體系統(tǒng)[16]、電子商務(wù)業(yè)務(wù)流[17]，以及概率開(kāi)放系統(tǒng)[18]等的分析驗(yàn)證。

本文的研究任務(wù)是文獻(xiàn)[14]工作的延續(xù)。首先通過(guò)將模糊交互時(shí)態(tài)邏輯的模型檢測(cè)問(wèn)題轉(zhuǎn)化為有限個(gè)經(jīng)典的交互時(shí)態(tài)邏輯的模型檢測(cè)問(wèn)題，從而將模糊交互時(shí)態(tài)邏輯的模型檢測(cè)可以轉(zhuǎn)化為使用經(jīng)典的時(shí)態(tài)交互邏輯的模型檢測(cè)算法來(lái)解決，進(jìn)一步分析了模糊交互時(shí)態(tài)邏輯的模型檢測(cè)問(wèn)題的不動(dòng)點(diǎn)迭代算法的時(shí)間復(fù)雜性。最后研究了模糊交互時(shí)態(tài)邏輯語(yǔ)義的連續(xù)性問(wèn)題，即模糊并發(fā)博弈結(jié)構(gòu)發(fā)生微小變化時(shí)，模糊交互時(shí)態(tài)邏輯的語(yǔ)義是否也相應(yīng)地發(fā)生微小的變化。

與本文工作最相關(guān)的是廣義可能性計(jì)算樹(shù)邏輯的模型檢測(cè)問(wèn)題[9-11]的研究。廣義可能性計(jì)算樹(shù)邏輯用可能性算子 GPo（generalized possibility operator）取代計(jì)算樹(shù)邏輯的路徑全稱(chēng)量詞和路徑存在量詞。為了解決廣義可能性計(jì)算樹(shù)邏輯的模型檢測(cè)問(wèn)題，文獻(xiàn)[11]利用截集的方法，將廣義可能性計(jì)算樹(shù)邏輯的模型檢測(cè)問(wèn)題規(guī)約為經(jīng)典的計(jì)算樹(shù)邏輯模型檢測(cè)，給出了解決廣義可能性計(jì)算樹(shù)邏輯的模型檢測(cè)問(wèn)題的算法及其計(jì)算復(fù)雜度。

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

本章將回顧模糊并發(fā)博弈結(jié)構(gòu)和模糊交互時(shí)態(tài)邏輯的語(yǔ)法和語(yǔ)義。在正式引入模糊交互時(shí)態(tài)邏輯的語(yǔ)法和語(yǔ)義之前，給出一些記號(hào)。后文用N表示自然數(shù)集合，用S+表示有限狀態(tài)序列集合。設(shè)X是經(jīng)典集合，則函數(shù)F:X→[0,1]成為集合X上的模糊集合。若X是有限集合，||X表示集合X中的元素個(gè)數(shù)。設(shè)A和B是X上兩個(gè)模糊集合，后文用A?B表示A(x)≤B(x)，x∈X。

定義1[14]（模糊并發(fā)博弈結(jié)構(gòu)）模糊并發(fā)博弈結(jié)構(gòu)（fuzzy concurrent game structure，F(xiàn)CGS）是六元組：

M=(n,S,AP,V,d,δ)其中：

（1）n是系統(tǒng)中智能體的數(shù)目，用自然數(shù)1,2,…,n來(lái)指代每個(gè)智能體，用Σ表示智能體集合{1,2,…,n}。

（2）S是有限狀態(tài)集。

（3）AP是有限原子命題集合。

（4）V:S×AP→[0,1]是模糊賦值函數(shù)，狀態(tài)s∈S，原子命題p∈AP，V(s,p)表示狀態(tài)s下，滿足原子命題p的真值。

（5）da(s)表示系統(tǒng)在狀態(tài)為s下，智能體a可用的非空動(dòng)作集合，這里，a∈Σ，s∈S。＜j1,j2,…,jn>表示系統(tǒng)在狀態(tài)s下，智能體集合Σ可采取的一個(gè)動(dòng)作向量，其中，ja∈da(s)。同時(shí)，定義動(dòng)作向量集D(s)=d1(s)×d2(s)×…×dn(s)。

（6）δ是狀態(tài)遷移函數(shù)，表示系統(tǒng)在動(dòng)作向量＜j1,j2,…,jn>∈D(s)的作用下，從狀態(tài)s遷移到下一個(gè)狀態(tài)δ(s,j1,j2,…,jn)。

注意到，經(jīng)典的并發(fā)博弈結(jié)構(gòu)是一種特殊的FCGS，因?yàn)槿鬎CGSM的模糊賦值函數(shù)的值域限制為{0,1}，則M為經(jīng)典的并發(fā)博弈結(jié)構(gòu)。若沒(méi)有特別說(shuō)明，后文用M表示一個(gè)FCGS。

智能體a的策略fa是一個(gè)函數(shù)fa:S+→Ν：如果λ的最后狀態(tài)為s，則fa(λ)∈da(s)。{fa|a∈A}為A的聯(lián)盟策略，記作FA。另外，記ΠA為A的所有的聯(lián)盟策略之集。令FA∈ΠA。用out(s,FA)表示聯(lián)盟體A遵循聯(lián)盟策略FA得到的所有源自s的路徑集合。換句話說(shuō)，若λ=s0s1s2…∈out(s,FA)當(dāng)且僅當(dāng)s0=s，且對(duì)于任意i≥ 0，存在動(dòng)作向量 ＜j1,j2,…,jn>∈D(si)，使得任意a∈A，ja=fa(λ(0,i))，δ(si,j1,j2,…,jn)=si+1。這里用λ(i)，λ(0,i)，λ(i,∞)分別表示狀態(tài)路徑λ的第i個(gè)狀態(tài)、λ的有限前綴和λ的無(wú)限后綴。

下面給出用于描述FCGS性質(zhì)的模糊交互時(shí)態(tài)邏輯的語(yǔ)法和語(yǔ)義。

定義2[14]（FATL語(yǔ)法）原子命題集合AP上的模糊交互時(shí)態(tài)邏輯（fuzzy alternating-time temporal logic，F(xiàn)ATL）公式定義如下：

其中，p∈AP，A?Σ。

定義3（FATL語(yǔ)義）設(shè)φ為FATL公式，M=(n,S,AP,V,d,δ)是FCGS，φ在M上的語(yǔ)義定義如下：對(duì)于任意狀態(tài)s，有

從上述定義不難看出，F(xiàn)ATL的語(yǔ)法和經(jīng)典ATL的語(yǔ)法是完全一致的，它們的區(qū)別主要表現(xiàn)在其語(yǔ)義上。

值得一提的是，若定義3中的語(yǔ)義模型FCGS就是經(jīng)典的并發(fā)博弈結(jié)構(gòu)，那么FATL的語(yǔ)義與ATL的語(yǔ)義是一致的。若M是經(jīng)典的并發(fā)博弈結(jié)構(gòu)，常用M,s╞φ表示||φ||(M,s)=1。當(dāng)上下文明確時(shí)，常省略M。

命題1[14]設(shè)M=(n,S,AP,V,d,δ)是FCGS。φ1、φ2、φ為FATL公式，Y是S上的一個(gè)模糊集合，函數(shù)E、F分別定義如下：

其中，s∈S。則 ||＜＜A>>φ1Uφ2||和||＜＜A>>Gφ||分別是E(Y)和F(Y)的最小和最大不動(dòng)點(diǎn)。

3 模型檢測(cè)

本章通過(guò)將FATL的模型檢測(cè)問(wèn)題轉(zhuǎn)換為有限個(gè)ATL的模型檢測(cè)問(wèn)題，進(jìn)而可利用ATL的模型檢測(cè)法來(lái)解決FATL的模型檢測(cè)問(wèn)題。FATL的模型檢測(cè)問(wèn)題是指：對(duì)于給定的FCGSM，狀態(tài)s∈S及FATL公式φ，計(jì)算||φ||(s)的值。在正式討論FATL的模型檢測(cè)問(wèn)題之前，引入一些記號(hào)。

設(shè)φ是FATL公式，公式φ的長(zhǎng)度，記作|φ|，歸納定義為：

模型FCGSM的規(guī)模大小為：

定義4（閾值為α的并發(fā)博弈結(jié)構(gòu)）設(shè)M=(n,S,AP,V,d,δ)是一個(gè)FCGS，對(duì)任意的α∈[0,1]，構(gòu)造一個(gè)并發(fā)博弈結(jié)構(gòu)Mα為：

其中，Vα(s)={p:V(s,p)≥α,p∈AP}。

引理1設(shè)φ是不包含?連接詞的任意FATL公式，M是一個(gè)FCGS，則對(duì)任意的α∈[0,1]以及M中的任意狀態(tài)s，||φ||(M,s)≥α當(dāng)且僅當(dāng)Mα,s╞φ。

證明采用結(jié)構(gòu)歸納法證明。

（1）當(dāng)φ=true時(shí)，||true||(M,s)=1≥α?Mα,s╞true。

（2）當(dāng)φ=p，p∈AP時(shí)，由Mα的定義知，||p||(M,s)≥α?Mα,s╞p。

（3）當(dāng)φ=φ1∨φ2時(shí)，由歸納假設(shè)知：

（4）當(dāng)φ=＜＜A>>Xφ1時(shí)，由歸納假設(shè)知：

?在M中存在一個(gè)策略FA∈ΠA，對(duì)于任意的λ∈out(s,FA)，有 ||φ1||(λ(1))≥α

?在Mα中存在一個(gè)策略FA∈ΠA，對(duì)于任意的λ∈out(s,FA)，有Mα,λ(1)╞φ1

（5）當(dāng)φ=＜＜A>>φ1Uφ2時(shí)，由歸納假設(shè)，定義3和定義4知：

?在M中存在一個(gè)策略FA∈ΠA，對(duì)于任意的λ∈out(s,FA)，存在一個(gè)i∈N 使得||φ2||(λ(i))≥α且對(duì)于任意的j,0 ≤j＜i，||φ1||(λ(j))≥α

?在Mα中存在一個(gè)策略FA∈ΠA，對(duì)于任意的λ∈out(s,FA)，存在一個(gè)i∈N使得Mα,λ(i)╞φ2且對(duì)于任意的j,0≤j＜i，

（6）當(dāng)φ=＜＜A>>Gφ1時(shí)，由歸納假設(shè)，定義3和定義4知：

?在M中存在一個(gè)策略FA∈ΠA，對(duì)于任意的λ∈out(s,FA)和i∈N，||φ1||(M,λ(i))≥α

?在Mα中存在一個(gè)策略FA∈ΠA，對(duì)于任意的λ∈out(s,FA)和i∈N，Mα,λ(i)╞φ1

根據(jù)以上結(jié)論，下面定理1的證明過(guò)程給出了將FATL的模型檢測(cè)問(wèn)題轉(zhuǎn)換為經(jīng)典的ATL的模型檢測(cè)的方法。

定理1（時(shí)間復(fù)雜度）設(shè)φ是任意的FATL公式，M是一個(gè)FCGS，則對(duì)任意狀態(tài)s，計(jì)算||φ||(s)的時(shí)間復(fù)雜度是O(|φ|·|M|·|S|·|AP|)。

證明若φ=?φ1，根據(jù)定義2，可先通過(guò)計(jì)算||φ1||(s)，然后求 ||φ||(s)=1-||φ1||(s)。由引理 1 知，若φ不包含?連接詞的FATL公式，則對(duì)任意狀態(tài)s有||φ||(s)=max{α∈Im(M):Mα,s╞φ}，這里Im(M)={V(s,p):s∈S,p∈AP}?{1-V(s,p):s∈S,p∈AP}。因此 FATL 的模型檢測(cè)問(wèn)題可轉(zhuǎn)換為至多|Im(M)|個(gè)ATL的模型檢測(cè)問(wèn)題。注意到經(jīng)典的ATL的模型檢測(cè)問(wèn)題能在O(|φ|×|M|)時(shí)間內(nèi)解決。因此計(jì)算||φ||(s)的時(shí)間復(fù)雜度是O(|φ|× |M|× |S|× |AP|)。

通過(guò)下面的例子解釋如何將FATL的模型檢測(cè)問(wèn)題規(guī)約為ATL的模型檢測(cè)問(wèn)題，并利用定理2中的算法步驟求 ||φ||(s)。

例1現(xiàn)在用一個(gè)模糊并發(fā)博弈結(jié)構(gòu)FCGSM=(n,S,AP,V,d,δ)來(lái)建模市場(chǎng)中兩家企業(yè)銷(xiāo)售某產(chǎn)品的情況，其中：

（1）n=2表示有兩家企業(yè)：企業(yè)1和企業(yè)2。

（2）S={s0,s1,s2}，s0表示市場(chǎng)供小于求，s1表示市場(chǎng)供求平衡，而s2表示市場(chǎng)供大于求。

（3）AP={a,b}，表示企業(yè)1銷(xiāo)售該產(chǎn)品方式：高價(jià)壟斷a和薄利多銷(xiāo)b。

（4）V(s0,a)=0.6，V(s1,a)=0.3，V(s1,b)=0.4，V(s2,b)=0.5，V(s2,a)=V(s0,b)=0表示產(chǎn)品在不同市場(chǎng)狀態(tài)下不同銷(xiāo)售方式成功的可能性，例如V(s0,a)=0.6表示供不應(yīng)求的市場(chǎng)狀態(tài)下，高價(jià)壟斷方式銷(xiāo)售成功的可能性是0.6。

（5）d1(s0)=d1(s1)=d1(s2)={1,2}，d2(s0)=d2(s1)=d2(s2)={1,2}表示各企業(yè)在各市場(chǎng)狀態(tài)下采取的不同動(dòng)作來(lái)進(jìn)行銷(xiāo)售，提高利潤(rùn)。其中，d1(s0)={1,2}，表示供小于求的市場(chǎng)狀態(tài)下，企業(yè)1增加市場(chǎng)產(chǎn)品投放量（動(dòng)作1）和提高產(chǎn)品科技含量（動(dòng)作2）。d2(s0)={1,2}，表示供小于求的市場(chǎng)狀態(tài)下，企業(yè)2采用提價(jià)（動(dòng)作1）和維持原價(jià)（動(dòng)作2）。d1(s1)={1,2}，表示供求平衡的市場(chǎng)狀態(tài)下，企業(yè)1采用保持原價(jià)及贈(zèng)送禮包（動(dòng)作1）和提高科技含量（動(dòng)作2）。d2(s1)={1,2}，表示供求平衡的市場(chǎng)狀態(tài)下，企業(yè)2采用降價(jià)（動(dòng)作1）和維持原價(jià)（動(dòng)作2）。d1(s2)={1,2}，表示供大于求的市場(chǎng)狀態(tài)下，企業(yè)1采用贈(zèng)送禮包促銷(xiāo)（動(dòng)作1）和降價(jià)處理（動(dòng)作2）。d2(s2)={1,2}，表示供大于求的市場(chǎng)狀態(tài)下，企業(yè)2采用降價(jià)處理（動(dòng)作1）和提高產(chǎn)品科技含量（動(dòng)作2）。

（6）δ(s0,1,1)=δ(s0,1,2)=s1，δ(s0,2,1)=δ(s0,2,2)=s0，δ(s1,1,1)=δ(s1,1,2)=s2，δ(s1,2,1)=δ(s1,2,2)=s0，δ(s2,1,1)=δ(s2,2,1)=s2，δ(s2,1,2)=δ(s2,2,2)=s1。表示不同市場(chǎng)狀態(tài)下，在企業(yè)間的聯(lián)合動(dòng)作下，市場(chǎng)狀態(tài)變遷情況。

該結(jié)構(gòu)如圖1所示。

Fig.1 Schematic diagram of FCGS圖1 FCGS示例圖

設(shè)φ=＜＜1>>aUb。用定理1的證明過(guò)程中提出的模型檢測(cè)方法來(lái)計(jì)算||φ||。首先令α=0.3，構(gòu)造出M0.3=(n,S,AP,V0.3,d,δ)，其中：

根據(jù)ATL的模型檢測(cè)算法，得到：

再令α=0.4。同理可以構(gòu)造出并發(fā)博弈結(jié)構(gòu)M0.4=(n,S,AP,V0.4,d,δ)，其中：

也利用ATL模型檢測(cè)算法，得到：

然后令α=0.5。則構(gòu)造出并發(fā)博弈結(jié)構(gòu)M0.5=(n,S,AP,V0.5,d,δ)，其中：

最后令α=0.6。則構(gòu)造出并發(fā)博弈結(jié)構(gòu)M0.6=(n,S,AP,V0.6,d,δ)，其中：

因此

文獻(xiàn)[14]指出采用不動(dòng)點(diǎn)迭代算法FATL公式φ的模型檢測(cè)問(wèn)題需要O(|φ|×|M|×|S|×|AP|)時(shí)間。根據(jù)定理1，給出不動(dòng)點(diǎn)迭代算法的時(shí)間復(fù)雜性一個(gè)更理想的漸進(jìn)上界。

定理2設(shè)φ是任意的FATL公式，M是一個(gè)FCGS，則采用不動(dòng)點(diǎn)迭代算法能在復(fù)雜度為O(|φ|×|M|×|S|)時(shí)間內(nèi)正確地計(jì)算 ||φ||的值。

證明用φ=＜＜A>>Gφ1為例來(lái)說(shuō)明本定理成立。根據(jù)已有結(jié)論，對(duì)任意狀態(tài)s，Mα,s╞＜＜A>>Gφ1當(dāng)且僅當(dāng)在Mα中存在一個(gè)策略FA∈ΠA，對(duì)于任意的λ∈out(s,FA)和i≤|S|，Mα,λ(i)╞φ1。因此由定理1可得這 說(shuō)明用不動(dòng)點(diǎn)迭代算法求解||＜＜A>>Gφ1||至多需要|S|次迭代，而每次迭代需要O(|M|)時(shí)間，因此采用不動(dòng)點(diǎn)迭代算法能在復(fù)雜度為O(|φ|×|M|×|S|)時(shí)間內(nèi)計(jì)算出 ||φ||(M,s)。

4 一致連續(xù)性

本章研究FATL語(yǔ)義的一致連續(xù)性。為了研究FATL語(yǔ)義的一致連續(xù)性，需要給出FCGS間“距離”的概念。

定義5（距離）給定兩個(gè)FCGSM1=(n1,S1,AP1,V1,d1,δ1)和M2=(n2,S2,AP2,V2,d2,δ2)且滿足n1=n2,S1=S2,AP1=AP2,d1=d2,δ1=δ2，M1和M2間的距離定義為：

定理3設(shè)φ是FATL公式。對(duì)于任意給定的ε>0，存在一個(gè)η>0，使得只要d(M1,M2)＜η，有|||φ||(M1,,這里S是FCGSM1和M2的狀態(tài)集合。

證明利用結(jié)構(gòu)歸納法證明定理成立。

（1）當(dāng)φ=true時(shí)，結(jié)論明顯成立。

（2）當(dāng)φ=p，p∈AP時(shí)，對(duì)于任意的ε>0，令η=ε，當(dāng)d(M1,M2)＜η時(shí)，顯然有：

（3）當(dāng)φ=?ψ時(shí)，由歸納假設(shè)知，對(duì)于任意的ε>0，存在η>0，當(dāng)d(M1,M2)＜η時(shí)，滿足|||ψ||(M1,s)-||ψ||(M2,s)|＜ε。由定義2得到：

（4）當(dāng)φ=φ1∨φ2時(shí)，根據(jù)歸納假設(shè)，任意的ε>0，存在η1>0，當(dāng)d(M1,M2)＜η1時(shí)，滿足：

同樣地存在η2>0，當(dāng)d(M1,M2)＜η2時(shí)，滿足：

令η=min{η1,η2}，則d(M1,M2)＜η，可以推出：

（5）當(dāng)φ=＜＜A>>Xφ1時(shí)，由歸納假設(shè)知，對(duì)于ε>0，對(duì)于任意的FA∈ΠA，λ∈out(s,FA)，存在ηλ>0，當(dāng)d(M1,M2)＜ηλ時(shí)，使得：

令η=min{ηλ:FA∈ΠA,λ∈out(s,FA)}，由d(M1,M2)＜η可以推出：

（6）當(dāng)φ=＜＜A>>φ1Uφ2時(shí)，由命題1，序列x0=?，xn+1=||φ2||(M1)?(||φ1||(M1)?||＜＜A>>X||(xn))的極限是||＜＜A>>φ1Uφ2||(M1)，序 列y0=?，yn+1=||φ2||(M2)?(||φ1||(M2)?||＜＜A>>X||(xn))的極限是 ||＜＜A>>φ1Uφ2||(M2)。對(duì)n實(shí)施歸納法證明命題對(duì)于φ=＜＜A>>φ1Uφ2情形成立。當(dāng)n=0時(shí)，結(jié)論明顯成立。設(shè)n≤k時(shí)定理成立。當(dāng)n=k+1時(shí)，由歸納假設(shè)對(duì)于任意給定的ε>0，存在一個(gè)η1>0，使得只要d(M1,M2)＜η1，有：

對(duì)于任意給定的ε>0，存在一個(gè)η2>0，使得只要d(M1,M2)＜η2，有：

且對(duì)于任意給定的ε>0，存在一個(gè)η3>0，使得只要d(M1,M2)＜η3，有：

令η=min{η1,η2,η3}。因此對(duì)于任意給定的ε>0，存在一個(gè)η>0，使得只要d(M1,M2)＜η，有：

（7）當(dāng)φ=＜＜A>>Gφ1時(shí)，由于證明過(guò)程類(lèi)似于φ=＜＜A>>φ1Uφ2的證明過(guò)程，故省略證明過(guò)程。

5 結(jié)論

本文進(jìn)一步研究了模糊交互時(shí)態(tài)邏輯的模型檢測(cè)問(wèn)題。通過(guò)將FATL的模型檢測(cè)問(wèn)題歸約到經(jīng)典的ATL模型檢測(cè)問(wèn)題，從而可以利用ATL的模型檢測(cè)問(wèn)題的研究結(jié)果來(lái)解決FATL的模型檢測(cè)問(wèn)題。另外使用這種歸約方法，給出了FATL的模型檢測(cè)問(wèn)題的不動(dòng)點(diǎn)迭代算法一個(gè)更精確的時(shí)間復(fù)雜性。研究了FATL語(yǔ)義的連續(xù)性，當(dāng)模糊并發(fā)博弈結(jié)構(gòu)發(fā)生微小變化時(shí)，模糊交互時(shí)態(tài)邏輯公式的語(yǔ)義也相應(yīng)地發(fā)生微小的變化。本文所獲得的研究結(jié)果為模糊開(kāi)放系統(tǒng)的形式化驗(yàn)證提供了一種新的方法和理論指導(dǎo)。