Abstract: This presentation talks about failure diagnosis of discrete event systems with linear time temporal logic specifications. The use of Linear Temporal Logic formulae for specifying failures in the system is advocated. The LTL-based specifications is shown to make the specification process easier and more user-friendly than other formal language/automata-based specifications. It is argued that they can capture the failures representing the violation of both liveness and safety properties, whereas earlier developed formal language/automaton-based specifications can capture only failures representing the violation of safety properties (such as the occurrence of a faulty event or the arrival at a failure state). Pre-diagnosability and diagnosability of discrete event systems in the temporal logic setting are defined. The problem of testing pre-diagnosability and diagnosability is then be reduced to the problem of model checking. An algorithm for the test of pre-diagnosability 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. Finally, a simple example is given for illustration.

Shengbing Jiang received the B.S. degree in electrical engineering from the University of Science and Technology of China, Hefei, China, the M.S. degree in electrical engineering from East China Institute of Technology, Nanjing, China, and the Ph.D. degree in electrical engineering from the University of Kentucky, Lexington, in 1987, 1990, and 2002, respectively. He joined General Motors R&D, Warren, MI, in 2002. His research interests include formal methods, formal verification, supervisory control, and failure diagnosis of discrete-event and hybrid systems, and their applications in embedded software design.