\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 delay 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 could have its own delay characteristics; our analysis would
still hold up, since we would look 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.

\section{Delay Buffers}

We model both the inbound and the outbound delays by special delay
buffers. To obtain the delayed system, we 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 variables with $n$
        members in each set \\
        \> Let $V(s)$, where $s$ is a variable, be a valuation of
        the variable $s$;\\
        \>\>$V(S)$, where $S$ is a set of variables, 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)) = w(t).saved(d).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) = V(S_i)$
and represents the most recent input; $saved(d)$ represents the
least recent input, the one that is just about to be output.
\end{itemize}

\paragraph{Trajectories}
Condition (1) sets up the output variables to take their values
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 a {\em HA}.

\paragraph{Properties}
From the automaton definition, it follows 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 using 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, the inbound delay buffer}
\atsL = \atK(3, $\{x_1, \dot{x}_1, \ddot{x}_1\}$, $\{x_{d1},
\dot{x}_{d1}, \ddot{x}_{d1}\}$, $var$, $d_i$, $Init$), where $var(x_1) =
x_{d1}$, $var(\dot{x}_1) = \dot{x}_{d1}$, and $var(\ddot{x}_1) =
\ddot{x}_{d1}$; $d_i \in \nnr$, the inbound delay, is the 
    ``information'' delay -- the time it takes the controller
    to get the information from the sensors. The inbound delay
automaton delays the position, velocity and acceleration data of the
first vehicle, with delay $d_i$. 

Given arbitrary initial values for input values for $x_1, \dot{x}_1,
\ddot{x}_1$, {\em Init} is set up so that the $Init(0)$ matches up
with these values. The least restrictive conditions on the behavior of
the second controller are obtained if we assume
that the leading vehicle was decelerating at the maximum possible rate
throughout the $d_i$ time period. Then the second controller does not
have to push the brakes thinking that there is a ``dangerous''
situation during the initial $d_i$ time period.
Safety is preserved as long as
$Init(0)$ matches up with the actual data at time $0$. So, {\em Init}
assumes vehicle $1$ was decelerating at $a_{min}$ and fills the
position and velocity values accordingly.

Formally, $Init$ is set up as follows. For any start values $a_1, a_2,
a_3$ of $x_1,
\dot{x}_1, \ddot{x}_1$, respectively, construct a trajectory $w$ of \atL, of length $d_i$ such that
\begin{align*} 
\forall t \in [0, d_i), w(t).\ddot{x}_1 & = a_{min}\text{, and
}w(d_i).\ddot{x}_1 = a_3, \\
\forall t \in [0, d_i], w(t).\dot{x}_1 & = a_2 + (t - d_i) a_{min}, \\
\forall t \in [0, d_i], w(t).x_1 & = a_1 + a_2 (t - d_i) +
\frac{a_{min}{(t - d_i)}^2}{2}.
\end{align*}
Then, $w(d_i).\{x_1, \dot{x}_1, \ddot{x}_1\} = \{a_1, a_2, a_3\}$, so that it matches up with real data at time $0$.
Let $Init(t) = w(d_i - t).(x_1, \dot{x}_1, \ddot{x}_1)$, then
$Init(0)$ matches up with the actual values at time $0$.
\end{automaton}

\begin{automaton}{\aatM, the outbound delay buffer}
\atsM = \atK(1, $\{acc_{d2}\}$, $\{acc_2\}$, $var$, $d_o$, $Init$),
where $var(acc_{d2}) = acc_2$; $d_o \in \nnr$, the outbound delay, is the ``action 
delay'' -- the time that it can take for a vehicle to react to
the controller's directives; $\forall t \in [0, d_i], \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 Variables:} \+\\

        Input:\>\>\>      $x_{d1}, \dot{x}_{d1} \in \nnr$,
$\ddot{x}_{d1} \in \reals$ \\
                \>\>\>    $x_{2}, \dot{x}_2 \in \nnr$, $\ddot{x}_2 \in
\reals$ \\

        Output: \>\>\>    $acc_{d2}$, initially arbitrary, where
$acc_{d2} \geq a_{min}$ \\
        Internal: \>\>\>  internal variables of \atsD ($\dot{x}_{int2}$
        and $x_{int2}$), \\

{\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_1 =
w(t).x_{d1}$, $w'(t).\dot{x}_1 = w(t).\dot{x}_{d1}$, $w'(t).\ddot{x}_1
= w(t).\ddot{x}_{d1}$, \\
        \>$w'(t).acc_2 = w(t).acc_{d2}$, and all other state
components are the same as in \atW \\

\end{myiotab}

\caption{\atsW Hybrid Automaton}

\label{fig:spec-d2}

\end{figure}

Finally, we modify the controller specification so that it
communicates with the buffers correctly.

\begin{automaton}{\aatW}
The controller \atsW (see Figure \ref{fig:spec-d2}), composed
with delay buffers \atsL and \atM, implements
\atD. It is an {\em HA} since the changes to trajectory definitions do
not violate axioms $T2-3$. It is
similar to \atsD, except that the input and output variables are
changed, and the restriction on trajectories is modified.

\paragraph{Variables} 
The new controller gets its data about the first vehicle from the
inbound delay buffer \atsL, and the ``self'' data (data about the
second vehicle) directly from the \atsA automaton. This models the
situation in which there is delay in getting the information via the
sensors about the other vehicle, but there is perfect self information.
The output variable goes into the outbound delay buffer
\atM. 

\paragraph{Trajectories} Condition (1) makes sure that the
trajectories of \atsW are allowed by \atD, after the variable change.
It is needed to ensure that \atsW composed with the delay buffers
implements \atD. 

\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($D$) hybrid automaton}
\label{fig:del}
\end{figure}

\begin{automaton}{\aatO($D$)}
\atsO($D$) = 

VarHide($\{x_{d1}$, $\dot{x}_{d1}$, $\ddot{x}_{d1}$, $acc_{d2}\}$,
\atsL $\parallel D \parallel$ \atsM), where $D$ is an implementation
of \atW (see Figure \ref{fig:del}). The variables that communicate
between the sensors and the controller are hidden so that \atsO($D$) is
comparable to \atG.

The following two theorems state relationships between the variables
of \atsW at different points in time.

\begin{theorem}
\label{theo:ds-prop1}
Let $A_1$ be any implementation of \aatC, $s''$ be a reachable state of
the \aatE(\aatAA, $A_1$, \aatO(\aatW)) system, and $s'$ be a state
reachable from $s''$ such that
$s'.now = s''.now + d_i$ and collided = false in $s'$. Then,
$$s'.x_{d1} = s''.x_1, s'.\dot{x}_{d1} = s''.\dot{x}_1 \text{, and }
s'.\ddot{x}_{d1} = s''.\ddot{x}_1.$$
\end{theorem}

\begin{proof}
The theorem states the relationships between a state $s''$, and a $s'$
that occurred time $d_i$ after $s''$ (see Figure \ref{fig:timing}). It states
that the data received through the input buffer \atsL is exactly the same as the
actual data time $d_i$ ago. This follows from Property 2 of \atsK
(outputs of a buffer in state $s$ equal the buffer's inputs in state
$s'$ that occurred time $d$ ago).
\end{proof}

\begin{theorem}
\label{theo:ds-prop2}
Let $A_1$ be any implementation of \aatC, $s'$ be a reachable
state of the \aatE(\aatAA, $A_1$, \aatO(\aatW)) system, and $s$ be a
state reachable from $s'$ such that 
$s.now = s'.now + d_o$, collided = false in $s$, and $s$ is reachable
from $s'$. Then,
\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)}$.
\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)}$.
\end{enumerate}
\end{theorem}

\begin{proof}
The theorem states the relationships between a state $s'$, and a state
$s$
that occurs time $d_o$ after $s'$ (see Figure \ref{fig:timing}).
By Theorem \ref{theo:ds-prop1},
the position, velocity and acceleration data in state $s'$ equal the
``delayed'' values in state $s$. By Properties 1 ($\ddot{x}_i \geq
a_{min}$) and 2  (the fact that position and velocity are integrals of
acceleration) of \atsAA (see chapter 4), the position and velocity
bounds can be obtained by integrating the maximum deceleration.

In particular, the first clause states that the actual velocity of vehicle $1$
in state $s$ is at least as great as its velocity in state $s''$
that occurred time $d_i + d_o$ in the past, plus the maximum possible
decrease in velocity during that time. The second clause states that the actual position of vehicle $1$ in
state $s$ is at least as great as its position in state $s''$ that
occurred time $d_i + d_o$ ago, adjusted by the velocity time $d_i +
d_o$ ago and the maximum allowed deceleration. 
\end{proof}
\end{automaton}

\section{Correctness of \atO}

We give an implementation of \atsW that is sufficient to guarantee
{\em correctness}.

\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_{int2} + l_2) + \frac{({\dot{x}_{int2}})^2 - {(\dot{x}_{d1} + a_{min} t')}^2 - {(v_{allow})}^2}{2 a_{min}}$, \\

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

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

{\bf Variables:} \+\\

        Input:\>\>\> same as \atW \\ 
        Output: \>\>\>    $acc_{d2}$, initially if $\ssmd \leq 0$,
        then $acc_{d2} = a_{min}$, \\
        \>\>\>\> else arbitrary, where $acc_{d2}
        \geq a_{min}$\\
        Internal: \>\>\>  internal variables of \atW, plus \\

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

{\bf Trajectories:} \+\\

        an $I$-trajectory $w$ is included among the set of nontrivial trajectories exactly if \+\\
        1. $w$ is a trajectory of \atW \\

        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}}$ else $acc_{d2} \geq 0$\\

                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}_{int2} = w(t).\dot{x}_2 + {\int_{0}}^{d_o}w(t).a_2(u) du $ \\

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

\end{myiotab}

\caption{\atsN Hybrid Automaton}

\label{fig:d2}

\end{figure}

\begin{automaton}{\aatN}
The controller \atsN (see Figure \ref{fig:d2}) is a sufficient
controller to guarantee {\em correctness} of \atO(\atN).
It is an {\em HA} since the changes from \atsW do not violate
axioms $T2-3$.
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 $\ssm$,
modified by replacing the position, velocity and acceleration data of
vehicles by their delayed values. For vehicle $2$, the
delayed values are the values resulting from executing the
controller's commands for the outbound delay time $d_o$, as given by
$x_{int2}$ and $\dot{x}_{int2}$; for vehicle $1$, the ``worst
possible'' delayed values are generated by decelerating 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.''
In particular, using Theorems \ref{theo:ds-prop2} and \ref{theo:dd2-prop},
\begin{align*}
\text{replace } x_1 & \text{ by } x_{d1} + \dot{x}_{d1} t' + \frac{a_{min} {t'}^2}{2} \\
\text{replace } x_2 & \text{ by } x_{int2} \\
\text{replace } \dot{x}_1 & \text{ by } \dot{x}_{d1} + a_{min} t' \\
\text{replace } \dot{x}_2 & \text{ by } \dot{x}_{int2}
\end{align*}

\paragraph{Variables} 
External variables are the same as in \atW. $x_{int2}$,
$\dot{x}_{int2}$, 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
the values of 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} Condition (1) restricts each trajectory to satisfy
\atsW requirements. Condition (2.1) is 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 executed next.
Finally, clauses (2.3) and
(2.4) set up $x_{int2}$ and $\dot{x}_{int2}$ 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 at time $d_o$ in the future (see Theorem \ref{theo:dd2-prop}).

\begin{theorem}
\label{theo:dd2-prop}
Let $A_1$ be any implementation of \aatC, $s'$ be reachable states of
\aatE(\aatAA, $A_1$, \aatO(\aatW)), and $s$ be reachable from $s'$, such that
$s.now = s'.now + d_o$, collided = false in $s$. Then,
\begin{enumerate}
\item
$s.\dot{x}_2 = s'.\dot{x}_{int2}$;
\item
$s.x_2 = s'.x_{int2}.$
\end{enumerate}
\end{theorem}

\begin{proof}
The theorem states that the actual position and velocity of vehicle
$2$ in state $s'$ are equal to the ``predicted'' values (given by the internal
variables) in state $s$ that occurred time $d_o$ earlier. This follows
from Property 2 of \atsK (buffer outputs in state $s$ equal buffer
inputs in state $s'$ that happened time $d$ before $s$), Property 2 of
\atsAA (position and velocity are integrals of acceleration), and
Conditions (2.3-4) of \atsN trajectories.
\end{proof}
\end{automaton}

We prove that \atsN is sufficient to guarantee {\em
  correctness}. Throughout the rest of this section we will use the
  following notation:

For any implementation $A_1$ of \atC, let

$CV_I(A_1) = $ \atE(\atA, $A_1$, \atO(\atN)), and

$CV_D(A_1) = $ \atE(\atA, $A_1$, \atG).

We show that $CV_D(A_1)$ implements $CV_I(A_1)$.

The key result, proven in Lemma \ref{del2:sm} proves that if the old \sm (the one used in the ideal case) is
non-positive in some state of a trajectory of \atO(\atN), then
\atO(\atN) will also output maximum deceleration, just as the old
(ideal) controller \atsG would. Formally, 

\begin{lemma} \label{del2:sm}
Let $A_1$ be any implementation of \aatC, and let $s$ be a reachable state of the $CV_D(A_1)$ system, such that
$s.\mathit{collided} = {false}$ and $\ssm \leq 0$. Then $s.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}
By induction on the number of discrete and continuous steps in the hybrid execution. 
Initially, the lemma is true by restriction on the start states of
\atN. The discrete steps $e$ and the internal steps of $A_1$ do not
change any of the quantities involved; the $collide$ step makes the
Lemma true vacuously.

Without loss of generality, consider hybrid executions where all
trajectories have duration less than $d_o$. Let $s$ be any reachable state such that $s.\mathit{collided}
= \mathit{false}$ and $\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 (from the $Init$ function), $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 reachable 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 controller \atsN
decided what acceleration the vehicle should have in state $s$). This
states $s'$ cannot be in the same trajectory because of our
restriction on hybrid executions, so we can use the inductive
hypothesis on $s'$. For
such a state, by Theorem \ref{theo:dd2-prop}, $s'.x_{int2}  =
s.x_2$ and $s'.\dot{x}_{int2} = s.\dot{x}_2$. Also, by Theorem
\ref{theo:ds-prop2},
\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}
\end{align*}
where $t' = \min(d_i + d_o, - \frac{\dot{x}_{d1}}{a_{min}})$.

We take inequality \ref{del2:alt1}, and substitute the delayed values
for the actual ones (using the statements above), still keeping the
correctness of the inequality.

\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_{int2} + l_2) &
\leq - \frac{{(\dot{x}_{int2})}^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'$!

We do the same with inequality \ref{del2:alt2}.

\begin{align*}
\dot{x_2} & \geq \dot{x}_1 + v_{allow} \tag{at $s$}\\
\dot{x}_{int2} & \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, in \atO(\atN), $s.acc_2 = a_{min}$ as needed.
\end{proof}

\begin{lemma} \label{del2:sim}
Let $A_1$ be any implementation of \aatC, and let $f$ be the identity
relation on all the components of the $CV_I(A_1)$
system, except that $CV_I(A_1).x_{int2} = CV_D(A_1).x_2$, and
$CV_I(A_1).\dot{x}_{int2} = CV_D(A_1).\dot{x}_2$. Then $f$ is
a forward simulation from the composed system $CV_D(A_1)$ to $CV_I(A_1)$.
\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(\atN).

\paragraph{Discrete Steps:} The only discrete steps are {\em collide,
e} and the internal steps of $A_1$. The latter two steps cannot change
any of the quantities involved. Since the {\em collide} step is the
same for both automata, it respects the simulation relation. Also, the
effects of the {\em collide} step satisfy Predicate $S$ vacuously, thus
the state reached after the {\em collide} action is a valid state of $CV_I(A_1)$.

\paragraph{Trajectories:}
Suppose that $w_D$ is an $I$-trajectory of the delayed controller
system $CV_D(A_1)$ and its first state $s_D$ is reachable. Suppose that
$s_C$ is a reachable state of $CV_I(A_1)$ such that $(s_D, s_C) \in f$. Then
let the corresponding hybrid execution fragment of $CV_I(A_1)$ consist of a
single trajectory $w_C$, where $w_C(t) = w_D(t)$ (all variables have
the same values). 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 remaining thing to show is that $w_C$ is in fact a
trajectory allowed by \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 is 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}
\aatO(\aatN) is a correct controller for \aatA.
\end{theorem}

\begin{proof}
We need to prove that for any implementation $A_1$ of \atC, $CV_D(A_1)$ implements the {\em safety}
specification automaton \atF. $CV_D(A_1)$ is comparable to $CV_I(A_1)$, and, by Lemma \ref{del2:sim}, there exists a
simulation relation from $CV_D(A_1)$ to $CV_I(A_1)$. So $CV_D(A_1)$ implements $CV_I(A_1)$.

$CV_I(A_1)$ implements \atsF by Theorem \ref{th:impl}. Thus,
$CV_D(A_1)$ also implements \atsF, which means that \atO(\atN) is, in fact,
{\em correct}, by definition \ref{def:correctness}.
\end{proof}

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

We give and prove necessary conditions for an implementation
of \atsW to be {\em correct}. We base the proofs on the fact that
if an implementation $B_2$ of \atsD is correct, then for any
implementation $B_1$ of \atC, \atE(\atA, $B_1$, $B_2$) must implement \atE(\atA, $B_1$, \atsJ) (see section \ref{ss:opt}). First, we define
a new automaton, \atV, which gives necessary conditions for {\em
safety}. 
Then, we show that if for some implementation $D$ of \atsW
there exists an implementation $B_1$ of \atsC such that \atE(\atA,
$B_1$, \atO($D$)) does not implement \atE(\atA, $B_1$, \atO(\atV)),
then the \atO($D$) system will not be {\em correct}.
This should be intuitively clear, since we only
changed \sm to account for the ``worst-case'' (but 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
simplifies the proofs: 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.4 of \atsN are satisfied \-\-\\
\end{myiotab}
\caption{\atsV 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_1$ and $B_{d2}$ be implementations of \atsC and \atW,
respectively. Then $B_1$ is $Bad_d$ for $B_{d2}$ if and only if in the
system \atE(\atA, $B_1$, \atO($B_{d2}$)) there exists a reachable state $s$
that violates Predicate $S_d$. $B_{d2}$ is $Bad_d$ if and only if
there exists some $B_1$ that is $Bad_d$ for this $B_{d2}$.
\end{definition}

\begin{definition}{VeryBad$_d$}
Let an implementation $B'_1$ of \atsC be called {\bf VeryBad$_d$}
for an implementation $D$ of \atsD if
\begin{enumerate}
\item
$B'_1$ is $Bad_d$ for $B_{d2}$;
\item
In any execution of \aatE(\aatA, $B'_1$, $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{definition}

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

\begin{lemma}
\label{lem:badd}
If $B_{d2}$ is $Bad_d$ then there exists an implementation $B'_1$
of \aatC, such that $B'_1$ is VeryBad for $B_{d2}$.
\end{lemma}

\begin{proof}
The proof is identical to proof of a similar Lemma \ref{lem:bad} in
the previous Chapter.
\end{proof}

Next, we prove that if an implementation of \atsW does not implement
\atsN then it must be $Bad_d$.

\begin{lemma}
\label{lem:bbad2}
Let $B_{d2}$ be an implementation of \aatW. If there exists an
implementation $B_1$ of \atsC such that \aatE(\aatA, $B_1$,
\aatO($B_{d2}$)) does not implement \aatE(\aatA, $B_1$, \aatO(\aatV))
then $B_{d2}$ is $Bad_d$.
\end{lemma}

\begin{proof}
Identical to that of Lemma \ref{lem:bad2}.
\end{proof}

Lemma \ref{lem:del-opt} relates the $Bad_d$ and $Bad$ terms.

\begin{lemma}
\label{lem:del-opt}
Let $B_{d2}$ be an implementation $B_{d2}$ of \aatW. If $B_{d2}$ is
Bad$_d$, then \aatO($B_{d2}$) is Bad.
\end{lemma}

\begin{proof}
Let $B_{d2}$ be a $Bad_d$ implementation of \atW. Then, by Lemma
\ref{lem:badd}, there must
exist an implementation $B'_1$ of \atsC that is {\em VeryBad} for
$B_{d2}$. We
need to prove that $B'_1$ is $Bad$ for \atO($B_{d2}$), and not only
$Bad_d$ for $B_{d2}$. In particular, we need to show that there exists
a reachable state of
\atE(\atA, $B'_1$, \atO($B_{d2}$)) that violates Predicate $S$, and not only
Predicate $S_d$ (violation of Predicate $S_d$ follows from the
definition of $Bad_d$).

Let's look at a reachable state $s$ of this \atsE system that 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_{int2} +
l_2) < - \frac{{(\dot{x}_{int2})}^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}_{int2} - v_{allow},
\end{equation}
where $t' = \min{(- {\dot{x}_{d1} \over a_{\mathit{min}}}, d_i + d_o)}$.

By the definition of $B'_1$, it always decelerates at the maximum
allowable rate, $a_{min}$. Let's look at a state $s'$ reachable from
$s$ in time $d_o$, such that $s'.now = s.now + d_o$. 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}_{int2} \text{ and } s'.x_2 = s.x_{int2},$$
where $t' = \min{(- {\dot{x}_{d1} \over a_{\mathit{min}}}, d_i +
d_o)}$. The first 2 equations follow from the fact that position and
velocity are integrals of acceleration (Property 2 of \atAA); the last
2 follow from Theorem \ref{theo:dd2-prop}.
Note that 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$. But $\ssm <
0$ means that Predicate $S$ is violated, and, therefore, \atO($B_{d2}$) is
$Bad$.
\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 easily prove the
necessity of the delayed controller:

\begin{theorem}
\label{theo:dopt}
Let $B_{d2}$ be an implementation of \aatW. If there exists an
implementation $B_1$ of \atsC such that \aatE(\aatA, $B_1$,
\aatO($B_{d2}$)) does not implement \aatE(\aatA, $B_1$, \aatO(\aatV)) then
\aatO($B_{d2}$) is not correct.
\end{theorem}

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

Theorem \ref{theo:del} proves that \atO(\atN) is sufficient, and
Theorem \ref{theo:dopt} proves that \atO(\atV) is
necessary to guarantee {\em correctness}. Since the distinction between \atsN
and \atsV is very small, they can serve as the {\em correctness} specification.


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: 
