An Improved Method Of Liveness-enforcing Petri Net Supervisors Based On The Theory Of Regions

Deadlocks are a very important problem that must be considred for designing and controlling flexible manufacturing systems (FMS). Many researchers use Petri net as a formalism to deal with deadlock problems in FMS. As a deadlock prevention approach based on the reachability graph (RG), the theory of regions obtains a liveness-enforcing supervisor for each marking/transition separation instances (MTSI) via solving a linear programming problem (LPP). The most advantage of the approach is that an optimal supervisor can be definitely obtained if such a supervisor exists. However, it still suffers from computational complexity problem since the number of LPP to be solved increases exponentially with respect to the size of a net model.This paper proposes a deadlock prenention policy for FMS based on a vector covering approach and the theory of regions. First of all, we reduce the number of MTSI by the fact that different MTSI have the same separation condition if they lead to the same first-met bad marking (FBM). Using a vector covering approach, we identify a minimal covered set of the MTSI. Then, only the MTSI in the minimal covered set of the MTSI are considered to obtain a maximally permissive liveness-enforcing Petri net supervisor, which can greatly reduce the number of LPP to be solved. Finally, a redundancy verification method is used to remove the redundant control places. Therefore, the proposed method can obtain a maximally permissive liveness-enforcing Petri net supervisor that has no redundant control places.