Robot Swarms as Hybrid Systems: Modelling and Verification

Electronic Proceedings in Theoretical Computer Science, vol. 361, pp. 61–77

Abstract

A swarm robotic system consists of a team of robots performing cooperative tasks without any centralized coordination. In principle, swarms enable flexible and scalable solutions; however, designing individual control algorithms that can guarantee a required global behavior is difficult. Formal methods have been suggested by several researchers as a mean to increase confidence in the behavior of the swarm. In this work, we propose to model swarms as hybrid systems and use reachability analysis to verify their properties. We discuss challenges and report on the experience gained from applying hybrid formalisms to the verification of a swarm robotic system.

Authors 5

1. Stefan Schupp

   TU Wien

   Affiliation as printed

   TU Wien

   TU Wien, Vienna, Austria

2. Francesco Leofante

   Imperial College London

   Affiliation as printed

   Imperial College London

   Imperial College London, London, United Kingdom

3. Leander Behr Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University

   RWTH Aachen University, Aachen, Germany

4. Erika Ábrahám Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University

   RWTH Aachen University, Aachen, Germany

5. Armando Taccella

   University of Genoa

   Affiliation as printed

   University of Genoa

   University of Genoa, Genoa, Italy