Compositional supervisor synthesis with state merging and transition removal

This working paper proposes a framework to obtain memory-efficient supervisors for large discrete event systems, which are least restrictive, controllable, and nonblocking. The approach combines compositional synthesis and state-based abstraction with transition removal to mitigate the state-space explosion problem and reduce the memory requirements. Hiding and nondeterminism after abstraction are also supported. To ensure least restrictiveness after transition removal, the synthesised supervisor has the form of cascaded maps representing the safe states. These maps have lower space complexity than previous automata-based supervisors. The algorithm has been implemented in the DES software tool Supremica and applied to compute supervisors for several large industrial models. The results show that supervisor maps can be computed efficiently and in many cases require less memory than automata-based supervisors