具有DP的廣義可能性模糊時(shí)態(tài)CTL模型檢測(cè)*

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

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

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

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

1 引言

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

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

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

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

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

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

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

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

2.1 可能性理論

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

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

（1）POS(?)=0；

（2）POS(X)=1；

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

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

2.2 廣義可能性決策過(guò)程

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

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

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

（2）Act是動(dòng)作的集合；

（3）P:S×Act×S→[0,1]是可能性轉(zhuǎn)移分布，對(duì)任意狀態(tài)s∈S和動(dòng)作α∈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|都是有窮時(shí)，則稱M為有窮的，P(s,α,t)表示狀態(tài)s在動(dòng)作α的作用下，到達(dá)狀態(tài)t的可能性。如果存在t∈S，使得P(s,α,t)＞0,則稱α在s上是可以觸發(fā)的。Act(s)表示狀態(tài)s的有效動(dòng)作集合，表示狀態(tài)集合T中所有狀態(tài)的可觸發(fā)動(dòng)作集合。如果P(s,α,t)＞0，則稱t是s的后繼，s是t的前驅(qū)Post(s,α)={t∈S|P(s,α,t)＞0}表示狀態(tài)s在動(dòng)作α下的全體后繼狀態(tài)，Pref(t)表示狀態(tài)t的所有α前驅(qū)狀態(tài)，表示從s出發(fā)在α的作用下到T中狀態(tài)的最大可能性。

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

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

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

定義3[3]設(shè)M=(S,Act,P,I,AP,L) 是GPDP，定義映射Adv:S+→Act為M上的調(diào)度，對(duì)所有s0s1s2…sn∈S+，使得Adv(s0s1s2…sn)∈Act(sn)。對(duì)所有的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下的柱集和廣義可能性測(cè)度的定義如下。

定義4[3]給定一個(gè)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)。

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

對(duì)有窮的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路徑最大可能性測(cè)度?？梢愿鶕?jù)文獻(xiàn)[3]得到rAdv的計(jì)算方法，如下：

用模糊矩陣計(jì)算形式為：

2.3 廣義可能性計(jì)算樹(shù)邏輯

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

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

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

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

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

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

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

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

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

3 具有決策過(guò)程的廣義可能性模糊時(shí)態(tài)計(jì)算樹(shù)邏輯模型檢測(cè)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

證明設(shè)Φ是GPoFCTL狀態(tài)公式，M是GPKS，π∈PathsAdv(s)是M的任意路徑。對(duì)于“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的任意路徑，從文獻(xiàn)[32]可以知道：

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

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

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

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

例1某軟件在A、B兩種不同的操作系統(tǒng)下更新的可能性用ΦA(chǔ)和ΦB表示，Φ(π[i])表示軟件在第i個(gè)星期更新的可能性，η(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 兩種方法），通過(guò)求其||N□≤4Φ||Max(π)，||N□≤4Φ||Min(π)來(lái)得到該軟件在4 周之內(nèi)幾乎都更新的可能性。

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

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

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

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

3.2 具有決策過(guò)程的廣義可能性模糊時(shí)態(tài)計(jì)算樹(shù)邏輯模型檢測(cè)算法

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

由命題3得：

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

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

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

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

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

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

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

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

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

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

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

4 結(jié)束語(yǔ)

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