紀(jì)明宇，王海濤，陳志遠(yuǎn)，李艷梅

（1.東北林業(yè)大學(xué) 信息與計(jì)算機(jī)工程學(xué)院，黑龍江 哈爾濱150040；2.哈爾濱工程大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，黑龍江 哈爾濱150001）

0 引 言

作為一種重要的自動(dòng)驗(yàn)證技術(shù)，模型檢測(cè)［1］因其可以自動(dòng)執(zhí)行，并能在系統(tǒng)不滿足性質(zhì)時(shí)提供反例路徑等優(yōu)點(diǎn)而在軟、硬件系統(tǒng)的性能驗(yàn)證方面應(yīng)用日益廣泛。然而隨著待驗(yàn)證系統(tǒng)模型的不斷增大，狀態(tài)爆炸的問(wèn)題在很大程度上制約著模型檢測(cè)技術(shù)的進(jìn)一步應(yīng)用，現(xiàn)有的抑制狀態(tài)爆炸問(wèn)題的技術(shù)主要有：符號(hào)模型檢測(cè)［2］、約減技術(shù)［3］等。其中符號(hào)模型檢測(cè)技術(shù)利用有序二元決策圖 （ordered binary decision diagrams，OBDD）對(duì)模型的狀態(tài)空間進(jìn)行壓縮表示，然而OBDD只能表示布爾函數(shù)，對(duì)于支持復(fù)雜參數(shù)特征性質(zhì)定量分析驗(yàn)證的概率模型［4，5］狀態(tài)空間爆炸問(wèn)題并不適用。

與符號(hào)模型檢測(cè)不同，約減技術(shù)利用系統(tǒng)行為中的等價(jià)關(guān)系減少本質(zhì)上相同的重復(fù)路徑，在傳統(tǒng)模型檢測(cè)及概率模型中得到了很好的應(yīng)用［6，7］，文獻(xiàn) ［8］將對(duì)稱(chēng)約減技術(shù)應(yīng)用于連續(xù)時(shí)間馬爾可夫鏈 （continuous time Markov chain，CTMC）和馬爾可夫判定過(guò)程 （Markov decision process，MDP）模型，并給出了實(shí)例分析，但未對(duì)支持遷移資源描述的隨機(jī)模型約減方法進(jìn)行說(shuō)明。

本文將結(jié)合符號(hào)模型檢測(cè)與對(duì)稱(chēng)約減技術(shù)，使其應(yīng)用于支持遷移資源消耗的概率模型中，使用改進(jìn)的多終端二元決策圖表示狀態(tài)遷移矩陣，基于對(duì)稱(chēng)約減理論給出針對(duì)遷移矩陣的約減算法，并給出實(shí)例說(shuō)明。

1 基本概率模型

定義1 DTMC

DTMC為五元組Μ ＝ （S，P，L，AP，v），其中S表示狀態(tài)集合，P：S×S→［0，1］為狀態(tài)轉(zhuǎn)移概率矩陣，對(duì)于狀態(tài)集的狀態(tài)s，有 ∑s＇∈Sp（s，s＇）＝1，L：S→2AP為狀態(tài)標(biāo)記函數(shù)，AP表示原子命題的有限集，v∈Distr（S）為初始分布集合。

下面基于DTMC給出支持遷移回報(bào)的離散時(shí)間Markov 判 定 過(guò) 程 （Discrete Time Markov Rewards Decision Process，DTMRDP）的定義。

定義2 DTMRDP

DTMRDP為七元組M ＝ （S，A，P，L，AP，N，v），它是在原有的DTMC的基礎(chǔ)上增加了遷移動(dòng)作集合A和一個(gè)用于表示遷移資源消耗的遷移回報(bào)結(jié)構(gòu)N：S×A×S→R≥0后構(gòu)成的。

模型中，若P（s1，a，n，s2）＝0.5，則表示在s1與s2存在一個(gè)動(dòng)作a的遷移，發(fā)生遷移的概率為0.5，遷出s1狀態(tài)的遷移資源消耗為n。

2 模型MTBDD表示

OBDD作為化簡(jiǎn)了的二元決策圖，是一個(gè)具有1個(gè)根節(jié)點(diǎn)和2個(gè)終端結(jié)點(diǎn) （標(biāo)記為0和1）的有向無(wú)環(huán)圖，使用OBDD驗(yàn)證模型的基本思想是通過(guò)蘊(yùn)含的辦法，用OBDD來(lái)表示模型檢測(cè)中轉(zhuǎn)移關(guān)系、可達(dá)狀態(tài)集合，以此來(lái)進(jìn)行不動(dòng)點(diǎn)的計(jì)算［9］，OBDD的使用使得現(xiàn)有的模型檢測(cè)器可以對(duì)狀態(tài)數(shù)高達(dá)10120的系統(tǒng)進(jìn)行驗(yàn)證［10］。

多終 端 二 元 決 策 圖 （multi－terminal binary decision diagrams，MTBDD）擴(kuò)展了OBDD的表示范圍，可以用來(lái)表示一個(gè)從多維布爾值域到任意實(shí)數(shù)集的函數(shù)f（v1，v2，…vn）：｛0，1｝n→R，因其終端結(jié)點(diǎn)可以有多個(gè)并且可以是任意實(shí)數(shù)，因此可通過(guò)終端結(jié)點(diǎn)來(lái)表示隨機(jī)系統(tǒng)模型的不同遷移概率、遷移離開(kāi)率等信息，進(jìn)而進(jìn)行隨機(jī)系統(tǒng)模型的分析驗(yàn)證。

例1 隨機(jī)系統(tǒng)模型MTBDD舉例

圖1表示一個(gè)由4個(gè)狀態(tài)構(gòu)成的DTMC，其狀態(tài)遷移MTBDD表示如圖2所示。

對(duì)于傳統(tǒng)的MTBDD，本文通過(guò)以下的方法進(jìn)行改進(jìn)：將終端節(jié)點(diǎn)的取值范圍集合由實(shí)數(shù)集變改為實(shí)數(shù)對(duì)偶集，從而使這種多終端二元決策圖可用來(lái)表示任一從多維布爾值域到任意實(shí)數(shù)對(duì)偶集合的函數(shù)f（v1，v2，…vn）：｛0，1｝n→（R∈［0，1］，R＇≥0），其中實(shí)數(shù)對(duì)偶分別用來(lái)表示隨機(jī)系統(tǒng)模型的遷移概率及遷移資源消耗。

圖1 DTMC模型舉例

圖2 DTMC模型MTBDD表示

3 DTMRDP模型對(duì)稱(chēng)約減

對(duì)于本文描述的DTMRDP模型，由于在狀態(tài)遷移過(guò)程中，伴隨著多種復(fù)雜特征信息，因此其對(duì)稱(chēng)約減方法有別于一般的非概率遷移系統(tǒng)。

定義3 自同構(gòu)

若遷移系統(tǒng)M＝（S，R），其中S為狀態(tài)的有限集，遷移關(guān)系RS×S，則狀態(tài)空間S上的自同構(gòu)表示為π：S→S，且滿足：如果 （s，s＇）∈R ，則 （π（s），π（s＇））∈R 。

定義4 等價(jià)關(guān)系

對(duì)于給定的一組自同構(gòu)G，狀態(tài)空間S的等價(jià)關(guān)系θ表示為 （s，π（s））∈θ。

定義5 遷移系統(tǒng)商

設(shè)遷移系統(tǒng)M＝（S，R），對(duì)于狀態(tài)空間的每一個(gè)等價(jià)類(lèi)，通過(guò)引入遷移關(guān)系珚R＝｛（rep（s），rep（s，s＇）∈R｝及等價(jià)類(lèi)狀態(tài)唯一表示函數(shù)rep：S→珚S，可構(gòu)造出原遷移系統(tǒng)的商，表示為珨M＝（珚S，珚R）。對(duì)于M＝（S，R）而言，因?yàn)樽酝瑯?gòu)保留了遷移關(guān)系R，所以遷移系統(tǒng)商珨M與原遷移系統(tǒng)M等價(jià)互模擬。

對(duì)于前文中提到的DTMC、DTMRDP模型，約減后的商模型定義如下：

定義6 DTMC商模型

定義7 DTMRDP商模型

若DTMRDP模型M ＝ （S，P，A，N），則其商模型表示為＝），對(duì)于所有狀態(tài)s，商模型狀態(tài)遷移概率及遷移回報(bào)計(jì)算方法如下

在DTMC及DTMRDP商模型的定義中，由于標(biāo)記函數(shù)、原子命題、初始狀態(tài)與商模型構(gòu)造無(wú)關(guān)，所以在商模型構(gòu)造中并未對(duì)它們進(jìn)行具體說(shuō)明。

例2 DTMRDP模型對(duì)稱(chēng)約減示例

本例修改使用了文獻(xiàn) ［8］中的對(duì)稱(chēng)進(jìn)程實(shí)例，假設(shè)存在兩個(gè)對(duì)稱(chēng)的進(jìn)程，每個(gè)進(jìn)程有三個(gè)狀態(tài) （0、1和2），且兩個(gè)進(jìn)程在進(jìn)行狀態(tài)變遷時(shí)除了滿足一定的隨機(jī)性以外，同時(shí)還會(huì)消耗數(shù)量為n的資源，這樣的兩個(gè)對(duì)稱(chēng)進(jìn)程的工作狀態(tài)變遷可由DTMRDP模型表示。

設(shè)最初兩個(gè)進(jìn)程都處于狀態(tài)0，進(jìn)程的工作時(shí)序如下：第一步，兩個(gè)進(jìn)程中的任一個(gè)均可以以概率0.5隨機(jī)地移動(dòng)到狀態(tài)1或2；第二步：在第一步中未發(fā)生狀態(tài)變化的進(jìn)程隨機(jī)地移動(dòng)到狀態(tài)1或2，但要求若該步中某一進(jìn)程移動(dòng)到狀態(tài)2，則另一進(jìn)程在此步驟須移動(dòng)到狀態(tài)1。

本例可通過(guò)圖3所示的DTMRDP模型進(jìn)行描述，由于假設(shè)各狀態(tài)在發(fā)生狀態(tài)變遷時(shí)的動(dòng)作相同，故在圖3中省略了動(dòng)作描述。

通過(guò)圖4中給出的等價(jià)關(guān)系唯一表示函數(shù)，可以對(duì)原模型中的狀態(tài)集進(jìn)行約減，借助于本文后面提出的遷移關(guān)系對(duì)稱(chēng)約減算法將得出如圖5所示的對(duì)稱(chēng)約減商DTMRDP模型，模型的狀態(tài)個(gè)數(shù)及遷移個(gè)數(shù)明顯減少。

圖3 對(duì)稱(chēng)進(jìn)程DTMRDP模型

圖4 等價(jià)關(guān)系唯一表示函數(shù)

4 算法描述

圖5 對(duì)稱(chēng)約減商DTMRDP模型

對(duì)于DTMRDP模型的對(duì)稱(chēng)約減過(guò)程，下面給出基于原模型狀態(tài)遷移矩陣的對(duì)稱(chēng)約減算法，其轉(zhuǎn)換過(guò)程大致可以分為矩陣行消除、矩陣列累加和規(guī)一化處理等幾步，相應(yīng)的算法描述如下：

狀態(tài)遷移矩陣的對(duì)稱(chēng)約減算法：

本算法基本操作為矩陣運(yùn)算，算法復(fù)雜性不高，由于篇幅原因，本文不做具體分析。

5 實(shí)例說(shuō)明

對(duì)于圖3所示的對(duì)稱(chēng)進(jìn)程DTMRDP模型，該模型的遷移矩陣MTBDD表示如圖6所示。

依據(jù)本文提出的算法，相應(yīng)的模型遷移矩陣對(duì)稱(chēng)約減轉(zhuǎn)換過(guò)程見(jiàn)圖7（a）至圖7（d）。

得出模型約減后的狀態(tài)遷移MTBDD表示如圖8所示，可見(jiàn)原模型中的狀態(tài)集及遷移關(guān)系均被大大縮減。

圖6 約減前狀態(tài)遷移MTBDD表示

圖7 遷移矩陣對(duì)稱(chēng)約減算法實(shí)例說(shuō)明

圖8 約減后狀態(tài)遷移MTBDD表示

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

本文借鑒了傳統(tǒng)的符號(hào)模型檢測(cè)技術(shù)，改進(jìn)了二元決策圖的表示形式，將符號(hào)模型檢測(cè)技術(shù)和對(duì)稱(chēng)約減技術(shù)綜合應(yīng)用于復(fù)雜概率模型，基于遷移矩陣提出了相應(yīng)的約減方法并給出了算法描述，通過(guò)實(shí)例證明了該方法的有效性，縮減了模型的狀態(tài)空間，提高了隨機(jī)系統(tǒng)模型的驗(yàn)證規(guī)模，擴(kuò)大了模型檢測(cè)的應(yīng)用范圍。下一步作者將進(jìn)一步研究其它概率模型的約減處理方法，并對(duì)現(xiàn)實(shí)系統(tǒng)的應(yīng)用進(jìn)行深入分析。

［1］Marta Kwiatkowska，Gethin Norman，David Parker.Advances and challenges of probabilistic model checking ［C］／／Proceedings of the 48th Annual Allerton Conference on Communication，Control and Computing.2010：1691－1698.

［2］WU Lijun，SU Jinshu，SU Kaile.Symbolic model checking knowledge and time in multi－agent system via extended mu－calculus［J］.Chinese Journal of Computers，2008 （2）：245－252（in Chinese）.［吳立軍，蘇金樹(shù)，蘇開(kāi)樂(lè).多智能體系統(tǒng)時(shí)態(tài)認(rèn)知規(guī)范高效符號(hào)模型檢測(cè)的算法研究 ［J］.計(jì)算機(jī)學(xué)報(bào)，2008 （2）：245－252.］

［3］MA Yanan，LIU Nan，ZHU Yuefei，et al.Stuttering partial－order reduction algorithm in verification of security protocols ［J］.Application Research of Computers，2011 （9）：3488－3491 （in Chinese）.［馬亞南，劉楠，祝躍飛，等.安全協(xié)議狀態(tài)空間的束動(dòng)作偏序約簡(jiǎn)算法 ［J］.計(jì)算機(jī)應(yīng)用研究，2011 （9）：3488－3491.］

［4］ZHOU Conghua，LIU Zhifeng，WANG Changda.Bounded model checking for probabilistic computation tree logic ［J］.Journal of Software，2012，23 （7）：1665－1668 （inChinese）.［周從華，劉志鋒，王昌達(dá).概率計(jì)算樹(shù)邏輯的限界模型檢測(cè)［J］.軟件學(xué)報(bào)，2012，23（7）：1665－1668.］

［5］NIU Jun，ZENG Guosun，WANG Wei.An approach of model checking time or space performance ［J］.Chinese Journal of Computers，2010，33 （9）：1621－1633（in Chinese）. ［鈕俊，曾國(guó)蓀，王偉.基于模型檢測(cè)的時(shí)間空間性能驗(yàn)證方法 ［J］.計(jì)算機(jī)學(xué)報(bào)，2010，33 （9）：1621－1633.］

［6］Jaghoori M M，Sirjani M，Mousavi M R，et al.Symmetry and partial order reduction techniques in model checking rebeca ［J］.Acta Informatica，2010 （47）：33－66.

［7］Donaldson A F，Miller A，Parker D.Language level symmetry reduction for probabilistic model checking ［C］／／Proceedings of the Sixth International Conference on the Quantitative Evaluation of Systems.Washington DC，USA：IEEE Computer Society，2009：289－298.

［8］Marta Kwiatkowska，Gethin Norman，David Parker.Symmetry reduction for probabilistic model checking ［C］／／Proceedings of the 18th International Conference on Computer Aided Verification.Seattle，United States：Springer－Verlag，2006：7－20.

［9］YAO Quanzhu，WEI Xiaoyong.Improved algorithm of PRE■operation in symbolic model checking based on OBDD ［J］.Computer Engineering，2008（14）：69－71 （in Chinese）.［姚全珠，魏小勇.基于OBDD的SMC中PRE■操作的改進(jìn)算法［J］.計(jì)算機(jī)工程，2008（14）：69－71.］

［10］Clarke E M，Emerson E A，Sifakis J.Model checking：Algorithmic verification and debugging ［J］.Communications of the ACM 2009，52（11）：74－84.