Verification of Swarm Robots

Overview

A robot swarm is a collection of simple (often identical) robots working together to carry out some task. Each robot usually has a small set of behaviours and can interact with other (nearby) robots and with its environment. Robot swarms are particularly appealing when compared with fewer, more complex robots, in that it may be possible to design a swarm so that the failure of some of the robots will not result in the failure of the overall mission, i.e. the swarm is fault tolerant. Such swarms may also be advantageous from a financial point of view since each robot is relatively simple and often cheap to produce. The use of swarms has many applications for example in areas difficult for humans such as underwater environments, contaminated areas, and space.

Despite the advantages of deploying swarms in practice, it is non-trivial for designers to formulate individual robot behaviours so that the emergent behaviour of the swarm as a whole is guaranteed to achieve the task required of the swarm, while the swarm will not exhibit any other, undesirable, behaviours. The analysis of swarm behaviour is usually carried out by experimenting with robot swarms in a laboratory setting or by simulating the robot swarms and testing various scenarios. In both these cases, any errors found will only be relevant to the particular scenarios constructed. The aim of our work is to develop, apply, and analyse formal verification techniques for robot swarms. In particular we have applied a range of temporal verification techniques (both algorithmic- model checking, and deductive- using formal proof) to different robot swarm algorithms. We aim to advance these tools and techniques to more complex swarm algorithms and domains to provide swarm designers with additional tools to ensure the reliability of robot swarms.

Collaborators

Clare Dixon, University of Liverpool

Michael Fisher, University of Liverpool

Savas Konur, University of Sheffield

Alan Winfield, Bristol Robotics Lab

Publications

Last modified: Fri May 10 12:28:19 BST 2013