Strong Co-Detectability for Labeled Petri Nets and Its Enforcement via Additional Sensors

This article addresses the problem of verifying co-detectability for a labeled Petri net (LPN) that is observed at multiple observation sites, each with its own observation map. A system is strongly co-detectable if at least one site is able to determine the state of the system uniquely following any long enough sequence of observations. We check strong co-detectability for an LPN using an approach that exploits the notion of basis markings, which avoids an exhaustive enumeration of all reachable markings of the net. Specifically, a structure based on the basis reachability graph (BRG) of the system, called a BRG-based co-verifier, is obtained for the verification of strong co-detectability. In addition, using the proposed BRG-based co-verifier, some rules and relabeling options are provided to identify a new relabeling function such that a system that is not strongly co-detectable becomes strongly co-detectable. An integer programming problem is formulated to find an optimal relabeling function when considering different relabeling costs on transitions. Finally, two application examples are presented to illustrate the proposed approach.