Critical Observability of Partially Observed Petri Nets

This paper studies the problem of checking critical observability of discrete event systems modeled by partially observed Petri nets (POPNs) that are measured by sensors associated with both transitions and places. In particular, a POPN is said to be critically observable, if all the markings consistent with any observation of the POPN are included either in a critical set or outside it. To address the problem in the framework of POPNs, we first build a reachability graph that can describe the evolution of the POPN. Based on the reachability graph, we construct an automaton called verifier that permits us to check the critical observability. Then, a notion of belief is introduced to evaluate the possibility of the critical observability of the POPN. Finally, two examples are presented to shed light on the validity of the proposed approach.