## Supervisory controller synthesis

Supervisory controller synthesis (or supervisor synthesis, or just synthesis) is a generative technique, where one derives a supervisory controller from a collection of plants and requirements. Synthesis is the main ingredient of the synthesis-based engineering approach to develop supervisory controllers. Synthesis allows to focus on the what, i.e. which requirements should hold, rather than on the how, i.e. how to implement this in a controller.

The plants describe capabilities or behavior of a physical system 'as is', without any integrated control. They represent the available behavior of the uncontrolled system. Requirements model (a part of) the functions a system is supposed to perform. They represents behavior that is allowed in the controlled system, or more precisely, they specify the behavior that is not allowed in the controlled system. In other words, requirements restrict the behavior of the plants, to ensure that only the desired behavior remains. The goal of supervisory controller synthesis is to compute a supervisory controller (or supervisor) that enforces the requirements, assuming the behavior of the plants, additionally preventing deadlock and livelock, and without restricting the system any further than is required.

CIF has several features that are used solely of modeling systems for the purpose of supervisory controller synthesis. These concepts are explained in upcoming lessons:

- Automaton kinds

- Invariant kinds

- Event controllability

- Marker predicates

- Reachability requirement annotations (as part of the 'annotations' lessons category)

When a model is not used for supervisory controller synthesis, e.g. for simulation, these concepts are usually ignored.

For an example of how these concepts can be used for modeling of a concrete example, see the synthesis-based engineering in practice example section.