Synthesis of Safety Controller

For a detailed version of the synthesis algorithm, we refer the reader to [6]. The synthesis of safety controllers based on NCES is performed in a way which is very similar to Ostroff's safety controller (described in Section 5.2). The idea of the algorithm is to transform the specification into the controller function by systematically extending Boolean expressions. The procedure is as follows:

1. For each fact , determine the (partial) marking that enables it. Write the Boolean expression in the set of ``enabling places'' of the fact, say , also called ``pre-places.'' This marking is declared to be forbidden by setting .
2. For each place p which is part of this expression and has not been replaced yet, determine the set of transitions which need to fire in order to mark p. A place may become marked if at least one of its input transitions is enabled. For each place p which is contained in the specification expression, we have to replace p by the characteristic function of its predecessor markings/conditions, and the characteristic functions of transitions which would force a transition that would bring a token to p.
3. Stop further substitution of new places in if:
   A term contains places which are part of a place invariant that has less tokens than places are part of them. Such a term will evaluate to zero.
   A term contains an input signal, since the controller can ensure that this signal evaluates to zero.
   We do not find any new transitions which could produce tokens at the places which have not been replaced.
4. Add to the original expression all new expressions from step 2 by OR operation and start again at step 2. After reaching a fixed point, we have a Boolean expression . We separate an expression which has only places from as arguments. describes the extended forbidden markings; i.e., markings from which we cannot avoid through controllable input the enabling of a fact.
5. Check that the initial marking is not part of the extended forbidden marking set. If this were the case, we clearly fail to guarantee safety.

We illustrate the synthesis of the safety controller with the Two-Pusher example in Section 6.4.