Failure diagnosis of discrete event systems with linear-time temporal logic fault specifications

The failure diagnosis problem of discrete event systems with linear-time temporal logic specifications is studied. Diagnosability of discrete event systems in the temporal logic setting is defined. The problem of testing diagnosability is reduced to the problem of model checking. An algorithm for the test of diagnosability and the synthesis of a diagnoser is obtained.