Opacity of Hierarchical Discrete-event Systems

Considering the opaque problem of discrete event systems (DESs), we propose a method to verify the opacity of DESs with a hierarchical structure. First, we formalize hierarchical DESs, and then introduce two concepts of the hierarchical DES:opacity and K-delay opacity. To verify the opacity of systems, we propose two respective corresponding verifiers, obtain the necessary and sufficient conditions for opacity and K-delay opacity, and then analyze the complexity of constructing an opacity verifier.