Synthesis of liveness enforcing supervisor for automated manufacturing systems using insufficiently marked siphons

A liveness enforcing supervisor synthesis technique is presented for Petri net modeling automated manufacturing systems. The insufficiently marked siphons are deployed to characterize the deadlock situations in an incidence matrix based way, which makes possible the study of the modeled systems from both structural and algebraic perspectives. The approach generates at each step a generalized mutual exclusion constraint which contains only markings for which liveness can be enforced. To avoid the explicit enumeration of all the set of strict minimal siphons, a set of mathematical programming formulations are established to implement the derivation of insufficiently marked siphons from the PT-transformation of the plant system. Further, a generalized elementary siphon control approach is involved such that the final supervisor can be structurally simplified. Several examples are used to illustrate these results.