Information Technology Reference
In-Depth Information
sp X-Machines: Formal State-Based Modelling
of Spatial Agents
Isidora Petreska 1 , Petros Kefalas 2 , Marian Gheorghe 3 , and Ioanna Stamatopoulou 2
1 South East European Research Centre (SEERC),
24 Proxenou Koromila Str., Thessaloniki 54622, Greece
2 CITY College, International Faculty of the University of Sheffield,
3 Leontos Sofou Str., Thessaloniki 54626, Greece
3 University of Sheffield, Dept. of Computer Science,
Regent Court, 211 Portobello Str., Sheffield S1 4DP, U.K.
ispetreska@seerc.org,
{ kefalas,istamatopoulou } @city.academic.gr,
m.gheorghe@dcs.shef.ac.uk
Abstract. Applications of biological or biologically inspired multi-agent sys-
tems (MAS) often assume a certain level of reliability and robustness, which
is not always straightforward. Formal modelling and verification of MAS may
present many interesting challenges. For instance, formal verification may be
cumbersome or even impossible to be applied on models with increased complex-
ity. On the other hand, the behaviour of MAS consists of communities evolving
in space and time (such as social insects, tissues, colonies of bacteria, etc.) which
are characterised with a highly dynamic structure. In order to provide a neat and
effective way to modelling and verification of these systems, we focus on their
spatial characteristics. Spatial agents (i.e. agents distributed and moving through
a physical space) can be modelled with X-machines - one of the most promi-
nent formalisms for modelling the behaviour of biological colonies. However, it
will be demonstrated that there are certain problems in the X-machines models,
common to every spatial MAS. To overcome these disadvantages, we introduce
an X-machines variation that besides facilitating formal modelling, will provide
grounds towards visual animation of these systems. This approach resulted into
a novel progression, Spatial X-machines ( sp XM), without retracting the legacy
characteristics of X-machines such as testing and verification strategies. Finally,
we present a supporting framework to modelling and verification of spatial multi-
agent system, by utilizing the Spatial X-machines approach.
Keywords: Formal modelling, X-machines, Spatial agents.
1
Introduction
Formal modelling is considered as one of the most essential stages in Multi-agent sys-
tem (MAS) development and can be carried out with many different methods and tech-
niques, ex. Z [1], VDM [2], FSM [3], Petri Nets [4], and others. These varieties of
Search WWH ::




Custom Search