Algorithms for computing liveness enforcing supervisors for discrete event-driven systems modeled by petri nets

The dynamics of Discrete-Event/Discrete-State (DEDS) Systems are due to an event-driven mechanism where occurrence of events at discrete points in time results in a change in the (discrete) state of the system. The behavior of DEDS systems can be controlled by means of a supervisory policy, which prevents the occurrence of events at a given state of the supervised system, when deemed appropriate. A supervisory policy is said to enforce a safety property, if it ensures that nothing "bad" ever occurs in the supervised DEDS system. A policy that ensures something "good" eventually occurs, is said to enforce a liveness property. In this thesis, we focus on the synthesis of Liveness Enforcing Supervisory Policies (LESPs) that ensures DEDS system never gets into a livelock. A DEDS system is said to be deadlocked (resp. livelocked) if all (resp. some) events of the system can never be completed. A system that is livelock-free is also deadlock-free, but the converse is not necessarily true. To model DEDS systems, we use Petri Net (PN) structures in which states of the system translate into the markings of the PN, and the events of the system are represented by transitions whose firing changes the marking of the PN. The existence of an LESP for an arbitrary PN structure is not decidable. For any PN structure, an LESP can be effectively represented by a set of initial markings for which an LESP exists. We restrict our attention to certain classes of PN structures for which the aforementioned set is known to be right-closed. A set of non-negative integral vectors is said to be right-closed if the presence of a vector in the set implies all term-wise larger vectors also belong to the set. We address two problems in LESP synthesis of DEDS systems modeled by PNs. The first problem is motivated by the fact that not all events of a DEDS system can be prevented by a supervisor. The set of events of the DEDS system is partitioned into the set of controllable (resp. uncontrollable) events. The controllable (resp. uncontrollable) events can (resp. cannot) be prevented from occurring by the supervisor. Thus, the target right-closed set of markings which enforces the liveness property needs to be control invariant with respect to the PN structure in that the occurrence of any uncontrollable event at any state cannot result in a state that is outside the target right-closed set. Equivalently, a set of markings is control invariant with respect to a PN structure if the firing of any uncontrollable transition at any marking in this set results in a new marking that is also in the set. Every right-closed set of markings has a unique supremal control invariant subset, which is the largest subset that is control invariant with respect to the PN structure. The supremal control invariant subset of a right-closed set of markings is not necessarily right-closed. However, this supremal control invariant subset has a unique supremal right-closed control invariant subset (i.e. the "largest" right-closed control invariant subset). As a preliminary key step in the synthesis of LESPs for certain classes of PN structures, we present a formal algorithm that computes the supremal right-closed control invariant subset of a right-closed of markings with respect to an arbitrary PN structure. The supremal property of the proposed algorithm is necessary to identify the minimally restrictive LESP for a given PN. If an event is prevented by a minimally restrictive LESP, no other LESP would allow that event to occur. The second problem discussed in this thesis is a learning-based framework for LESP synthesis for certain classes of PN structures. In this paradigm, initially the DEDS system is supervised by a policy that is not necessarily an LESP. If the supervised-system experiences a deadlock, the learning framework updates supervisory policy to ensure that the deadlock state is avoided in future. The state of the supervised DEDS system is reset to an appropriate initial state, and the supervision is continued under the newly updated policy, Essentially, this procedure systematically improves the current estimate of the target right-closed set of markings which enforces the liveness property for the given PN structure. In fact, the so-called `learning' approach for LESP synthesis provides an alternative to an Integer Linear Programming (ILP)-based approach that is applied on the coverability graph of a PN. As the size of the PN grows, the computational complexity of such ILP-based approaches to LESP-synthesis increases. The main motivation behind our exploration of the proposed learning framework was to circumvent the dependency of LESP synthesis procedures on ILPs and thus, mitigate the computational burden of finding liveness enforcing supervisors for complex PN structures.U of I OnlyAuthor requested U of Illinois access only (OA after 2yrs) in Vireo ETD syste