Verification of Current-State Opacity in Time Labeled Petri Nets With Its Application to Smart Houses

This work addresses the verification of current-state opacity with respect to a real-time observation generated from time-dependent systems. The secret behavior of a time-dependent system is defined as a set of states in a time labeled Petri net. The current-state opacity of a real-time observation means that a given secret remains opaque to the intruder who can partially observe the system behavior in the framework of a time labeled Petri net at a given time instant. We introduce a novel directed graph, called a parallel state class graph, to represent the parallel evolution of time-dependent systems exhaustively. Based on the parallel state class graph, we design an algorithm for the construction of a critical observer and show that the current-state opacity of a real-time observation in time labeled Petri nets can be efficiently solved by the critical observer. This approach is computationally competitive since the critical observer can be constructed by solving a number of linear programming problems.