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