An Efficient Algorithm for the Verification of Codiagnosability of Discrete Event Systems With Dynamic Observations

In this work, we propose a new algorithm for the verification of codiagnosability of a discrete event system with dynamic observations, which is an extension of a recently proposed algorithm for the verification of codiagnosability of discrete event systems with static observations. The proposed verifier, called E-VERIFIER, is compared with two different verifiers presented in the literature: ( i ) the T-VERIFIER, which is proposed for the verification of transition-based codiagnosability; and (ii) the C-VERIFIER, which employs cluster automata as the basic element for computation instead of the original states of the automaton system model. We show that although the E-VERIFIER has the same computational complexity as the C-VERIFIER and the T-VERIFIER, it has the following advantages over the other methods: ( i ) since the E-VERIFIER represents all faulty and fault-free traces of the system that have the same dynamic projection, then, unlike the C-VERIFIER, the traces that lead the system to violating the codiagnosability condition can be straightforwardly obtained from the E-VERIFIER, and the delay for decentralized diagnosis can be computed using only the E-VERIFIER; and ( ii ) the E-VERIFIER can be computed more efficiently than the T-VERIFIER when its number of states grows. As a consequence of the proposed approach, we present a method for the computation of the delay for decentralized diagnosis of discrete event systems with dynamic observations, adapting an algorithm based on the verifier for the case of static observations.