一種基于MDDs的可達狀態的算法研究

段珊，王金娟

（湖南涉外經濟學院信息科學與工程學部，長沙 410025）

一種基于MDDs的可達狀態的算法研究

段珊，王金娟

（湖南涉外經濟學院信息科學與工程學部，長沙 410025）

以固定點為數學基礎，多值決策圖（Multi-Valued Decision Diagrams，MDDs）為存儲結構來實現系統可達狀態空間建立的飽和算法在異步系統的模型中顯示其良好的空間和時間效應。對該算法的理論和實現方法進行詳細的闡述和分析，提出通過對當前事件中的擴展鏈的預先判斷，修改原飽和算法來實現取消無擴展鏈的事件的函數遞歸調用、新節點的內存空間的申請與回收，達到提高算法的時間和空間效率；并從理論推理和實驗上進行驗證。

可達狀態；固定點；飽和算法；MDDs

0 引言

可達狀態空間的計算與存儲是形式化驗證工具必需面對的關鍵性問題，例如模型檢測器，它需要窮盡系統的所有可達狀態來實現系統性質的確認。隨著所研究系統的復雜化，如何構建和存儲巨大的狀態空間是當前數字系統一個瓶頸。以BDD[1]為代表的符號技術使符號模型檢測[2]技術在同步系統中運用取得了較大的成功。但在異步系統中，由于事件行為交替執行的不確定性，它依然不得不面臨空間狀態的爆炸問題。

Ciardo和Andrew在SMART[3]（Stochastic Model checking Analyzer for Reliability and Timing）這個模型檢測工具中采用了一種基于MDDs[4]存儲結構，利用不動點理論計算可達狀態的飽和算法[5-6]。該算法針對分布式異步系統的特性，通過對其高層模型的邏輯結構在MDD結構上的映射關系的定義，采用有效的迭代策略實現了可達狀態空間的存儲與建立。實驗證明通過在一些高層次的系統模型，例如Petri網[7]，MARKOV鏈[8]的運用，顯示了該算法比其他通用的可達狀態算法（BFS和DFS）在時間上和空間上的高效[9]。本文對該算法的原理與實現進行闡述，提出了基于當前事件的擴展鏈的預先判斷的新飽和算法，并通過理論推理和實驗進行了論證。

1 系統狀態模型的描述

●s：系統的初始狀態。

N為各事件的遷移函數的邏輯和，即N（i）=∪а∈εNα（i），Nα：與事件α關聯的遷移函數，α∈ε，ε表示系統有限的事件集合。Nα（i）為系統狀態i在α事件發生時系統遷移到的狀態。如果Nα（i）≠Φ表明事件α在狀態i可被激活；若Nα（i）=i，表明事件α不影響狀態i。

1.1 狀態的符號表示與操作

飽和算法采用MDDs來實現可達狀態空間的建立和存儲。MDDs由一個根節點，一個或多個非終節點，兩個0和1的終節點構成。與BDD不同的是，它的每個節點可以有多個取值，每個節點可以有多條引出邊。與BDD相比，MDD更能直接、緊湊的描述一個由K個子系統組成的異步系統的狀態。K個子系統用K個變量表示，分布在K到1層，子系統的狀態值即變量的取值，系統狀態的K元組（iK，…，i1）直接對應MDD的K層到1層任意路徑上的變量取值。

系統的節點采用＜k，p＞形式表示，k表示節點所在的層，p為該節點在本層的唯一標識。K層只包含一個根節點，K-1到1層包含一或多個非終節點。0層有兩個終節點＜0，0＞和＜0，1＞。

每個非終節點＜k，p＞可以有|?k|條引出邊指向k-1或下層的節點。若有一條邊，邊上的值為i，i∈Sk，指向節點〈k-1，q＞，則寫成＜k，p＞[i]=q。與BDD不同，MDD允許存在冗余節點，也就是他們的所有邊指向同一節點，但不能存在復制節點（若同一層中節點＜k，p＞、＜k，q＞，對任意的i∈Sk，有＜k，p＞[i]=＜k，q＞[i]。這樣的節點稱為復制節點）。

圖1為一具有四個子系統模型狀態的MDD表示。

圖1 一個四個變量的MDD和它表示的狀態

同OBDD類似，MDD所表示的狀態操作可以直接由MDD的操作簡單來實現[11]，并操作是飽和算法中最常用的MDD操作，同BDD的并操作類似。

1.2 遷移函數的符號表示

基于事件的異步系統中，遷移函數反映著事件的行為。當事件α對每個子模塊的作用相互獨立時，事件α的遷移函數可以寫成子模塊的Kronecker積的形式。即Na=X…X，其中稱為事件α在子模塊k上的遷移函數。

遷移函數可以采用MDD描述，也可以采用矩陣MxDs（Matrix Diagrams）表示[12]。同BDD描述遷移關系類似，MDD需要用雙倍數的層變量表示遷移關系。MxDs與MDDs結構類似，每一層對應一個|Sk|*|Sk|的0，1矩陣描述該層的狀態變遷，行表示當前狀態值，列表示下一狀態值，若行列對應的遷移存在，該位置引出值為1的邊指向下一層的遷移函數矩陣；如某層不存在狀態變遷，該層的遷移函數I，上層的引出邊可以跳過該層直接指向下層。MxDs能很好描述滿足Kronecker積的事件遷移函數。遷移函數N1（001）={101}，N2（011）={111}，N3（021）={121}，N4（101）={200，201}，N5（111）={210，211}，N6（121）={220，221}。

圖2 MxDs和MDDs表示遷移函數

2 飽和算法

飽和算法以固定點的數學理論為基礎，基于MDDs結構模型的節點迭代算法。從初始狀態的MDD出發，按一定的順序迭代使用事件的遷移函數擴展狀態來實現可達狀態空間建立，直到不再增加新的狀態。

飽和算法是以事件的遷移函數滿足Kronecker積為條件的，對系統中不滿足該條件的事件，可以通過合理的分解、合并來達到這一要求[12]。另外為了減少飽和算法迭代次數，往往依據事件對層的依賴關系對事件進行分類，為此提出一些相關概念。

對所有i∈Sk，若（i）=i，則α不依賴k層，=I。若存在i，j∈Sk，（i）≠j，α依賴k層，≠I。

εk={α∈ε:First（α）=k}最高依賴層為k的事件集合；

N*≤K:top（α）≤k的事件的遷移函數。

2.1 飽和算法實現

定義1飽和節點，一個MDD節點B＜k，p＞在k層是飽和的，當且僅當對所有α∈{α：top（α）≤k}事件的執行不會為該節點增加任何新狀態，B（＜k，p＞）=（B（＜k，p＞）成立。

推論1：若B＜k，p＞節點是飽和的，則這從＜k，p＞點所能到達的節點都是飽和的。

推論2：若B＜k，p＞，B＜k，q＞兩節點是飽和的，則B＜k，p＞∪B＜k，q＞是飽和的。

為了減少節點飽和中的遞歸次數，盡可能先飽和下層節點。飽和算法的基本方法自下而上依次飽和節點。

①建立一個L層的MDD，表示系統的初始狀態s。

②將第一層的節點飽和化，執行ε1事件的變遷函數（i）擴展節點；

③將第二層的節點飽和化，執行ε2中事件的變遷函數（i）擴展節點；如果在第一層創建了新的節點，同時將它飽和化；

④將第三層的節點飽和化，執行ε3中事件的變遷函數（i）擴展節點；，如果在第二層、第一層創建了新的節點，同時將它們飽和化；

⑤將L層根節點飽和化，通過執行εL中事件的變遷函數（i）擴展節點；，若在第L-1，L-2，…層創建了新節點，同時將它們飽和化。

為了簡單起見，本文中只對單個節點的飽和算法進行了描述，并不對整個系統狀態節點生成進行描述。

算法主要由兩個函數來實現，Saturate（＜k，p＞）使用α∈εk事件來飽和B＜k.，r＞節點時，先通過調用Recfire函數遞歸調用完成下層節點在α事件下的擴展飽和，然后再返回該層實施該層的節點飽和。

為降低算法復雜度，算法中定義一些相關的hash表對飽和算法中的運算結果和中間過程進行記錄。唯一表UT[k]，存放k層唯一節點，對于已飽和化的k層節點，先檢查UT[K]表，若該節點已存在，則刪除新飽和化的節點，返回表中的原節點，否則新節點插入UT[K]表；k層的并運算表UC[K]，存放＜k，p＞、＜k，q＞并運算后的返回結果＜k，s＞，即B（k，s）=B（k，p）∪B（k，q）；FC [k]記錄k層的已擴展的節點，＜k.q＞在α事件的作用下建立新的并飽和化的節點＜k，s＞后（注意First（α）＞k，并且B（k，s）=（Nα（B（＜k，p＞）））），要將條目（FC[k]，{q，e}，s）插入FC[k]中。以便下次需要擴展時，不需要重復計算，根據從該條目直接返回結果。

2.2 新飽和算法

飽和算法的時間和空間效率取決于符號狀態產生的迭代次數。迭代的次數與當前狀態、事件遷移函數密切相關。實際系統中引發當前狀態變遷的事件往往是少數，事件對節點進行狀態擴展飽和之前，判斷該事件中是否存在擴展鏈，減少無擴展鏈的迭代是提高飽和算法效率的方向之一。

定義2可擴展狀態，節點＜k，p＞中存在狀態i，＜k，p＞[i]≠0，且[i，j]≠Ф，則稱i為α事件的可擴展狀態。

＜k|p＞[i]稱為當前結點，由當前節點中的可擴展狀態指向的下層節點為下層的當前節點。

定義4擴展鏈，若α事件在所有k層（last（α）≤k≤top（α））的當前節點中存在α事件的可擴展狀態，則α事件中存在擴展鏈。

擴展鏈的依據是事件的遷移函數滿足Kronecker積為條件。

只有α事件中存在當前狀態的擴展鏈，才能實現當前狀態的擴展飽和。原飽和算法是通過Recfire函數的遞歸調用來實現對下層當前節點的擴展。在遞推過程中若遇到某層當前節點為非擴展狀態，即刻依次返回到最初調用點。最壞的情況是遞推深入到k=last（α）層時，當前節點中不存在α事件的可擴展狀態，則必須從該層開始逐層向上返回退出，顯然此時前面的調用都是無效調用，創建的新節點也需依次回收。

為了減少這種無效的迭代調用，本文提出在用α事件對當前節點B＜k，p＞擴展飽和之前，先確認它是否存在擴展鏈。若是，則調用Recfire函數的依次進入當前節點下層，進行擴展。若不是，則不進入。進入Recfire函數后，要窮盡該當前節點中所有可擴展狀態，并對下層的不同節點的分支擴展鏈進行判斷和提取，若不存在及時退出，存在則繼續進入不同分支，以便在返回時窮盡所有可能飽和所有節點。根據這樣的思想在Saturate和Recfire函數中引入了一個新的函數Even_Enable，并對這兩個函數實現做相應的修改。

Even_Enable函數描述了α事件在＜k|p＞節點是否存在擴展鏈的判斷算法。其基本思想從＜k|p＞節點開始對當前節點的可擴展狀態進行搜索，若存在則直接進入該當前節點的各下層當前節點進行搜索，重復這個過程，直到到返回false或者1；查找擴展鏈時只要找到當前節點的一個擴展狀態后就進入當前節點的下層，若當前分支節點無擴展狀態，則進入當前節點的另外一節點，進入另一分支繼續尋找。

如果能進入k=last（α）-1層，則當前節點＜k|p＞存在擴展鏈，返回1，否則就會在窮盡了某層的當前結點的所有分支后返回false，＜k|p＞節點無擴展鏈。

擴展鏈的提前判斷，減少Recfire無效調用的次數和內存空間的申請與回收，從而提高時間、空間效率。

//Ecng當前分支擴展鏈標識；

Saturate函數的修改，實現了無擴展鏈事件的及時退出；Recfire函數的修改保證了對下層擴展鏈分支進行及時判斷和提取，若不存在分支鏈，退出分支擴展鏈，否則同時進入不同的分支鏈，既消除了無擴展鏈分支的進入也保證了盡可能飽和所有下層節點。

2.3 算法驗證

下面實例直觀的呈現了利用新飽和算法實現可達狀態的MDDs的建立過程。實例初始狀態為（0，0，0，0），各事件對狀態的影響及遷移函數見下表。

表1 事件遷移表

“*”表示該層不受事件的影響，遷移函數的表示見圖3。

圖3 遷移函數的MxDs表示

圖4用圖示的方法直觀的展示了新飽和算法完成可達狀態空間的建立過程。

①系統的遷移函數的MxDs如圖3。初始狀態（0，0，0，0）的MDD表示如圖4-a。

②依據飽和算法首先從從底部的節點＜1，1＞開始，該節點中存在可擴展狀態0，事件α1存在有效擴展鏈，直接調用Recfire函數擴展了當前節點＜1，1＞，增加了兩個狀態1，2。見圖（4-b）;

③飽和＜2，1＞節點，該節點中存在α2的可擴展狀態0，Evalid（1，＜2，1＞[0]，Nα21）返回1，α2中存在擴展鏈。Saturate函數調用Recfire（α2，1，＜2，1＞[0]）在下層創建新的節點＜1，2＞，第一層的當前節點＜2，1＞[0]存在α2的可擴展狀態1，Recfire自身調用Recfire（α2，0，＜1，1＞[1]），因k=0＜last（α），從本層結束遞推并開始向上返回，返回中完成本層新建節點＜1，2＞的狀態3添加和飽和。并將已飽和的節點在FC[1]表中進行記錄。見圖4-c。

④Saturate（3，1＞，該節點中存在α3的可擴展狀態0，Saturate調用Evalid（2，＜3，1＞[0]，Nα32）函數，返回值1，判斷α3中存在擴展鏈，調用Recfire進入下層節點的擴展和飽和。依次在第一層、第二層建立了新的節點＜1，3＞、＜2，2＞，并將它們飽和，在FC[1]、FC[2]表中進行記錄。返回到節點＜3，1＞后，節點新狀態1成為α3的可擴展狀態，Saturate再次調用Evalid（2，＜3，1＞[0]，Nα32）函數，返回值0，表明當前狀態下，α3不存在擴展鏈，返回。重復④直到沒有新的節點產生。見圖4-d。

⑤同樣方法用α4，α5對節點＜4.1＞進行飽和，最終的狀態空間的MDDS如圖4-e。

圖4 飽和算法執行

最后的可達狀態空間{0000，0001，0002，0013，0122，1213，2213}

上述飽和過程采用了新飽和算法，在Saturate函數還沒調用Recfire函數之前，一次性的利用Evalid函數來判斷當前事件中是否存在擴展鏈。若有，則調用Recfire函數進入下層當前節點的做進一步分支擴展鏈判斷。否則及時退出。

用C語言對新算法和原算法進行了編程實現，并在多個典型事例上運行，統計了兩種算法中調用Recfire函數的次數。

表2列出了幾個實例運行中的Recfire函數的調用情況，一般來說系統中的層變量越多，當前無擴展鏈情況越多，新算法的優越性越明顯。

表2 實例運行結果

3 結語

Ciardo、Andrew提出的以固定點為依據、基于MDD結構的飽和算法在異步系統模型例如Petri Net、Markov鏈等中顯示它較好的空間和時間特性。本文詳細的闡述了飽和算法理論依據、實現方法；提出了通過對當前事件的擴展鏈進行預先判斷，只有在當前事件中存在擴展鏈時才用Recfire函數來繼續下層節點分支擴展鏈的提取判斷，以便回歸時進行擴展、飽和；取消無擴展鏈的事件的Refire函數的遞歸調用、新節點的內存空間的申請與回收，理論推理分析和實驗證明了新飽和算法的有效性。

[1]R.E.Bryant.Graph-Based Algorithms for Boolean Function Manipulation.IEEE Trans.Comp.，35（8）:677-691，Aug.1986.

[2]J.R.Burch，E.M.Clarke，D.E.Long.Symbolic Model Checking with Partitioned Transition Relations.In A.Halaas and P.B.Denyer，Editors，Int.Conference on Very Large Scale Integration，pages 49-58，Edinburgh，Scotland，Aug.1991.IFIP Transactions，North--Holland.

[3]G.Ciardo，R.L.Jones，A.S.Miner，R.Siminiceaunu.Logical and Stochastic Modeling with SMART.In Proc.Modelling Techniques and Tools for Computer Performance Evaluation，LNCS 2794，pages 78-97，Urbana，IL，USA，Sept.2003.Springer-Verlag.

[4]T.Kam，T.Villa，R.Brayton，A.Sangiovanni-Vincentelli.Multi-Valued Decision Diagrams:Theory and Applications.Multiple-Valued Logic，4（1-2）:9-62，1998.

[5]Ciardo，G.，Marmorstein，R.，&Siminiceanu，R..The Saturation Algorithm for Symbolic State-Space Exploration.International Journal on Software Tools for Technology Transfer，8（1），4-25，2006.

[6]Andrew S.Miner.Saturation for a General Class of Models.IEEE Trans.Softw.Eng.，32（8）:559-570，August 2006.

[7]吳哲輝.Petri網導論.北京：機械工業出版社，2006.4

[8]Min Wan，Gianfranco Ciardo，Andrew S.Miner.Approximate Steady-State Analysis of Large Markov Models Based on the Structure of Their Decision Diagram Encoding.Perf.Eval.，68（5）:463-486，2011.

[9]G.Ciardo，R.L.Jones，A.S.Miner，R.Siminiceanu.Logical and Stochastic Modeling with SMART.Perf.Eval.，63:578-608，2006.

[10]P.Buchholz，G.Ciardo，S.Donatelli，P.Kemper.Complexity of Memory-Efficient Kronecker Operations with Applications to the Solution of Markov Models.IN-FORMS J.Comp.，12（3）:203-222，2000.

[11]T.Kam，T.Villa，R.Brayton，A.Sangiovanni-Vincentelli.Multi-Valued Decision Diagrams:Theory and Applications.Multiple-Valued Logic，4（1-2）:9-62，1998.

[12]Andrew S.Miner.Implicit GSPN Reachability Set Generation Using Decision Diagrams.Perf.Eval.，56（1-4）:145-165，March 2004.

Research on the Algorithm for Reachable State Based on MDDs

DUAN Shan，WANG Jin-juan

（Hunan International Economics University，Changsha 410205）

On the mathematical basis of fixed point,MDDs are good for storage structure to realize the computation of reachable state space;the saturation algorithm shows its good in space and time effect in asynchronous system.Presents the theory and implementation method of the algorithm in detail and analysis,and puts forward a method that prejudge extension chain of the current event,modifies the original saturate event to call for recursive function to realize the expansion of the lower nodes and saturation algorithm to cancel the calling for function,applying and recycle of new node for memory without extension chain,so as to improve the efficiency of the algorithm of time and space.The new method is proved from the theoretical analysis and experiment.

Reachable State Space;Fixed Point;Saturation Algorithm;MDDs

1007-1423（2016）35-0043-07

10.3969/j.issn.1007-1423.2016.35.009

2016-11-22

2016-12-05

段珊，碩士，研究方向為形式化驗證、高性能計算

王金娟（1981-），女，湖南長沙人，碩士，系統分析師，研究方向為軟件工程技術與應用