Modular Verification and Supervisory Controller Design for Discrete-Event Systems Using Abstraction and Incremental Construction.
Hill, Richard Charles
2008
Abstract
The subject of this dissertation is modular approaches to the verification and control of discrete-event systems (DES). DES are dynamic systems characterized by discrete states and event-driven evolution. In recent years, a substantial body of work has been built up to provide a theory and framework for the control and verification of DES. Despite all the advancements that have been made in this area, application to real-life systems has been somewhat slow. A significant hurdle to the adoption of these methods is the state-space explosion that occurs in modeling systems of the size most commonly found in industry. A common approach that has been applied to address this complexity problem is to construct a series of smaller modular supervisors, rather than a single monolithic supervisor. The problem with this approach is that the modular supervisors can often conflict with one another. This dissertation develops three new approaches to the supervisory control of DES that adopt a modular aspect to their control, while addressing the potential problem of conflict. The first approach addresses the problem of state-space explosion by offering a procedure for incrementally building modular supervisors that are guaranteed to not conflict with one another by construction. An observer type abstraction is employed to make the procedure more computationally feasible. The second approach of this dissertation constructs traditional modular supervisors, then adds another level of coordinating control to resolve conflict between the supervisors. This work employs a conflict-equivalence preserving abstraction to detect and resolve the conflict. The final approach of this dissertation employs interfaces between different components of the global system. The additional structure of these interfaces allows global properties to be verified through the achievement of local properties. Additionally, these interfaces allow for modular supervisors to be synthesized locally such that the necessary requirements are met by construction. In this work, the correctness of the three approaches is proven. Additionally, application to some manufacturing based examples are employed to illustrate the potential strengths and weaknesses of each of the approaches.Subjects
Supervisory Control Discrete Event Systems Logic Control Modular Control Hierarchical Control
Types
Thesis
Metadata
Show full item recordCollections
Showing items related by title, author, creator and subject.
-
Lemay, Joseph Louis (1963)
-
Park, Sukyung (2002)
-
Mechanical and dosimetric quality control for computer controlled radiotherapy treatment equipment Thompson, Antoinette V.; Lam, Kwok L.; Balter, James M.; McShan, Daniel L.; Martel, Mary K.; Weaver, Tamar A.; Fraass, Benedick A.; Ten Haken, Randall K. (Wiley Periodicals, Inc.American Association of Physicists in Medicine, 1995-05)
Remediation of Harmful Language
The University of Michigan Library aims to describe library materials in a way that respects the people and communities who create, use, and are represented in our collections. Report harmful or offensive language in catalog records, finding aids, or elsewhere in our collections anonymously through our metadata feedback form. More information at Remediation of Harmful Language.
Accessibility
If you are unable to use this file in its current format, please select the Contact Us link and we can modify it to make it more accessible to you.