Symbolic Synthesis and Verification of Hierarchical Interface-based Supervisory Control

Hierarchical Interface-based Supervisory Control (HISC) decomposes a discrete-event system (DES) into a high-level subsystem which communicates with $n\geq 1$ low-level subsystems, through separate interfaces which restrict the interaction of the subsystems. It provides a set of local conditions that can be used to verify global conditions such as nonblocking and controllability. The current HISC verification and synthesis algorithms are based …