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 syst...

Full description

Saved in:
Bibliographic Details
Published in:Automatica (Oxford) 2017-09, Vol.83, p.199-205
Main Authors: Yin, Xiang, Lafortune, Stéphane
Format: Article
Language:English
Subjects:
Computational complexity
Discrete event systems
Modular diagnosis
PSPACE-completeness
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0005-1098
1873-2836
DOI:10.1016/j.automatica.2017.06.013