Petri nets liveness analysis by minimal siphons

In this paper, we presents a class of nets, called process nets with resources (PNRs), which model shared-resource automated manufacturing systems based on the concept of separately specifying the 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 for modeling the availability of system resources. It is shown that the liveness and reversibility of a PNR only depends on whether all minimal siphons are marked.