Traffic Management for Urban Air Mobility

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.