Synthesis of Monitor-Based Liveness-Enforcing Supervisors for S³ PR With ξ -Resources

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 α-S3PR with i-resources. First, an algorithm is presented to reduce an S3PR via a i-resource. Based on the algorithm, i-resources in α-S3PRs are classified into two types: 1) A-ξ-resources and 2) B-ξ-resources. Next, for an α-S3PR with only B-ξ-resources, it is proved that a maximally permissive liveness-enforcing supervisor can be designed by controlling all emptied strict minimal siphons. For an α-S3PR 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 deadlock prevention algorithm for α-S3PRs is presented. Two FMS examples are used to illustrate its application. Its comparison results with other state-of-the-art deadlock prevention policies validate its overall advantages in terms of computational complexity, structural complexity, and behavior permissiveness.