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

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

0 引 言

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

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

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

1 基本概率模型

定義1 DTMC

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

下面基于DTMC給出支持遷移回報的離散時間Markov 判 定 過 程 （Discrete Time Markov Rewards Decision Process，DTMRDP）的定義。

定義2 DTMRDP

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

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

2 模型MTBDD表示

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

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

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

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

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

圖1 DTMC模型舉例

圖2 DTMC模型MTBDD表示

3 DTMRDP模型對稱約減

對于本文描述的DTMRDP模型，由于在狀態(tài)遷移過程中，伴隨著多種復(fù)雜特征信息，因此其對稱約減方法有別于一般的非概率遷移系統(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 等價關(guān)系

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

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

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

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

定義6 DTMC商模型

定義7 DTMRDP商模型

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

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

例2 DTMRDP模型對稱約減示例

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

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

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

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

圖3 對稱進程DTMRDP模型

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

4 算法描述

圖5 對稱約減商DTMRDP模型

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

狀態(tài)遷移矩陣的對稱約減算法：

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

5 實例說明

對于圖3所示的對稱進程DTMRDP模型，該模型的遷移矩陣MTBDD表示如圖6所示。

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

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

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

圖7 遷移矩陣對稱約減算法實例說明

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

6 結(jié)束語

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

［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）.［吳立軍，蘇金樹，蘇開樂.多智能體系統(tǒng)時態(tài)認(rèn)知規(guī)范高效符號模型檢測的算法研究 ［J］.計算機學(xué)報，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)空間的束動作偏序約簡算法 ［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）.［周從華，劉志鋒，王昌達.概率計算樹邏輯的限界模型檢測［J］.軟件學(xué)報，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）. ［鈕俊，曾國蓀，王偉.基于模型檢測的時間空間性能驗證方法 ［J］.計算機學(xué)報，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］.計算機工程，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.