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

This article presents a procedure for <inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"><tex-math notation="LaTeX">$K$</tex-math></inline-formula>-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 <inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"><tex-math notation="LaTeX">$K$</tex-math></inline-formula>-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 <inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"><tex-math notation="LaTeX">$K$</tex-math></inline-formula> 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 <inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"><tex-math notation="LaTeX">$K$</tex-math></inline-formula>-step opacity of a timed observation by solving a number of linear programming problems. Finally, when the timed observation is not <inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"><tex-math notation="LaTeX">$K$</tex-math></inline-formula>-step opaque, a strategy by adjusting the time horizons of transitions with soft time intervals is proposed for the opacity enforcement purpose.