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

该建议的动机是对具有时间逻辑规范的离散事件系统的控制和诊断进行全面和正式的研究。监督控制理论为事件驱动系统提供了一种形式主义或综合控制器，以强制执行所需的定性规范。这些规范传统上表示为形式语言或等价的状态机。然而，用一种接近自然口语的语言来表达规范更为实际。时间逻辑试图在形式语言和自然语言之间架起一座桥梁。这是我们的目的是开发技术的控制和诊断的离散事件系统，当规范是在时间逻辑表示。我们选择由Clarke-Emerson-Sitsla提出的CTL（计算树逻辑）和LTL（线性时间逻辑）的时间逻辑，其中存在自动化技术来验证系统属性。拟议的研究通过开发合成控制器和诊断器的自动化技术来补充这项工作。在此背景下提出了完全观测控制、部分观测控制、模块化控制、故障建模与诊断、符号法计算等问题。我们的初步工作表明，使用时间逻辑，没有计算复杂性的损失，但肯定有可表达性和用户友好性的增益。

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.