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

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

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

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

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