Modeling free flight with collision avoidance.

Free jlight has been proposed as a future alternative to the current policy in Air Trafic Management (ATM) where aircraft follow predefined corridors. In free Pight pilots can choose their own optimal routes, altitudes and velocities but are also responsible for the safe and fair resolution of trajectory conjlicts. This would require a safe distributed control system were the trajectories that aircraft follow are as optimal as possible respecting suficient safety distances. In this paper we model aircraft behaviour using non-determinism in such a way that reachability analysis provides the optimal trajectories of the aircraft. We compare the obtained results with the conflict resolution solutions proposed in the literature.