Grants and Contributions:

Grant or Award spanning more than one fiscal year. (2017-2018 to 2022-2023)

Discrete-Event Systems (DES) model a system's behaviour as automata, and use this to formally verify properties such as controllability (will the system stay within desired behaviour) and nonblocking (a form of deadlock detection). Application areas include manufacturing, communication, and transport systems, as well as automotive applications.

The long-term goal of this project is to improve the adoption of Discrete-Event Systems by industry. The short-term objectives we will focus on in this proposal are 1) simplifying supervisor implementation and 2) design, and 3) improving scalability.

The short-term objective of simplifying implementation will be addressed by building upon the Sampled-Data (SD) supervisory control work of Wang. This method addresses a number of concurrency and timing issues involved in converting a Timed DES (TDES) supervisor into an implementation as a Moore Finite State Machine (FSM). To make this translation possible, a number of SD properties must be satisfied, many of which may not be easy to address by hand, nor specified based solely on safety and deadlock concerns. To make all steps of the translation easy and automatic, we will develop a synthesis method and a discrete optimization approach that will resolve any remaining control decisions. This will provide a key missing step that will not only provide a higher quality result, but remove a difficult and time consuming process from the design.

The short-term objective of simplifying supervisor design will be addressed by creating a method to allow the designer to specify controllers directly as Moore finite state machine (FSM), and then automatically convert the FSM (a common design format for engineers) into equivalent supervisors for verification. As a major barrier to the adoption of formal methods is the lack of users trained in the area, this should make this approach much more accessible to non-experts.

The short-term objective of improving scalability will be primarily addressed by leveraging the Hierarchical Interface-based Hierarchical Supervisory Control (HISC) approach of Leduc. This project will start with extending timed DES to HISC. This will allow TDES to be applied to much larger systems, making the method more useful to industry, and lay the foundation for extending the sampled-data method to HISC as well.

We will also investigate improving the scalability of fault diagnosis and the fault-tolerant supervisors. These topics were chosen as the ability to detect and handle faults is of wide interest to industry, so improving the size of systems they can handle is highly desirable. For fault diagnosis, a method to manually design diagnosers (as opposed to the current synthesis-based approach) will be developed that should allow for significant reduction in algorithm complexity. For fault-tolerance, we will adapt the approach of Leduc to make use of the HISC infrastructure.