Liveness-enforcing supervisor for LS3PR with uncontrollable and unobservable transitions

This paper focuses on a subclass of Petri nets that appears in the modeling of a wide set of flexible manufacturing systems (FMS). A deadlock prevention policy is developed to design a liveness-enforcing supervisor for this kind of Petri nets with uncontrollable and unobservable transitions. Some special transitions are defined such that liveness-enforcing constraints are enforced directly through these transitions. The existence of a monitor that enforcing a constraint is also discussed. A sufficient condition and a necessary condition are proposed for uncontrollable transitions and unobservable transitions, respectively.