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 below. 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.

Automaton kinds

For supervisory controller synthesis, different kinds of automata are treated in different ways. Regular automata, as used in the language tutorial so far, are specified using only the automaton keyword. Regular automata do not specify a kind for supervisory controller synthesis, and are therefore sometimes also referred to as kindless automata. Synthesis tools typically require knowledge about the purpose of each of the automata, and therefore don’t support regular automata.

For supervisory controller synthesis, three different kinds of automata are available: plant automata, requirement automata, and supervisor automata. These automata are identical to regular automata, except for the keywords used to declare their intent. The automaton keyword is preceded or replaced by the plant, requirement, or supervisor keyword respectively.

For instance, the following are two alternative ways to model the same plant automaton:

// Plant automaton, long form.
plant automaton lamp:
  event turn_on, turn_off;

  location off:
    initial;
    edge turn_on goto on;

  location on:
    edge turn_off goto off;
end

// Plant automaton, short form.
plant lamp:
  event turn_on, turn_off;

  location off:
    initial;
    edge turn_on goto on;

  location on:
    edge turn_off goto off;
end

Invariant kinds

Similar to automata, different kinds of invariants are treated in different ways for supervisory controller synthesis. Invariants can be declared as plant, requirement, or supervisor invariants, by preceding or replacing the invariant keyword with a plant, requirement, or supervisor keyword respectively.

For instance, consider the following CIF specification:

invariant inv1: lamp.on or lamp.off;      // Regular/kindless invariant.

plant lamp:
  event turn_on, turn_off;

  requirement invariant req1: not off;    // Requirement invariant. Long form.
  requirement req2: not off;              // Requirement invariant. Short form.

  location off:
    initial;
    edge turn_on goto on;

  location on:
    edge turn_off goto off;
end

The inv1 invariant, does not specify an additional supervisory kind keyword. It is therefore a regular invariant, also called a kindless invariant. The req1 invariant, in the lamp automaton, explicitly specifies a requirement kind and is therefore a requirement invariant. The req2 invariant is identical to the req1 invariant, except that the invariant keyword has been omitted. It is also a requirement invariant, but written in a shorter form.

There are two forms of invariants: state invariants and state/event exclusion invariants. Both forms can be used for synthesis. For instance, consider the following example of a counter:

plant counter:
  controllable increment, decrement;
  disc int x = 0;

  plant invariant 0 <= x and x <= 10;

  requirement increment needs x < 8;

  location:
    initial;
    edge increment do x := x + 1;
    edge decrement do x := x - 1;
end

The counter can be incremented and decremented. The plant invariant specifies that it is not possible for the counter to count negative values, or values more than 10. It is a requirement that synthesis ensures that the counter can only be incremented as long as the counted value is less than 8.

Event controllability

Supervisory controller synthesis distinguishes two kinds of events: controllable events and uncontrollable events.

Uncontrollable events are events that a supervisor can not prohibit, and are usually related to sensors. A typical example are events that indicate that a button has been pushed or released. A button is essentially a sensor that is on if the user pushes the button, and off if the user doesn’t push it. The supervisor can not prevent a user from physically pushing or releasing a button, and can also not determine when the user pushes or releases it. The supervisor thus also can not prevent the events from occurring.

Another example is an event that indicates that a moving part has reached its outer position (limit sensor turns on). If the part reaches its outer position, the event will occur. The supervisor can not control the sensor, as it is physically linked to the position of the moving part.

Controllable events may be restricted by a supervisor, and are usually related to actuators. Typical examples are events used to turn a motor on or off, to turn a lamp on or off, or to change the direction of movement.

Even though a supervisor may not be able to control a limit sensor directly, and thus restrict the corresponding events, it may be able to influence it indirectly. For instance, a motor may be available that makes it possible for the part to move. That motor may then be controlled using controllable on and off events. Stopping the motor then makes the part stop moving, ensuring that the part never reaches its outer position, indirectly preventing the limit sensor from turning on, and the corresponding event from happening.

Events and channels in CIF are declared using the event keyword. For controllable events, the event keyword may be preceded or replaced by the controllable keyword. Similarly, for uncontrollable events, the event keyword may be preceded or replaced by the uncontrollable keyword. Similar to event declarations, for event parameters the event keyword may by preceded or replaced by the controllable or uncontrollable keyword, for controllable and uncontrollable event parameters respectively.

As a convention, controllable events are given names that start with c_, and uncontrollable events are given names that start with u_. This allows them to be highlighted in different colors.

For instance, consider the following CIF specification:

controllable c_on, c_off;
uncontrollable u_pushed, u_released;

Marker predicates

Marking is very weak form of liveness, and is used by supervisory controller synthesis to prevent livelocks, to ensure progress. It is also used to prevent deadlocks. A supervisor per definition ensures that a marked state can always be reached, for the entire system. A system is marked if all its automata are marked. An automaton is marked if its active location is a marked location. In literature, marked location are also called safe locations. Note that deadlock in marked states is not prevented, as a marker state (the state itself) can be reached by not taking any transition. In literature, marked deadlock states are also called final states.

Marking can be specified using marker predicates. Locations can be marked using the marked keyword, as follows:

plant lamp:
  controllable c_turn_on, c_turn_off;

  location off:
    initial;
    marked;
    edge c_turn_on goto on;

  location on:
    edge c_turn_off goto off;
end

In this example location off is both initial and marked, while location on is neither initial nor marked.

Marker predicates are very similar to initialization predicates, as by default, locations are not marked, similar to how by default locations are not initial. Marker predicates can be specified in locations, automata, groups, and the top level of the specification (which can be seen as a group), similar to initialization predicates.

The following specification shows an example of a variable that is only marked for a certain value:

plant counter:
  controllable c_increment, c_decrement;
  disc int[0..10] count = 0;

  marked count = 0;

  location off:
    initial;
    marked;
    edge c_increment do count := count + 1;
    edge c_decrement do count := count - 1;
end

Variable count of plant automaton counter is only marked if it has value zero. That is, the entire system can only be marked if count is zero. Supervisor synthesis will ensure that it is always possible to get back to a state where count is zero.