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 <tex-math notation="LaTeX">[Tₗ,Tᵤ]</tex-math>-opacity and <tex-math notation="LaTeX">[Tₗ,+∞)</tex-math>-opacity. A system is said to be <tex-math notation="LaTeX">[Tₗ,Tᵤ]</tex-math>-opaque (respectively, <tex-math notation="LaTeX">[Tₗ,+∞)</tex-math>-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 <tex-math notation="LaTeX">Tₗ</tex-math>. 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 <tex-math notation="LaTeX">O(2|X|)</tex-math> and <tex-math notation="LaTeX">O(2^3· |X|)</tex-math>, respectively, and the complexity of the structural analysis of the observer is <tex-math notation="LaTeX">O((|Q|+2)· 22· |X|)</tex-math>, where <tex-math notation="LaTeX">|X|</tex-math> and <tex-math notation="LaTeX">|Q|</tex-math> are the numbers of states and labels in a plant.