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

At last, we may define the annotated environment LTS as follows.

Definition 13 (Annotated Environment LTS). Let E be an environment
(Def. 4), and let be the transition relation induced by the π -calculus opera-

tional semantics. Then an annotated environment LTS is an LTS

→

S, L, such

that:

- L EEvents (see Def. 2);

- S and

=

are constructed inductively as follows:

• Initial state. ([ E ] π ,es ) ∈ S ,where es = Stimulation, Response such

AgentIDs we have
Stimulation(n, s) = Absent and Response(n, a) = NotEmitting.
• Other states and transitions.
If s 1 =(

that for all a ∈ Actions , s ∈ Stimuli ,and n ∈

P 1 , Stimulation 1 ,Response 1 ) ∈ S ,

l

then s 2 =( P 2 , Stimulation 2 ,Response 2 ) ∈ S and s 1 s 2 if and only

if:
∗

l
→

P 1 P 2 ;

∗ Stimulation 2 is defined w.r.t. P 2 according to Def. 11;

l

∗ s 1 s 2 is not forbidden by Def. 12.

3 Convenience Elements and Operations

So far we have defined the bare minimum for describing environments so that
they can be formally analysed. Clearly, though, more constructs are necessary
in order to make such specifications. For example, in Def. 3 we established what
is an operation in general, but we have not presented any particular one. In the
present section, then, we provide a number of convenience elements that can be
used to build concrete EMMAS models. These, however, are merely examples of
what can be expressed with the basic model given before, designed to show its
usefulness, and the reader may well imagine many other convenience elements.

3.1 Composition Operators

In order to build complex operations on top of the basic ones, it is useful to
define composition operators. Some of these can be mapped directly to π -calculus
operators, but others require more sophistication.

Definition 14 (Sequential Composition). Let Op 1 and Op 2 be operations.
Then their sequential composition is also an operation and is written as:

Op 1 ; Op 2

Moreover,

[ Op 1 ; Op 2 ] π =( νstart )[ Op 1 ] π { start/done }| start. [ Op 2 ] π