\chapter{Delayed Response}

In this chapter we consider the delay between the receipt of
information by the controller for vehicle $2$ and its resulting
action. There are two distinct types of delays to consider
--- the inbound and the outbound delay; we model them separately. The
inbound delay is delay due to the controller's sensors getting the
information (about the position and velocity of the leading
vehicle). The outbound delay is the delay between the time the
controller makes the decision and the time the decision is actually
implemented by the vehicle. 

These delays are between the vehicle
and its controller, and so only the delays in the trailing vehicle are
relevant to our analysis, as we only care about the external {\em
  behavior} of the leading vehicle, and not about its controller. In
particular, if we were to extend our analysis to a multi-car case, each
vehicle can have its own delay characteristics; our analysis would
still hold up, if we looked at the delays in the trailing vehicle of
each vehicle pair.

We use levels of abstractions to deal with the complexity of the
delayed case. First, we devise the ``delayed'' controller, and then we
use simulation relations to the controller of the first (ideal) case,
to show that this controller is  sufficient for the
delayed case. We also give a slightly less restrictive controller
specification, and prove that it is necessary to guarantee
correctness, based on necessity of the similar controller in the ideal
case.

\section{Delay Buffers}

We model both the inbound and the outbound delays by special delay
buffers. To obtain the delayed system, we then compose our new
controller with the delay buffers. First, we introduce a generic delay
buffer \atK, and then specify the inbound and outbound delays
as instances of the generic automaton.

\begin{figure}[ht]

\begin{myiotab}
{\bf Parameters:} \+\\
        $n$ --- number of input variables \\
        $S_i$, $S_o$ - two disjoint sets of variable names with $n$
        members in each set \\
        \> Let $V(s)$, where $s$ is a variable name, be a valuation of
        the variable $s$;\\
        \>\>$V(S)$, where $S$ is a set of variables
        names, be a valuation of the entire set. \\
        $var: S_i \rightarrow S_o$, a 1-1 mapping from $S_i$ to $S_o$
        \\
        $d$ --- the delay of the buffer \\
        $Init : (0, d) \rightarrow V(S_o)$ --- a function giving the
        output of the buffer for the initial $d$ time period \-\\ 
{\bf Variables:} \+\\

        Input:\>\>\>      $S_i$ \\

        Output: \>\>\>    $S_o$ \\

        Internal: \>\>\>  $\mathit{saved}: (0, d) \rightarrow V(S_o)$,
        where $saved$ acts as FIFO queue for outputs; \\
        \>initially, $\mathit{saved} = \mathit{Init}$ \-\\

{\bf Trajectories:} \+\\

        an $I$-trajectory $w$ is included among the set of nontrivial trajectories exactly if \+\\
        for all $t \in I$, $t > 0$, the following hold: \+\\

                1. for all variables $v_i \in S_i$, \\  
                $w(t).V(var(v_i))$ = 

                        $\begin{cases}

                        w(0).saved(t) & \text{ if } t < d, \\

                        w(t-d).V(v_i) & \text{ otherwise. }

                        \end{cases}$ \\

                2. $\forall t' \in (0,d)$, \\

                      $w(t).saved(t')$ = 

                        $\begin{cases}

                        w(0).saved(t'-t)& \text{ if } t' > t, \\

                        w(t - t').V(S_i) & \text{ otherwise. } 

                        \end{cases}$ \\

\end{myiotab}

\caption{\atK($n$, $S_i$, $S_o$, $var$, $d$, $Init$) Hybrid Automaton}

\label{fig:d-buffer}

\end{figure}

\begin{automaton}{\aatK($n$, $S_i$, $S_o$, $var$, $d$, $Init$)}
The buffer outputs its inputs (the connection between inputs and outputs given by the
$var$ function) exactly in the same order as received,
and exactly time $d$ later. Initially, it outputs values given by the
$Init$ function. The automaton is described formally in Figure \ref{fig:d-buffer}.

\paragraph{Parameters}
\begin{itemize}
\item
$n$ is the number of (input, output) variable pairs;
\item
$S_i$, $S_o$ are two disjoint sets of input and output variables names, respectively;
\item
$var: S_i \rightarrow S_o$ is a 1-1 mapping from input to output variables. 
Each pair corresponds to a
variable the buffer is ``delaying.'' For convenience, we also define
valuations of single variable names and their sets, by the function $V$.
\item
$d$ is the maximum absolute delay (it is the same for all variables
delayed by this buffer). This delay buffer actually implements the more realistic
setup, in which the duration of the delay varies nondeterministically
within known bounds, with given longest possible delay. 
\item
$Init$ is a function that sets up the initial ``contents'' of the buffer --- it tells the buffer
what to output for the initial $d$ time period, when no inputs have
reached the output yet.
\end{itemize}

\paragraph{Variables}
\begin{itemize}
\item
$S_i$ is a set of input variables, and $S_o$ is a set of output
variables. Both sets are given by the parameters of the automaton.
\item
{\em saved}  is an internal variable that stores the input variables
for the delay duration $d$. Initially, it is prefed with information
using the function {\em Init}. {\em saved} acts as a
First-In-First-Out continuous queue of the buffers inputs. $saved(0^+)$
represents the most recent input, and $saved(d^-)$ represents the
least recent input, the one that going to be output the fastest.
\end{itemize}

\paragraph{Trajectories}
Condition (1) sets up the output variables to take their values
either directly from the inputs, or from the internal variable {\em
  saved} exactly time $d$ ago. Condition (2) updates the {\em saved}
variable with new information.

\paragraph{HA}
Trajectories are not restricted in duration, so axiom $T2$ is
satisfied; also, trajectories are never {\em required} to stop, so
axiom $T3$ is also satisfied. Thus, by discussion in Section \ref{sec:model},
\atsK is clearly an {\em HA}.

\paragraph{Properties}
From the automaton definition, it is clear that
\begin{enumerate}
\item
For the initial $d$ time period, output $w(t).V(S_o) = Init(t)$, from
the initialization of internal variable $saved$, and trajectory
condition (1).
\item
Afterwards, for all $t$, $w(t).V(S_o) = w(t-d).V(S_i)$, from
trajectory conditions (1) and (2).
\end{enumerate}

\end{automaton}

\section{The System with Inbound and Outbound Delays}

We compose the delayed controller from two instances of the delay
buffer \atK, and a modified controller. 

First, we define two instances of the \atsK automaton, the inbound
and outbound delay buffers.

\begin{automaton}{\aatL}
\atsL = \atK(2, $S_i$, $S_o$, $var$, $d_i$, $Init$), where $S_i =
\{x_1, \dot{x}_1\}$, $S_o = \{x_{d1}, \dot{x}_{d1}\}$; $var(x_1) =
x_{d1}$ and $var(\dot{x}_1) = \dot{x}_{d1}$; $d_i$ is the
    ``information'' delay -- the time it takes the controller
    to get the information from the sensors. The inbound delay
automaton delays the position and velocity data of the first vehicle,
with delay $d_i$.

{\em Init} is set up so that the $Init(0)$ matches up with the values
at $w(0)$ of \atA. For the controller to be the optimal (proof of
necessity is given in the Optimality section), we also have to assume
that the leading vehicle was decelerating at the maximum possible rate
throughout the $d_i$ time period. So, {\em Init} assumes vehicle $1$
was decelerating at $a_{min}$ and fills the position and velocity
values accordingly.

%    is set up as follows. For any start state $s$ of the system, construct a trajectory
%$w$ of length $d_i$ of \atsE so that $w(0).\dot{x}_1 = s.\dot{x}_1 +
%    d_i a_{min}$, $w(0).x_1 = s.x_1 + s.\dot{x}_1 d_i + \frac{a_{min}
%    {d_i}^2}{2}$, and $\forall t \in (0, d_i)$, $w(t).\ddot{x}_1 = a_{min}$. The second vehicle's state components can be arbitrary,
%    as long as no collisions occur. Now, $\forall t \in (0, d_i)$, let
%    $Init(t) = w(t).(\dot{x}_1, x_1)$. Informally, we just prefed the
%    buffer with information that could have happened in that initial
%    time period (so that the last position and velocity values in the
%    buffer match up the initial position and velocity values of the
%    vehicles). Assuming that the leading vehicle was decelerating at
%    the maximum rate for that ``imaginary'' time period lets the
%    controller of the trailing vehicle be the most flexible (which is
%    proven in the Optimality section), in the initial $d_i$ time period. 
\end{automaton}

\begin{automaton}{\aatM}
\atsM = \atK(1, $\{acc_{d2}\}$, $\{acc_2\}$, $var$, $d_o$, $Init$,
$d_o$), where $var(acc_{d2}) = acc_2$; $d_o \in \nnr$ is the ``action
delay'' -- the time that it can take for a vehicle to react to
the controllers directives; $\mathit{Init}(t) = a_{min}$. Setting {\em Init} so conservatively makes the vehicles safe
in the initial $d_o$ time interval even if the first vehicle starts
decelerating at the maximum rate. This is the best we can do without
any further knowledge. This automaton delays the acceleration commands by $d_o$.
\end{automaton}

\begin{figure}[ht]

\begin{myiotab}

{\bf Definition:} \\

\>      $\mathit{safe}\text{-}\mathit{measure}_d = \max(x_{d1} +
\dot{x}_{d1} t' + \frac{a_{min} {t'}^2}{2} - (x_{dint2} + l_2) + \frac{{\dot{x}_{dint2}}^2 - {(\dot{x}_{d1} + a_{min} t')}^2 - {(v_{allow})}^2}{2 a_{min}}$, \\

        \>\>\>\>\>\> $\dot{x}_{d1} + a_{min} t' - \dot{x}_{dint2} + v_{allow})$, \\

\>\>    where $t' = \min(d_i+d_o, - \frac{\dot{x}_{d1}}{a_{min}})$ \\

{\bf Variables:} \+\\

        Input:\>\>\>      $\dot{x}_{d1} \in \nnr$ \\
                \>\>\>    $x_{d1} \in \nnr$\\

        Output: \>\>\>    $acc_{d2}$, initially if $\ssmd \leq 0$, then $acc_{d2} = a_{min}$\\
        Internal: \>\>\>  internal variables of \atsD ($\dot{x}_{int2}$
        and $x_{int2}$), which are now initialized using the info from
        \atL \\

                  \>\>\> $a_2$ - maps from an interval $(0, d_o)$ to $acc_{d2}$, \\
                \>\>\>\> initially, $\forall t \in (0, d_o), a_2(t) = a_{min}$\\

                \>\>\> $x_{dint2}$, $\dot{x}_{dint2}$ - the position and velocity of the second vehicle \\

                \>\>\>\> after time $d_o$ passes, provided $\mathit{collided}$ still equals $\mathit{false}$\-\\

{\bf Trajectories:} \+\\

        an $I$-trajectory $w$ is included among the set of nontrivial trajectories exactly if \+\\
        1. $w'$ is a trajectory of \atD, where $w'$ is a trajectory
constructed from $w$ such that \\
	\> in all states of $w'$, $w'(t).x_{d1} =
w(t).x_1$, $w'(t).\dot{x}_{d1} = w(t).\dot{x}_1$, and $w'(t).acc_{d2}
= w(t).acc_2$ \\

        2. if $\mathit{collided} = \mathit{false}$ in $w(0)$ then for all $t \in I$, $t > 0$: \+\\ 

                2.1. if in state $w(t)$ $\ssmd \leq 0$ then $acc_{d2} = a_{\mathit{min}}$\\

                2.2. $\forall t' \in (0,d_o)$, \\ 

        \>      $w(t).a_2(t')$ = 

                $\begin{cases}

                w(0).a_2(t'-t)& \text{ if } t' > t \\

                w(t - t').acc_{d2}& \text{ otherwise } 

                \end{cases}$\\

        2.3. $w(t).\dot{x}_{dint2} = w(t).\dot{x}_{int2} + {\int_{0}}^{d_o}w(t).a_2(u) du $ \\

        2.4. $w(t).x_{dint2} = w(t).x_{int2} + {\int_{0}}^{d_o}w(t).\dot{x}_{dint2}du$ \\

\end{myiotab}

\caption{\atsN Hybrid Automaton}

\label{fig:d2}

\end{figure}

Finally, we modify the controller so that it handles the delays
correctly. 

\begin{automaton}{\aatN}
The controller \atsN (see Figure \ref{fig:d2}), composed
with delay buffers \atsL and \atM, implements
\atD. It is an {\em HA} since the changes from \atsD do not violate
axioms $T2-3$, because they do restrict trajectory duration. It is similar to \atsG in that it also tries
to keep the second vehicle within the bounds set by
$\ssmd$, which is \sm redefined for the delayed case.

\paragraph{Definition} 
\smd is exactly like \sm,
modified by replacing the position, velocity and acceleration data of
both vehicles by their ``worst possible'' values. For vehicle $2$, these
are the projected values after $d_o$ time units pass, described by
$x_{dint2}$ and $\dot{x}_{dint2}$; for vehicle $1$, this means
deceleration at the maximum possible rate for the last $d_i + d_o$
time units, since the controller's information is $d_i + d_o$ time
units ``old.''
The derivation of these new values is described below (see properties).

\paragraph{Variables} 
The new controller gets its inputs from the inbound delay buffer \atsL
and its output variable goes into the outbound delay buffer
\atM. Thus, the input variables are now $\dot{x}_{d1}$, $x_{d1}$
instead of $\dot{x}_1$, $x_1$; and the output variable is $acc_{d2}$
instead of $acc_2$. Additional internal variables, $x_{dint2}$,
$\dot{x}_{dint2}$, represent the position and velocity
of the second vehicle after time $d_o$ passes, provided
$\mathit{collided}$ still equals $\mathit{false}$. They are used
for \smd calculations. In order to calculate
these variables, we add a special buffer, $a_2$, that stores the
controller's acceleration commands that have not been executed yet
(due to the outbound delay). Initially, $\forall t \in (0, d_o),
a_2(t) = a_{min}$, so that it matches the initial information in the
outbound buffer. 

\paragraph{Trajectories} Conditions (1) and (2.1) are exactly the same as
for \atG, substituting the new \smd
definition. Clause (2.2) sets up $a_2$ to save acceleration commands
output by the controller in the last $d_o$ time units. $a_2(0^+)$
represents the most recent command issued, and $a_2(d_o^-)$ represents
the command that is going to be implemented the fastest.
Finally, clauses (2.3) and
(2.4) set up $x_{dint2}$ and $\dot{x}_{dint2}$ to be the integrals of the
commanded acceleration. Since there is no uncertainty, these variables
represent the actual values of the corresponding variables in \atA,
but time $d_o$ in the future (see Properties below).

\paragraph{Properties}
The following delay relationships will be useful later. Take any $I$-trajectory $w$ such that at $w(0)$, $\mathit{collided} = \mathit{false}$. For any state $s$, the following will hold in a state $s'$, such that $s'.now = s.now + d_o$ (a state that occurs time $d_o$ later):
\begin{enumerate}
\item
$s'.\dot{x}_1 \geq s.\dot{x}_{d1} + a_{\mathit{min}} t'$,
where $t' = \min{({- s.\dot{x}_{d1} \over a_{\mathit{min}}}, d_i + d_o)}$.

That is, the actual velocity of vehicle $1$ is at least as great as the velocity time $d_i + d_o$ in the past, plus the maximum possible decrease in velocity during time $d_i + d_o$.

\item
$s'.x_1 \geq s.x_{d1} + s.\dot{x}_{d1} t' + \frac{1}{2} a_{\mathit{min}} {t'}^2$,
where $t' = \min{({- s.\dot{x}_{d1} \over a_{\mathit{min}}}, d_i + d_o)}$.

That is, the actual position of vehicle $1$ is at least as great as
the position time $d_i + d_o$ ago, adjusted by the velocity time $d_i + d_o$ ago and the greatest deceleration.

\item
$s'.\dot{x}_2 = s.\dot{x}_{dint2}$ and $s'.x_2 = s.x_{dint2}$.

That is, the actual position and velocity of vehicle $2$ in state $s'$
are equal to the ``predicted'' values (given by the internal
variables) from state $s$, that occurred time $d_o$ earlier.
\end{enumerate}

The proof of these delay relationships is straightforward, because
they are based on physical principles of motion.
Note that these delay relationships hold in
the initial $(0, d_o + d_i)$ time period, since we prefed all the
buffers with suitable data that will match up with real data at time
$0$.
\end{automaton}

Finally, we compose this new controller with the delay buffers, to get
an automaton that implements \atD.

\begin{figure}
\center{\PSbox{Fig/Slide3.PS hscale=75 vscale=75}{4.3in}{2.8in}}
\caption{\atsO hybrid automaton}
\label{fig:del}
\end{figure}

\begin{automaton}{\aatO}
\atsO = VarHide($\{x_{d1}, \dot{x}_{d1}, acc_{d2}\}$, \atsL x \atsN x
\atsM), see Figure \ref{fig:del}. The variables that communicate
between the sensors and the controller are hidden so that \atsO is
comparable to \atG.
\end{automaton}

\section{Correctness of \atO}

A straightforward simulation relation shows that \atsO implements
\atsG controller. This simulation relation $f$ is the identity on all the external
state components of \atsG automaton. The use of simulation relations allows
us to prove correctness of our more complicated delayed controller
relatively easily, since we have already proven correctness in the
simple (ideal) case.

First we prove that if the old \sm (the one used in the ideal case) is
non-positive in some state of a trajectory of \atO, then the new
controller \atsO (the one that has both the inbound and the outbound
delays), will also output maximum deceleration, just as the old
(ideal) controller \atsG would. Formally, 

\begin{lemma} \label{del2:sm}
In the Delayed-Controller$_2$ system, if $\mathit{collided} = {false}$ in $w(0)$ of trajectory $w$, then for all $t \in I$, such that $\ssm \leq 0$, $acc_2 = a_{min}$.
\end{lemma}

\begin{figure}
\center{\PSbox{Fig/Slide5.PS hscale=75 vscale=75}{5.8in}{1.5in}}
\caption{The timing diagram of the in- and outbound controller}
\label{fig:timing}
\end{figure}

\begin{proof}
Suppose that $\mathit{collided} = \mathit{false}$ in $w(0)$ and there
exists a reachable state $s$, such that $\ssm \leq 0$ in
$s$. If $s.now < d_o$ (we are still in the initial period when
the controller's commands do not reach the vehicle, and \atsM just outputs maximum deceleration), then by definition of the outbound buffer \atM, $acc_2 = a_{min}$ and we are done. Otherwise, at $s$ we have
\begin{equation} \label{del2:alt1}
x_1 - (x_2 + l_2)  \leq - \frac{{(\dot{x_2})}^2 - {(\dot{x}_1)}^2 - {(v_{allow})}^2}{2 a_{min}}
\end{equation}
and
\begin{equation} \label{del2:alt2}
\dot{x_2} \geq \dot{x}_1 + v_{allow}.
\end{equation}

Let's look at any state $s'$ of this system such that $s'.now = s.now - d_o$ (see Figure \ref{fig:timing}), and from which $s$ is reachable in time $d_o$ ($s'$ is the state in which the second controller \atsN decided what acceleration the vehicle should have in state $s$). For such a state, we have from the delay relationships, $s'.x_{dint2}  = s.x_2$ and $s'.\dot{x}_{dint2} = s.\dot{x_2}$. Also, from the delay relationships,
\begin{align*} 
s.\dot{x}_1 & \geq s'.\dot{x}_{d1} + a_{min} t', \\
s.x_1 & \geq s'.x_{d1} + s'.\dot{x}_{d1} t' + \frac{a_{min}
{t'}^2}{2}, \\
s.x_2 & = s'.x_{dint2}, \\
s.\dot{x}_2 & = s'.\dot{x}_{dint2} 
\end{align*}
where $t' = \min(d_i + d_o, - \frac{\dot{x}_{d1}}{a_{min}})$.

\paragraph{Inequality \ref{del2:alt1}} 

\begin{align*}
x_1 - (x_2 + l_2)  & \leq - \frac{{(\dot{x_2})}^2 - {(\dot{x}_1)}^2 - {(v_{allow})}^2}{2 a_{min}} \tag{at $s$} \\
x_{d1} + \dot{x}_{d1} t' + \frac{a_{min} {t'}^2}{2} - (x_{dint2} + l_2) &
\leq - \frac{{(\dot{x}_{dint2})}^2  - {(\dot{x}_{d1} + a_{min} t')}^2 - {(v_{allow})}^2}{2 a_{min}} \tag{at $s'$},
\end{align*}
where $t' = \min(d_i + d_o, - \frac{\dot{x}_{d1}}{a_{min}})$.

But this is exactly equivalent to the first part of \smd at $s'$!

\paragraph{Inequality \ref{del2:alt2}} 
\begin{align*}
\dot{x_2} & \geq \dot{x}_1 + v_{allow} \tag{at $s$}\\
\dot{x}_{dint2} & \geq \dot{x}_{d1} + a_{min} t' + v_{allow}, \tag{at $s'$}
\end{align*}
where $t' = \min(d_i + d_o, - \frac{\dot{x}_{d1}}{a_{min}})$. 

But this is exactly equivalent to the second part of \smd at $s'$!

We proved that in $s'$, both parts of \smd will be non-positive and so $\ssmd \leq 0$. Then the definition of \atsN guarantees that $s'.acc_{d2} = a_{min}$. And by the definition of \atM, $s.acc_2 = s'.acc_{d2}$. Thus, $s.acc_2 = a_{min}$ as needed.
\end{proof}

\begin{lemma} \label{del2:sim}
$f$, an identity relation on all the external components of \atG, is a forward simulation from the composed system Delayed-Controller$_2$ to \atG.
\end{lemma}

\begin{proof}
By induction on the number of steps in the hybrid execution.

\paragraph{Start States:} Trivial, since all the restrictions on start states of \atsG are also restrictions on start states of \atO.

\paragraph{Discrete Steps:} In the composed system there are no discrete steps, except for a dummy action $e$, but since there are no environmental inputs it does not do anything.

\paragraph{Trajectories:}
Suppose that $w_D$ is an $I$-trajectory of the delayed controller system \atsO and its first state $s_D$ is reachable. Suppose that $s_C$ is a reachable state of \atsG such that $(s_D, s_C) \in f$. Then let the corresponding hybrid execution fragment of \atsG consist of a single trajectory $w_C$, where $w_C(t).\dot{x}_1 = w_D(t).\dot{x}_1$, $w_C(t).x_1 = w_D(t).x_1$ and $w_C(t).acc_2 = w_D(t).acc_2$. It is obvious that the two trajectories have the same hybrid trace and that the final states of both trajectories are $f$-related. 

The only interesting thing to show is that $w_C$ is in fact a
trajectory of \atG. By the definition of a trajectory of \atsG we must show that
\begin{enumerate}
\item $w_C$ is a trajectory of \atD. This is
  trivial, since it also a restriction on the trajectories of \atN,
  and the buffers do not change any of the values involved.
\item If $\mathit{collided} = \mathit{false}$ in $w_C(0)$ then in all
reachable states $s$ of trajectory $w_C$, if $\ssm \leq 0$, then $s.acc_2 = a_{min}$. This follows directly from Lemma \ref{del2:sm}. 
\end{enumerate}
\end{proof}

\begin{theorem}
\label{theo:del}
Delayed-Controller$_2$ is a correct controller for \aatA.
\end{theorem}

\begin{proof}
We need to prove that The system \atE(\atA, $A_1$, \atO), where $A_1$
is any implementation of \atC, implements \atF.
\atsO is comparable to \atG, and by Lemma \ref{del2:sim}, there exists a
simulation relation from \atsO to \atG. So \atsO implements \atG.

By Theorem
  \ref{th:impl}, \atE(\atA, $A_1$, \atG)  implements \atF. Thus,
\atE(\atA, $A_1$, \atO)
also implements \atsF by the hybrid I/O automata
  composition rules, which means that it is, in fact, {\em correct},
  by definition \ref{def:correctness}.
\end{proof}


\section{Optimality of \atN} \label{ss:del-opt}

We will now give and prove necessary conditions for \atsN (and the
\atsO system) to be correct. Again,
we will be basing our proofs on the fact that \atJ's conditions are
necessary, which was proven in section \ref{ss:opt}. First, we define
a new automaton, \atV, which gives necessary conditions for {\em
safety}. Then, we show that if some implementation of \atsD includes inbound and
outbound delay buffers, but does not implement \atV,
then \atsL $\times D \times$ x \atsM system, where $D$ is this controller, will not be {\em correct}.
This should be intuitively clear, since we only
changed \sm to account for the ``worst-case'' (but
{\em possible}) behavior of the vehicles during the last $d_i + d_o$ time
period of the delays. Relying on the fact that \atsJ is necessary
makes the proof much easier: we only need to show that a controller
that would let \smd get negative, will eventually
lead to a state in which \sm itself is
negative. Then we can use necessity of \atsJ to show that any such
controller would not be {\em correct}.

\begin{figure}[ht]
\begin{myiotab}
{\bf Variables:} \+\\
        Input, Output, Internal: same as in \atN \-\\
{\bf Trajectories:} \+\\
        an $I$-trajectory $w$ is included among the set of nontrivial
        trajectories exactly if \+\\
        it satisfies condition 1 of \atN, plus \\
        2. for all $t \in I$, \+\\
                2.1. if $\mathit{collided} = \mathit{false}$ and $\ssmd
  < 0$ then $w(t).acc_2 = a_{\mathit{min}}$\\
                conditions 2.2-2.5 of \atsN are satisfied \-\-\\
\end{myiotab}
\caption{\atsJ Hybrid Automaton}
\label{fig:n-d2}
\end{figure}

\begin{automaton}{\aatV}
This automaton is exactly like \atN, except that condition (2.1) for
trajectories is slightly modified. In particular, \atsV commands
maximum deceleration when $\ssmd < 0$, while \atsN does it when $\ssm
\leq 0$. The formal model is given in Figure \ref{fig:n-d2}; thus the
only difference is the boundary in condition (2.1).
We claim that this condition is necessary to guarantee {\em correctness}. 
\end{automaton}

\begin{definition}{Predicate ${S_d}$}
If {\em collided = false} then $\ssmd \geq 0$.
\end{definition}

We now define $Bad_d$ controllers, similar to the $Bad$
controllers in the ideal case in the last chapter.

\begin{definition}{$Bad_d$}
Let $B_{d1}$ and $B_{d2}$ be implementations of \atC, and \atO,
respectively. $B_{d1}$ is $Bad_d$ for $B_{d2}$ if in any execution of the
system \atE(\atA, $B_{d1}$, $B_{d2}$) there exists a reachable state $s$
that violates Predicate $S_d$. $B_{d2}$ is said to be $Bad_d$ if
there exists an implementation of \atsC which is $Bad_d$ for $B_{d2}$.
\end{definition}

Based on the above definitions, we will now state an existence lemma,
very similar to Lemma \ref{lem:bad}. 

\begin{definition}{VeryBad$_d$}
Let an implementation $B'_{d1}$ of \atsC be called {\bf VeryBad$_d$}
for an implementation $D$ of 
\begin{enumerate}
\item
$B'_{d1}$ is $Bad_d$ for $B_{d2}$;
\item
In any execution of \aatE(\aatA, $B'_{d1}$, $B_{d2}$), for any state $s$ that
does not satisfy Predicate $S$, strictly after the occurrence of $s$,
$acc_1 = a_{min}$. 
\end{enumerate}
\end{lemma}

\begin{lemma}
\label{lem:badd}
If $B_{d2}$ is $Bad_d$ then there exists $B'_{d1}$, such that 


\begin{proof}

\end{proof}

\begin{lemma}
\label{lem:del-opt}
If an implementation of \aatO is $Bad_d$, then it is also Bad.
\end{lemma}

\begin{proof}
Let $B_{d2}$ be a $Bad_d$ implementation of \atO. Then, by Lemma
\ref{lem:badd}, there must
exist an implementation $B'_{d1}$ of \atsC that is both 1) $Bad_d$ for
this $B_{d2}$, and b) decelerates at the maximum rate right after
violating Predicate $S'$. We
need to prove that $B'_{d1}$ is also $Bad$ for $B_{d2}$, and not only
$Bad_d$. In particular, we need to show that any execution of
\atE(\atA, $B'_{d1}$, $B_{d2}$) violates Predicate $S$, and not only
Predicate $S_d$, which follows from the definition of $Bad_d$.

Let's look at a state $s$ of this \atsE system, which violates
Predicate $S_d$; existence of this state follows from the fact that
$B_{d2}$ is $Bad_d$. For such $s$, $\mathit{collided} = \mathit{false}$ and $\ssmd < 0$, meaning that
\begin{equation} 
x_{d1} + \dot{x}_{d1} t' + \frac{a_{min} {t'}^2}{2} - (x_{dint2} +
l_2) < - \frac{{(\dot{x}_{dint2})}^2 - {(\dot{x}_{d1} + a_{min} t')}^2 - {(v_{allow})}^2}{2 a_{min}}
\end{equation}
and
\begin{equation} \label{del:alt2}
\dot{x}_{d1} + a_{min} t' < \dot{x}_{dint2} - v_{allow},
\end{equation}
where $t' = \min{(- {\dot{x}_{d1} \over a_{\mathit{min}}}, d_i + d_o)}$.

By the definition of $B'_{d1}$, it always decelerates at the maximum
allowable rate, $a_{min}$. Let's look at a reachable state $s'$ of the composed system, in which $s'.now = s.now + d_o$ and which is reachable from $s$ in $d_o$ time units. Then in $s'$,
$$s'.\dot{x}_1 = s.\dot{x}_{d1} + a_{\mathit{min}} t',$$
$$s'.x_1 = s.x_{d1} + s.\dot{x}_{d1} t' + \frac{1}{2} a_{\mathit{min}} {t'}^2,$$
$$s'.\dot{x_2} = s.\dot{x}_{dint2} \text{ and } s'.x_2 = s.x_{dint2},$$
where $t' = \min{(- {\dot{x}_{d1} \over a_{\mathit{min}}}, d_i + d_o)}$. Note, these equalities also hold in the initial $d_i$ time interval, because our data in the inbound delay buffer assumes that the first controller is decelerating at the maximum rate.

Substituting these equations into the above inequalities will yield
the two parts of \sm in state $s'$; moreover, both parts turn out to
be negative, which means that in state $s'$, $\ssm < 0$, thus violating
Predicate $S$, which is exactly what we needed to prove.
\end{proof}

Since we have just shown that the delayed controller (composed with
delay buffers) implements the non-delayed one, we can use the
necessity property of the ideal case controller, to prove the
necessity of the delayed controller easily:

\begin{theorem}
If an implementation of \atsD has inbound and outbound delays but does
not implement \aatO, then it is not correct.
\end{theorem}

\begin{proof}
Let $B_{d2}$ be an implementation of \atsD that has inbound and
outbound delays but does not implement \atO. It must be $Bad_d$, since
the only restriction on \atsO is that it always satisfies Predicate
$S_d$, which is precisely the condition $Bad_d$ controllers violate.

By Lemma \ref{lem:del-opt}, $B_{d2}$ is also $Bad$. But then, by
Theorem \ref{theo:opt}, there exists an implementation $B_1$ of \atC,
such that a system \atE(\atA, $B_1$, $B_{d2}$) has a reachable state
that violates {\em safety}. If this \atsE system violates {\em safety},
then it does not implement \atF, which means that $B_{d2}$ is not {\em
correct}, by Definition \ref{def:correctness}.
\end{proof}

Therefore, \atsO is both necessary and sufficient.

