IEEE Transactions on Automatic Control, Vol.60, No.7, 1915-1920, 2015
On a Sufficient Information Structure for Supervisory Policies That Enforce Liveness in a Class of General Petri Nets
A Petri net (PN) is said to be live if it is possible to fire any transition, although not immediately, from every reachable marking. A liveness enforcing supervisory policy (LESP) determines which controllable transition is to be prevented from firing at a marking, to ensure the supervised Petri net (PN) is live. In this paper, we restrict our attention to a class of general Petri nets (PN) structures, where the existence of an LESP for an instance initialized at a marking, implies the existence of an LESP when the same instance is initialized with a termwise-larger initial marking. We show that the minimally restrictive LESP for an instance N from this class is characterized by a collection of boolean formulae {Theta(tc)(N)}(tc is an element of Tc), where T-c is the set of controllable transitions in the PN. The literals in Theta(tc)(N) are true if and only if the token-load of specific places meet a threshold. Consequently, appropriately placed threshold-sensors, which detect if the token-load of a place is greater than or equal to a predetermined threshold, provide sufficient information to implement the minimally restrictive LESP. The paper concludes with some directions for future research.
Keywords:Petri nets;supervisory control