Control and Diagnosis of Discrete-event Systems with Temporal Logic Specifications

该建议的动机是从一个全面的和正式的研究与时序逻辑规范的离散事件系统的控制和诊断。监督控制理论为事件驱动的系统提供了一种形式化的或综合的控制器，以实现所需的定性规范。这样的规范传统上被表示为形式语言或等价地表示为状态机。然而，用一种接近自然口语的语言来表达规范更实用。时态逻辑试图在形式语言和自然语言之间架起一座差距的桥梁。这是我们的目的是开发技术的离散事件系统的控制和诊断时，表示在时序逻辑的规范。我们选择的时间逻辑CTL（计算树逻辑）和LTL（线性时间逻辑）提出的Clarke-Emerson-Sitsla的自动化技术存在验证系统属性。拟议的研究补充，通过开发自动化技术，综合控制器和诊断器的工作。在这种情况下，已经提出了几个问题，包括完全观察下的控制，部分观察下的控制，模块化控制，故障建模和诊断，以及使用符号方法的计算。我们的初步工作表明，使用时序逻辑，没有损失的计算复杂性，但肯定有一个增益的可表达性和用户友好性。

The proposal is motivated from a comprehensive and formal study of control and diagnosis of discrete event systems with temporal logic specifications. The supervisory control theory provides a formalism or synthesizing controllers for event-driven systems in order to enforce desired qualitative specifications. Such specifications are traditionally expressed as formal languages or equivalently as state machines. It is more practical, however, to express specifications in a language close to a natural spoken language. Temporal logic is an attempt to bridge the gap between formal and natural languages. It is our intent to develop techniques for control and diagnosis of discrete event systems when the specifications are expressed in temporal logic. We choose the temporal logics of CTL (computational tree logic) and LTL (linear time logic) proposed by Clarke-Emerson-Sitsla for which automated techniques exist for verifying system properties. The proposed research complements that work by developing automated techniques for synthesizing controllers and diagnosers. Several problems in this context have been proposed including, control under complete observation, control under partial observation, modular control,failure modeling and diagnosis, and computation using the symbolic method. Our initial work shows that with the usage of temporal logic, there is no loss of computational complexity, yet there is surely a gain of expressibility and user-friendliness.