一種基于MDDs的可達(dá)狀態(tài)的算法研究

段珊，王金娟

（湖南涉外經(jīng)濟(jì)學(xué)院信息科學(xué)與工程學(xué)部，長沙 410025）

一種基于MDDs的可達(dá)狀態(tài)的算法研究

段珊，王金娟

（湖南涉外經(jīng)濟(jì)學(xué)院信息科學(xué)與工程學(xué)部，長沙 410025）

以固定點(diǎn)為數(shù)學(xué)基礎(chǔ)，多值決策圖（Multi-Valued Decision Diagrams，MDDs）為存儲(chǔ)結(jié)構(gòu)來實(shí)現(xiàn)系統(tǒng)可達(dá)狀態(tài)空間建立的飽和算法在異步系統(tǒng)的模型中顯示其良好的空間和時(shí)間效應(yīng)。對(duì)該算法的理論和實(shí)現(xiàn)方法進(jìn)行詳細(xì)的闡述和分析，提出通過對(duì)當(dāng)前事件中的擴(kuò)展鏈的預(yù)先判斷，修改原飽和算法來實(shí)現(xiàn)取消無擴(kuò)展鏈的事件的函數(shù)遞歸調(diào)用、新節(jié)點(diǎn)的內(nèi)存空間的申請(qǐng)與回收，達(dá)到提高算法的時(shí)間和空間效率；并從理論推理和實(shí)驗(yàn)上進(jìn)行驗(yàn)證。

可達(dá)狀態(tài)；固定點(diǎn)；飽和算法；MDDs

0 引言

可達(dá)狀態(tài)空間的計(jì)算與存儲(chǔ)是形式化驗(yàn)證工具必需面對(duì)的關(guān)鍵性問題，例如模型檢測(cè)器，它需要窮盡系統(tǒng)的所有可達(dá)狀態(tài)來實(shí)現(xiàn)系統(tǒng)性質(zhì)的確認(rèn)。隨著所研究系統(tǒng)的復(fù)雜化，如何構(gòu)建和存儲(chǔ)巨大的狀態(tài)空間是當(dāng)前數(shù)字系統(tǒng)一個(gè)瓶頸。以BDD[1]為代表的符號(hào)技術(shù)使符號(hào)模型檢測(cè)[2]技術(shù)在同步系統(tǒng)中運(yùn)用取得了較大的成功。但在異步系統(tǒng)中，由于事件行為交替執(zhí)行的不確定性，它依然不得不面臨空間狀態(tài)的爆炸問題。

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

1 系統(tǒng)狀態(tài)模型的描述

●s：系統(tǒng)的初始狀態(tài)。

N為各事件的遷移函數(shù)的邏輯和，即N（i）=∪а∈εNα（i），Nα：與事件α關(guān)聯(lián)的遷移函數(shù)，α∈ε，ε表示系統(tǒng)有限的事件集合。Nα（i）為系統(tǒng)狀態(tài)i在α事件發(fā)生時(shí)系統(tǒng)遷移到的狀態(tài)。如果Nα（i）≠Φ表明事件α在狀態(tài)i可被激活；若Nα（i）=i，表明事件α不影響狀態(tài)i。

1.1 狀態(tài)的符號(hào)表示與操作

飽和算法采用MDDs來實(shí)現(xiàn)可達(dá)狀態(tài)空間的建立和存儲(chǔ)。MDDs由一個(gè)根節(jié)點(diǎn)，一個(gè)或多個(gè)非終節(jié)點(diǎn)，兩個(gè)0和1的終節(jié)點(diǎn)構(gòu)成。與BDD不同的是，它的每個(gè)節(jié)點(diǎn)可以有多個(gè)取值，每個(gè)節(jié)點(diǎn)可以有多條引出邊。與BDD相比，MDD更能直接、緊湊的描述一個(gè)由K個(gè)子系統(tǒng)組成的異步系統(tǒng)的狀態(tài)。K個(gè)子系統(tǒng)用K個(gè)變量表示，分布在K到1層，子系統(tǒng)的狀態(tài)值即變量的取值，系統(tǒng)狀態(tài)的K元組（iK，…，i1）直接對(duì)應(yīng)MDD的K層到1層任意路徑上的變量取值。

系統(tǒng)的節(jié)點(diǎn)采用＜k，p＞形式表示，k表示節(jié)點(diǎn)所在的層，p為該節(jié)點(diǎn)在本層的唯一標(biāo)識(shí)。K層只包含一個(gè)根節(jié)點(diǎn)，K-1到1層包含一或多個(gè)非終節(jié)點(diǎn)。0層有兩個(gè)終節(jié)點(diǎn)＜0，0＞和＜0，1＞。

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

圖1為一具有四個(gè)子系統(tǒng)模型狀態(tài)的MDD表示。

圖1 一個(gè)四個(gè)變量的MDD和它表示的狀態(tài)

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

1.2 遷移函數(shù)的符號(hào)表示

基于事件的異步系統(tǒng)中，遷移函數(shù)反映著事件的行為。當(dāng)事件α對(duì)每個(gè)子模塊的作用相互獨(dú)立時(shí)，事件α的遷移函數(shù)可以寫成子模塊的Kronecker積的形式。即Na=X…X，其中稱為事件α在子模塊k上的遷移函數(shù)。

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

圖2 MxDs和MDDs表示遷移函數(shù)

2 飽和算法

飽和算法以固定點(diǎn)的數(shù)學(xué)理論為基礎(chǔ)，基于MDDs結(jié)構(gòu)模型的節(jié)點(diǎn)迭代算法。從初始狀態(tài)的MDD出發(fā)，按一定的順序迭代使用事件的遷移函數(shù)擴(kuò)展?fàn)顟B(tài)來實(shí)現(xiàn)可達(dá)狀態(tài)空間建立，直到不再增加新的狀態(tài)。

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

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

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

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

2.1 飽和算法實(shí)現(xiàn)

定義1飽和節(jié)點(diǎn)，一個(gè)MDD節(jié)點(diǎn)B＜k，p＞在k層是飽和的，當(dāng)且僅當(dāng)對(duì)所有α∈{α：top（α）≤k}事件的執(zhí)行不會(huì)為該節(jié)點(diǎn)增加任何新狀態(tài)，B（＜k，p＞）=（B（＜k，p＞）成立。

推論1：若B＜k，p＞節(jié)點(diǎn)是飽和的，則這從＜k，p＞點(diǎn)所能到達(dá)的節(jié)點(diǎn)都是飽和的。

推論2：若B＜k，p＞，B＜k，q＞兩節(jié)點(diǎn)是飽和的，則B＜k，p＞∪B＜k，q＞是飽和的。

為了減少節(jié)點(diǎn)飽和中的遞歸次數(shù)，盡可能先飽和下層節(jié)點(diǎn)。飽和算法的基本方法自下而上依次飽和節(jié)點(diǎn)。

①建立一個(gè)L層的MDD，表示系統(tǒng)的初始狀態(tài)s。

②將第一層的節(jié)點(diǎn)飽和化，執(zhí)行ε1事件的變遷函數(shù)（i）擴(kuò)展節(jié)點(diǎn)；

③將第二層的節(jié)點(diǎn)飽和化，執(zhí)行ε2中事件的變遷函數(shù)（i）擴(kuò)展節(jié)點(diǎn)；如果在第一層創(chuàng)建了新的節(jié)點(diǎn)，同時(shí)將它飽和化；

④將第三層的節(jié)點(diǎn)飽和化，執(zhí)行ε3中事件的變遷函數(shù)（i）擴(kuò)展節(jié)點(diǎn)；，如果在第二層、第一層創(chuàng)建了新的節(jié)點(diǎn)，同時(shí)將它們飽和化；

⑤將L層根節(jié)點(diǎn)飽和化，通過執(zhí)行εL中事件的變遷函數(shù)（i）擴(kuò)展節(jié)點(diǎn)；，若在第L-1，L-2，…層創(chuàng)建了新節(jié)點(diǎn)，同時(shí)將它們飽和化。

為了簡單起見，本文中只對(duì)單個(gè)節(jié)點(diǎn)的飽和算法進(jìn)行了描述，并不對(duì)整個(gè)系統(tǒng)狀態(tài)節(jié)點(diǎn)生成進(jìn)行描述。

算法主要由兩個(gè)函數(shù)來實(shí)現(xiàn)，Saturate（＜k，p＞）使用α∈εk事件來飽和B＜k.，r＞節(jié)點(diǎn)時(shí)，先通過調(diào)用Recfire函數(shù)遞歸調(diào)用完成下層節(jié)點(diǎn)在α事件下的擴(kuò)展飽和，然后再返回該層實(shí)施該層的節(jié)點(diǎn)飽和。

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

2.2 新飽和算法

飽和算法的時(shí)間和空間效率取決于符號(hào)狀態(tài)產(chǎn)生的迭代次數(shù)。迭代的次數(shù)與當(dāng)前狀態(tài)、事件遷移函數(shù)密切相關(guān)。實(shí)際系統(tǒng)中引發(fā)當(dāng)前狀態(tài)變遷的事件往往是少數(shù)，事件對(duì)節(jié)點(diǎn)進(jìn)行狀態(tài)擴(kuò)展飽和之前，判斷該事件中是否存在擴(kuò)展鏈，減少無擴(kuò)展鏈的迭代是提高飽和算法效率的方向之一。

定義2可擴(kuò)展?fàn)顟B(tài)，節(jié)點(diǎn)＜k，p＞中存在狀態(tài)i，＜k，p＞[i]≠0，且[i，j]≠Ф，則稱i為α事件的可擴(kuò)展?fàn)顟B(tài)。

＜k|p＞[i]稱為當(dāng)前結(jié)點(diǎn)，由當(dāng)前節(jié)點(diǎn)中的可擴(kuò)展?fàn)顟B(tài)指向的下層節(jié)點(diǎn)為下層的當(dāng)前節(jié)點(diǎn)。

定義4擴(kuò)展鏈，若α事件在所有k層（last（α）≤k≤top（α））的當(dāng)前節(jié)點(diǎn)中存在α事件的可擴(kuò)展?fàn)顟B(tài)，則α事件中存在擴(kuò)展鏈。

擴(kuò)展鏈的依據(jù)是事件的遷移函數(shù)滿足Kronecker積為條件。

只有α事件中存在當(dāng)前狀態(tài)的擴(kuò)展鏈，才能實(shí)現(xiàn)當(dāng)前狀態(tài)的擴(kuò)展飽和。原飽和算法是通過Recfire函數(shù)的遞歸調(diào)用來實(shí)現(xiàn)對(duì)下層當(dāng)前節(jié)點(diǎn)的擴(kuò)展。在遞推過程中若遇到某層當(dāng)前節(jié)點(diǎn)為非擴(kuò)展?fàn)顟B(tài)，即刻依次返回到最初調(diào)用點(diǎn)。最壞的情況是遞推深入到k=last（α）層時(shí)，當(dāng)前節(jié)點(diǎn)中不存在α事件的可擴(kuò)展?fàn)顟B(tài)，則必須從該層開始逐層向上返回退出，顯然此時(shí)前面的調(diào)用都是無效調(diào)用，創(chuàng)建的新節(jié)點(diǎn)也需依次回收。

為了減少這種無效的迭代調(diào)用，本文提出在用α事件對(duì)當(dāng)前節(jié)點(diǎn)B＜k，p＞擴(kuò)展飽和之前，先確認(rèn)它是否存在擴(kuò)展鏈。若是，則調(diào)用Recfire函數(shù)的依次進(jìn)入當(dāng)前節(jié)點(diǎn)下層，進(jìn)行擴(kuò)展。若不是，則不進(jìn)入。進(jìn)入Recfire函數(shù)后，要窮盡該當(dāng)前節(jié)點(diǎn)中所有可擴(kuò)展?fàn)顟B(tài)，并對(duì)下層的不同節(jié)點(diǎn)的分支擴(kuò)展鏈進(jìn)行判斷和提取，若不存在及時(shí)退出，存在則繼續(xù)進(jìn)入不同分支，以便在返回時(shí)窮盡所有可能飽和所有節(jié)點(diǎn)。根據(jù)這樣的思想在Saturate和Recfire函數(shù)中引入了一個(gè)新的函數(shù)Even_Enable，并對(duì)這兩個(gè)函數(shù)實(shí)現(xiàn)做相應(yīng)的修改。

Even_Enable函數(shù)描述了α事件在＜k|p＞節(jié)點(diǎn)是否存在擴(kuò)展鏈的判斷算法。其基本思想從＜k|p＞節(jié)點(diǎn)開始對(duì)當(dāng)前節(jié)點(diǎn)的可擴(kuò)展?fàn)顟B(tài)進(jìn)行搜索，若存在則直接進(jìn)入該當(dāng)前節(jié)點(diǎn)的各下層當(dāng)前節(jié)點(diǎn)進(jìn)行搜索，重復(fù)這個(gè)過程，直到到返回false或者1；查找擴(kuò)展鏈時(shí)只要找到當(dāng)前節(jié)點(diǎn)的一個(gè)擴(kuò)展?fàn)顟B(tài)后就進(jìn)入當(dāng)前節(jié)點(diǎn)的下層，若當(dāng)前分支節(jié)點(diǎn)無擴(kuò)展?fàn)顟B(tài)，則進(jìn)入當(dāng)前節(jié)點(diǎn)的另外一節(jié)點(diǎn)，進(jìn)入另一分支繼續(xù)尋找。

如果能進(jìn)入k=last（α）-1層，則當(dāng)前節(jié)點(diǎn)＜k|p＞存在擴(kuò)展鏈，返回1，否則就會(huì)在窮盡了某層的當(dāng)前結(jié)點(diǎn)的所有分支后返回false，＜k|p＞節(jié)點(diǎn)無擴(kuò)展鏈。

擴(kuò)展鏈的提前判斷，減少Recfire無效調(diào)用的次數(shù)和內(nèi)存空間的申請(qǐng)與回收，從而提高時(shí)間、空間效率。

//Ecng當(dāng)前分支擴(kuò)展鏈標(biāo)識(shí)；

Saturate函數(shù)的修改，實(shí)現(xiàn)了無擴(kuò)展鏈?zhǔn)录募皶r(shí)退出；Recfire函數(shù)的修改保證了對(duì)下層擴(kuò)展鏈分支進(jìn)行及時(shí)判斷和提取，若不存在分支鏈，退出分支擴(kuò)展鏈，否則同時(shí)進(jìn)入不同的分支鏈，既消除了無擴(kuò)展鏈分支的進(jìn)入也保證了盡可能飽和所有下層節(jié)點(diǎn)。

2.3 算法驗(yàn)證

下面實(shí)例直觀的呈現(xiàn)了利用新飽和算法實(shí)現(xiàn)可達(dá)狀態(tài)的MDDs的建立過程。實(shí)例初始狀態(tài)為（0，0，0，0），各事件對(duì)狀態(tài)的影響及遷移函數(shù)見下表。

表1 事件遷移表

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

圖3 遷移函數(shù)的MxDs表示

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

①系統(tǒng)的遷移函數(shù)的MxDs如圖3。初始狀態(tài)（0，0，0，0）的MDD表示如圖4-a。

②依據(jù)飽和算法首先從從底部的節(jié)點(diǎn)＜1，1＞開始，該節(jié)點(diǎn)中存在可擴(kuò)展?fàn)顟B(tài)0，事件α1存在有效擴(kuò)展鏈，直接調(diào)用Recfire函數(shù)擴(kuò)展了當(dāng)前節(jié)點(diǎn)＜1，1＞，增加了兩個(gè)狀態(tài)1，2。見圖（4-b）;

③飽和＜2，1＞節(jié)點(diǎn)，該節(jié)點(diǎn)中存在α2的可擴(kuò)展?fàn)顟B(tài)0，Evalid（1，＜2，1＞[0]，Nα21）返回1，α2中存在擴(kuò)展鏈。Saturate函數(shù)調(diào)用Recfire（α2，1，＜2，1＞[0]）在下層創(chuàng)建新的節(jié)點(diǎn)＜1，2＞，第一層的當(dāng)前節(jié)點(diǎn)＜2，1＞[0]存在α2的可擴(kuò)展?fàn)顟B(tài)1，Recfire自身調(diào)用Recfire（α2，0，＜1，1＞[1]），因k=0＜last（α），從本層結(jié)束遞推并開始向上返回，返回中完成本層新建節(jié)點(diǎn)＜1，2＞的狀態(tài)3添加和飽和。并將已飽和的節(jié)點(diǎn)在FC[1]表中進(jìn)行記錄。見圖4-c。

④Saturate（3，1＞，該節(jié)點(diǎn)中存在α3的可擴(kuò)展?fàn)顟B(tài)0，Saturate調(diào)用Evalid（2，＜3，1＞[0]，Nα32）函數(shù)，返回值1，判斷α3中存在擴(kuò)展鏈，調(diào)用Recfire進(jìn)入下層節(jié)點(diǎn)的擴(kuò)展和飽和。依次在第一層、第二層建立了新的節(jié)點(diǎn)＜1，3＞、＜2，2＞，并將它們飽和，在FC[1]、FC[2]表中進(jìn)行記錄。返回到節(jié)點(diǎn)＜3，1＞后，節(jié)點(diǎn)新狀態(tài)1成為α3的可擴(kuò)展?fàn)顟B(tài)，Saturate再次調(diào)用Evalid（2，＜3，1＞[0]，Nα32）函數(shù)，返回值0，表明當(dāng)前狀態(tài)下，α3不存在擴(kuò)展鏈，返回。重復(fù)④直到?jīng)]有新的節(jié)點(diǎn)產(chǎn)生。見圖4-d。

⑤同樣方法用α4，α5對(duì)節(jié)點(diǎn)＜4.1＞進(jìn)行飽和，最終的狀態(tài)空間的MDDS如圖4-e。

圖4 飽和算法執(zhí)行

最后的可達(dá)狀態(tài)空間{0000，0001，0002，0013，0122，1213，2213}

上述飽和過程采用了新飽和算法，在Saturate函數(shù)還沒調(diào)用Recfire函數(shù)之前，一次性的利用Evalid函數(shù)來判斷當(dāng)前事件中是否存在擴(kuò)展鏈。若有，則調(diào)用Recfire函數(shù)進(jìn)入下層當(dāng)前節(jié)點(diǎn)的做進(jìn)一步分支擴(kuò)展鏈判斷。否則及時(shí)退出。

用C語言對(duì)新算法和原算法進(jìn)行了編程實(shí)現(xiàn)，并在多個(gè)典型事例上運(yùn)行，統(tǒng)計(jì)了兩種算法中調(diào)用Recfire函數(shù)的次數(shù)。

表2列出了幾個(gè)實(shí)例運(yùn)行中的Recfire函數(shù)的調(diào)用情況，一般來說系統(tǒng)中的層變量越多，當(dāng)前無擴(kuò)展鏈情況越多，新算法的優(yōu)越性越明顯。

表2 實(shí)例運(yùn)行結(jié)果

3 結(jié)語

Ciardo、Andrew提出的以固定點(diǎn)為依據(jù)、基于MDD結(jié)構(gòu)的飽和算法在異步系統(tǒng)模型例如Petri Net、Markov鏈等中顯示它較好的空間和時(shí)間特性。本文詳細(xì)的闡述了飽和算法理論依據(jù)、實(shí)現(xiàn)方法；提出了通過對(duì)當(dāng)前事件的擴(kuò)展鏈進(jìn)行預(yù)先判斷，只有在當(dāng)前事件中存在擴(kuò)展鏈時(shí)才用Recfire函數(shù)來繼續(xù)下層節(jié)點(diǎn)分支擴(kuò)展鏈的提取判斷，以便回歸時(shí)進(jìn)行擴(kuò)展、飽和；取消無擴(kuò)展鏈的事件的Refire函數(shù)的遞歸調(diào)用、新節(jié)點(diǎn)的內(nèi)存空間的申請(qǐng)與回收，理論推理分析和實(shí)驗(yàn)證明了新飽和算法的有效性。

[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網(wǎng)導(dǎo)論.北京：機(jī)械工業(yè)出版社，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

段珊，碩士，研究方向?yàn)樾问交?yàn)證、高性能計(jì)算

王金娟（1981-），女，湖南長沙人，碩士，系統(tǒng)分析師，研究方向?yàn)檐浖こ碳夹g(shù)與應(yīng)用