Polynomial-time verification of pattern diagnosability for timed discrete event systems

This work focuses on the verification of diagnosability of timed patterns in discrete event systems by using a specific class of timed automata. A timed pattern refers to a set of behaviors which are defined by a sequence of events taking place in a given order and within specific time intervals. A silent closure is derived from a tick recognizer by removing all silent events, which provides benefits for the systems encompassing numerous silent events. For the diagnosability test, a timed pair composition structure is created by combining a normal silent closure with an accepted silent closure, both of which are obtained from the silent closure with respect to normal and faulty behaviors, respectively. The constructed timed pair composition can track normal and faulty behaviors simultaneously. By analyzing the timed pair composition regarding the presence of indeterminate cycles, we formulate a necessary and sufficient condition for the diagnosability verification of timed patterns, affirming that a system is diagnosable if and only if there is no indeterminate cycle in the timed pair composition. The proposed method is shown to be of polynomial time complexity at most.