IEEE Transactions on Automatic Control, Vol.60, No.10, 2825-2830, 2015
On Invariant-Based Monitors That Enforce Liveness in a Class of Partially Controlled General Petri Nets
We consider a class of Petri Net structures where the existence of a liveness enforcing supervisory policy (LESP) for an initialmarking implies there is a LESP for a larger initial marking. That is, the set of initial markings for which there is a LESP for any instance of this class is right-closed. If a transition is prevented from firing at a marking by a LESP, and all LESPs, irrespective of the implementation-paradigm that is chosen, prescribe the same control for the marking, then it is a minimally restrictive LESP. It is possible to synthesize the minimally restrictive LESP for any instance of this class that uses this right-closed set of markings. Alternately, one could consider invariant-based monitors for liveness enforcement in an instance of this class. If and when they exist, invariant-based monitors that enforce liveness are not minimally restrictive, in general. In this technical note, we derive a necessary and sufficient condition for the existence of a minimally restrictive, invariant-based monitor for the class of PNs introduced above.