A Software Tool for Live-Lock Avoidance in Systems Modelled Using a Class of Petri NETS

If a manufacturing system enters into a state where a task enters into a state of suspended animation for perpetuity, we say it is in a livelocked state.In contrast, all tasks of the system remain suspended for perpetuity in a deadlocked state of the system.A livelock-free manufacturing system can never experience deadlocks, but the converse is not necessarily true.A livelock-prone manufacturing system can be regulated using a supervisory policy such that the resulting supervised system is livelock-free.If a liveness enforcing supervisory policy (LESP) prevents the occurrence of an event at given state of the manufacturing system, and every other LESP, irrespective of the implementation paradigm, prescribes the same control for that state, we say the original LESP is minimally restrictive.This paper is about two enhancements to an existing software tool that synthesizes the minimally restrictive LESP for a manufacturing system modelled using a class of weighted Petri nets (PNs).The first enhancement is about broadening the scope of the software tool to a larger class of PNs.The second enhancement is about improving the running time of the software tool using a property identified in this paper.We identify a class, ℋ, of general Petri net (PN) structures where the existence of a liveness enforcing supervisory policy (LESP) for an instance of this class, initialized at a marking, is sufficient to infer the existence of an LESP when the same instance is initialized at a larger marking.As a consequence, the existence of an LESP for the PN that results when a member of this class is initialized with a marking, is decidable.Additionally, the maximally permissive LESP, when it exists, can be synthesized using a software tool described in an earlier paper.We also highlight a property that plays a critical role in the speed of convergence of the iterative procedure for the synthesis of the minimally restrictive LESP, when it exits, for any instance of ℋ that uses the aforementioned software package.