Symmetry Reduction Enables Model Checking of More Complex Emergent Behaviours of Swarm Navigation Algorithms

Laura Antuna, Dejanira Araiza Illan*, Sergio Campos, Kerstin I Eder

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)

7 Citations (Scopus)
39 Downloads (Pure)

Abstract

The emergent global behaviours of robotic swarms are important to achieve their navigation task goals. These emergent behaviours can be verified to assess their correctness, through techniques like model checking. Model checking exhaustively explores all possible behaviours, based on a discrete model of the system, such as a swarm in a grid. A common problem in model checking is the state-space explosion that arises when the states of the model are numerous. We propose a novel implementation of symmetry reduction, in the form of encoding navigation algorithms relatively with respect to a reference, based on the symmetrical properties of swarms in grids. We applied the relative encoding to a swarm navigation algorithm, Alpha, modelled for the NuSMV model checker. A comparison of the state-space and verification results with an absolute (or global) and a relative encoding of the Alpha algorithm highlights the advantages of our approach, allowing model checking larger grid sizes and number of robots, and consequently, verifying more complex emergent behaviours. For example, a property was verified for a grid with 3 robots and a maximum allowed size of 8x8 cells in a global encoding, whereas this size was increased to 16x16 using a relative encoding. Also, the time to verify a property for a swarm of 3 robots in a 6x6 grid was reduced from almost 10 hours to only 7 minutes. Our approach is transferable to other swarm navigation algorithms.
Original languageEnglish
Title of host publicationTowards Autonomous Robotic Systems
Subtitle of host publication16th Annual Conference, TAROS 2015, Liverpool, UK, September 8-10, 2015, Proceedings
EditorsClare Dixon, Karl Tuyls
PublisherSpringer Verlag
Pages26-37
Number of pages12
ISBN (Electronic)9783319224169
ISBN (Print)9783319224152
DOIs
Publication statusPublished - 18 Jul 2015
Event16th Annual Conference on Towards Autonomous Robotic Systems, TAROS 2015 - Liverpool, United Kingdom
Duration: 8 Sep 201510 Sep 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer Verlag
Volume9287
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference16th Annual Conference on Towards Autonomous Robotic Systems, TAROS 2015
CountryUnited Kingdom
CityLiverpool
Period8/09/1510/09/15

Fingerprint Dive into the research topics of 'Symmetry Reduction Enables Model Checking of More Complex Emergent Behaviours of Swarm Navigation Algorithms'. Together they form a unique fingerprint.

Cite this