TY - GEN
T1 - SMT-Based Aircraft Conflict Detection and Resolution
AU - Paul, Saswata
AU - Meng, Baoluo
AU - Alexander, Christopher
N1 - Publisher Copyright:
© The Author(s), under exclusive license to Springer Nature Switzerland AG 2024.
PY - 2024
Y1 - 2024
N2 - The integration of Unmanned Aircraft Systems (UAS) in the National Airspace System (NAS) for Urban Air Mobility (UAM) operations will create the need to develop robust, efficient, and verifiable tools and techniques for UAS Traffic Management (UTM). In this paper, we present a novel approach for strategic detection and resolution of airborne conflicts using Satisfiability Modulo Theories (SMT) solvers. Our approach takes a flight plan for an ownship, a set of immutable flight plans for traffic aircraft, and a set of constraints, and then returns a flight plan for the ownship that satisfies all constraints and is also conflict free with respect to the traffic aircraft. The constraints can relate to operational, business, or other aspects which must be considered while setting up the conflict resolution task as a constraint satisfaction problem. We present simulations of our approach using a prototype implementation based on dReal, an SMT solver that is specialized for solving non-linear real function problems, showing promising results.
AB - The integration of Unmanned Aircraft Systems (UAS) in the National Airspace System (NAS) for Urban Air Mobility (UAM) operations will create the need to develop robust, efficient, and verifiable tools and techniques for UAS Traffic Management (UTM). In this paper, we present a novel approach for strategic detection and resolution of airborne conflicts using Satisfiability Modulo Theories (SMT) solvers. Our approach takes a flight plan for an ownship, a set of immutable flight plans for traffic aircraft, and a set of constraints, and then returns a flight plan for the ownship that satisfies all constraints and is also conflict free with respect to the traffic aircraft. The constraints can relate to operational, business, or other aspects which must be considered while setting up the conflict resolution task as a constraint satisfaction problem. We present simulations of our approach using a prototype implementation based on dReal, an SMT solver that is specialized for solving non-linear real function problems, showing promising results.
KW - Autonomous Navigation
KW - Constraint Solving
KW - SMT-Based Deconfliction
KW - UAS Traffic Management
KW - Urban Air Mobility
UR - http://www.scopus.com/inward/record.url?scp=85195449423&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-60698-4_11
DO - 10.1007/978-3-031-60698-4_11
M3 - Conference contribution
AN - SCOPUS:85195449423
SN - 9783031606977
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 186
EP - 203
BT - NASA Formal Methods - 16th International Symposium, NFM 2024, Proceedings
A2 - Benz, Nathaniel
A2 - Gopinath, Divya
A2 - Shi, Nija
PB - Springer Science and Business Media Deutschland GmbH
T2 - 16th International Symposium on NASA Formal Methods, NFM 2024
Y2 - 4 June 2024 through 6 June 2024
ER -