{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/108444"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/108444","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"On the decidability of problems in liveness of controlled Discrete Event Systems modeled by Petri Nets","abstract":"\"A Discrete Event System (DES) is a discrete-state system, where the state changes at discrete-time instants due to the occurrence of events. Informally, a liveness property stipulates that a 'good thing' happens during the evolution of a system. Some examples of liveness properties include starvation freedom -- where the 'good thing' is the process making progress; termination -- in which the good thing is for an evolution to not run forever; and guaranteed service -- such as in resource allocation systems, when every request for resource is satisfied eventually. In this thesis, we consider supervisory policies for DESs that, when they exist, enforce a liveness property by appropriately disabling a subset of preventable events at certain states in the evolution of DES. One of the main contributions of this thesis is the development of a system-theoretic framework for the analysis of Liveness Enforcing Supervisory Policies (LESPs) for DESs. We model uncertainties in the forward- and feedback-path, and present necessary and sufficient conditions for the existence of Liveness Enforcing Supervisory Policies (LESPs) for a general model of DESs in this framework. The existence of an LESP reduces to the membership of the initial state to an appropriately defined set. The membership problem is undecidable. For characterizing decidable instances of this membership problem, we consider a modeling paradigm of DESs known as Petri Nets, which have applications in modeling concurrent systems, software design, manufacturing systems, etc. Petri Net (PN) models are inherently monotonic in the sense that if a transition (which loosely represents an event of the DES) can fire from a marking (a non-negative integer-valued vector that represents the state of the DES being modeled), then it can also fire from any larger marking. The monotonicity creates a possibility of representing an infinite-state system using what can be called a \"\"finite basis\"\" that can lead to decidability. However, we prove that several problems of our interest are still undecidable for arbitrary PN models. That is, informally, a general PN model is still too powerful for the analysis that we are interested in. Much of the thesis is devoted to the characterization of decidable instances of the existence of LESPs for arbitrary PN models within the system-theoretic framework introduced in the thesis. The philosophical implication of the results in this thesis is the existence of what can be called a \"\"finite basis\"\" of an infinite state system under supervision, on which the membership tests can be performed in finite time; hence resulting in the decidability of problems and finite-time termination of algorithms. The thesis discusses various scenarios where such a finite basis exists and how to find them.\"","abstract_html":""A Discrete Event System (DES) is a discrete-state system, where the state changes at discrete-time instants due to the occurrence of events. Informally, a liveness property stipulates that a 'good thing' happens during the evolution of a system. Some examples of liveness properties include starvation freedom -- where the 'good thing' is the process making progress; termination -- in which the good thing is for an evolution to not run forever; and guaranteed service -- such as in resource allocation systems, when every request for resource is satisfied eventually. In this thesis, we consider supervisory policies for DESs that, when they exist, enforce a liveness property by appropriately disabling a subset of preventable events at certain states in the evolution of DES. One of the main contributions of this thesis is the development of a system-theoretic framework for the analysis of Liveness Enforcing Supervisory Policies (LESPs) for DESs. We model uncertainties in the forward- and feedback-path, and present necessary and sufficient conditions for the existence of Liveness Enforcing Supervisory Policies (LESPs) for a general model of DESs in this framework. The existence of an LESP reduces to the membership of the initial state to an appropriately defined set. The membership problem is undecidable. For characterizing decidable instances of this membership problem, we consider a modeling paradigm of DESs known as Petri Nets, which have applications in modeling concurrent systems, software design, manufacturing systems, etc. Petri Net (PN) models are inherently monotonic in the sense that if a transition (which loosely represents an event of the DES) can fire from a marking (a non-negative integer-valued vector that represents the state of the DES being modeled), then it can also fire from any larger marking. The monotonicity creates a possibility of representing an infinite-state system using what can be called a ""finite basis"" that can lead to decidability. However, we prove that several problems of our interest are still undecidable for arbitrary PN models. That is, informally, a general PN model is still too powerful for the analysis that we are interested in. Much of the thesis is devoted to the characterization of decidable instances of the existence of LESPs for arbitrary PN models within the system-theoretic framework introduced in the thesis. The philosophical implication of the results in this thesis is the existence of what can be called a ""finite basis"" of an infinite state system under supervision, on which the membership tests can be performed in finite time; hence resulting in the decidability of problems and finite-time termination of algorithms. The thesis discusses various scenarios where such a finite basis exists and how to find them."","abstract_has_math":false,"creators":["Raman, Arun"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Systems & Entrepreneurial Engr","degree_department":null,"school":null,"contributors":["Sreenivas, Ramavarapu","Basar, Tamer","Beck, Carolyn","Garg, Jugal"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2020,"date_issued":"2020-10-07T20:59:35Z","date_published":"2020-10-07T20:59:35Z","updated_at":"2026-07-22T22:24:48Z","subjects":["Liveness","Petri Nets","Supervisory Control","Discrete Event Systems","Deadlock"],"languages":["en"],"rights":["Copyright 2020 Arun Raman"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/108444","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Sreenivas, Ramavarapu","Basar, Tamer","Beck, Carolyn","Garg, Jugal"]},{"key":"dc:creator","label":"Author","values":["Raman, Arun"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2020-10-07T20:59:35Z","2020-07-09","2020-08"]},{"key":"dc:type","label":"Dc Type","values":["text","Thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Systems & Entrepreneurial Engr"]},{"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":["Liveness","Petri Nets","Supervisory Control","Discrete Event Systems","Deadlock"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2020 Arun Raman"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/108444"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["\"A Discrete Event System (DES) is a discrete-state system, where the state changes at discrete-time instants due to the occurrence of events. Informally, a liveness property stipulates that a 'good thing' happens during the evolution of a system. Some examples of liveness properties include starvation freedom -- where the 'good thing' is the process making progress; termination -- in which the good thing is for an evolution to not run forever; and guaranteed service -- such as in resource allocation systems, when every request for resource is satisfied eventually. In this thesis, we consider supervisory policies for DESs that, when they exist, enforce a liveness property by appropriately disabling a subset of preventable events at certain states in the evolution of DES. One of the main contributions of this thesis is the development of a system-theoretic framework for the analysis of Liveness Enforcing Supervisory Policies (LESPs) for DESs. We model uncertainties in the forward- and feedback-path, and present necessary and sufficient conditions for the existence of Liveness Enforcing Supervisory Policies (LESPs) for a general model of DESs in this framework. The existence of an LESP reduces to the membership of the initial state to an appropriately defined set. The membership problem is undecidable. For characterizing decidable instances of this membership problem, we consider a modeling paradigm of DESs known as Petri Nets, which have applications in modeling concurrent systems, software design, manufacturing systems, etc. Petri Net (PN) models are inherently monotonic in the sense that if a transition (which loosely represents an event of the DES) can fire from a marking (a non-negative integer-valued vector that represents the state of the DES being modeled), then it can also fire from any larger marking. The monotonicity creates a possibility of representing an infinite-state system using what can be called a \"\"finite basis\"\" that can lead to decidability. However, we prove that several problems of our interest are still undecidable for arbitrary PN models. That is, informally, a general PN model is still too powerful for the analysis that we are interested in. Much of the thesis is devoted to the characterization of decidable instances of the existence of LESPs for arbitrary PN models within the system-theoretic framework introduced in the thesis. The philosophical implication of the results in this thesis is the existence of what can be called a \"\"finite basis\"\" of an infinite state system under supervision, on which the membership tests can be performed in finite time; hence resulting in the decidability of problems and finite-time termination of algorithms. The thesis discusses various scenarios where such a finite basis exists and how to find them.\"","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2020-10-02 without embargo terms","The student, Arun Raman, accepted the attached license on 2020-07-03 at 01:45.","The student, Arun Raman, submitted this Dissertation for approval on 2020-07-03 at 01:55.","This Dissertation was approved for publication on 2020-07-09 at 11:52.","DSpace SAF Submission Ingestion Package generated from Vireo submission #15491 on 2020-10-02 at 15:11:44","Made available in DSpace on 2020-10-07T20:59:35Z (GMT). No. of bitstreams: 2 RAMAN-DISSERTATION-2020.pdf: 4776777 bytes, checksum: 2a270e7e3a18682890eacfbfd9eeaff7 (MD5) LICENSE.txt: 4207 bytes, checksum: f906fbca92c7a7257163ea9f19d9057e (MD5) Previous issue date: 2020-07-09"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["On the decidability of problems in liveness of controlled Discrete Event Systems modeled by Petri Nets"]}]}],"canonical_facts":{"dc:contributor":["Sreenivas, Ramavarapu","Basar, Tamer","Beck, Carolyn","Garg, Jugal"],"dc:creator":["Raman, Arun"],"dc:date":["2020-10-07T20:59:35Z","2020-07-09","2020-08"],"dc:description":["\"A Discrete Event System (DES) is a discrete-state system, where the state changes at discrete-time instants due to the occurrence of events. Informally, a liveness property stipulates that a 'good thing' happens during the evolution of a system. Some examples of liveness properties include starvation freedom -- where the 'good thing' is the process making progress; termination -- in which the good thing is for an evolution to not run forever; and guaranteed service -- such as in resource allocation systems, when every request for resource is satisfied eventually. In this thesis, we consider supervisory policies for DESs that, when they exist, enforce a liveness property by appropriately disabling a subset of preventable events at certain states in the evolution of DES. One of the main contributions of this thesis is the development of a system-theoretic framework for the analysis of Liveness Enforcing Supervisory Policies (LESPs) for DESs. We model uncertainties in the forward- and feedback-path, and present necessary and sufficient conditions for the existence of Liveness Enforcing Supervisory Policies (LESPs) for a general model of DESs in this framework. The existence of an LESP reduces to the membership of the initial state to an appropriately defined set. The membership problem is undecidable. For characterizing decidable instances of this membership problem, we consider a modeling paradigm of DESs known as Petri Nets, which have applications in modeling concurrent systems, software design, manufacturing systems, etc. Petri Net (PN) models are inherently monotonic in the sense that if a transition (which loosely represents an event of the DES) can fire from a marking (a non-negative integer-valued vector that represents the state of the DES being modeled), then it can also fire from any larger marking. The monotonicity creates a possibility of representing an infinite-state system using what can be called a \"\"finite basis\"\" that can lead to decidability. However, we prove that several problems of our interest are still undecidable for arbitrary PN models. That is, informally, a general PN model is still too powerful for the analysis that we are interested in. Much of the thesis is devoted to the characterization of decidable instances of the existence of LESPs for arbitrary PN models within the system-theoretic framework introduced in the thesis. The philosophical implication of the results in this thesis is the existence of what can be called a \"\"finite basis\"\" of an infinite state system under supervision, on which the membership tests can be performed in finite time; hence resulting in the decidability of problems and finite-time termination of algorithms. The thesis discusses various scenarios where such a finite basis exists and how to find them.\"","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2020-10-02 without embargo terms","The student, Arun Raman, accepted the attached license on 2020-07-03 at 01:45.","The student, Arun Raman, submitted this Dissertation for approval on 2020-07-03 at 01:55.","This Dissertation was approved for publication on 2020-07-09 at 11:52.","DSpace SAF Submission Ingestion Package generated from Vireo submission #15491 on 2020-10-02 at 15:11:44","Made available in DSpace on 2020-10-07T20:59:35Z (GMT). No. of bitstreams: 2 RAMAN-DISSERTATION-2020.pdf: 4776777 bytes, checksum: 2a270e7e3a18682890eacfbfd9eeaff7 (MD5) LICENSE.txt: 4207 bytes, checksum: f906fbca92c7a7257163ea9f19d9057e (MD5) Previous issue date: 2020-07-09"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/108444"],"dc:language":["en"],"dc:rights":["Copyright 2020 Arun Raman"],"dc:subject":["Liveness","Petri Nets","Supervisory Control","Discrete Event Systems","Deadlock"],"dc:title":["On the decidability of problems in liveness of controlled Discrete Event Systems modeled by Petri Nets"],"dc:type":["text","Thesis"],"thesis:degree_discipline":["Systems & Entrepreneurial Engr"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:48Z"}