Monitor-based liveness-enforcing petri net supervisors for flexible manufacturing systems

Deadlocks are a rather undesirable phenomenon in flexible manufacturing systems (FMSs). This work, by adding monitors, develops a deadlock prevention policy for FMSs that can be modeled by a class of Petri nets called α-S³PR with ξ-resources. First, an algorithm is given to reduce an S³PR via a ξ-resource. Based on it, ξ-resources in α-S³PRs are classified into A-ξ-resources and B-ξ-resources. Next, for an α-S³PR with only B-ξ-resources, it is proved that a maximally permissive liveness-enforcing supervisor can be designed by M-controlling all the emptied strict minimal siphons (SMSs). For an α-S³PR containing A-ξ-resources, a liveness-enforcing supervisor can be designed by iteratively reducing the net via A-ξ-resources and adding the corresponding monitors. Finally, a comprehensive deadlock prevention algorithm for α-S³PRs is presented. An FMS example is used to illustrate its application.