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.