Formal modelling of multi-agent systems (MAS) present many interesting challenges. In this extended abstract we present a framework of how formal modelling can lead towards identication and verication of emergent properties of spatial biology-inspired MAS. We discuss the problem in question as well as initial work done on the formal modelling side and the visual animation of these formal models.
Verication of the emergent behaviour of multi-agent systems is an extremely complex task. It is not only the fact that the verication process, formal or model checking, leads to combinatorial explosion, but also the fact that emergent properties should be identied rst before there is an attempt to be veried. The latter is not always straightforward. It is therefore desirable to combine several formal with informal techniques that would be able to join forces towards the verication of MAS.
In agents that operate in a 2 or 3-dimensional space, such as biology or biology-inspired agents, emergence is characterised by a pattern appearing in the agents conguration at some instance during the operation of the system. Trivial examples are colonies of social insects, like ants, birds, sh etc. The type of emergence observed is related to the positioning in space, for example line formation, ocks, schools, herds etc. Modelling such agents would require modelling of their position and verication would require the exploration of a state space developed by the combination of all agent positions evolved through time.
Someone could apply formal verication techniques, such as model checking,
under the assumption that we know what emergent property we are looking
for. With biology agents this is known in advance, since it has been observed
invivo. With articial agents it is not as simple, there is however an active research
that proposes a framework for empirical exploration of emergent formations [
In the aggressor-defender game [
All the agents defend at each turn everyone tends to position between a friend and an enemy (such as they were defending the friend against the enemy), Fig. 1 a).
All the agents ee at each turn everyone tries to position in a way that a friend is between themselves and an enemy (such as the friend protects them from an enemy), Fig. 1 b).
Some agents defend while the rest of the agents ee.
Assuming that we can develop a formal model to be used for model checking, it is interesting to consider what property to check for, that is, whether there is an emergent behaviour in all the above three cases, if this MAS is massively populated with similar agents.
This work aims to set up a framework of study concerning the above interesting problems and more in particular to demonstrate preliminary results in identifying emergent behaviour through the automatic transformation of a formal model to an executable visual simulation. 2
The proposed research framework is depicted in Fig. 2. At the top, we start
by formal modelling of agents. Such formal models should be able to clearly
distinguish modelling of various types of behaviours, such as spatial or other
behaviours, communication, dynamic organisation etc. By separating the
various behaviours within the same formal model, it is possible to apply dierent
transformations which will facilitate further processing. On one hand, the spatial
behaviour determined by movement in space, can lead towards visual animation.
The latter is a useful informal tool which will help observing potential emergent
properties. On the other hand, suitable abstractions of spatial behaviour
together with the rest of the behaviours can lead towards simulation and logging
of time series data. These could be used to identify patterns of behaviours which
combined with the visual animation produce a set of desired properties. Finally,
the desired properties (including emergence) can be veried in the original
spatial agent model by model checking, as long as there is a way to transform the
original model into an equivalent, susceptible to formal verication, model.
We have been long experimenting with state-based modelling for agents and
MAS [35]. The state-based modelling method we use is X-Machines (XM). XM
are state machines with memory and instead of inputs triggering transitions,
they trigger functions which label the transitions. XM are able to communicate
through message exchange, thus forming Communicating X-Machines [
spXMs represent a variation of Stream XMs by dening additional
components that allow specication of the current position and direction of an agent,
as well as to formally specify a movement of an agent within its environment.
Formally, a spXM is a 13-tuple; spXM = (Σ, Γ , Q, q0, M, m0, π, π0, θ, θ0, E,
Φ, F) [
A spXM model which demonstrates the third strategy is presented on Fig. 3.
The model’s states are Q={DEFENDING, STAYING_STILL, FLEEING}. There
are three corresponding functions: to defend, to stay still and to ee . The
memory stores the game strategy of the agent, an agent’s friend and enemy, as well as
its position and direction. The input consists of the friend’s and the enemy’s
current position. Finally, the output is the new position of the agent, because every
agent outputs its position to the other agents thus constructing a communicating
spX-machine system [
spXMDL is the notation used to dene spXMs [
#fun functor (($input$), ($memory tuple$), ($position$), ($direction$)) = (($output$), ($memory tuple’$), ($position’$), ($direction’$)) = where $<list of operations including positioning>$
Considering Fig. 3, the function defend is: #fun defend ( ((?x_fr, ?y_fr),(?x_en, ?y_en)), (?strategy, ?friend, ?enemy), (?my_xcor, ?my_ycor), (?curr_direction) ) = (("move to ?new_xcor ?new_ycor"), (?strategy, ?friend, ?enemy), (?new_xcor, ?new_ycor), (?curr_direction)) where ?new_xcor <- (?x_fr + ?x_en)/2 and ?new_ycor <- (?y_fr + ?y_en)/2.
As part of the rst steps towards the achievement of formal verication of
emergent properties, we have developed a tool for automatic translation of a spXM
model to NetLogo [
For the aggressor-defender MAS, an executable counterpart is generated. The output shows a visual animation with which the emergent spatial behaviour is observable (Fig. 4), such as:
The model in which all the agents defend, see Fig. 4 a), behaved as all the agents quickly collapsed into a tight knot, The model in which all the agents ee, see Fig. 4 b), behaved as a highly dynamic group that expands over time towards the ends of the environment, and The model in which the agents randomly choose whether to defend or to ee, see Fig. 4 c), exhibited there dierent behaviours. In some situations the agents were all collapsed into a tight knot (as the model from the defender game) with the dierence that this knot was now oscillating around the environment (i), in others they were stationary, randomly distributed and oscillating (ii), and in the last case the agents would form a ocking (iii).
The case of this game clearly demonstrated that visual animation aided in discovery of the system’s emergence and properties that could be veried at a later stage, which in turn proved that even the small changes within the individual agent rules might cause a huge dierence in behaviour of the system as a whole. 5
The contribution of this paper is to present the overall picture of a framework
towards the verication of emergent behaviour of spatial MAS. We have also
reported progress so far, that is, a denition of spXM and a tool for automatic
transformation to NetLogo. Using this experience, the next steps in the
framework are instantiated (Fig. 2) as follows:
spXM can be transformed into a simulation tool that can generate a time
series data. Such tool may be FLAME [
The logged time series data could be used as an input to a tool identifying
patterns, such as DAIKON [
The spXM can be suitably transformed into an equivalent model in SPIN, PRISM or SMV [1719], which given the temporal formulae will verify that all the desired properties hold in the original model.
Of course the above would assume that a correct transformation from the original model to equivalent models is possible, something which is an interesting problem by itself.