馬占有，李永明

(1.陜西師范大學計算機科學學院，陜西 西安 710062；2.北方民族大學計算機科學與工程學院，寧夏 銀川 750021)

廣義可能性決策過程的計算樹邏輯模型檢測*

馬占有1，2，李永明1

(1.陜西師范大學計算機科學學院，陜西 西安 710062；2.北方民族大學計算機科學與工程學院，寧夏 銀川 750021)

模型檢測作為一種形式化驗證技術，已被廣泛應用于各種并發(fā)系統(tǒng)的正確性驗證。針對具有非確定性選擇和廣義可能性分布的并發(fā)系統(tǒng)，引入廣義可能性決策過程作為此類系統(tǒng)的模型；給出描述其性質的規(guī)范語言廣義可能性計算樹邏輯的概念；研究此類系統(tǒng)的廣義可能性計算樹邏輯模型檢測問題。結論表明，其模型檢測算法的時間復雜度也為多項式時間。所獲得的結果擴大了廣義可能性測度在模型檢測中的應用范圍。

并發(fā)系統(tǒng)；廣義可能性決策過程；廣義可能性計算樹邏輯；模型檢測

1 引言

模型檢測作為一種形式化的自動驗證技術，自1981年由Clarke E等人[1]提出以來，在計算機軟硬件設計、通信協(xié)議、安全協(xié)議、分布式算法的正確性和可靠性分析等方面取得了成功的應用[2～10]。

經(jīng)典的模型檢測技術主要用于驗證系統(tǒng)的定性性質，近年來，許多學者開始關注系統(tǒng)的定量性質，提出了量化模型檢測技術，而基于多值(模糊)邏輯的模型檢測技術[8,9]是具有代表性的成果之一。李永明等[10～13]將模糊集合中可能性測度與模型檢測技術相結合，提出了基于可能性測度的模型檢測技術?？赡苄阅Ｐ蜋z測技術主要用于不完備信息的非確定性系統(tǒng)和非可加性系統(tǒng)的模型檢測。在可能性模型檢測技術中，廣義可能性Kripke結構GPKS(Generalized Possibilistic Kriple Structure)[12]被用來描述系統(tǒng)的模型。GPKS的主要特點是Kripke結構圖中狀態(tài)到其后繼狀態(tài)是一個模糊值。在實際系統(tǒng)開發(fā)過程中，我們經(jīng)常會遇到同時具有非確定性和模糊性的并發(fā)系統(tǒng)。為了對此類系統(tǒng)的性質進行分析，我們首先采用類似于馬爾科夫決策過程[3]的廣義可能性決策過程作為此類系統(tǒng)的模型。廣義可能性決策過程中傳遞既有非確定性選擇又有可能性分布，傳遞首先從當前狀態(tài)開始非確定選擇可能性分布；再選擇到其后續(xù)狀態(tài)可能性；然后引入廣義可能性計算樹邏輯作為此類系統(tǒng)的規(guī)范語言；最后給出廣義可能性計算樹邏輯模型檢測的算法和相應的實例對全文內(nèi)容進行說明。

2 廣義可能性決策過程

基于文獻[12]中的GPKS，本文提出廣義可能性決策過程作為系統(tǒng)模型，該模型類似于馬爾科夫決策過程模型。下面給出廣義可能性決策過程的定義。

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

(2) Act是動作的集合；

(5) AP是一組原子命題集合；

(6) L:S→2AP是標簽函數(shù)，即每個狀態(tài)為真的原子命題的集合(AP的子集)。

Figure 1 Structure model of 4 states group organizations圖1 四狀態(tài)的GPKS

Figure 2 GPKS Mmax圖2 GPKS Mmax

Figure 3 GPKS M+圖3 GPKS M+

GPo可由Paths(M)擴張到2Paths(M)上，設GPo:2Paths(M)→[0,1]為在Ω=2Paths(M)上的廣義可能性測度。對A?Paths(M)，有GPo(A)=∨{GPo(π)|π∈A}。

容易驗證GPo滿足如下性質:

s,si∈S,αi∈Act}

其中,rP(s)表示從M中狀態(tài)s出發(fā)的路徑的最大可能性，將用于定理1中的結果。下面通過以Pmax和P+為傳遞矩陣構造的GPKS，給出rP(s)的計算方法。

證明 對任意s∈S，

s,si∈S,αi∈Act}

由于S是有窮的，則M中存在路徑π=s0α0s1α1…siαitβ0t1β1t2…βjt…；s0=s,si,t,tj∈S,αi,βj∈Act,使得:

另一方面，

因此，定理成立。

□

證明Cyl(s0α0s1α1…αn-1sn)=∪{π∈Paths(M)|s0α0s1α1…αn-1sn∈Pref(π)}，則有:

□

GPDP描述的是具有非確定性和模糊性的系統(tǒng)，則訪問GPDP時，先確定狀態(tài)間的可能性分布，然后再確定狀態(tài)間的可能性，我們把確定狀態(tài)間可能性分布的方法叫做策略，即調度表。下面給出調度表的定義。

上面由Pmax構造的GPKSMmax=(S,Pmax,I,AP,L)和由P+構造的GPKSM+=(S,P+,I,AP,L)實際上分別對應著GPDPM的一個調度表μ。

Mμ中狀態(tài)s滿足Pr的可能性為:

GPomax(s|=Pr)=maxμ{GPoμ(s|=Pr)}，

GPomin(s|=Pr)=minμ{GPoμ(s|=Pr)}

3 廣義可能性計算樹邏輯(GPoCTL)

定義4(GPoCTL語法) 原子命題集合AP上GPoCTL狀態(tài)公式的語法定義如下:

路徑公式的語法定義如下:

φ::=O

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

用∪能夠推導出◇和□，即：

◇：“最終”，◇Φ=true∪Φ，表示Φ最終在將來的某個時間為真。

□：“總是”，□Φ=◇Φ，表示從現(xiàn)在一直到永遠Φ都為真。

對于GPDPM和GPKSMμ，用SatM(Φ)和SatMμ(Φ)分別表示M和Mμ滿足公式Φ的狀態(tài)集合，≡M和≡Mμ分別表示M和Mμ中兩個狀態(tài)公式等價，即對于狀態(tài)公式Φ1和Φ2，Φ1≡MΦ2表示SatM(Φ1)=SatM(Φ2)；Φ1≡μΦ2表示SatMμ(Φ1)=SatMμ(Φ2)，我們可以得出如下結論：

4 GPoCTL模型檢測

(1)

(2)

(2) 當φ=Φ1∪Φ2時，設C=Sat(Φ1)，B=Sat(Φ2)，對于任意的調度表μ,則有：

GPoμ{π∈Paths(s)|?j≥0,π[j]∈B,

?

(3)

(4)

對s∈S?的狀態(tài)s，有:

(3) 當φ=Φ1∪≤nΦ2，設C=Sat(Φ1)，B=Sat(Φ2)，對于任意的μ,我們有:

GPoμ({π∈Paths(s)|?j≤n,π[j]∈B,

?

5 實例分析

從而得(xs max)s∈S=(0.9,1,1,1)，

同理向量(xs min)s∈S的值迭代過程如下：

因此，poor|=GPo[0.7,0.9](◇{excellent})，說明病人通過治療后恢復的最大可能性為0.9，最小可能性為0.7。

(3) 計算公式GPo(s|={poor,fair}∪≤6{excellent})。

此時S0={good}，Sr={excellent}，S?={poor,fair}，從而得(xs max)s∈S=(0.9,0.9,0,1)，(xs min)s∈S=(0.7,0.7,0,1)。

因此，poor|=GPo[0.7,0.9]({poor,fair}∪≤6{excellent})，說明了病人通過六天的治療恢復的最大可能性和最小可能性分別為0.9和0.7。

6 結束語

本文引入了GPDP來描述系統(tǒng)的模型，給出了描述系統(tǒng)的性質的規(guī)范語言GPoCTL，探討了系統(tǒng)的GPoCTL模型檢測問題，提出了解決GPoCTL模型檢測問題的算法，拓展了可能性測度在模型檢測中的應用范圍。

[1]ClarkeE,GrumbergO,PeledD.ModelChecking[M].Massachusetts:TheMITPress,1999.

[2]LinHM,ZhangWH.Modelchecking:Theories,techniquesandapplications[J].ChineseJournalofElectronics,2002,30(12A): 1907-1912. (inChinese)

[3]BaierC,KatoenJP.Principlesofmodelchecking[M].Massachusetts:TheMITPress, 2007.

[4]CranenS,GrooteJF,ReniersM.AlineartranslationfromCTL*tothefirst-ordermodalμ-calculus[J].TheoreticalComputerScience, 2011,412(28): 3129-3139.

[5]RozierKY.Lineartemporallogicsymbolicmodelchecking[J].ComputerScienceReview, 2011,5(2):163-203.

[6]CleavelandR,PurushothamanS,NarasimhaIM.Probabilistictemporallogicsviathemodalmu-calculus[J].TheoreticalComputerScience, 2005,342(2-3): 316-350.

[7]BentaharJ,YahyaouiH,KovaM,etal.Symbolicmodelcheckingcompositewebservicesusingoperationalandcontrolbehaviors[J]．ExpertSystemswithApplications, 2013,40(2)：508-522．

[8]FischerD,GradelE,KaiserL.Modelcheckinggamesforthequantitativeμ-calculus[J].TheoryofComputingSystems, 2010,47(3): 696-719．

[9]ChechikM,DevereuxB,EasterbrookS,etal.Multi-valuedsymbolicmodel-checking[J].ACMTransactionsonSoftwareEngineeringandMethodology,2003,12(4):1-38．

[10]LiYM,LiLJ.Modelcheckingoflinear-timepropertiesbasedonpossibilitymeasure[J].IEEETransactionsinFuzzySystems, 2013,21(5)：842-854.

[11]LiYM,LiYL,MaZY.Computationtreelogicmodelcheckingbasedonpossibilitymeasure[J].FuzzySetsandSystems, 2015,262(5): 44-59.

[12]LiYM,MaZY.Quantitativecomputationtreelogicmodelcheckingbasedongeneralizedpossibilitymeasures[J].IEEETransactionsonFuzzySystems,2014(09),doi:10.1109/TFUZZ.2015.2396537.

[13]ZhangXX,DengNY,MaZY,etal.Possibilisticbisimulationbasedongeneralizedpossibilitymeasuresanditslogicalcharacterizations[J].ComputerEngineering&Science, 2015,37(5)：951-957. (inChinese)

[14]GarmendiaL,GonzálezR,delCampoV,etal.Analgorithmtocomputethetransitiveclosure,atransitiveapproximationandatransitiveopeningofafuzzyproximity[J].MathwareandSoftComputing, 2009,16(2)：175-191.

[15]XingHY,ZhangQS,HuangKS.Analysisandcontroloffuzzydiscreteeventsystemsusingbisimulationequivalence[J].TheoreticalComputerScience, 2012,456(19)：100-111.

附中文參考文獻：

[2] 林惠民,張文輝.模型檢測:理論 方法與應用[J].電子學報, 2002,36(12A)：1907-1012.

[13] 張興興, 鄧楠軼, 馬占有, 等. 廣義可能性互模擬及其邏輯刻畫[J]. 計算機工程與科學, 2015,37(5)：951-957.

馬占有(1979-),男，寧夏固原人，博士生，副教授，研究方向為多值模型檢測。E-mail:mazhany@126.com

MA Zhan-you,born in 1979,PhD candidate,associate professor,his research interest includes multi-valued model checking.

Computation tree logic model checking for generalized possibilistic decision processes

MA Zhan-you1，2，LI Yong-ming1

(1.College of Computer Science,Shaanxi Normal University,Xi’an 710062;2.College of Computer Science and Engineering,Beifang University of Nationalities,Yinchuan 750021,China)

Model checking is a widespread formal technique for verifying the correctness of concurrent systems. We introduce the generalized possibilistic decision process as the model of the systems, which have non-deterministic choices and generalized possibility distributions.To describe its attributes, we define the concept of generalized possibilistic computation tree logic (GPCTL) specification language and study the GPCTL model checking problems.The time complexity of the computation tree logic model checking algorithm shows to be polynomial time. The results obtained in this paper extend the application scope of model checking based on generalized possibility measurement.

concurrent systems；generalized possibilistic decision process；generalized possibilistic computation tree logic (GPCTL)；model checking

1007-130X(2015)11-2162-07

2015-08-13;

2015-10-11

國家自然科學基金資助項目(11271237,61228305,61462001);北方民族大學資助項目(2014XB213)

TP301

A

10.3969/j.issn.1007-130X.2015.11.025

通信地址：750021 寧夏銀川市北方民族大學計算機科學與工程學院

Address:College of Computer Science and Engineering,Beifang University of Nationalities,Yinchuan 750021,Ningxia,P.R.Chin