On the decidability of problems in liveness of controlled Discrete Event Systems modeled by Petri Nets

Raman, Arun

Content Files

RAMAN-DISSERTATION-2020.pdf

Download Options

Download All Files Download Counts…

Loading…

Download Files

Loading…

Download Counts (All Files)

Loading…

Edit File

Loading…

Permalink

https://hdl.handle.net/2142/108444 Copy

Description

Title

On the decidability of problems in liveness of controlled Discrete Event Systems modeled by Petri Nets

Author(s)

Raman, Arun

Issue Date

2020-07-09

Director of Research (if dissertation) or Advisor (if thesis)

Sreenivas, Ramavarapu

Doctoral Committee Chair(s)

Sreenivas, Ramavarapu

Committee Member(s)

• Basar, Tamer
• Beck, Carolyn
• Garg, Jugal

Department of Study

Industrial&Enterprise Sys Eng

Discipline

Systems & Entrepreneurial Engr

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Date of Ingest

2020-10-07T20:59:35Z

Keyword(s)

• Supervisory Control
• Discrete Event Systems
• Deadlock
• Liveness
• 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."

Graduation Semester

2020-08

Type of Resource

Thesis

Permalink

http://hdl.handle.net/2142/108444

Copyright and License Information

Copyright 2020 Arun Raman

Owning Collections