A Three-Level Analysis of a Vehicle AccelerationManeuver with Uncertainties |

We give a three-level analysis of a toy vehicle
acceleration maneuver.
The goal of the maneuver is to cause a vehicle, starting at
velocity 0 at time 0,
to attain a velocity of b (or as close to b as possible) at a
later time a.
The vehicle is assumed to provide accurate sampled data every d time
units.
The vehicle is assumed to be capable of receiving control signals,
one immediately after each vehicle data output.
Each control signal can set an ``acceleration variable'',
The vehicle interacts with a controller, presumably a computer.
In this note, we describe a particular controller and analyze the
behavior of the combination of the vehicle and controller.
A conclusion we draw is that the velocity of the vehicle at time a
is in the range We prove this fact using invariants and levels of abstraction (in particular, forward simulation methods), based on a (slight) variant of the Lynch-Vaandrager timed automaton model. Many of the pieces of the proofs use standard continuous methods, such as solving algebraic and differential equations. The entire proof represents a smooth combination of discrete and continuous methods.
The point of this exercise is to demonstrate some simple uses of
We do not claim to contribute anything new in the way of techniques for continuous mathematics; for example, we adopt standard methods of solving differential equations. Our contributions lie, rather, in the smooth combination of discrete and continuous methods within a single mathematical framework, and in the application of standard methods of discrete analysis (in particular, invariants and levels of abstraction) to hybrid systems. Our methods are particularly good at handling uncertainties and other form of system nondeterminism.
Nancy Lynch. |

TOC /
LCS /
MIT Last modified: Fri Jan 16 15:01:26 1998 |
Comments? |