A Sequence-Based Approach for the Verification of Current-State Opacity in Bounded Discrete Event Systems

Opacity deals with the capability of a system to hide a secret from a malicious intruder that partially observes the dynamic behavior of a system. When current-state opacity is considered, the secret consists of a set of reachable states. In this context, a system is said to be opaque if the intruder cannot infer whether the system reached either a secret or a non-secret state. A necessary and sufficient condition to verify current-state opacity in discrete event systems modeled with Petri nets is given. The proposed approach requires only system boundedness, without any additional assumptions, such as acyclicity of induced subnets, which is usually required in the results proposed in the literature. We prove that in bounded systems, opacity can be assessed by checking the corresponding condition only on a finite set of enabled words. Such asequence-basedapproach may lead to speeding up the opacity verification, as it is shown by means of a comparison with observer-based approaches. Moreover, the proposed algorithm for opacity verification, which relies on the solution of optimization problems, can be parallelized, further improving its efficiency. A motivating example is referred to throughout the paper to illustrate step-by-step the proposed approach.