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

Agent Stimulation Operations. The following operations are provided to
control the stimulation of agents.
Definition 19 (Begin stimulation operation). Let ag = n, S, A be an

agent profile, and s ∈ S be a stimulus. Then the begin stimulation operation

is writen as:

BeginStimulation ( s, ag )

Moreover,

beginning s .stable s .done
Definition 20 (End stimulation operation). Let ag

[ BeginStimulation ( s, ag )] π =

= n, S, A be an agent

profile, and s

∈ S be a stimulus. Then the end stimulation operation is writen

as:

EndStimulation ( s, ag )

Moreover,

ending s .absent s .done
Definition 21 (Stimulate operation). Let ag

[ EndStimulation ( s, ag )] π =

= n, S, A be an agent profile,

and s ∈ S be a stimulus. Then the stimulate operation is defined as:

Stimulate ( s, ag )= BeginStimulation ( s, ag ); EndStimulation ( s, ag )

Action Transformers Operations. The following operations are provided to
manipulate action transformers.
Definition 22 (Create action transformer operation). Let ag 1 = n, S 1 ,A 1

be an agent profile, ag 2 = m, S 2 ,A 2 be another agent profile, a ∈ A 1 be an ac-

tion, and s ∈ S 2 be a stimulus. Then the create action transformer operation is

written as:

Create ( ag 1 ,a,s,ag 2 )

Moreover,
[ emit a ,stop a ,absent s , beginning s ,

stable s ,ending s ,destroy s,m

Create ( ag 1 ,a,s,ag 2 )] π = ccn (

) .done

a,n

In the above definition, notice that ccn is crafted to react with the component
NewAT given in Def. 4. Since operations will ultimately be put together with
parallel composition in the environment, it follows that the Create

ag 1 ,a,s,ag 2 )
operation will be able to react with NewAT and originate a new action trans-
former.
Definition 23 (Destroy action transformer operation). Let ag 1 =

(

n, S 1 ,

A 1 be an agent profile, ag 2 = m, S 2 ,A 2 be another agent profile, a ∈ A 1 be an

action, and s ∈ S 2 be a stimulus. Then the destroy action transformer operation

is writen as:

Destroy ( n, a, s, m )

Moreover,

destroy s,m

[ Destroy ( n, a, s, m )] π =

a,n .done