A Formal Environment Model for Multi-Agent Systems - Formal Methods: Foundations and Applications - page 65

A MAS can be decomposed into two aspects. The first relates to the agents.
The second deals with how such agents come together and interact among them-
selves. The elements that form this second aspect constitute the environment 1
of a MAS.
That said, our overall work is concerned with how one can build a MAS to
model a complex situation suitable for both exploratory simulation and approx-
imate formal verification. To achieve this, we aim at providing three basic ele-
ments: (i) an agent model, which we have already described in [10]; (ii) a formal
specification of the environment of these agents, so that they can be composed
into a MAS; and (iii) techniques to formally analyse the resulting MAS.
In this paper we focus on the problem of defining environments. Our environ-
ments have a social network structure in which nodes are agents, and the links
between them are defined by the capabilities that agents have to act upon each
other. Furthermore, environments are more than a network structure, as they
may change dynamically, either spontaneously or as a reaction to an agent's
actions. These design choices arise from the agent model that we consider [10].
In it, agents are described from the point of view of behavioral psychology [11],
which suggests a number of desirable features from an environment that brings
them together. For instance, great importance is placed on the possibility of
performing experiments of different kinds, and of responding to agent's actions
in appropriate ways. As we shall see, our approach achieves this by the envi-
ronment behaviors it defines. Furthermore, interaction is mostly interestingly
treated by abstracting physical properties away and dealing only with relation-
ships, which we do by adopting a social network structure and operations to
modify it. We believe that these characteristics already differentiate our work
substantially from other existing environment description methods (see Weyns
et al. [14] for a survey).
Here we develop a simple formal framework in which to define such environ-
ments so that they can be subject to automated analyses procedures. A mathe-
matical model is provided, which we call the Environment Model for Multi-Agent
Systems (EMMAS), and its semantics is given in terms of the π -calculus process
algebra [4,7].
Process algebras are typically employed to describe concurrent systems. They
are good at succinctly describing behaviors relevant for inter-process communica-
tion. Our particular choice of π -calculus as a theoretical foundation is motivated
by a number of its distinguishing features among existing such algebras. First, it
takes communication through channels as a primitive notion, which makes it a
natural choice for representing networks. Second, it allows for dynamic modifi-
cation, which makes the creation and destruction of connections between agents
possible. Third, it provides a convenient representation for broadcast behavior
1 Notice that the term “environment” is not used consistently in the MAS literature
[14]. Sometimes, it is used to mean the conceptual entity in which the agents and
other objects exist and that allows them to interact; sometimes, it is used to mean
the computational infrastructure that supports the MAS (e.g., a simulator). We use
the term in the former sense.