Data-based supervisory controller synthesis
The data-based supervisory controller synthesis tool performs data-based supervisory controller synthesis, or simply data-based synthesis. It can be used to synthesize a supervisor for an untimed CIF specification, with data (e.g. discrete variables). Synthesis is an essential part of the synthesis-based engineering approach to develop supervisory controllers.
For a CIF specification with plants and requirements, the tool computes a supervisor. The supervisor restricts the plants in such a way that the resulting controlled system satisfies the following properties:
-
The controlled system is safe. That is, all reachable states in the controlled system satisfy the requirements.
-
The controlled system is controllable. That is, for all reachable states in the controlled system, the uncontrollable events that are enabled in the same state in the uncontrolled system are still possible in the controlled system. In other words, uncontrollable events are not restricted.
-
The controlled system is non-blocking. That is, it is possible to reach a marked state from all reachable states in the controlled system.
-
The controlled system is maximally permissive (or simply maximal). That is, the controlled system permits all safe, controllable, and non-blocking behaviors.
Note that deadlock is not prevented for marked states, nor for states that satisfy reachability requirements.
The synthesis algorithm is based on [Ouedraogo et al. (2011)] and explained in quite some detail in [Hendriks et al. (2025)].
The following additional information is available: