A Study of Property Analysis in Petri Nets

• Main Authors: Peng, Mao-Yu, 彭茂裕
• Other Authors: Jeng Mu-Der
• Format: Others
• Language: zh-TW
• Published: 1997
• Online Access: http://ndltd.ncl.edu.tw/handle/48927193171576022077

碩士 === 國立海洋大學 === 電機工程學系 === 85 === This thesis is divided into three parts: an augmented reachability tree (ART), a new algorithm for finding minimal siphons and traps, and a class of nets, called process nets with resources (PNRs). An augmented reachability tree (ART) extends the ability of the classical reachability tree for solving the liveness problem of a class of Petri nets where there exists at most one unbounded place. The idea is based on the computation of the minimal token number of the unbounded place. An algorithm for obtaining the minimal token number is shown. The proposed method can also be used to solve the shortest path problem in graphs with negative costs. Classical theorems that adopt siphons and traps to verify reachability and liveness of Petri nets are shown to be only tied to minimal siphons and traps. A new algorithm for finding minimal siphons and traps has been presented using two proposed theorems that enhances the efficiency of the algorithm. A class of nets, called process nets with resources (PNRs), models shared-resource automated manufacturing systems based on the concept of separately specifying operation and resource requirements. A PNR is built from a live net that is an acyclic net after removing so called process idle places, and a set of places called resource idle places modeling the availability of system resources. It is shown that the liveness, reversibility and reachability of a PNR only depends on whether all minimal siphons are marked. An algorithms is presented to show how the state equation is used to examine the reachability with a restriction. Liveness of PNRs can be obtained by checking the reachability of PNRs.