Most permissive liveness-enforcing Petri net supervisors for discrete event systems via linear monitors

This paper proposes a deadlock prevention method to design a maximally permissive liveness-enforcing pure Petri net supervisor for a discrete event system, if such a supervisor exists; otherwise, it obtains the most permissive one in the sense that no other pure liveness-enforcing supervisors via linear monitors can be more permissive than it. This paper exploits an iterative method. At each iteration, a first-met bad marking (FBM) is singled out and an integer linear programming problem (ILPP) is configured. If a feasible solution can be found for the ILPP, then a place invariant (PI) is designed to prohibit the FBM from being reached while no legal marking is forbidden. If the ILPP has no solution, we collect all these FBMs that cannot be optimally controlled. For each of such FBMs, another ILPP is designed to find the least number of legal markings whose reachability conditions contradict the current considered FBM and enumerate all the optimal solutions of this ILPP. Based on it, we develop a 0-1 linear programming problem to find the maximal number of legal markings after removing all the contradictory legal markings. Then, the new sets of legal markings and FBMs are obtained, and we return to the iteration stage to redesign a PI to control each FBM if the ILPP has a feasible solution. Repeat the above process until no FBM can be reached. Finally, a most permissive pure liveness-enforcing supervisor via linear monitors is derived. Two Petri net models are used to illustrate the proposed method.