Delay predictive models of the national airspace system using hybrid control theory

We present a model for analyzing and simulating the propagation of delays through several sectors of the Oakland Air Route Traffic Control Center. Aircraft are represented as points moving along straight lines with constant velocity, and the air traffic controller is modelled as an action which can provide instantaneous heading and velocity changes to each aircraft. If the controller action is restricted to one velocity change per aircraft, we show that the problem of computing the time that the controller action must be applied in order to achieve an exact metering constraint on the spacing between aircraft, may be solved analytically. More generally, the problem of computing the time that controller action must be applied on each aircraft, in order to satisfy a metering constraint and minimize the overall arrival time, may be posed and solved as, a linear program. We show that cases involving heading change may be solved analytically using the theorem prover STeP. Finally, we validate our results through our simulator of air traffic control action in the Oakland Center.