Verification complexity of a class of observational properties for modular discrete events systems. (September 2017)

• Record Type: Journal Article
• Authors: Yin, Xiang; Lafortune, Stéphane
• Is Part Of: Automatica. Volume 83(2017)
• Page Start: 199
• Page End: 205
• Publication Date: 2017-09
• Subjects: Computational complexity -- PSPACE-completeness -- Modular diagnosis -- Discrete event systems; Automatic control -- Periodicals; Automation -- Periodicals; 629.805
• DOI: 10.1016/j.automatica.2017.06.013
• Languages: English
• ISSNs: 0005-1098

Abstract

Abstract: 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.