This paper presents a new class of Petri nets, called process nets with resources (PNRs), for modeling manufacturing systems where only parts can interact with resources, and resources alone cannot interact with one another. PNRs properly include S/sup 3/PR, augmented marked graphs, and some subclasses of resource control net (RCN) merged nets and ERCN merged nets. As a result, PNRs can model far more complex manufacturing process flows and resource sharing than these nets. To construct a PNR, we first build a process net to specify the process flow for each part type. A process net is a consistent, conservative, strongly connected, and live Petri net that satisfies three conditions, including strong reversibility. Then resource places denoting the availability of resource types are added to the process nets. We generalize strong reversibility for PNRs in order to check a sufficient condition for reversibility of PNRs. It is shown that strong reversibility and reversibility of a PNR depends on the siphons. Liveness of a PNR can be verified by checking the potential firing ability of all transitions of each isolated process net, which is, informally speaking, a process net with all resources allocated to it. A manufacturing example is given to show the applicability of PNRs.

An augmented reachability tree (ART) is proposed to extend the capability of the classical reachability tree (RT) for analyzing qualitative properties, such as liveness, of a class of unbounded generalized Petri nets, called 1-place-unbounded nets, where there is at most one unbounded place for each net. The idea is based on the computation of the minimal marking of each node in the tree. An algorithm for obtaining the minimal marking is shown. Examples are given to illustrate the technique. In addition to liveness, the proposed method can verify other properties such as reversibility and feasible firing sequences. Furthermore, properties verifiable by RT are also verifiable by ART.