Verification of safe diagnosability of stochastic discrete-event systems

Safe diagnosability of discrete-event systems (DESs) is viewed as the first necessary step of fault-tolerant supervision in the literature. For safe diagnosable systems, it is required that not only failures occurring in systems can be detected within a finite delay, but also the detection should be completed before running any unsafe operation. In this paper, we present a novel approach to deal with the safe diagnosis issue for stochastic DESs by constructing a nondeterministic automaton called the safe verifier, and the necessary and sufficient condition for safe diagnosability of stochastic DESs is presented. It is worth noting that the proposed approach has lower complexity than the existing approach based on safe diagnoser as far as the number of states.