魏杰林，袁 申，李永明+，梁常建

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

2.陜西師范大學(xué) 數(shù)學(xué)與信息科學(xué)學(xué)院，西安710119

+通訊作者E-mail:liyongm@snnu.edu.cn

1 引言

模型檢測（model checking）[1-2]是一種形式化驗證方法，主要分為計算樹邏輯（computation tree logic，CTL）模型檢測和線性時態(tài)邏輯（linear temporal logic，LTL）模型檢測。模型檢測作為一種形式化的驗證技術(shù)，已被成功應(yīng)用于許多大規(guī)模軟硬件系統(tǒng)中。

模型檢測的基本思想是用狀態(tài)轉(zhuǎn)換系統(tǒng)M表示系統(tǒng)的模型，用時態(tài)邏輯公式F描述系統(tǒng)的性質(zhì)，這樣檢測一個系統(tǒng)是否滿足一個規(guī)范就轉(zhuǎn)換為驗證M?F是否成立的模型檢測問題[3]。以定性方法研究的經(jīng)典模型檢測很難解決具有量化行為特征的計算機系統(tǒng)如，多智能體系統(tǒng)[4-7]。為了處理諸如此類系統(tǒng)的驗證問題，定量的模型檢測方法引起了學(xué)術(shù)界以及工業(yè)界諸多研究者的關(guān)注。如Hart等提出了基于概率測度的概率模型檢測[8-9]。Sultan 等提出了概率多智能體模型檢測[10-11]。Chechik 等研究了取值于有限D(zhuǎn)e Morgan 代數(shù)的多值Kripke 結(jié)構(gòu)上的CTL 和LTL 的模型檢測問題[12-13]。Pan 等從任意模糊邏輯角度討論了CTL模型檢測問題[14]，并研究了取值于任意有限格的CTL 的模型檢測問題[15]。Li 等將模糊理論中的可能性測度與模型檢測技術(shù)結(jié)合起來，提出了基于可能性測度的模型檢測[16-18]。

可能性模型檢測技術(shù)主要用于不完備信息的系統(tǒng)和非可加性系統(tǒng)的模型檢測[19-23]。在可能性模型檢測技術(shù)中，用可能性Kripke結(jié)構(gòu)[14-15]和廣義可能性Kripke結(jié)構(gòu)[18]來描述系統(tǒng)模型，其狀態(tài)轉(zhuǎn)換關(guān)系中下一個狀態(tài)的選擇不是通過動作的非確定性選擇。為了解決所建模型的每個狀態(tài)轉(zhuǎn)換到其他狀態(tài)有多種可能性分布這一問題，Ma 等提出了基于決策過程的廣義可能性計算樹邏輯模型檢測[3]。

廣義可能性[24]、多值、模糊時態(tài)邏輯[25-26]等相對于經(jīng)典的時態(tài)邏輯只是對布爾連接詞和命題的模糊化，但時序上仍然是經(jīng)典的，對于“不久發(fā)生、幾乎總是發(fā)生”等模糊時間性質(zhì)的模糊時態(tài)沒有進行討論。例如，評估一個外賣員的準(zhǔn)時程度，因為送外賣的過程或多或少的會遇到一些因素的影響，送達時間有可能早幾分鐘，或者是晚幾分鐘，所以只能觀察“幾乎總是發(fā)生”的情況，類似這樣的情況用經(jīng)典的時態(tài)連接詞無法表示明確。

文章首先引入描述非確定性系統(tǒng)模型的廣義可能性決策過程（generalized possibilistic decision process，GPDP）和描述系統(tǒng)屬性的廣義可能性模糊時態(tài)計算樹邏輯（generalized possibilistic fuzzy-time computation tree logic，GPoFCTL），然后給出具有決策過程的GPoFCTL模型檢測算法。并說明了具有模糊時態(tài)的GPDP具有更強的表達能力，最后在廣義可能性調(diào)度下通過模糊矩陣運算討論了“soon,within,last,nearly”等幾類具有模糊時態(tài)的模糊計算樹性質(zhì)的模型檢測問題。

這篇文章與文獻[3]的不同之處是引入了模糊時態(tài)算子，它與模糊集理論是不同的，模糊時態(tài)的“模糊”是由延遲時間的多少產(chǎn)生的，由此引入了懲罰函數(shù)，對延遲進行懲罰。具體懲罰函數(shù)的選擇按照實際情況，為了方便理解模糊時態(tài)，本文列舉了一些日常能夠碰到的事件來說明GPoFCTL 可以表示具有“nearly”等模糊時間的性質(zhì)。文獻[27]僅僅討論了模糊時態(tài)連接詞以及連接詞間的關(guān)系，有關(guān)的模型檢測算法研究也沒有討論，文獻[28]只在LTL下進行研究，且只討論了部分模糊時態(tài)算子。本文是在GPDP和廣義可能性計算樹邏輯（generalized possibilistic computation tree logic，GPoCTL）的基礎(chǔ)上引入了模糊時態(tài)，且對文獻[28]未解決的“∪,N∪,∪t,N∪t”做了研究，此處∪表示意為“until”的時態(tài)算子，并通過模糊矩陣之間的運算來研究模糊時態(tài)算子在具有決策過程的GPoCTL下的模型檢測算法。

2 預(yù)備知識

本章介紹可能性理論、GPDP模型以及GPoCTL。

2.1 可能性理論

可能性測度理論是為了處理不完備信息和非確定性信息。與概率測度理論不同，可能性測度理論包含可能性測度和必然性測度，能更好地處理細微的信息。

定義1[18-23,29]設(shè)X為非空集合，Ω是X冪集的一個子集。如果它可數(shù)，且對取補運算和取并運算封閉，則稱Ω為σ-代數(shù)。Ω上的可能性測度是一個映射POS:Ω→[0,1]，滿足如下條件：

（1）POS(?)=0；

（2）POS(X)=1；

（3）若Ei∈Ω,i∈I，則。

如果只滿足以上條件（1）、（3），則稱POS為廣義可能性測度。注意到如果POS是冪集2X上的廣義可能性測度，對于任意A?X，有。

2.2 廣義可能性決策過程

廣義可能性決策過程中轉(zhuǎn)移的權(quán)重表示到達目標(biāo)狀態(tài)的可能性，轉(zhuǎn)移可以是模糊的。廣義可能性決策過程的形式化定義如下。

定義2[3]廣義可能性決策過程（GPDP）是一個六元組M=(S,Act,P,I,AP,L)，其中：

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

（2）Act是動作的集合；

（3）P:S×Act×S→[0,1]是可能性轉(zhuǎn)移分布，對任意狀態(tài)s∈S和動作α∈Act，存在狀態(tài)t∈S，使得P(s,α,t)＞0；

（4）I:S→L是可能性初始分布，存在狀態(tài)s使得I(s)＞0；

（5）AP是一組原子命題集合；

（6）L:S×AP→L是標(biāo)簽函數(shù)，L(s,α)表示原子命題α在狀態(tài)s上的成立的真值。

若|S|,|Act|,|AP|都是有窮時，則稱M為有窮的，P(s,α,t)表示狀態(tài)s在動作α的作用下，到達狀態(tài)t的可能性。如果存在t∈S，使得P(s,α,t)＞0,則稱α在s上是可以觸發(fā)的。Act(s)表示狀態(tài)s的有效動作集合，表示狀態(tài)集合T中所有狀態(tài)的可觸發(fā)動作集合。如果P(s,α,t)＞0，則稱t是s的后繼，s是t的前驅(qū)Post(s,α)={t∈S|P(s,α,t)＞0}表示狀態(tài)s在動作α下的全體后繼狀態(tài)，Pref(t)表示狀態(tài)t的所有α前驅(qū)狀態(tài)，表示從s出發(fā)在α的作用下到T中狀態(tài)的最大可能性。

對于GPDPM=(S,Act,P,I,AP,L)，用序列s0α0s1α1s2…∈(S×Act)ω表示M中的無窮路徑，Paths(s)和Pathsfin(s)分別表示M中從狀態(tài)s出發(fā)所有的無窮路徑和有窮路徑的集合，同樣的Paths(s)表示M中的所有無窮路徑的集合，Pathsfin(s)表示M中所有有窮路徑的集合。

在GPDPM=(S,Act,P,I,AP,L)中，對于任意α∈Act，可能性分布函數(shù)P:S×Act×S→[0,1]可以用模糊矩陣[3]Pα表示，為動作α在M中對應(yīng)的模糊轉(zhuǎn)移矩陣[30]。用模糊矩陣[3]PMax(PMin) 分別表示P:S×Act×S→[0,1]對應(yīng)的最大可能性轉(zhuǎn)移矩陣（最小可能性轉(zhuǎn)移矩陣），即：

在此引入了調(diào)度（Schedulers）來區(qū)分一般情況下的路徑與廣義決策過程下的路徑，為了計算方便在后面的計算中把P(s0,α0,s1)簡寫為PAdv(s0,s1)。

定義3[3]設(shè)M=(S,Act,P,I,AP,L) 是GPDP，定義映射Adv:S+→Act為M上的調(diào)度，對所有s0s1s2…sn∈S+，使得Adv(s0s1s2…sn)∈Act(sn)。對所有的i＞0，若αi=Adv(s0s1…si)，則稱路徑π=s0α0s1α1s2…為M上的Adv路徑。

注1本文用Max 表示最大傳遞可能性的調(diào)度，稱為最大可性能調(diào)度；用Min 表示最小傳遞可能性的調(diào)度，稱為最小可性能調(diào)度。

設(shè)M=(S,Act,P,I,AP,L)是有窮的GPDP，Adv是M中的調(diào)度，用PathsAdv(s)表示在調(diào)度Adv下，從s出發(fā)的所有路徑集合,PathsAdv(M)和PathsfinAdv(M)分別表示在調(diào)度Adv下，M的全部路徑集合和全部有窮路徑的集合。

模糊矩陣PAdv的轉(zhuǎn)移閉包記為P+Adv。若S為有窮集，則，其中PAdv。模糊矩陣PAdv的自反轉(zhuǎn)移閉包定義為，其中表示恒等矩陣。

在Adv下的柱集和廣義可能性測度的定義如下。

定義4[3]給定一個GPDPM=(S,Act,P,I,AP,L)，設(shè)，其 中n＞0 且n∈N，則有窮路徑的柱集定義為:

定義5[3]設(shè)M=(S,Act,P,I,AP,L)是有窮的GPDP，定義映射GPoAdv:PathsAdv(M)→[0,1]如下：

其中，π=s0α0s1α1s2…∈PathsAdv(M)。

對于E?PathsAdv(M)，定義GPoAdv(E)如下：GPoAdv(E)=∨{GPoAdv(π)|π∈E}，從而得到函數(shù)[0,1]為Ω=2PathsAdv(M)上的廣義可能性測度。

對有窮的GPDPM=(S,Act,P,I,AP,L)，定義rAdv:S→[0,1][3]為：

其中，s1=s，si∈S,αi∈Act，則rAdv(s)表示從狀態(tài)s出發(fā)的Adv路徑最大可能性測度?？梢愿鶕?jù)文獻[3]得到rAdv的計算方法，如下：

用模糊矩陣計算形式為：

2.3 廣義可能性計算樹邏輯

定義6[17]（GPoCTL語法）基于原子命題集合AP上的GPoCTL狀態(tài)公式遞歸定義如下：

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

GPoCTL路徑公式遞歸定義如下：

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

通過連接詞∨,∧,?,→,?,∪可以推導(dǎo)出下面公式：

定義7[17]（GPoCTL 語義）設(shè)M=(S,Act,P,I,AP,L)是GPDP,a∈AP,s∈S,Φ1、Φ2是GPoCTL 的 狀 態(tài) 公式，φ是GPoCTL 的路徑公式，對狀態(tài)公式Φ，其在M上的語義是模糊子集，||Φ||:S→[0,1]對任意s∈S，歸納定義為：

對路徑公式φ，其在M上的語義是||φ||:PathsAdv(M)→[0,1]，歸納定義如下：

GPoAdv(s?φ)表示從狀態(tài)s出發(fā)，在所有調(diào)度Adv下的所有滿足公式φ的可能性，有如下定義：

GPoCTL的具體應(yīng)用可以參考文獻[32-36]。

3 具有決策過程的廣義可能性模糊時態(tài)計算樹邏輯模型檢測

本章引入模糊時態(tài)來對廣義可能性計算樹邏輯進行擴充。首先給出廣義可能性模糊時態(tài)計算樹時序邏輯（GPoFCTL）的語法以及在GPDP 上的語義解釋，并通過例子和證明得到GPoFCTL 是對GPoCTL的擴展，然后研究了在GPDP 下的GPoFCTL 模型檢測算法。

3.1 具有模糊時態(tài)的廣義可能性計算樹邏輯

GPoFCTL由狀態(tài)公式和路徑公式構(gòu)成。下面給出GPoFCTL的語法及其在GPDP上的語義解釋。

定義8（GPoFCTL 語法）基于原子命題集合AP上的GPoFCTL狀態(tài)公式遞歸定義如下：

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

GPoFCTL路徑公式遞歸定義如下：

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

定義9（GPoFCTL 語義）設(shè)M=(S,Act,P,I,AP,L)是GPDP,a∈AP,s∈S,Φ1、Φ2是GPoCTL 的狀態(tài)公式，φ是GPoCTL 的路徑公式，對狀態(tài)公式Φ，其在M上的語義是模糊子集，||Φ||:S→[0,1]對任意s∈S，歸納定義為：

對路徑公式φ，其在M上的語義是||φ||:PathsAdv(M)→[0,1]，歸納定義如下：

其中，“?”表示乘法運算，j＞0 且j∈N，在||N□≤tΦ||(π)中，It為指標(biāo)集，H表示t時間內(nèi)忽略i個時刻后剩余的時刻，表示忽略了某i個時刻后事件發(fā)生的可能性賦值，表示忽略了所有可能的i個時刻后事件發(fā)生的可能性賦值，由η(i)對忽略的時刻數(shù)進行懲罰。

GPoAdv(s?φ)表示從狀態(tài)s出發(fā)，在所有調(diào)度Adv下的所有滿足公式φ的可能性，有如下定義：

在定義8的路徑公式中引入了許多模糊時態(tài)詞，其中引入了懲罰函數(shù)η[22]，η是整數(shù)到[0,1]的一個映射，當(dāng)i≤0 時，η(i)=1，其中i∈N，且存在整數(shù)nη，當(dāng)0 ≤i≤nη時，η(i)的值減小，當(dāng)i≥η時,nη=0。

其中Φ1N∪Φ2表示Φ2之前的狀態(tài)幾乎一直為Φ1，直到狀態(tài)為Φ2時的可能性測度，“幾乎一直發(fā)生”指在這一段路徑中可以有不是Φ1的狀態(tài)。例如小明打算在做完A事件之后就做B事件，而小明在做A事件的這段時間有可能還有其他活動，這用經(jīng)典的時序邏輯是難以表示出來的，但可以用ΦA(chǔ)N∪ΦB來表示，這對于經(jīng)典的來說是在模糊時態(tài)上進行了延伸。下文命題4的證明中能夠得到當(dāng)懲罰函數(shù)η=1，即i≤0 時，模糊時態(tài)與經(jīng)典的時序邏輯具有等價性。

“soon”為不久，表示在下一時刻或者之后的某個時刻事件發(fā)生，可以容許一定的延遲（最多nη的延遲），||soonΦ||(π)表示π在當(dāng)前狀態(tài)之后發(fā)生的可能性程度，即發(fā)生得越快可能性程度也就越大。用η(i-1)表示對時間在下一時刻之后的延遲時刻的可能性程度大小進行懲罰，延遲的時間越久懲罰力度越大，此外可以通過下面的命題4 知道“soon”是對“○”在時間上的延伸。

“Wt”為在t時間內(nèi)或者t時間之后不久的某段時間（最多nη時間）完成，因此用η(i-t)對t時刻之后的事件的程度進行懲罰，i越大懲罰力度越大。例如，外賣需要在1 小時之內(nèi)送達，不可預(yù)計的一些因素會耽誤外賣的送達，但是這個延遲總得有個限度，設(shè)定限度為1 小時30 分鐘。當(dāng)i≤9 時η(i)=0，就可以用||W6||來表示外賣送達的按時度的一個評估（10分鐘當(dāng)作1個計量）。在“Wt”的定義中可以得知，是從當(dāng)前時刻開始的，而計算“soon”時，從下一時刻開始?！癢t”可以看作是對“soon”在時間上進行的延伸。

“Lt”為一直持續(xù)t時間，表示在t時間或者t-i時間以內(nèi)都是持續(xù)的，它是對于一段時間而言的。在這一段時間內(nèi)必須持續(xù)，從下面語義的定義形式可以知道與“N□≤t”是不相同的，后者在任意一段時間都可以容許有不滿足的單個情況出現(xiàn)，而前者在滿足的一段時間是“□≤t”的形式計算?！癓t”可以表示對電池或者電器的壽命評估，幫助一些部門判斷是否與廠商所說的一致。

注2文獻[27]中定義的“∪t”在GPDP的情況下與定義6 中的“∪≤n”具有相同的語義，其中t=n，對于任意t＞0，“∪t”如下定義：

命題1設(shè)Φ是GPoFCTL狀態(tài)公式，M為GPKS（generalized possibilistic kripke structure），π是M的任意路徑，則“∪t”算子是定義好的。并且對于任意的π∈PathsAdv(s),有||Φ1∪Φ2||(π)≤||◇Φ2||(π)。

證明設(shè)Φ是GPoFCTL狀態(tài)公式，M是GPKS，π∈PathsAdv(s) 是M的任意路徑。易證||Φ1∪tΦ2||(π)的值是遞增的。對于t＞0，顯然：

令||α||(π)=1,α∈AP，則有||Φ1∪Φ2||(π)≤||α∪Φ2||(π)成 立，且 有||Φ1∪Φ2||(π)≤||α∪Φ2||(π)≤||◇Φ2||(π) 成立，因此有：

命題2設(shè)Φ是GPoFCTL狀態(tài)公式，M為GPKS，π是M的任意路徑，則“N∪”算子是定義好的。對于任意的π∈PathsAdv(s)有||Φ2||(π)=||Φ1∪0Φ2||(π)≤||Φ1∪t Φ2||(π)≤||Φ1N∪tΦ2||(π)≤||Φ1N∪Φ2||(π)。

證明設(shè)Φ是GPoFCTL狀態(tài)公式，M是GPKS，π∈PathsAdv(s)是M的任意路徑。對于“N∪”算子，易得：

因此，||Φ1N∪tΦ2||(π)的值是遞增的，“N∪t”算子是定義好的。 □

命題3設(shè)Φ是GPoFCTL狀態(tài)公式，M為GPKS，π∈PathsAdv(s)是M的任意路徑。則“N□”算子是定義好的。

證明設(shè)Φ,Ti是GPoFCTL狀態(tài)公式，M為GPKS，π是M的任意路徑，從文獻[32]可以知道：

其中，Ti按如下方式遞歸所得，一般地，T0定義為對任意的路徑π及任意的j∈N，有||T0||(π[j])=||Φ||(π[j])；Ti是由Ti-1遞歸得到，設(shè)ki-1∈N 是使得對任意的j∈N，有最小的數(shù)，令，當(dāng)j＜ki-1時，，當(dāng)j≥ki-1時，就有：

命題4GPoFCTL公式是GPoCTL公式在模糊時態(tài)上的擴張，即i≤0，懲罰函數(shù)η=1 時，GPoFCTL和GPoCTL公式等價。

證明設(shè)Φ是GPoFCTL狀態(tài)公式，M為GPKS，π∈PathsAdv(s)是M的任意路徑。當(dāng)懲罰函數(shù)為1時，由定義9以及命題1、命題2、命題3可知：

由以上證明可知GPoCTL 是GPoFCTL 的一個特例。

例1某軟件在A、B兩種不同的操作系統(tǒng)下更新的可能性用ΦA(chǔ)和ΦB表示，Φ(π[i])表示軟件在第i個星期更新的可能性，η(i)表示懲罰函數(shù)，具體定義如表1、表2，求該軟件在4周內(nèi)幾乎每周都更新的可能性。

Table 1 Definition of Φ(π[i])表1 Φ(π[i])的定義

Table 2 Definition of η(i)表2 η(i)的定義

求該軟件在4 周之內(nèi)幾乎都更新的可能性相當(dāng)于求||N□≤4Φ||Adv(π)。在A、B 兩種環(huán)境下（也可以看作是A、B 兩種方法），通過求其||N□≤4Φ||Max(π)，||N□≤4Φ||Min(π)來得到該軟件在4 周之內(nèi)幾乎都更新的可能性。

首先來求||N□≤4Φ||Max(π)，當(dāng)i=1 時（這個i表示在4周內(nèi)有一次沒更新，之后以此類推），結(jié)果如下：

當(dāng)i=2 時，結(jié)果如下：

當(dāng)i=3 時，結(jié)果如下：

因此||N□≤4Φ||Max(π)=0.42 ∨0.35 ∨0.1=0.42，同理得||N□≤4Φ||Min(π)=0.3，因此在4 周之內(nèi)實際不更新的次數(shù)越多，對在4 周內(nèi)幾乎每周都更新的可能性程度在懲罰函數(shù)的影響下值會越?。涣硪环矫?，||□≤4Φ||Max(π)=0.4,||□≤4Φ||Min(π)=0，后者表現(xiàn)出4 周內(nèi)幾乎每周都更新的可能性為0，顯然用公式||N□≤4Φ||Adv(π)去計算4 周之內(nèi)幾乎每周都更新的可能性比||□≤4Φ||Adv(π)更合適。

3.2 具有決策過程的廣義可能性模糊時態(tài)計算樹邏輯模型檢測算法

GPDP上的GPoFCTL模型檢測問題可以描述如下：對于一個給定的GPDPM，M中的狀態(tài)s以及GPoFCTL 狀態(tài)公式Φ，計算||Φ||(s) 的值。在調(diào)度Adv下，為方便計算，用|Φ|表示公式Φ的子公式個數(shù)，其遞歸定義如下：

若Φ∈AP∪{true}，則|Φ|=1。

形如公式Φ=a∈AP,Φ=Φ1∧Φ2和Φ=?Φ2，其||Φ||(s)可能性值可分別由式（13）、式（14）和式（15）計算得出。而對于公式Φ=GPoAdv(φ)，有||Φ||(s)=GPoAdv(s?φ)=∨π∈PathsAdv(s)(GPoAdv(π)∧||φ||(π))。首先計算出所有調(diào)度Adv下的||Φ||(s)的值，再算出狀態(tài)s滿足公式Φ的最大（最小）可能性。給出模糊矩陣運算來計算狀態(tài)s滿足公式Φ的最大（最?。┛赡苄哉{(diào)度對應(yīng)的算法。用||Φ||Max(s)(||Φ||Min(s))表示狀態(tài)s滿足公式Φ的最大（最?。┛赡苄哉{(diào)度對應(yīng)的可能性測度。下面給出路徑公式“○jΦ,□≤tΦ,WtΦ,soonΦ,N□≤tΦ,Φ1N∪tΦ2,Φ1N∪Φ2,LtΦ”分別對應(yīng)的||Φ||Max(s)和||Φ||Min(s)情況。

（1）對于φ=○jΦ，最大、最小可能性調(diào)度對應(yīng)的||○jΦ||Max(s),||○jΦ||Min(s)計算分別如下：

其中j＞0 且j∈N，對狀態(tài)公式Φ，DΦ表示|S|×|S|的模糊對角線矩陣，當(dāng)s=t時，D(s,t)=||Φ||(s)，否則D(s,t)=0,||GPo(○jΦ)||Max(s) 和||GPo(○jΦ)||Min(s) 的矩陣計算形式為：

其中，模糊矩陣PMax(PMin)表示在所有調(diào)度Adv下的GPDP 對應(yīng)的最大（最?。┺D(zhuǎn)移矩陣，rMax(rMin)表示以模糊矩陣PMax(PMin)為轉(zhuǎn)移矩陣的GPDP 中狀態(tài)s出發(fā)的最大可能性（最小可能性）。

（2）對于φ=□≤tΦ，最大、最小可能性調(diào)度對應(yīng)的||GPo(□≤tΦ)||Max(s)、||GPo(□≤tΦ)||Min(s)計算如下：

||GPo(□≤tΦ)||Max(s)，||GPo(□≤tΦ)||Min(s)的矩陣計算形式為：

（3）對于φ=WtΦ，最大、最小可能性調(diào)度對應(yīng)的||GPo(WtΦ)||Max(s)、||GPo(WtΦ)||Min(s)計算如下：

其中，DΦ～=diag(Φ(si)?η(i-t))si∈S為對角矩陣。

||GPo(WtΦ)||Max(s)和||GPo(WtΦ)||Min(s)的矩陣計算形式為：

當(dāng)t+nη-1 ≥|S|時，式（22）、式（23）可以寫成：

（4）對于φ=soonΦ，最大、最小可能性調(diào)度對應(yīng)的||GPo(soonΦ)||Max(s)、||GPo(soonΦ)||Min(s)計算如下：

其中，DΦ～=diag(Φ(si)?η(i-t))si∈S為對角矩陣。

||GPo(soonΦ)||Max(s)，||GPo(soonΦ)||Min(s) 的矩陣計算形式為：

當(dāng)nη≥|S|時，式（24）、式（25）分別可以寫成：

（5）對于φ=LtΦ，最大、最小可能性調(diào)度對應(yīng)的||GPo(LtΦ)||Max(s)，||GPo(LtΦ)||Min(s)計算如下：

在（2）中已經(jīng)計算出GPoAdv(s?□≤tΦ)s∈S=(PAdv°DΦ)t+1°rAdv(s)，可以直接引入。其中DΦ～=diag(Φ(si)?η(i))si∈S為對角矩陣。||GPo(LtΦ)||Max(s)、||GPo(LtΦ)||Min(s)的矩陣計算形式為：

（6）對于φ=N□≤tΦ，最大、最小可能性調(diào)度對應(yīng)的||GPo(N□≤tΦ)||Max(s)、||GPo(N□≤tΦ)||Min(s)計算如下：

由命題3得：

其中，DΦ～=diag(Φ(si)?η(i))si∈S為對角矩陣。

||GPo(N□≤tΦ)||Max(s)、||GPo(N□≤tΦ)||Min(s)的矩陣計算形式為：

對任意狀態(tài)s，有，得GPo(s?，從而可以得到：

因為當(dāng)t→∞時，t-nη+1 也是趨近于無窮的，肯定是大于狀態(tài)數(shù)|S|的，所以就有式（30）、式（31）。

（7）對于φ=Φ1N∪tΦ2，最大、最小可能性調(diào)度對 應(yīng) 的||GPo(Φ1N∪tΦ2)||Max(s)、||GPo(Φ1N∪tΦ2)||Min(s)計算如下：

||GPo(Φ1N∪tΦ2)||Max(s)，||GPo(Φ1N∪tΦ2)||Min(s) 的 矩陣計算形式為：

對任意狀態(tài)s，有，得，從 而 可 以得到：

因為當(dāng)t→∞時，t-nη也是趨近于無窮的，肯定是大于狀態(tài)數(shù)|S|的，所以就有式（34）、式（35）。

其中φ=□Φ的可能性調(diào)度在文獻[3]中已經(jīng)給出了計算方法，采用了不動點的算法。

在GPoCTL 模型檢測算法中，公式Φ=a∈AP，Φ=Φ1∧Φ2和Φ1=?Φ2，計算||Φ||(s)的時間只與GPDPM的大小和公式Φ的長度有關(guān)。GPoCTL時間復(fù)雜度可以根據(jù)文獻[3]計算為O(size(M)?poly(S)?|Φ|)。但是在GPoFCTL 模型檢測算法中，計算||Φ||(s)的時間不只與GPDPM的大小和公式Φ的長度有關(guān)，還跟η函數(shù)的規(guī)模和計算次數(shù)有關(guān)，而η函數(shù)的規(guī)模由不同的系統(tǒng)情況而定，因此它的時間復(fù)雜度的大小與η函數(shù)有關(guān)；對于GPoFCTL 模型檢測算法中不含懲罰函數(shù)η的情況下的時間復(fù)雜度與GPoCTL 模型檢測算法的時間復(fù)雜度類似，由此可以得到定理1。

定理1給出一個GPoFCTL 公式Φ和一個有窮的GPDPM=(S,Act,P,I,AP,L)，在不含有η的情況下M?Φ的 時 間 復(fù) 雜 度 為O(size(M)?poly(S)?|Φ|)，其 中size(M)是模型的大小，poly(S)是S的多項式函數(shù)，|Φ|是公式的長度。

4 結(jié)束語

本文在模糊時態(tài)和具有決策過程的GPoCTL 的基礎(chǔ)上，研究了具有決策過程的GPoFCTL 模型檢測問題。首先引入了GPDP 模型和GPoCTL，定義了GPoFCTL的語法及其在GPDP上的語義。然后通過模糊矩陣的方式提出并討論了GPoFCTL的模型檢測算法。通過證明和例子說明GPoFCTL是對GPoCTL在模糊時態(tài)方面的擴張，具有更強的表達能力。未來將繼續(xù)研究模糊時態(tài)在可能性測度下的表達能力，同時研究在決策過程下的廣義可能性模糊時態(tài)線性時序邏輯模型檢測問題。