Modular Verification and Supervisory Controller Design for Discrete-Event Systems Using Abstraction and Incremental Construction.

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.