K-Step Opacity Verification and Enforcement of Time Labeled Petri Net Systems

• 成果类型: Article
• 署名作者: Dong, Yifan; Lefebvre, Dimitri; Li, Zhiwu
• 署名单位: Macau University of Science & Technology; Universite Le Havre Normandie
• 刊物名称: IEEE TRANSACTIONS ON AUTOMATIC CONTROL
• ISSN/ISSBN: 0018-9286
• DOI: 10.1109/TAC.2025.3552020
• 发表日期: 2025
• 页码: 5848-5863
• 关键词: Petri nets; Discrete-event systems; Automata; Fault diagnosis; observers; Time factors; Real-time systems; Firing; trajectory; training; Delayed marking estimator (DME); discrete event system; K-step opacity; time labeled Petri net

摘要

This article presents a procedure for K-step opacity verification and enforcement of timed observations generated from discrete event systems modeled by time labeled Petri nets. Within the framework of a timed discrete event system that is partially observed by an intruder, a K-step opaque timed observation means that an intruder has observed the system with time stamps but is not able to deduce the secret information within the knowledge derived from the last K steps of the timed observation. We propose an information structure called a partial modified state class graph with respect to a timed observation. Then, based on the particular graph, an algorithm is designed to construct a delayed marking estimator that is used for the verification of K-step opacity of a timed observation by solving a number of linear programming problems. Finally, when the timed observation is not K-step opaque, a strategy by adjusting the time horizons of transitions with soft time intervals is proposed for the opacity enforcement purpose.