Reachability requirement annotations

CIF supports marker predicates that allow to specify marked states. Supervisory controller synthesis then ensures that from every state in the controlled system, a marked state can always be reached. Marking serves as a means to specify a form of liveness requirements. However, marking is a very weak for of liveness; in every state only a single marked state needs to be reachable. In many cases, you may want to express stronger liveness requirements. You can use reachability requirements for this.

Marking is not always sufficient

To show why marking alone is not always sufficient, consider a bridge that may be open or closed, modeled as an automaton with two locations:

plant bridge:
  controllable c_open, c_closed;

  location open:
    initial;
    marked;
    edge c_close goto closed;

  location closed:
    edge c_open goto open;
end

We could mark the location where the bridge is open, to ensure it can always be opened. However, then synthesis could determine that it needs to forbid closing the bridge (event c_close), for instance due to some other requirement that we wrote. The automaton would then remain in its marked open location. The supervisor would not be empty, so you may assume you got the desired supervisor. You could find the problem that the bridge is always open and can never close by means of simulation. However, for large models with many possible simulation scenarios, such problems could be hard to find, especially if they concern behaviors that do not occur very often.

Alternatively, we could mark the location where the bridge is closed. However, then synthesis could similarly decide it needs to forbid opening the bridge.

Yet another alternative would be to mark both locations. However, synthesis then only needs to ensure that one of those locations can always be reached. It could still block either opening or closing the bridge.

Reachability requirements

What we want for this model, is that you can always open the bridge, but also always close the bridge. Both must always be possible. You can specify that using reachability requirements, as follows:

@requirement:reachable(open)
@requirement:reachable(closed)
plant bridge:
  controllable c_open, c_closed;

  location open:
    initial;
    marked;
    edge c_close goto closed;

  location closed:
    edge c_open goto open;
end

The plant automaton now has two reachability requirements. The first requirement indicates that a state where open is the current location of bridge must always be reachable. The second requirement indicates that a state where closed is the current location of bridge must always be reachable.

Together these two requirements will ensure that the bridge can always be opened and always be closed. That is, synthesis will ensure that for every state in the controlled system, it is possible to reach a state where open holds and it is possible to reach a state where closed holds. If that is somehow not possible, for instance due to other parts of the specification, such as conflicting requirements, then synthesis results in an 'empty supervisor' error.

Reachability requirements may be specified in specifications, on components (automata and groups), on component definitions and on component instantiations. This allows to specify them as locally as possible. This makes it easier to see to what part of the specification they relate. It also makes it easier to specify them, as the variables, locations, and so on, of the local scope can be referred to directly. Consider for instance the following alternative to the specification above, where the reachability requirements are now specified in the root of the specification, rather than on the automaton:

@@requirement:reachable(system.bridge.open)
@@requirement:reachable(system.bridge.closed)

group system:
  plant bridge:
    controllable c_open, c_closed;

    location open:
      initial;
      marked;
      edge c_close goto closed;

    location closed:
      edge c_open goto open;
  end
end

In general, each reachability requirement specifies a predicate, such as open or closed in the example above. Synthesis then ensures that every state in the controlled system can always reach a state that satisfies that predicate.

Marking vs reachability requirements

Reachability requirements are very similar to marking. Synthesis will ensure that from every state in the controlled system, always a marked state can be reached. Similarly, synthesis will ensure that from every state in the controlled system, for each reachability requirement, always a state can be reached that satisfies the reachability requirement. In fact, in the example above, the reachability requirement @requirement:reachable(open) is superfluous, as it is already ensured by marking.

There are a few key difference between marking and reachability requirements. The first is that you can specify as many reachability requirements as you want, and that they each indicate an independent set of states from which at least one must always be reachable, while for marking there is only one such set of states.

The second is that marking needs to be ensured globally. A specification is marked if each automaton is marked, and an automaton is marked if its current location is marked. Marking must thus be considered for every automaton. Reachability requirements can be specified locally for a single automaton, without having to think about any of the other automata. The combination of marking and reachability requirements allows you to benefit from the guarantees of global completeness as well as the ease of local specification.

Note that marking is mandatory for supervisory controller synthesis, as without marking you will always get an empty supervisor. Reachability requirements on the other hand are optional.

For more detailed information on reachability requirement annotations, see the reference manual.