Local Opacity Verification for Distributed Discrete Event Systems

TL;DR

This paper introduces efficient methods for verifying current-state and initial-state opacity in distributed discrete event systems by leveraging local system properties and observer automata, reducing the complexity of global verification.

Contribution

It proposes sufficient conditions and approaches for opacity verification that depend solely on local system analysis, simplifying the process for distributed systems.

Findings

Sufficient conditions for global opacity based on local opacity.

Verification methods relying on local observer automata.

Efficient approach reduces computational complexity.

Abstract

This paper studies current-state opacity and initial-state opacity verification of distributed discrete event systems. The distributed system's global model is the parallel composition of multiple local systems: each of which represents a component. We propose sufficient conditions for verifying opacity of the global system model based only on the opacity of the local systems. We also present efficient approaches for the opacity verification problem that only rely on the intruder's observer automata of the local systems.