SMT-Based Aircraft Conflict Detection and Resolution

Saswata Paul, Baoluo Meng, Christopher Alexander

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

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.

Original languageEnglish
Title of host publicationNASA Formal Methods - 16th International Symposium, NFM 2024, Proceedings
EditorsNathaniel Benz, Divya Gopinath, Nija Shi
PublisherSpringer Science and Business Media Deutschland GmbH
Pages186-203
Number of pages18
ISBN (Print)9783031606977
DOIs
Publication statusPublished - 2024
Externally publishedYes
Event16th International Symposium on NASA Formal Methods, NFM 2024 - Moffett Field, United States
Duration: 4 Jun 20246 Jun 2024

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume14627 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference16th International Symposium on NASA Formal Methods, NFM 2024
Country/TerritoryUnited States
CityMoffett Field
Period4/06/246/06/24

Keywords

  • Autonomous Navigation
  • Constraint Solving
  • SMT-Based Deconfliction
  • UAS Traffic Management
  • Urban Air Mobility

Fingerprint

Dive into the research topics of 'SMT-Based Aircraft Conflict Detection and Resolution'. Together they form a unique fingerprint.

Cite this