MESSI – Maude Ensemble Strategies Simulator and Inquirer

Design, validation and performance evaluation of self-assembly strategies with Maude


Adaptive self-assembly strategies are a crucial mechanism that allows groups of simple individual entities to act as a single complex entity exhibiting emergent behaviours. Notable examples include bacteria or insect swarms, modular and self-assembling robots and software components with dynamic coupling mechanisms.

The following video1 (borrowed from a paper by Rehan O’GradyRoderich GroßAnders Lyhne Christensen and Marco Dorigo from the Université Libre de Bruxelles) is a nice example where robots apply self-assembly strategies to tackle obstacles like hills or holes in the terrain to be explored.

The considered self-assembly strategy (the basic self-assembly response strategy) is independently executed by each robot, and is defined in the mentioned paper as the following finite-state automaton:

Each circle (actually a bird-eye view of a robot) represents a basic behaviour of a robot as well as the color of its LEDs, while transitions among basic behaviours, labelled with the firing condition, denote adaptations. For example, a robot in state IP (Independent Phototaxis) independently navigates towards the goal (e.g. a given color emission). When an hole is found, the robot changes in state AP (Anti Phototaxis), i.e. it retracts from the hole. After a given amount of time the robot changes in state AGG (Aggregate) searching for robots to be grabbed.

We face these kind of self-assembly strategies (for robots and not only) by (i) following our recently proposed conceptual framework for adaptation; (ii) exploiting the declarative and reflective features of the Maude language; and (iii) relying on the Maude tool framework for the analysis.

Our implementation MESSI can be used to prototype self-assembly strategies to be simulated and analysed in early development phases. The design of self-assembly strategies is greatly facilitated by a library of basic behaviours like “move towards light“, or “grab an admissible LED emission“, so that self-assembly strategies can be defined in terms of adaptations among basic behaviours.

Once a self-assembly strategy is defined, it is possible to debug it by resorting to the animations automatically generated from single simulations of robots executing them. For example, a simulation of the above scenario can be seen in the below video.

Sometimes things can go wrong:

  • A robot can remain isolaled (video);
  • Robots can fall into the hole believing that they are safely attached (video).

Such are exactly the kind of situations we aim at spotting with our tool. Moreover, one may be interested in knowing the probability with which those situations arise, or in comparing different strategies, e.g. to focus on the most performant ones. This can be done by resorting to the parallel statistical model checker PVeStA which allows to estimate quantitative properties of a self-assembly strategy. More details can be found in Modelling and analyzing adaptive self-assembly strategies with Maude.

Clearly, self-assembly strategies may be defined for other scenarios like the collective healing ones, where robots cooperate to heal broken ones. The following is a simulation in which robots execute a self-assembly strategy for the collective healing scenario: a broken robot (i.e. a robot with red LEDs) is surrounded by other robots which irradiate it with yellow light to heal it.


  1. Roberto Bruni, Andrea Corradini, Fabio Gadducci, Alberto Lluch Lafuente, Andrea Vandin, Modelling and analyzing adaptive self-assembly strategies with Maude, Submitted to Science of Computer Programming
  2. Roberto Bruni, Andrea Corradini, Fabio Gadducci, Alberto Lluch Lafuente, Andrea Vandin, Modelling and analyzing adaptive self-assembly strategies with Maude, International Workshop on Rewriting Logic and its Applications (WRLA’12)
  3. Roberto Bruni, Andrea Corradini, Fabio Gadducci, Alberto Lluch Lafuente, Andrea Vandin, A conceptual framework for adaptation, International Conference on Fundamentals of Software Engineering (FASE 2012).


  1. Modelling and analyzing Self-Assembling Strategies with Maude, ASCENS General Meeting, March 15, 2012. Florence.
  2. A conceptual framework for adaptation, ASCENS General Meeting, July 7 2011, Grenoble.
  3. On graph-based verification of evolving structures, ASCENS General Meeting, July 7 2011, Grenoble.
  4. Maude .:° ASCENS, ASCENS General Meeting, March 4, 2011, Pisa.


The implementation of the case study and its simulator in Maude can be downloaded here



Invoke the simulation script as follows

./ {what} {steps} {where} [{module}]

where {what} indicates if one is interested in the initial state (initial), a goal state (goal), some random state (random) or an entire simulation (simulate). The current version is restricted to “simulate”. The number of simulation steps must be indicated. Moreover, {where} indicates the output folder for the generated images, and [{module}] is an optional parameter where the user can specify the initial configuration.

For example, to launch a simulation with 200 steps you can

./ simulate 200 ./output/

For more details on this we refer to the above mentioned publications.


Roberto Bruni, Andrea Corradini, Fabio Gadducci, Alberto Lluch Lafuente, Andrea Vandin.


Our work is developed within and supported by the European Integrated Project 257414 ASCENS.


For suggestions, remarks, bugs or requests please do not hesitate to contact any of:



1 Courtesy of Rehan O’Grady.