一種精準有限可達樹及其在無界Petri網(wǎng)屬性分析上的應用.pdf

1、Petri網(wǎng)具有嚴格的數(shù)學基礎和直觀的圖形化表示，一直是離散事件系統(tǒng)建模分析、控制與仿真的主要工具之一。然而，Petri網(wǎng)的理論方法中的無界網(wǎng)可達性分析問題一直是困擾著各國學者的世界性難點問題。針對這一問題，本文提出了一種精準有限可達樹(Exact Finite Reachability Tree，EFRT)，并用于可達性分析理論方法的研究。具體工作與成果如下:
　　(1)首次深入分析了無界網(wǎng)無界庫所的產(chǎn)生機理與根源，以及狀態(tài)可達

2、性的本質，給出了無界庫所判定的一個充分非必要條件，突破了人們對無界網(wǎng)可達性問題的認識局限。
　　(2)提出了一種全新的EFRT，結合新提出的“充分使能”條件確保了該樹對廣義無界網(wǎng)可達狀態(tài)的完全表征。EFRT的ω節(jié)點只能作為葉節(jié)點存在且不再生長，每個這樣的標識只包含一個ω量，突破了現(xiàn)有的有限可達樹的ω節(jié)點參與生長且標識表達式復雜等局限。同時，EFRT允許ω節(jié)點以最小普通標識來繼續(xù)展開，這為后續(xù)的基于樹搜索的增量式可達性分析打開了方便

3、之門。
　　(3)基于EFRT建立了無界網(wǎng)可達性分析理論方法，給出了包括可達性、有界性、安全性、死鎖、活性、可逆性等屬性的分析理論與算法，對所有理論結論都進行了嚴格證明。突破了現(xiàn)有的可達性理論多集中于死鎖分析的現(xiàn)狀。
　　(4)依據(jù)上述的理論結果和算法，設計開發(fā)了基于EFRT的無界Petri網(wǎng)屬性分析軟件，實現(xiàn)了EFRT的生成，以及有界性、安全性、死鎖、活性、可逆性等屬性的分析。最后用實例驗證了本文提出的理論和方法。