文/王博 代飛 黃苾
Petri網(wǎng)是1962年由德國(guó)科學(xué)家Carl Adam Petri博士在他的博士論文《用自動(dòng)機(jī)通信》中創(chuàng)立的一種網(wǎng)狀結(jié)構(gòu)。本質(zhì)上,它是一個(gè)有向二分圖,由庫(kù)所和變遷組成。
可達(dá)圖作為分析Petri網(wǎng)動(dòng)態(tài)性質(zhì)的一種重要分析技術(shù),被大量廣泛使用。但是,基于可達(dá)圖的狀態(tài)空間搜索方法需要考慮并發(fā)事件間所有的交織可能,進(jìn)而導(dǎo)致?tīng)顟B(tài)空爆炸。也就是說(shuō),使用基于可達(dá)圖的狀態(tài)空間搜索方法對(duì)并發(fā)系統(tǒng)進(jìn)行分析時(shí),常常面臨效率低下的問(wèn)題。
針對(duì)上述問(wèn)題,McMillan在1995提出了展開(unfolding)的概念。與基于可達(dá)圖的狀態(tài)空間搜索方法相比,基于展開的狀態(tài)空間搜索方法不需要考慮并發(fā)事件間的所有可能交織,可避免狀態(tài)空間爆炸。本文將給出展開Petri網(wǎng)的算法,通過(guò)一個(gè)例子,直觀比較可達(dá)圖和出現(xiàn)網(wǎng)(Occurrence Net,由展開Petri網(wǎng)得到)的規(guī)模。
圖1:一個(gè)Petri網(wǎng)
圖2:可達(dá)圖
定義1(Petri網(wǎng))Petri網(wǎng)是一個(gè)四元組∑=(P, T; F, M),其中:
(4) 映 射 M:P→ {0, 1, 2, 3...}稱 為Petri網(wǎng)的一個(gè)標(biāo)識(shí)。通常用M0表示Petri網(wǎng)的初始標(biāo)識(shí)。
通常,庫(kù)所使用圓圈表示,變遷使用方框表示,流關(guān)系使用有向線段表示,托肯使用實(shí)心小黑點(diǎn)表示。
定義2(可達(dá)標(biāo)識(shí)集)設(shè)∑=(P, T; F, M0)是一個(gè)Petri網(wǎng),其中M0是初始情態(tài)。S的可達(dá)標(biāo)識(shí)集R(M0)為滿足下面條件的最小集合:
(1)M0∈ R(M0);
(2)若M∈R(M0),且存在t∈T,使得M[t>M’,則M’∈R(M0)。
可達(dá)標(biāo)識(shí)集R(M0)描述了∑所有可能的狀態(tài)。若以R(M0)中的元素為節(jié)點(diǎn),有向弧描述標(biāo)識(shí)間的后繼關(guān)系,可構(gòu)造出∑的可達(dá)圖。
定義3(可達(dá)圖)設(shè)∑=(P, T; F, M0)是Petri網(wǎng),其中M0是初始情態(tài)。∑的可達(dá)圖定義為一個(gè)三元組RG(Σ)=(R(M0), E, Tran),其中:
(1)E={(Mi, Mj)|Mi, Mj∈ R(M0),tk∈ T:Mi[tk>Mj};
(2) 映 射Tran:E→T稱 為 遷 移,Tran(Mi, Mj)=tk當(dāng)且僅當(dāng) Mi[tk>Mj;
稱 R(M0)為 RG(Σ)的頂點(diǎn)集,E 為 RG(Σ)的弧集。若Tran(Mi, Mj)=tk,稱tk為弧(Mi, Mj)的旁標(biāo),通常,將其記為
定義4(出現(xiàn)網(wǎng))設(shè)Σ=(P, T; F, M0)是一個(gè)Petri網(wǎng),Σ的展開是一個(gè)出現(xiàn)網(wǎng)O=(P', T', F';L),其中:
(1)L:P'∪T'→P∪T是標(biāo)號(hào)函數(shù),用于建立P'到P及T'到T的映射,通常稱P'為條件集,T'為事件集,:
圖3:出現(xiàn)網(wǎng)
對(duì)于任意給定的一個(gè)Petri網(wǎng),可由算法1構(gòu)造得到出現(xiàn)網(wǎng)。
算法1 展開Petri網(wǎng)。
輸入:任意一個(gè)Petri網(wǎng)是Σ=(P, T; F, M);
輸出:該P(yáng)etri網(wǎng)的出現(xiàn)網(wǎng)O=(P', T', F'; L)。
(1)將Petri網(wǎng)中每一個(gè)初始托肯所在的庫(kù)所復(fù)制到出現(xiàn)網(wǎng)中;
(2)從Petri網(wǎng)中選擇一個(gè)變遷t;
(3)對(duì)于·t中的每個(gè)庫(kù)所,在出現(xiàn)網(wǎng)中尋找其副本,如果無(wú)法找到,返回步驟2。對(duì)于一個(gè)變遷,不要兩次選擇相同的庫(kù)所子集;
(4)如果被選中的一對(duì)庫(kù)所是沖突關(guān)系或者有前后關(guān)系(即它們不是并發(fā)的),則返回步驟2;
(5)將t復(fù)制到出現(xiàn)網(wǎng)中,稱為t'。從步驟3中找到的每個(gè)庫(kù)所畫一條弧到t';
(6)對(duì)于t·中的每個(gè)庫(kù)所,將其復(fù)制到出現(xiàn)網(wǎng)中,并從t'畫一條弧到這些庫(kù)所;
(7)無(wú)限地重復(fù)步驟2~6。
如上所述,算法1構(gòu)造的出現(xiàn)網(wǎng)是一個(gè)無(wú)限網(wǎng),它在保持Petri網(wǎng)中的各變遷間的關(guān)系(順序、沖突、并發(fā)等)的同時(shí),表示了網(wǎng)內(nèi)所有托肯的轉(zhuǎn)移過(guò)程。
下面通過(guò)一個(gè)例子,來(lái)直觀比較可達(dá)圖和出現(xiàn)網(wǎng)的規(guī)模。
圖1所示的是一個(gè)Petri網(wǎng)。在Petri網(wǎng)存在多個(gè)變遷間的并發(fā)關(guān)系,例如變遷t1和t2,變遷t2和t3,變遷t1和t3,變遷t1和t5等。
圖2是使用開源工具PIPE 4.3生成的圖1所示Petri網(wǎng)的可達(dá)圖截圖。
從圖2可以看出:圖1所示Petri網(wǎng)對(duì)應(yīng)的可達(dá)圖有29個(gè)狀態(tài),在圖2中用橢圓表示。其中,狀態(tài)s1-s27刻畫了并發(fā)變遷產(chǎn)生的狀態(tài)遷移關(guān)系。進(jìn)一步分析,不難看出:隨著Petri網(wǎng)中并發(fā)變遷的數(shù)量增加,可達(dá)圖中的狀態(tài)呈指數(shù)增長(zhǎng),不可避免地會(huì)出現(xiàn)狀態(tài)空間爆炸。
圖3是根據(jù)算法1生成的圖1所示Petri網(wǎng)的出現(xiàn)網(wǎng)。其中,p0-1表示原Petri網(wǎng)中庫(kù)所p0在出現(xiàn)網(wǎng)的生成次序;t0-1表示原Petri網(wǎng)中變遷t0在出現(xiàn)網(wǎng)的生成次序。
對(duì)比圖2和圖3,可以看出:圖3所示出現(xiàn)網(wǎng)的規(guī)模遠(yuǎn)遠(yuǎn)小于圖2所示可達(dá)圖的規(guī)模。由此可以說(shuō)明:基于展開的狀態(tài)空間搜索方法可避免狀態(tài)空間爆炸問(wèn)題
通過(guò)一個(gè)例子,直觀對(duì)比了基于展開的狀態(tài)空間搜索方法和基于可達(dá)圖的狀態(tài)空間搜索方法,以說(shuō)明基于展開的狀態(tài)空間搜索方法可避免狀態(tài)空間爆炸問(wèn)題。