Critical Observability of Labeled Time Petri Net Systems

A time Petri net is said to be critically observable at a given time instant if the markings consistent with any observation at the time instant are included either in the set of critical markings or non-critical markings. This work studies the verification problem of critical observability for timed discrete event systems modeled by bounded labeled time Petri nets. The proposed method is a two-fold process: a preliminary verification of critical observability for the underlying logic labeled Petri net and a further verification considering the time constraint associated with each transition. The first step is based on the concurrent composition of a reachability graph of the logic net. If the logic net is critically observable, then the time net is also critically observable at any given time instant. Otherwise, the second step is to design an algorithm to compute all pairs of transition-class sequences that violate critical observability at the given time instant, and then a set of linear programming problems is exploited to check critical observability for the corresponding timed system.
Note to Practitioners
—Timed discrete event systems provide a theoretical model for safety-critical real applications such as air traffic management, smart grid, and industrial control, which are vulnerable to malicious attack and destruction at some particular time instants such that a system may be misled to dangerous states. Critical observability of a timed discrete event system is a property with which the predefined dangerous states can be determined and detected from the observation by an observer at a given time instant. This research aims to offer a systematic approach to check critical observability for timed discrete event systems modeled by bounded labeled time Petri nets, which can also present some new ideas and insights for practitioners in the field of safety-critical systems.