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

• 成果类型: Article
• 署名作者: Li, Jun; Lefebvre, Dimitri; Hadjicostis, Christoforos N.; Li, Zhiwu
• 署名单位: Xidian University; Universite Le Havre Normandie; University of Cyprus; Macau University of Science & Technology
• 刊物名称: IEEE TRANSACTIONS ON AUTOMATIC CONTROL
• ISSN/ISSBN: 0018-9286
• DOI: 10.1109/TAC.2024.3432788
• 发表日期: 2025
• 页码: 503-509
• 关键词: automata; Servers; observers; clocks; Real-time systems; privacy; Petri nets; Discrete event system (DES); graph theory; timed automaton; timed opacity

摘要

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.