Verification of Detectability for Time Labeled Petri Net Systems with Unobservable Transitions

We investigate the detectability verification problem of time-dependent systems modeled by time labeled Petri nets that are a typical time-dependent model of many computer-integrated systems in modern society, characterized by networked connections. In a time labeled Petri net, the detectability proposed in this paper characterizes the current state of a time-dependent system that can be uniquely determined after a finite number of observations within a given time instant. Moreover, we further define strong and weak detectability in a time labeled Petri net system. To verify strong and weak detectability, we excogitate a label-based state class graph, which is not required to enumerate all states of a system, to compute the states for a given real-time observation. Based on the proposed label-based state class graph, an information structure called a timed state observer is formulated to verify strong and weak detectability. The proposed verification technique is advantageous and is effectively applied to an intelligent garage system, since the enumeration of all states of the time-dependent system is not required.