On Opacity Verification for Discrete-Event Systems

TL;DR

This paper investigates the complexity of verifying opacity in simple discrete-event systems modeled by automata, showing that even restricted models pose computational challenges.

Contribution

It analyzes the tractability of opacity verification under structural restrictions on automata models, specifically acyclic and self-loop-only automata.

Findings

Opacity verification remains hard for acyclic automata.

Opacity verification remains hard for automata with only self-loop cycles.

Simpler models do not necessarily lead to easier opacity verification.

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.