Verification of State-Based Timed Opacity for Constant-Time Labeled Automata

This article proposes and verifies two types of state-based timed opacity notions for constant-time labeled automata (a class of timed models with partially observable transitions), called [T-l,T-u]-opacity and [T-l,+infinity)-opacity . A system is said to be [T-l,T-u]-opaque (respectively, [T-l,+infinity)-opaque ) if no timed observation can lead to the exposure of specified states (called secret states ) within a finite time window (respectively, an infinite time window) starting at the time instant TTl . Based on the design principle of a timed observer developed in our previous work, we show that the timed observer of a system can be used to estimate the set of states in which the system may stay within certain (finite or infinite) time windows. The key of this approach is to determine whether a given time value is a possible elapsed time value from one observer state to another according to the structural information of the timed observer. From this methodology, we present two algorithms to verify the proposed opacity notions. The complexities of the algorithms are O(2|(X)|) and O(2(3 & sdot;|X|)) , respectively, and the complexity of the structural analysis of the observer is O((|Q|+2)& sdot;2(2 & sdot;|X|)) , where |X| and |Q| are the numbers of states and labels in a plant.