Codiagnosability Analysis of Bounded Petri Nets

In this paper, we propose a novel approach to perform codiagnosability analysis of labeled bounded Petri nets. 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. In a previous work by some of us, it has been proven that a necessary and sufficient condition for codiagnosability under such a framework is the absence of sequences that are ambiguous with respect to all sites and whose length may grow indefinitely after the occurrence of some 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 allows one to detect the presence of ambiguous sequences. Finally, we introduce the notion of K-codiagnosability: a system is K-codiagnosable if and only if faults can be detected in the above framework within at most K observations after their occurrence. An algorithm is provided to compute the smallest value of K such that the system is K-codiagnosable.