Efficient Validation of Supervisory Controllers using Symmetry Reduction

Supervisory control synthesis is a method to automatically generate a correct-by-construction supervisory controller. Validation of the synthesized controller is an important step to guarantee correct and safe system behavior. Especially requirement validation for systems with numerous components can be a difficult and time-consuming task. This paper proposes a method that reduces the required validation time and eort of systems through symmetry reduction, and is based on the concept of isomorphism. Isomorphism of component models and requirement models means that these models are equivalent in behavior, and therefore only part of the system needs to be validated. This method is used in an industrial case study, in which a supervisory controller is synthesized for a road tunnel (the Koning Willem-Alexandertunnel, the Netherlands). In this case study, the modeling of the plant and the requirements, supervisor synthesis, simulation, and validation are described.