On Verification of Weak and Strong k-Step Opacity for Discrete-Event Systems

Abstract

Opacity is an important property asking whether a passive observer (an intruder), who knows the structure of the system but has only a limited observation of its behavior, may reveal the secret of the system. Several notions of opacity have been studied 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 to verify weak k-step opacity, the complexity of which is lower than that of existing algorithms and that does not depend on the parameter k. Then, we show how to use this algorithm to verify strong k-step opacity by reducing the verification of strong k-step opacity to the verification of weak k-step opacity. The complexity of the resulting approach is again better than that of existing algorithms, and does not depend on the parameter k.

Projects

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

Compositional Methods for the Control of Concurrent Timed Discrete-Event Systems

Jan Komenda, Jörg Raisch
Tomáš Masopust, Thomas Moor

Links

Link

Authors

Jiří Balun
Tomáš Masopust

IFAC PapersOnLine 55(28), 108-113, 2022
Discrete-Event Systems and Theoretical Computer Science Research Group
DOI

Downloads

BibTex