\chapter{Uncertainty}

Our model already includes both the inbound and the outbound delays in
sending and receiving information between the controller and
\atA. We introduce extra complexity which
makes the model even more realistic: the inbound and outbound
uncertainty (inexactness) in information. 
The inbound uncertainty is the maximum absolute difference between the actual position
and velocity data of the vehicle and the data reported by the sensors
to the controller; it arises from inexact sensors that communicate
data to the controllers. The outbound
uncertainty is the maximum absolute difference between the acceleration commanded by
the controller and the acceleration actually implemented by the
vehicle; it is due to the inherent inexactness in the performance of
the brakes and accelerators. 

We use similar methods to the ones used in the delay case. A
special ``uncertainty buffer'' automaton is defined, similar to
the previous \atsK automaton. We use two instances of this
parameterized buffer to get the inbound and outbound uncertainty.
Then, we compose these two buffers with the modified controller
that accounts for uncertainties, and prove that this new composed
controller is sufficient to guarantee
safety. The proof uses the fact that the \atO(\atN) is
sufficient. This use of
levels of abstraction makes the proofs for this complicated case,
involving both delays and uncertainties, easier to write and understand.

\section{The Uncertainty Buffer}

We introduce a parameterized uncertainty buffer, similar in function to
the delay buffer.

\begin{figure}[ht]

\begin{myiotab}
{\bf Parameters:} \+\\
        $n$ - the number of input variables \\
        $S_i$, $S_o$ - two disjoint sets of variables with $n$
        members in each set \\
        \> Let $V$ be a valuation function, same as in \atK \\
        $var: S_i \rightarrow S_o \times \posr$, with selectors $v_o$
and $\Delta u$ \-\\
{\bf Variables:} \+\\
        Input:\>\>      $S_i$\\
        Output: \>\>    $S_o$ \-\\
{\bf Trajectories:} \+\\
        an $I$-trajectory $w$ is included among the set of nontrivial
        trajectories exactly if \+\\
        1. for all $v_o \in S_o$, $v_o(t)$ is an integrable
function \\
        2. for all $t \in I$, $t > 0$ the following holds for all $v_i
\in S_i$: \+\\
                $V(var(v_i).v_o) \in [V(v_i) - var(v_i).\Delta u, V(v_i) + var(v_i).\Delta u]$

\end{myiotab}
\caption{\atsQ($n$, $S_i$, $S_o$, $var$) Hybrid I/O Automaton}
\label{fig:u-buffer}

\end{figure}

\begin{automaton}{\aatQ($n$, $S_i$, $S_o$, $var$)}
The \atsQ automaton
nondeterministically perturbs all input variables within given bounds
to produce output variables.

\paragraph{Parameters}
\begin{itemize}
\item
$n$ is the number of input variables;
\item
$S_i$, $S_o$ are two disjoint sets of input and output variables, respectively;
\item
$var: S_i \rightarrow S_o \times \posr$ is a 1-1 mapping from input
to pairs consisting of an output variable and an uncertainty bound. So, the input variable
$v_i$ becomes output variable $var(v_i).v_o$, with maximum uncertainty
$var(v_i).\Delta u$, where $v_i \in S_i, v_o \in S_o, \Delta u \in \posr$.
\end{itemize}

\paragraph{Variables} The input and output variables are
parameterized by the $S_i$ and $S_o$ sets. It does not matter for the
generalized automaton which variables it perturbs.

\paragraph{Trajectories} The first restriction guarantees that all
the data is still integrable after the uncertainty buffer. This
is important, because both the controllers and the \atsA automata
integrate the data from the buffers to obtain position and velocity data.
Condition (2) lets outputs vary within given bounds of the inputs. The
bounds are given by the $var(v_i).\Delta u$ function and represent the
maximum absolute value of uncertainty in the data for variable $v_i$. 
\end{automaton}

\begin{theorem}
\label{ub-prop}
In all reachable states $s$ of \aatQ, for all $v_i \in S_i$,
\begin{enumerate}
\item
$s.V(var(v_i).v_o) \geq s.V(v_i) - var(v_i).\Delta u$,
\item
$s.V(var(v_i).v_o) \leq s.V(v_i) + var(v_i).\Delta u.$
\end{enumerate}
\end{theorem}

\begin{proof}
By restriction (2) on trajectories of \atQ.
\end{proof}

\section{The System}

The controller
\atsN is implemented by a composition of three hybrid automata: another controller
\atsT and two instances of the uncertainty buffer --- the inbound and
outbound uncertainty buffers.The composed system is called \atsU (see Figure  \ref{fig:u-in}).

\begin{figure*}[ht]
\center{\PSbox{Fig/Slide4.PS hscale=75 vscale=75}{5.8in}{2.6in}}
\caption{Sensor-Uncertainty Vehicles Model}
\label{fig:u-in}
\end{figure*}

We define two instances of the \atsQ automaton -- the inbound
and outbound uncertainty buffers. These buffers use the following
constants:
\begin{itemize}
\item $\delta$ - the maximum absolute uncertainty in position data;
\item $\dot{\delta}$ - the maximum absolute uncertainty in velocity data;
\item $\ddot{\delta}$ - the maximum absolute uncertainty in acceleration.
\end{itemize}

\begin{automaton}{\aatR}
\atsR = \atQ($3$, $\{x_{d1}, \dot{x}_{d1}, \ddot{x}_{d1}\}$, $\{x_{u1},
\dot{x}_{u1}, \ddot{x}_{u1}\}$, $var$), where $var(x_{d1}) = (x_{u1},
\delta)$, $var(\dot{x}_{d1}) = (\dot{x}_{u1}, \dot{\delta})$, and $var(\ddot{x}_{d1}) = (\ddot{x}_{u1}, \ddot{\delta})$.
This automaton inputs the delayed position, velocity and acceleration data from the
inbound delay buffer \atL, and outputs them with ``uncertainty'' to
the controller \atT.
\end{automaton}

\begin{automaton}{\aatS}
\atsS = \atQ($1$, $\{acc_{u1}\}$, $\{acc_{d1}\}$, $var$), where
$var(acc_{u1}) = (acc_{d1}, \ddot{\delta})$. The outbound uncertainty buffer automaton inputs the
acceleration commands from the controller \atT, and outputs the perturbed values
to the outbound delay buffer \atM. 
\end{automaton}

\begin{figure}[ht]

\begin{myiotab}

{\bf Definition:} \\

\>     $\ssmu = \max(((x_{u1} - \delta) + (\dot{x}_{u1} - \dot{\delta})
t'' + \frac{a_{min} {t''}^2}{2}) - (x_{int2} + \dot{x}_{int2} d_o +
\frac{\ddot{\delta} d_o^2}{2} + l_2)$ \\
\>\>\>\>\>\> $+ \frac{{(\dot{x}_{int2} + \ddot{\delta} d_o)}^2 - {(\dot{x}_{u1} - \dot{\delta} + a_{min} t'')}^2 - {(v_{allow})}^2}{2 a_{min}},$ \\
\>\>\>\>\>\>$(\dot{x}_{u1} - \dot{\delta}) + a_{min} t'' -
(\dot{x}_{int2} + \ddot{\delta} d_o) + v_{allow}),$ \\
\>\> $\text{where } t'' = \min(d_i + d_o, -\frac{\dot{x}_{u1} + \dot{\delta}}{a_{min}})$ \\

{\bf Variables:} \+\\

        Input:\>\>\> $x_{u1}, \dot{x}_{u1} \in \nnr$,
$\ddot{x}_{u1} \in \reals$ \\
                \>\>\>    $x_{2}, \dot{x}_2 \in \nnr$, $\ddot{x}_2 \in
\reals$ \\     
        Output: \>\>\>    $acc_{u2}$, initially if
        $\ssmu \leq 0$, then $acc_{u2} = a_{min} - \ddot{\delta}$, \\
        \>\>\>\>else arbitrary, where $acc_{u2} \geq a_{min}$\\
        Internal: \>\>\> $a_2$ - maps from an interval $[0, d_o]$ to $\reals$, \\
                \>\>\>\>initially, $\forall t \in [0, d_o], a_2(t) = a_{min}-\ddot{\delta}$\\

                \>\>\> $x_{int2}$, $\dot{x}_{int2}$ - the position
and velocity of the second vehicle after time $d_o$ passes, \\
                \>\>\>\> provided $\mathit{collided} =
\mathit{false}$;\\
                \>\>\>\>initially, $\dot{x}_{int2} = \dot{x}_2 +
a_{min} t, x_{int2} = x_2 + \dot{x}_2 t + \frac{a_{min} t^2}{2}$, where
$t = \min(d_o, -\frac{\dot{x}_2}{a_{min}})$. \-\\

{\bf Trajectories:} \+\\

        an $I$-trajectory $w$ is included among the set of nontrivial trajectories exactly if \+\\
        1. $w$ is a trajectory of $\mathit{Controller}_2$ \\

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

                2.1. if in $w(t)$, $\ssmu \leq 0$ then  $acc_{u2} =
                a_{\mathit{min}} - \ddot{\delta}$ else $acc_{u2} \geq a_{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}_{int2} = w(t).\dot{x}_2 +
        {\int_{0}}^{d_o}(w(t).a_2(u) + \ddot{\delta}) du $ \\

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

\end{myiotab}

\caption{\atsT Hybrid I/O Automaton}

\label{fig:u2}

\end{figure}

In the uncertainty case we give a specific controller \atsT that accounts
for uncertainties, and prove
that it is sufficient to guarantee correctness. No specification
controller, or parameterized composition automaton is given in this
case ---
optimality results are not presented, and only sufficiency of a
specific controller is proved. This controller is presented below.

\begin{automaton}{\aatT}
The controller \atsT (shown in figure \ref{fig:u2}) is the same as \atsN except that:
\begin{enumerate}
\item Input and output variables communicate through uncertainty
  buffers; the $a_2$ buffers remembers the new output variable $acc_{u2}$.
\item $\dot{x}_{int2}$ is redefined to account for the
  ``worst'' possible uncertainty in the brake performance, i.e.,
  it assumes that the vehicle accelerates at $acc_{u2} + \ddot{\delta}$.
\item $\ssmu$ is defined to account for the uncertainties. 
\end{enumerate}

\clearpage

The only changes from
\smd are that the first vehicle's data is adjusted to
the ``worst possible'' uncertainty in the behavior of the first vehicle. This ``worst possible''
behavior is defined by the following inequalities:
\begin{enumerate}
\item
$x_{d1} \geq x_{u1} - \delta$;
\item
$\dot{x}_{d1} \geq \dot{x}_{u1} - \dot{\delta}$;
\item
$x_{int2}^{D_2} \leq x_{int2}^{D_2} + \dot{x}_{int2}^{U_2} d_o +
\frac{\ddot{\delta} d_o^2}{2}$;
\item
$\dot{x}_{int2}^{D_2} \leq \dot{x}_{int2}^{U_2} + \ddot{\delta} d_o$;
\end{enumerate}

These inequalities are used in changing $\ssmd$ to \smu. The proof of
these relationships is given below, in Theorem \ref{theo:u-prop}.

\end{automaton}

\begin{automaton}{\aatU}
\atsU = VarHide($\{x_{u1}$, $\dot{x}_{u1}$, $\ddot{x}_{u1}$, $acc_{u1}\}$, \atsR
$\parallel$ \atsT $\parallel$ \atS), is the composition of the
uncertainty buffers with the new controller. We show that it
implements \atN in the context of the \atsE system. This
automaton is not parameterized by the choice of the controller, unlike
the previous composed controllers. No parameterization is necessary
because only sufficiency of the specific controller \atsT is proven.
\end{automaton}

\begin{theorem}
\label{theo:u-prop}
Let $A_1$ be any implementation of \aatC. Then, in any reachable state
$s$ of the \aatE(\aatAA, $A_1$, \aatO(\aatU)) system such that $s.collided =
false$, the following hold:
\begin{enumerate}
\item
$acc_{d2} \leq acc_{u2} + \ddot{\delta}$;
\item
$x_{d1} \geq x_{u1} - \delta$;
\item
$\dot{x}_{d1} \geq \dot{x}_{u1} - \dot{\delta}$;
\item
$\ddot{x}_{d1} \geq \ddot{x}_{u1} - \ddot{\delta}$;
\item
$x_{int2}^{D_2} \leq x_{int2}^{U_2} + \dot{x}_{int2}^{U_2} d_o +
\frac{\ddot{\delta} d_o^2}{2}$;
\item
$\dot{x}_{int2}^{D_2} \leq \dot{x}_{int2}^{U_2} + \ddot{\delta}
d_o$.
\end{enumerate}
\end{theorem}

\begin{proof}
Claim (1) follows from Property 2 of \atQ; claims (2)-(4) follow from
Property 1 of \atQ. Finally, claims (5) and (6) follow from claim (1)
of this theorem and Property 2 of \atsAA (position and velocity are
integrals of acceleration).
\end{proof}

Note that the symmetric properties also hold, but these are the
relationships that are used later on in the proofs.

\section{Correctness of \atT}

As in the delayed case, we want to simulate
the previous delayed system using the new uncertain
system, and thus
show that the new controller is sufficient.

Throughout this section we will use the following notation: for any
implementation $A_1$ of \atC, let

$CV_U(A_1)$ = \atE(\atA, $A_1$, \atO(\atU)), and

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

%In this case we cannot simulate \atsN by a combination of \atsT and
%  the uncertainty buffers using an identity relation, like we did in
%the previous chapters. The reason is that \atsT outputs $a_{min}
%  - \ddot{\delta}$ in an emergency, which \atsN never outputs (it
%  outputs $a_{min}$). The \atsT has to add that
%  $\ddot{\delta}$ factor to ensure that the vehicle executes
%  $a_{min}$. If it commanded $a_{min}$, then the \atsAA automaton could
%execute $a_{min} + \ddot{\delta}$ because of the outbound uncertainty. However, the \atsA automaton will make sure that nothing less than $a_{min}$
%  would ever get executed. This model is realistic, since it makes the
%  vehicle check the deceleration settings, by ``hard-wiring'' the
%  lowest possible deceleration the brakes can provide. This means that
% if the controller asks for very high deceleration rate, the vehicle would
%  just decelerate at the maximum possible rate. 

%Since we cannot simulate \atsN with \atsU using an identity
%relation, we construct a new simulation relation $f$ to account for this
%difficulty: the simulation relation $f$ from the system composed of
%\atsT and the uncertainty buffers to \atsN is the identity on all
%state components of \atN, except that $acc_{d2}^{delay} =
%\text{max}(a_{min}, acc_{d2}^{uncert})$. Since the \atsA automaton
%actually implements the restriction of this simulation relation, this
%is enough to prove correctness of the new system with delays and
%uncertainties.

First we show that if the old \smd (the one used in
the delayed case) is non-positive in some state of
\atU, then the new controller \atsT (the one that has
inbound and outbound uncertainty), also outputs maximum
deceleration. Formally, 

\begin{lemma} \label{un:sm}
Let $A_1$ be any implementation of \aatC, and let $s$ be a reachable state of the $CV_U(A_1)$ system, such that $s.\mathit{collided} = {false}$
and $\ssmd \leq 0$. Then, $\ssmu \leq 0$ and $s.acc_{u2} = a_{min} - \ddot{\delta}$.
\end{lemma}

\begin{proof}
Initially, the lemma is true by restriction on initial conditions of
\atU. Consider any reachable state $s$ of $CV_U(A_1)$, such that $s.\mathit{collided}
= \mathit{false}$ and \smd $\leq 0$. At $s$ we have
\begin{equation} \label{un:alt1}
(x_{d1} + \dot{x}_{d1} t' + \frac{a_{min} {t'}^2}{2}) - (x_{int2}^{D_2} +
l_2) + \frac{{(\dot{x}_{int2}^{D_2})}^2 - {(\dot{x}_{d1} + a_{min}
    t')}^2 - {(v_{allow})}^2}{2 a_{min}} \leq 0
\end{equation}
and
\begin{equation} \label{un:alt2}
\dot{x}_{d1} + a_{min} t' + v_{allow} - \dot{x}_{int2}^{D_2} \leq 0
\end{equation}
where $t' = \min(d_i + d_o, - \frac{\dot{x}_{d1}}{a_{min}})$.

Let $t'' = min(d_i + d_o, -\frac{\dot{x}_{int2}^{D_2} +
\dot{\delta}}{a_{min}})$. Then, by Theorem \ref{theo:u-prop}, in $s$,
\begin{enumerate}
\item
$x_{d1} \geq x_{u1} - \delta$;
\item
$\dot{x}_{d1} \geq \dot{x}_{u1} - \dot{\delta}$;
\item
$x_{int2}^{D_2} \leq x_{int2}^{U_2} + \dot{x}_{int2}^{U_2} d_o +
\frac{\ddot{\delta} d_o^2}{2}$;
\item
$\dot{x}_{int2}^{D_2} \leq \dot{x}_{int2}^{U_2} + \ddot{\delta}
d_o$.
\end{enumerate}

Using the above inequalities, we replace each delayed variable
($x_{d1}$, $\dot{x}_{d1}$, $x_{int2}^{D_2}$, $\dot{x}_{int2}^{D_2}$) in inequalities \ref{un:alt1} and \ref{un:alt2} with an expression that is
smaller than the delayed variable, and using only
the ``uncertain'' values, which are the ones known to \atT. 
Then, we get exactly the two parts of
$\ssmu$; moreover, since we used only smaller values, the
resulting expressions are still non-positive. So, $$\ssmu \leq 0$$ 
Then, by the definition of \atT, $acc_{u2} = a_{min} - \ddot{\delta}$,
as needed.
\end{proof}

\begin{lemma} \label{un:sim}
Let $A_1$ be any implementation of \aatC, and let $f$ be an identity relation on all state components of
$CV_D(A_1)$, except that $acc_{d2}^{CV_D} = \max(acc_{u2}^{CV_U},
a_{min})$. Then $f$ is a simulation from $CV_U(A_1)$ to $CV_D(A_1)$.
\end{lemma}

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

\paragraph{Start States:} The restrictions on start states of $CV_D(A_1)$
and $CV_U(A_1)$ are identical. 

\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_d$ vacuously, thus
the state reached after the {\em collide} action is a valid state of
$CV_D(A_1)$.

\paragraph{Trajectories:}
Suppose that $w_U$ is an $I$-trajectory of the uncertainty-buffered
system $CV_U(A_1)$ and its first state $s_U$ is reachable. Suppose that $s_D$
is a reachable state of $CV_D(A_1)$ such that $(s_U, s_D) \in f$. Then let
the corresponding hybrid execution fragment of $CV_D(A_1)$ consist of a
single trajectory $w_D$, where all the state components in all the
states of $w_D$ are equal to corresponding components in $w_U$, except
that $w_D.acc_{d2} = \max(w_U.acc_{d2}, a_{min})$. It
is clear 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_D$ is in fact a trajectory
of $CV_D(A_1)$. In particluar, we must show that the projections of
$w_D$ on the components of $CV_D(A_1)$ are allowed by these
components. 

First, we show that $w_D$ is allowed by the \atO(\atN) controller. By
the definition of a trajectory we must show that
\begin{enumerate}
\item $w_D$ is allowed by $\mathit{Controller}_2$. 

This is trivial, since it is also a restriction on the trajectories of \atT,
  and the buffers preserve these conditions by preserving
  integrability.
\item
If $\mathit{collided} = \mathit{false}$ in $w_D(0)$ then $\forall t
\in I$ such that
$\mathit{safe}\text{-}\mathit{measure}_d \leq 0$ we have
$w_D(t).acc_{d2} = a_{min}$.

Consider the trajectory $w_U$ of $CV_U(A_1)$. Since \smd uses
the same variables with the same values in both the $CV_D(A_1)$ and
the $CV_U(A_1)$ systems, we can apply Lemma \ref{un:sm}, so that
$w_U(t).acc_{u2} = a_{min} - \ddot{\delta}$. By Theorem 
\ref{theo:u-prop}, in all reachable states $s$ of $CV_U(A_1)$, $s.acc_{d2} \leq
s.acc_{u2} + \ddot{\delta}$, so $w_U(t).acc_{d2} \leq a_{min}$. Then,
using the definition of trajectory $w_D$,
$$w_D(t).acc_{d2} = \max(w_U(t).acc_{d2}, a_{min}) = a_{min},$$
as needed.
\end{enumerate}

We also show that the projection of $w_D$ on \atsA is
allowed by \atA, and has the same hybrid trace as $w_U$.

We know that $w_U$ is allowed by \atA. But $w_D$ is exactly the same as
$w_U$, except for the input variable $acc_2$. Also, since all the
variables are the same, the hybrid trace of $w_D$ and $w_U$ is the
same. Thus, we only need to
show that the condition (3) of \atsA trajectories, namely, that
$w_D.\ddot{x}_2 = \max(w_D.acc_2, a_{min})$, is preserved.

By the definition of $w_D$, $w_D(t).\ddot{x}_2 = w_U(t).\ddot{x}_2$
for all $t$ throughout the trajectory. By restriction (3) on
trajectories of \atA, $w_U(t).\ddot{x}_2 = \max(w_U(t).acc_2,
a_{min})$. Also, by the definition of $w_D$, $w_D(t).acc_2 =
\max(w_U(t).acc_2, a_{min})$. Putting these equations together we get
$$w_D(t).\ddot{x}_2 = w_U(t).\ddot{x}_2 = \max(w_U(t).acc_2, a_{min}) =
w_D(t).acc_2 = \max(w_D(t).acc_2, a_{min}).$$

Therefore, $w_D$ is a valid trajectory of \atA.

\end{proof}

\begin{theorem}
\aatO(\aatU) is a correct controller for \aatA.
\end{theorem}

\begin{proof} We need to prove that for any implementation $A_1$ of
  \atC, $CV_U(A_1)$, implements \atF.
By Lemma \ref{un:sim}, there
is a simulation relation $f$ from $CV_U(A_1)$ to $CV_D(A_1)$. Since $CV_U(A_1)$ and $CV_D(A_1)$
are comparable, $CV_U(A_1)$ implements $CV_D(A_1)$.

By Theorem \ref{theo:del}, \atO(\atN) is {\em correct}, which means that $CV_D(A_1)$
implements \atF. Then, since $CV_U(A_1)$ implements $CV_D(A_1)$, $CV_U(A_1)$
also implements \atF. It follows that
\atO(\atU) is {\em correct}.
\end{proof}

\section{Optimality}

We do not present a necessary controller here, as opposed to the
controllers considered in the previous chapters. Before, we always
made \sm to account for the ``worst-case'', but possible,
conditions. Then, we were able to prove necessity by making the first
vehicle have its worst possible behavior. However, with the
uncertainty involved, we did not make \sm as tight as
possible. The problem is that in our analysis, the position and
velocity data are used independently. However, the
position and velocity data are dependent upon each other, and thus we
could use the relationship between the two values to get
tighter approximations to their real values, resulting in a more optimal
controller. We did not model it this way because it is not realistic:
in most situations it is impractical to deduce the tighter
bounds, since just calculating these bounds takes too much time,
eliminating any benefits obtained from using tighter bounds. This would ultimately decrease the
performance, instead of improving it.

%If we assume, however, that the position and velocity data are
%independent, and there always exists a possibility of both values
%being the ``most uncertain'' simultaneously (as is probably the case
%in practice), then the controller that is identical to \atT, but with
%a different behavior on the \smu boundary, gives necessary conditions for correctness. The proof would be
%very similar to the proof of the fact that \atsV is necessary.

