Information Technology Reference
In-Depth Information
sp
XM Model
Other
behaviours
Spatial
behaviours
Transformation
Transformation
Transformation
sp
XMDL
Model
sp
XMDL
Model
MAS Model
suitable for
Model Checking
Simulation
Transformation
Time Series Data
NetLogo
Model
Repast,
Pattern Identification
Visual animation
Other
properties
Spatial
properties
Emergence
Fig. 5.
A framework for validating emergent properties in spatial biology-inspired MAS
next step involves utilizing a tool for identifying patterns, such as DAIKON [26]. Fi-
nally, the
sp
XM can be suitably transformed into an equivalent model in SPIN, PRISM
or SMV [27-29]. In this case, given a temporal formulae, all of the desired properties
could be verified upon the original model. More information about this framework can
be found in [15].
6
Conclusions and Future Work
Given X-machines, one might argue that the bio-MAS models might be very abstract,
i.e. there is a freedom in the representation of a model. On the other hand, certain
knowledge is required for simulating a biological agent, for instance the initial posi-
tion or direction of the agent. This introduces difficulties in simulating a given model,
because an X-machine does not specify how these knowledge will be modelled. Thus
we presented an idea of extending X-machines into more specific formalism for mod-
elling spatial agents that move in space, called
sp
XMs. Unlike other formalisms that go
behind the concept of treating the agent's behaviour as one uniform component, Spa-
tial X-machines tend to draw a separation between different types of agent's behaviour.
This approach facilitates the verification of emergent behaviour of spatial MAS fitting
perfectly in the proposed framework towards verification of spatial MAS.
