Synthesis rules for colored Petri nets and their applications to automated manufacturing systems

Synthesis methods for colored Petri nets are presented. The final net constructed by these methods always guarantees liveness and boundedness. The methods are the extended version of the authors´ previous transformation methods for generalized Petri nets (1990, 1991). Some restrictions for incidence functions and color sets are given to apply the previous theorems to colored Petri nets. Using these restrictions, and defining a live-and-bounded circuit (LB-circuit) for colored Petri nets, it is shown that the union of two LB-circuits is live and bounded if the two LB-circuits are fused along two types of common directed paths. Then, a method is presented for synthesis of a new live and bounded net by fusing an LB-circuit to a live and bounded net while preserving the properties. Using this bottom-up approach a complex colored Petri net can be constructed. These synthesis methods are illustrated for modeling automated manufacturing systems by means by two examples