The TTM for pusher i in the Two-Pusher Example (see Figure
11) consists of 
where the set of variables is 
, and 
represents the position of pusher i; the initial condition is
; and the transition set 
is
described in the table below.
Figure 11: Timed Transition Model for Pusher i
The uncontrolled plant model P consists of 
where 
= 
, 
, t,
n 
, 
, and 
. Notice that
there are no shared transitions.
The description of Specifications I in Temporal Logic is as
follows:
(i) 
(ii) 
.
We now illustrate Ostroff's synthesis procedure for the safety
controller given requirement (i):
First, we start with 
. We clearly have
that
, so the initial state is a safe one.
Now, the ``prebad'' states are 
, with
corresponding ``unsafe'' transition 
, and 
, with corresponding ``unsafe'' transition 
.
We try to make y1 safe by one of the following strategies: (i)
change its enabling condition, if possible, from 
to
; or, (ii) force the
occurrence of a safe transition prior to the occurrence of , for
example, by making sure that 
. A similar step
would be done for the ``unsafe'' transition .