模糊交互時態(tài)邏輯的一些標(biāo)記*

朱 曄，袁紅娟,+，錢俊彥，潘海玉

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

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

1 引言

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

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

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

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

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

2 預(yù)備知識

本章將回顧模糊并發(fā)博弈結(jié)構(gòu)和模糊交互時態(tài)邏輯的語法和語義。在正式引入模糊交互時態(tài)邏輯的語法和語義之前，給出一些記號。后文用N表示自然數(shù)集合，用S+表示有限狀態(tài)序列集合。設(shè)X是經(jīng)典集合，則函數(shù)F:X→[0,1]成為集合X上的模糊集合。若X是有限集合，||X表示集合X中的元素個數(shù)。設(shè)A和B是X上兩個模糊集合，后文用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來指代每個智能體，用Σ表示智能體集合{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可用的非空動作集合，這里，a∈Σ，s∈S。＜j1,j2,…,jn>表示系統(tǒng)在狀態(tài)s下，智能體集合Σ可采取的一個動作向量，其中，ja∈da(s)。同時，定義動作向量集D(s)=d1(s)×d2(s)×…×dn(s)。

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

智能體a的策略fa是一個函數(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的路徑集合。換句話說，若λ=s0s1s2…∈out(s,FA)當(dāng)且僅當(dāng)s0=s，且對于任意i≥ 0，存在動作向量 ＜j1,j2,…,jn>∈D(si)，使得任意a∈A，ja=fa(λ(0,i))，δ(si,j1,j2,…,jn)=si+1。這里用λ(i)，λ(0,i)，λ(i,∞)分別表示狀態(tài)路徑λ的第i個狀態(tài)、λ的有限前綴和λ的無限后綴。

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

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

其中，p∈AP，A?Σ。

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

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

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

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

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

3 模型檢測

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

證明若φ=?φ1，根據(jù)定義2，可先通過計算||φ1||(s)，然后求 ||φ||(s)=1-||φ1||(s)。由引理 1 知，若φ不包含?連接詞的FATL公式，則對任意狀態(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 的模型檢測問題可轉(zhuǎn)換為至多|Im(M)|個ATL的模型檢測問題。注意到經(jīng)典的ATL的模型檢測問題能在O(|φ|×|M|)時間內(nèi)解決。因此計算||φ||(s)的時間復(fù)雜度是O(|φ|× |M|× |S|× |AP|)。

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

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

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

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

（3）AP={a,b}，表示企業(yè)1銷售該產(chǎn)品方式：高價壟斷a和薄利多銷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)品在不同市場狀態(tài)下不同銷售方式成功的可能性，例如V(s0,a)=0.6表示供不應(yīng)求的市場狀態(tài)下，高價壟斷方式銷售成功的可能性是0.6。

（5）d1(s0)=d1(s1)=d1(s2)={1,2}，d2(s0)=d2(s1)=d2(s2)={1,2}表示各企業(yè)在各市場狀態(tài)下采取的不同動作來進(jìn)行銷售，提高利潤。其中，d1(s0)={1,2}，表示供小于求的市場狀態(tài)下，企業(yè)1增加市場產(chǎn)品投放量（動作1）和提高產(chǎn)品科技含量（動作2）。d2(s0)={1,2}，表示供小于求的市場狀態(tài)下，企業(yè)2采用提價（動作1）和維持原價（動作2）。d1(s1)={1,2}，表示供求平衡的市場狀態(tài)下，企業(yè)1采用保持原價及贈送禮包（動作1）和提高科技含量（動作2）。d2(s1)={1,2}，表示供求平衡的市場狀態(tài)下，企業(yè)2采用降價（動作1）和維持原價（動作2）。d1(s2)={1,2}，表示供大于求的市場狀態(tài)下，企業(yè)1采用贈送禮包促銷（動作1）和降價處理（動作2）。d2(s2)={1,2}，表示供大于求的市場狀態(tài)下，企業(yè)2采用降價處理（動作1）和提高產(chǎn)品科技含量（動作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。表示不同市場狀態(tài)下，在企業(yè)間的聯(lián)合動作下，市場狀態(tài)變遷情況。

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

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

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

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

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

也利用ATL模型檢測算法，得到：

然后令α=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]指出采用不動點(diǎn)迭代算法FATL公式φ的模型檢測問題需要O(|φ|×|M|×|S|×|AP|)時間。根據(jù)定理1，給出不動點(diǎn)迭代算法的時間復(fù)雜性一個更理想的漸進(jìn)上界。

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

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

4 一致連續(xù)性

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

定義5（距離）給定兩個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公式。對于任意給定的ε>0，存在一個η>0，使得只要d(M1,M2)＜η，有|||φ||(M1,,這里S是FCGSM1和M2的狀態(tài)集合。

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

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

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

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

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

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

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

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

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

（6）當(dāng)φ=＜＜A>>φ1Uφ2時，由命題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)。對n實(shí)施歸納法證明命題對于φ=＜＜A>>φ1Uφ2情形成立。當(dāng)n=0時，結(jié)論明顯成立。設(shè)n≤k時定理成立。當(dāng)n=k+1時，由歸納假設(shè)對于任意給定的ε>0，存在一個η1>0，使得只要d(M1,M2)＜η1，有：

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

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

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

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

5 結(jié)論

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