The Effects of Modeling Choices on Supervisory Controller Synthesis Performance: A Case Study

Supervisory controllers are crucial for industrial cyber-physical systems to ensure their safe and efficient operations. Correct-by-construction supervisory controllers can automatically be generated from requirements using supervisory controller synthesis. Whilst formal synthesis techniques are well-established, their applications in real-world systems often suffer from scalability challenges. Rather than improving the synthesis algorithms and underlying data structures, this paper investigates how choices in modeling constructs affect synthesis performance. We propose a structured approach to identify
modeling patterns that significantly hinder synthesis efficiency, analyze the cause of such bottlenecks, and resolve them in a generic manner to also benefit other practitioners. Drawing upon a collection of industrial models developed at ASML, we apply the approach to resolve two such bottlenecks, gaining remarkable improvements in synthesis time. By making our improvements available in the open-source Eclipse ESCET toolkit, these results directly benefit practitioners, further bridging the gap between theoretical synthesis and industrial development. Finally, our work shows that small changes in modeling can
lead to significant differences in synthesis performance, and that there is still much to be gained by further investigations into synthesis performance bottlenecks, not just from an algorithmic perspective, but also from a modeling perspective.