Verifying Safety and Reliability of Robotic Swarms

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.

[1] P. Kouvaros, A. Lomuscio. Parameterised Verification for Multi-Agent Systems. Artificial Intelligence. Elsevier. 2015
[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.
[5] P. Kouvaros, A. Lomuscio, E. Pirovano, H. Punchihewa. Formal Verification of Open Multi-Agent Systems. Proceedings of the 18th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS19). Montreal, Canada. IFAAMAS Press. 2019.
[6] A. Lomuscio, E. Pirovano. Parameterised Verification of Strategic Properties in Probabilistic Multi-Agent Systems. Proceedings of the 19th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS20). Auckland, New Zealand. IFAAMAS Press. 2020
[7] A. Lomuscio, E. Pirovano. Verifying Fault-Tolerance in Probabilistic Swarm Systems Proceedings of the 29th International Joint Conference on Artificial Intelligence and the 17th Pacific Rim International Conference on Artificial Intelligence (IJCAI-PRICAI20). Yokohama, Japan. AAAI Press. 2020.

See https://www.youtube.com/watch?v=JmyTJSYw77g for the Kilobot Swarm developed at Harvard.

Pre-requisites: Working knowledge of Logic, Verification via Model Checking and Theorem Proving recommended.

Project ID

STAI-CDT-2021-IC-6

Supervisor