Solving the reachability problem of a class of Petri nets

We present a theorem on the reachability of a class of Petri nets, called process nets with resources (PNRs), which model shared-resource automated manufacturing systems based on the concept of separately specifying operation and resource requirements. It is shown that the 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. Since it has been proven that the liveness is also tied to whether minimal siphons are unmarked, liveness of PNRs can be obtained by checking the reachability of PNRs.