=Paper=
{{Paper
|id=Vol-1382/paper19
|storemode=property
|title=Outline of a Formalization of JADE Multi-Agent Systems
|pdfUrl=https://ceur-ws.org/Vol-1382/paper19.pdf
|volume=Vol-1382
|dblpUrl=https://dblp.org/rec/conf/woa/BergentiIP15
}}
==Outline of a Formalization of JADE Multi-Agent Systems==
https://ceur-ws.org/Vol-1382/paper19.pdf
Proc. of the 16th Workshop “From Object to Agents” (WOA15) June 17-19, Naples, Italy
Outline of a Formalization
of JADE Multi-Agent Systems
Federico Bergenti Eleonora Iotti, Agostino Poggi
Dipartimento di Matematica e Informatica Dipartimento di Ingegneria dell’Informazione
Università degli Studi di Parma Università degli Studi di Parma
Parco Area delle Scienze 53/A, 43124 Parma, Italy Parco Area delle Scienze 181/A, 43124 Parma, Italy
Email: federico.bergenti@unipr.it Email: eleonora.iotti@studenti.unipr.it, agostino.poggi@unipr.it
Abstract—This paper proposes a formalization of JADE agents reviewed in terms of the proposed semantics. No refinement
and multi-agent systems based on transition systems. The first of the JADE agent model is proposed and the semantics is
section introduces the aims and scope of the research and it ground on the semantics of Java classes. We always assume
focuses the content of the paper. The second section enumerates the availability of an underlying Java transition system and we
the abstractions and the structures used in the formalization. refrain from formalizing it because it is a critical topic out of
Successively, third section presents the formal semantics of the
the scope of this paper (see, e.g., [10]).
parts of a JADE-based source code that are involved in the
management of (i) the life cycle of agents and (ii) the behaviours For the sake of brevity, only an outline of the proposed
of agents. Fourth section shows a very simple JADE agent and
it exemplifies the use of the proposed transition system. Finally,
semantics is presented in this paper, and interested readers are
a brief recapitulation of the work concludes the paper. invited to consult an upcoming paper that provides a complete
description of the formalization.
I. I NTRODUCTION
JADE [1] is today one of the most widely used tools for the II. D EFINITIONS AND T ERMINOLOGY
development of multi-agent systems both in research and in the
industry. It is a core component of a complex software system The proposed formalization considers only five main en-
that helps managing one of the most penetrating telecommu- tities that collectively describe a JADE multi-agent system.
nication networks in Europe, serving millions of consumers The first of such entities is the multi-agent system itself—the
daily [2]. It has been recently enhanced to support smart MAS—which is seen as a sort of environment where agents
appliances [3], and it is the base of a recent initiative intended live. Such an environment is subject to internal and external
to revitalize the use of software agents to support social events that may modify its state and the state of each agent
activities [4], both cooperative (see, e.g., [5], [6]) and com- belonging to the MAS. Also, a MAS accounts for all entities
petitive. Besides this, JADE was initially conceived primarily that we need to formalize the JADE system: within a MAS
as a practical tool to help researchers experimenting with we are able to see all agents and their respective behaviours.
FIPA technology (www.fipa.org). JADE was recognized by The second entity that we consider is the agent. An agent is
FIPA community as the tool that most accurately implemented a complex entity that has a state, detailed in Section II-C,
FIPA specifications, and it was often used for validating new and a list of behaviours. The behaviour is the third entity that
specifications and for assessing the conformance of other we consider: it has a state, a type and an associated action.
tools to FIPA guidelines and specifications. Moreover, it was Actions are not entities in the proposed formalization, and
often selected to experiment potential enhancements to FIPA they are always associated to behaviours. Actually, we may
specifications (see, e.g., [7]), and to gather the interest of think of an action as a list of activites that an agent performs
FIPA members on common projects (see, e.g., [8]). Such a when it decides to activate the behaviour that encapsulates
close relationship with an official standardization body forced the action. The type of the behaviour changes the way the
JADE architects to let the design of JADE APIs open, so that agent performs the associated action, e.g., a cyclic behaviour
third-party developers could adopt JADE—and FIPA together permits the agent to perform the action cyclically; conversely,
with it—with minimal restrictions. For example, the agent a one-shot behaviour in meant to have the action performed
model that JADE provides was intentionally left simple and only once. Each agent (respectively, behaviour) belongs to one
not formally specified so that developers were not forced to agent class (respectively, behaviour class), and such classes are
adopt a specific agent model just because they wanted their the last two of the five entities that we consider. An agent
agents to be FIPA compliant. class is defined as a group of agents that have behaviours
belonging to the same classes, and a behaviour class is a group
After more than 15 years of JADE development and use, of behaviours that have the same type and the same action. It
this paper first proposes a formal semantics of JADE agents is worth noting that the word class was chosen to identify
and multi-agent systems to support reasoning on JADE-based the means that JADE provides to group agents and behaviours
software systems. The proposed semantics is based on transi- by specific properties, i.e., Java classes. This choice implicitly
tion systems [9] and it closely follows the intended meaning of types agents, but this work does not address this issue and
JADE APIs to ensure that properly written JADE agents can be related issues (see, e.g., [11]).
123
Proc. of the 16th Workshop “From Object to Agents” (WOA15) June 17-19, Naples, Italy
A. Constants Similarly, we define the function β that accesses the state of
a behaviour as
In order to give a formal definition of the aforementioned
five entities, we choose a first-order language whose alphabet β : I → B. (7)
consists of a finite set of constants, predicate symbols, function
symbols, and the usual logical symbols (i.e., variables, connec- The composition α ◦ aid : V → A associates an agent to
tives, and quantifiers). We let C be the finite set of constants a variable in the first-order language, while the composition
and V the countably infinite set of variables. β ◦ bid : V → B does the same with respect to a behaviour.
In order to account for the life cycle state of an agent, we We may write α(a) instead of α(aid(a)) with a slight abuse
define specific constants:initiated, deleted, active, of notation when the intended meaning is evident from the
suspended, and waiting. Similarly, the life cycle state of context.
a behaviour is described by constants initiated, active,
done, and blocked. We call SA the finite set of the agent C. Events
life cycle state constants, and SB the finite set of behaviour
life cycle state constants. Each behaviour needs a type and a A MAS is constantly subject to two types of events: internal
description of its internal state: we call T and S the sets of and external. Each agent is fed with a sub-sequence of such
such constants, respectively. Moreover, we also need a finite events in its life. Some of such events are particularly important
set of constants that describes the state of the environment because they can change the state of the MAS (these are
where agents live, which we call W. the external events), and/or the state of agents and respective
behaviours (these are the internal events). The set of such
In summary, the set of constants that we allow for the notable events that JADE manages, which we call E, contains
first-order language used to describe the proposed semantics the following events:
is composed of the union of all aforementioned sets:
• Create(a, F ) denotes the creation of the agent a of
C = SA ∪ SB ∪ T ∪ S ∪ W. (1) class F ;
• Kill(a) denotes the destruction of the agent a;
B. Variables and identifiers
• Wait(a) denotes the state change of the agent a to the
In addition to constants and variables, we define a set of state waiting;
identifiers called I. Every time an entity is created, it gets a
name from such a set. Each agent class and behaviour class is • Wake(a) denotes the state change of the agent a from
associated with a specific identifier in the set I. Therefore we waiting to active;
need a semantic structure that associates the name of the class • Suspend(a) denotes the state change of the agent a
to the class itself. We call FA the set of all agents classes and to the state suspended;
FB the set of all behaviour classes. Such semantic structures
are called semantic contexts of the classes, and they are • Activate(a) denotes the state change of the agent a
from suspended to the state it had before becoming
ρA : I → FA , (2) suspended;
ρB : I → FB . (3) • Create(a, b, F ) denotes the creation of the behaviour
b of class F and agent a;
In JADE, each agent has a name and a global unique
• Block(b) denotes the state change from active to
identifier (called AID, for agent identifier), which contains its
blocked for the behaviour b;
local name and its platform name. So we can consider the AID
as a structured identifier defined a function • Restart(b) denotes the state change from blocked
to active for the behaviour b;
aid : V → I (4)
• Start(MAS) denotes the first event that occurs in the
that maps a variable a representing an agent to its AID. MAS; and
Moreover, each behaviour has a name, which is its unique
identifier. We can access such an identifier through the function • End(MAS) denotes the event that marks the termina-
tion of the MAS (with all agents and behaviours); it
bid : V → I. (5) is the last event that occurs in a computation of the
MAS.
Each agent (respectively, behaviour) needs to be instanti- The events in E that denotes changes in the state of an
ated and maintained in a semantic structure, here generically agent are related to each other as shown in Figure II-C (left).
called heap, which associates a concrete reference (i.e., an Similarly, Figure II-C (right) shows the finite state machine
identifier) to the representation of the agent (respectively, that represents the state changes of a behaviour.
behaviour). We call A the set of all agents and B the set
of all behaviours, and we define a function α that accesses the In order to analyze the life cycle of agents and behaviours,
state of an agent as we need to consider which event occurs in single steps of the
computation: if e ∈ E and t ∈ N, the pair ht, ei means that
α : I → A. (6) the event e occurred at step t.
124
Proc. of the 16th Workshop “From Object to Agents” (WOA15) June 17-19, Naples, Italy
Kill(a)
Suspend(a)
q2 q4 q1
Create(a, b, F )
Activate(a)
Kill(a)
q0 Wake(a) Wait(a) q5 q0 q3
Block(b) Restart(b)
Kill(a)
Create(a, F ) Activate(a)
q1 q3
q2
Suspend(a)
Kill(a)
Figure 1. Agent (left) and behaviour (right) life cycle events and their relationships. For agents: q0 = initiated, q1 = active, q2 = waiting,
q3 = suspended_from_active, q4 = suspended_from_waiting and q5 = deleted; for behaviours q0 = initiated, q1 = active,
q2 = blocked and q3 = done.
D. Structures Definition 3 (MAS): A MAS is defined by a tuple
An agent class is a pair Fa = hLB , ϕi, where LB is a list MAS = hA0 , B 0 , LE iT (10)
of possible behaviours and ϕ a function that maps the names
of its methods (in the set I of identifiers) to the associated where A0 ⊆ A is a finite set of agents, B 0 ⊆ B is a finite set
blocks of code, i.e., sequences of statements written in Java of behaviours, LE is the list of events occurred in this MAS
with JADE. up to time step T ∈ N.
Similarly, a behaviour class is a pair Fb = ht, ψi, where In addition, to support the semantics described in next
t ∈ T ⊆ C fixes the type of the behaviour in the class (e.g., section, we define Sb , a selector for the behaviours of an agent,
cyclic or one-shot), and ψ is a function that associates specific i.e., the behaviour scheduler. Such a function computes the
names to the related blocks of code. current behaviour to execute, from the list Lb of an agent a as
In JADE, an agent is an entity that belongs to a particular
Sb : A0 → B 0 . (11)
class and that has a list of behaviours. So, an agent is
completely described by the name of its class and by its state,
as follows. III. S EMANTICS
Definition 1 (Agent): An agent is a tuple The semantics of the life cycle of agents, given the events
described in Section II-C, is described in the form of a labelled
hF, sa , sw , Lb , Le i ∈ A (8) transition system (see, e.g., [9]). The proposed transition
where F ∈ I is the identifier of the class, sa ∈ SA is the state system, called MAS transition system, is a pair hΓ, →i where
of the agent, sw ∈ W the state of the environment seen by the Γ is a finite set of configurations and → is a binary relation on
agent, Lb is a finite list of behaviours and Le a finite list of Γ. Once a MAS is fixed, the labels of such a transition system
events. are the pairs time-event defined above.
Similarly, we can define a behaviour as a specific entity Definition 4 (Configuration): A configuration in the tran-
which belongs to a class, as follows. sition system is described by a tuple
Definition 2 (Behaviour): A behaviour is a tuple hC, σ, α, βi ∈ Γ (12)
hF, myAgent, sb , sw , si ∈ B (9)
where C is a command, σ represents the state (stores and
where F ∈ I is the identifier of the class, myAgent ∈ I is environments) of the underlying Java system, α and β are
the unique identifier of the associated agent, sb ∈ SB is the the heaps that represent the state of all agents and of all
state of the behaviour, sw ∈ W is the state of the environment behaviours, respectively.
seen by the behaviour and s ∈ S is the internal state of the
For the sake of clarity and when no ambiguity can arise, we
behaviour. We call B the set of all behaviours.
may not enumerate all four elements of a configuration in the
In JADE, each agent lives within a MAS and therefore, for description of transition rules. Moreover, we use the symbol
every time step T we can consider a global list of events LE ε for a configuration with no commands. The abstract syntax
that occurred to all agents of that MAS since its activation, used for a command (or statement) C is the Java syntax, as
i.e., since event Start(MAS). defined, e.g., in [10].
125
Proc. of the 16th Workshop “From Object to Agents” (WOA15) June 17-19, Naples, Italy
Each transition refers to an environment, or semantic B. Agent life cycle
context. In this case, we use the class contexts defined in
Section II-D. So, for example, a transition may be written as We describe the life cycle of a generic agent, instantiated
follows in the MAS hA0 , B 0 , LE iT , starting from its creation. When
a new agent a ∈ A of class Fa = hLB , ϕi is created, it is
ht,ei
ρA , ρB `N hC, σ, α, βi −−−→ hC 0 , σ 0 , α0 , β 0 i. (13) memorized in a location a of the heap α and the function
setup of its class is executed. We assume that the code of
where ρA and ρB are the class contexts and N ⊆ I ∪ V is the method setup is accessible from the function ϕ of the
a finite set of names, i.e., identifiers or variables used in the agent class
transition. ϕ(setup) = {B}. (17)
A. Semantics of commands with events In this case, the MAS system has the transition
We need a formal semantics to manage the events and ht,ei
ρA ` hε, αi −−−→ ha.setup(){B}, α0 i (18)
the state changes that occur in the life cycle of an agent. To
this extent, we use a subsystem of the main MAS transition where α = α[hF, initiated, ω, [], [Create(a, F )]i/a].
0
system. Such a subsystem has the same configuration of the Note that the agent class context is crucial within this transition
MAS system, but the transition relation is called →com . The because it gives us the necessary information regarding the
execution of such a system may be interrupted by an event that setup method.
may cause a state change: this is represented by taking the label
on the transition relation that indicates the current execution The block B of the agent setup is computed by the
step and by matching it with the event just occurred. Notably, commands transition system, as follows
at some execution step no event occurs, and we indicate them ht,ei
with ht, $i. ρA `a hB, σ, α, βi −−−→com hε, σ 0 , α0 , β 0 i ...
(19)
ht,ei
Let us consider a fixed MAS hA0 , B 0 , LE iT . A list of ρA ` ha.setup(){B}, σ, α, βi −−−→ hε, σ 0 , α00 , β 0 i
statements, indicated with C1 ; C2 , is computed as usual from where α00 = α0 [hF, active, sw , Lb , Le i/a].
left to right taking care of the propagation of the current event,
as shown by the rule During setup, agent a can add and/or remove behaviours
from its list Lb , through the following statements
ht,ei
hC1 , σ, α, βi −−−→com hε, σ 0 , α0 , β 0 i
. (14) addBehaviour(b), removeBehaviour(b).
ht,ei
hC1 ; C2 , σ, α, βi −−−→com hC2 , σ 0 , α0 , β 0 i
It is worth noting that such statements can be used also inside
the action of a behaviour, and not only in the setup method,
When no event occurs, as we can see in the rule (15), to change the list of behaviours dynamically. Finally, after
the statement C is computed by means of the underlying Java setup, the agent enters the active state and it becomes
semantics system, which we call →jstmt ready to select a behaviour in its list. The life of an agent
hC, σi →jstmt hε, σ 0 i continues by performing actions of behaviours until the event
. (15) Kill(a) occurs. When an agent a is killed, it computes the
ht,$i
hC, σi −−−→com hε, σ 0 i function takeDown. Only after the execution of takeDown
the agent a is removed from the heap by assigning α(a) = $.
We work under the reasonable assumption that such a
subsystem may change only the state σ and we do not consider C. Behaviour actions
changes in all stores and environments of Java.
If α(a) = a = hF0 , sa , s0w , Lb , Le i ∈ A0 is an instantiated
We then define specific rules to update the state of an agent. agent and β(b) = b = hF, a, active, sw , si ∈ B 0 is a
When an event e related to the agent a = hF, sa , sw , Lb , Le i behaviour that appears in the list of the agent, i.e., b ∈ Lb , then
occurs, sa is changed to a new state, and e is stored in the list the behaviour may be selected by the behaviour scheduler of
of events Le . Similarly, we define rules for the behaviour state the agent to perform the relative action, i.e., Sb (a) = b. The
changes. In this case, there is no need for a list of events inside transition of the main system then calls the action method
the behaviour entity, as shown in Figure II-C. For example, of the class of b
the following rule describes the state change from active to
blocked ρB ` hε, σ, α, βi → hb.action(){C}, σ, α, βi.
e = Block(b) β(b) = hF, active, sw , si Just like for the method setup of the agent, the block of code
. (16)
ht,ei C of action is executed by the subsystem →com .
hC, βi −−−→com hC, β[hF, blocked, sw , si/b]i
A one-shot behaviour terminates after a single execution
There is no explicit rule for the change from active to of its action, and it is removed from the list of behaviours of
done because the latter is reached only after the execution the agent, through the function removeBehaviour. So, if
of the action for a one-shot behaviour, and cyclic behaviours the agent is still alive, the behaviour scheduler chooses another
never change to done. Obviously the event End(MAS) stops behaviour. On the contrary, if the behaviour b is cyclic, then
all behaviours and agents in a MAS, forcing them to reach its action is performed cyclically and it is never automatically
their respective final states. removed from the list of behaviours of the agent.
126
Proc. of the 16th Workshop “From Object to Agents” (WOA15) June 17-19, Naples, Italy
ht,ei
ρA , ρB `a,b hC;removeBehaviour(b), σ, α, βi −−−→com hε, σ 0 , α0 , β 0 i
. . . β 0 (b) = hF, a, active, sw , si
(20)
ht,ei
ρB ` hb.action(){C}, σ, α, βi −−−→ hε, σ 0 , α0 , β 0 [hF, a, done, sw , si/b]i
ht,ei
ρA , ρB `a,b hC;removeBehaviour(b), σ, α, βi −−−→com hε, σ 0 , α0 , β 0 i
. . . β 0 (b) = hF, a, blocked, sw , si
(21)
ht,ei
ρB ` hb.action(){C}, σ, α, βi −−−→ hε, σ 0 , α0 , β 0 i
Figure 2. Rules governing the transition of a one-shot behaviour from the active to the blocked state. The behaviour scheduler of an agent can select only
behaviours that are in the active state.
Note that a necessary condition for the scheduler Sb (a) ϕ(setup) = {
to choose a behaviour is that it must be in the active state. Greetings greetings =
A behaviour is normally in the active state, but it can reach
new Greetings(this);
the blocked state during the execution of its action. When this
occurs, the execution continues up to the natural termination addBehaviour(greetings);
of the action and the blocked behaviour is not removed from }
the list of behaviours. Anyway, the scheduler cannot choose
it until it returns to the active state, as detailed, for one-shot
ψ(action) = {
behaviours, in rules (20) and (21), summarized in Figure 2.
System.out.println("Hello world");
IV. A D IDACTIC E XAMPLE }
This section discusses a simple example of JADE agent and
shows its semantics according to the transition system outlined Suppose that the MAS starts at execution step 0, and
in previous sections. The simple agent has the following source that the first event that occurs is the creation of agent hello,
code. belonging to the class HelloAgent
1 import j a d e . c o r e . Agent ; e0 = h0, Start(MAS)i MAS = h∅, ∅, [e0 ]iT
2 import j a d e . c o r e . b e h a v i o u r s . O n e S h o t B e h a v i o u r ;
3
↓
4 p u b l i c c l a s s H e l l o A g e n t e x t e n d s Agent { e1 = h1, Create(hello, HelloAgent)i
5 protected void s e t u p ( ) { A0 = {hello}, LE = [e1 , e0 ].
6 G r e e t i n g s g r e e t i n g s = new G r e e t i n g s ( t h i s ) ;
7
Variable hello allows retrieving the information about the new
8 addBehaviour ( g r e e t i n g s ) ;
9 } agent, and we can access its AID by function aid(hello) =
10
hello, and control its state thanks to the heap α.
11 private s t a t i c c l a s s Greetings extends
OneShotBehaviour { The event Create(hello, HelloAgent) activates the first
12 p u b l i c G r e e t i n g s ( Agent a ) { transition
13 super ( a ) ; e
14 }
1
ρA ` hε, αi −→ hhello.setup(){B}, αi i
15
16 public void a c t i o n ( ) { where {B} is the block of code obtained by ϕ(setup) and
17 System . o u t . p r i n t l n ( ” H e l l o w o r l d ” ) ;
18 } αi = α[hHelloAgent, initiated, ω, [], [e1 ]i
19 } /hello].
20 }
Class HelloAgent defines an agent class and its static Suppose that no event occurs at execution step 2: the main
inner class a behaviour class. This is formalized by setting transition system enters in the subsystem →com , as follows.
the pairs hLB , ϕi and ht, ψi using the information contained
in the source code. Then, the context is initialized to create ρA `hello hGreetings greetings =
a reference between the identifier of classes and their relative new Greetings(), σ, αi , βi
structures, as follows. ↓ e3
ρA (HelloAgent) = hLB , ϕi haddBehaviour(greetings), σ i , αi , β i i
ρB (Greetings) = hone-shot, ψi ↓ e4
LB = [Greetings] hε, σ , αii , β i i
ii
127
Proc. of the 16th Workshop “From Object to Agents” (WOA15) June 17-19, Naples, Italy
where σ ii is obtained from a transition of the Java subsystem where E is a special command which denotes the termination
→jstmt , called at every execution step, and of the execution. The event occurred are summarized below.
e2 = h2, $i
β i = β[hGreetings, hello, active, ω, ωi
↓
/greetings]
e3 = h3, Create(hello, greetings, Greetings)i
↓
αii = αi [hHelloAgent, initiated, e4 = h4, $i
ω, [greetings], [e3 , e1 ]i/hello]. ↓
e5 = h5, $i
This transition is necessary to apply rule (19) ↓
e
e6 = h6, $i
ρA `hello hB, σ, αi , βi −→
2 ii ii i
com hε, σ , α , β i ... ↓
2 e
ρA ` hhello.setup(){B}, σ, αi , βi −→ hε, σ ii , αiii , β i i e7 = h7, End(MAS)i
where the state of the agent is eventually changed to active
V. C ONCLUSIONS
αiii = αii [hHelloAgent, active,
ω, [greetings], [e3 , e1 ]i/hello]. This paper provides an outline of the major ingredients of
a semantics of JADE agents and multi-agent systems based
on transition systems. The five main entities that we consider,
Then, because agent hello is active, the scheduler can choose namely the multi-agent system, agents and their classes, be-
a behaviour to execute. The only behaviour in the list of haviours and their classes, are discussed. The paper provides
behaviours of the agent is greetings so Sb (hello) = greetings an example of the transition system that can be obtained from
a very simple JADE agent. The complete description of the
ρB ` hε, σ ii , αiii , β i i semantics cannot fit the constraints of a workshop paper and
↓ e5 interested readers are directed to an upcoming journal paper
hgreetings.action(){B}, σ ii , αiii , β i i. that also discusses the complete semantics of message passing.
The block of code {B} of the action, accessed through the R EFERENCES
function ψ, is executed in the →com subsystem, as follows. [1] F. Bellifemine, G. Caire, and D. Greenwood, Developing multi-agent
systems with JADE. Wiley Series in Agent Technology, 2007.
ρA , ρB `hello,greetings [2] F. Bergenti, G. Caire, and D. Gotta, “Large-scale network and service
management with WANTS,” in Industrial Agents: Emerging Applica-
hSystem.out.println("Hello world")σ ii , αiii , β i i tions of Software Agents in Industry. Elsevier, 2015, pp. 231–246.
↓ e6 [3] F. Bergenti, G. Caire, and D. Gotta, “Agents on the move: JADE for
Android devices,” in Procs. Workshop From Objects to Agents, 2014.
hε, σ iii , αiii , β i i
[4] F. Bergenti, G. Caire, and D. Gotta, “Agent-based social gaming with
AMUSE,” in Procs. 5th Int’l Conf. Ambient Systems, Networks and
where σ iii is obtained by the Java transition system. According Technologies (ANT 2014) and 4th Int’l Conf. Sustainable Energy
to rule (20), at the end of the computation of its action, the Information Technology (SEIT 2014), ser. Procedia Computer Science.
Elsevier, 2014, pp. 914–919.
state of the behaviour is changed to done.
[5] F. Bergenti and A. Poggi, “Agent-based approach to manage negoti-
ii iii i
ation protocols in flexible CSCW systems,” in Procs. 4th Int’l Conf.
ρA , ρB `hello,greetings hB, σ , α , β i Autonomous Agents, 2000, pp. 267–268.
6 e iii iii i [6] F. Bergenti, A. Poggi, and M. Somacher, “A collaborative platform
−→ com hε, σ , α , β i ...
. for fixed and mobile networks,” Communications of the ACM, vol. 45,
ρA ` hgreetings.action(){B}, σ ii , αiii , β i i no. 11, pp. 39–44, 2002.
e
6
−→ hε, σ iii , αiii , β ii i [7] F. Bergenti and A. Poggi, “Ubiquitous information agents,” Int’l J.
Cooperative Information Systems, vol. 11, no. 34, pp. 231–244, 2002.
In fact: [8] F. Bergenti, A. Poggi, B. Burg, and G. Caire, “Deploying FIPA-
compliant systems on handheld devices,” IEEE Internet Computing,
vol. 5, no. 4, pp. 20–25, 2001.
β ii = β i [hGreetings, hello, done, ω, ωi [9] G. D. Plotkin, “A Structural approach to Operational Semantics,” J. Log.
/greetings] Algebr. Program., vol. 60-61, pp. 17–139, 2004.
[10] J. Alves-Foss, Formal syntax and semantics of Java. Springer Science
& Business Media, 1999, no. 1523.
Let us now suppose that when T = 7 the event End(MAS)
[11] M. Baldoni, C. Baroglio, and F. Capuzzimati, “Typing multi-agent sys-
occurs, thus producing the following transition tems via commitments,” Post-Procs. 2nd Int’l Workshop on Engineering
Multi-Agent Systems (EMAS 2014), Revised Selected and Invited Papers,
e
ρA , ρB ` hε, σ iii , αiii , β ii i −→
7
hE, σ iii , αiii , β ii i pp. 388–405, 2014.
128