We introduce an extension of global and local types tailored to the description of FIPA agent interaction protocols, formalize one of such protocols with these types. This paper is the first step of an ongoing project aimed at the definition of agent systems correctly implementing protocols by construction. Introduction Dynamic systems are characterized by entities interacting in asynchronous ways. Software agents are software entities with the ability to [1]: react to environmental changes; take autonomous decisions and act accordingly to achieve their (explicit) goals; cooperate in loosely coupled Multi-Agent Systems (MASs). The interest in agent programming languages [2] dates back to the early proposals of agent technologies [3] and, since then, it has grown significantly. Agent programming languages represent an important research topic because they are recognized as important tools [4] to support Agent-Oriented Software Engineering (AOSE) [5] and applications [6]. Jadescript [7, 8] is an Agent-Oriented Programming (AOP) [3] language that was designed from participants of the current project [7] to support the construction of efective agents. The near-future development plans for Jadescript include a dedicated support for a collection of (agent) interaction protocols [9] standardized by the Foundation for Intelligent Physical Agents (FIPA, www.fipa.org), which is an IEEE Standards Committee established to promote interoperability among agents. FIPA specifies some generalpurpose interaction protocols and FIPA-compliant agents are requested to support at least some of them. FIPA encourages designers and programmers to adopt these interaction protocols, which motivates the need for a dedicated support for them in Jadescript. The seminal works on session types [10] and typestate have started a surge of research on behavioral type systems [11] for describing interaction protocols and enforcing various
properties including deadlock freedom [
The global types of [
A very expressive enhancement of global types was proposed in [
G ::= p → Q { ℓ⟨S⟩.G }∈ | X .G | X | End | for : ⟨R, q⟩ G1; G2 | → q Quit ̸= ∅ and ℓℎ ̸= ℓ for ℎ ̸= . local protocol name at R(p; ⟨R, q⟩) = T
T ::=
Q !{ ℓ⟨S⟩.T }∈
| p?{ ℓ⟨S⟩.T }∈
| X .T | X
| End
| for : ⟨R, q⟩ T1; T2
| !Quit | q ? Quit
X that can be used in its body to return to the beginning of G. As usual we assume recursion to
be guarded. End stands for the end of the protocol, but also the end of a sub-protocol as we
will see shortly. The for construct prescribes that the same protocol G1 be executed by all the
participants in the role set R. In G1 the variable denotes any participant in R. The semicolon
preceding G2 means that the coordinator q of R must have completed the protocol G1 on all
the participants in R before continuing as specified by G2. So End occurring in G1 does not
mean the end of the whole interaction, but just of the sub-protocol G1. In G1 there cannot
occur free recursion variables. We also impose the restriction that for cannot be nested. The
FIPA protocols analysed, so far, can be formalized without nesting of for. However, eventually
we would like to remove this restriction. Finally the last clause of the definition is used by a
participant in a role set to exit from the protocol. This means that subsequent messages sent
from the coordinator to the participants of its role set will not be sent to this participant. The
highlighted constructs are the extension w.r.t. [
The local/session types are the view of a protocol from the perspective of each participant. A local protocol declaration, , defined in Figure 2, specifies the participants and the role sets involved in the protocol from the point of view of a participant or role set and the associated local/session. The body of the declaration is a local/session type T.
For local types, we have the standard constructs: choice of outputs (sending a message) also
called internal choices, choice of inputs (receiving a message) also called external choices and
guarded recursion. Then we have for construct and the request and accept of the message
for exiting from the interaction. The for construct can only occur in the local type of the
coordinator of a role set and similar restrictions apply for the request and accept of the Quit
message. We now show how a FIPA protocol is described with our types. The example illustrates
also how the projection of the global type onto the participants and role sets is defined.
Global and Local Types for the Brokering Interaction Protocol In Figure 3 we formalize,
using our global types, the FIPA Brokering Interaction and in Figures 4 and 5 we give the
projections on its participants and role set. We use the Java-like syntax, coming from Scribble [
The participants of the protocol are the initiator, the broker and a number of agents in
1 global protocol myBrokering(role initiator,role broker,roleset Subagents:broker){
2 forward(string) from initiator to broker.
3 choice at broker{
4 refuse() from broker to initiator.
5 stop() from broker to Subagents.End
6 } or {
7 agree() from broker to initiator.
8 findAgent(string) from broker to Subagents.
9 for agent:<Subagents,broker>{
10 choice at agent {
11 notPossible() from agent to broker.
12 QUIT() from agent to broker
13 } or {
14 canDo() from agent to broker.End
15 }
16 } ;
17 choice at broker {
18 failureNoMacth() from broker to initiator.
19 stop() from broker to Subagents. End
20 } or {
21 foundMatches() from broker to initiator.
22 inputData(string) from broker to Subagents.
23 for agent:<Subagents,broker>{
24 choice at agent {
25 result(string) from agent to broker.End
26 } or {
27 someError() from agent to broker.End
28 }
29 }
30 } ;
31 choice at broker {
32 replyFromSubagents(string) from broker to initiator.End
33 } or {
34 failureBrokering() from broker to initiator.End
35 }}}}
the role set Subagents with the broker as their coordinator, line 1 of Figure 3. The interaction
starts with the initiator asking, by sending a message forward to the broker, to forward
its request to the subagents. We specified a simple string as the request, but more complex data
structures maybe exchanged. After this there is a choice made by the broker that may decide
to fulfil the request or to refuse it. So we have a choice, with leader the broker which branches,
starting at lines 4 and 7, begin with a message sent from the broker to the initiator. In
order to have the projection on the role set Subagents, whose participants will behave in a
diferent manner in the two branches, the broker must send them a diferent message in two
branches. Our projection use the merge operator of [
Conclusion
The work presented is a part of a larger research project, within the PRIN project
“T-Ladies”, [