Verification and enforcement of strong infinite- and k-step opacity using state recognizers. (November 2021)

• Record Type: Journal Article
• Authors: Ma, Ziyue; Yin, Xiang; Li, Zhiwu
• Is Part Of: Automatica. Volume 133(2021)
• Publication Date: 2021-11
• Subjects: Discrete event system -- Infinite-step opacity -- k-step opacity -- State recognizer; Automatic control -- Periodicals; Automation -- Periodicals; 629.805
• DOI: 10.1016/j.automatica.2021.109838
• Languages: English
• ISSNs: 0005-1098

Abstract

Abstract: 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 ∞ -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 ⋅ | X | ⋅ | E o | ) and O ( 2 ( k + 2 ) ⋅ | X | ⋅ | E o | ), respectively, which are lower than that of existing methods in the literature ( | X | and | E o | 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.