— This paper describes reachability calculations for a hybrid system formalism governing UAVs interacting with another vehicle in a safety-critical situation. We examine this problem to lay the foundations toward the goal of certifying certain protocols for flight critical systems. In order to pursue these goals, we describe here what mathematical foundations are necessary to inform protocol certification, as well as describe how such formalisms can be used to automatically synthesize simulations to test against certain danger areas in the protocol. This can provide a mathematical basis for the UAV to perhaps reject a command based on the known unsafe behavior of the vehicle. We describe how creating this formalism can help to refine or design protocols for multi-UAV and/or manned vehicle interaction to avoid such scenarios, or to define appropriate behaviors in those cases.
Jerry Ding, Jonathan Sprinkle, Shankar S. Sastry,