盧委紅，丁志軍

1.同濟(jì)大學(xué)電子與信息工程學(xué)院，上海201804

2.同濟(jì)大學(xué)教育部嵌入式系統(tǒng)與服務(wù)計(jì)算重點(diǎn)實(shí)驗(yàn)室，上海201804

3.同濟(jì)大學(xué)上海市電子交易與信息服務(wù)協(xié)同創(chuàng)新中心，上海201804

Petri 網(wǎng)是一種重要的形式化建模工具，能有效地對(duì)信息系統(tǒng)進(jìn)行描述和建模.作為一種系統(tǒng)模型，Petri 網(wǎng)不僅可以刻畫系統(tǒng)的結(jié)構(gòu)，還可以描述系統(tǒng)的動(dòng)態(tài)行為；既有直觀的圖形表示，又可以引入許多數(shù)學(xué)方法分析其性質(zhì).Petri 網(wǎng)具有可達(dá)性、有界性、活性等[1]重要的性質(zhì)，同Petri 網(wǎng)所模擬的實(shí)際系統(tǒng)聯(lián)系密切.

在這些性質(zhì)中，Petri 網(wǎng)的有界性[2]反映了被模擬系統(tǒng)運(yùn)行過程中對(duì)有關(guān)資源的容量要求.如果能夠求出每個(gè)庫所p的界b，那么在系統(tǒng)設(shè)計(jì)時(shí)，只要庫所p所表示資源的容量不小于b，就能保證系統(tǒng)正常運(yùn)行.此外，庫所界的信息還可以指導(dǎo)可達(dá)標(biāo)識(shí)的存儲(chǔ)，通過位存儲(chǔ)的方式減少存儲(chǔ)可達(dá)標(biāo)識(shí)所需的空間.也就是說，若已知庫所p的界為b，則只需lbb比特的存儲(chǔ)空間來存儲(chǔ)該庫所的標(biāo)識(shí)數(shù).

目前求解庫所界的方法有兩種：一種方法是完全生成狀態(tài)空間[2-3]，但對(duì)存儲(chǔ)空間的要求過高；另一種方法是用P 不變量估計(jì)庫所界[4]，但存在無法精確求解所有庫所界的問題.為此，本文提出了一種基于部分狀態(tài)空間存儲(chǔ)求解庫所界的算法，在Petri 網(wǎng)生成狀態(tài)空間的過程中，只需存儲(chǔ)其中一部分能標(biāo)識(shí)就可以精確求解所有庫所的界.實(shí)驗(yàn)中選取了模型檢測競賽中的部分模型，并對(duì)3 種求解界的方法進(jìn)行了比較分析，實(shí)驗(yàn)結(jié)果說明了本文算法的有效性.

1 相關(guān)工作

Petri 網(wǎng)中庫所界的含義是系統(tǒng)運(yùn)行過程中庫所p獲得標(biāo)識(shí)數(shù)的最大值.庫所界的概念提出后，F(xiàn)inkel[3]提出了求解庫所界的方法，即從Petri 網(wǎng)的初始標(biāo)識(shí)開始運(yùn)行整個(gè)Petri 網(wǎng)系統(tǒng)，在此過程中記錄全部庫所的最大托肯值，從而精確求解Petri 網(wǎng)中全部庫所的界.然而，該方法需要生成、記錄并存儲(chǔ)所有可達(dá)標(biāo)識(shí)，對(duì)系統(tǒng)存儲(chǔ)空間要求較高.

2019年，Wolf[4]提出用P 不變量方法估計(jì)庫所界，以壓縮每個(gè)標(biāo)識(shí)所需的存儲(chǔ)空間.若i是1 個(gè)P 不變量，則對(duì)于所有可達(dá)標(biāo)識(shí)m有m(p)≤，從而求解得到庫所p的估計(jì)界.該方法存在如下問題：1）P 不變量無法覆蓋全部庫所；2）即使是大于零的分量所對(duì)應(yīng)的庫所，仍然存在界估計(jì)不準(zhǔn)確的問題.例如，圖1(a)所示的Petri 網(wǎng)PN0中P 不變量為(2,1,1,1,1).由P 不變量的性質(zhì)可得，在任何可達(dá)標(biāo)識(shí)m下，滿足2m(p1)+m(p2)+m(p3)+m(p4)+m(p5)=2，則庫所p2的上界估計(jì)為2.而通過生成可達(dá)圖可以得到該庫所的上界實(shí)際為1，如圖1(b)所示，因此實(shí)際只需1 比特來存儲(chǔ).

圖1 Petri 網(wǎng)PN0 及其可達(dá)圖Figure 1 Petri net PN0 and its reachability graph

Schmidt[5-6]提出在生成Petri 網(wǎng)狀態(tài)空間時(shí)，用T不變量方法只存儲(chǔ)部分狀態(tài)空間來驗(yàn)證Petri 網(wǎng)的可達(dá)性、死鎖等性質(zhì).該方法通過求解T不變量存儲(chǔ)可達(dá)圖中的部分標(biāo)識(shí)，以保證可達(dá)圖生成的正常終止，減少了驗(yàn)證Petri 網(wǎng)性質(zhì)過程中所需的存儲(chǔ)空間.同時(shí)該方法在驗(yàn)證相關(guān)性質(zhì)的過程中會(huì)訪問到每一個(gè)狀態(tài)，保證了驗(yàn)證結(jié)果的正確性.但該方法沒有討論P(yáng)etri 網(wǎng)的有界性及庫所界的求解.

本文提出了一種基于部分狀態(tài)空間存儲(chǔ)求解庫所界的算法，在Petri 網(wǎng)生成狀態(tài)空間的過程中，只需存儲(chǔ)其中一部分狀態(tài)就能精確求解所有庫所的界.與完全生成狀態(tài)空間的方法[3]相比，本文算法由于只存儲(chǔ)部分標(biāo)識(shí)，減少了所需的空間資源.與P 不變量估計(jì)庫所界方法[4]相比，本文算法可以精確求解所有庫所的界，提高了庫所界求解的精確度.

2 基本概念

Petri 網(wǎng)是用于描述分布式系統(tǒng)的一種模型，既能夠描述系統(tǒng)的結(jié)構(gòu)，又能夠模擬系統(tǒng)的運(yùn)行.利用Petri 網(wǎng)為一個(gè)實(shí)際系統(tǒng)建模時(shí)，網(wǎng)的部分描述系統(tǒng)的結(jié)構(gòu)，可以將每個(gè)庫所看作一個(gè)條件，每個(gè)變遷看作一個(gè)事件，事件有發(fā)生權(quán)當(dāng)且僅當(dāng)它的每個(gè)前置條件都成立.標(biāo)識(shí)部分反映系統(tǒng)的狀態(tài)，包含事件發(fā)生前后的狀態(tài).

假設(shè)N是自然數(shù)的集合，Petri 網(wǎng)的一些基本概念[7]如下：

定義1（Petri 網(wǎng)）

Petri 網(wǎng)是一個(gè)五元組PN=(P,T,F,W,M0)，其中P和T是兩個(gè)不相交的有限集合，P中元素稱為庫所，T中元素稱為變遷.F是有向弧的集合，定義為F ?(P ×T)∪(T ×P).W是弧的權(quán)重函數(shù)，定義為W:F→N.當(dāng)(x,y)/∈F時(shí)，W(x,y)=0.M0是初始標(biāo)識(shí).網(wǎng)PN 的一個(gè)標(biāo)識(shí)M是一個(gè)映射M:P→N，表示標(biāo)識(shí)M下各個(gè)庫所的托肯分布，其中M(p)表示標(biāo)識(shí)‘M下庫所p中的托肯數(shù)目.

定義2

給定一個(gè)Petri 網(wǎng)PN，x?={y|(x,y)∈F}，?x={y|(y,x)∈F}，其中x,y ∈P ∪T.若x是庫所（變遷），則?x稱為x的輸入變遷（庫所）集合，x?稱為x的輸出變遷（庫所）集合.

定義3（變遷發(fā)生規(guī)則）

給定一個(gè)Petri 網(wǎng)PN，在一個(gè)標(biāo)識(shí)M下，對(duì)于一個(gè)變遷t ∈T，若?p ∈?t，M(p) ≥W(p,t)，則稱變遷t在標(biāo)識(shí)M下使能，使能變遷可以發(fā)生并產(chǎn)生新標(biāo)識(shí)M＇，記為M[t>M＇，滿足?p ∈P，M＇(p)=M(p)?W(p,t)+W(t,p).

定義4（可達(dá)性）

給定一個(gè)Petri 網(wǎng)PN，若存在t ∈T，使得M[t>M＇，則稱M＇為從M直接可達(dá)的.若存在變遷序列t1,t2,···,tk和標(biāo)識(shí)序列M1,M2,···,Mk使得

則稱Mk為從M可達(dá)的.從M可達(dá)的一切標(biāo)識(shí)的集合記為R(M).

定義5（可達(dá)圖）

給定一個(gè)Petri 網(wǎng)PN，PN 的可達(dá)圖定義為一個(gè)三元組RG(PN)=(R(M0),E,P)，其中

稱R(M0)為RG(PN)的頂點(diǎn)集，E為RG(PN)的弧集；若P(Mi,Mj)=tk，則稱tk為弧(Mi,Mj)的旁標(biāo).

例如，圖2是一個(gè)Petri 網(wǎng)模型，庫所用圓圈表示，變遷用矩形表示，弧用有向邊表示.若邊上沒有標(biāo)記，則默認(rèn)弧的權(quán)重為1.初始托肯用庫所中的黑點(diǎn)表示.

圖2 Petri 網(wǎng)模型——ERKFigure 2 Petri net model—ERK

定義6（有界性）

給定一個(gè)Petri 網(wǎng)PN，p ∈P.若存在正整數(shù)B，使得?M ∈R(M0):M(p)≤B，則稱庫所p為有界的，并稱滿足此條件的最小正整數(shù)B為庫所p的界，記為B(p)，即B(p)=min{B|?M ∈R(M0):M(p)B}.當(dāng)B(p)=1 時(shí)，稱庫所p是安全的.

定義7（關(guān)聯(lián)矩陣）

給定一個(gè)Petri 網(wǎng)PN，P={p1,p2,···,pm}，T={t1,t2,···,tn}，則Petri 網(wǎng)PN 的結(jié)構(gòu)可以用一個(gè)m行n列矩陣A=[aij]m×n表示，其中aij=W(tj,pi)?W(pi,tj),i ∈{1,2,···,m}，j ∈{1,2,···,n}，稱A為網(wǎng)PN 的關(guān)聯(lián)矩陣.

定義8（狀態(tài)方程）

給定一個(gè)Petri 網(wǎng)PN，A為網(wǎng)PN 的關(guān)聯(lián)矩陣.若M ∈R(M0)，則存在非負(fù)整數(shù)的n維向量X，使得

則該式稱為Petri 網(wǎng)的狀態(tài)方程.式(3)中的n維非負(fù)整數(shù)向量X稱為發(fā)生數(shù)向量.如果M是從M0可達(dá)的，則使得M0[σ >M的任意一個(gè)變遷序列σ都有一個(gè)滿足狀態(tài)方程的n維向量X，使得#(ti/σ)=X(i)，即X中的第i個(gè)分量等于ti在σ中出現(xiàn)的次數(shù).

定義9（P 不變量）

給定一個(gè)Petri 網(wǎng)PN，|P|=m，|T|=n，A為PN 的關(guān)聯(lián)矩陣.若存在非平凡的m維非負(fù)整數(shù)向量X滿足ATX=0，則稱X為網(wǎng)PN 的一個(gè)P 不變量.

結(jié)合狀態(tài)方程可得，若標(biāo)識(shí)從標(biāo)識(shí)m可達(dá)，則滿足=Xm.若p是一個(gè)庫所，滿足X(p)0，可得

例如，在圖2所示的Petri 網(wǎng)中，(1,0,1,1,0,0,0,0,0,0,0)T為一個(gè)P 不變量.

定義10（T 不變量）

給定一個(gè)Petri 網(wǎng)PN，|P|=m，|T|=n，A為PN 的關(guān)聯(lián)矩陣.若存在非平凡的n維非負(fù)整數(shù)向量Y滿足AY=0，則稱Y為網(wǎng)PN 的一個(gè)T不變量.

從一個(gè)標(biāo)識(shí)m下發(fā)生T 不變量Y中非零分量的變遷，能再次產(chǎn)生標(biāo)識(shí)m，反映了可達(dá)圖中狀態(tài)的回路關(guān)系.

例如，在圖2所示的Petri 網(wǎng)中，初始標(biāo)識(shí)下可以發(fā)生變遷序列t1,t2,并再次產(chǎn)生初始標(biāo)識(shí).因此(1,1,0,0,0,0,0,0,0,0,0)T為一個(gè)T 不變量.

3 基于部分狀態(tài)空間的Petri 網(wǎng)庫所界求解算法

3.1 算法原理

如前所述，本文算法的主要思想為，在不存儲(chǔ)Petri 網(wǎng)的所有狀態(tài)，實(shí)現(xiàn)所有庫所精確界的求解.該算法核心在于所存儲(chǔ)的部分狀態(tài)既能保證從這些狀態(tài)出發(fā)可以遍歷到Petri網(wǎng)的所有可達(dá)狀態(tài)，以準(zhǔn)確獲取每個(gè)庫所中的托肯數(shù)進(jìn)而計(jì)算庫所界；又能確保可達(dá)圖生成算法的終止.這其中，由于Petri 網(wǎng)的可達(dá)狀態(tài)都可由初始狀態(tài)依據(jù)Petri 網(wǎng)變遷發(fā)生規(guī)則計(jì)算產(chǎn)生，所以理論上只要保存包含初始狀態(tài)的部分狀態(tài)一定是可以遍歷到Petri 網(wǎng)的所有可達(dá)狀態(tài).因此算法需主要解決第二個(gè)問題，即只存儲(chǔ)部分狀態(tài)如何保證可達(dá)圖生成算法的正常終止.

進(jìn)一步分析可知，該情況下可達(dá)圖生成算法無法終止的原因是在可達(dá)圖中有回路的存在.所謂回路，即從一個(gè)狀態(tài)出發(fā)，發(fā)生一個(gè)變遷序列后能再次產(chǎn)生該狀態(tài).顯然對(duì)于可達(dá)圖中的某個(gè)狀態(tài)m：

1）若狀態(tài)m在一個(gè)回路內(nèi)，假設(shè)該回路中任何一個(gè)狀態(tài)都沒有存儲(chǔ)和記錄，則在可達(dá)圖生成過程中由于無法判斷狀態(tài)m之前是否生成過，所以會(huì)不斷重復(fù)生成該狀態(tài)，導(dǎo)致可達(dá)圖會(huì)一直生成.

2）若狀態(tài)m不存在于任何一個(gè)回路內(nèi)，即狀態(tài)m在可達(dá)圖生成過程中只會(huì)產(chǎn)生一次，則無需存儲(chǔ)狀態(tài)m也能夠保證可達(dá)圖的終止.特別地，若可達(dá)圖中沒有回路，則只需記錄初始狀態(tài)就能保證可達(dá)圖生成算法的終止.

通過上述分析可知，對(duì)于狀態(tài)m所在的回路至少需要存儲(chǔ)回路上的一個(gè)狀態(tài)才能保證算法不會(huì)陷入無限循環(huán)，確保算法終止.

下面利用Schmidt[5]的方法，通過T不變量的性質(zhì)找到覆蓋可達(dá)圖中所有回路的狀態(tài)集合，通過存儲(chǔ)這些狀態(tài)可以保證可達(dá)圖中的每個(gè)回路都至少存儲(chǔ)了一個(gè)狀態(tài)，從而實(shí)現(xiàn)可達(dá)圖生成算法的正常終止.

對(duì)關(guān)聯(lián)矩陣A進(jìn)行初等行變換能夠?qū)⑵滢D(zhuǎn)化成上三角形式[4]，即某行最左邊的非零元素總在之前行最左邊非零元素的右邊.將包含某行最左邊非零元素的列稱為頭列，其余列稱為尾列.

如圖3所示，矩陣A為圖2中Petri 網(wǎng)關(guān)聯(lián)矩陣的上三角形式，t1,t3,t5,t6,t8,t9所在的列為頭列，t2,t4,t7,t10,t11所在的列為尾列.

圖3 關(guān)聯(lián)矩陣的上三角形式AFigure 3 Upper triangular form A of incidence matrix

矩陣A的每一列對(duì)應(yīng)變量x，因此可以將變量分為頭變量和尾變量.在本例中頭變量為x1,x3,x5,x6,x8,x9，尾變量為x2,x4,x7,x10,x11.

定義11（Uset）

將關(guān)聯(lián)矩陣轉(zhuǎn)化為上三角形式后，所有尾變量對(duì)應(yīng)的變遷集合稱為Uset.在本例中，Uset={t2,t4,t7,t10,t11}.

實(shí)際上，變遷集合Uset是覆蓋所有T 不變量的最小變遷集合.因?yàn)榧蟄set中的元素為與所有尾變量對(duì)應(yīng)的變遷集合，而對(duì)所有尾變量賦值為1、所有頭變量賦值為0 的向量I表示所有T 不變量的線性組合，并且是覆蓋變遷數(shù)目最少的一個(gè)線性組合.因此向量I中非零元素組成的集合Uset是覆蓋所有T 不變量的最小變遷集合.只要存儲(chǔ)發(fā)生Uset中的變遷產(chǎn)生的標(biāo)識(shí)集合就意味著可達(dá)圖中的每個(gè)回路都至少存儲(chǔ)了一個(gè)狀態(tài).

通過前述分析可知，可達(dá)圖中每個(gè)回路都需要存儲(chǔ)一個(gè)狀態(tài)以保證生成算法的終止.如果能夠消除可達(dá)圖中的回路，就有可能進(jìn)一步減少求取界過程中需要存儲(chǔ)的狀態(tài)數(shù)目.為此，本文引入了變遷對(duì)、變遷環(huán)的概念，通過識(shí)別變遷對(duì)、變遷環(huán)，抑制部分變遷的發(fā)生，在不影響狀態(tài)生成的同時(shí)，避免可達(dá)圖回路的產(chǎn)生.

3.1.1 變遷對(duì)

定義12（支集、變遷對(duì)）

設(shè)X為網(wǎng)PN 的一個(gè)T 不變量，記

稱為T 不變量X的支集.特別地，若滿足X(t)=1，則稱該支集中的兩個(gè)變遷為變遷對(duì).

如圖4所示，在PN1中，變遷t1、t2構(gòu)成了變遷對(duì).對(duì)應(yīng)PN1的可達(dá)圖如圖4(b)所示，其構(gòu)成了一個(gè)回路.

針對(duì)上述變遷對(duì)發(fā)生所產(chǎn)生的回路，可以通過抑制變遷t2發(fā)生來避免回路的產(chǎn)生.方法如下：若標(biāo)識(shí)m0下變遷t1使能，且t1、t2對(duì)應(yīng)一個(gè)變遷對(duì)，此時(shí)就標(biāo)記變遷t2不使能，限制其在標(biāo)識(shí)m1下發(fā)生，從而避免回路的產(chǎn)生.

特別地，若在任意標(biāo)識(shí)m下，變遷對(duì)中的兩個(gè)變遷均使能，則不對(duì)變遷對(duì)中的某個(gè)變遷進(jìn)行抑制發(fā)生的處理.如圖5所示，在標(biāo)識(shí)m1下，變遷對(duì)中的兩個(gè)變遷t1、t2均使能，此時(shí)若抑制變遷t2的發(fā)生會(huì)使得標(biāo)識(shí)m3無法生成，進(jìn)而影響求解的界數(shù)組的準(zhǔn)確性，因此這種情況下不能抑制變遷t2的發(fā)生.

通過上述分析可以看到，通過定義變遷對(duì)及對(duì)變遷對(duì)進(jìn)行處理，可以避免一部分可達(dá)圖回路的產(chǎn)生，從而減少了生成可達(dá)圖時(shí)需要存儲(chǔ)的狀態(tài)數(shù)目.

圖4 Petri 網(wǎng)PN1 及其可達(dá)圖Figure 4 Petri net PN1 and its reachability graph

圖5 Petri 網(wǎng)PN2 及其可達(dá)圖Figure 5 Petri net PN2 and its reachability graph

3.1.2 變遷環(huán)

定義13（變遷環(huán)）

設(shè)X為網(wǎng)PN 的一個(gè)T 不變量，滿足若?ti ∈PXP，?tj,tk ∈PXP，，滿足=?tj且?ti=，則稱該支集為變遷環(huán).

如圖6所示，在圖PN3中，變遷t1、t2、t3構(gòu)成了變遷環(huán).變遷t1的發(fā)生將庫所p1中的托肯轉(zhuǎn)移到庫所p2中，變遷t2的發(fā)生將庫所p2中的托肯轉(zhuǎn)移到庫所p3中，而變遷t3的發(fā)生又將庫所p3中的托肯再次轉(zhuǎn)移到庫所p1中，對(duì)應(yīng)PN3的可達(dá)圖如圖6(b)所示，m0、m1、m2構(gòu)成了一個(gè)回路.

參考前述變遷對(duì)的處理方法并針對(duì)上述變遷環(huán)發(fā)生所產(chǎn)生的回路，可以通過抑制變遷t3發(fā)生來避免回路產(chǎn)生.方法如下：若標(biāo)識(shí)m0下發(fā)生變遷t1產(chǎn)生標(biāo)識(shí)m1，標(biāo)識(shí)m1下發(fā)生變遷t2產(chǎn)生標(biāo)識(shí)m2，且t1、t2、t3對(duì)應(yīng)一個(gè)變遷環(huán)，通過對(duì)變遷環(huán)中已發(fā)生的變遷t1，t2進(jìn)行計(jì)數(shù)處理，此時(shí)標(biāo)記變遷t3不使能，限制其在標(biāo)識(shí)m2下發(fā)生，從而避免回路產(chǎn)生.

圖6 Petri 網(wǎng)PN3 及其可達(dá)圖Figure 6 Petri net PN3 and its reachability graph

特別地，若在任意標(biāo)識(shí)m下，變遷環(huán)中有2 個(gè)及以上變遷可以使能，則在該標(biāo)識(shí)下，不對(duì)變遷環(huán)中某個(gè)變遷的發(fā)生進(jìn)行計(jì)數(shù)處理.如圖7所示，在標(biāo)識(shí)m1下，變遷環(huán){t1，t2，t3}中的2個(gè)變遷t1，t3均使能，此時(shí)若對(duì)變遷t1，t3的發(fā)生進(jìn)行計(jì)數(shù)，則在標(biāo)識(shí)m2下會(huì)抑制變遷t2發(fā)生，使標(biāo)識(shí)m4無法生成，進(jìn)而影響求解界的準(zhǔn)確性，因此這種情況下對(duì)變遷t1，t3的發(fā)生進(jìn)行不計(jì)數(shù).同時(shí)，為了避免變遷環(huán)中計(jì)數(shù)處理的復(fù)雜化，若一個(gè)標(biāo)識(shí)下能發(fā)生變遷環(huán)中的多個(gè)變遷，則在后續(xù)可達(dá)圖生成過程中出現(xiàn)該變遷環(huán)時(shí)都不再進(jìn)行消除變遷環(huán)的處理.

圖7 Petri 網(wǎng)PN4 及其可達(dá)圖Figure 7 Petri net PN4 and its reachability graph

3.2 求解算法

按照上述算法原理，本文算法在Petri 網(wǎng)可達(dá)狀態(tài)生成中使用一個(gè)界數(shù)組bound[]來存儲(chǔ)當(dāng)前每個(gè)庫所的最大托肯數(shù)，在遍歷每個(gè)可達(dá)狀態(tài)時(shí)，根據(jù)該狀態(tài)中每個(gè)庫所的托肯數(shù)更新界數(shù)組.對(duì)算法中的相關(guān)變量說明如下：M0為初始標(biāo)識(shí)；visited[]為可達(dá)圖生成過程中需要存儲(chǔ)的標(biāo)識(shí)集合，初始化為空；Uset為前文定義的尾變量變遷集合；disable[]為一個(gè)變遷集合，表示若某標(biāo)識(shí)下能發(fā)生該集合中的變遷，則不再計(jì)算后續(xù)標(biāo)識(shí)，初始化為空；circle[]為一個(gè)計(jì)數(shù)數(shù)組，表示變遷環(huán)中已發(fā)生變遷的個(gè)數(shù)，大小為Petri 網(wǎng)中變遷環(huán)的個(gè)數(shù)，初始化為0.

算法求解Petri 網(wǎng)中各庫所界

輸入：Petri 網(wǎng)(N,M0) ；網(wǎng)N的T 不變量

輸出：各個(gè)庫所的界bound[]～bound[k]（k為Petri 網(wǎng)庫所數(shù)目）

以圖4所示的PN1為例進(jìn)行算法運(yùn)行演示如下：

對(duì)于m0下的使能變遷t1.第6 行判斷t1對(duì)應(yīng)變遷對(duì){t1,t2}，且t2在m0下不使能；第7行t1不屬于disable 集合，所以disable 集合中加入變遷t2；第15 行m0下發(fā)生t1得到m1，bound 數(shù)組由[1,1,0]更新為[1,1,1]；第16 行判斷m1不屬于visited 集合；第17 行由于Uset={t2}，而t1不屬于Uset集合，所以visited 中不存儲(chǔ)m1.

對(duì)于m1下的使能變遷t2.第6 行判斷t2對(duì)應(yīng)變遷對(duì){t1,t2}，且t1在m1下不使能；第8行t2屬于disable 集合，所以跳出本層for 循環(huán).此時(shí)，由于不存在“新”結(jié)點(diǎn)，因此跳出while循環(huán)，算法結(jié)束.

對(duì)算法中的相關(guān)步驟解釋說明如下：

第6 行，如前文所述，若標(biāo)識(shí)m下的使能變遷同時(shí)包含1 個(gè)變遷對(duì)中的2 個(gè)變遷，則抑制某個(gè)變遷的產(chǎn)生會(huì)影響求解界數(shù)組的正確性，因此跳至15 行繼續(xù)執(zhí)行且后續(xù)使用Uset判斷是否存儲(chǔ)標(biāo)識(shí).第7 行，若變遷ti是變遷對(duì)中在時(shí)間順序上先發(fā)生的變遷，則將變遷對(duì)中的另一個(gè)變遷放入集合disable 中.第8 行，若變遷ti對(duì)應(yīng)一個(gè)變遷對(duì)且已經(jīng)被放入集合disable中，則在標(biāo)識(shí)m下不發(fā)生該變遷，達(dá)到了消除可達(dá)圖中回路的目的.

第9～14 行，若變遷環(huán)中變遷數(shù)目為s，則在發(fā)生了變遷環(huán)的s ?1 個(gè)變遷后，抑制第s個(gè)變遷的發(fā)生，則不會(huì)再次產(chǎn)生之前狀態(tài)，因此可以消除該回路.第10 行，若一個(gè)標(biāo)識(shí)m下能發(fā)生變遷環(huán)中的多個(gè)變遷，對(duì)這些變遷進(jìn)行計(jì)數(shù)會(huì)影響求解界數(shù)組的正確性，因此將circle數(shù)組中該變遷環(huán)所在的分量值記為–1，即之后若發(fā)生該變遷環(huán)中的變遷都不進(jìn)行計(jì)數(shù).第11行，若變遷環(huán)C還未發(fā)生s ?1 個(gè)變遷時(shí)，則circle[C]加1，表示該變遷環(huán)中已發(fā)生變遷的個(gè)數(shù)加1.第12～14 行，若變遷ti對(duì)應(yīng)的變遷環(huán)C已經(jīng)發(fā)生了s ?1 個(gè)變遷時(shí)，則第s個(gè)變遷ti使其不使能，同時(shí)計(jì)數(shù)數(shù)組置0，達(dá)到了消除可達(dá)圖中回路的目的.

通過引入第6～14 行的方法，減少了可達(dá)圖中回路數(shù)目，從而減少了可達(dá)圖中需要存儲(chǔ)的標(biāo)識(shí)數(shù)目.舉例來說，如圖8和10 所示，若只用Uset判定，由于標(biāo)識(shí)m2下發(fā)生集合Uset中的變遷t7能夠產(chǎn)生標(biāo)識(shí)m1則需存儲(chǔ)標(biāo)識(shí)m1，但用上述方法在標(biāo)識(shí)m2下變遷t7不再使能，因此不需存儲(chǔ)標(biāo)識(shí)m1.

第15 行，生成一個(gè)新的標(biāo)識(shí)并對(duì)界數(shù)組bound 進(jìn)行更新.第16 行，若新標(biāo)識(shí)已經(jīng)存在于集合visited 中，說明該標(biāo)識(shí)前已經(jīng)產(chǎn)生過，則跳出本次循環(huán).第17 行，m下發(fā)生變遷ti得到標(biāo)識(shí)后，決定標(biāo)識(shí)是否存儲(chǔ)的依據(jù)是ti是否是Uset中的變遷.若一個(gè)標(biāo)識(shí)不是由Uset中變遷發(fā)生得到的，則不會(huì)在集合visited 中存儲(chǔ)這個(gè)狀態(tài)，所以可能會(huì)再次生成該標(biāo)識(shí)，并再次計(jì)算其使能變遷.由于不存儲(chǔ)的狀態(tài)不會(huì)構(gòu)成一個(gè)回路，因此仍然能夠保證可達(dá)圖的終止.

可達(dá)圖用以描述Petri 網(wǎng)的可達(dá)標(biāo)識(shí)集，既與Petri 網(wǎng)的結(jié)構(gòu)有關(guān)，還與Petri 網(wǎng)的初始標(biāo)識(shí)有關(guān).設(shè)可達(dá)圖中標(biāo)識(shí)數(shù)目為n，平均情況下每個(gè)標(biāo)識(shí)的使能變遷數(shù)為d，同時(shí)在這一過程中，每產(chǎn)生一個(gè)標(biāo)識(shí)需要判斷是否已經(jīng)產(chǎn)生過，消耗的時(shí)間為則傳統(tǒng)可達(dá)圖生成算法的時(shí)間復(fù)雜度為O(n2d).設(shè)本文算法變遷對(duì)、變遷環(huán)的數(shù)量為a，則與其相關(guān)的判斷操作耗費(fèi)的時(shí)間為an，所以本文算法的時(shí)間復(fù)雜度為O(n2d+n).

4 實(shí)例分析

選取模型檢測比賽[8-9]（model checking contest）中的Petri 網(wǎng)模型ERK[10]，如圖2所示，結(jié)合本文算法進(jìn)行具體分析.

完全存儲(chǔ)狀態(tài)空間求取庫所界的方法（Complete）[3]通過完全生成狀態(tài)空間求解各個(gè)庫所界，能夠精確求解界以達(dá)到可達(dá)標(biāo)識(shí)存儲(chǔ)所需空間的最強(qiáng)壓縮效果.但在此過程中，為了保證可達(dá)圖生成的終止必須存儲(chǔ)所有狀態(tài)，因此需要耗費(fèi)大量的空間資源.

使用P 不變量估計(jì)庫所界的方法（P-inv）[4]通過求解Petri 網(wǎng)的P 不變量，結(jié)合狀態(tài)方程估計(jì)庫所界.但該方法無法保證得到精確的庫所界，沒有達(dá)到可達(dá)標(biāo)識(shí)存儲(chǔ)的最強(qiáng)壓縮，因此浪費(fèi)了部分空間.

與Complete 方法相比，本文提出的算法通過存儲(chǔ)部分狀態(tài)實(shí)現(xiàn)庫所界的精確求解，無需存儲(chǔ)全部狀態(tài)空間，更有利于在復(fù)雜大規(guī)模系統(tǒng)中的應(yīng)用.特別地，在可達(dá)圖中回路較少甚至不存在回路的情況下，只需存儲(chǔ)極少的狀態(tài)數(shù)目甚至無需存儲(chǔ)狀態(tài)就能實(shí)現(xiàn)庫所界的精確求解.與P-inv 方法相比，本文算法可以在覆蓋所有庫所的同時(shí)實(shí)現(xiàn)可達(dá)標(biāo)識(shí)存儲(chǔ)的最強(qiáng)壓縮，提高壓縮效果.

對(duì)圖2所示的ERK 模型進(jìn)行P 不變量估計(jì)的方法求庫所界時(shí)，可以得到庫所p1、p3、p4、p7,p8、p10、p11的界估計(jì)，即這些庫所的界都為1.在后續(xù)可達(dá)標(biāo)識(shí)存儲(chǔ)時(shí)，這些庫所的托肯值最大為1，所以可以采用位存儲(chǔ)對(duì)這些庫所使用1 bit 進(jìn)行存儲(chǔ).但還有36%的庫所由于不在P 不變量支集中而無法估計(jì)其界，所以對(duì)于這些庫所的托肯值無法使用位壓縮，仍需使用一個(gè)int 整型類型的存儲(chǔ)空間（32 bit）進(jìn)行存儲(chǔ)，沒有達(dá)到最強(qiáng)的壓縮效果，還有進(jìn)一步的提升空間.

采用存儲(chǔ)部分狀態(tài)空間的方法求解庫所界如圖8所示，若僅存儲(chǔ)能發(fā)生在Uset集合中變遷的狀態(tài)，雖然能夠保證可達(dá)圖的終止，但需要存儲(chǔ)的狀態(tài)（圖8中灰色部分所示）占比整個(gè)狀態(tài)空間為9/13=69%.

圖8 狀態(tài)空間——UsetFigure 8 State space—Uset

如圖9所示，通過求解T不變量可以得到本例中變遷對(duì)為{t1,t2},{t3,t4},{t6,t7},{t9,t10}.

圖9 T 不變量Figure 9 T invariant

通過消除變遷對(duì)的方法，如圖10所示，本文的算法只需存儲(chǔ)4 個(gè)狀態(tài)（圖10中灰色部分所示），占比整個(gè)狀態(tài)空間減少至31%，即可求得庫所精確界.求得該P(yáng)etri 網(wǎng)所有庫所界為1，因此每個(gè)標(biāo)識(shí)中的每個(gè)庫所的托肯數(shù)只需1 bit 來存儲(chǔ)，比起之前32 bit 來存儲(chǔ)，標(biāo)識(shí)的存儲(chǔ)空間壓縮了32 倍.

圖10 狀態(tài)空間——本文算法Figure 10 State space—the proposed algorithm

隨機(jī)選取了模型檢測比賽的部分Petri 網(wǎng)模型，按照狀態(tài)空間數(shù)目遞增的模型順序，將本文算法與完全生成狀態(tài)空間求取庫所界（Complete）、使用P不變量估計(jì)庫所界（P-inv）兩種方法進(jìn)行對(duì)比，實(shí)驗(yàn)結(jié)果顯示，本文算法在狀態(tài)空間壓縮方面效果較好，在一定程度上緩解了狀態(tài)空間爆炸問題.另外，由于不同模型的空間消耗、標(biāo)識(shí)大小差異較大，為了在同一個(gè)曲線圖（圖12空間消耗對(duì)比、圖13標(biāo)識(shí)壓縮對(duì)比）中更加直觀地呈現(xiàn)不同模型的實(shí)驗(yàn)效果，本文根據(jù)狀態(tài)空間的大小將模型分成2組，分別呈現(xiàn)實(shí)驗(yàn)效果.

以下是第1 組模型的實(shí)驗(yàn)結(jié)果.

表1 第1 組模型Table 1 The first group models 個(gè)

覆蓋率定義為能夠求解估計(jì)界的庫所數(shù)占所有庫所數(shù)的比例；準(zhǔn)確率定義為正確得到庫所準(zhǔn)確界的庫所數(shù)占所有庫所數(shù)的比例.表2和圖11分別給出了P-inv 方法與本文算法對(duì)表1模型求解計(jì)算得到的覆蓋率和準(zhǔn)確率.

表2 庫所覆蓋率和界準(zhǔn)確率對(duì)比表Table 2 Comparison of place coverage rate and bound accuracy rate %

圖11 庫所覆蓋率和界準(zhǔn)確率對(duì)比圖Figure 11 Comparison of place coverage rate and bound accuracy rate

本文算法能夠精確求解庫所界，因此覆蓋率和準(zhǔn)確率都達(dá)到了100%.

Complete 空間為存儲(chǔ)所有可達(dá)標(biāo)識(shí)需要的空間；P-inv 空間為存儲(chǔ)P不變量需要的空間；本文空間為存儲(chǔ)T不變量及部分狀態(tài)空間需要的空間.表3和圖12分別給出了3 種方法對(duì)表1模型求解計(jì)算得到的空間消耗.

本文方法消耗空間介于Complete 和P-inv 兩種方法之間，且比Complete 方法低得多.在model 9 中，可達(dá)圖中不存在回路，無需存儲(chǔ)狀態(tài)空間也能保證可達(dá)圖生成的正常終止，因此使用本文方法求解庫所的界，空間消耗最低為0.

Complete 標(biāo)識(shí)存儲(chǔ)、P-inv 標(biāo)識(shí)存儲(chǔ)、本文方法標(biāo)識(shí)存儲(chǔ)分別為使用3 種方法求得庫所界后，存儲(chǔ)一個(gè)標(biāo)識(shí)需要的空間.如model 1 的Complete 標(biāo)識(shí)存儲(chǔ)，共8 個(gè)庫所，每個(gè)庫所分配空間1 bit，所以表格中是1B.不壓縮存儲(chǔ)為不求取庫所界，存儲(chǔ)一個(gè)標(biāo)識(shí)需要的空間.表4和圖13分別給出了4 種方法對(duì)表1模型求解計(jì)算得到的標(biāo)識(shí)存儲(chǔ)空間.

表3 空間消耗對(duì)比表Table 3 Comparison of space consumption B

圖12 空間消耗對(duì)比圖Figure 12 Comparison of space consumption

表4 標(biāo)識(shí)壓縮對(duì)比表Table 4 Comparison of marking compression B

圖13 標(biāo)識(shí)壓縮對(duì)比Figure 13 Comparison of marking compression

本文方法和Complete 方法求得了庫所的精確界，因此都達(dá)到了庫所最強(qiáng)壓縮的效果.以下是第2 組模型的實(shí)驗(yàn)結(jié)果.

表5 第2 組模型Table 5 The second group models

表6給出了P-inv 方法和本文方法對(duì)表5模型求解計(jì)算得到的覆蓋率和準(zhǔn)確率.

表6 庫所覆蓋率和界準(zhǔn)確率對(duì)比表Table 6 Comparison of place coverage rate and bound accuracy rate %

本文算法能夠精確求解庫所界，因此覆蓋率和準(zhǔn)確率都達(dá)到了100%.表7和圖14給出了3 種方法對(duì)表5模型求解計(jì)算得到的空間消耗.在狀態(tài)空間數(shù)目較大的情況下，存儲(chǔ)T 不變量、P 不變量所耗費(fèi)的空間幾乎可以忽略不計(jì).而消耗的這些空間對(duì)于提升求解得到的庫所界的準(zhǔn)確性是十分有效的.

表8和圖15分別給出了Complete、P-inv、本文方法、不壓縮存儲(chǔ)等4 種方法對(duì)于表5模型求解計(jì)算得到的標(biāo)識(shí)存儲(chǔ)空間.

表7 空間消耗對(duì)比表Table 7 Comparison of space consumption MB

圖14 空間消耗對(duì)比圖Figure 14 Comparison of space consumption

表8 標(biāo)識(shí)壓縮對(duì)比表Table 8 Comparison of marking compression B

圖15 標(biāo)識(shí)壓縮對(duì)比圖Figure 15 Comparison of marking compression

本文方法和Complete 方法由于求得了庫所的精確界，因此都達(dá)到了庫所最強(qiáng)壓縮的效果.表9及圖16對(duì)比了三種方法求取庫所界消耗的時(shí)間.

表9 三種方法求取庫所界耗費(fèi)的時(shí)間對(duì)比表Table 9 Time comparison of three methods to get place bound s

圖16 三種方法求取庫所界耗費(fèi)的時(shí)間對(duì)比圖Figure 16 Time comparison of three methods to get place bound

本文算法通過存儲(chǔ)部分狀態(tài)空間求得了庫所的精確界，但由于只存儲(chǔ)部分狀態(tài)會(huì)有一部分未被存儲(chǔ)的狀態(tài)反復(fù)產(chǎn)生，與Complete 方法相比，耗費(fèi)的時(shí)間更多.

在實(shí)驗(yàn)結(jié)果中部分模型消耗的時(shí)間比Complete 方法少，其原因?yàn)槊慨?dāng)生成一個(gè)標(biāo)識(shí)時(shí)，需要判斷該標(biāo)識(shí)之前是否產(chǎn)生過，這就需要與已經(jīng)存儲(chǔ)的標(biāo)識(shí)集合visited 進(jìn)行對(duì)比.在Complete 方法中，visited 中存儲(chǔ)的是當(dāng)前生成的全部可達(dá)標(biāo)識(shí).而在本文算法中，visited 中存儲(chǔ)的是當(dāng)前生成的部分可達(dá)標(biāo)識(shí)，因此本文算法在實(shí)驗(yàn)過程中耗費(fèi)的時(shí)間更少.

在model 6、model 8、model 10 中，由于沒有存儲(chǔ)全部可達(dá)標(biāo)識(shí)，導(dǎo)致部分標(biāo)識(shí)反復(fù)產(chǎn)生，因此本文方法比Complete 方法和P-inv 方法耗費(fèi)的時(shí)間多，但在空間資源緊張的情況下，這種時(shí)間代價(jià)是值得的.

5 結(jié) 語

在Petri 網(wǎng)的眾多性質(zhì)中，由于Petri 網(wǎng)的有界性反映了被模擬系統(tǒng)運(yùn)行過程中對(duì)有關(guān)資源的容量要求，因此受到廣泛關(guān)注.但目前精確求解庫所界的方法需要存儲(chǔ)整個(gè)狀態(tài)空間，給系統(tǒng)的內(nèi)存資源帶來了巨大挑戰(zhàn).本文提出了一種新的求解庫所界的算法，與現(xiàn)有方法相比，本文算法結(jié)合了T 不變量的性質(zhì)及引導(dǎo)消除可達(dá)圖中的部分回路，減少了求解過程中所需的內(nèi)存資源，實(shí)驗(yàn)結(jié)果驗(yàn)證了這一結(jié)論.

未來工作將注重于該算法在模型檢測方面的應(yīng)用.一方面，將結(jié)合on-the-fly 方法、對(duì)稱約簡、偏序約簡等多種方法來進(jìn)一步減少模型檢測過程中消耗的時(shí)間、空間資源；另一方面，將深入思考在求庫所界的過程中能否得到更多有效信息來提高模型檢測的效率.