Formally Verified Timing Computation for Non-deterministic Horizontal Turns During Aircraft Collision Avoidance Maneuvers.

We develop a library of proofs to support rigorous mathematical reasoning about horizontal aircraft turning maneuvers, and apply it to formally verify a timing computation for use during mixed horizontal and vertical aircraft collision avoidance maneuvers. We consider turns that follow non-deterministic circular turn-to-bearing horizontal motion, formalizing path-length and timing properties. These kinematics are the building blocks for Dubins trajectories, and can be used to formalize a variety of techniques, including those that contain non-determinism. The timing computation establishes, for intersecting trajectories, the exact bounds of time intervals when the horizontal position of the aircraft might coincide, and during which they must be at different altitudes to avoid collision.