康 輝，張雙雙，2，梅 芳

（1.吉林大學(xué)，計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，長(zhǎng)春130012；2.吉林信息安全測(cè)評(píng)中心，長(zhǎng)春130062）

隨著面向服務(wù)的計(jì)算（Service-oriented computing SOC／Service-oriented architecture，SOA）技術(shù)［1］和業(yè)務(wù)流程管理（Business process management，BPM）技術(shù)［2］的廣泛應(yīng)用以及對(duì)軟件可信性要求越來(lái)越高，很多學(xué)者用π演算和Petri網(wǎng)作為服務(wù)組合和業(yè)務(wù)流程技術(shù)的理論基礎(chǔ)。π演算用來(lái)描述拓?fù)浣Y(jié)構(gòu)動(dòng)態(tài)變化的并發(fā)系統(tǒng)，通過(guò)相應(yīng)的數(shù)學(xué)分析方法，對(duì)系統(tǒng)的屬性和行為進(jìn)行分析。但是π演算［3－7］的進(jìn)程表達(dá)式比較繁瑣，不能形象地反應(yīng)系統(tǒng)物理結(jié)構(gòu)信息，不能刻畫(huà)系統(tǒng)的真并發(fā)行為，而且從系統(tǒng)驗(yàn)證角度來(lái)看，其支持工具少，僅有MVB和HAL等幾種自動(dòng)驗(yàn)證工具，這樣給后續(xù)的形式化驗(yàn)證帶來(lái)了困難。Petri網(wǎng)［8－9］是一種形式化圖形驗(yàn)證工具，它側(cè)重于系統(tǒng)的結(jié)構(gòu)描述和性質(zhì)分析，并且能有效地刻畫(huà)系統(tǒng)真正的并發(fā)語(yǔ)義。它是一種可用網(wǎng)狀圖形表示的系統(tǒng)模型［10－11］，適合描述異步、并發(fā)、分布式的系統(tǒng)，既可用于靜態(tài)的結(jié)構(gòu)分析，又可用于動(dòng)態(tài)的行為分析。

由于π演算存在固有缺陷，很多學(xué)者已經(jīng)在將π演算向Petri網(wǎng)轉(zhuǎn)換這方面做了很多研究［12－13］，例如Raymond Devillers［12］等人已經(jīng)提出了其轉(zhuǎn)換的一般方法。但是對(duì)于π演算中遞歸結(jié)構(gòu)的轉(zhuǎn)換，目前仍然空白。在π演算中，對(duì)遞歸的表達(dá)是其基本的語(yǔ)義，較為簡(jiǎn)單；而在一般Petri網(wǎng)中，對(duì)遞歸的描述非常困難。實(shí)際應(yīng)用π演算時(shí)遞歸結(jié)構(gòu)經(jīng)常出現(xiàn)，因此，本文給出了一種π演算中遞歸結(jié)構(gòu)轉(zhuǎn)換為Petri網(wǎng)的方法。

1 基本概念及轉(zhuǎn)換規(guī)則

1.1 基本概念

關(guān)于π演算的基本概念，在文獻(xiàn)［3］中已有詳細(xì)介紹在此不再贅述。在給出π演算中遞歸表達(dá)式基本形式之前，先看一個(gè)例子：

式（1）中每個(gè)通道a、b、c、…中都保存著一個(gè)數(shù)值h′（這個(gè)數(shù)值可以不一樣），從已知通道a開(kāi)始，讀取通道內(nèi)當(dāng)前值h′加到現(xiàn)有的值上，直到得到的h值大于10時(shí)可以選擇執(zhí)行輸出該值。這樣，從a開(kāi)始到輸出h時(shí)所有計(jì)算過(guò)的通道即是該get函數(shù)的路徑。

在式（1）中，既有自調(diào)用的算子，又有非自調(diào)用的算子，并且有選擇運(yùn)算符“＋”將兩個(gè)進(jìn)程相連。在不滿(mǎn)足遞歸出口條件時(shí)，多次執(zhí)行前綴算子ab獲取下一個(gè)通道，并執(zhí)行計(jì)算h值操作。當(dāng)滿(mǎn)足遞歸出口條件時(shí)，可以選擇繼續(xù)自調(diào)用，也可以終止調(diào)用過(guò)程。

本文給出了一種一般π演算的遞歸表達(dá)式的基本形式：

當(dāng)然，在一些表達(dá)式中也會(huì)出現(xiàn)有多個(gè)自調(diào)用表達(dá)式的形式，比如：

在式（3）至式（5）中，均有兩次自調(diào)用，雖然在轉(zhuǎn)換時(shí)與式（2）有點(diǎn)不同，但基本轉(zhuǎn)換思路大致相同。為了方便描述轉(zhuǎn)換過(guò)程，在本文中，以式（2）這種遞歸形式為例。

為了更好地記錄遞歸運(yùn)算的層次，本文引入軌跡的概念。通常，軌跡一般用來(lái)指進(jìn)程P所依次執(zhí)行的一系列活動(dòng)，一般用〈action1，action2…〉表示。

定義1 軌跡：π演算遞歸結(jié)構(gòu)執(zhí)行時(shí)，為了記錄遞歸運(yùn)算的層次，我們將遞歸調(diào)用的順序稱(chēng)為軌跡，用字母trail表示。調(diào)用一次用σ1表示，調(diào)用第二次用σ2表示，以此類(lèi)推，調(diào)用第n次用σn表示，則進(jìn)程中遞歸結(jié)構(gòu)執(zhí)行的軌跡trail＝〈σ1，σ2，…，σn〉。

定義2 逆軌跡：與軌跡相應(yīng)地，在遞歸返回時(shí)其軌跡稱(chēng)為逆軌跡，記為trail－1，上述遞歸返回的逆軌跡即為trail－1＝〈σn，σn－1，…，σ1〉。

在本文中，π演算進(jìn)程P轉(zhuǎn)換而成的Petri網(wǎng)記為NP，NP是一個(gè)有向連通圖，其節(jié)點(diǎn)分別稱(chēng)為庫(kù)所和變遷。這些節(jié)點(diǎn)通過(guò)有向弧相連。相同類(lèi)型的兩個(gè)節(jié)點(diǎn)之間是不允許相連的。

1.2 轉(zhuǎn)換規(guī)則

遞歸π演算向Petri網(wǎng)轉(zhuǎn)換要遵循一些轉(zhuǎn)換規(guī)則，在本文中將這些規(guī)則概括為兩類(lèi)：基本進(jìn)程的轉(zhuǎn)換規(guī)則以及組合規(guī)則。

1.2.1 基本進(jìn)程轉(zhuǎn)換規(guī)則

對(duì)于向子網(wǎng)K（ρ）的轉(zhuǎn)換，是根據(jù)表達(dá)式ρ的語(yǔ)法樹(shù)，其組成為給定基本子項(xiàng)（進(jìn)程項(xiàng)0，進(jìn)程調(diào)用，內(nèi)部動(dòng)作以及輸入輸出前綴）的圖轉(zhuǎn)換。

由于不涉及任何的名字操作，因此進(jìn)步進(jìn)程項(xiàng)0和內(nèi)部動(dòng)作前綴τ十分簡(jiǎn)單。進(jìn)程調(diào)用X（α1，…，αnX）也類(lèi)似，但是結(jié)果將產(chǎn)生一個(gè)層次變遷，它將通過(guò)標(biāo)識(shí)等價(jià)規(guī)則進(jìn)行激發(fā)變換［10］。

具體的轉(zhuǎn)換規(guī)則如圖1所示。

圖1 空進(jìn)程、啞動(dòng)作τ、進(jìn)程調(diào)用、動(dòng)作前綴向Petri網(wǎng)轉(zhuǎn)換規(guī)則Fig.1 Translation rules from o，τ，the process call and the prefix to Petri nets

1.2.2 組合規(guī)則

本節(jié)中的組合規(guī)則用于合并Petri網(wǎng)的算子，包括前綴組合規(guī)則、選擇組合規(guī)則、并行組合規(guī)則以及范圍處理規(guī)則，其中前3個(gè)規(guī)則給出了合并標(biāo)簽庫(kù)所、相應(yīng)的持有者的方法［12］。

假設(shè)有網(wǎng)Ni＝（∪，Ti，ιi）（i＝1，2）是兩個(gè)不相干的未標(biāo)記的Petri網(wǎng)，并且有?s1，s1∈，?s2，s2∈，如果ι1（s1）＝（λ，D1），ι2（s2）＝（λ，D2），那么D1＝D2，即被相同符號(hào)標(biāo)識(shí)的持有者庫(kù)所也有同樣的值類(lèi)型集合。下面將給出四種組合規(guī)則的形式化處理方法，如圖2所示。前綴組合規(guī)則：N1.N2。假設(shè)N1有唯一的入口控制庫(kù)所和唯一的出口控制庫(kù)所（出口控制庫(kù)所記作s1），通過(guò)如下步驟獲得組合結(jié)果：

（1）網(wǎng)N1和網(wǎng)N2并排放置。

（2）對(duì)應(yīng)每個(gè)s2∈°N2，創(chuàng)建一個(gè)新的庫(kù)所s′2，用符號(hào)i標(biāo)識(shí)，同時(shí)將網(wǎng)N1和網(wǎng)N2中在si和t∈Ti（i∈｛1，2｝）的弧Ψ在新的庫(kù)所s′2和t上標(biāo)記，并使用同樣的注釋符號(hào)和同樣的弧類(lèi)型（無(wú)向或是有向的）標(biāo)記，而后網(wǎng)N1的唯一出口控制庫(kù)所和網(wǎng)N2的出口控制庫(kù)所將被刪除。

（3）對(duì)于有相同標(biāo)識(shí)符號(hào)和類(lèi)型的持有者庫(kù)所將被合并為一個(gè)持有者庫(kù)所，并且如前一樣，具有相同的標(biāo)識(shí)符號(hào)和類(lèi)型，在原來(lái)的網(wǎng)N1和網(wǎng)N2中連接合并的持有者庫(kù)所與變遷之間的弧及注釋標(biāo)識(shí)在合并后的持有者庫(kù)所中保持不變。

1）選擇組合規(guī)則：N1＋N2，可通過(guò)如下過(guò)程獲得圖轉(zhuǎn)換結(jié)果：

①網(wǎng)N1和網(wǎng)N2并排放置。

對(duì)于每個(gè)s1∈°N1和s2∈°N2，創(chuàng)建一個(gè)新的庫(kù)所s，用符號(hào)e標(biāo)識(shí)，并且使得每個(gè)在si和t∈Ti，i∈｛1，2｝的弧Ψ在新的庫(kù)所s和變遷t上作同樣標(biāo)識(shí)，即使用相同的注釋符號(hào)和相同的弧類(lèi)型（無(wú)向或是有向的）；類(lèi)似地，對(duì)于每個(gè)s1∈和s2∈，創(chuàng)建一個(gè)新的庫(kù)所s，用符號(hào)x標(biāo)識(shí)，其連接性與上面規(guī)則定義一致。最后，將原來(lái)在網(wǎng)N1和網(wǎng)N2中標(biāo)識(shí)的入口控制庫(kù)所（被符號(hào)e標(biāo)識(shí)）和出口控制庫(kù)所（被符號(hào)x標(biāo)識(shí)）刪除。

圖2 組合規(guī)則Fig.2 Composition rules

②具有相同名字的持有者庫(kù)所的合并可參見(jiàn)前綴組合規(guī)則。

2）并行組合規(guī)則：N1｜N2，可通過(guò)如下過(guò)程獲得圖轉(zhuǎn)換結(jié)果：

①網(wǎng)N1和網(wǎng)N2并排放置；

②具有相同名字的持有者庫(kù)所的合并可參見(jiàn)前綴組合規(guī)則。

3）范圍處理規(guī)則：N＝sco（N1），可通過(guò)如下過(guò)程獲得圖轉(zhuǎn)換結(jié)果：

①對(duì)于每對(duì)變遷t1，t2∈T1，其中t1和t2分別被snd或rcv所標(biāo)識(shí)，創(chuàng)建一個(gè)新的變遷t，用符號(hào)τ標(biāo)識(shí)，而在變遷t與庫(kù)所s上的弧注釋符號(hào)是在變遷t1與庫(kù)所s以及變遷t2與庫(kù)所s的弧注釋符號(hào)的簡(jiǎn)單合并。在這里注意在snd所標(biāo)識(shí)的變遷周?chē)幕∨crcv所標(biāo)識(shí)的變遷周?chē)幕∈腔ゲ幌喔傻?，所以不需要進(jìn)行反復(fù)的合并操作。

②最后刪除被snd和rcv所標(biāo)識(shí)的變遷以及與其相連接的弧。

2 遞歸π演算向Petri網(wǎng)的轉(zhuǎn)換及等價(jià)性證明

2.1 準(zhǔn)備與討論

類(lèi)似于式（1）中的例子，當(dāng)數(shù)據(jù)h滿(mǎn)足h＞10時(shí)才可以選擇執(zhí)行h.0，因此在執(zhí)行遞歸時(shí)要判斷是否滿(mǎn)足遞歸出口的條件。因此在遞歸調(diào)用和遞歸返回間加入一個(gè)判定庫(kù)所，用來(lái)存儲(chǔ)判定是否滿(mǎn)足遞歸出口條件的判定托肯。判定托肯的形式為F.D或者T.D，其中F.D表示不滿(mǎn)足遞歸出口條件，D表示這個(gè)托肯的類(lèi)型是判定托肯（decision token）；T.D表示滿(mǎn)足遞歸出口條件。

對(duì)于如何記錄當(dāng)前數(shù)據(jù)屬于哪次遞歸操作，本文采用trail.data.place的形式，即當(dāng)前軌跡.數(shù)據(jù)值.所在庫(kù)所的形式存儲(chǔ)在棧庫(kù)所中。

對(duì)于軌跡，在執(zhí)行遞歸調(diào)用時(shí)，調(diào)用一次用σ1標(biāo)記，調(diào)用第二次用σ2標(biāo)記，…，調(diào)用第n次用σn表示，進(jìn)程中遞歸結(jié)構(gòu)執(zhí)行的軌跡trail＝〈σ1，σ2，…，σn〉。例如遞歸主體X（a1，…，an）將用軌跡標(biāo)記為σ1，σ2，…，σn.X（a1，…，an）。對(duì)于遞歸主體后面的Q（a″1，…，a″n），在遞歸返回之前是不執(zhí)行的，在執(zhí)行Q（a″1，…，a″n）時(shí)是按照軌跡〈σ1，σ2，…，σn〉的逆軌跡〈σn，σn－1，…，σ1〉執(zhí)行的。

2.2 遞歸π演算向Petri網(wǎng)的轉(zhuǎn)換

對(duì)于π演算遞歸結(jié)構(gòu)向Petri網(wǎng)的轉(zhuǎn)換，本文采用層次化方法，即將表達(dá)式中的每一個(gè)子表達(dá)式（包括遞歸主體）都先轉(zhuǎn)換成對(duì)應(yīng)的子網(wǎng)，然后組合起來(lái)；如果自調(diào)用表達(dá)式?jīng)]有滿(mǎn)足遞歸出口條件，那么對(duì)自調(diào)用表達(dá)式的網(wǎng)結(jié)構(gòu)進(jìn)行進(jìn)一步細(xì)化，將下一次調(diào)用的網(wǎng)結(jié)構(gòu)展開(kāi)代替上一層中自調(diào)用表達(dá)式對(duì)應(yīng)的網(wǎng)結(jié)構(gòu)。

下面給出關(guān)于式（2）的遞歸結(jié)構(gòu)全景圖第一層，如圖3所示。

說(shuō)明：

（1）最開(kāi)始的庫(kù)所e與最后的庫(kù)所x是此π演算表達(dá)式對(duì)應(yīng)網(wǎng)結(jié)構(gòu)的控制庫(kù)所，這是假設(shè)該表達(dá)式是一個(gè)主式；如果此遞歸π演算表達(dá)式是其他π演算表達(dá)式的子式，這兩個(gè)庫(kù)所應(yīng)換成與外界相連、用于傳遞控制信號(hào)的內(nèi)部庫(kù)所i。

圖3 典型π演算遞歸結(jié)構(gòu)轉(zhuǎn)換結(jié)果全景圖第一層Fig.3 First layer of franslation panoramic view from typical recursionπcalculus to Petri net

（2）圖中的庫(kù)所d是本文新加庫(kù)所——判定庫(kù)所，存儲(chǔ)了判定是否滿(mǎn)足遞歸出口條件的判定托肯F.D和T.D。

（3）在自調(diào)用表達(dá)式對(duì)應(yīng)的網(wǎng)結(jié)構(gòu)與判定庫(kù)所d之間有一條弧相連，表示在執(zhí)行自調(diào)用表達(dá)式時(shí)，其中的條件發(fā)生了變化，這個(gè)變化的條件要及時(shí)傳給判定庫(kù)所，使判定庫(kù)所做出合理的判斷。

（4）在P（a1，…，an）、Q（a″1，…，a″n）等表達(dá)式前進(jìn)行了軌跡的標(biāo)記；而表達(dá)式R（b1，…，bn）卻沒(méi)有軌跡標(biāo)記，因?yàn)樵谶f歸調(diào)用時(shí)此表達(dá)式只執(zhí)行一次。

（5）判定庫(kù)所對(duì)應(yīng)一個(gè)判斷邏輯，嚴(yán)格來(lái)講，如果系統(tǒng)中有多個(gè)遞歸表達(dá)式，則每一個(gè)表達(dá)式單獨(dú)對(duì)應(yīng)一個(gè)判定庫(kù)所。

（6）出于版面考慮，這里沒(méi)有畫(huà)出棧庫(kù)所、名字持有者庫(kù)所、標(biāo)簽庫(kù)所以及相關(guān)弧。

式（2）遞歸結(jié)構(gòu)全景的第二層如圖4所示。

圖4 典型π演算遞歸結(jié)構(gòu)轉(zhuǎn)換結(jié)果全景圖第二層Fig.4 Second layer of translation panoramic view from typical recursionπcalculus to Petri net

類(lèi)似地，調(diào)用多次的π演算表達(dá)式對(duì)應(yīng)的網(wǎng)結(jié)構(gòu)也能夠給出。

對(duì)于形如式（2）的π演算表達(dá)式，采用層次化方法，將π演算遞歸結(jié)構(gòu)轉(zhuǎn)換成Petri網(wǎng)的步驟為：

（1）按照1.2節(jié)中的基本進(jìn)程轉(zhuǎn)換規(guī)則及組合規(guī)則將P（a1，…，an）、R（b1，…，bn）以及Q（a″1，…，a″n）分別轉(zhuǎn)換成對(duì)應(yīng)的子網(wǎng)NP1、NP2、NP3。

（2）將自調(diào)用表達(dá)式X（a′1，…，a′n）先看做一個(gè)整體表示，對(duì)應(yīng)的網(wǎng)結(jié)構(gòu)先用NP0表示。各個(gè)組成部分用構(gòu)造sco（NP1｜NP2｜NP3｜NP0）網(wǎng)連接起來(lái)，這將多種標(biāo)簽庫(kù)所和可能來(lái)自不同部分的有uv和v標(biāo)記的變遷對(duì)合并起來(lái)。這個(gè)構(gòu)造并不合并其他的持有者庫(kù)所。移除所有標(biāo)記為uv和u－v的變遷。

（3）判斷X（a′1，…，a′n）是否滿(mǎn)足遞歸出口條件，若不滿(mǎn)足，將X（a′1，…，a′n）視為X（a1，…，an），轉(zhuǎn)步驟（1）。用不同的標(biāo)記來(lái)記錄不同的調(diào)用；若滿(mǎn)足，轉(zhuǎn)（4）。

（4）將圖3中的變遷P（a1，…，an）用子網(wǎng)NP1替換，如果NP1只有一個(gè)輸入庫(kù)所e，那么將此庫(kù)所與開(kāi)始的庫(kù)所e合并，仍舊記為e；否則創(chuàng)建一個(gè)輔助變遷t1，使開(kāi)始庫(kù)所e指向輔助變遷t1，然后由變遷t1指向NP1所有的輸入庫(kù)所e，再將NP1所有的輸入庫(kù)所e改為內(nèi)部庫(kù)所i。

同樣地，如果NP1只有一個(gè)輸出庫(kù)所x，將此庫(kù)所與最后庫(kù)所x合并，記為x；否則創(chuàng)建一個(gè)輔助變遷t2，使NP1所有的輸出庫(kù)所x指向輔助變遷t2，然后由變遷t2指向最后的庫(kù)所x，再將NP1所有的輸出庫(kù)所x改為內(nèi)部庫(kù)所i。

在用NP2、NP3替換R（b1，…，bn）、Q（a″1，…，a″n）時(shí)也做同樣的處理。

（5）將相同的名字持有者庫(kù)所合并，與原庫(kù)所相連的弧以原方式練到合并后的庫(kù)所上。將需要保存數(shù)據(jù)的變遷用弧與棧庫(kù)所相連。

（6）為了得到完整的變遷網(wǎng)NP，向輸入庫(kù)所中插入一個(gè)小黑點(diǎn)作為托肯，并把下面的通道插入到持有者庫(kù)所中去：

①把ζ（α）插入到每個(gè)α標(biāo)記的持有者庫(kù)所中，其中α∈domain（ζ）；

②把a(bǔ).a.K插入到標(biāo)簽庫(kù)所中，其中對(duì)于每一個(gè)a∈konwn（ζ）；

③把n.N插入到標(biāo)簽庫(kù)所中，其中n∈C＼konwn（ζ）；

④把Δ.R插入到標(biāo)簽庫(kù)所中，其中Δ∈rstr（ζ）。

2.3 互模擬等價(jià)

本文定義了從遞歸π演算到Petri網(wǎng)的語(yǔ)義轉(zhuǎn)換，從而產(chǎn)生了有限結(jié)構(gòu)轉(zhuǎn)換網(wǎng)——NP，它是具有有限庫(kù)所、變遷和弧的網(wǎng)結(jié)構(gòu)，該遞歸結(jié)構(gòu)的標(biāo)號(hào)遷移系統(tǒng)ItsP與轉(zhuǎn)換后的Petri網(wǎng)所對(duì)應(yīng)的標(biāo)號(hào)遷移系統(tǒng)ItsNp是強(qiáng)互模擬。

定理1 NP是具有有限庫(kù)所、變遷和弧的Petri網(wǎng)圖，并且使得ItsP和ItsNp是互為強(qiáng)互模擬的標(biāo)號(hào)遷移系統(tǒng)。

證明 基本π演算部分的Petri網(wǎng)語(yǔ)義等價(jià)證明在文獻(xiàn)［12］中詳細(xì)介紹了轉(zhuǎn)換的思想、方法以及相關(guān)的語(yǔ)義等價(jià)證明，在此不再贅述。

關(guān)于遞歸結(jié)構(gòu)的Petri網(wǎng)語(yǔ)義等價(jià)的證明采用數(shù)學(xué)歸納法。具體如下：

設(shè)K為遞歸結(jié)構(gòu)執(zhí)行次數(shù)，即遞歸層數(shù)。

（1）當(dāng)K＝1時(shí)，按照文中所述遞歸π演算向Petri網(wǎng)的轉(zhuǎn)換方法，其直接轉(zhuǎn)換為不帶遞歸結(jié)構(gòu)的基本π演算，其互模擬等價(jià)性是已知的。

（2）假設(shè)當(dāng)K＝n時(shí)，從遞歸π演算向Petri網(wǎng)的轉(zhuǎn)換具有互模擬等價(jià)性，那么證明當(dāng)K＝n＋1時(shí)互模擬等價(jià)仍成立。由于當(dāng)K＝n時(shí)，前n層的遞歸調(diào)用已經(jīng)實(shí)現(xiàn)，即可以將前n層遞歸調(diào)用得到的π演算表達(dá)式看做一個(gè)復(fù)雜無(wú)遞歸的基本π演算表達(dá)式，這樣再加上第n＋1層的遞歸調(diào)用轉(zhuǎn)化為（1）中的形式，此時(shí)K′＝1，符合（1）中所證互模擬等價(jià)。因此當(dāng)K＝n＋1時(shí)遞歸π演算向Petri網(wǎng)轉(zhuǎn)化的互模擬等價(jià)性成立。證畢。

對(duì)不同密度、不同施肥處理的相對(duì)增加量進(jìn)行雙因素方差分析，結(jié)果表明(表5)：3種不同施肥處理并未對(duì)毛竹相對(duì)增產(chǎn)量產(chǎn)生顯著差異(P=0.138>0.05)；在試驗(yàn)所設(shè)2種密度中，低密度毛竹林相對(duì)增加產(chǎn)量顯著高于高密度毛竹林(P=0.023<0.05)。

3 更簡(jiǎn)潔的Petri網(wǎng)表示

Petri網(wǎng)是一個(gè)很好的描述與分析并行系統(tǒng)的模型。但是當(dāng)遞歸結(jié)構(gòu)遞歸的次數(shù)較多時(shí)，會(huì)產(chǎn)生巨大的Petri網(wǎng)。尤其是在實(shí)際應(yīng)用中，如果系統(tǒng)過(guò)大或較復(fù)雜時(shí)，會(huì)遇到結(jié)點(diǎn)數(shù)過(guò)多的情況。系統(tǒng)的組合狀態(tài)數(shù)又隨結(jié)點(diǎn)數(shù)成指數(shù)函數(shù)增長(zhǎng)，這就是所謂的組合爆炸問(wèn)題。解決結(jié)點(diǎn)數(shù)過(guò)多引起的組合爆炸問(wèn)題的辦法是盡量減少模型的結(jié)點(diǎn)個(gè)數(shù)。為了使轉(zhuǎn)換后的Petri網(wǎng)較為簡(jiǎn)潔，本文給出了壓縮的Petri網(wǎng)圖，它保留了系統(tǒng)的語(yǔ)義，并編碼完全相同的軌跡集合。

3.1 一種更簡(jiǎn)潔的Petri網(wǎng)表示

分析如式（2）形式的π演算的遞歸結(jié)構(gòu)，如果該π演算表達(dá)式不滿(mǎn)足遞歸出口條件，那么會(huì)循環(huán)執(zhí)行自調(diào)用表達(dá)式之前的子表達(dá)式P（a1，…，an），執(zhí)行過(guò)程大致如圖5所示。

如果π演算表達(dá)式的遞歸結(jié)構(gòu)執(zhí)行多次，那么會(huì)產(chǎn)生巨大的Petri網(wǎng)，因此本文考慮將其進(jìn)行簡(jiǎn)化，得到一種更簡(jiǎn)潔的Petri網(wǎng)表示。受圖3啟發(fā)，本文將典型π演算遞歸結(jié)構(gòu)轉(zhuǎn)換結(jié)果用全景圖表示，如圖6所示。

這里需要考慮以下幾個(gè)問(wèn)題：

圖5 π演算表達(dá)式遞歸結(jié)構(gòu)執(zhí)行圖Fig.5 Execution ofπcalculus expression recursive structure

圖6 一種更簡(jiǎn)潔的Petri網(wǎng)表示Fig.6 A more compact representation of Petri net

對(duì)于遞歸出口之前每次執(zhí)行的表達(dá)式P（a1，…，an），其每次具體執(zhí)行是不一樣的，我們?cè)谄淝懊嬗密壽E標(biāo)記，表示按照軌跡σ1，σ2，…，σn執(zhí)行，這里的軌跡是根據(jù)判定庫(kù)所的變化一步一步生成的。然后在執(zhí)行遞歸返回時(shí)，Q（a″1，…，a″n）按照軌跡σ1，σ2，…，σn的逆軌跡σn，σn－1，…，σ1執(zhí)行。

3.2 等價(jià)性證明

本文給出了Np的一種更簡(jiǎn)潔Petri網(wǎng)表示，記為Nc，它是具有有限庫(kù)所、變遷和弧的網(wǎng)結(jié)構(gòu)，保留了系統(tǒng)的語(yǔ)義，編碼完全相同的軌跡集合。

定理2 Nc是具有有限庫(kù)所、變遷和弧的Petri網(wǎng)圖，并且使得Np和Nc編碼完全相同的軌跡集合（激發(fā)順序）。

證明 針對(duì)遞歸結(jié)構(gòu)，分別從遞歸調(diào)用、遞歸出口及遞歸返回三部分考慮其執(zhí)行的軌跡集合。

（1）對(duì)每次遞歸調(diào)用執(zhí)行的表達(dá)式P（a1，…，an），Np和Nc的執(zhí)行軌跡均為｛σ1，σ2，…，σn｝。

（2）對(duì)遞歸出口執(zhí)行的表達(dá)式R（b1，…，bn），由于只執(zhí)行一次，因此其軌跡集合可以忽略。

（3）對(duì)遞歸返回表達(dá)式Q（a″1，…，a″n），Np和Nc的軌跡集合均為｛σn，σn－1，…，σ1｝。證畢。

4 結(jié)束語(yǔ)

通過(guò)對(duì)π演算遞歸結(jié)構(gòu)和Petri網(wǎng)的經(jīng)典理論進(jìn)行研究分析，本文首先給出了遞歸π演算的基本形式，然后將遞歸π演算向Petri網(wǎng)進(jìn)行轉(zhuǎn)換，并證明這種轉(zhuǎn)換的互模擬等價(jià)性；隨后針對(duì)多次遞歸的情況對(duì)由π演算遞歸結(jié)構(gòu)轉(zhuǎn)換得到的Petri網(wǎng)進(jìn)行簡(jiǎn)化，得到了一種保持系統(tǒng)語(yǔ)義的、編碼完全相同的軌跡集合的更簡(jiǎn)潔的Petri網(wǎng)，與原Petri網(wǎng)相比能夠提高對(duì)于模型驗(yàn)證的效率，比如對(duì)移動(dòng)系統(tǒng)的驗(yàn)證等。

［1］Thomas E.Service-Oriented Architecture（SOA）：Concepts，Technology，and Design［M］.New Jersey：Prentice Hall，2005.

［2］Leymann F，Roller D，Schmidt M T.Web services and business process management［J］.IBM Systems Journal，2002，41（2）：198-211.

［3］Milner R，Parrow J，Walker D.A calculus of mobile processes part I／II［J］.Journal of Information and Computation，1992，100（1）：1-77.

［4］Milner R.Communication and Concurrent［M］. New Jersey：Pretice Hall，1989.

［5］Roland Meyer.A theory of structural stationarity in theπ-Calculus［J］.Acta Informatica，2009，46：87-137.

［6］Michele B，Davide S.A fully abstract semantics for causality in the Pi calculus［C］∥Proceedings of STACS＇95，LNCS，Springer，1995，900：243-254.

［7］Baeten J C M，Bergstra J A，Klop J W.An operational semantics for process algebra［J］.Mathematical Problems in Computation Theory，1988，21：47-81.

［8］Eile B，Raymond D，Maciei K.Petri Net Algebra［M］.Bolin：Springer，2001.

［9］Ulrich B，Daniel M.Object-oriented concepts for coloured Petri nets［C］∥IEEE International Conference on Systems，Man and Cybernetics，1993，3：279-286.

［10］Peschanski F，Klaudel H，Devillers R.A Petri Net Interpretation of Open Reconfigurable Systems［C］∥PETRI NETS 2011，LNCS 6709，2011：208-227.

［11］Christensen S，Hansen N D.Coloured Petri nets extended with place capacities，test arcs and inhibitor arcs［J］.Application and Theory of Petri Nets，1993，691：186-205.

［12］Raymond D，Hanna K，Maciej K.A compositional Petri net translation of general Pi calculus terms［J］. Formal Aspects of Computing，2008，20：429-450.

［13］Peschanski F，Klaudel H，Devillers R.A decidable characterization of a graphical pi-calculus with iterators［C］∥In：Infinity.EPTCS，2010，39：47-61.