KB3D Release 1.b (5/16/07)

Remark

KB3D is no longer maintained. It has been replaced by ACCoRD, a framework for the design and verification of state-based conflict detection and resolution algorithms. In addition to all the capabilities offered by KB3D, ACCoRD also provides:

Better algorithms and better interfaces.
Loss of separation recovery.
Prevention bands

KB3D is an algorithm for conflict detection and resolution in a 3-dimensional airspace for two aircraft, namely ownship and traffic. The development of KB3D was supported by NASA's Distributed Air/Ground Traffic Management (DAG-TM) Project and it is currently supported by NASA's Next Generation of Air Traffic Systems (NGATS)

A conflict is a projected incursion of the traffic aircraft within the protected zone of the ownship. A resolution is a single maneuver, to be performed by the ownship, that effectively keeps the required minimum separation. Four kind of resolutions are provided: ground track only, ground speed only, vertical speed only, and a combination of track and ground speed that is geometrically optimal (see KB2D).

KB3D resolutions are coordinated in the sense that if the traffic aircraft maneuvers to solve the conflict at the same time as the ownship maneuvers, the resulting trajectories are repulsive. However, the resolution keeps separation even if the traffic does not maneuver.

KB2D is the algorithm that implements a combination of track and ground speed that is geometrically optimal. RR3D is the algorithm that implement recovery courses with a time arrival constraint. CD3D is the conflict detection algorithm used by KB3D.

Last but not least, KB3D, KB2D, RR3D, and CD3D have been formally verified in the Prototype Verification System (PVS).

KB3D Reference Manual - Version 1.a.

CD3D soundness and correctness proofs in PVS 4.1.

KB3D correctness proof in README, PVS 4.1.

KB2D correctness proof in PVS 4.1.

RR3D correctness proof in PVS PVS 2.4 and PVS 3.1.

Papers about KB3D, KB2D, and RR3D

Conflict Detection and Resolution for 1,2,..,N Aircraft, Gilles Dowek and César Muñoz, 7th AIAA Aviation Technology, Integration and Operations Conference, BibTex Reference, 2007.
Formal Verification of an Optimal Air Traffic Conflict Resolution and Recovery Algorithm, André Galdino, César Muñoz, and Mauricio Ayala, 14th Workshop on Logic, Language, Information and Computation, BibTex Reference, 2007.
KB3D Reference Manual - Version 1.a, César Muñoz, Radu Siminiceanu, Víctor Carreño, and Gilles Dowek, NASA/TM-2005-213769, BibTex Reference, 2005.
Provably Safe Coordinated Strategy for Distributed Conflict Resolution, Gilles Dowek, César Muñoz, and Víctor Carreño, AIAA Guidance Navigation, and Control Conference and Exhibit 2005, BibTeX Reference, 2005.
Jeffrey Maddalon, Ricky Butler, Alfons Geser and César Muñoz, Formal Verification of a Conflict Resolution and Recovery Algorithm, NASA/TP-2004-213015, BibTex Reference, 2004.
Ricky Butler, Alfons Geser, Jeffrey Maddalon, and César Muñoz, Formal Analysis of Air Traffic Management Systems: The case of Conflict Resolution and Recovery, Proceedings of the 2003 Winter Simulation Conference, WSC 2003, BibTex Reference, 2003.
Alfons Geser and César Muñoz, A Geometric Approach to Strategic Conflict Detection and Resolution, Proceedings of the 21st Digital Avionics Systems Conference, DASC 2002, BibTex Reference, 2002.
Alfons Geser, César Muñoz, Gilles Dowek, and Florent Kirchner, Air Traffic Conflict Resolution and Recovery, ICASE Report 2002-12, BibTex Reference, 2002.
Gilles Dowek, Alfons Geser, and César Muñoz, Tactical Conflict Detection and Resolution in a 3-D Airspace, Proceedings of the Fourth International Air Traffic Management R&D Seminar ATM 2001, BibTeX Reference, 2001. Extended version available as ICASE Report 2001-7, BibTeX Reference, 2001.

Maintained by: César A. Muñoz