Codiagnosability Enforcement in Labeled Petri Nets

This article aims to enforce codiagnosability in labeled Petri nets, which are monitored by a series of sites. A labeled Petri net is codiagnosable with respect to a certain fault, if the occurrence of such a fault could be detected by at least one of the sites. We assume that codiagnosability is imposed to a noncodiagnosable system by appropriately positioning additional sensors. In particular, the goal is that of minimizing the cost of the new sensors. The enumeration of the whole state space is avoided, thanks to the notions of basis markings and minimal explanations. An automaton, called unfolded verifier, is introduced to verify codiagnosability. Finally, the set of optimal labeling functions is obtained solving an integer nonlinear programming problem.an integer nonlinear programming problem.