Hybrid control of air traffic management systems

Today's crowded skies and ever-increasing demand for air travel, coupled with new technologies for navigation and surveillance, are fueling a change in the way that the Federal Aviation Administration manages air traffic. Current Air Traffic Control (ATC) practice manually routes aircraft along predefined paths between "fixes", using radar track and flight information from plan view displays and voice communication over radio channels. The use of Global Positioning Systems and datalink communication will enable automation of some ATC functionality, such as the prediction and resolution of trajectory conflicts between aircraft. For such a safety critical system, the integrity and acceptance of new automated control functionality depends on a provably-safe design, which requires accurate system models, and procedures for verifying and synthesizing safe control actions.; We present a model and controller synthesis scheme for a nonlinear hybrid automaton, a system that combines discrete event dynamics with nonlinear continuous dynamics. The discrete event dynamics model linguistic and qualitative information, such as the flight mode of an aircraft or the interaction between several aircraft. Discrete event models also naturally accommodate mode switching logic, which is triggered by events internal or external to the system. The continuous dynamics model the physical processes themselves, such as the continuous response of an aircraft to the forces of aileron and throttle. Our model includes input variables to model both continuous and discrete control and disturbance parameters.; We translate safety specifications into restrictions on the system's reachable sets of states. Then, using analysis based on two-person zero-sum game theory for automata and continuous dynamical systems, we derive Hamilton-Jacobi equations whose solutions describe the boundaries of reachable sets. These equations are the heart of our general controller synthesis technique for hybrid systems, in which we calculate feedback control laws for the continuous and discrete variables which guarantee that the hybrid system remains in the "safe subset" of the reachable set. We present the extension of a level set method to compute numerical solutions of the Hamilton-Jacobi equations. Throughout, we demonstrate our techniques on examples of interesting nonlinear hybrid automata modeling aircraft conflict resolution and autopilot flight mode switching.