Current-state opacity and initial-state opacity of modular discrete event systems

The verifications of current-state opacity (CSO) and initial-state opacity (ISO) in discrete event systems (DESs) both suffer from the curse of dimensionality, as these issues were proved to be PSPACE-complete. Hence, how to reduce the state space is crucial. In this paper, we investigate CSO and ISO in modular DESs, which consist of several individual components. Necessary and sufficient conditions of CSO and ISO for modular DESs are derived under the assumption that all synchronous events are observable by each components of modular DESs. Moreover, we prove that the initial state estimator of modular system is isomorphic to the synchronous composition of initial state estimators for individual components. These results offer us the opportunity to reduce the complexity in verifying the opacity of modular DESs.