Modular synthesis of Petri nets for modeling flexible manufacturing systems

This paper proposes a modular Petri net synthesis method for modeling flexible manufacturing systems based on synchronization among control processes of the manufacturing resources (such as robots and machines). In the method, the target system is modeled in a bottom-up and uniform manner by first describing the system's control processes using strongly connected state machines (SCSMs) as the basic modules. Each SCSM may contain multiple tokens to represent resources from the same type such as spaces in a buffer. Next, the common transitions and common transition subnets of the modules are merged to represent their synchronization. The system model constructed is proven to be conservative and thus bounded. Moreover, a restricted class of merged nets is proven to be live and reversible. For general classes of merged nets, this paper shows theorems that easily calculateP-invariants of the final net without solving the linear system equations. TheseP-invariants can be used to help in verifying the model's qualitative properties such as liveness.