Verifying Emergence Properties of Robotic Swarms

The effective development and deployment of single-robot systems is increasingly shown to be 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, ants, bees, swarm robotic 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. Yet, for robot swarms to be put in practice, guarantees about their behaviour need to be established. This is a challenging problem, as, 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.

The aim of this project is to develop the area of verification of emergence for robotic swarms
further. This could be done in several ways, including by considering a different semantics, a
stochastic model, and beyond.

[1] P. Kouvaros, A. Lomuscio. Parameterised Verification for Multi-Agent Systems. Artificial
Intelligence. Elsevier.
[2] P. Kouvaros, A. Lomuscio. Verifying Emergent Properties of Swarms. Proceedings of the
24th Conference on Artificial Intelligence (IJCAI15).
[3] P. Kouvaros, A. Lomuscio. A Counter Abstraction Technique for the Verification of Robot
Swarms. Proceedings of the 29th AAAI Conference on Artificial Intelligence (AAAI15).
[4] P. Kouvaros, A. Lomuscio. Formal Verification of Opinion Formation in Swarms.
Proceedings of the 15th International Conference on Autonomous Agents and Multi-Agent
systems (AAMAS16). Singapore. pp 1200-1209. IFAAMAS Press.
[5] A. Lomuscio, H. Qu, F. Raimondi MCMAS: An Open-Source Model Checker for the
Verification of Multi-Agent Systems. International Journal on Software Tools for Technology
Transfer.
See https://www.youtube.com/watch?v=JmyTJSYw77g for the Kilobot Swarm developed at
Harvard. Pre-requisites: Model Checking, Logic, C++.

Project ID

STAI-CDT-2020-IC-31

Supervisor

Category

AI Planning, Logic, Verification