Verifying Weak and Strong k-Step Opacity in Discrete-Event Systems

Abstract

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 time 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.

Projects

IGA PrF 2023 026

Martin Trnečka
Jiří Balun, Jiří Valůšek

IGA PrF 2022 018

Martin Trnečka
Jiří Balun, Jiří Valůšek

Verification and Control of Networked Discrete Event Systems

Tomáš Masopust, Jan Komenda
Jiří Balun, Stéphane Lafortune, Spyros Reveliotis, Feng Lin

Links

Link

Authors

Jiří Balun
Tomáš Masopust

Automatica 155, 111153, 2023
Discrete-Event Systems and Theoretical Computer Science Research Group
DOI

Downloads

BibTex