Formally Verified Next-Generation Airborne Collision Avoidance Games in ACAS X

TL;DR

This paper introduces a formally verified, game-theoretic model of aircraft collision avoidance in ACAS X, providing provable safety guarantees for complex, adversarial flight scenarios through differential game logic.

Contribution

It generalizes ACAS X to hybrid games with independent decision-makers and proves the existence of safe strategies using differential game logic.

Findings

Proved collision-freedom in complex aircraft encounter models.

Developed symbolic conditions for safe maneuvers.

Established the existence of winning strategies for ownship.

Abstract

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.