Version:
[release notes]

Module 4.3: Synthesis with requirements

In the third module, we discussed the supervisory controller synthesis algorithm. But, it did not yet take user-specified requirements into account. Now, we adapt the algorithm to also consider such requirements.

The difference between plant and requirement automata is how they are handled during synthesis. A plant automaton may specify that a certain event is not possible in a certain location. This is taken as a given by the synthesis algorithm. A requirement automaton may also limit certain events in certain locations. However, the effect of doing so differs between controllable and uncontrollable events. A supervisor may only disable controllable events, but not uncontrollable ones that are possible in the plant. Hence, if a requirement automaton disables a controllable event, the supervisor will simply take this into account as a restriction. But, if a requirement automaton disables an uncontrollable event that is possible in the plant, then synthesis must prevent getting into that state, to ensure the controllability guarantee of synthesis.

Dealing with requirements during synthesis

State requirement invariants are taken into account during synthesis by marking any states that do not adhere to the requirement as bad states. The steps of the synthesis algorithm will then ensure these bad states can't be reached, regardless of whether they could be reached in the plant through controllable or uncontrollable events.

State/event exclusion requirement invariants for controllable events can be taken into account by simply disabling the events in the relevant states. That is, for a disables requirement, the states that satisfy the condition, and for a needs requirement, the states that don't satisfy the condition. State/event exclusion requirement invariants for controllable events can be handled in a similar way, but additionally, the source states of these transitions must be marked as bad states, to ensure that the controllability guarantee still holds.

To deal with a requirement automaton during synthesis, it is first converted to a plant automaton and some state/event exclusion requirements. That is, the requirement automata is rebranded as a plant automaton. And all restrictions are moved to state/event exclusion requirements. The rebranded requirement then by itself is a non-restrictive plant automaton, that does not prevent any behavior. As an example, consider again the railway crossing example from earlier in this module, with the following state space:

We defined the following requirement automaton, to ensure the correct order of events in the system:

If we plantify this requirement automaton, we get the following plant automaton:

Note how the events that are disabled by the requirement are re-added as self-loops, to ensure they are no longer blocked by this plant automaton.

The following state/event exclusion requirement invariants are then added, to replace the restrictions of the original requirement automaton:

  • OffOpen disables close
  • OnOpen disables turn_off
  • OnClosed disables open
  • OffClosed disables turn_on

The plantified requirement automaton is then taking into account during synthesis like any plant automaton. And the newly added state/event exclusion requirement invariants are taken into account like any state/event exclusion requirement invariant.

In general, plantification can be slightly more complex. If in a location of a requirement automaton, an edge for an event has a guard, the self loop gets the negated guard. For instance, if an edge has guard x > 0, then the self loop would get guard not (x > 0), which is the same as x <= 0. And if there are multiple outgoing edges for the same event, the self loop gets a guard that indicates that none of the guards of the original edges is satisfied. That is, the self loop gets a guard that is only enabled if none of the other edges is enabled. For instance, if there are two edges with guards x > 0 and x < 0, the self loop would get guard (not x > 0) and (not x < 0), which is the same as x = 0. An added self loop has no updates, and therefore just ensures that the event is not disabled by the plantified requirement automaton.

The updated synthesis algorithm

The synthesis algorithm still takes the uncontrolled plant as input, but now additionally gets requirements as well. It then performs the following steps:

  1. Plantify the requirement automata to plant automata and state/event exclusion requirement invariants.
  2. Determine all states where state requirement invariants don't hold. Mark them as bad states and remove them.
  3. Disable all transitions for controllable events in states where they violate a state/event exclusion requirement invariant.
  4. Disable all transitions for uncontrollable events in states where they violate a state/event exclusion requirement invariant. Additionally, mark their source states as bad states and remove them.
  1. Determine all blocking states. Mark them as bad states and remove them.
  2. Determine all non-controllable states, the states from which an uncontrollable-event transition is possible to a bad state. Mark them as bad states and remove them.
  3. Optionally, determine all unreachable states. Mark them as bad states and remove them.
  4. Disable all transitions for controllable events in states where they lead to a bad state.
  5. If any of the previous steps led to removing any states or disabling any transitions, repeat the steps again, starting from step 5.

The first four steps are preparation steps that are only performed once. The remaining steps are repeated as often as is necessary, until no more behavior is removed.

Quiz

[ { type: 'single-choice', question: "How are state requirement invariants taken into account during synthesis?", answers: [ "They are converted to state/event exclusion requirement invariants and taken into accounts as such.", "They are converted to requirement automata and taken into account as such.", "They are taken into account by removing transitions and marking additional bad states.", "They are taken into account by marking additional bad states.", ], correctAnswer: '4' }, { type: 'single-choice', question: "How are state/event exclusion requirement invariants taken into account during synthesis?", answers: [ "They are converted to state/event exclusion requirement invariants and taken into accounts as such.", "They are converted to requirement automata and taken into account as such.", "They are taken into account by removing transitions and marking additional bad states.", "They are taken into account by marking additional bad states.", ], correctAnswer: '3' }, { type: 'single-choice', question: "How are requirement automata taken into account during synthesis?", answers: [ "They are converted to plant automata and state/event exclusion requirement invariants and taken into accounts as such.", "They are converted to plant automata and state requirement invariants and taken into accounts as such.", "They are taken into account by removing transitions and marking additional bad states.", "They are taken into account by marking additional bad states.", ], correctAnswer: '1' }, { type: 'single-choice', question: "Why would happen if physical relations between a sensor an actuator are accidentally modeled as a requirement automaton rather than a plant automaton?", answers: [ "That is fine, as it is up to the modeler to decide whether it is a plant for a requirement.", "That is fine, as synthesis will correct for this and ensure the controlled system still works as desired.", "This would lead to an undesired controlled system, as the requirement then disables uncontrollable events.", ], correctAnswer: '3' } ]
Go back to Module 4.2
|
Proceed to Module 4.4