Information Technology Reference
In-Depth Information
-
Φ
is a finite set of partial functions
φ
that map a memory state, position, direction
and set of inputs to a new memory state, position, direction and set of outputs:
φ
:M
×
π
×
θ
×
Σ
−→
×
π
×
θ
×
Γ
;and
M
-
F: Q
Q is a function that determines the next state, given a state and a
function from the type
Φ
.
×
Φ
→
If we take a closer look at the memory M, it may be noted that M is composed of
M
ˆ
<π
,
θ>
,where
M
is a memory structure from the standard XM. Moreover,
regarding the set of elementary operations, we have currently defined three operations:
-
change direction
m
- changes the spatial agent's direction to
m
,where
m
is of type
θ
and
m
Θ
(ex.
change direction 60
)
-
move n forward
n
- moves forward for
n
units, where
n
is an integer (ex.
move n forward 3
)
-
move to position
xy
- moves to specific position (
x
,
y
), where
x
is the x-coordinate,
y
is the y-coordinate of the agent and (
x
,
y
)
∈
∈
Π
(ex.
move to
position 126 43
)
As it can be determined from the definition, an
sp
XM in essence provides a separation
of the behaviour within the system that deals with the movement (and the other spatial
attributes) from the rest of the behaviour. This way we establish a standardised way
to modelling motion that is easily understandable and provides a direct mapping to
an animation/simulation. And finally, this definition maintains an obvious equivalence
with the standard XM.
4
Verification and Validation Strategies
Formal verification of spatial agents is an extremely complex task. On one hand stands
the fact that the verification process leads to combinatorial explosion, because mod-
elling these agents means modelling of their spatial properties. Therefore, the verifi-
cation would require exploration of a state space developed by the combination of all
agent positions evolved through time [15]. On the other hand, there is the fact that the
emergent properties of the system should be known in advance in order to be verified
in silico. The concept of emergence can be explained as a pattern appearing in the con-
figuration of the agents, at some instance during the lifetime of the system. In bio-MAS
the emergence can be observed in-vivo (for example, line formation, flocks, schools,
herds etc.). However, when it comes to artificial agents, it is not always straightforward.
Driven from these two problems, it might be desirable to combine several formal with
informal techniques that would be able to join forces towards the verification of spatial
MAS [15].
Verification and Validation of
sp
XMs
4.1
The models of an X-machine can be described with the X-machine Definition Language
(XMDL [11]) and textual simulation. XMDL is a listing of definitions that match the
tuples of X-machine's definition. Similar to the diagram of Fig. 3 (which is essence tar-
gets
sp
XMs), XMDL is facilitated with a parser built using Definite Clause Grammars
