Critical Observability Verification and Enforcement of Labeled Petri Nets by Using Basis Markings

A discrete event system is said to be critically observable if the observer can always determine whether the current state necessarily belongs to a set of critical states. This paper focuses on two issues related to the safety and security of discrete event systems, namely critical observability verification and enforcement of labeled Petri nets. First, given a bounded net, we verify its critical observability by using basis markings and solving some integer linear programming problems, thus avoiding the enumeration of the full state space of a net system. Moreover, for a non-critically observable net system, we obtain a feasible stop-free event set from a twin basis reachability graph such that a valid control policy can be always found, if the feasible stop-free event set is non-empty. Finally, according to the feasible stop-free event set, a set of disabled edges is generated, and an online control policy is developed based on the supervisory control theory, which guarantees that the closed-loop system is critically observable and deadlock-free.