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

点击翻译按钮获取中文摘要

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.