Robot Swarms as Hybrid Systems: Modelling and Verification

Swarm robotic systems are distributed systems wherein a set of robots cooperatively perform a task, without any centralized coordination [29]. Although individual robots are governed by relatively simple reactive controllers, interactions within the swarm may give rise to complex behaviors that were not explicitly programmed. Ultimately, these behaviors enable the swarm to achieve goals that would defy each single robot in isolation, or would require more expensive robots to achieve the same goals as effectively as the swarm does - see, e.g, [4, 33] for some examples. While understanding individual robot behavior is easy, predicting the overall swarm behavior is difficult, and thus engineering controllers for individual robots that will guarantee a desired swarm behavior is not a straightforward task. Traditionally, the analysis of swarms is carried out either by testing real robot implementations, or by computational simulations [20, 22]; however, these approaches provide little guarantees as they suffer from intrinsically incomplete coverage. As suggested by many authors, higher levels of assurance in swarm behavior can be obtained via formal methods [32, 30, 16, 5, 18, 23].