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

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). The 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.