Critical Observability of Discrete-Event Systems in a Petri Net Framework

This article focuses on the issue of checking critical observability for labeled Petri nets. Critical observability is a property related to the safety concern of cyber-physical systems. With the aim of checking this property of a net system, it is required to detect whether a set of markings consistent with any observed word of the net system is a subset of a set of critical states representing undesirable operations or a set of noncritical states. In this work, we prove a necessary and sufficient condition to check critical observability when the critical state set is described by an arbitrary subset of reachable markings. Then, the result is extended to the case when a critical state set is modeled by all the reachable markings that satisfy disjunctions of generalized mutual exclusion constraints. The proposed method is derived from the solutions of integer linear programming problems and is applicable to net systems with liveness and boundness. Several case studies show the performance of the presented methodology for discrete-event systems.