Verification complexity of a class of observational properties for modular discrete events systems

A modular discrete event system is modeled by a set of module automata running synchronously. In this paper, we investigate the complexity of the verification problems of three different properties, diagnosability, predictability, and detectability, for partially-observed modular discrete event systems. We first show that deciding diagnosability for modular discrete event systems is PSPACE-complete when the number of modules is unbounded. Then we show that deciding predictability and detectability for modular discrete event systems are both PSPACE-hard problems. These results reveal that in order to verify these properties for the complete system, exploring the state space of the monolithic model may be unavoidable, in the worst case.