Verification and enforcement of strong infinite- and k-step opacity using state recognizers

In this paper, we study the verification and enforcement problems of strong infinite-step opacity and k-step opacity for partially observed discrete-event systems modeled by finite state automata. Strong infinite-step opacity is a property such that the visit of a secret state cannot be inferred by an intruder at any instance along the entire observation trajectory, while strong k-step opacity is a property such that the visit of a secret state cannot be inferred within k steps after the visit. We propose two information structures called an 8-step recognizer and a k-step recognizer to verify these two properties. The complexities of our algorithms to verify strong infinite- and k-step opacity are O(2(2.vertical bar X vertical bar) . vertical bar E-o vertical bar) and O(2((k+2)) .vertical bar X vertical bar . vertical bar Eo vertical bar), respectively, which are lower than that of existing methods in the literature (vertical bar X vertical bar and vertical bar E-o vertical bar are the numbers of states and observable events in a plant, respectively). We also derive an upper bound for the value of k in strong k-step opacity, and propose an effective algorithm to determine the maximal value of k for a given plant. Finally, we note that enforcement of strong infinite- and k-step opacity can be transformed into a language specification enforcement problem and hence be solved using supervisory control. (C) 2021 Elsevier Ltd. All rights reserved.