$K$-Step Opacity Verification and Enforcement of Time Labeled Petri Net Systems
Yifan Dong, Dimitri Lefebvre, Zhiwu Li · IEEE Transactions on Automatic Control · 2025
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.