A Compositional Approach for Verifying Hierarchical Interface-Based Supervisory Control

Hierarchical Interface-based Supervisory Control (HISC) decomposes a discrete-event system into a high-level subsystem which communicates through interfaces with several low-level subsystems. The framework provides a set of local conditions that can be checked for each subsystem individually to conclude global conditions such as nonblocking and controllability. The size of HISC systems that can be verified automatically is primarily limited by the size of the largest subsystem. To overcome this limitation, this paper proposes the use of compositional verification. Most of the HISC conditions can be verified efficiently using existing methods for compositional verification, but a few are more challenging. This paper shows how these more challenging conditions can be expressed equivalently as generalized nonblocking problems, so the compositional approach for generalized nonblocking developed by the authors in (Malik and Leduc, 2009) is applicable. This makes all the HISC conditions amenable for compositional verification, considerably increasing the size of systems that can be handled using the framework.