Failure Diagnosis of Discrete-Event Systems With Linear-Time Temporal Logic Specifications
- 14 June 2004
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Automatic Control
- Vol. 49 (6), 934-945
- https://doi.org/10.1109/tac.2004.829616
Abstract
The paper studies failure diagnosis of discrete-event systems (DESs) with linear-time temporal logic (LTL) specifications. The LTL formulas are used for specifying failures in the system. The LTL-based specifications make the specification specifying process easier and more user-friendly than the formal language/automata-based specifications; and they can capture the failures representing the violation of both liveness and safety properties, whereas the prior formal language/automaton-based specifications can capture the failures representing the violation of only the safety properties (such as the occurrence of a faulty event or the arrival at a failed state). Prediagnosability and diagnosability of DESs in the temporal logic setting are defined. The problem of testing prediagnosability and diagnosability is reduced to the problem of model checking. An algorithm for the test of prediagnosability and diagnosability, and the synthesis of a diagnoser is obtained. The complexity of the algorithm is exponential in the length of each specification LTL formula, and polynomial in the number of system states and the number of specifications. The requirement of nonexistence of unobservable cycles in the system, which is needed for the diagnosis algorithms in prior methods to work, is relaxed. Finally, a simple example is given for illustration.Keywords
This publication has 35 references indexed in Scilit:
- Synthesizing processes and schedulers from temporal specificationsPublished by Springer Nature ,2005
- Polynomial-time verification of diagnosability of partially observed discrete-event systemsIEEE Transactions on Automatic Control, 2002
- A fault tolerant control architecture for automated highway systemsIEEE Transactions on Control Systems Technology, 2000
- Communication protocols for a fault-tolerant automated highway systemIEEE Transactions on Control Systems Technology, 2000
- Failure diagnosis using discrete-event modelsIEEE Transactions on Control Systems Technology, 1996
- Diagnosability of discrete-event systemsIEEE Transactions on Automatic Control, 1995
- A temporal framework for assembly sequence representation and analysisIEEE Transactions on Robotics and Automation, 1994
- Verifying a class of nondeterministic discrete event systems in a generalized temporal logicIEEE Transactions on Systems, Man, and Cybernetics, 1992
- Decidability for a temporal logic used in discrete-event system analysisInternational Journal of Control, 1990
- Control problems in a temporal logic frameworkInternational Journal of Control, 1986