On opacity verification for discrete-event systems

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F20%3A00537812" target="_blank" >RIV/67985840:_____/20:00537812 - isvavai.cz</a>

Nalezeny alternativní kódy

RIV/61989592:15310/21:73602451

Výsledek na webu

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

DOI - Digital Object Identifier

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

Jazyk výsledku

angličtina

Název v původním jazyce

On opacity verification for discrete-event systems

Popis výsledku v původním jazyce

Opacity is an information flow property characterizing whether a system reveals its secretto an intruder. Verification of opacity for discrete-event systems modeled by automata is in general ahard problem. We discuss the question whether there are structural restrictions on the system modelsfor which the opacity verification is tractable. We consider two kinds of automata models: (i) acyclicautomata, and (ii) automata where all cycles are only in the form of self-loops. In some sense, thesemodels are the simplest models of (deadlock-free) systems. Although the expressivity of such systemsis weaker than the expressivity of linear temporal logic, we show that the opacity verification for thesesystems is still hard.

Název v anglickém jazyce

On opacity verification for discrete-event systems

Popis výsledku anglicky

Opacity is an information flow property characterizing whether a system reveals its secretto an intruder. Verification of opacity for discrete-event systems modeled by automata is in general ahard problem. We discuss the question whether there are structural restrictions on the system modelsfor which the opacity verification is tractable. We consider two kinds of automata models: (i) acyclicautomata, and (ii) automata where all cycles are only in the form of self-loops. In some sense, thesemodels are the simplest models of (deadlock-free) systems. Although the expressivity of such systemsis weaker than the expressivity of linear temporal logic, we show that the opacity verification for thesesystems is still hard.

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í

2020

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 53, Issue 2 - 21st IFAC World Congress on Automatic Control - Meeting Societal Challenges

ISBN

—

ISSN

2405-8963

e-ISSN

—

Počet stran výsledku

6

Strana od-do

2075-2080

Název nakladatele

Elsevier

Místo vydání

Amsterdam

Místo konání akce

Berlin

Datum konání akce

11. 7. 2020

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

WRD - Celosvětová akce

Kód UT WoS článku

000652592500335