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 et al. 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. Note to Practitioners-Fault diagnosis is a very important problem in several domains of applications, such as manufacturing, telecommunication, electronics, and so on, since after the occurrence of a fault the system usually deviates from its nominal behavior and appropriate actions of recovery should be performed. As a consequence, this problem has been extensively studied in the past years both in the case of time-driven and discrete-event systems, and several approaches have been proposed. A problem strictly related to fault diagnosis is diagnosability. Solving a problem of diagnosability is equivalent to determine if a system is diagnosable with respect to a given fault, i.e., to determine if, once the fault has occurred, the system can detect its occurrence after a finite observation of the system evolution. Obviously, diagnosability is an essential property that must hold if a diagnosis approach is to be applied in real life applications. This paper is devoted to diagnosability analysis and a procedure based on labeled Petri nets is proposed.