Designing the Control of a UAV Fleet with Model Checking

Abstract

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 evader's 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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 2004
Accession Number
AD1001130

Entities

People

  • Bruce W. Weide
  • Christopher A. Bohn
  • Paolo A. Sivilotti

Organizations

  • Ohio State University

Tags

Communities of Interest

  • Autonomy
  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Air Force
  • Aircrafts
  • Algorithms
  • Automata
  • Autonomous Vehicles
  • Computations
  • Cooperative Control
  • Department Of Defense
  • Grids
  • Guarantees
  • Moving Targets
  • Situational Awareness
  • Specifications
  • Target Tracking
  • Targets
  • Unmanned Aerial Vehicles
  • Vehicles

Fields of Study

  • Computer science

Readers

  • Applied Combinatorial Optimization and Logic Circuit Design.
  • Game Theory.
  • Mathematical Modeling and Probability Theory.

Technology Areas

  • Autonomy
  • Autonomy - Autonomous System Control
  • Autonomy - UAVs
  • Space
  • Space - Spacecraft Maneuvers