Abstract
Urban air mobility (UAM) refers to on-demand air transportation services within an urban area. We seek to perform mission planning for vehicles in a UAM fleet, while guaranteeing system safety requirements such as traffic separation. In this paper, we present a localized hierarchical planning procedure for the traffic management problem of a fleet of (potentially autonomous) UAM vehicles. We apply decentralized policy synthesis for route planning on individual vehicles, which are modeled by Markov decision processes. We divide the operating region into sectors and use reactive synthesis to generate local runtime enforcement modules or shields, each of which satisfies its own assume-guarantee contract that encodes requirements of conflict management, safety, and interactions with neighbouring sectors. We prove that the realization of these contracts ensures that the entire network of shields satisfies the safety specifications with each shield limited to acting in its local sector of operation.
Original language | English |
---|---|
Title of host publication | NASA Formal Methods - 11th International Symposium, NFM 2019, Proceedings |
Editors | Kristin Yvonne Rozier, Julia M. Badger |
Pages | 71-87 |
Number of pages | 17 |
DOIs | |
State | Published - 2019 |
Event | 11th International Symposium on NASA Formal Methods, NFM 2019 - Houston, United States Duration: May 7 2019 → May 9 2019 |
Publication series
Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 11460 LNCS |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 11th International Symposium on NASA Formal Methods, NFM 2019 |
---|---|
Country/Territory | United States |
City | Houston |
Period | 5/7/19 → 5/9/19 |
Bibliographical note
Publisher Copyright:© Springer Nature Switzerland AG 2019.
Funding
The authors would like to thank Ali Husain and Dr. Bruce Porter from Spark-Congition Inc. for inspiring discussions. This work was supported in part by grantsAFRLFA 8650-15-C-2546 and DARPAW911NF-16-1-0001. Acknowledgement. The authors would like to thank Ali Husain and Dr. Bruce Porter from Spark-Congition Inc. for inspiring discussions. This work was supported in part by grants AFRL FA 8650-15-C-2546 and DARPA W911NF-16-1-0001.
Funders | Funder number |
---|---|
Defense Advanced Research Projects Agency | W911NF-16-1-0001 |
Air Force Research Laboratory | FA 8650-15-C-2546 |
Keywords
- Air traffic management
- Reactive synthesis
- System safety
ASJC Scopus subject areas
- Theoretical Computer Science
- General Computer Science