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.