  The design of aircraft collision avoidance algorithms is a subtle but
important challenge that merits the need for provable safety guarantees.
Obtaining such guarantees is nontrivial given the unpredictability of the
interplay of the intruder aircraft decisions, the ownship pilot reactions, and
the subtlety of the continuous motion dynamics of aircraft. Existing collision
avoidance systems, such as TCAS and the Next-Generation Airborne Collision
Avoidance System ACAS X, have been analyzed assuming severe restrictions on the
intruder's flight maneuvers, limiting their safety guarantees in real-world
scenarios where the intruder may change its course. This work takes a
conceptually significant and practically relevant departure from existing ACAS
X models by generalizing them to hybrid games with first-class representations
of the ownship and intruder decisions coming from two independent players,
enabling significantly advanced predictive power. By proving the existence of
winning strategies for the resulting Adversarial ACAS X in differential game
logic, collision-freedom is established for the rich encounters of ownship and
intruder aircraft with independent decisions along differential equations for
flight paths with evolving vertical/horizontal velocities. We present three
classes of models of increasing complexity: single-advisory infinite-time
models, bounded time models, and infinite time, multi-advisory models. Within
each class of models, we identify symbolic conditions and prove that there then
always is a possible ownship maneuver that will prevent a collision between the
two aircraft.
