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 behavior. Several notions of opacity have been discussed in the literature, including current-state opacity, k-step opacity, and infinite-step opacity. We investigate weak and strong k-step opacity, the notions that generalize both current-state opacity and infinite-step opacity, and ask whether the intruder is not able to decide, at any instant, when respectively whether the system was in a secret state during the last k observable steps. We design a new algorithm verifying weak k-step opacity, the complexity of which is lower than the complexity of existing algorithms and does not depend on the parameter k, and show how to use it to verify strong k-step opacity by reducing strong k-step opacity to weak k-step opacity. The complexity of the resulting algorithm is again better than the complexity of existing algorithms and does not depend on the parameter k.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
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 …
Abstraction-Based Verification of Approximate Pre-Opacity for Control Systems
In this paper, we consider the problem of verifying pre-opacity for discrete-time control systems. Pre-opacity is an important information-flow security property that secures the intention of a system to execute some sec…
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 …
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 …
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…