Diagnosability of discrete event systems using labeled Petri nets

In this paper, we focus on labeled Petri nets with silent transitions that may either correspond to fault events or to regular unobservable events. We address the problem of deriving a procedure to determine if a given net system is diagnosable, i.e., the occurrence of a fault event may be detected for sure after a finite observation. The proposed procedure is based on our previous results on the diagnosis of discrete-event systems modeled with labeled Petri nets, whose key notions are those of basis markings and minimal explanations, and is inspired by the diagnosability approach for finite state automata proposed by Sampath in 1995. In particular, we first give necessary and sufficient conditions for diagnosability. Then, we present a method to test diagnosability that is based on the analysis of two graphs that depend on the structure of the net, including the faults model, and the initial marking.