The effective development and deployment of single-robot systems is known to be increasingly problematic in a variety of application domains including search and rescue, remote exploration, de-mining, etc. These and other practical settings require expensive and complex designs that are typically realised by machines with little or no fault-tolerance. Inspired by biological swarms, e.g, colonies of ants, bees, fish, etc, robotic swarm systems have been put forward to overcome these difficulties. The inherent simplicity of an individual robot, as well as the arbitrarily big numbers of robots composing a swarm, makes swarm robotics a cheap and robust alternative to single-robot systems.
For robot swarms to be put in practice, guarantees about their behaviour need to be established. This is a challenging problem, since, in contrast to traditional systems, a robot swarm may be deployed with a varying number of components depending on the application domain. Recent research in the parameterised verification for multi-agent systems put forward methodologies to assess the correctness of swarm systems irrespectively of the number of robots composing the swarm [1,2,3,4]. In particular, [2] defines the decision problem of determining whether a swarm satisfies an emergent property and introduces the Emergence Identification Procedure (EIP) for solving the problem. More recently approaches dealing with probabilistic swarm systems have also been pursued [5,6,7].
The inherent limitation of all these approaches lies in the semantics that is considered which limits the amount of agent-to-agent communication that is possible. The primary aim of this project will be to overcome this limitation so that realistic swarm protocols can be analysed and their safety and robustness verified.
Pre-requisites: Working knowledge of Logic, Verification via Model Checking and Theorem Proving recommended.