Diagnosability of Petri nets with observation graphs

This paper addresses the problem of diagnosability for dynamic discrete event systems modeled with bounded or unbounded Petri nets that are deadlock-free and monitored with sensor configurations with marking and event measurements. The proposed method gives necessary and sufficient conditions for diagnosability. It is based on the transformation of the coverability graph into an observation graph that encodes all observation sequences of measured markings and events with respect to the sensor configuration. This graph also encodes all sequences of transitions that may fire from any reachable marking of the Petri net. Diagnosability is determined by analyzing the paths and circuits in the observation graph. The method is illustrated with several examples of bounded or unbounded Petri nets.