Siphon-Based Divide-and-Conquer Policy for Enforcing Liveness on Petri Net Models of FMS Suffering from Deadlocks or Livelocks

A novel siphon-based divide-and-conquer (SbDaC) policy is presented in this paper for the synthesis of Petri net (PN) based liveness-enforcing supervisors (LES) for flexible manufacturing systems (FMS) prone to deadlocks or livelocks. The proposed method takes an uncontrolled and bounded PN model (UPNM) of the FMS. Firstly, the reduced PNM (RPNM) is obtained from the UPNM by using PN reduction rules to reduce the computation burden. Then, the set of strict minimal siphons (SMSs) of the RPNM is computed. Next, the complementary set of SMSs is computed from the set of SMSs. By the union of these two sets, the superset of SMSs is computed. Finally, the set of subnets of the RPNM is obtained by applying the PN reduction rules to the superset of SMSs. All these subnets suffer from deadlocks. These subnets are then ordered from the smallest one to the largest one based on a criterion. To enforce liveness on these subnets, a set of control places (CPs) is computed starting from the smallest subnet to the largest one. Once all subnets are live, this process provides the LES, consisting of a set of CPs to be used for the UPNM. The live controlled PN model (CPNM) is constructed by merging the LES with the UPNM. The SbDaC policy is applicable to all classes of PNs related to FMS prone to deadlocks or livelocks. Several FMS examples are considered from the literature to highlight the applicability of the SbDaC policy. In particular, three examples are utilized to emphasize the importance, applicability and effectiveness of the SbDaC policy to realistic FMS with very large state spaces.