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 form 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_close;

  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_close;

  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_close;

    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 goal predicate, such as open or closed in the example above. For the requirements in this example, synthesis ensures that every state in the controlled system can reach a state that satisfies that predicate.

A reachability requirement that only specifies a goal predicate is called a basic reachability requirement. It can be extended with various additional arguments as explained below.

Both basic and extended reachability requirements ensure that a path to the goal remains available wherever the requirement applies, subject to any restrictions specified by its arguments. They do not enforce that such a path is actually taken.

Marking vs basic reachability requirements

Basic 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, for a basic reachability requirement, synthesis will ensure that from every state in the controlled system a state can always be reached that satisfies the requirement’s goal predicate. In the bridge example above, the basic reachability requirement @requirement:reachable(open) is superfluous, as it is already ensured by marking.

There are a few key differences between marking and basic reachability requirements. The first is that you can specify as many basic reachability requirements as you want, and that each defines an independent set of goal states, at least one of which must be reachable from every state in the controlled system. 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. Basic 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 basic 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. Basic reachability requirements on the other hand are optional.

Conditional reachability with from

The optional from argument defines conditional reachability. It restricts the source states to which the requirement applies:

@requirement:reachable(closed, from: open)

This requirement only requires states where open holds to be able to reach a state where closed holds. States that do not satisfy open are not affected by this requirement.

On its own, the requirement does not ensure that any open state remains reachable in the controlled system. For example, if the bridge is initially closed and no other requirement demands that it can open, synthesis could prevent it from opening, leaving no source states to which this requirement applies. If opening must also remain possible, the basic reachability requirement @requirement:reachable(open) can be added. This ensures that from every state in the controlled system, at least one state where open holds remains reachable.

Restricted reachability with avoid or stay

The optional avoid and stay arguments define restricted reachability by limiting the states that may occur on the path to the goal. They also determine the states to which the requirement applies.

The annotation @requirement:reachable(goal, avoid: avoid_pred) requires reaching goal without visiting states that satisfy avoid_pred. The avoid states are not allowed to occur anywhere along the path to the goal, including the starting and goal states. States that already satisfy avoid_pred are not affected by this reachability requirement.

The annotation @requirement:reachable(goal, stay: stay_pred) requires reaching goal while staying in states that satisfy stay_pred. For states to which the requirement applies, this means every state on the path to the goal, including the starting and goal states, must satisfy stay_pred. States that already do not satisfy stay_pred are not affected by this reachability requirement.

The avoid and stay arguments express the same kind of path restriction in inverse forms: avoid: pred is equivalent to stay: not pred, and stay: pred is equivalent to avoid: not pred. The arguments are mutually exclusive, so use the form that best describes the intended behavior and avoids unnecessary logical negations.

The following annotations illustrate restrictions on paths for opening and closing a bridge:

@requirement:reachable(open, avoid: maintenance)
@requirement:reachable(closed, stay: operational)
@requirement:reachable(closed, from: open, stay: operational)
plant bridge:
  ...
end

The first requirement indicates that open must remain reachable from states outside maintenance, without visiting a maintenance state. The second one indicates that closed must remain reachable from operational states along a path of operational states. The third one combines conditional and restricted reachability: from states satisfying both open and operational, closed must remain reachable along an operational path.

Bounded reachability with bound

The optional bound argument defines bounded reachability by limiting the maximum number of transitions on the path to the goal:

@requirement:reachable(closed, bound: 3)
@requirement:reachable(open, from: closed, bound: 2)
@requirement:reachable(open, from: closed, stay: operational, bound: 2)
plant bridge:
  ...
end

The first requirement requires the goal to be reachable in at most three transitions from every state in the controlled system. The second requirement combines conditional and bounded reachability, so only states satisfying closed must be able to reach open within two transitions. The third also specifies stay: operational, so states satisfying both closed and operational must be able to reach open within two transitions along operational states. Conditional, restricted and bounded reachability can be combined in this way.

For bound: 0, a state satisfies the requirement only if it already satisfies the goal predicate, unless it is not affected by the requirement due to a from, avoid or stay argument.

The bound counts discrete transitions, not elapsed time. Choosing a bound that is too small may disable behavior or result in an empty supervisor. For guidance on choosing reachability requirements and bounds, see modeling reachability requirements in practice.

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