Synthesis of Liveness-Enforcing Petri Net Supervisors Based on a Think-Globally-Act-Locally Approach and Vector Covering for Flexible Manufacturing Systems

This paper proposes the synthesis of Petri net supervisors based on a think-globally-act-locally (TGAL) approach and a vector covering technique for flexible manufacturing systems. Given a Petri net model with deadlocks, the TGAL approach first temporarily adds a global idle place (GP). A GP has initially only one token. Then, we generate the reachability graph of the net model with the GP. If there are deadlocks, we find all the legal markings and first-met bad markings (FBMs). The legal markings and FBMs that need to be considered can be reduced by using a vector covering approach. An integer linear programming problem is formulated to design a set of control places to forbid all FBMs but no legal markings. Meanwhile, the redundancy of the obtained control places is checked to remove the redundant ones. Then, we increase one token in the GP and compute a set of control place again. This process is carried out until the reachable markings of the Petri net model do not increase when the number of tokens in the GP is increased. As a result, we can find a set of control places to make the Petri net model live. Finally, some Petri net examples from the literature are used to demonstrate the proposed methods. It can be verified that the obtained supervisors can lead to more reachable markings, since the obtained control places are maximally permissive at each iteration.