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 {Θ_tc(N)_tc∈Tc, where T_c is the set of controllable transitions in the PN. The literals in Θ_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.