基于約束程序的Petri網(wǎng)可達問題的研究.pdf

1、Petri網(wǎng)是一種廣泛應(yīng)用于描述異步并發(fā)現(xiàn)象的圖形化建模和分析工具，Petri網(wǎng)的可達性判定問題是進行Petri網(wǎng)建模和分析的基礎(chǔ)。判定Petri網(wǎng)可達性的基本方法有可達樹、可達圖、狀態(tài)方程和不變量分析等，由于合爆炸問題的存在，使得這些基本Petri網(wǎng)的分析方法隨著問題規(guī)模的增大而超出目前計算機的運算能力，嚴(yán)重限制著Petri網(wǎng)建模機制在現(xiàn)實中的應(yīng)用。 本文采用邏輯抽象技術(shù)和約束程序的方法，主要對三種類型的可達問題進行的研究。即

2、： 問題l：給定Petri網(wǎng)∑=(P，T；F，W，m<,0>)和任一標(biāo)識m<,f>，判斷該標(biāo)識是否由初始標(biāo)識m<,n>可達。 問題2：給定Petri網(wǎng)∑=(P，T；F，W，m<,0>)和一組標(biāo)識，求這組標(biāo)識中的元素從初始標(biāo)識m<,n>可達的情況。 問題3：給定Petri網(wǎng)∑=(P，T；F，W，m<,0>)和任-T向量U，判斷是否有對應(yīng)T向量U的實際變遷序列由初始標(biāo)識m<,n>發(fā)生。即在對應(yīng)T向量U的實際變遷序列的

3、作用下標(biāo)識m<,f>=m<,n>+C.U是由初始標(biāo)識m<,n>可達。 針對以上3個問題，本文具體工作為： 首先，在分析邏輯抽象技術(shù)和序列深度參數(shù)算法的基礎(chǔ)上，引入最大步集、部分標(biāo)識的關(guān)鍵標(biāo)識、部分步關(guān)鍵變遷等概念，證明關(guān)鍵約束的可用、完整和正確性。豐富了基于約束程序的Petri網(wǎng)理論。其次，提出了解決問題1、問題2的基于關(guān)鍵約束理論的可達集及序列深度參數(shù)求解算法和可達判定算法。使得算法不但可以在并行度高、多Token或存

4、在家態(tài)情況下，使用更少約束和變量，避免搜索重復(fù)路徑與產(chǎn)生重復(fù)標(biāo)識；而且對有界。Petri網(wǎng)判定時，不需要指定K值，并可以一次對一組標(biāo)識完成可達判定。大大地提高了判定的效率和適用范圍。 最后，在分析變遷約束可達問題的各種求解辦法和缺陷的基礎(chǔ)上，提出了變遷約束可達問題的求解模型和判定算法。使用該約束模型的構(gòu)造的算法充分利用 T 向量提供的信息，對可達圖進行展望搜索，忽略了對不相關(guān)分支的搜索；在約束搜索策略的指導(dǎo)下，使得變量(解)快速