Diagnosability for discrete event systems based on Petri net language

In this paper, the diagnosability for discrete event systems has been extended to Petri net language, which is motivated from some network systems. A composition net, called as verifier, is constructed for analysis of diagnosability. It is proved that the diagnosability for Petri net language is equal to a reachability problem of verifier with respect to the marked markings set for any failure transition of system. The practical verification condition is further given for general unbounded Petri net based on the coverability tree of verifier.