Methods and Tools in Supervisory Control Theory: Operator Aspects, Computational Efficiency, and Applications

This thesis presents a tool together with efficient algorithms for verification and synthesis of discrete-event supervisors that might share responsibilities with human operators. It is also shown how the supervisory control theory can be used to solve resource allocation problems for flexible manufacturing systems. The supervisory control theory is a formal methodology for analyzing properties of discrete-event systems and also for generating supervisors that enforce that a system behaves according to given specifications. The supervisory control theory shows great promise to help developers to create correct control functions for discrete event systems. Unfortunately, industrial acceptance has been limited so far. In this thesis we try to identify the major factors that prevent the supervisory control theory from becoming an industrial success. Four major limiting factors are identified. First, we note that supervisory control problems are inherently hard to solve. This implies that brute-force algorithms will only be able to solve relatively small problems, thus there is a need for more intelligent algorithms that will take advantage of the structure present in many systems. Second, control systems that interact with humans are becoming more widely used. In this thesis a framework for analysis and synthesis of discrete event supervisors that need to interoperate with human users is developed. Third, the lack of efficient tools is an important factor that limits the industrial acceptance of the supervisory control theory. An efficient tool for supervisor synthesis, verification, simulation, and code-generation has been developed as part of this work. Fourth, the lack of industrial success stories is holding back the acceptance of the supervisory control theory. We show how a large class of resource allocation systems can be easily solved by the supervisory control theory. A commercial chemical batch control system has been extended with resource allocation capabilities where a supervisor is automatically synthesized according to the supervisory control theory. The supervisor guarantees that the concurrently running batches never run into circular waits for shared resources. The supervisor handles flexible batch recipes with sequential, parallel, and alternative operations, where each operation might be produced in a number of resources. Alternative operations are used to handle errors that emerge during the production of a batch