On the computational complexity of the verification of modular discrete-event systems

Kurt Rohloff, Stéphane Lafortune

Research output: Contribution to journalArticlepeer-review

18 Scopus citations


This paper investigates issues related to the computational complexity of automata intersection problems. For several classes of problems, comparing the behavior of sets of interacting finite automata is found to be PSPACE-complete, even in the case of automata accepting prefix-closed languages (equivalently, even when all states are marked). This paper uses these results to investigate the computational complexity of problems related to the verification of supervisory controllers for modular discrete-event systems. Modular discrete-event systems are sets of finite automata combined by the parallel composition operation. We find that a large number of modular discrete-event system verification problems are also PSPACE-complete, even for prefix-closed cases. These results suggest that while system decomposition by parallel composition could lead to significant space savings, it may not lead to sufficient time savings that would aid in the study of “large scale" systems.

Original languageEnglish (US)
Pages (from-to)16-21
Number of pages6
JournalProceedings of the IEEE Conference on Decision and Control
StatePublished - 2002
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Control and Systems Engineering
  • Modeling and Simulation
  • Control and Optimization


Dive into the research topics of 'On the computational complexity of the verification of modular discrete-event systems'. Together they form a unique fingerprint.

Cite this