馬占有，李永明

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

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

馬占有1，2，李永明1

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

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

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

1 引言

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

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

2 廣義可能性決策過程

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

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

(2) Act是動作的集合；

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

(6) L:S→2AP是標(biāo)簽函數(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)擴(kuò)張到2Paths(M)上，設(shè)GPo:2Paths(M)→[0,1]為在Ω=2Paths(M)上的廣義可能性測度。對A?Paths(M)，有GPo(A)=∨{GPo(π)|π∈A}。

容易驗(yàn)證GPo滿足如下性質(zhì):

s,si∈S,αi∈Act}

其中,rP(s)表示從M中狀態(tài)s出發(fā)的路徑的最大可能性，將用于定理1中的結(jié)果。下面通過以Pmax和P+為傳遞矩陣構(gòu)造的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)間可能性分布的方法叫做策略，即調(diào)度表。下面給出調(diào)度表的定義。

上面由Pmax構(gòu)造的GPKSMmax=(S,Pmax,I,AP,L)和由P+構(gòu)造的GPKSM+=(S,P+,I,AP,L)實(shí)際上分別對應(yīng)著GPDPM的一個調(diào)度表μ。

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。

用∪能夠推導(dǎo)出◇和□，即：

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

□：“總是”，□Φ=◇Φ，表示從現(xiàn)在一直到永遠(yuǎ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)，我們可以得出如下結(jié)論：

4 GPoCTL模型檢測

(1)

(2)

(2) 當(dāng)φ=Φ1∪Φ2時，設(shè)C=Sat(Φ1)，B=Sat(Φ2)，對于任意的調(diào)度表μ,則有：

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

?

(3)

(4)

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

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

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

?

5 實(shí)例分析

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

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

因此，poor|=GPo[0.7,0.9](◇{excellent})，說明病人通過治療后恢復(fù)的最大可能性為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})，說明了病人通過六天的治療恢復(fù)的最大可能性和最小可能性分別為0.9和0.7。

6 結(jié)束語

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

[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.

附中文參考文獻(xiàn)：

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

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

馬占有(1979-),男，寧夏固原人，博士生，副教授，研究方向?yàn)槎嘀的Ｐ蜋z測。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

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

TP301

A

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

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

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