Safe Schedule Verification for Urban Air Mobility Networks With Node Closures

In urban air mobility (UAM) networks, takeoff and landing sites, called vertiports, are likely to experience intermittent closures due to, e.g., adverse weather. To ensure safety, all in-flight urban air vehicles (UAVs) in a UAM network must therefore have alternative landing sites with sufficient landing capacity in the event of a vertiport closure. In this article, we study the problem of safety verification of UAM schedules in the face of vertiport closures. We first provide necessary and sufficient conditions for a given UAM schedule to be safe in the sense that if a vertiport closure occurs, then all UAVs will be able to safely land at a backup landing site. We then extend these results to the scenario of multiple vertiport closures. Next, we convert these conditions into an efficient algorithm for verifying the safety of a UAM schedule via a linear program by using the properties of totally unimodular matrices. Our algorithm 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 1000 UAVs.