Analysing Robot Swarm Decision-making with Bio-PEPA

Mieke Massink, Manuele Brambilla, Diego Latella ,Marco Dorigo, and Mauro Birattari
May 2012


This page contains all supplementary information that was not possible to included in the paper.

Table of Contents
  1. Paper Abstract
  2. Bio-PEPA specification - Cheetah template
  3. Bio-PEPA specification - Full
  4. PRISM specification

Paper Abstract

We present a novel method to analyse swarm robotics systems based on Bio-PEPA. Bio-PEPA is a process algebraic language originally developed to analyse biochemical systems. Its main advantage is that it allows different kinds of analyses of a swarm robotics system starting from a single description. In general, to carry out different kinds of analysis, it is necessary to develop multiple models, raising issues of mutual consistency. With Bio-PEPA, instead, it is possible to perform stochastic simulation, fluid flow analysis and statistical model checking based on the same system specification. This reduces the complexity of the analysis and ensures consistency between analysis results. Bio-PEPA is well suited for swarm robotics systems, because it lends itself well to modelling distributed scalable systems and their space-time characteristics. We demonstrate the validity of Bio-PEPA by modelling collective decision-making in a swarm robotics system and we evaluate the result of different analyses.

Keywords: Swarm robotics, Modelling, Bio-PEPA, Collective decision-making

Bio-PEPA specification - Cheetah template

Cheetah template: this is a Cheetah template of the Bio-PEPA robot swarm specification in which scripting is used to allow a more compact way of writing of the specification and to generate specification with different path lengths. The Cheetah package can be obtained from the University of Edinburgh via Stephen Gilmore and Alan Clark.
Python script: This is a python script to run with the above file in order to produce the full Bio-PEPA specification of the system with the desired path lengths.
To run the script you need to execute the command in a Unix-like environment: "python robo_bridge_v6.py robo_bridge_v6_32robots_NewNames.template > FINAL_robo_bridge_v6_32robots_NewNames.biopepa"

Bio-PEPA specification - Full

The full Bio-PEPA specification: this is the full Bio_PEPA specification for a short path with 8 sections and a long path with 15 sections obtained from the above generation. The specification has been provided with comments to ease understanding.
The above specification can be imported in the Bio-PEPA Eclipse plugin that can be downloaded from: http://homepages.inf.ed.ac.uk/s9552712/bio-pepa/download.html.
The Bio-PEPA Eclipse plugin provides, among others, analysis tools for stochastic simulation and fluid flow (ODE) analysis. Moreover, after a small adaptation of the Bio-PEPA specification excluding the use of the H-function, the specification can be exported into the input language of the PRISM tool.

PRISM specification

The PRISM specification: this file is the PRISM version of the Bio_PEPA specification. It needed a few minor modifications due to the fact that not all features of Bio-PEPA have yet been fully implemented. The modifications are indicated at the top of the file.
The PRISM properties file: this file is the input file for PRISM containing among others the properties discussed in the paper.
The PRISM specification can be imported by the PRISM model checker, that can be found at: http://www.prismmodelchecker.org
The analyses presented in the paper have been performed with PRISM 4.0.2 on an iMAC 3.2 Ghz Intel Core i3 with MAC OS 10.6.8.
The PRISM model checker provides, among others, a statistical (or approximate) model checking tool that we have used to check the relevant properties described in the paper. Note that traditional stochastic model-checking cannot be used for this model because of its too large state-space.