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

Fig. 1. An example of environment. Circles denote agent profiles ag 1 , ag 2 and
ag 3 . There are three action transformers: ag 1 ,a 1 ,s 1 ,ag 2 , ag 1 ,a 1 ,s 2 ,ag 3 and
ag 3 ,a 2 ,s 3 ,ag 1 . Moreover, there is also an environment behavior, behavior 1 ,thatis
executed whenever agent ag 1 performs action a 1 . Notice that the same action a 1 ,per-
formed by agent ag 1 , has three simultaneous consequences. Notice further that while
two of these consequences are stimulations, another merely triggers some operation.
This shows that it is technically interesting to have actions and stimuli as different
entities, since they are not always related.
2.4 Semantics
The semantics of EMMAS is given by considering: (i) a syntactical transla-
tion of EMMAS into π -calculus expressions; and (ii) a mathematical foundation
which relates π -calculus events to the stimuli and actions of agents. The π -
calculus translation of (i), through its operational semantics, provides an over-
approximation of the desired behavior, which is then made precise using the
restrictions provided by (ii). By this method, we shall be able to build an LTS
that defines the possible states and transitions for any particular environment
specification.
For the sake of clarity, we divide this section in two parts. First we define
some preliminary structures required for building the transition system, which
is then presented.
Preliminary Definitions. Our model must have a way to effectively interact
with the agents of a MAS. Agents may trigger events that have a meaning in the
environment specification (e.g., the performance of an action). Conversely, the
environment specification may request the performance of an operation (e.g., to
stimulate an agent). It is necessary, therefore, to have a mathematical foundation
that formally defines how to accomplish this. We fulfill this requirement by
providing both a vocabulary in which a few primitives are defined and a definition
for what constitutes an environment status with respect to these primitives.
Definition 7 (Vocabulary). A vocabulary is a tuple
Stimuli, Actions, AgentIDs
such that:
- Stimuli is a finite set of stimuli ;
- Actions is a finite set of actions ;
- AgentIDs is a finite set of agent identifiers ;