On the Existence of a Maximally Permissive Liveness-enforcing Petri Net Supervisor for Flexible Manufacturing Systems

Behavior permissiveness is the most important criterion in evaluating the performance of a liveness-enforcing supervisor. For a class of Petri nets, S³PR, this paper explores a sufficient condition under which there exists a maximally permissive monitor-based liveness-enforcing Petri net supervisor. It can be computed in an iterative way. At each iteration, a siphon is derived by the MlP-based deadlock detection method and controlled with its control depth variable being unit. We conclude that, for any S³PR structure N, there exists an initial marking Mo such that a maximally permissive liveness- enforcing supervisor can be always found for (N, M₀). The results obtained in this research are fully based on elementary siphons that are developed in our previous work. A flexible manufacturing example is used to demonstrate the proposed methodology.