A Three-Level Analysis of a Vehicle Acceleration Maneuver 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'', acc, to an arbitrary real number. However, the actual acceleration exhibited by the vehicle need not be exactly equal to acc -- instead, we assume that it is defined by an integrable function whose values are always in the range [acc - epsilon, acc]. (We could also have included some uncertainty in the upper bound, but that would not add any interesting features to the example.) We can think of this uncertainty as representing, say, uncertainty in the performance of the vehicle's propulsion system. 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 [b - epsilon d,b]. That is, the uncertainty in setting acc combines multiplicatively with the sampling period to yield the uncertainty in the final velocity of the vehicle. More strongly, we obtain a range for the velocity of the vehicle at each time in the interval [0,a]. 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 levels of abstraction, a standard method for reasoning about discrete systems, in reasoning about hybrid control problems. We use levels of abstraction here for two purposes: (a) To express the relationship between a derivative-based description of a system and an explicit description. (b) To express the relationship between a system in which corrections are made at discrete sampling points and a system in which corrections are made continuously. The uncertainty in the acceleration is treated at all three levels of our example, and is integrated throughout the presentation. 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. Related Publications Nancy Lynch. A Three-Level Analysis of a Simple Acceleration Maneuver, with Uncertainties. Proceedings of the Third AMAST Workshop on Real-Time Systems, Salt Lake City, Utah, pages 1-22, March 1996. Paper Also in AMAST Workshops on Real-Time Systems 95 & 96, published by World Scientific Publishing Company, in the AMAST Series in Computing. .pdf

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