On supervisory policies that enforce liveness in controlled Petri nets that are similar

In this paper we consider event-driven systems, modeled by Petri nets (PNs) that are prone to livelocks when left unsupervised. There are well-known conditions for the existence of supervisory policies that can regulate the sequence of task-executions in such a manner that there are no livelocks in the supervised system. We consider the problem of modifying a supervisory policy that ensures livelock-freedom for a given event-driven system into a similar policy for another event-driven system. The formal concept of simulation was introduced in the Petri net (PN) literature to capture the notion of 'similarity' among PNs. In this paper we generalize this concept to controlled PNs. The set of transitions in a controlled PN are partitioned into controllable- and uncontrollable-subsets. The supervisory policy determines which of a subset of controllable transitions are permitted to fire at any marking of the PN. A transition in a controlled PN can fire if and only if (1) there are sufficient tokens in its input places, and (2) the supervisory policy permits it to fire. A transition in a supervised PN is live if it can be fired, not necessarily immediately, from every marking that is reachable under supervision. The synthesis of a liveness enforcing supervisory policy (LESP) for a subset of transitions in a PN serves as the motivating problem for this work. We consider two PNs that in a simulation relationship under supervision, and we derive a necessary and sufficient condition for the existence of a LESP for a subset of transitions in these PNs. Using an illustrative example, we show how this observation can be used to synthesize LESPs in a PN that simulates another PN. Further investigations into formalizing this synthesis procedure is suggested as a future research topic.