Designing protocols for multi-agent interaction that achieve the desired behavior is a challenging and error-prone process. The standard practice is to manually develop proofs of protocol correctness that rely on human intuition and require significant effort to develop. Even then, proofs can have mistakes that may go unnoticed after peer review, modeling and simulation, and testing. The use of formal methods can reduce the potential for such errors. In this paper, we discuss our experience applying model checking to a previously published multi-agent protocol for unmanned air vehicles. The original publication provides a compelling proof of correctness, along with extensive simulation results to support it. However, analysis through model checking found an error in one of the proof’s main lemmas. In this paper, we start by providing an overview of the protocol and its original “proof” of correctness, which represents the standard practice in multi-agent protocol design. We then describe how we modeled the protocol for a three-vehicle system in a model checker, the counterexample it returned, and the insight this counterexample provided. We also discuss benefits, limitations, and lessons learned from this exercise, as well as what future efforts would be needed to fully verify the protocol for an arbitrary number of vehicles.

This paper poses the cooperative perimeter-surveillance problem and offers a decentralized solution that accounts for perimeter growth (expanding or contracting) and insertion/deletion of team members. By identifying and sharing the critical coordination information and by exploiting the known communication topology, only a small communication range is required for accurate performance. Simulation and hardware results are presented that demonstrate the applicability of the solution.

Numerous applications require aerial surveillance. Civilian applications include monitoring forest fires, oil fields, and pipelines and tracking wildlife. Applications to homeland security include border patrol and monitoring the perimeter of nuclear power plants. Military applications are numerous. The current approach to these applications is to use a single manned vehicle for surveillance. However, manned vehicles are typically large and expensive. In addition, hazardous environments and operator fatigue can potentially threaten the life of the pilot. Therefore, there is a critical need for automating aerial surveillance using unmanned air vehicles (UAVs). This paper gives an overview of a cooperative control strategy for aerial surveillance that has been successfully flight tested on small (48-in wingspan) UAVs. Our approach to cooperative control problems can be summarized in four steps: 1) the definition of a cooperation constraint and cooperation objective; 2) the definition of a coordination variable as the minimal amount of information needed to effect cooperation; 3) the design of a centralized cooperation strategy; and 4) the use of consensus schemes to transform the centralized strategy into a decentralized algorithm. The effectiveness of the solution will be shown using both high-fidelity simulation and actual flight tests