On Opacity Verification for Discrete-Event Systems

Abstract

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

Projects

Verification and Control of Networked Discrete Event Systems

Tomáš Masopust, Jan Komenda
Jiří Balun, Stéphane Lafortune, Spyros Reveliotis, Feng Lin

Authors

Jiří Balun
Tomáš Masopust

IFAC World Congress, IFAC-PapersOnLine 53(2), 2020
Discrete-Event Systems and Theoretical Computer Science Research Group
DOI

Downloads

BibTex