|Title||On the Formal Specification of Emergent Behaviours of Swarm Robotics Systems|
|Publication Type||Journal Article|
|Year of Publication||2005|
|Authors||A. Winfield, J. Sa, C. Fernandez-Gago, C. Dixon, and M. Fisher|
|Journal||International Journal of Advanced Robotics Systems|
|Keywords||Swarm Robotics, temporal resolution|
It is a characteristic of swarm robotics that specifying overall emergent swarm behaviours in terms of the low-level behaviours of individual robots is very difficult. Yet if swarm robotics is to make the transition from the laboratory to real-world engineering realisation we need such specifications. This paper explores the use of temporal logic to formally specify, and possibly also prove, the emergent behaviours of a robotic swarm. The paper makes use of a simplified wireless connected swarm as a case study with which to illustrate the approach. Such a formal approach could be an important step toward a disciplined design methodology for swarm robotics.