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

We may now define the Stimulation function present in each state as follows.
Definition 11 (Stimulation)
Let

be the tran-
sition relation induced by the π -calculus operational semantics. Then, for all
s

( P, Stimulation, Response ) be a state. Moreover, let →

∈ Stimuli and n ∈ AgentIDs , we have:

⎧
⎨

beginning s
→

P such that unr P

Absent if ∃ ( P )

stable s
→ Beginning if ∃ P such that unr ( P ) P

Stimulation ( n, s )=

ending s
→

⎩

P such that unr P

Stable if ∃ ( P )

absent s
→ P such that unr P Ending if ∃ ( P )

The Stimulation definition establishes the status of a particular stimulation
based on the order that stimulations must change (see Def. 5). For instance, if
a process is capable of receiving a beginning s event, it must be the case that
stimulus s is currently absent in agent identified by n .The Stimulation function,
therefore, merely gives a way of reading the π -calculus LTS in order to have this
information explicitly for every agent and stimulus in any given process.
The Response function, on the other hand, is assumed as given (e.g., by a
simulator that implements the black-box behavior of the agents). Thus, we do
not define it. However, it imposes some constraints on the LTS, which we must
specify and take in account. As we shall see shortly, these constraints turn the π -
calculus over-approximation into an exact description of the transition system's
structure that we wish to assign to EMMAS.
Definition 12 (Transition constraints)
Let s 1 =(

P 1 , Stimulation 1 ,Response 1 ) and

s 2 =( P 2 , Stimulation 2 ,Response 2 ) be states in an annotated environment

LTS be the transition relation induced by the π -

calculus operational semantics. Then the transition s 1

S, L, . Moreover, let →

l

s 2 is forbidden if one

of the cases hold:
- there exists a

∈ Actions and n ∈ AgentIDs such that:

• Response 1 ( n, a )= Emitting ;

P 2 was obtained by internally producing the event stop a in P 1 .
- there exists a

•

∈ Actions and n ∈ AgentIDs such that:

• Response 1 ( n, a )= NotEmitting ;

P 2 was obtained by internally producing the event emit a in P 1 .
- there exists a

•

∈ Actions and n ∈ AgentIDs such that:

• Response 1 ( n, a )= Emitting ;

• Response 2 ( n, a )= NotEmitting ;

emit a
→

there exists a P P .

• such that unr ( P 1 )

- there exists a ∈ Actions and n ∈ AgentIDs such that:

• Response 1 ( n, a )= NotEmitting ;

• Response 2 ( n, a )= Emitting ;

stop a
→ •

there exists a P such that unr

( P 1 ) P .