{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/113147"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/113147","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Algorithms for computing liveness enforcing supervisors for discrete event-driven systems modeled by petri nets","abstract":"\"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.\"","abstract_html":""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."","abstract_has_math":false,"creators":["Khaleghi, Roshanak"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Industrial Engineering","degree_department":null,"school":null,"contributors":["Sreenivas, Ramavarapu","Beck, Carolyn","Salapaka, Srinivasa","Stipanovic, Dusan"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2022,"date_issued":"2022-01-12T22:35:02Z","date_published":"2022-01-12T22:35:02Z","updated_at":"2026-07-22T22:24:53Z","subjects":["Discrete Event Dynamic Systems, Petri Nets, Right-Closed Sets, Liveness Enforcing Supervisory Policy, Control Invariance"],"languages":["en"],"rights":["Copyright 2021 Roshanak Khaleghi"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/113147","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Sreenivas, Ramavarapu","Beck, Carolyn","Salapaka, Srinivasa","Stipanovic, Dusan"]},{"key":"dc:creator","label":"Author","values":["Khaleghi, Roshanak"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2022-01-12T22:35:02Z","2024-01-12T22:35:30Z","2021-07-08","2021-08"]},{"key":"dc:type","label":"Dc Type","values":["text","Thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Industrial Engineering"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Discrete Event Dynamic Systems, Petri Nets, Right-Closed Sets, Liveness Enforcing Supervisory Policy, Control Invariance"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2021 Roshanak Khaleghi"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/113147"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["\"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.\"","Submission published under a 24 month embargo labeled 'U of I Access', the embargo will last until 2023-08-01","The student, Roshanak Khaleghi, accepted the attached license on 2021-07-06 at 22:37.","The student, Roshanak Khaleghi, submitted this Dissertation for approval on 2021-07-06 at 22:48.","This Dissertation was approved for publication on 2021-07-08 at 09:07.","DSpace SAF Submission Ingestion Package generated from Vireo submission #16776 on 2022-01-12 at 12:53:39","Made available in DSpace on 2022-01-12T22:35:02Z (GMT). No. of bitstreams: 2 KHALEGHI-DISSERTATION-2021.pdf: 13716742 bytes, checksum: b8ffc33aae460d9cccb0a1ae3f7113cd (MD5) LICENSE.txt: 4214 bytes, checksum: 91112710fc5bde0521a7bf55235703b2 (MD5) Previous issue date: 2021-07-08","Embargo set by: Seth Robbins for item 121073 Lift date: 2024-01-12T22:35:30Z Reason: Author requested U of Illinois access only (OA after 2yrs) in Vireo ETD system","Author requested U of Illinois access only (OA after 2yrs) in Vireo ETD system","U of I Only"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Algorithms for computing liveness enforcing supervisors for discrete event-driven systems modeled by petri nets"]}]}],"canonical_facts":{"dc:contributor":["Sreenivas, Ramavarapu","Beck, Carolyn","Salapaka, Srinivasa","Stipanovic, Dusan"],"dc:creator":["Khaleghi, Roshanak"],"dc:date":["2022-01-12T22:35:02Z","2024-01-12T22:35:30Z","2021-07-08","2021-08"],"dc:description":["\"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.\"","Submission published under a 24 month embargo labeled 'U of I Access', the embargo will last until 2023-08-01","The student, Roshanak Khaleghi, accepted the attached license on 2021-07-06 at 22:37.","The student, Roshanak Khaleghi, submitted this Dissertation for approval on 2021-07-06 at 22:48.","This Dissertation was approved for publication on 2021-07-08 at 09:07.","DSpace SAF Submission Ingestion Package generated from Vireo submission #16776 on 2022-01-12 at 12:53:39","Made available in DSpace on 2022-01-12T22:35:02Z (GMT). No. of bitstreams: 2 KHALEGHI-DISSERTATION-2021.pdf: 13716742 bytes, checksum: b8ffc33aae460d9cccb0a1ae3f7113cd (MD5) LICENSE.txt: 4214 bytes, checksum: 91112710fc5bde0521a7bf55235703b2 (MD5) Previous issue date: 2021-07-08","Embargo set by: Seth Robbins for item 121073 Lift date: 2024-01-12T22:35:30Z Reason: Author requested U of Illinois access only (OA after 2yrs) in Vireo ETD system","Author requested U of Illinois access only (OA after 2yrs) in Vireo ETD system","U of I Only"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/113147"],"dc:language":["en"],"dc:rights":["Copyright 2021 Roshanak Khaleghi"],"dc:subject":["Discrete Event Dynamic Systems, Petri Nets, Right-Closed Sets, Liveness Enforcing Supervisory Policy, Control Invariance"],"dc:title":["Algorithms for computing liveness enforcing supervisors for discrete event-driven systems modeled by petri nets"],"dc:type":["text","Thesis"],"thesis:degree_discipline":["Industrial Engineering"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:53Z"}