基于決策圖的復雜系統模型對稱約減方法

紀明宇，王海濤，陳志遠，李艷梅

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

0 引 言

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

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

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

1 基本概率模型

定義1 DTMC

DTMC為五元組Μ ＝ （S，P，L，AP，v），其中S表示狀態集合，P：S×S→［0，1］為狀態轉移概率矩陣，對于狀態集的狀態s，有 ∑s＇∈Sp（s，s＇）＝1，L：S→2AP為狀態標記函數，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的基礎上增加了遷移動作集合A和一個用于表示遷移資源消耗的遷移回報結構N：S×A×S→R≥0后構成的。

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

2 模型MTBDD表示

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

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

例1 隨機系統模型MTBDD舉例

圖1表示一個由4個狀態構成的DTMC，其狀態遷移MTBDD表示如圖2所示。

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

圖1 DTMC模型舉例

圖2 DTMC模型MTBDD表示

3 DTMRDP模型對稱約減

對于本文描述的DTMRDP模型，由于在狀態遷移過程中，伴隨著多種復雜特征信息，因此其對稱約減方法有別于一般的非概率遷移系統。

定義3 自同構

若遷移系統M＝（S，R），其中S為狀態的有限集，遷移關系RS×S，則狀態空間S上的自同構表示為π：S→S，且滿足：如果 （s，s＇）∈R ，則 （π（s），π（s＇））∈R 。

定義4 等價關系

對于給定的一組自同構G，狀態空間S的等價關系θ表示為 （s，π（s））∈θ。

定義5 遷移系統商

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

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

定義6 DTMC商模型

定義7 DTMRDP商模型

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

在DTMC及DTMRDP商模型的定義中，由于標記函數、原子命題、初始狀態與商模型構造無關，所以在商模型構造中并未對它們進行具體說明。

例2 DTMRDP模型對稱約減示例

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

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

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

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

圖3 對稱進程DTMRDP模型

圖4 等價關系唯一表示函數

4 算法描述

圖5 對稱約減商DTMRDP模型

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

狀態遷移矩陣的對稱約減算法：

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

5 實例說明

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

依據本文提出的算法，相應的模型遷移矩陣對稱約減轉換過程見圖7（a）至圖7（d）。

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

圖6 約減前狀態遷移MTBDD表示

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

圖8 約減后狀態遷移MTBDD表示

6 結束語

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

［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）.［吳立軍，蘇金樹，蘇開樂.多智能體系統時態認知規范高效符號模型檢測的算法研究 ［J］.計算機學報，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）.［馬亞南，劉楠，祝躍飛，等.安全協議狀態空間的束動作偏序約簡算法 ［J］.計算機應用研究，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］.軟件學報，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］.計算機學報，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.