2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院1第14章形式化方法形式化方法提供了規(guī)約環(huán)境的基礎(chǔ)，它使得所生成的分析模型比用傳統(tǒng)的或面向?qū)ο蟮姆椒ㄉ傻哪Ｐ透暾?、一致和無二義性。本章內(nèi)容：14.1基礎(chǔ)知識14.2有限狀態(tài)機(jī)（FSM）14.3PETRI網(wǎng)基本原理2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院214.1基礎(chǔ)知識形式化方法的定義：[定義14.1]：用于開發(fā)計(jì)算機(jī)系統(tǒng)的形式化方法是描述系統(tǒng)性質(zhì)的基于數(shù)學(xué)的技術(shù)。這樣的形式化方法提供了一個(gè)框架，人們可以在框架中以系統(tǒng)的方式刻畫、開發(fā)和驗(yàn)證系統(tǒng)。形式化規(guī)約的目標(biāo)：無二義性、一致性和完整性。注：使用形式化方法，完整性是難以達(dá)到的。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院314.1.1形式化方法概念例14-1：符號表：它由一組沒有重復(fù)的項(xiàng)構(gòu)成。如圖14-1所示。程序被用于維護(hù)一個(gè)符號表，在許多不同類型的應(yīng)用中使用此符號表。

圖14-1符號表2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院4例14-1如果對于上表有一個(gè)陳述：包括不多于MaxIds的用戶名，那么就為表設(shè)定了一個(gè)限制，這就稱為數(shù)據(jù)不變式的條件的一個(gè)構(gòu)成成分。數(shù)據(jù)不變式是一個(gè)條件，它在包含一組數(shù)據(jù)的系統(tǒng)的執(zhí)行過程中總保持為真。上面討論的符號表的數(shù)據(jù)不變式有兩個(gè)構(gòu)成成分：（1）表中包含的名字?jǐn)?shù)不超過MaxIds。（2）在表中沒有重復(fù)的名字。在上面描述的符號表程序的情形下，這意味系統(tǒng)執(zhí)行過程中無論什么時(shí)候檢查符號表，它將總是包含不超過MaxIds的職員標(biāo)識符，并且沒有重復(fù)。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院5形式化方法概念狀態(tài)的概念，在形式化方法的語言環(huán)境中，狀態(tài)是系統(tǒng)訪問和修改的存儲數(shù)據(jù)。在上述符號表程序的例子中，狀態(tài)是符號表。操作的概念，這是在系統(tǒng)中發(fā)生的讀或?qū)憼顟B(tài)數(shù)據(jù)的動(dòng)作。如果對符號表程序考慮從符號表加入或移出職員名，則它將關(guān)聯(lián)兩個(gè)操作：一個(gè)是加一個(gè)指定名到符號表中的操作，另一個(gè)是從表中移出一個(gè)現(xiàn)存名的操作。如果程序提供檢查某指定名是否包含在表中的機(jī)制，則有一個(gè)返回某種表示名字是否在表中的指示值的操作。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院6一個(gè)操作和兩個(gè)條件相關(guān)聯(lián)：前置條件和后置條件。前置條件定義某特定操作在其中合法的環(huán)境。操作的后置條件定義當(dāng)操作完成后所產(chǎn)生的現(xiàn)象，是通過其對狀態(tài)的影響來定義的。在加標(biāo)識符到職員標(biāo)識符符號表的操作的例子中，后置條件已經(jīng)將數(shù)學(xué)的刻畫表增加了新標(biāo)識符。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院714.1.2形式化規(guī)約語言形式化規(guī)約語言通常由三個(gè)主要的成分構(gòu)成：（1）語法，定義用于表示規(guī)約的特定符號。（2）語義，幫助定義用于描述系統(tǒng)的“對象的全域（universeofobjects）”。（3）一組關(guān)系，定義確定出哪個(gè)對象真正滿足規(guī)約的規(guī)則。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院8Z的符號的縮略集合：集合：S∶PX S被聲明為X的集合。x∈S x是S中的成員。xS x不是S中的成員。ST S是T的子集：S中每個(gè)元素均在T中。S∪T S和T的并：包含在S或T或兩者中的每個(gè)元素。S∩T S和T的交：包含同時(shí)在S和T中的元素。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院9S＼T S和T的差：包含在S中的而不在T中的每個(gè)元素。 空集：不包含任何成員。｛x｝ 單元素集：僅僅包含x元素。N 自然數(shù)集合：0，1，2，…S∶FX S被聲明為X的有限集。Max(S) 數(shù)的非空集合S中的最大元素。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院10功能：f∶xy

f被聲明為從x到y(tǒng)的部分內(nèi)射。domf

f的定義域:f(x)有定義的值x的集合ranf

f的值域:x在f的定義域上變化而形成的f(x)值的集合。f⊕｛xy｝ 一個(gè)和f相同的函數(shù)，除了x被映射到y(tǒng)(x)值的集合。｛x｝f

一個(gè)和f相似的函數(shù)，除了x被從定義域中去除。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院11邏輯：P∧Q P與Q同時(shí)為真時(shí)才為真。PQ

P蘊(yùn)含Q：或者Q為真或者P為假時(shí)為真。θS'=θS

在操作中schemaS中沒有成分改變。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院12例14-2例14-2：下面用Z語言schema的例子描述了塊處理器的狀態(tài)和數(shù)據(jù)不變式：2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院1314.2有限狀態(tài)機(jī)（FSM）很多實(shí)時(shí)系統(tǒng)，特別是實(shí)時(shí)控制系統(tǒng)，其整個(gè)分析機(jī)制與系統(tǒng)的狀態(tài)有相當(dāng)大的關(guān)系。有限狀態(tài)機(jī)由有限的狀態(tài)和相互之間的轉(zhuǎn)移構(gòu)成，在任何時(shí)候只能是給定數(shù)目的狀態(tài)中的一個(gè)。主要有兩種方法來建立有限狀態(tài)機(jī)，一種是“狀態(tài)轉(zhuǎn)移圖”，另一種是“狀態(tài)轉(zhuǎn)移表”，分別用圖形方式和表格方式建立有限狀態(tài)機(jī)。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院14有限狀態(tài)機(jī)的組成如下：（1）一個(gè)有限的狀態(tài)集合Q。（2）一個(gè)有限的輸入集合I。（3）一個(gè)變遷函數(shù)δ：Q×I→Q變遷函數(shù)也是一個(gè)狀態(tài)函數(shù)，在某一狀態(tài)下，給定輸入后，F(xiàn)SM轉(zhuǎn)入該函數(shù)產(chǎn)生的新狀態(tài)。δ的定義域內(nèi)的某些數(shù)值可以是未定義的。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院15簡單有限狀態(tài)機(jī)圖14-2中的左圖表明該FSM有q0、q1、q2、q3四個(gè)狀態(tài)，輸入集中有a、b、c、ｄ四個(gè)元素；右圖中各個(gè)狀態(tài)之間的轉(zhuǎn)換關(guān)系則更清晰。有限狀態(tài)機(jī)非常適合于描述這樣的系統(tǒng)：系統(tǒng)含有有限個(gè)狀態(tài)，不同事件的發(fā)生可以用不同狀態(tài)之間的轉(zhuǎn)換來模擬。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院16有限狀態(tài)機(jī)的特點(diǎn)有限狀態(tài)機(jī)的優(yōu)點(diǎn)在于簡單易用，狀態(tài)間的關(guān)系能夠直觀看到。但應(yīng)用在實(shí)時(shí)系統(tǒng)中時(shí)，其最大的缺點(diǎn)是：任何時(shí)刻系統(tǒng)只能有一個(gè)狀態(tài)，無法表示并發(fā)性，不能描述異步并發(fā)的系統(tǒng)。另外，在系統(tǒng)部件較多時(shí)，狀態(tài)數(shù)隨之增加，導(dǎo)致復(fù)雜性顯著增長。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院1714.3Petri網(wǎng)基本原理Petri網(wǎng)在軟件分析中，是一種系統(tǒng)的數(shù)學(xué)和圖形的描述與分析的方法。對于具有并發(fā)、異步、分布、并行、不確定性或隨機(jī)性的信息處理系統(tǒng)，都可以利用Petri網(wǎng)構(gòu)造出要開發(fā)的Petri網(wǎng)模型。這種模型可以表示系統(tǒng)結(jié)構(gòu)和動(dòng)態(tài)行為方面的信息。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院18由于Petri網(wǎng)的表示方法是用圖形工具。因此其表示形式與傳統(tǒng)方法的結(jié)構(gòu)圖、流程圖具有同樣的直觀、形象效果。其特別之處在于可以使用標(biāo)記模擬系統(tǒng)的動(dòng)態(tài)行為和并發(fā)活動(dòng)。另一方面，作為一種數(shù)學(xué)工具，便于計(jì)算和驗(yàn)證系統(tǒng)的數(shù)學(xué)方程。它可以建立狀態(tài)方程、代數(shù)方程以及系統(tǒng)行為的其他數(shù)學(xué)模型。因此，系統(tǒng)開發(fā)人員和理論研究工作者都可以根據(jù)需要利用Petri網(wǎng)。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院1914.3.1靜態(tài)結(jié)構(gòu)Petri網(wǎng)的基本成分可以表示為一個(gè)三元組：N=（P，T；F）并滿足以下條件：（1）P∪T≠ф。（2）P∩T=ф。（3）F（P×T）∪（T×P）。（4）DOM（F）∪COD（F）=P∪T。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院20其中：P={p1，p2，…，pn}是N的有窮位置集合。T={t1，t2，…，tn}是N的有窮轉(zhuǎn)移集合。F是由N中一個(gè)P元素和一個(gè)T元素組成的有序偶的集合。DOM（F）={x│y：（y，x）∈F}，COD（F）={x│y：（x，y）∈F}。如果用圓圈表示位置，用矩形框表示轉(zhuǎn)移，用有向邊表示位置與轉(zhuǎn)移的有序偶，那么就構(gòu)成了Petri網(wǎng)的圖形表示。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院21例14-3:N的Petri網(wǎng)例14-3：N的Petri網(wǎng)

N=（P，T；F）P={p1，p2，p3，p4，p5，p6}T={t1，t2，t3，t4，t5，t6}F={(p1，t1)，(t1，p2)，(p2，t2)，(t2，p1)，(p1,

t3)，(t3，p3)，(t3，p4)，(p3，t4)，(p4，t5)，(t4，p5)，(t5，p6)，(p5，t6)，(p6，t6)}N的Petri網(wǎng)圖形表示，如圖14-3所示。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院22圖14-3N的Petri網(wǎng)的圖形表示2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院2314.3.2動(dòng)態(tài)特征具有動(dòng)態(tài)特征的Petri網(wǎng)就可以表示為六元組：∑=（P，T；F，K，W，M0）其中：（P，T；F）的含義與前面靜態(tài)結(jié)構(gòu)中的含義相同。K：P→N+∪{w}，是位置上容量函數(shù)，N+={1，2，3，…}；若K(p)=w，表示位置p的容量為無窮。W：F→N+，是弧集合上的權(quán)函數(shù)。M：P→N0，是Petri網(wǎng)∑的標(biāo)識（marking），M0為初始標(biāo)識，N0={0，1，2，3，…}，p∈P，必須滿足M（p）≤K（p）。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院24在Petri網(wǎng)的圖形表示中，?。▁，y）上的W值標(biāo)在?。▁，y）上，M(p)的值不是用數(shù)字，而是用實(shí)心點(diǎn)表示，即在位置P對應(yīng)的圓圈中標(biāo)注M(p)個(gè)實(shí)心點(diǎn)，每個(gè)實(shí)心點(diǎn)稱為一個(gè)標(biāo)記（token）。同一位置中的諸多標(biāo)記代表同一類完全等價(jià)的個(gè)體。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院25例14-4：具有M0和W的Petri網(wǎng)可以表示為如圖14-4所示。圖14-4具有M0和W的Petri網(wǎng)

2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院26對于圖14-4所示的Petri網(wǎng)：M0=（1，0，0，0，0，0）W（t2，p1）=W（t5，p6）=W（t6，p1）=4W（t3，p3）=6W（t4，p5）=5W（p1，t3）=W（p3，t4）=W（p5，t6）=W（p6，t6）=W（t3，p4）=W（p4，t5）=W（p1，t1）=W（t1，p2）=W（p2，t2）=12022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院2714.3.3轉(zhuǎn)移啟動(dòng)規(guī)則前面介紹的Petri網(wǎng)的動(dòng)態(tài)特征是Petri網(wǎng)的動(dòng)態(tài)行為的特性描述。這種動(dòng)態(tài)行為是通過轉(zhuǎn)移啟動(dòng)引起標(biāo)識改變的變化來體現(xiàn)的。而轉(zhuǎn)移啟動(dòng)則要有可以啟動(dòng)轉(zhuǎn)移（轉(zhuǎn)移有效）的條件和啟動(dòng)規(guī)則。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院281.轉(zhuǎn)移t有效的條件若在標(biāo)識M下，p1，p1∈*tM（p1）≥W（p1，t），且：p2，p2∈t*M（p2）＋W（t，p2）≤K（p2）此時(shí)稱t在M下有效，記為M[t＞。在定義轉(zhuǎn)移有效的條件時(shí)，如果一個(gè)沒有任何輸入位置的轉(zhuǎn)移叫源轉(zhuǎn)移，一個(gè)源轉(zhuǎn)移的有效是無條件的。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院292.轉(zhuǎn)移t啟動(dòng)的結(jié)果若t在M下有效，t就可以啟動(dòng)。啟動(dòng)后將M變成新標(biāo)識M’，記為M[t＞M’或MM’，并稱M’為M的后繼標(biāo)識。在定義轉(zhuǎn)移t啟動(dòng)的結(jié)果時(shí)，如果一個(gè)沒有任何輸出位置的轉(zhuǎn)移叫潭轉(zhuǎn)移，一個(gè)潭轉(zhuǎn)移的啟動(dòng)將消耗標(biāo)記，而不產(chǎn)生任何標(biāo)記。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院30轉(zhuǎn)移啟動(dòng)規(guī)則例圖圖14-5轉(zhuǎn)移啟動(dòng)規(guī)則的Petri網(wǎng)

2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院31圖14-6混惑的Petri網(wǎng)2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院32并發(fā)與沖突1）并發(fā)設(shè)M為Petri網(wǎng)∑的一個(gè)標(biāo)識，若存在t1和t2使得M[t1＞和M[t2＞，并滿足M[t1＞M1M1[t2＞，且M[t2＞M2M[t1＞，則稱t1和t2在M下并發(fā)。就是說在M標(biāo)識下，t1和t2都有效，且它們當(dāng)中任一個(gè)轉(zhuǎn)移，啟動(dòng)都不會使另一個(gè)轉(zhuǎn)移無效。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院332）沖突設(shè)M為Petri網(wǎng)∑的一個(gè)標(biāo)識，若存在t1和t2使得M[t1＞和M[t2＞，并滿足M[t1＞M1]M1[t2＞，且M[t2＞M2]M2[t1＞，則稱t1和t2在M下沖突，就是說在M標(biāo)識下，t1和t2都有效，但t1和t2中只有一個(gè)能啟動(dòng)，而且其中任一個(gè)轉(zhuǎn)移啟動(dòng)都會使另一個(gè)轉(zhuǎn)移無效。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院3414.3.4行為特性1.可達(dá)性2.有界性3.活性4.可逆性5.可覆蓋性6.持久性7.同步距離8.公平性2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院3514.3.5行為特性分析方法行為特性分析方法分為三類：（1）可覆蓋性（可達(dá)性）樹。這種方法實(shí)質(zhì)上包含了所有可達(dá)標(biāo)識或它們的可覆蓋標(biāo)識的枚舉，適用于所有類型的網(wǎng)。但由于“狀態(tài)空間的爆炸”的問題，它只限制于規(guī)模較小的網(wǎng)。（2）矩陣方程求解。這種方法求解能力強(qiáng)，但在許多情況下，它僅適用于Petri網(wǎng)的一些特殊子類或特殊情況。（3）分層或化簡。這種方法是在保證網(wǎng)系統(tǒng)要分析的性質(zhì)不變的情況下進(jìn)行分層或化簡，它涉及一些變換方法的研究，許多問題有待探索。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院361.不變量所謂不變量是指網(wǎng)系統(tǒng)中有S-不變量和T-不變量。

例14-5：如圖14-7所示的是不變量的Petri網(wǎng)。圖14-7不變量的Petri網(wǎng)2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院37例14-6：如圖14-8所示顯示的是不變量的Petri網(wǎng)圖14-8顯示的是不變量的Petri網(wǎng)

2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院38例14-7：如圖14-9所示顯示的是不變量的Petri網(wǎng)圖14-9顯示的是不變量的Petri網(wǎng)2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院392.狀態(tài)方程如果N=（P，T；F）是純網(wǎng)，則C與N存在一一對應(yīng)的關(guān)系。在此，用m維列向量來表示標(biāo)識M，即M=[M(p1)，M(p2），…，M(pm)]T。這樣，M[tJ＞的充分必要條件則為：

i∈{1，2，…，m}：(C－)Tij≤M(i)或?qū)憺椋?C－)T*j≤M其中(C－)T*j表示矩陣(C－ij)T的第j列。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院40如果M1[tj＞M2，則有M2=M1+CT*j。若M0[σ＞M，就可以推出狀態(tài)方程為：M=M0+CT·U其中CT·U是矩陣乘法；σ是轉(zhuǎn)移序列，U是T-向量，它以tj為序標(biāo)的分量值為tj在σ中出現(xiàn)的次數(shù)，即U(tj)=#(tj/σ)；M0是∑的初始標(biāo)識的S-向量表示，由σ導(dǎo)出的可達(dá)標(biāo)識M也表示為S-向量的形式。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院413.關(guān)聯(lián)矩陣[定義14-2]：設(shè)∑=（N，M0），其中N=（P，T；F）是一個(gè)純網(wǎng)，即x∈X：*x∩x*=。其中：P={p1，p2，…，pm}T={t1，t2，…，tn}（1）用S-元素作序標(biāo)的列向量V：P→Z稱為∑的S-向量。（2）用T-元素作序標(biāo)的列向量U：T→Z稱為∑的T-向量。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院42（3）用T×P作序標(biāo)的矩陣C：T×P→Z稱為∑的關(guān)聯(lián)矩陣，其矩陣元素C(tj，pi)=W(tj，pi)－W(pi，tj)。也可寫作：

[Cji]n×m=[C+ji]n×m－[C－ji]n×m或：C=C+－C－2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院43定義14-2其中：C+ji就是從轉(zhuǎn)移j到它的輸出位置i的弧的權(quán)，C－ji是轉(zhuǎn)移的輸入位置i到轉(zhuǎn)移j的弧的權(quán)。從轉(zhuǎn)移規(guī)則很容易可以看出，C－ji、C+ji和Cji分別表示當(dāng)轉(zhuǎn)移j一旦啟動(dòng)（發(fā)生），位置i中標(biāo)記取走、增加和改變的數(shù)量。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院44關(guān)聯(lián)矩陣一般表示

其中Cji表示取走、增加后產(chǎn)生的變化數(shù)。此關(guān)聯(lián)矩陣給出了系統(tǒng)∑的結(jié)構(gòu)。

2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院454.用關(guān)聯(lián)矩陣和狀態(tài)方程求不變量通過網(wǎng)系統(tǒng)的關(guān)聯(lián)矩陣和狀態(tài)方程，就可以很方便地求出S-不變量。設(shè)I是∑的S-不變量，M∈[M0＞，則：IT·M=IT·M0設(shè)σ是從M0到M的轉(zhuǎn)移序列：M0[σ＞M。于是M0+CT·U=M，其中U是對應(yīng)于σ的T-向量，對所有tj∈T，U(tj)是tj在σ中出現(xiàn)的次數(shù)。兩邊同時(shí)乘以IT，則得：IT·M0+IT·CT·U=IT·M因?yàn)镮為S-不變量，則IT·CT=(C·I)T=θT，θ是分量全為0的T-向量。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院46定義14-3[定義14-3]：設(shè)I為系統(tǒng)∑的一個(gè)S-向量，C是∑的關(guān)聯(lián)矩陣，CT是C的轉(zhuǎn)置矩陣。（1）若C·I=θ，就稱I為∑的S-不變量。（2）若‖I‖={si∈S│I(si)＞0}稱為S-不變量I的子集。（3）若I>θs，就稱I為非負(fù)S-不變量，其中θs為分量全為0的S-向量。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院47（4）若不存在比I小的非負(fù)S-不變量，即不存在非負(fù)S-不變量I’，使θs＜I’＜I，就說I是最小非負(fù)S-不變量。（5）θs也稱為∑的S-不變量。但若它是惟一的S-不變量，就說∑沒有S-不變量。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院48定義14-4[定義14-4]：設(shè)J為系統(tǒng)∑的一個(gè)T-向量，θs為零S-向量，則：（1）只要CT·J=θs，即在S所引起的變化均為0，就說J是∑的T-不變量。（2）若T-不變量J＞θ，就說J是非負(fù)T-不變量。（3）‖J‖={tj∈T│J(tj)＞0}稱為T-不變量J的子集。（4）非負(fù)T-不變量J是最小的。如果不存在比J更小的非負(fù)T-不變量，即不存在非負(fù)T-不變量J’，使θ<J’<J。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院495.狀態(tài)方程的應(yīng)用前面介紹了不變量，狀態(tài)方程，關(guān)聯(lián)矩陣，用關(guān)聯(lián)矩陣和狀態(tài)方程求不變量。現(xiàn)在用這些基礎(chǔ)及狀態(tài)方程在可達(dá)性分析方面的應(yīng)用。狀態(tài)方程M=M0+CT·U為部分解決可達(dá)性問題提供了一個(gè)依據(jù)。若Md從M0可達(dá)，則方程CT·U=Md-M0=△M必然存在一個(gè)非負(fù)整數(shù)解Ux，該解即為啟動(dòng)計(jì)數(shù)向量。若無這樣的解，Md就不能從M0到達(dá)。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院50例14-8：作為一個(gè)舉例，考察圖14-10所示的Petri網(wǎng)圖14-10狀態(tài)方程在可達(dá)性分析的Petri網(wǎng)

2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院51例14-8分析2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院52在狀態(tài)M0下，轉(zhuǎn)移t3是有效的。設(shè)M1是啟動(dòng)t3所得到的標(biāo)識。則有：2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院53啟動(dòng)序列θ=t3t2t3t2t1表示成啟動(dòng)計(jì)數(shù)向量（1，2，2），啟動(dòng)后產(chǎn)生的新標(biāo)識：2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院54考查標(biāo)識，它可以從標(biāo)識M0到達(dá)，方程：2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院55有一個(gè)解U=（0，4，5），它對應(yīng)于啟動(dòng)序列σ=t3t2t3t2t3t2t3t2t3。再考查標(biāo)識，因方程：無解，所以標(biāo)識為不可達(dá)標(biāo)識。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院56例14-9：考察圖14-11所示的Petri網(wǎng)圖14-11狀態(tài)方程在可達(dá)性分析的Petri網(wǎng)

在圖14-11所示的Petri網(wǎng)中：

M0=CT=方程:=+U有一個(gè)解U=(1,1)。這個(gè)解對應(yīng)的兩個(gè)可能啟動(dòng)序列為t1t2或t2t1，而這兩個(gè)序列都不是有效啟動(dòng)序列。因?yàn)樵贛0下，t1、t2都不是有效的。

2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院57例14-9分析△M=M0=

若取初始標(biāo)識為：

M’0=

M’=M’0+CT

則為可達(dá)的，且對應(yīng)于啟動(dòng)計(jì)數(shù)向量的啟動(dòng)序列為t1t2。

2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院5814.3.6結(jié)構(gòu)特性分析方法Petri網(wǎng)有它的拓?fù)浣Y(jié)構(gòu)。結(jié)構(gòu)特性依賴于Petri網(wǎng)的拓?fù)浣Y(jié)構(gòu)。這些特性適合于網(wǎng)的任何初始標(biāo)識，也就是說這些特性是獨(dú)立于網(wǎng)的初始標(biāo)識M0的。簡單地講，這些特性只與起始于某個(gè)初始標(biāo)識的特定啟動(dòng)序列有關(guān)。因此，這些特性通?？梢杂藐P(guān)聯(lián)矩陣C及其相關(guān)的次方程或不等式來刻畫。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院59首先約定：假設(shè)本節(jié)所涉及的網(wǎng)都是純網(wǎng)（沒有自環(huán)）。用X(i)表示向量X的第i項(xiàng)。就向量X和Y來說，X＞Y是指對每個(gè)i都有X(i)＞Y(i)；X≥Y是指對每個(gè)i都有X(i)≥Y(i)；而X＞≠Y則表示X≥Y，但必須存在某些i使得X(i)≠Y(i)。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院60對于Petri網(wǎng)N，引入如下結(jié)構(gòu)特性：1.結(jié)構(gòu)活性2.完全可控性3.結(jié)構(gòu)有界性

[定義14-5]：Petri網(wǎng)N是結(jié)構(gòu)有界的，當(dāng)且僅當(dāng)存在一個(gè)m維正整數(shù)向量Y，使得CY≤0。表14-1線性不等式理論中的四種情況情況系統(tǒng)α系統(tǒng)β1（Minkowski-Farkas）CTX≥b，X無限制YTb＞02（Minkowski-Farkas）CTX≥b，X≥0CY=0，Y≥0，YTb＞03（Stiemke）CTX＞≠0，X無限制CY=0，Y＞04（Farkas）CTX＞≠0，X≥0CY≤0，Y＞02022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院614.守恒性[定義14-6]：Petri網(wǎng)是（部分）守恒的，當(dāng)且僅當(dāng)存在一個(gè)正的（非負(fù)）整數(shù)m維向量Y，滿足CY=0，Y≠0。5.重復(fù)性[定義14-7]：Petri網(wǎng)N是（部分）重復(fù)的，當(dāng)且僅當(dāng)存在一個(gè)正的（非負(fù)）整數(shù)n維向量X，使得CTX≥0，X≠02022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院626.一致性[定義14-8]：Petri網(wǎng)N是（部分）一致的，當(dāng)且僅當(dāng)存在一個(gè)正的（非負(fù)）整數(shù)n維向量X，便得CTX=0，X≠0。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院63表14-2某些結(jié)構(gòu)特性的必要和充分條件特性必要和充分條件結(jié)構(gòu)有界Y>0,Cy≤0(或X≥0，CTX＞≠0）守恒

Y＞0，Cy=0（或

X，CTX＞≠0）部分守恒Y＞≠0，CY=0重復(fù)X＞0，CTX≥0部分重復(fù)

X＞0，CTX=0（或

X＞≠0，CTX≥0一致Y，CY＞≠0）部分一致X＞≠0，CTX=02022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院64例14-10：用表14-2中的結(jié)論分析圖14-12至14-16所示五個(gè)網(wǎng)的結(jié)構(gòu)特性。2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院652022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院662022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院672022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院682022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院69表14-3用表14-2中結(jié)論對圖14-12至圖14-16的分析結(jié)果圖14-12圖14-13圖14-14圖14-15圖14-16結(jié)構(gòu)有界＋－－＋－守恒－－－－－部分守恒－－－－－重復(fù)－＋＋－－部分重復(fù)－＋＋－＋一致－－＋－－部分一致－－＋－－2022/11/3廣東工業(yè)大學(xué)計(jì)算機(jī)學(xué)院7014.3.7Petri網(wǎng)到程序結(jié)構(gòu)的轉(zhuǎn)換從Petri網(wǎng)的概念與分析方法可以知道，Petri網(wǎng)是用來描述和分析要開發(fā)系統(tǒng)模型的工具，不是計(jì)算機(jī)的實(shí)現(xiàn)應(yīng)用工具。另一方面，Petri網(wǎng)的結(jié)構(gòu)與軟件結(jié)構(gòu)的性質(zhì)也不同。其表現(xiàn)形式也不同。由此可以得出：通過分析，有了