Most permissive liveness-enforcing Petri net supervisors for flexible manufacturing systems

This paper presents a deadlock prevention approach to find a maximally permissive liveness-enforcing pure Petri net supervisor, expressed by a set of monitors, for a flexible manufacturing system (FMS), if such a supervisor exists. Otherwise, it derives the most permissive one in the sense that there are no other Petri net supervisors that are more permissive than it. The proposed approach computes the reachability graph of a plant model only once. By using a vector covering approach, the sets of legal markings and first-met bad markings (FBMs) are reduced to two smaller ones, namely the minimal covering set of legal markings and the minimal covered set of FBMs. At each iteration, an FBM is selected. By solving an integer linear programming problem (ILPP), a place invariant (PI) is designed to prevent the FBM from being reached while no marking in the minimal covering set of legal markings is forbidden. If the ILPP has no solution, implying that there is no maximally permissive Petri net supervisor for the plant net model, another ILPP is designed to remove the least number of legal markings whose reachability conditions contradict others. Then, a PI is redesigned to ensure that the remaining legal markings are reachable. This process is carried out until no FBM can be reached. Finally, a most permissive liveness-enforcing supervisor is obtained. FMS examples are presented to illustrate the proposed approaches.