Current-State Opacity Verification in Modular Discrete Event Systems

In this paper we address the opacity verification problem in modular discrete event systems. We assume that the system is composed by several components that are modeled by deterministic finite automata and there is one intruder. The notion of current-state opacity in modular systems is defined. Rather than constructing the modular system through parallel composition and its observer, we show that current-state opacity of modular systems can be locally determined, i.e., determined by opacity of its components.