模糊交互時態邏輯的一些標記*

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

1.泰州學院 計算機科學與技術學院，江蘇 泰州 225300

2.桂林電子科技大學 廣西可信軟件重點實驗室，廣西 桂林 541004

1 引言

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

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

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

本文的研究任務是文獻[14]工作的延續。首先通過將模糊交互時態邏輯的模型檢測問題轉化為有限個經典的交互時態邏輯的模型檢測問題，從而將模糊交互時態邏輯的模型檢測可以轉化為使用經典的時態交互邏輯的模型檢測算法來解決，進一步分析了模糊交互時態邏輯的模型檢測問題的不動點迭代算法的時間復雜性。最后研究了模糊交互時態邏輯語義的連續性問題，即模糊并發博弈結構發生微小變化時，模糊交互時態邏輯的語義是否也相應地發生微小的變化。

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

2 預備知識

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

定義1[14]（模糊并發博弈結構）模糊并發博弈結構（fuzzy concurrent game structure，FCGS）是六元組：

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

（1）n是系統中智能體的數目，用自然數1,2,…,n來指代每個智能體，用Σ表示智能體集合{1,2,…,n}。

（2）S是有限狀態集。

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

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

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

（6）δ是狀態遷移函數，表示系統在動作向量＜j1,j2,…,jn>∈D(s)的作用下，從狀態s遷移到下一個狀態δ(s,j1,j2,…,jn)。

注意到，經典的并發博弈結構是一種特殊的FCGS，因為若FCGSM的模糊賦值函數的值域限制為{0,1}，則M為經典的并發博弈結構。若沒有特別說明，后文用M表示一個FCGS。

智能體a的策略fa是一個函數fa:S+→Ν：如果λ的最后狀態為s，則fa(λ)∈da(s)。{fa|a∈A}為A的聯盟策略，記作FA。另外，記ΠA為A的所有的聯盟策略之集。令FA∈ΠA。用out(s,FA)表示聯盟體A遵循聯盟策略FA得到的所有源自s的路徑集合。換句話說，若λ=s0s1s2…∈out(s,FA)當且僅當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,∞)分別表示狀態路徑λ的第i個狀態、λ的有限前綴和λ的無限后綴。

下面給出用于描述FCGS性質的模糊交互時態邏輯的語法和語義。

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

其中，p∈AP，A?Σ。

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

從上述定義不難看出，FATL的語法和經典ATL的語法是完全一致的，它們的區別主要表現在其語義上。

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

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

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

3 模型檢測

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

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

模型FCGSM的規模大小為：

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

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

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

證明采用結構歸納法證明。

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

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

（3）當φ=φ1∨φ2時，由歸納假設知：

（4）當φ=＜＜A>>Xφ1時，由歸納假設知：

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

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

（5）當φ=＜＜A>>φ1Uφ2時，由歸納假設，定義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）當φ=＜＜A>>Gφ1時，由歸納假設，定義3和定義4知：

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

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

根據以上結論，下面定理1的證明過程給出了將FATL的模型檢測問題轉換為經典的ATL的模型檢測的方法。

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

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

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

例1現在用一個模糊并發博弈結構FCGSM=(n,S,AP,V,d,δ)來建模市場中兩家企業銷售某產品的情況，其中：

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

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

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

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

該結構如圖1所示。

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

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

根據ATL的模型檢測算法，得到：

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

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

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

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

因此

文獻[14]指出采用不動點迭代算法FATL公式φ的模型檢測問題需要O(|φ|×|M|×|S|×|AP|)時間。根據定理1，給出不動點迭代算法的時間復雜性一個更理想的漸進上界。

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

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

4 一致連續性

本章研究FATL語義的一致連續性。為了研究FATL語義的一致連續性，需要給出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設φ是FATL公式。對于任意給定的ε>0，存在一個η>0，使得只要d(M1,M2)＜η，有|||φ||(M1,,這里S是FCGSM1和M2的狀態集合。

證明利用結構歸納法證明定理成立。

（1）當φ=true時，結論明顯成立。

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

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

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

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

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

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

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

（6）當φ=＜＜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實施歸納法證明命題對于φ=＜＜A>>φ1Uφ2情形成立。當n=0時，結論明顯成立。設n≤k時定理成立。當n=k+1時，由歸納假設對于任意給定的ε>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）當φ=＜＜A>>Gφ1時，由于證明過程類似于φ=＜＜A>>φ1Uφ2的證明過程，故省略證明過程。

5 結論

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