A New Approach for Diagnosability Analysis of Petri Nets Using Verifier Nets
Maria Paola Cabasino, Alessandro Giua, Stéphane Lafortune, Carla Seatzu · IEEE Transactions on Automatic Control · 2012
In this paper, we analyze the diagnosability properties of labeled Petri nets. We consider the standard notion of diagnosability of languages, requiring that every occurrence of an unobservable fault event be eventually detected, as well as the stronger notion of diagnosability inKsteps, where the detection must occur within a fixed bound ofKevent occurrences after the fault. We give necessary and sufficient conditions for these two notions of diagnosability for both bounded and unbounded Petri nets and then present an algorithmic technique for testing the conditions based on linear programming. Our approach is novel and based on the analysis of the reachability/coverability graph of a special Petri net, called Verifier Net, that is built from the Petri net model of the given system. In the case of systems that are diagnosable inKsteps, we give a procedure to compute the boundK. To the best of our knowledge, this is the first time that necessary and sufficient conditions for diagnosability and diagnosability inKsteps of labeled unbounded Petri nets are presented.