Optimal sensor selection for ensuring diagnosability in labeled bounded Petri nets

This paper studies the problem of optimal static sensor selection for ensuring diagnosability in labeled bounded and unbounded Petri nets. Starting from a non-diagnosable labeled Petri net system, we present a systematic procedure to design a new labeling function that makes the system diagnosable and optimizes a given objective function. This procedure employs a particular net, called Verifier Net, that is built from the original Petri net and provides necessary and sufficient conditions for diagnosability. We exploit the system structure captured in the verifier net to guide the search for the desired new labeling function. The search is performed over an unfolding of the reachability/coverability tree of the verifier net and follows a set of rules that capture the relabeling strategy. We allow for unobservable transitions that cannot be labeled as well as for multiple fault classes. We formulate an integer linear programming problem that finds an optimal labeling function when numerical costs are associated with transition relabeling.