-This paper proposes a formalization of JADE agents and multi-agent systems based on transition systems. The first section introduces the aims and scope of the research and it focuses the content of the paper. The second section enumerates the abstractions and the structures used in the formalization. Successively, third section presents the formal semantics of the parts of a JADE-based source code that are involved in the management of (i) the life cycle of agents and (ii) the behaviours of agents. Fourth section shows a very simple JADE agent and it exemplifies the use of the proposed transition system. Finally, a brief recapitulation of the work concludes the paper.
I. INTRODUCTION
JADE [
After more than 15 years of JADE development and use,
this paper first proposes a formal semantics of JADE agents
and multi-agent systems to support reasoning on JADE-based
software systems. The proposed semantics is based on
transition systems [
For the sake of brevity, only an outline of the proposed semantics is presented in this paper, and interested readers are invited to consult an upcoming paper that provides a complete description of the formalization.
II.
The proposed formalization considers only vfie main
entities that collectively describe a JADE multi-agent system.
The first of such entities is the multi-agent system itself—the
MAS—which is seen as a sort of environment where agents
live. Such an environment is subject to internal and external
events that may modify its state and the state of each agent
belonging to the MAS. Also, a MAS accounts for all entities
that we need to formalize the JADE system: within a MAS
we are able to see all agents and their respective behaviours.
The second entity that we consider is the agent. An agent is
a complex entity that has a state, detailed in Section II-C,
and a list of behaviours. The behaviour is the third entity that
we consider: it has a state, a type and an associated action.
Actions are not entities in the proposed formalization, and
they are always associated to behaviours. Actually, we may
think of an action as a list of activites that an agent performs
when it decides to activate the behaviour that encapsulates
the action. The type of the behaviour changes the way the
agent performs the associated action, e.g., a cyclic behaviour
permits the agent to perform the action cyclically; conversely,
a one-shot behaviour in meant to have the action performed
only once. Each agent (respectively, behaviour) belongs to one
agent class (respectively, behaviour class), and such classes are
the last two of the vfie entities that we consider. An agent
class is defined as a group of agents that have behaviours
belonging to the same classes, and a behaviour class is a group
of behaviours that have the same type and the same action. It
is worth noting that the word class was chosen to identify
the means that JADE provides to group agents and behaviours
by specific properties, i.e., Java classes. This choice implicitly
types agents, but this work does not address this issue and
related issues (see, e.g., [
In order to give a formal definition of the aforementioned vfie entities, we choose a first-order language whose alphabet consists of a finite set of constants, predicate symbols, function symbols, and the usual logical symbols (i.e., variables, connectives, and quantifiers). We let C be the finite set of constants and V the countably infinite set of variables.
In order to account for the life cycle state of an agent, we define specific constants: initiated, deleted, active, suspended, and waiting. Similarly, the life cycle state of a behaviour is described by constants initiated, active, done, and blocked. We call SA the finite set of the agent life cycle state constants, and SB the finite set of behaviour life cycle state constants. Each behaviour needs a type and a description of its internal state: we call T and S the sets of such constants, respectively. Moreover, we also need a finite set of constants that describes the state of the environment where agents live, which we call W.
In summary, the set of constants that we allow for the first-order language used to describe the proposed semantics is composed of the union of all aforementioned sets:
C = SA ∪ SB ∪ T ∪ S ∪ W.
In addition to constants and variables, we define a set of identifiers called I. Every time an entity is created, it gets a name from such a set. Each agent class and behaviour class is associated with a specific identifier in the set I. Therefore we need a semantic structure that associates the name of the class to the class itself. We call FA the set of all agents classes and FB the set of all behaviour classes. Such semantic structures are called semantic contexts of the classes, and they are ρA : I → FA, ρB : I → FB. aid : V → I bid : V → I.
In JADE, each agent has a name and a global unique identifier (called AID, for agent identifier), which contains its local name and its platform name. So we can consider the AID as a structured identifier defined a function that maps a variable a representing an agent to its AID. Moreover, each behaviour has a name, which is its unique identifier. We can access such an identifier through the function Similarly, we define the function β that accesses the state of a behaviour as β : I → B. (7)
The composition α ◦ aid : V → A associates an agent to a variable in the first-order language, while the composition β ◦ bid : V → B does the same with respect to a behaviour. We may write α(a) instead of α(aid(a)) with a slight abuse of notation when the intended meaning is evident from the context.
A MAS is constantly subject to two types of events: internal and external. Each agent is fed with a sub-sequence of such events in its life. Some of such events are particularly important because they can change the state of the MAS (these are the external events), and/or the state of agents and respective behaviours (these are the internal events). The set of such notable events that JADE manages, which we call E, contains the following events: • • • • • • • • • • •
Create(a, F ) denotes the creation of the agent a of class F ; Kill(a) denotes the destruction of the agent a; Wait(a) denotes the state change of the agent a to the state waiting; Wake(a) denotes the state change of the agent a from waiting to active; Suspend(a) denotes the state change of the agent a to the state suspended; Activate(a) denotes the state change of the agent a from suspended to the state it had before becoming suspended; Create(a, b, F ) denotes the creation of the behaviour b of class F and agent a; Block(b) denotes the state change from active to blocked for the behaviour b; Restart(b) denotes the state change from blocked to active for the behaviour b; Start(MAS) denotes the first event that occurs in the MAS; and End(MAS) denotes the event that marks the termination of the MAS (with all agents and behaviours); it is the last event that occurs in a computation of the MAS. (1) (2) (3) (4) (5) (6)
Each agent (respectively, behaviour) needs to be instantiated and maintained in a semantic structure, here generically called heap, which associates a concrete reference (i.e., an identifier) to the representation of the agent (respectively, behaviour). We call A the set of all agents and B the set of all behaviours, and we define a function α that accesses the state of an agent as α : I → A.
The events in E that denotes changes in the state of an agent are related to each other as shown in Figure II-C (left). Similarly, Figure II-C (right) shows the finite state machine that represents the state changes of a behaviour.
In order to analyze the life cycle of agents and behaviours, 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 the event e occurred at step t. q0
q2 q1
where A0 ⊆ A is a finite set of agents, B0 ⊆ B is a finite set of behaviours, LE is the list of events occurred in this MAS up to time step T ∈ N.
In addition, to support the semantics described in next section, we define Sb, a selector for the behaviours of an agent, i.e., the behaviour scheduler. Such a function computes the current behaviour to execute, from the list Lb of an agent a as q1 q2
Sb : A0 → B0.
The semantics of the life cycle of agents, given the events
described in Section II-C, is described in the form of a labelled
transition system (see, e.g., [
Definition 4 (Configuration): A configuration in the transition system is described by a tuple
hC, σ, α, βi ∈ Γ where C is a command, σ represents the state (stores and environments) of the underlying Java system, α and β are the heaps that represent the state of all agents and of all behaviours, respectively.
For the sake of clarity and when no ambiguity can arise, we
may not enumerate all four elements of a configuration in the
description of transition rules. Moreover, we use the symbol
ε for a configuration with no commands. The abstract syntax
used for a command (or statement) C is the Java syntax, as
defined, e.g., in [
An agent class is a pair Fa = hLB, ϕi, where LB is a list of possible behaviours and ϕ a function that maps the names of its methods (in the set I of identifiers) to the associated blocks of code, i.e., sequences of statements written in Java with JADE.
Similarly, a behaviour class is a pair Fb = ht, ψi, where t ∈ T ⊆ C fixes the type of the behaviour in the class (e.g., cyclic or one-shot), and ψ is a function that associates specific names to the related blocks of code.
In JADE, an agent is an entity that belongs to a particular 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.
An agent is a tuple hF, sa, sw, Lb, Lei ∈ A where F ∈ I is the identifier of the class, sa ∈ SA is the state of the agent, sw ∈ W the state of the environment seen by the agent, Lb is a finite list of behaviours and Le a finite list of events.
Similarly, we can define a behaviour as a specific entity which belongs to a class, as follows.
A behaviour is a tuple hF, myAgent, sb, sw, si ∈ B where F ∈ I is the identifier of the class, myAgent ∈ I is the unique identifier of the associated agent, sb ∈ SB is the state of the behaviour, sw ∈ W is the state of the environment seen by the behaviour and s ∈ S is the internal state of the behaviour. We call B the set of all behaviours.
In JADE, each agent lives within a MAS and therefore, for every time step T we can consider a global list of events LE that occurred to all agents of that MAS since its activation, i.e., since event Start(MAS). (8) (9)
Each transition refers to an environment, or semantic context. In this case, we use the class contexts defined in Section II-D. So, for example, a transition may be written as follows where ρA and ρB are the class contexts and N ⊆ I ∪ V is a finite set of names, i.e., identifiers or variables used in the transition.
We need a formal semantics to manage the events and the state changes that occur in the life cycle of an agent. To this extent, we use a subsystem of the main MAS transition system. Such a subsystem has the same configuration of the MAS system, but the transition relation is called →com. The execution of such a system may be interrupted by an event that may cause a state change: this is represented by taking the label on the transition relation that indicates the current execution step and by matching it with the event just occurred. Notably, at some execution step no event occurs, and we indicate them with ht, $i.
Let us consider a fixed MAS hA0, B0, LE iT . A list of statements, indicated with C1; C2, is computed as usual from left to right taking care of the propagation of the current event, as shown by the rule
ht,ei hC1, σ, α, βi −−−→com hε, σ0, α0, β0i
ht,ei hC1; C2, σ, α, βi −−−→com hC2, σ0, α0, β0i .
When no event occurs, as we can see in the rule (15), the statement C is computed by means of the underlying Java semantics system, which we call →jstmt hC, σi →jstmt hε, σ0i .
ht,$i hC, σi −−−→com hε, σ0i
We work under the reasonable assumption that such a subsystem may change only the state σ and we do not consider changes in all stores and environments of Java.
We then define specific rules to update the state of an agent. When an event e related to the agent a = hF, sa, sw, Lb, Lei occurs, sa is changed to a new state, and e is stored in the list of events Le. Similarly, we define rules for the behaviour state changes. In this case, there is no need for a list of events inside the behaviour entity, as shown in Figure II-C. For example, the following rule describes the state change from active to blocked e = Block(b) β(b) = hF, active, sw, si
ht,ei hC, βi −−−→com hC, β[hF, blocked, sw, si/b]i . (16)
There is no explicit rule for the change from active to done because the latter is reached only after the execution of the action for a one-shot behaviour, and cyclic behaviours never change to done. Obviously the event End(MAS) stops all behaviours and agents in a MAS, forcing them to reach their respective final states. (14) (15)
We describe the life cycle of a generic agent, instantiated in the MAS hA0, B0, LE iT , starting from its creation. When a new agent a ∈ A of class Fa = hLB, ϕi is created, it is memorized in a location a of the heap α and the function setup of its class is executed. We assume that the code of the method setup is accessible from the function ϕ of the agent class
ϕ(setup) = {B}.
In this case, the MAS system has the transition
ht,ei ρA ` hε, αi −−−→ ha.setup(){B}, α0i where α0 = α[hF, initiated, ω, [], [Create(a, F )]i/a]. Note that the agent class context is crucial within this transition because it gives us the necessary information regarding the setup method.
The block B of the agent setup is computed by the commands transition system, as follows
ht,ei ρA `a hB, σ, α, βi −−−→com hε, σ0, α0, β0i . . . ht,ei ρA ` ha.setup(){B}, σ, α, βi −−−→ hε, σ0, α00, β0i (19) where α00 = α0[hF, active, sw, Lb, Lei/a].
During setup, agent a can add and/or remove behaviours from its list Lb, through the following statements addBehaviour(b),
removeBehaviour(b).
It is worth noting that such statements can be used also inside the action of a behaviour, and not only in the setup method, to change the list of behaviours dynamically. Finally, after setup, the agent enters the active state and it becomes ready to select a behaviour in its list. The life of an agent continues by performing actions of behaviours until the event Kill(a) occurs. When an agent a is killed, it computes the function takeDown. Only after the execution of takeDown the agent a is removed from the heap by assigning α(a) = $. (17) (18)
If α(a) = a = hF0, sa, s0w, Lb, Lei ∈ A0 is an instantiated agent and β(b) = b = hF, a, active, sw, si ∈ B0 is a behaviour that appears in the list of the agent, i.e., b ∈ Lb, then the behaviour may be selected by the behaviour scheduler of the agent to perform the relative action, i.e., Sb(a) = b. The transition of the main system then calls the action method of the class of b
ρB ` hε, σ, α, βi → hb.action(){C}, σ, α, βi.
Just like for the method setup of the agent, the block of code C of action is executed by the subsystem →com.
A one-shot behaviour terminates after a single execution of its action, and it is removed from the list of behaviours of the agent, through the function removeBehaviour. So, if the agent is still alive, the behaviour scheduler chooses another behaviour. On the contrary, if the behaviour b is cyclic, then its action is performed cyclically and it is never automatically removed from the list of behaviours of the agent. ht,ei ρA, ρB `a,b hC;removeBehaviour(b), σ, α, βi −−−→com hε, σ0, α0, β0i . . .
β0(b) = hF, a, active, sw, si
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, β0i . . .
β0(b) = hF, a, blocked, sw, si
ht,ei ρB ` hb.action(){C}, σ, α, βi −−−→ hε, σ0, α0, β0i (20) (21)
Note that a necessary condition for the scheduler Sb(a) to choose a behaviour is that it must be in the active state. A behaviour is normally in the active state, but it can reach the blocked state during the execution of its action. When this occurs, the execution continues up to the natural termination 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 behaviours, in rules (20) and (21), summarized in Figure 2.
This section discusses a simple example of JADE agent and shows its semantics according to the transition system outlined in previous sections. The simple agent has the following source code. 1 import j a d e . c o r e . Agent ; 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 5 6 7 8 a d d B e h a v i o u r ( g r e e t i n g s ) ; 9 } 10 11 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 { p r o t e c t e d v o i d s e t u p ( ) {
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 ) ; p r i v a t e s t a t i c c l a s s G r e e t i n g s e x t e n d s
O n e S h o t B e h a v i o u r { p u b l i c G r e e t i n g s ( Agent a ) {
s u p e r ( a ) ; p u b l i c v o i d a c t i o n ( ) {
System . o u t . p r i n t l n ( ” H e l l o w o r l d ” ) ; 12 13 14 15 16 17 18 19 20 } } } }
Class HelloAgent defines an agent class and its static inner class a behaviour class. This is formalized by setting the pairs hLB, ϕi and ht, ψi using the information contained in the source code. Then, the context is initialized to create a reference between the identifier of classes and their relative structures, as follows.
ρA(HelloAgent) = hLB, ϕi ρB(Greetings) = hone-shot, ψi LB = [Greetings] ϕ(setup) = {
Greetings greetings =
new Greetings(this); addBehaviour(greetings); } } ψ(action) = {
System.out.println("Hello world");
Suppose that the MAS starts at execution step 0, and that the first event that occurs is the creation of agent hello, belonging to the class HelloAgent e0 = h0, Start(MAS)i
MAS = h∅, ∅, [e0]iT ↓ e1 = h1, Create(hello, HelloAgent)i
A0 = {hello}, LE = [e1, e0].
Variable hello allows retrieving the information about the new agent, and we can access its AID by function aid(hello) = hello, and control its state thanks to the heap α.
The event Create(hello, HelloAgent) activates the first transition
e1 ρA ` hε, αi −→ hhello.setup(){B}, αii where {B} is the block of code obtained by ϕ(setup) and αi = α[hHelloAgent, initiated, ω, [], [e1]i
/hello].
Suppose that no event occurs at execution step 2: the main transition system enters in the subsystem →com, as follows.
ρA `hello hGreetings greetings = new Greetings(), σ, αi, βi
↓ e3 haddBehaviour(greetings), σi, αi, βii
↓ e4 hε, σii, αii, βii where σii is obtained from a transition of the Java subsystem →jstmt, called at every execution step, and βi = β[hGreetings, hello, active, ω, ωi
/greetings] αii = αi[hHelloAgent, initiated,
This transition is necessary to apply rule (19)
e2 ρA `hello hB, σ, αi, βi −→com hε, σii, αii, βii . . . e2 ρA ` hhello.setup(){B}, σ, αi, βi −→ hε, σii, αiii, βii where the state of the agent is eventually changed to active αiii = αii[hHelloAgent, active,
Then, because agent hello is active, the scheduler can choose a behaviour to execute. The only behaviour in the list of behaviours of the agent is greetings so Sb(hello) = greetings
The block of code {B} of the action, accessed through the function ψ, is executed in the →com subsystem, as follows.
ρA, ρB `hello,greetings hSystem.out.println("Hello world")σii, αiii, βii where σiii is obtained by the Java transition system. According to rule (20), at the end of the computation of its action, the state of the behaviour is changed to done.
. . . ρA ` hgreetings.action(){B}, σii, αiii, βii .
βii = βi[hGreetings, hello, done, ω, ωi
/greetings] Let us now suppose that when T = 7 the event End(MAS) occurs, thus producing the following transition e7 ρA, ρB ` hε, σiii, αiii, βiii −→ hE, σiii, αiii, βiii where E is a special command which denotes the termination of the execution. The event occurred are summarized below.
↓ e3 = h3, Create(hello, greetings, Greetings)i
↓ e4 = h4, $i
↓ e5 = h5, $i
↓ e6 = h6, $i
↓ e7 = h7, End(MAS)i V.
This paper provides an outline of the major ingredients of a semantics of JADE agents and multi-agent systems based on transition systems. The vfie main entities that we consider, namely the multi-agent system, agents and their classes, behaviours and their classes, are discussed. The paper provides an example of the transition system that can be obtained from a very simple JADE agent. The complete description of the semantics cannot fit the constraints of a workshop paper and interested readers are directed to an upcoming journal paper that also discusses the complete semantics of message passing.