Designing supervisory policies that avoid livelocks in Manufacturing- and service-systems modeled using general Petri Nets: A tutorial using an illustrative example

When a Manufacturing- or Service-System gets into a deadlocked state none of the activities can proceed towards completion. When the same system is in a livelocked state, some activity of the system enters a state of suspended animation and is never completed, while other activities proceed to completion without hindrance. A livelock-free system does not experience deadlocks; but a deadlock-free system can experience livelocks. This tutorial is about the synthesis of livelock avoidance policies for Manufacturing- and Service-Systems that are modeled by Petri Nets (PNs). After characterizing livelock-freedom, we introduce the paradigm of liveness enforcing supervisory policies (LESPs). An LESP is said to be minimally restrictive, if the fact that it prevents the occurrence of an event at a given state is reason enough to infer that all livelock-avoidance policies would do the same. If there is an LESP for a system, there is a unique minimally restrictive LESP. We restrict attention to LESPs that can be implemented using a Disjunctive Normal Form (DNF) expression on the state of the PN modeling the system. We describe the process of synthesizing the minimally restrictive LESPs using an illustrative example using a software-product developed by the authors.