@inproceedings{633a08afa5cc41379312fd74fa61b245,
title = "Verifying large numbers of cooperating adaptive agents",
abstract = "NASA is proposing to use large numbers of cooperating spacecraft in future exploration missions. These swarms will exhibit complex behaviors and interactions that can result in unintended emergent properties. Verifying the proper behavior of these new types of missions will be critical to their success. This paper gives the results of research into the use of formal methods techniques for verification of a large number of cooperating agents. Multiple formal methods were evaluated to determine their effectiveness in assuring the behavior of swarms of spacecraft. The NASA ANTS mission was used as an example of swarm intelligence against which to apply the formal methods. This paper discusses the evaluation of these formal methods, provides a partial specification of ANTS using four selected methods, and an outline of an integrated formal method for verifying future NASA swarm missions.",
keywords = "Autonomy, Emergent behavior, Formal methods, Spacecraft, Swarms, Verification",
author = "Christopher Rouff and Mike Hinchey and Walt Truszkowski and James Rash",
year = "2005",
doi = "10.1109/ICPADS.2005.294",
language = "English",
isbn = "0769522815",
series = "Proceedings of the International Conference on Parallel and Distributed Systems - ICPADS",
pages = "391--397",
editor = "L. Barolli",
booktitle = "Proceedings - 11th International Conference on Parallel and Distributed Systems Workshops, ICPADS 2005",
note = "11th International Conference on Parallel and Distributed Systems Workshops, ICPADS 2005 ; Conference date: 20-07-2005 Through 22-07-2005",
}