% $Log: abstract.tex,v $
% Revision 1.1  93/05/14  14:56:25  starflt
% Initial revision
% 
% Revision 1.1  90/05/04  10:41:01  lwvanels
% Initial revision
% 
%
%% The text of your abstract and nothing else (other than comments) goes here.
%% It will be single-spaced and the rest of the text that is supposed to go on
%% the abstract page will be generated by the abstractpage environment.  This
%% file should be \input (not \include 'd) from cover.tex.

In this thesis we formally model a  system consisting of two
vehicles moving along a single track, plus controllers that operate the
vehicles, plus communication channels. The modeling formalism used is
the Hybrid Automata model developed by Lynch, Segala, Vaandrager and
Weinberg. We formulate a
key safety requirement of such a system, namely, that
the two vehicles never collide at a relative velocity greater than a
given bound, $v_{allow}$. We give necessary and sufficient conditions
for the controller of the follower vehicle to guarantee that the safety
requirement is satisfied
regardless of the behavior of the leading vehicle. The model includes
handling of communication delays and uncertainty. The proofs use
composition, invariants, and levels of abstraction, together with methods
of mathematical analysis. This case study is derived from the
California PATH intelligent highway project. 
