Safety Verification for Urban Air Mobility Scheduling

In Urban Air Mobility (UAM) networks, takeoff and landing sites, called vertiports, are likely to experience intermittent closures due to, e.g., adverse weather. For safety, it will be required that all in-transit Urban Air Vehicles (UAVs) in a UAM network have alternative landing sites in the event of a vertiport closure. In this paper, we propose analytical conditions for developing an efficient algorithm that, given a proposed UAM schedule, verifies whether all UAVs are able to safely reach a back-up landing site in the event of a vertiport closure without violating the limited landing capacity of each vertiport in the network. If safety verification is not possible, the algorithm returns a counterexample demonstrating the violation. Our solution allows for uncertain travel time between UAM vertiports and scales quadratically with the number of scheduled UAVs. We demonstrate our algorithm on a UAM network with up to 1,000 UAVs.Copyright (c) 2022 The Authors. This is an open access article under the CC BY-NC-ND license (https://creativecommons.org/licenses/by-nc-nd/4.0/)