On verification of weak and strong k-step opacity for discrete-event systems

0564912 - MÚ 2023 RIV NL eng C - Konferenční příspěvek (zahraniční konf.)
Balun, J. - Masopust, Tomáš
On verification of weak and strong k-step opacity for discrete-event systems.
IFAC-PapersOnLine. Volume 55, Issue 28 - Proceedings of 16th IFAC Workshop on Discrete Event Systems WODES 2022. Amsterdam: Elsevier, 2022 - (Komenda, J.; Reveliotis, S.; Masopust, T.; Burget, P.), s. 108-113. ISSN 2405-8963.
[16th IFAC Workshop on Discrete Event Systems WODES 2022. Prague (CZ), 07.09.2022-08.09.2022]
Grant CEP: GA ČR(CZ) GC19-06175J
Institucionální podpora: RVO:67985840
Klíčová slova: discrete event systems * finite automata * opacity * verification * complexity
Obor OECD: Automation and control systems
https://doi.org/10.1016/j.ifacol.2022.10.331

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.


Trvalý link: https://hdl.handle.net/11104/0336489