Codiagnosability verification of bounded Petri nets using basis markings

In this paper we propose a novel approach to perform codiagnosability analysis of bounded Petri nets with arbitrary labeling functions. In more detail, a set of sites observe the system evolution, each one with its own observation mask. Sites do not exchange information with each other but communicate with a coordinator. The coordinator is able to detect a fault if and only if at least one site is able to do that. The proposed approach is based on a necessary and sufficient condition for codiagnosability, namely the absence of sequences that are 'ambiguous' with respect to all sites and whose length may grow indefinitely after the occurrence of some fault (i.e., sequences of infinite length that could be observed either in the presence of a fault and with no fault). The novelties of the approach consist in using the notion of basis markings to avoid exhaustive enumeration of the set of reachable markings, and in the construction of an automaton, called Verifier, that enables to detect the presence of ambiguous sequences.