Complexity of Detectability, Opacity and A-Diagnosability for Modular Discrete Event Systems
This work provides complexity bounds for key verification problems in modular discrete event systems, which are important for state estimation, privacy, and fault diagnosis.
The paper studies the complexity of deciding weak detectability, opacity, and A-diagnosability for modular discrete event systems, proving that these problems are EXPSPACE-complete, which is worse than the PSPACE-complete complexity for monolithic systems.
We study the complexity of deciding whether a modular discrete event system is detectable (resp. opaque, A-diagnosable). Detectability arises in the state estimation of discrete event systems, opacity is related to the privacy and security analysis, and A-diagnosability appears in the fault diagnosis of stochastic discrete event systems. Previously, deciding weak detectability (opacity, A-diagnosability) for monolithic systems was shown to be PSPACE-complete. In this paper, we study the complexity of deciding weak detectability (opacity, A-diagnosability) for modular systems. We show that the complexities of these problems are significantly worse than in the monolithic case. Namely, we show that deciding modular weak detectability (opacity, A-diagnosability) is EXPSPACE-complete. We further discuss a special case where all unobservable events are private, and show that in this case the problems are PSPACE-complete. Consequently, if the systems are all fully observable, then deciding weak detectability (opacity) for modular systems is PSPACE-complete.