\chapter{Safety In The Ideal Case} \label{s:ideal}

We start with a treatment of the safety property in the ideal setting.
This allows us to prove some important properties of the simpler model
first, and then extend them to the more complicated models, which
include delays and uncertainties, via
simulation mappings. By ideal setting we mean that there are no delays
and/or uncertainties in either the sensors' data or the controller's
directives. In the next chapters we make the model more
realistic by relaxing these restrictions. 

\section{Problem Statement}

We want to give conditions on an implementation of \atsD that are both
necessary and sufficient to satisfy the {\em
correctness} property of Definition \ref{def:correctness}. In the next
section we present such conditions by showing an
implementation of \atD, called \atG, which guarantees {\em
  correctness}. Then, we show that the conditions are sufficient by
proving that this conroller is {\em correct}. Finally, we give slightly
less restrictive conditions on the controller and prove that these
conditions are necessary.

\section{The Model}

In any state of \atAA, define 

\begin{align*}
\ssm =
& \max(x_1 - (x_2 + l_2)
       + {(\dot{x}_2)^2 - (\dot{x}_1)^2 - (v_{\mathit{allow}})^2 
           \over 2 a_{min}}, \\
& \dot{x}_1 + v_{\mathit{allow}} - \dot{x}_2).
\end{align*}

We are not interested in the actual value of $\ssm$, but
only in whether or not it is negative. If it is nonnegative, it means
that either (a) the distance between the two vehicles is great enough
to allow vehicle $2$ to stop before hitting vehicle
$1$, even if vehicle $1$ decelerates at its fastest possible rate, or
(b) the relative velocities of the two vehicles are already close
enough. Thus, nonnegative \sm gives us the boundaries
of the safe region for the second vehicle.

\begin{figure}[ht]
\begin{myiotab}

{\bf Variables:} \+\\
        Input, Output, Internal: same as in \atD \-\\
{\bf Trajectories:} \+\\
        an $I$-trajectory $w$ is included among the set of nontrivial
        trajectories exactly if \+\\
        1. it satisfies condition 1 of \atD, plus \\
        2. for all $t \in I$, \+\\
                2.1-2.3 of \atsD are satisfied \\
                2.4. if $\mathit{collided} = \mathit{false}$ and $\ssm
  \leq 0$ then $w(t).acc_2 = a_{\mathit{min}}$\-\-\\
\end{myiotab}
\caption{$C_2$ Hybrid Automaton}
\label{fig:c2}
\end{figure}

\begin{automaton}{\aatG}
This automaton is exactly like \atD, with one extra restriction on its
trajectories. The formal model is given in Figure \ref{fig:c2}.
Condition (2.4) ensures that if the position and velocity parameters
are on the boundary defined by $\ssm$, then
\atsG commands maximum deceleration, by setting
$acc_2 = a_{min}$. In this ideal (no delays, no uncertainties)
setting, vehicle
$2$ will execute the command exactly, because $\ddot{x}_2 = acc_2$,
and so vehicle $2$ is decelerating as fast as possible. Since this
restriction does not violate axioms $T2$ and $T3$, \atsG is a valid {\em HA}.
We claim that this restriction is sufficient to guarantee {\em correctness}. 
\end{automaton}

\section{Correctness of \atG} \label{ss:correct}

We will now prove {\em correctness} of our controller. This means that any controller that implements \atG, will be correct (safe).

\begin{definition}{Predicate S}
If $\mathit{collided} = \mathit{false}$ then $\ssm \geq 0$.
\end{definition}

The above definition says that before the first collision occurs, \sm
is nonnegative. We will later prove that non-negativity of {\em
  safe-measure} guarantees {\em safety}.

\begin{figure}[ht]

\begin{myiotab}

{\bf Constants:} \+\\
        $l_i$, the length of the vehicle \\
        $a_{min} \in \negr$, the maximum emergency deceleration \-\\

{\bf Variables:} \+\\
        Input:\>\>
          $acc_i \in \reals$, initially arbitrary\\
        Output: \+\+ 
        $x_i \in \nnr$, initially $x_2 = 0$ and $x_1$ is arbitrary \\
        $\dot{x_i} \in \nnr$, initially arbitrary \\        
        $\ddot{x}_i \in \reals$, initially arbitrary \\
        {\em now}, initially $0$ \\
        {\em collided}, Boolean, initially {\em false} \\
        {\bf initial state is subject to Predicate S}  \-\-\-\\

{\bf Actions:} \\

\>      Internal:\>\>\>${collide}$\+\+\+\+\\

        Pre:\>\>        $x_1 = x_2 + l_2$ \\
        \>\>    ${collided} = {false}$ \\
        Effect:
        \>\>    $\ddot{x}_i :=$ arbitrary value\\
        \>\>    $\dot{x}_i := $ arbitrary value\\
        \>\>    ${collided} := {true}$ \-\-\-\-\\

{\bf Trajectories:} \+\\
        an $I$-trajectory $w$ is included among the set of nontrivial trajectories exactly if \+\\
        1. ${collided}$ is unchanged in $w$ \\
        2. $\ddot{x}_i$ is integrable twice in $w$ \\
        for all $t \in I$ the following hold:\+\\
                  3. If ${collided} = {false}$ in $w$ then \\

                           \>$ w(t).\ddot{x}_i = max(w(t).acc_i, a_{min})$\\
                  4. $ w(t).\dot{x}_i = w(0).\dot{x}_i + {\int_{0}}^{t}w(u).\ddot{x}_idu$\\
                  5. $w(t).x_i = w(0).x_i + {\int_{0}}^{t}w(u).\dot{x_i}du$\\
                  6. $w(t).x_2 + l_2 \leq w(t).x_1$\\
                  7. $w(t).now = w(0).now + t$\\
                  8. If $w(t).x_1 = w(t).x_2 + l_2$ and $t$ is not the right endpoint of $I$ then \\
                \>${collided} = {true}$.\\
\end{myiotab}

\caption{The \atsA Hybrid Automaton}

\label{fig:init-v}

\end{figure}

We construct a new automaton, \atA, which is exactly like \atAA,
except that all its start states are restricted to satisfy Predicate $S$.
This guarantees that the system is {\em safe}
initially. 

\begin{automaton}{\aatA}
Exactly like \atAA, but guarantees {\em safety} initially.
The formal model is shown in Figure \ref{fig:init-v}, with
the new restrictions in bold. Again, it is a valid {\em HA}, since
the modifications do not violate axioms $T2-3$.
\end{automaton}

\atsG is designed to guarantee explicitly that if $S$ is ever violated, or
is even in danger of being violated (because equality holds),
vehicle $2$ is decelerating as fast as possible. We claim that this
strategy is sufficient to guarantee that $S$ is always true. To prove
this, we will use the {\em Non-negativity Theorem}
\ref{s-pos:im-theo}, which states that all functions satisfying
certain conditions must be non-negative.

\begin{lemma}
\label{inv: simple-safe}
Predicate $S$ is true in every reachable state of \aatE(\aatA, $A_1$,
\atG), where $A_1$ is any implementation of \aatC.
\end{lemma}

\begin{proof}
By induction on the number of steps in a hybrid execution. Initially,
the claim is true by the restriction on the initial states of \atA.

The only discrete steps are {\em collide, e} and the internal steps of
$A_1$. The latter two steps do not change any of the quantities involved. The effect of the {\em collide} step ensures that {\em collided = true} in the post-state, which makes $S$ true vacuously.

\clearpage

Now we consider a trajectory $w$ whose domain is the interval $[0,T]$.
Since a trajectory cannot change $\mathit{collided}$, and $S$ is
vacuously true if $\mathit{collided} = \mathit{true}$, we only need to
consider the case where $\mathit{collided} = \mathit{false}$
throughout $w$. We may assume (by the induction hypothesis) that $S$
is true in $w(0)$. We must show that $S$ is true in $w(T)$. By
definition of $S$, we may assume that $\ssm \geq 0$ in state $w(0)$
and must show that this is also true in $w(T)$. 

Here we will use the notation $f(t)$ to mean $w(t).f$,
where $f$ is defined in terms of state components of $w(t)$.
Let $f(t) = x_1 - (x_2 + l_2) + \frac
{({\dot{x}_2})^2 - ({\dot{x}_1})^2 - ({v_{allow}})^2} {2 a_{min}}$,
$g(t) = \dot{x}_1 +v_{allow} - \dot{x}_2$. Then $s(t) = \max(f(t), g(t)) =
\ssm(t)$. We now use Theorem \ref{s-pos:im-theo} to prove that if $s(0) \geq 0$,
then $\forall t \geq 0, s(t) \geq 0$. 

{\em Claim 1.} $s(t)$ is continuous. 
\begin{proof}
By continuity of $f(t)$ and $g(t)$. 
\end{proof}

{\em Claim 2.} $s(0) \geq 0$.
\begin{proof}
Follows from the induction hypothesis.
\end{proof}

{\em Claim 3.} For all $t$ such that $s(t) \leq c$, it is the case
that $s'(t^+)$ and $s'(t^-)$ exist, $s'(t^+) \geq 0$ and $s'(t^-) \geq 0$.

\begin{proof}
The right derivative of $s$ equals the right derivative of
either $f(t)$ or $g(t)$, and the same is true for the left derivative,
by Theorem \ref{th:max}. We
need to check that for all $t$ such that $s(t) \leq 0$, we have $\dot{f}(t) \geq
0$ and $\dot{g}(t) \geq 0$. So, fix $t$ such that $s(t) \leq 0$. Then,
at $t$, we have: 
$$\dot{f} = 
\dot{x}_1 - \dot{x}_2 + \frac{1}{2 a_{min}} (2 \dot{x}_2
\ddot{x}_{2} - 2 \dot{x}_1 \ddot{x}_{1})
= \dot{x}_1 - \dot{x}_2 + \frac{1}{a_{min}} (\dot{x}_2
\ddot{x}_{2} - \dot{x}_1 \ddot{x}_{1})$$

By definition of \atsG we have that since $s \leq 0$, $acc_2 = \ddot{x}_2
= a_{min}$. Also, by restriction on \atA, we have $\ddot{x}_1 \geq a_{min}$. Therefore,
\begin{align*}
\dot{f} & = \dot{x}_1 - \dot{x}_2 + \frac{1}{a_{min}} (\dot{x}_2
\ddot{x}_2 - \dot{x}_1 \ddot{x}_1) \\
& = \dot{x}_1 - \dot{x}_2 + \dot{x}_2 \frac{a_{min}}{a_{min}} -
\dot{x}_1 \frac{\ddot{x}_1}{a_{min}} \\
& = \dot{x}_1 + \dot{x}_1 \frac{\ddot{x}_1}{- a_{min}} \\
& \geq \dot{x}_1 + \dot{x}_1 \frac{a_{min}}{- a_{min}} \\
& = 0.
\end{align*}

Now let's do the same for $\dot{g}$:
$$\dot{g} = \ddot{x}_{1} - \ddot{x}_{2} = \ddot{x}_{1} - a_{min} \geq
a_{min} - a_{min} = 0.$$

This proves Claim 3.
\end{proof}

From Claims 1, 2 and 3, $s$ satisfies the conditions of the {\em Non-negativity Theorem} and, therefore, by Theorem \ref{s-pos:im-theo}, $\forall t$ $s(t) \geq 0$. 

This suffices.
\end{proof} 

As a simple consequence of Lemma \ref{inv: simple-safe}, we prove the
{\em safety} property.

\begin{lemma}
\label{lm: invt-simple-safe-2}
In any reachable state of \aatE(\aatA, $A_1$, \atG), where $A_1$ is any
implementation of \atC, if $x_1 = x_2 + l_2$ and $\mathit{collided} = \mathit{false}$, then $\dot{x}_2 \leq
\dot{x}_1 + v_{\mathit{allow}}$.
\end{lemma}

\begin{proof}
Initially, $S$ is true by the restriction on initial states of \atA.
Consider any reachable state in which $x_1 = x_2 + l_2$ and $\mathit{collided} = \mathit{false}$. Then Lemma \ref{inv: simple-safe} implies that $\ssm \geq 0$. That is, either 
$$x_1 - (x_2 + l_2) \geq {(\dot{x}_2)^2 - (\dot{x}_1)^2 - (v_{\mathit{allow}})^2 \over 2 a_{\mathit{min}}}$$
or
$$\dot{x}_1 + v_{\mathit{allow}} \geq \dot{x}_2.$$
In the latter case, we are done. In the former, setting $x_1 - (x_2 +
l_2) = 0$, we get

$${(\dot{x}_2)^2 - (\dot{x}_1)^2 - (v_{\mathit{allow}})^2 \over 2
a_{\mathit{min}}} \leq 0$$
$$ (\dot{x}_2)^2 \leq  (\dot{x}_1)^2 + (v_{\mathit{allow}})^2 
        \leq (\dot{x}_1 + v_{allow})^2$$
$$ \dot{x}_2 \leq \dot{x}_1 + v_{allow},$$

as needed.
\end{proof}

Now we use Lemma \ref{lm: invt-simple-safe-2} to prove that the system
is in fact {\em correct}, i.e., that it implements \atF.

\begin{lemma}
\label{lm:imp-safe}
Let $f$ be the identity on all state components of \aatF
(velocities, positions, accelerations, and the $\mathit{collided}$ flag). Then $f$ is
a forward simulation from the composed system \aatE(\aatA, $A_1$, \atG), where
$A_1$ is any implementation of \atC, to \aatF.
\end{lemma}

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

\paragraph{Start States:} 
Suppose $s_{IP}$ is a start state of \atE(\atA, $A_1$, \atG), and
$(s_{IP}, s_{SP}) \in f$. We have to prove that $s_{SP}$ is a valid
start state of \atF. By the definition of start states of \atF, it
must satisfy the conditions of \atA, which follows from the fact that
$s_{IP}$ is a start state of \atsE and so it does satisfy all those
conditions. Also, by Lemma \ref{lm: invt-simple-safe-2}, $s_{SP}$
satisfies $\mathit{Safety}$.

\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 {\em safety} vacuously, thus
the state reached after the {\em collide} action is a valid state of \atF.

\paragraph{Trajectories:}
Suppose that $w_{IP}$ is an $I$-trajectory of \atsE and its first state $s_{IP}$ is reachable. Suppose that $s_{SP}$ is a reachable state of \atsF such that $(s_{IP}, s_{SP}) \in f$. Let the corresponding hybrid execution fragment of \atsF consist of a single trajectory $w_{SP}$, where $w_{SP}(t).\dot{x_i} = w_{IP}(t).\dot{x_i}$, $w_{SP}(t).x_i = w_{IP}(t).x_i$ for $i \in \{1,2\}$, $w_{SP}(t).collided = w_{IP}(t).collided$ and $w_{SP}(t).now = w_{IP}(t).now$. It is obvious that the two trajectories have the same hybrid trace and that the final states of both trajectories are $f$-related. 

We need to show that $w_{SP}$ is in fact a trajectory of \atF. By the definition of a trajectory we must show that it satisfies all the properties of a trajectory of \atA, but this is trivial, since it is a trajectory of \atsE which has all the restrictions of \atA. We must also show that it always satisfies the {\em safety} condition, but this follows directly from Lemma \ref{lm: invt-simple-safe-2}. Therefore, $f$ is also a valid simulation relation for all the trajectories.

\end{proof}

\begin{theorem} \label{th:impl}
\atsG is correct for \aatA, where correctness is defined by Definition \ref{def:correctness}.
\end{theorem}

\begin{proof}
To prove {\em correctness}, we need to show that the \atE(\atA, $A_1$,
\atG) automaton,
where $A_1$ is any implementation of \atC, implements \atF. \atE(\atA, $A_1$, \atG) and \atsF are
comparable and by Lemma \ref{lm:imp-safe}, there is a simulation
relation $f$ from \atsE to
\atF. Therefore, this composed system implements \atF. This proves
{\em correctness} of \atG.
\end{proof}

\section{Optimality of \atG} \label{ss:opt}

We devise a new controller, \atJ, which is slightly less restrictive
than \atsG and prove that \atsJ gives necessary conditions
for satisfying {\em correctness}.

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

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

We define a notion of {\em Bad} controllers. Let $B_1$ and
$B_2$ be implementations of \atsC and \atD, respectively. Then $B_1$ is
{\em Bad} for $B_2$ if $B_1$ makes $B_2$ violate Predicate $S$ by
going out of the \sm region. $B_2$
is {\em Bad} if there exists some $B_1$ which is {\em Bad} for it.

\begin{definition}{\aatH}
Let $B_1$ and $B_2$ be implementations of \atsC and \atD,
respectively. Then $B_1$ is {\bf Bad} for $B_2$ if and only if in the system \atE(\atA,
$B_1$, $B_2$) there exists a reachable state $s$ that does not
satisfy Predicate $S$.
\end{definition}

\begin{definition}{\aatI}
\label{def:bad1}
$B_2$ is {\bf Bad} if and only if there exists some $B_1$ that is Bad for this $B_2$.
\end{definition}

The following lemma shows that if $B_2$ is {\em Bad}, then we can construct
a $B'_1$ that is {\em Bad} for $B_2$ and decelerates at
the maximum rate once Predicate $S$ is violated. This $B'_1$ will later
be used to show that $B_2$ can violate {\em Safety}.

\begin{definition}{VeryBad}
\label{def:bbad1}
Let an implementation $B'_1$ of \atsC be called {\bf VeryBad} for an
implementation $B_2$ of \atsD if 
\begin{enumerate}
\item
$B'_1$ is {\em Bad} for $B_2$;
\item
In any execution $\alpha$ of \atE(\atA, $B'_1$, $B_2$), any state $s$ that
does not satisfy Predicate $S$, and any state $s'$ occurring strictly
after $s$, it is the case that $s'.acc_1 = a_{min}$. 
\end{enumerate}
\end{definition}

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

\begin{proof}
Since $B_2$ is {\em Bad}, there exists $B_1$ that is {\em Bad} for
this $B_2$. Using $B_1$, we construct an implementation of \atC, called
$B'_1$, as follows. We add an extra internal variable $stop$,
initially $stop = false$. In any execution of the system \atE(\atA,
$B'_1$, $B_2$),
\begin{enumerate}
\item
$B'_1$ behaves exactly like $B_1$ until Predicate $S$ is violated.
\item
Exactly when $\ssm < 0$, an internal variable $stop$ is set to
$true$. Note that $B'_1$ has enough information (positions and
velocities of both vehicles, $a_{min}$) to detect when $\ssm < 0$.
\item
If $stop = true$, then $acc_1 = a_{min}$.
\end{enumerate}

$B'_1$ preserves the behavior of $B_1$ up to the point when Predicate
$S$ is violated, so $B'_1$ is also {\em Bad} for $B_2$. The second
condition of the {\em VeryBad} definition is satisfied by
construction. So $B'_1$ is {\em VeryBad} for $B_2$.
\end{proof}

\begin{lemma}
\label{lem:bad2}
Let $B_2$ be an implementation of \aatD. If there exists an
implementation $B_1$ of \atsC such that
\atE(\atA, $B_1$, $B_2$) does not implement \atE(\atA, $B_1$, \aatJ)
%$$\{ \pi(\alpha) | \alpha \in h-traces(\atE(\atA, $B_1$, $B_2$)) \}
%\subseteq h-traces(\aatJ)$$
then $B_2$ is Bad.
\end{lemma}

\begin{proof}
We must show that there exists some implementation $B_1$ of \atC, such
that the system \atE(\atA, $B_1$, $B_2$) has a reachable state $s$
that does not satisfy Predicate $S$.

\begin{definition}{Predicate T}
If $\ssm < 0$ then $a_2 = a_{min}$.
\end{definition}

The only restriction of \atsJ (trajectory condition (2.4)) requires
that if {\em collided = false} then Predicate $T$ is satisfied. 

{\em Claim 1.} There
exists $B_1$ such that the system \atE(\atA, $B_1$, $B_2$) has a
reachable state $s$ in which {\em collided = false} and Predicate $T$ is
not satisfied. 

{\em Proof of Claim 1.} Proof by contradiction. Suppose such $B_1$
does not exist. Then, for all implementations $B_1$ of \atC, all the
reachable states of \atE(\atA, $B_1$, $B_2$) in which {\em collided =
false} satisfy Predicate $T$. But then 
all the hybrid traces of \atE(\atA, $B_1$, $B_2$) are allowed by
\atE(\atA, $B_1$, \atJ). It follows that for all implementations $B_1$
of \atC,
\atE(\atA, $B_1$, $B_2$) implements \atE(\atA, $B_1$, \atJ). This contradicts the hypothesis of the Lemma.

{\em Claim 2.} Predicate $S$ is violated in state $s$ of
\atE(\atA, $B_1$, $B_2$) in which Predicate $T$ is not satisfied.

{\em Proof of Claim 2.}
In state $s$, $\ssm < 0$ and $a_2 \not= a_{min}$, since Predicate $T$
is not satisfied. But (because {\em collided = false} in $s$) this means that Predicate $S$ is also violated.
This suffices.

$B_1$ is {\em Bad} for $B_2$ by Claim 2. This proves that $B_2$ is
{\em Bad}.
\end{proof}

Let $B_2$ be {\em Bad} and $B'_1$ be {\em VeryBad} for $B_2$. Then
Lemma \ref{lsr:ma1}, shows that in any hybrid execution of \atE(\atA, $B'_1$,
$B_2$), once Predicate $S$ is violated, it will continue to be violated
throughout the hybrid execution. In Lemma \ref{lsr:ma2} we
show that violation of Predicate $S$ always leads to violation of {\em
  safety}. Finally, Theorem \ref{theo:opt} proves that if for an
implementation $B_2$ there exists an implementation $B_1$ of \atsC
such that \atE(\atA, $B_1$, $B_2$) does not implement \atE(\atA,
$B_1$, \atJ) then this $B_2$ is not a {\em correct} controller.

\begin{lemma} 
\label{lsr:ma1}
Let $B_2$ be Bad, and $B'_1$ be VeryBad for $B_2$. Then, in any execution of \aatE(\aatA, $B'_1$, $B_2$), Predicate $S$ is violated in all
the states that occur strictly after a state $s$ in which
$\mathit{collided} = \mathit{false}$ and Predicate $S$ is violated.
\end{lemma}

\begin{proof}
By induction on the number of steps in a fixed hybrid execution $h$. Suppose
that there exists a state $s$ in $h$ in which {\em collided = false}
and Predicate $S$ is violated. 

Initially, the claim is true vacuously.

The only discrete steps are {\em collide, e} and the internal steps of $B'_1$. The latter two steps cannot change any of the quantities involved. The effect of the {\em collide} step ensures that {\em collided = true} which makes the Lemma true vacuously.

Consider any
trajectory $w$ of $h$, whose domain is the interval $[0,t]$,
that occurs after Predicate $S$ is violated and in which
$\mathit{collided} = \mathit{false}$ throughout the trajectory. From the
definition of $B'_1$, $\ddot{x}_1 = acc_1 = a_{min}$ throughout that trajectory.

Let's apply Lemma \ref{lsr:dec} to our problem. This Lemma states that
if both the right and left derivatives of a function on an interval
are non-positive, then the function is non-increasing on that
interval. Right and left derivatives of \sm are always the right and
left derivatives, respectively, of either $f$ and $g$, as stated in Theorem \ref{th:max}. So we only
have to prove that $\dot{f} \leq 0$ and $\dot{g} \leq 0$ throughout
the interval $[0,t]$. We have:
$$\dot{f} = \dot{x}_1 - \dot{x}_2 + \frac{1}{a_{min}} (\dot{x}_2
\ddot{x}_{2} - \dot{x}_1 \ddot{x}_{1}).$$

By the definition of $B'_1$, we have that
$\ddot{x}_{1} =  a_{min}$. Also, by restriction on \atA,
$\ddot{x}_{2} = acc_2 \geq a_{min}$. Therefore,
\begin{align*}
\dot{f} & = \dot{x}_1 - \dot{x}_2 + \frac{1}{a_{min}} (\dot{x}_2 \ddot{x}_{2} - \dot{x}_1 a_{min}) \\
 & = \dot{x}_1 - \dot{x}_2 + \left( \frac{\dot{x}_2 \ddot{x}_2}{a_{min}} -
\dot{x}_1 \right)\\
 & = \dot{x}_2 \left(\frac{\ddot{x}_2}{a_{min}} - 1\right) \\
 & \leq \dot{x}_2 \left(\frac{a_{min}}{a_{min}} - 1\right) \\
 & = 0.
\end{align*}

Similarly for $\dot{g}$:
\begin{align*}
\dot{g} & = \ddot{x}_{1} - \ddot{x}_{2} \\
 & = a_{min} - \ddot{x}_{2} \\
 & \leq a_{min} - a_{min} \\
 & = 0.
\end{align*}

Therefore, by Lemma \ref{lsr:dec}, \sm is a non-increasing function.
Since in $w(0)$, $\ssm < 0$, \sm is negative throughout the
trajectory, which means that the \atE(\atA, $B'_1$, $B_2$) system
violates Predicate $S$ throughout the trajectory.
\end{proof}

\begin{lemma} \label{lsr:ma2}
Let $B'_1$ be VeryBad for $B_2$. Then there exists a reachable state
$s'$ of \aatE(\aatA, $B'_1$, $B_2$) that does not satisfy safety.
\end{lemma}

\begin{proof}
By the fact that $B'_1$ is {\em VeryBad}, there must exist some reachable state $s$ of
this \atsE system, in which Predicate $S$ is violated. Then, if there
exists a state $s'$, reachable from $s$, in which the vehicles do collide,
then by Lemma \ref{lsr:ma1}, in $s'$, $\ssm < 0$. But that means that
in $s'$, $\dot{x}_2 > \dot{x}_1 + v_{allow}$, violating {\em safety}.
All we have to prove now is that there exists a reachable state $s'$
in which the vehicles do, in fact, collide.

Suppose they don't collide. Since the first vehicle eventually stops (it is decelerating at its maximum rate),  this means that the second one also has to stop. Let $x_i$, $\dot{x}_i$ represent state components in state $s$, and ${x_i}'$ represent the state components of $s'$. Then,
$${x_1}' = x_1 + \frac{{\dot{x}_1}^2}{- 2 a_{min}} \text{ and } {x_2}'
\geq x_2 + \frac{{\dot{x}_2}^2}{- 2 a_{min}}.$$
From our non-collision assumption we get,
\begin{align*}
{x_1}' & \geq {x_2}' + l_2 \\
x_1 + \frac{{\dot{x}_1}^2}{- 2 a_{min}} & \geq x_2 +
\frac{{\dot{x}_2}^2}{- 2 a_{min}} + l_2 \\
x_1 - (x_2 + l_2) & \geq - \frac{{(\dot{x}_2)}^2 - {(\dot{x}_1)}^2} {2a_{min}} \\
x_1 - (x_2 + l_2) & \geq - \frac{{(\dot{x}_2)}^2 - {(\dot{x}_1)}^2 - {(v_{allow})}^2} {2a_{min}},
\end{align*}
which means that $\ssm \geq 0$ in state $s$. But then Predicate $S$ is true in state $s$, contrary to our assumption. 

Therefore, the vehicles do collide in some reachable state $s'$, and $s'$ does not satisfy $\mathit{safety}$.
\end{proof}

Theorem \ref{theo:id-opt} shows that any controller of the trailing vehicle
that does not implement \atsJ, and, therefore, violates Predicate $S$, violates {\em
  safety} for some behavior of the leading vehicle. 

\begin{theorem} \label{theo:opt}
Let $B_2$ be an implementation of \aatD. If there exists an
implementation $B_1$ of \aatC, such that \aatE(\aatA, $B_1$, $B_2$)
does not implement \aatE(\aatA, $B_1$, \aatJ), then $B_2$ is not a
correct controller for \aatA. 
\end{theorem}

\begin{proof}
\label{theo:id-opt}
$B_2$ must be {\em Bad} by Lemma \ref{lem:bad2}. Then, by
Lemma \ref{lem:bad}, there exists an implementation $B'_1$ of \atsC
that is {\em VeryBad} for $B_2$. Lemma \ref{lsr:ma2} shows that the system
\atE(\atA, $B'_1$, $B_2$) has a reachable
state $s'$ that violates {\em safety}, which means that $B_2$ is not
{\em correct}.
\end{proof}

\section{Results}

Theorem \ref{th:impl} shows that the controller \atsG is sufficient for
guaranteeing {\em correctness}, and Theorem \ref{theo:opt} proves that
the controller \atsJ is necessary to guarantee {\em
  correctness}. Combining these two results, we can check correctness,
in terms of {\em safety}, of any implementation $C$ of \atD. $C$ is
correct if it implements \atG, and is not correct if \atE(\atA, $B_1$,
$C$) does not implement \atE(\atA, $B_1$, \atJ) for some
implementation $B_1$ of \atC. Since \atsG and \atsJ differ in
behavior only in the boundary cases, they can be used to check
correctness of most controllers.














