Designing the Control of a UAV Fleet with Model Checking

We model the problem of unmanned aerial vehicles searching for moving targets as a pursuer-evader game in which the pursuers have a speed advantage over the evaders but are incapable of determining an evaders location unless a pursuer occupies the same location as that evader. By treating the players as nondeterministic finite automata, we can model the game and use it as the input for a model checker. By specifying that there is no way to guarantee the pursuer can locate the evader, the model checker will either confirm that this is the case, or it will provide a counter example showing one search pattern for the pursuer that will guarantee the evader must eventually be caught. As an ongoing eort to reduce the time to find pursuer-winning strategies, we also present heuristics to limit the state space of the game models.