Diagnosability Verification and Enforcement for Unbounded Petri Nets by Online Supervisors

This paper addresses the problems of diagnosability verification and enforcement of discrete event systems modeled with unbounded Petri nets. Diagnosability in such systems is critical for ensuring reliability and maintaining operational integrity, yet current methods often struggle with the complexity introduced by unboundedness and potential deadlocks. Given an unbounded labeled Petri net that may reach deadlocks, a quiescent basis coverability graph is established to verify the diagnosability of the considered system. This procedure employs a deterministic finite state automaton, called an extended verifier, derived from the proposed quiescent basis coverability graph. It is shown that an unbounded Petri net is diagnosable if and only if the verifier does not contain a class of cycles, called repetitive $F$ -cycles. This result also provides necessary and sufficient conditions for diagnosability enforcement by developing an online supervisor. Further, the designed supervisor is maximally permissive and also circumvents a plant entering deadlocks by firing non-fault sequences. Examples are presented to demonstrate the proposed method. Note to Practitioners-Fault diagnosis and diagnosability enforcement are critical for the development and operation of highly automated systems covering computer-integrated production processes, intelligent traffic, computer and communication networks, smart gird, etc. This work touches upon this problem from the perspective of discrete event systems that are modeled with unbounded labeled Petri nets. The feasibility and applicability of the reported method stem from the usage of a structurally compact representation of a considered plant such that the computational cost of a real-world system is acceptable. The graphical representation of Petri nets as well as the proposed quiescent basis coverability graph make the method easy to use and manipulate. Moreover the sufficient and necessary conditions of diagnosability enforcement can be readily verified by the supervisory theory, facilitating its adoption by practitioners.