Comparing the Notions of Opacity for Discrete-Event Systems
Opacity is an information flow property characterizing whether a system reveals its secret to a passive observer. Several notions of opacity have been introduced in the literature. We study the notions of language-based opacity, current-state opacity, initial-state opacity, initial-and-final-state opacity, K-step opacity, and infinite-step opacity. Comparing the notions is a natural question that has been investigated and summarized by Wu and Lafortune, who provided transformations among current-state opacity, initial-and-final-state opacity, and language-based opacity, and, for prefix-closed languages, also between language-based opacity and initial-state opacity. We extend these results by showing that all the discussed notions of opacity are transformable to each other. Besides a deeper insight into the differences among the notions, the transformations have applications in complexity results. In particular, the transformations are computable in polynomial time and preserve the number of observable events and determinism, and hence the computational complexities of the verification of the notions coincide. We provide a complete and improved complexity picture of the verification of the discussed notions of opacity, and improve the algorithmic complexity of deciding language-based opacity, infinite-step opacity, and K-step opacity.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
K-Step Opacity in Discrete Event Systems: Verification, Complexity, and Relations
Opacity is a property expressing whether a system may reveal its secret to a passive observer (an intruder) who knows the structure of the system but has a limited observation of its behavior. Several notions of opacity …
Secure Your Intention: On Notions of Pre-Opacity in Discrete-Event Systems
This paper investigates an important informationflow security property called opacity in partially-observed discrete-event systems. We consider the presence of a passive intruder (eavesdropper) that knows the dynamic mod…
Verifying Weak and Strong k-Step Opacity in Discrete-Event Systems
Opacity is an important system-theoretic property expressing whether a system may reveal its secret to a passive observer (an intruder) who knows the structure of the system but has only limited observations of its behav…
You Don't Know What I Know: On Notion of High-Order Opacity in Discrete-Event Systems
In this paper, we investigate a class of information-flow security properties called opacity in partial-observed discrete-event systems. Roughly speaking, a system is said to be opaque if the intruder, which is modeled b…
Local Opacity Verification for Distributed Discrete Event Systems
This paper studies current-state opacity and initial-state opacity verification of distributed discrete event systems. The distributed system's global model is the parallel composition of multiple local systems: each of …