In this paper, we propose a method to analyze diagnosability of bounded Petri nets with arbitrary labeling functions. The notion of basis marking is employed to avoid exhaustive enumeration of the set of reachable markings. The novelty consists in removing an assumption that is common in this framework, namely the Petri net system is deadlock-free after the occurrence of any fault. A finite state automaton, called DF-Verifier, is constructed, which allows one to perform diagnosability analysis by looking at some special cycles and states.
展开▼
