Complexity and Implementation for Discrete-Event Systems

离散事件系统（DES）将系统行为建模为自动机，并使用它来正式验证诸如可控性（系统是否保持期望的行为）和非阻塞性（死锁检测的一种形式）等属性。应用领域包括制造、通信和运输系统，以及汽车应用。******这个项目的长期目标是提高工业界对离散事件系统的采用。在本提案中，我们将关注的短期目标是1)简化监督器的实现和2)设计，以及3)提高可扩展性。******简化实施的短期目标将通过建立王的抽样数据（SD）监督控制工作来解决。此方法解决了将定时DES （TDES）管理器转换为作为Moore有限状态机（FSM）的实现所涉及的许多并发性和定时问题。要实现这种转换，必须满足许多SD属性，其中许多属性可能不容易手工处理，也不能仅根据安全和死锁问题指定。为了使翻译的所有步骤变得简单和自动化，我们将开发一种综合方法和一种离散优化方法，以解决任何剩余的控制决策。这将提供一个关键的缺失步骤，不仅将提供更高质量的结果，但从设计中删除一个困难和耗时的过程。******简化管理器设计的短期目标将通过创建一种方法来解决，该方法允许设计人员直接将控制器指定为Moore有限状态机（FSM），然后自动将FSM（工程师常用的设计格式）转换为等效的管理器以进行验证。由于采用正式方法的主要障碍是缺乏在该领域受过培训的用户，这应该使非专家更容易使用这种方法。******提高可扩展性的短期目标将主要通过利用Leduc基于分层接口的分层监督控制（HISC）方法来解决。该项目将从将定时DES扩展到HISC开始。这将允许TDES应用于更大的系统，使该方法对工业更有用，并为将采样数据方法扩展到HISC奠定基础。******我们还将研究提高故障诊断的可扩展性和容错监督器。之所以选择这些主题，是因为检测和处理故障的能力是工业界广泛关注的问题，因此提高它们可以处理的系统的大小是非常可取的。对于故障诊断，将开发一种手动设计诊断器的方法（与当前基于综合的方法相反），该方法应允许显著降低算法复杂性。对于容错，我们将采用Leduc的方法来利用HISC基础设施。

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.