Diagnosability Verification in Labeled Petri Nets Using a Twin Model

Abstract This paper deals with the problem of diagnosability verification in discrete event systems. Given a discrete event system modeled by labeled Petri nets that may contain deadlocks, a revised topology of the system, called a twin model, is established to test the diagnosability of the original net. This procedure employs a deterministic finite state automaton, called a diagnoser that is derived from the quiescent basis reachability graph of the twin model. We prove that the original net is diagnosable if and only if the diagnoser established from the twin model does not contain any cycle in which at least a state can reach an indeterminate state. Moreover, the proposed method does not need to calculate a complete or partial reachability set of the considered system, which in practice decreases the computational burden as revealed by experimental studies. Finally, a manufacturing example is presented to illustrate the proposed method.