{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/89010"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/89010","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"On computing a liveness enforcing supervisory policy for a class of general petri nets","abstract":"\"Discrete-Event/Discrete-State (DEDS) Systems are prone to livelocks. Once a system enters a livelocked-state, there is at least one activity of the modeled system that cannot be executed from all subsequent states of the system. This phenomenon is common to many operating systems where some process enters into a state of suspended animation for perpetuity, and the user is left with no other option than to terminate the process, or reboot the machine. This thesis is about computing Liveness Enforcing Supervisory Policies (LESPs) for Petri net (PN) models of DEDS systems. The existence of an LESP for general PNs is not even semi-decidable. This thesis identifies two classes of PNs F and H for which the existence of a LESP is decidable. It also describes an object-oriented implementation of a procedure for the synthesis of the minimally-restrictive LESP for any instance from these classes. The minimally-restrictive LESP prevents the occurrence of events in a DEDS system only when it is absolutely necessary. A suite of methods, based on refinement/abstraction concepts, is developed to reduce the complexity of LESP-synthesis. This involves the synthesis of a LESP for a simplified-version of a complex PN structure, which is subsequently refined to serve as a LESP for the original complex PN. Two PNs are in a simulation relationship if their behaviors are \"\"similar\"\" in a formal sense. The thesis concludes with a result that shows that the above mentioned procedure can be generalized to PNs in simulation relationships. That is, a LESP for a PN can be modified to serve as a LESP for another PN that is \"\"similar\"\". The implementation of this theoretical observation is suggested as a topic for future work.\"","abstract_html":""Discrete-Event/Discrete-State (DEDS) Systems are prone to livelocks. Once a system enters a livelocked-state, there is at least one activity of the modeled system that cannot be executed from all subsequent states of the system. This phenomenon is common to many operating systems where some process enters into a state of suspended animation for perpetuity, and the user is left with no other option than to terminate the process, or reboot the machine. This thesis is about computing Liveness Enforcing Supervisory Policies (LESPs) for Petri net (PN) models of DEDS systems. The existence of an LESP for general PNs is not even semi-decidable. This thesis identifies two classes of PNs F and H for which the existence of a LESP is decidable. It also describes an object-oriented implementation of a procedure for the synthesis of the minimally-restrictive LESP for any instance from these classes. The minimally-restrictive LESP prevents the occurrence of events in a DEDS system only when it is absolutely necessary. A suite of methods, based on refinement/abstraction concepts, is developed to reduce the complexity of LESP-synthesis. This involves the synthesis of a LESP for a simplified-version of a complex PN structure, which is subsequently refined to serve as a LESP for the original complex PN. Two PNs are in a simulation relationship if their behaviors are ""similar"" in a formal sense. The thesis concludes with a result that shows that the above mentioned procedure can be generalized to PNs in simulation relationships. That is, a LESP for a PN can be modified to serve as a LESP for another PN that is ""similar"". The implementation of this theoretical observation is suggested as a topic for future work."","abstract_has_math":false,"creators":["Somnath, Nisha"],"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","Stipanovic, Dusan","Voulgaris, Petros"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2016,"date_issued":"2016-03-02T19:33:54Z","date_published":"2016-03-02T19:33:54Z","updated_at":"2026-07-22T22:26:32Z","subjects":["Petri Nets","Supervisory control","Discrete event systems"],"languages":["en"],"rights":["Copyright 2015 Nisha Somnath"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/89010","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Sreenivas, Ramavarapu","Beck, Carolyn","Stipanovic, Dusan","Voulgaris, Petros"]},{"key":"dc:creator","label":"Author","values":["Somnath, Nisha"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2016-03-02T19:33:54Z","2015-12-01","2015-12"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"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":["Petri Nets","Supervisory control","Discrete event systems"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2015 Nisha Somnath"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/89010"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["\"Discrete-Event/Discrete-State (DEDS) Systems are prone to livelocks. Once a system enters a livelocked-state, there is at least one activity of the modeled system that cannot be executed from all subsequent states of the system. This phenomenon is common to many operating systems where some process enters into a state of suspended animation for perpetuity, and the user is left with no other option than to terminate the process, or reboot the machine. This thesis is about computing Liveness Enforcing Supervisory Policies (LESPs) for Petri net (PN) models of DEDS systems. The existence of an LESP for general PNs is not even semi-decidable. This thesis identifies two classes of PNs F and H for which the existence of a LESP is decidable. It also describes an object-oriented implementation of a procedure for the synthesis of the minimally-restrictive LESP for any instance from these classes. The minimally-restrictive LESP prevents the occurrence of events in a DEDS system only when it is absolutely necessary. A suite of methods, based on refinement/abstraction concepts, is developed to reduce the complexity of LESP-synthesis. This involves the synthesis of a LESP for a simplified-version of a complex PN structure, which is subsequently refined to serve as a LESP for the original complex PN. Two PNs are in a simulation relationship if their behaviors are \"\"similar\"\" in a formal sense. The thesis concludes with a result that shows that the above mentioned procedure can be generalized to PNs in simulation relationships. That is, a LESP for a PN can be modified to serve as a LESP for another PN that is \"\"similar\"\". The implementation of this theoretical observation is suggested as a topic for future work.\"","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2016-03-02 without embargo terms","The student, Nisha Somnath, accepted the attached license on 2015-11-24 at 20:26.","The student, Nisha Somnath, submitted this Dissertation for approval on 2015-11-24 at 20:27.","This Dissertation was approved for publication on 2015-12-01 at 08:03.","DSpace SAF Submission Ingestion Package generated from Vireo submission #8843 on 2016-03-02 at 12:50:29","Made available in DSpace on 2016-03-02T19:33:54Z (GMT). No. of bitstreams: 2 SOMNATH-DISSERTATION-2015.pdf: 2217931 bytes, checksum: 1b989a7a2285e8da85839dba7bafb8bc (MD5) LICENSE.txt: 4210 bytes, checksum: 2e713e45bef1b035c63cdf4c1c76db65 (MD5) Previous issue date: 2015-12-01"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["On computing a liveness enforcing supervisory policy for a class of general petri nets"]}]}],"canonical_facts":{"dc:contributor":["Sreenivas, Ramavarapu","Beck, Carolyn","Stipanovic, Dusan","Voulgaris, Petros"],"dc:creator":["Somnath, Nisha"],"dc:date":["2016-03-02T19:33:54Z","2015-12-01","2015-12"],"dc:description":["\"Discrete-Event/Discrete-State (DEDS) Systems are prone to livelocks. Once a system enters a livelocked-state, there is at least one activity of the modeled system that cannot be executed from all subsequent states of the system. This phenomenon is common to many operating systems where some process enters into a state of suspended animation for perpetuity, and the user is left with no other option than to terminate the process, or reboot the machine. This thesis is about computing Liveness Enforcing Supervisory Policies (LESPs) for Petri net (PN) models of DEDS systems. The existence of an LESP for general PNs is not even semi-decidable. This thesis identifies two classes of PNs F and H for which the existence of a LESP is decidable. It also describes an object-oriented implementation of a procedure for the synthesis of the minimally-restrictive LESP for any instance from these classes. The minimally-restrictive LESP prevents the occurrence of events in a DEDS system only when it is absolutely necessary. A suite of methods, based on refinement/abstraction concepts, is developed to reduce the complexity of LESP-synthesis. This involves the synthesis of a LESP for a simplified-version of a complex PN structure, which is subsequently refined to serve as a LESP for the original complex PN. Two PNs are in a simulation relationship if their behaviors are \"\"similar\"\" in a formal sense. The thesis concludes with a result that shows that the above mentioned procedure can be generalized to PNs in simulation relationships. That is, a LESP for a PN can be modified to serve as a LESP for another PN that is \"\"similar\"\". The implementation of this theoretical observation is suggested as a topic for future work.\"","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2016-03-02 without embargo terms","The student, Nisha Somnath, accepted the attached license on 2015-11-24 at 20:26.","The student, Nisha Somnath, submitted this Dissertation for approval on 2015-11-24 at 20:27.","This Dissertation was approved for publication on 2015-12-01 at 08:03.","DSpace SAF Submission Ingestion Package generated from Vireo submission #8843 on 2016-03-02 at 12:50:29","Made available in DSpace on 2016-03-02T19:33:54Z (GMT). No. of bitstreams: 2 SOMNATH-DISSERTATION-2015.pdf: 2217931 bytes, checksum: 1b989a7a2285e8da85839dba7bafb8bc (MD5) LICENSE.txt: 4210 bytes, checksum: 2e713e45bef1b035c63cdf4c1c76db65 (MD5) Previous issue date: 2015-12-01"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/89010"],"dc:language":["en"],"dc:rights":["Copyright 2015 Nisha Somnath"],"dc:subject":["Petri Nets","Supervisory control","Discrete event systems"],"dc:title":["On computing a liveness enforcing supervisory policy for a class of general petri nets"],"dc:type":["text"],"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:26:32Z"}