PSPACE-completeness of modular supervisory control problems

In this paper we investigate computational issues associated with the supervision of concurrent processes modeled as modular discrete-event systems. Here, modular discrete-event systems are sets of deterministic finite-state automata whose interaction is modeled by the parallel composition operation. Even with such a simple model process model, we show that in general many problems related to the supervision of these systems are PSPACE-complete. This shows that although there may be space-efficient methods for avoiding the state-explosion problem inherent to concurrent processes, there are most likely no time-efficient solutions that would aid in the study of such "large-scale" systems. We show our results using a reduction from a special class of automata intersection problem introduced here where behavior is assumed to be prefix-closed. We find that deciding if there exists a supervisor for a modular system to achieve a global specification is PSPACE-complete. We also show many verification problems for system supervision are PSPACE-complete, even for prefix-closed cases. Supervisor admissibility and online supervision operations are also discussed.