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

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F22%3A00564912" target="_blank" >RIV/67985840:_____/22:00564912 - isvavai.cz</a>

Nalezeny alternativní kódy

RIV/61989592:15310/22:73614732

Výsledek na webu

<a href="https://doi.org/10.1016/j.ifacol.2022.10.331" target="_blank" >https://doi.org/10.1016/j.ifacol.2022.10.331</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1016/j.ifacol.2022.10.331" target="_blank" >10.1016/j.ifacol.2022.10.331</a>

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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

Název v anglickém jazyce

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

Popis výsledku anglicky

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

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

20205 - Automation and control systems

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2022

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

IFAC-PapersOnLine. Volume 55, Issue 28 - Proceedings of 16th IFAC Workshop on Discrete Event Systems WODES 2022

ISBN

—

ISSN

2405-8963

e-ISSN

—

Počet stran výsledku

6

Strana od-do

108-113

Název nakladatele

Elsevier

Místo vydání

Amsterdam

Místo konání akce

Prague

Datum konání akce

7. 9. 2022

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000877003700016