文章基本信息

标题：On Opacity Verification for Discrete-Event Systems ⁎
本地全文：下载
作者：Jiří Balun ; Tomáš Masopust
期刊名称：IFAC PapersOnLine
印刷版ISSN：2405-8963
出版年度：2020
卷号：53
期号：2
页码：2075-2080
DOI：10.1016/j.ifacol.2020.12.2524
语种：English
出版社：Elsevier
摘要：AbstractOpacity is an information flow property characterizing whether a system reveals its secret to an intruder. Verification of opacity for discrete-event systems modeled by automata is in general a hard problem. We discuss the question whether there are structural restrictions on the system models for which the opacity verification is tractable. We consider two kinds of automata models: (i) acyclic automata, and (ii) automata where all cycles are only in the form of self-loops. In some sense, these models are the simplest models of (deadlock-free) systems. Although the expressivity of such systems is weaker than the expressivity of linear temporal logic, we show that the opacity verification for these systems is still hard.
关键词：KeywordsDiscrete event systemsfinite automataopacitycomplexity