Information Technology Reference
In-Depth Information
Fig. 4.
System architecture of
sp
XM2Visual
perception of the environment, etc.). Functions that deal with the modelling of the envi-
ronment (defining obstacles, defining agents, etc.) are also included. Other interesting
parts of the compiling component are the
rules for transformation
and the
translator
.
The rules for transformation are simple
if-then rules
. An example of such a rule for the
where statement
in an
sp
XMDL representation is presented in [23]. On the other hand,
the translator is composed of a reader (parses an
sp
XMDL representation and constructs
the necessary objects), an object model (function, memory, state, transition, etc.) and a
writer (used in writing the NetLogo code).
5
A Proposed Framework towards Verification of Spatial MAS
The concept of emergence can be explained as a pattern appearing in the configuration
of the agents, at some instance during the lifetime of the system. We are interested in
the type of emergence related to the positioning in space (such as line formation, flocks,
schools, herds etc.). However, formal verification techniques can only be applied under
the assumption that we know what is the emergent property. In order to be able to tackle
this kind of problems, we propose a research framework, depicted in Fig. 5. This frame-
work helps in identifying emergent behaviour through the automatic transformation of
a formal model to an executable visual simulation [15].
The frame on the right side of the figure, reflects the current work. At the top of the
framework is the phase of formal modelling of agents. For this step we utilise the
sp
XMs
approach, because the formal models should be able to clearly distinguish modelling of
various types of behaviours (such as spatial or other behaviours, communication, dy-
namic organisation etc.). This makes it possible to apply different transformations that
will facilitate further processing. On one hand, the spatial behaviour can lead towards
visual animation which can help in detecting emergence. On the other hand, abstrac-
tions of the spatial behaviour together with the rest of the behaviours can lead towards
simulation and logging of time series data [15]. Finally, all the patterns of behaviours
together with the visual animation would produce a set of desired properties. The prop-
erties can be verified in the original spatial agent model by model checking.
The spatial behaviour can be detected by utilizing NetLogo with the automatic trans-
lation tool of an
sp
XM model. On the other hand, the logging of time series data might
be accomplished with a tool such as FLAME [24, 25], used to animate XM models. The
