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

The sets Stimuli , Actions and AgentIDs define, respectively, all available stim-
uli, actions and agent identifiers. These are sets containing primitive, unstruc-
tured, elements.

Definition 8 (Environment Status)
An environment status is a pair

Stimulation, Response

such that:

- Stimulation : AgentIDs × Stimuli →{ Beginning, Stable, Ending, Absent } ;

- Response : AgentIDs × Actions →{ Emitting, NotEmitting } .

Building the Transition System. Givenanenvironment E , we shall build
an annotated environment LTS by considering the LTS induced by

] π ,whose
states shall be annotated with our environment status (Def. 8), and whose struc-
ture shall be subject to some restrictions based on the possible values for an envi-
ronment status. Then we shall then have an LTS whose states have the following
form.

[ E

Definition 9 (State). Let E be an environment and P be a π -calculus process
obtained by applying π -calculus operational semantics rules to [ E ] π . Moreover,

let Stimulation, Response be an environment status. Then a state is defined

as the following pair:

( P, Stimulation, Response )

By this construction, at any point of the LTS we shall be able to know both what
is the current situation of the agents (because of the added environment status)
and what are the possible changes from that point (because of the π -calculus
operational semantics).
To proceed with this construction, we need a number of definitions. Let us
begin by providing a way to observe the internal transitions of an environment,
which is a fundamental capability that we need before proceeding. Recall from
Def. 4 that an environment's π -calculus process has a number of restrictions that
would prevent such observations (i.e., the transitions would be internal to the
process and not discernible in the LTS). It is, however, possible to characterize
these restrictions syntactically, and thus we may provide a simple method to
remove them when needed. This is accomplished by the following environment
unrestriction function unr .

Definition 10 (Environment Unrestriction Function)
Let P and Q be π -calculus processes such that

P =( νen 1 ,...,en o ) Q

where { en 1 ,...,en o } = ENames . Then the environment unrestriction function

is defined as unr ( P )= Q .