Semantic Issues in the Verification of Agent Communication Languages.
This article examines the issue of developing semantics for agent communication languages. In particular, it considers the problem of giving a verifiable semantics for such languagesa semantics where conformance (or otherwise) to the semantics could be determined by an independent observer. These problems are precisely defined in an abstract formal framework. Using this framework, a number of example agent communication frameworks are defined. A discussion is then presented, of the various options open to designers of agent communication languages, with respect the problem of verifying conformance.
Introduction
One of the main reasons why multi-agent systems are currently a major
area of research and development activity is that they are seen as a key
enabling technology for the Internet-wide electronic commerce systems
that are widely predicted to emerge in the near future [20]. If this
vision of large-scale, open multi-agent systems is to be realised, then the
fundamental problem of inter-operability must be addressed. It must be
possible for agents built by dierent organisations using dierent hardware
and software platforms to safely communicate with one-another
via a common language with a universally agreed semantics.
The inter-operability requirement has led to the development of
several standardised agent communication languages (acls) [30, 19].
However, to gain acceptance, particularly for sensitive applications such
as electronic commerce, it must be possible to determine whether or not
any system that claims to conform to an acl standard actually does
so. We say that an acl standard is veriable if it enjoys this property.
Unfortunately, veriability has to date received little attention by the
standards community (although it has been recognised as an issue [19,
p46]). In this article, we establish a simple formal framework that allows
us to precisely dene what it means for an acl to be veriable. This
framework is dened in section 3, following a brief discussion of the
background to this work. We then formally dene what it means for an
acl to be veriable in section 4. The basic idea is to show how demonstrating
conformance to an acl semantics can be seen as a verication
problem in the standard software engineering sense [7]. Demonstrating
c
1999 Kluwer Academic Publishers. Printed in the Netherlands.
Michael Wooldridge
that a program semantically complies to a standard involves showing
that the program satises the specication given by the semantics. If
the semantics are logical, then demonstrating compliance thus reduces
to a proof problem. We discuss the practical implications of these definitions
in section 4.1. In section 5, we give examples of some acls,
and show that some of these are veriable, while others are not. In
section 6, we discuss an alternative approach to verication, in which
verication is done via model checking rather than proof. Finally, in
section 7, we discuss the implications of our results, with emphasis on
future directions for work on veriable acls.
2. Background
Current techniques for developing the semantics of acls trace their
origins to speech act theory. In this section, we give a brief overview of
this work.
2.1. Speech Acts
The theory of speech acts is generally recognised as having begun in the
work of the philosopher John Austin [4]. Austin noted that a certain
class of natural language utterances | hereafter referred to as speech
acts | had the characteristics of actions, in the sense that they change
the state of the world in a way analogous to physical actions. It may
seem strange to think of utterances changing the world in the way
that physical actions do. If we pick up a block from a table (to use
an overworked but traditional example), then the world has changed
in an obvious way. But how does speech change the world? Austin
gave as paradigm examples declaring war and saying \I now pronounce
man and wife". Stated in the appropriate circumstances, these
utterances clearly change the state of the world in a very tangible way 1 .
Austin identied a number of performative verbs, which correspond
to various dierent types of speech acts. Examples of such performative
verbs are request, inform, and promise. In addition, Austin distinguished
three dierent aspects of speech acts: the locutionary act, or
act of making an utterance (e.g., saying \Please make some tea"), the
illocutionary act, or action performed in saying something (e.g., \He
requested me to make some tea"), and perlocution, or eect of the act
(e.g., \He got me to make tea").
1 Notice that when referring to the eects of communication, we are ignoring
\pathological" cases, such as shouting while on a ski run and causing an avalanche.
Similarly, we will ignore \microscopic" eects (such as the minute changes in pressure
or temperature in a room caused by speaking).
Semantic Issues in Agent Communication 3
Austin referred to the conditions required for the successful completion
of performatives as felicity conditions. He recognized three important
felicity conditions:
1. a) There must be an accepted conventional procedure for the performative

b) The circumstances and persons must be as specied in the
procedure.
2. The procedure must be executed correctly and completely.
3. The act must be sincere, and any uptake required must be com-
pleted, insofar as is possible.
Austin's work was rened and considerably extended by Searle, in
his 1969 book Speech Acts [38]. Searle identied several properties that
must hold for a speech act performed between a hearer and a speaker
to succeed, including normal I/O conditions, preparatory conditions,
and sincerity conditions. For example, consider a request by speaker
to hearer to perform action:
1. Normal I/O conditions. Normal I/O conditions state that hearer
is able to hear the request, (thus must not be deaf, . ), the act
was performed in normal circumstances (not in a lm or play, . ),
etc.
2. Preparatory conditions. The preparatory conditions state what must
be true of the world in order that speaker correctly choose the
speech act. In this case, hearer must be able to perform action,
and speaker must believe that hearer is able to perform action.
Also, it must not be obvious that hearer will do action anyway.
3. Sincerity conditions. These conditions distinguish sincere performances
of the request; an insincere performance of the act might
occur if speaker did not really want action to be performed.
Searle also gave a ve-point typology of speech acts:
1. Representatives. A representative act commits the speaker to the
truth of an expressed proposition. The paradigm case is informing.
2. Directives. A directive is an attempt on the part of the speaker to
get the hearer to do something. Paradigm case: requesting.
3. Commissives. Commit the speaker to a course of action. Paradigm
case: promising.
4 Michael Wooldridge
4. Expressives. Express some psychological state (e.g., gratitude). Paradigm
case: thanking.
5. Declarations. Eect some changes in an institutional state of aairs.
Paradigm case: declaring war.
2.2. Speech Acts in Artificial Intelligence
In the late 1960s and early 1970s, a number of researchers in arti-
cial intelligence (ai) began to build systems that could plan how to
autonomously achieve goals [2]. Clearly, if such a system is required
to interact with humans or other autonomous agents, then such plans
must include speech actions. This introduced the question of how
the properties of speech acts could be represented such that planning
systems could reason about them. Cohen and Perrault [15] gave an
account of the semantics of speech acts by using techniques developed
in ai planning research [18]. The aim of their work was to develop a
theory of speech acts:
\[B]y modelling them in a planning system as operators dened
. in terms of speakers and hearers beliefs and goals. Thus speech
acts are treated in the same way as physical actions". [15]
The formalism chosen by Cohen and Perrault was the strips nota-
tion, in which the properties of an action are characterised via pre-and
post-conditions [18]. The idea is very similar to Hoare logic [24].
Cohen and Perrault demonstrated how the pre- and post-conditions of
speech acts such as request could be represented in a multi-modal logic
containing operators for describing the beliefs, abilities, and wants of
the participants in the speech act.
Consider the Request act. The aim of the Request act will be for a
speaker to get a hearer to perform some action. Figure 1 denes the
Request act. Two preconditions are stated: the \cando.pr" (can-do pre-
conditions), and \want.pr" (want pre-conditions). The cando.pr states
that for the successful completion of the Request , two conditions must
hold. First, the speaker must believe that the hearer of the Request
is able to perform the action. Second, the speaker must believe that
the hearer also believes it has the ability to perform the action. The
want.pr states that in order for the Request to be successful, the speaker
must also believe it actually wants the Request to be performed. If
the pre-conditions of the Request are fullled, then the Request will be
successful: the result (dened by the \eect" part of the denition) will
be that the hearer believes the speaker believes it wants some action
to be performed.
Semantic Issues in Agent Communication 5
Preconditions Cando.pr (S BELIEVE (H CANDO
Want.pr (S BELIEVE (S WANT requestInstance))
Effect (H BELIEVE (S BELIEVE (S WANT )))
Preconditions Cando.pr
Want.pr
Effect

Figure

1. Denitions from the Plan-Based Theory of Speech Acts
While the successful completion of the Request ensures that the
hearer is aware of the speaker's desires, it is not enough in itself to
guarantee that the desired action is actually performed. This is because
the denition of Request only models the illocutionary force of the
act. It says nothing of the perlocutionary force. What is required is a
mediating act. Table 1 gives a denition of CauseToWant , which is an
example of such an act. By this denition, an agent will come to believe
it wants to do something if it believes that another agent believes it
wants to do it. This denition could clearly be extended by adding more
pre-conditions, perhaps to do with beliefs about social relationships or
power structures.
Using these ideas, and borrowing a formalism for representing the
mental state of agents that was developed by Robert Moore [31], Douglas
Appelt was able to implement a system that was capable of planning
to perform speech acts [3].
2.3. Speech Acts as Rational Action
While the plan-based theory of speech acts was a major step forward,
it was recognised that a theory of speech acts should be rooted in
a more general theory of rational action. This observation led Cohen
and Levesque to develop a theory in which speech acts were modelled
as actions performed by rational agents in the furtherance of their
intentions [13]. The foundation upon which they built this model of
rational action was their theory of intention, described in [12]. The for-
6 Michael Wooldridge
mal theory is too complex to describe here, but as a
avour, here is the
Cohen-Levesque denition of requesting, paraphrased in English [13,
p241]:
A request is an attempt on the part of spkr , by doing e, to bring
about a state where, ideally, (i) addr intends , (relative to the
spkr still having that goal, and addr still being helpfully inclined to
spkr ), and (ii) addr actually eventually does , or at least brings
about a state where addr believes it is mutually believed that it
wants the ideal situation.
Actions in the Cohen-Levesque framework were modelled using techniques
adapted from dynamic logic [23].
2.4. Agent Communication Languages: KQML and FIPA
Throughout the 1980s and 1990s, interest in multi-agent systems developed
rapidly [6, 41]. An obvious problem in multi-agent systems
is how to get agents to communicate with one-another | the inter-operability
issue referred to in the introduction. To this end, in the early
1990s, the darpa Knowledge Sharing Eort (kse) began to develop
the Knowledge Query and Manipulation Language (kqml) and the
associated Knowledge Interchange Format (kif) as a common frame-work
via which multiple expert systems (cf. agents) could exchange
knowledge [33, 30].
kqml is essentially an \outer" language for messages: it denes a
simple lisp-like format for messages, and 41 performatives, or message
types, that dene the intended meaning of a message. Example kqml
performatives include ask-if and tell. The content of messages was
not considered part of the kqml standard, but kif was also dened,
to express such content. kif is essentially classical rst-order predicate
logic, recast in a lisp-like syntax.
To better understand the kqml language, consider the following
example [30, p354]:
(ask-one
:content (PRICE IBM ?price)
:receiver stock-server
:language LPROLOG
:ontology NYSE-TICKS
The intuitive interpretation of this message is that the sender is asking
about the price of ibm stock. The performative is ask-one, which an
agent will use to ask a question of another agent where exactly one reply
Semantic Issues in Agent Communication 7
is needed. The various other components of this message represent its
attributes. The most important of these is the :content eld, which
species the message content. In this case, the content simply asks for
the price of ibm shares. The :receiver attribute species the intended
recipient of the message, the :language attribute species that the
language in which the content is expressed is called LPROLOG (the recipient
is assumed to \understand" LPROLOG), and the nal :ontology
attribute denes the terminology used in the message.
Formal denitions of the syntax of kqml and kif were developed
by the kse, but kqml lacked any formal semantics until Labrou and
Finin's [26]. These semantics were presented using a pre- and post-condition
closely related to Cohen and Perrault's plan-based
theory of speech acts [15]. These pre- and post-conditions were specied
by Labrou and Finin using a logical language containing modalities
for belief, knowledge, wanting, and intending. However, Labrou and
Finin recognised that any commitment to a particular semantics for
this logic itself would be contentious, and so they refrained from giving
it a semantics. However, this rather begs the question of whether their
semantics are actually well-founded. We return to this issue later.
The take-up of kqml by the multi-agent systems community was
signicant. However, Cohen and Levesque (among others) criticized
kqml on a number of grounds [14], the most important of which being
that, the language was missing an entire class of performatives |
commissives, by which one agent makes a commitment to another. As
Cohen and Levesque point out, it is di-cult to see how many multi-agent
scenarios could be implemented without commissives, which appear
to be important if agents are to coordinate their actions with
one-another [25].
In 1995, the Foundation for Intelligent Physical Agents (fipa) began
its work on developing standards for agent systems. The centrepiece of
this initiative is the development of an acl [19] 2 . This acl is supercially
similar to kqml: it denes an \outer" language for messages,
it denes 20 performatives (such as inform) for dening the intended
interpretation of messages, and it does not mandate any specic language
for message content. In addition, the concrete syntax for fipa
acl messages closely resembles that of kqml. Here is an example of a
fipa acl message (from [19, p10]):
(inform
:sender agent1
simply refer to their acl as \acl", which can result in confusion when
discussing acls in general. To avoid ambiguity, we will always refer to \the fipa
acl".
8 Michael Wooldridge
:receiver agent2
:content (price good2 150)
:language sl
:ontology hpl-auction
Even a supercial glance conrms that the fipa acl is similar to kqml;
the relationship is discussed in [19, pp68{69].
The fipa acl has been given a formal semantics, in terms of a Semantic
Language (sl). The approach adopted for dening these semantics
draws heavily on [13], but in particular on Sadek's enhancements to
this work [9]. sl is a quantied multi-modal logic, which contains modal
operators for referring to the beliefs, desires, and uncertain beliefs of a-
gents, as well as a simple dynamic logic-style apparatus for representing
agent's actions. The semantics of the fipa acl map each acl message
to a formula of sl, which denes a constraint that the sender of the
message must satisfy if it is to be considered as conforming to the fipa
acl standard. fipa refer to this constraint as the feasibility condition.
The semantics also map each message to an sl-formula which denes
the rational eect of the action. The rational eect of a messages is its
purpose: what an agent will be attempting to achieve in sending the
message (cf. perlocutionary act). However, in a society of autonomous
agents, the rational eect of a message cannot (and should not) be
guaranteed. Hence conformance does not require the recipient of a
message to respect the rational eect part of the acl semantics |
only the feasibility condition.
To illustrate the fipa approach, we give an example of the semantics
of the fipa inform performative [19, p25]:
(1)
The B i is a modal connective for referring to the beliefs of agents (see
e.g., [21]); Bif is a modal connective that allows us to express whether
an agent has a denite opinion one way or the other about the truth
or falsity of its parameter; and U is a modal connective that allows us
to represent the fact that an agent is \uncertain" about its parameter.
Thus an agent i sending an inform message with content ' to agent j
will be respecting the semantics of the fipa acl if it believes ', and it
it not the case that it believes of j either that j believes whether ' is
true or false, or that j is uncertain of the truth or falsity of '.
fipa recognise that \demonstrating in an unambiguous way that a
given agent implementation is correct with respect to [the semantics]
Semantic Issues in Agent Communication 9
is not a problem which has been solved" [19, p46], and identify it as
an area of future work. (Checking that an implementation respects the
syntax of an acl like kqml or fipa is, of course, trivial.) If an agent
communication language such as fipa's acl is ever to be widely used
| particularly for such sensitive applications as electronic commerce
| then such conformance testing is obviously crucial. However, the
problem of conformance testing (verication) is not actually given a
concrete denition in [19], and no indication is given of how it might
be done. In short, the aim of the remainder of this article is to unambiguously
dene what it means for an agent communication language
such as that dened by fipa to be veriable, and then to investigate
the issues surrounding such verication.
3. Agent Communication Frameworks
In this section, we present an abstract framework that allows us to
precisely dene the veriable acl semantics problem. First, we will
assume that we have a set Ag ng of agent names | these are
the unique identiers of agents that will be sending messages to one
another in a system.
We shall assume that agents communicate using a communication
language L C . This acl may be kqml together with kif [26], it may be
the fipa-97 communication language [19], or some other proprietary
language. The exact nature of L C is not important for our purposes.
The only requirements that we place on L C are that it has a well-
dened syntax and a well-dened semantics. The syntax identies a
set w (L C ) of well-formed formulae of L C | syntactically acceptable
constructions of L C . Since we usually think of formulae of L C as being
messages, we use  (with annotations:  to stand for members
of w (L C ).
The semantics of L C are assumed to be dened in terms of a second
language L S , which we shall call the semantic language. The idea is that
if an agent sends a message, then the meaning of sending this message
is dened by a formula of L S . This formula denes what fipa [19,
p48] refer to as the feasibility pre-condition | essentially, a constraint
that the sender of the message must satisfy in order to be regarded
as being \sincere" in sending the message. For example, the feasibility
pre-condition for an inform act would typically state that the sender
of an inform must believe the content of the message, otherwise the
sender is not being sincere.
Michael Wooldridge
The idea of dening the semantics of one language in terms of another
might seem strange, but the technique is common in computer
science:
when Hoare-logic style semantics are given for programming lan-
guages, the semantics of a program written in, for example, pascal
or c are dened in terms of a second language | that of classical
rst-order logic [24];
an increasingly common approach to dening the semantics of
many programming languages is to give them a temporal seman-
tics, whereby the semantics of a program in a language such as c
or pascal are dened as a formula of temporal logic [28].
Note that in this article we are not concerned with the eects that
messages have on recipients. This is because although the \rational
eect" of a message on its recipient is the reason that the sender will
send a message (e.g., agent i informs agent j of ' because i wants j
to believe '), the sender can have no guarantee that the recipient will
even receive the message, still less that it will have the intended eect.
The key to our notion of semantics is therefore what properties must
hold of the sender of a message, in order that it can be considered to
be sincere in sending it.
Formally, the semantics of the acl L C are given by a function
which maps a single message  of L C to a single formula of L S ,
which represents the semantics of . Note that the \sincerity condition"
acts in eect like a specication (in the software
engineering sense), which must be satised by any agent that claims to
conform to the semantics. Verifying that an agent program conforms to
the semantics is thus a process of checking that the program satises
this specication.
To make the idea concrete, recall the fipa semantics of inform
messages, given in (1), above. In our framework, we can express the
fipa semantics as
It should be obvious how this corresponds to the fipa denition.
In order that the semantics of L C be well-dened, we must also
have a semantics for our semantic language L S itself. While there is
no reason in principle why we should not dene the semantics of L S in
terms of a further language L S 0 , (and so on), we assume without loss
Semantic Issues in Agent Communication 11
of generality that the semantics of L S are given with respect to a class
logical models for L S . More precisely, the semantics of L S
will be dened via a satisfaction relation \j= S ", where
By convention, if M 2 mod(L S ) and ' 2 w (L S ) then we write M
' to indicate that ('; M ) 2 then we read this as \'
is satised (or equivalently, is true) in M ". The meaning of a formula
' of L S is then the set of models in which ' is satised. We dene a
function
such that if ' 2 w (L S ), then is the set of models in which ' is
Agents are assumed to be implemented by programs, and we let
stand for the set of all such agent programs. For each agent i 2 Ag ,
we assume that  i 2  is the program that implements it. For our
purposes, the contents of  are not important | they may be java, c,
or c++ programs, for example. At any given moment, we assume that
a program  i may be in any of a set L i of local states. The local state
of a program is essentially just a snapshot of the agent's memory at
some instant in time. As an agent program  i executes, it will perform
operations (such as assignment statements) that modify its state. Let
i2Ag L i be the set of all local states. We use l (with annotations:
to stand for members of L.
One of the key activities of agent programs is communication: they
send and receive messages, which are formulae of the communication
language L C . We assume that we can identify when an agent emits
such a message, and write send( l ) to indicate the fact that agent
implemented by program  i 2 , sends a message  2 L C when
in state l 2 L i .
We now dene what we mean by the semantics of an agent program.
Intuitively, the idea is that when an agent program  i is in state l , we
must be able to characterise the properties of the program as a formula
of the semantic language L S . This formula is the theory of the program.
In theoretical computer science, the derivation of a program's theory is
the rst step to reasoning about its behaviour. In particular, a program
theory is the basis upon which we can verify that the program satises
its specication. Formally, a program semantics is a function that maps
a pair consisting of an agent program and a local state to a formula
Michael Wooldridge
Programs/state |   L
language | L Sn
Communication language | L C
Model structures for L S | mod(L S )1

Figure

2. The components of an agent communication framework.
L S of the semantic language. Note that the semantics of  must be
dened in terms of the same semantic language that was used to dene
the semantics of L C | otherwise there is no point of reference between
the two. Formally then, a semantics for agent program/state pairs is a
function
The relationships between the various formal components introduced
above are summarised in Figure 2. We now collect these various components
together and dene what we mean by an agent communication
framework.
DEFINITION 1. An agent communication framework is a (2n
tuple:
ng is a non-empty set of agents,  i 2  is an agent
program, L i is the set of local states of  i , L
communication language, L is a semantic language,
and is a semantics for .
We let F be the set of all such agent communication frameworks, and
use f (with annotations: f to stand for members of F .
Semantic Issues in Agent Communication 13
4. Veriability Dened
We are now in a position to dene what it means for an agent program,
in sending a message while in some particular state, to be respecting
the semantics of a communication framework. Recall that a communication
language semantics denes, for each message, a constraint, or
specication, which must be satised by the sender of the message if
it is to be considered as satisfying the semantics of the communication
language. The properties of a program when in some particular state
are given by the program semantics, This leads to the following
denition.
DEFINITION 2. Suppose
is an agent communication framework, and that send(
to respect the semantics
of framework f (written
Note that the problem could equivalently have been phrased in terms
of logical consequence: is an L S -logical consequence
of . If we had a sound and complete proof system ' S for L S ,
then we could similarly have phrased it as a proof problem:
. The rst approach, however, is probably the most
general.
Using this denition, we can dene what it means for a communication
framework to have a veriable semantics.
DEFINITION 3. An agent communication framework
is veriable i it is a decidable question whether
arbitrary  i , l , .
The intuition behind veriability is as follows: if an agent communication
framework enjoys this property, then we can determine whether
or not an agent is respecting the framework's communication language
semantics whenever it sends a message.
If a framework is veriable, then we know that it is possible in principle
to determine whether or not an agent is respecting the semantics
of the framework. But a framework that is veriable in principle is
not necessarily veriable in practice. This is the motivation behind the
following denition.
14 Michael Wooldridge
DEFINITION 4. An agent communication framework f 2 F is said to
be practically veriable i it is decidable whether
polynomial in jf j  jj  jj  jl j.
If we have a practically veriable framework, then we can do the
verication in polynomial time, which implies that we have at least
some hope of doing automatic verication using computers that we can
envisage today. Our ideal, when setting out an agent communication
should clearly be to construct f such that it is practically
veriable. However, practical veriability is quite a demanding proper-
ty, as we shall see in section 5. In the following subsection, we examine
the implications of these denitions.
4.1. What does it mean to be Verifiable?
If we had a veriable agent communication framework, what would it
look like? Let us take each of the components of such a framework in
turn. First, our set Ag of agents, implemented by programs  i , (where
these programs are written in an arbitrary programming language).
This is straightforward: we obviously have such components today.
Next, we need a communication language L C , with a well-dened syntax
and semantics, where the semantics are given in terms of L S , a semantic
language. Again, this is not problematic: we have such a language L C
in both kqml and the fipa-97 language. Taking the fipa case, the
semantic language is sl, a quantied multi-modal logic with equality.
This language in turn has a well dened syntax and semantics, and
so next, we must look for a program semantics . At this point, we
encounter problems.
Put simply, the fipa semantics are given in terms of mental states,
and since we do not understand how such states can be systematically
attributed to programs, we cannot verify that such programs respect
the semantics. More precisely, the semantics of sl are given in the
normal modal logic tradition of Kripke (possible worlds) semantics,
where each agent's \attitudes" (belief, desire, . ) are characterised as
relations holding between dierent states of aairs. Although Kripke
semantics are attractive from a mathematical perspective, it is important
to note that they are not connected in any principled way with
computational systems. That is, for any given
a java program), there is no known way of attributing to that program
an sl formula (or, equivalently, a set of sl models), which characterises
it in terms of beliefs, desires, and so on. Because of this, we say that sl
(and most similar logics with Kripke semantics) are ungrounded | they
have no concrete computational interpretation. In other words, if the
semantics of L S are ungrounded (as they are in the fipa-97 sl case),
Semantic Issues in Agent Communication 15
then we have no semantics for programs | and hence an unveriable
communication framework. Although work is going on to investigate
how arbitrary programs can be ascribed attitudes such as beliefs and
desires, the state of the art ([8]) is considerably behind what would be
required for acl verication. Other researchers have also recognised
this di-culty [39, 34].
Note that it is possible to choose a semantic language L S such
that a principled program semantics can be derived. For example,
temporal logic has long been used to dene the semantics of programming
languages [29]. A temporal semantics for a programming language
denes for every program a temporal logic formula characterising the
meaning of that program. Temporal logic, although ultimately based
on Kripke semantics, is rmly grounded in the histories traced out by
programs as they execute | though of course, standard temporal logic
makes no reference to attitudes such as belief and desire. Also note that
work in knowledge theory has shown how knowledge can be attributed
to computational processes in a systematic way [17]. However, this
work gives no indication of how attitudes such as desiring or intending
might be attributed to arbitrary programs. (We use techniques from
knowledge theory to show how a grounded semantics can be given to a
communication language in Example 2 of section 5.)
Another issue is the high computational complexity of the veri-
cation process itself [32]. Ultimately, determining whether an agent
implementation is respecting the semantics of a communication frame-work
reduces to a logical proof problem, and the complexity of such
problems is well-known. If the semantic language L S of a framework f
is equal in expressive power to rst-order logic, then f is of course not
veriable. For quantied multi-modal logics, (such as that used by fipa
to dene the semantics of their acl), the proof problem is often much
harder than this | proof methods for quantied multi-modal logics
are very much at the frontiers of theorem-proving research (cf. [1]). In
the short term, at least, this complexity issue is likely to be another
signicant obstacle in the way of acl verication.
To sum up, it is entirely possible to dene a communication language
LC with semantics in terms of a language L S . However, giving
a program semantics for a semantic language (such as that of fipa-97)
with ungrounded semantics is a serious unsolved problem.
5. Example Frameworks
To illustrate the idea of verication, as introduced above, in this section
we will consider a number of progressively richer agent communica-
Michael Wooldridge
tion frameworks. For each of these frameworks, we discuss the issue
of veriability, and where possible, characterise the complexity of the
verication problem.
5.1. Example 1: Classical Propositional Logic.
For our rst example, we dene a simple agent communication frame-work
f 1 in which agents communicate by exchanging formulae of classical
propositional logic. The intuitive semantics of sending a message
' is that the sender is informing other agents of the truth of '. An
agent sending out a message ' will be respecting the semantics of the
language if it \believes" (in a sense that we precisely dene below)
that ' is true. An agent will not be respecting the semantics if it
sends a message that it \believes" to be false. We also assume that
agent programs exhibit a simple behaviour of sending out all messages
that they believe to be true. We show that framework f 1 is veriable,
and that in fact every agent program in this framework respects the
semantics of f 1 .
Formally, we must dene the components of a framework
These components are as follows. First, Ag is some arbitrary non-empty
set | the contents are not signicant. Second, since agents communicate
by simply exchanging messages that are simply formulae of
classical propositional logic, L 0 , we have L . Thus the set w (L 0 )
contains formulae made up of the proposition symbols
combined into formulae using the classical connectives \:" (not), \^"
(and), \_" (or), and so on.
We let the semantic language L S also be classical propositional logic,
and dene the L C semantic function simply as the identity function:
. The semantic function
the usual propositional denotation function | the denition is entirely
standard, and so we omit it in the interests of brevity.
An agent i 's state l i is dened to be a set of formulae of propositional
logic, hence L is assumed to
simply implement the following rule:
In other words, an agent program  i sends a message  when in state l
i  is present in l . The semantics of agent programs are then dened
as follows:
Semantic Issues in Agent Communication 17
In other words, the meaning of a program in state l is just the conjunction
of formulae in l . The following theorem sums up the key properties
of this simple agent communication framework.
THEOREM 1.
1. Framework f 1 is veriable.
2. Every agent in f 1 does indeed respect the semantics of f 1 .
Proof. For (1), suppose that send(
g. Then  i is respecting the semantics for f 1 i
which by the f 1 denitions of reduces to
But this is equivalent to showing that  is an L 0 -logical consequence
of logical consequence is obviously a decidable
problem, we are done. For (2), we know from equation (2) that
l . Since  is clearly a logical consequence of l if
, we are done.
An obvious next question is whether f 1 is practically veriable, i.e.,
whether verication can be done in polynomial time. Here, observe that
verication reduces to a problem of determining logical consequence in
which reduces to a test for L 0 -validity, and hence in turn to L 0 -
unsatisability. Since the L 0 -satisability problem is well-known to be
np-complete, we can immediately conclude the following.
THEOREM 2. The f 1 verication problem is co-np-complete.
Note that co-np-complete problems are ostensibly harder than merely
np-complete problems, from which we can conclude that practical
verication of f 1 is highly unlikely to be possible 3 .
5.2. Example 2: Grounded Semantics for Propositional
Logic.
One could argue that Example 1 worked because we made the assumption
that agents explicitly maintain databases of L 0 formulae: checking
whether an agent was respecting the semantics in sending a message '
3 In fact, f 2 will be practically veriable if and only if which is regarded
as extremely unlikely [32].
Michael Wooldridge
amounted to determining whether ' was a logical consequence of this
database. This was a convenient, but, as the following example
trates, unnecessary assumption. For this example, we will again assume
that agents communicate by exchanging formulae of classical propositional
logic L 0 , but we make no assumptions about their programs or
internal state. We show that despite this, we can still obtain a veriable
semantics, because we can ground the semantics of the communication
language in the states of the program. There is an impartial, objective
procedure we can apply to obtain a declarative representation of the
\knowledge" implicit within an arbitrary program, in the form of Fagin-
Halpern-Moses-Vardi knowledge theory [17]. To check whether an agent
is respecting the semantics of the communication language, we simply
check whether the information in the message sent by the agent is a
logical consequence of the knowledge implicit within the agent's state,
which we obtain using the tools of knowledge theory.
In what follows, we assume all sets are nite. As in Example 1, we
set both the communication language L C and the semantic language
L S to be classical propositional logic L 0 . We require some additional
denitions (see [17, pp103{114] for more details). Let the set G of global
states of a system be dened by We use g (with
annotations: to stand for members of G . We assume that we
have a vocabulary primitive propositions to express
the properties of a system. In addition, we assume it is possible to
determine whether or not any primitive proposition p 2  is true of
a particular global state or not. We write g j= p to indicate that p is
true in state g . Next, we dene a relation  i  G  L i for each agent
Ag to capture the idea of indistinguishability. The idea is that if
an agent i is in state l 2 L i , then a global state
indistinguishable from the state l that i is currently in (written g  i l )
. Now, for any given agent program  i in local state l , we dene
the positive knowledge set of  i in l , (written ks to be the set of
propositions that are true in all global states that are indistinguishable
from l , and the negative knowledge set of  i in l , (written ks
to be the set of propositions that are false in all global states that are
indistinguishable from l . Formally,
ks
ks
Readers familiar with epistemic logic [17] will immediately recognise
that this construction is based on the denition of knowledge in distributed
systems. The idea is that if p 2 ks
ks given the information that i has available in
state l , p must necessarily be true (respectively, false). Thus ks
Semantic Issues in Agent Communication 19
represents the set of propositions that the agent i knows are true when
it is in state l ; and ks represents the set of propositions that i
knows are false when it is in state l .
The L C semantic function is dened to be the identity function
again, so For the program semantics, we dene
The formula thus encodes the knowledge that the program  i
has about the truth or falsity of propositions  when in state l . The L S
semantic function is assumed to be the standard L 0 semantic func-
tion, as in Example 1. An agent will thus be respecting the semantics
of the communication framework if it sends a message such that this
message is guaranteed to be true in all states indistinguishable from
the one the agent is currently in. This framework has the following
property.
THEOREM 3. Framework f 2 is veriable.
Proof. Suppose that send( arbitrary  i , , l . Then  i is
respecting the semantics for f 2 i
which by the f 2 denitions of reduces to
Computing G can be done in time O(jL 1      L n j); computing  i
can be done in time O(jL i j  jG j); and given G and  i , computing
ks ks can be done in time O(jj  jG j). Once given
ks ks (; l ), determining whether
reduces to the L 0 logical consequence problem
This problem is obviously decidable.
verication reduces to L 0 logical consequence checking, we can
use a similar argument to that used for Theorem 2 to show the problem
is in general no more complex than f 1 verication:
Michael Wooldridge
THEOREM 4. The f 2 verication problem is co-np-complete.
Note that the main point about this example is the way that the
semantics for programs were grounded in the states of programs. In
this example, the communication language was simple enough to make
the grounding easy. More complex communication languages with a
similarly grounded semantics are possible. We note in closing that
it is straightforward to extend framework f 2 to allow a much richer
agent communication language (including requesting, informing, and
commissives) [40].
5.3. Example 3: The fipa-97 acl.
For the nal example, consider a framework f 3 in which we use the
fipa-97 acl, and the semantics for this language dened in [19]. Following
the discussion in section 4.1, it should come as no surprise that
such a framework is not veriable. It is worth spelling out the reasons
for this. First, since the semantic language sl is a quantied multi-modal
logic, with greater expressive power than classical rst order
logic, it is clearly undecidable. (As we noted above, the complexity of
the decision problem for quantied modal logics is often much harder
than for classical predicate logic [1].) So the f 3 verication problem is
obviously undecidable. But of course the problem is worse than this,
since as the discussion in section 4.1 showed, we do not have any idea
of how to assign a program semantics for semantic languages like sl,
because these languages have an ungrounded, mentalistic semantics.
6. Verication via Model Checking
The problem of verifying whether an agent implements the semantics
of a communication language has thus far been presented as one of
determining logical consequence, or, equivalently, as a proof problem.
Readers familiar with verication from theoretical computer science
will recognise that this corresponds to the \traditional" approach to
verifying that a program satises a specication. Other considerations
aside, a signicant drawback to proof theoretic verication is the problem
of computational complexity. As we saw above, even if the semantic
language is as impoverished as classical propositional logic, verica-
tion will be co-np-complete. In reality, logics for verication must be
considerably more expressive than this.
Problems with the computational complexity of verication logics
led researchers in theoretical computer science to investigate other approaches
to formal verication. The most successful of these is model
Semantic Issues in Agent Communication 21
checking [27, 22, 10]. The idea behind model checking is as follows.
Recall that in proof theoretic verication, to verify that a program  i
has some property ' when in state l , we derive the theory of that
program and attempt to establish i.e., that property
' is a theorem of the theory In temporal semantics, for
example [28, 29], is a temporal logic formula such that the
models of this formula correspond to all possible runs of the program
In contrast, model checking approaches work as follows. To determine
whether or not  i has property ' when in state l , we proceed as
follows:
, and from them generate a model M  i ;l that encodes all
the possible computations of .
Determine whether or not M  i ;l whether the formula '
is valid in M  i ;l ; the program  i has property ' in state l just in
case the answer is \yes".
In order to encode all computations of the program, the model generated
in the rst stage will be a branching time temporal model [16].
Intuitively, each branch, (or path), through this model will correspond
to one possible execution of the program. Such a model can be generated
automatically from the text of a program in a typical imperative
programming language.
The main advantage of model checking over proof theoretic ver-
ication is in complexity: model checking using the branching time
temporal logic ctl [11] can be done in time O(j'j  jM j), where j'j is
the size of the formula to be checked, and jM j is the size of the model
(i.e., the number of states it contains) [16]. Model-checking approaches
have recently been used to verify nite-state systems with up to 10 120
states [10].
Using a model checking approach to conformance testing for acls,
we would dene the program semantics as a function
which assigns to every program/state pair an L S -model, which encodes
the properties of that program/state pair. Verifying that
would involve checking whether whether the
sincerity condition was valid in model
The comparative e-ciency of model checking is a powerful argument
in favour of the approach. Algorithms have been developed for
(propositional) belief-desire-intention logics that will take a model and
22 Michael Wooldridge
a formula and will e-ciently determine whether or not the formula is
satised in that model [35, 5]. These belief-desire-intention logics are
closely related to those used to give a semantics to the fipa-97 acl.
However, there are two unsolved problems with such an approach.
The rst problem is that of developing the program semantics
We have procedures that, given a program, will generate a branching
temporal model that encode all computations of that program. Howev-
er, these are not the same as models for belief-desire-intention logics.
Put simply, the problem is that we do not yet have any techniques for
systematically assigning beliefs, desires, intentions, and uncertainties
(as in the fipa-97 sl case [19]) to arbitrary programs. This is again
the problem of grounding that we referred to above. As a consequence,
we cannot do the rst stage of the model checking process for acls
that have (ungrounded) fipa-like semantics.
The second problem is that model checking approaches have been
shown to be useful for systems that can be represented as nite state
models using propositional temporal logics. If the verication logic allows
arbitrary quantication, (or the system to be veried is not nite
state), then a model checking approach is unlikely to be practicable.
To summarise, model checking approaches appear to have considerable
advantages over proof-theoretic approaches to verication with
respect to their much reduced computational complexity. However,
as with proof-theoretic approaches, the problem of ungrounded acl
semantics remains a major problem, with no apparent route of attack.
Also, the problem of model checking with quantied logics is an as-yet
untested area. Nevertheless, model checking seems a promising
direction for acl conformance testing.
7. Discussion
If agents are to be as widely deployed as some observers predict, then
the issue of inter-operation | in the form of standards for communication
languages | must be addressed. Moreover, the problem of
determining conformance to these standards must also be seriously
considered, for if there is no way of determining whether or not a system
that claims to conform to a standard does indeed conform to it, then the
value of the standard itself must be questioned. This article has given
the rst precise denition of what it means for an agent communication
framework to be veriable, and has identied some problematic issues
for veriable communication language semantics, the most important
of which being that:
Semantic Issues in Agent Communication 23
We must be able to characterise the properties of an agent program
as a formula of the language L S used to give a semantics
to the communication language. L S is often a multi-modal logic,
referring to (in the fipa-97 case, for example) the beliefs, desires,
and uncertainties of agents. We currently have very little idea
about systematic ways of attributing such mentalistic descriptions
to programs | the state of the art is considerably behind what
would be needed for anything like practical verication, and this
situation is not likely to change in the near future.
The computational complexity of logical verication, (particularly
using quantied multi-modal languages), is likely to prove a major
obstacle in the path of practical agent communication language
verication. Model checking approaches appear to be a promising
alternative.
In addition, the article has given examples of agent communication
frameworks, some of which are veriable by this denition, others of
which, (including the fipa-97 acl [19]), are not.
The results of this article could be interpreted as negative, in that
they imply that verication of conformance to acls using current techniques
is not likely to be possible. However, the article should emphatically
not be interpreted as suggesting that standards | particularly,
standardised acls | are unnecessary or a waste of time. If agent technology
is to achieve its much vaunted potential as a new paradigm for
software construction, then such standards are important. However, it
may well be that we need new ways of thinking about the semantics
and verication of such standards. A number of promising approaches
have recently appeared in the literature [39, 34, 40]. One approach
that can work eectively in certain cases is mechanism design [36].
The basic idea is that in certain multi-agent scenarios (auctions are a
well-known example), it is possible to design an interaction protocol
so that the dominant strategy for any participating agent is to tell
the truth. Vickrey's mechanism is probably the best-known example of
such a technique [37]. In application domains where such techniques are
feasible, they can be used to great eect. However, most current multi-agent
applications do not lend themselves to such techniques. While
there is therefore great potential for the application of mechanism design
in the long term, in the short term it is unlikely to play a major
role in agent communication standards.
Michael Wooldridge



--R


Readings in Planning.
Planning English Sentences.
How to Do Things With Words.

Readings in Distributed Arti
The Correctness Problem in Computer Science.









Reasoning About Knowledge.










The Temporal Logic of Reactive and Concurrent Systems.
Temporal Veri


Computational Complexity.



Rules of Encounter: Designing Conventions for Automated Negotiation among Computers.

Speech Acts: An Essay in the Philosophy of Language.



--TR

--CTR
Peter McBurney , Simon Parsons, Locutions for Argumentation in Agent Interaction Protocols, Proceedings of the Third International Joint Conference on Autonomous Agents and Multiagent Systems, p.1240-1241, July 19-23, 2004, New York, New York
Guido Boella , Rossana Damiano , Joris Hulstijn , Leendert van der Torre, Role-based semantics for agent communication: embedding of the 'mental attitudes' and 'social commitments' semantics, Proceedings of the fifth international joint conference on Autonomous agents and multiagent systems, May 08-12, 2006, Hakodate, Japan
Paurobally , Jim Cunningham , Nicholas R. Jennings, A formal framework for agent interaction semantics, Proceedings of the fourth international joint conference on Autonomous agents and multiagent systems, July 25-29, 2005, The Netherlands
Stefan Poslad , Patricia Charlton, Standardizing agent interoperability: the FIPA approach, Mutli-agents systems and applications, Springer-Verlag New York, Inc., New York, NY, 2001
Ulle Endriss , Nicolas Maudet, On the Communication Complexity of Multilateral Trading: Extended Report, Autonomous Agents and Multi-Agent Systems, v.11 n.1, p.91-107, July      2005
Peter McBurney , Simon Parsons, Posit spaces: a performative model of e-commerce, Proceedings of the second international joint conference on Autonomous agents and multiagent systems, July 14-18, 2003, Melbourne, Australia
Peter McBurney , Simon Parsons, A Denotational Semantics for Deliberation Dialogues, Proceedings of the Third International Joint Conference on Autonomous Agents and Multiagent Systems, p.86-93, July 19-23, 2004, New York, New York
Yuh-Jong Hu, Some thoughts on agent trust and delegation, Proceedings of the fifth international conference on Autonomous agents, p.489-496, May 2001, Montreal, Quebec, Canada
Peter McBurney , Simon Parsons , Michael Wooldridge, Desiderata for agent argumentation protocols, Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 1, July 15-19, 2002, Bologna, Italy
Peter McBurney , Simon Parsons, Games That Agents Play: A Formal Framework for Dialoguesbetween Autonomous Agents, Journal of Logic, Language and Information, v.11 n.3, p.315-334, Summer 2002
Rogier M. Van Eijk , Frank S. De Boer , Wiebe Van Der Hoek , John-Jules Ch. Meyer, A Verification Framework for Agent Communication, Autonomous Agents and Multi-Agent Systems, v.6 n.2, p.185-219, March
Peter Mcburney , Rogier M. Van Eijk , Simon Parsons , Leila Amgoud, A Dialogue Game Protocol for Agent Purchase Negotiations, Autonomous Agents and Multi-Agent Systems, v.7 n.3, p.235-273, November
Brahim Chaib-Draa , Marc-Andr Labrie , Mathieu Bergeron , Philippe Pasquier, DIAGAL: An Agent Communication Language Based on Dialogue Games and Sustained by Social Commitments, Autonomous Agents and Multi-Agent Systems, v.13 n.1, p.61-95, July      2006
N. Maudet , B. Chaib-Draa, Commitment-based and dialogue-game-based protocols: new trends in agent communication languages, The Knowledge Engineering Review, v.17 n.2, p.157-179, June 2002
semantics;conformance testing;verification;agent communication languages;standards