Reachability calculations for vehicle safety during manned/unmanned vehicle interaction

This paper describes an approach based on reachability calculations for ensuring robust operation guarantees in flight maneuver sequences performed by unmanned aerial vehicles under supervision of human operators, with applications to safety-critical scenarios. Using a hybrid system formalism to model the maneuver sequence, the paper devises systematic procedures for designing switching conditions to ensure the properties of safety, target attainability, and invariance, using Hamilton-Jacobi reachability calculations. These calculations lay the foundations for refining or designing protocols for multiple unmanned aerial vehicle and/or manned vehicle interaction. The mathematical foundations necessary are described in order to formulate verification problems on reachability and safety of flight maneuvers, including issues of command latency and disturbance. An example of this formalism is given in the context of automated aerial refueling, to inform unmanned aerial vehicle decisions that avoid unsafe scenarios while achieving mission objectives.