On Opacity Verification for Discrete-Event Systems
Formal Languages and Automata Theory
2019-12-17 v1 Systems and Control
Systems and Control
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.
Cite
@article{arxiv.1912.07314,
title = {On Opacity Verification for Discrete-Event Systems},
author = {Jiří Balun and Tomáš Masopust},
journal= {arXiv preprint arXiv:1912.07314},
year = {2019}
}