Model checking evaluation of airplane landing trajectories

Computing trajectories of a set of airplanes in their final descent is an important problem in air traffic control. It consists of deciding a trajectory, the runway, and the landing time for each airplane, such that several constraints are satisfied, while optimizing flying (fuel) costs, and minimizing waiting times. To solve this problem, we model it as a discrete game, the "k-king" puzzle, in which each airplane is represented (and it moves) as a king chess-piece on a chess-board. Although the model has already been introduced in the past, we propose several extensions, taking into account different aspects of the real problem, such as constrained airspaces, distinct airplane speeds, various separation distance among airplanes, and specific restrictions in the landing trajectories. Moreover, we model both "static" and "dynamic" cases for 2D and 3D airspaces. On these extensions, we describe an "exact" resolution method based on ideas and algorithms coming from the formal verification of correctness of hardware devices and software tools area. Furthermore, to improve the size, and complexity, of the models we are able to deal with, we propose a decomposition technique based on the divide-and-conquer paradigm. This solution, which we call "Plane by Plane" decomposition, trades-off between accuracy and efficiency, i.e., exact solutions degrade to non-optimal ones to maintain scalability. We finally propose an implementation of this algorithm based on (and taking advantages of) modern multi-core, multi-threaded, systems. We present a detailed description of the model and the algorithms, as well as our computational results for quite large static and dynamic 2D and 3D problems.