Good Fences Make Good Neighbors: Using Formally Verified Safe Trajectories to Design a Predictive Geofence Algorithm

For AI-controlled mobile platforms, avoiding collisions with walls and boundaries is an important safety requirement. This is a problem especially for fast-moving aerial vehicles, such as fixed-wing aircraft, that cannot be brought to a stop in an emergency. To enable geographic confinement of such AI-controlled vehicles, we present a formally verified algorithm for predicting geofence violations and selecting a safe maneuver that will keep the vehicle within the designated operations area. The algorithm is based on a higher-order dynamics model that generalizes circular turns using linearly changing centripetal acceleration and allows handling of uncertainty in model parameters. The proposed algorithm was implemented along with extensions to handle non-determinism, and flight-tested on an autonomous aircraft.