Verification and synthesis for failure diagnosis of discrete event systems subject to permanent sensor failures

In this paper, we consider a failure diagnosis problem for discrete event systems subject to permanent sensor failures. A notion of diagnosability subject to permanent sensor failures is introduced with respect to a certain nondeterministic observation mask. For its verification, we define an aggregated Mealy automaton with a deterministic and state-dependent observation mask. We show that diagnosability of the aggregated Mealy automaton is equivalent to diagnosability of the original system subject to permanent sensor failures. Then, we present a method for verifying diagnosability of the aggregated Mealy automaton. Moreover, we synthesize a diagnoser for the original system as an online diagnoser.