Woolridge - Reasnoning About Rational Agents
Woolridge - Reasnoning About Rational Agents
Woolridge - Reasnoning About Rational Agents
Michael Wooldridge
All rights reserved. No part of this book may be reproduced in any form by any electronic
or mechanical means (including photocopying, recording, or information storage and retrieval)
without permission in writing from the publisher.
This book was set in Times Roman by the author using the IHEX document preparation system
and printed and bound in the United States of America.
Preface IX
Acknowledgments Xlll
1 Rational Agents
3 Introduction to £ORA 47
4 £ORA Defined 69
7 Communication 125
8 Cooperation 147
Appendix A:
Summary of Notation 179
Appendix B:
Formal Foundations 18 1
References 205
Index 223
Preface
This book is about a certain class of computer systems that are known as
agents, and more specifically, rational agents. We call these computer systems
agents because they are capable of independent, autonomous action in order
to meet their design objectives: put crudely, they are capable of deciding for
themselves what to do in any given situation. We call them rational agents
because they make good decisions about what to do.
Engineering rational agents may at first sight appear to be a somewhat
abstract, even fanciful endeavor, divorced from the everyday reality of com
puter science and software engineering. This is not the case. Rational agents
are finding a wide range of applications. A famous example is NASA's Deep
Space 1 (OS 1) mission. Launched from Cape Canaveral on 24 October 1998,
OS 1 was the first space probe to have an autonomous, agent-based control sys
tem [ 165]. Before osl, space missions required a ground crew of up to 3 00
staff to continually monitor progress. This ground crew made all necessary
control decisions on behalf of the probe, and painstakingly transmitted these
decisions to the probe for subsequent execution. Given the length of typical
planetary exploration missions, such a procedure was expensive and, if the de
cisions were ever required quickly, it was simply not practical. The autonomous
control system in os 1 was capable of making many important decisions itself.
This made the mission more robust, particularly against sudden unexpected
problems, and also had the very desirable side effect of reducing overall mis
sion costs. The os 1 example may seem somewhat extreme: after all, spacecraft
control systems are hardly an everyday software engineering problem. But the
same technology is finding applications in much more commonplace domains.
For example, such agents are increasingly being used for Internet-based elec
tronic commerce applications, where they autonomously buy and sell goods
on behalf of a user [ 168].
As it turns out, for all but the simplest of applications, it is very diffi
cult to build computer systems that can autonomously make good decisions
about what to do. For sure, there are a number of very powerful mathemati
cal frameworks available, which can help us to understand and analyze many
decision-making scenarios. Decision theory is an obvious example. Decision
theory tells us that a rational agent is one that chooses an action which maxi
mizes expected utility, where expected utility is defined in terms of the actions
available to the agent, the probability of certain outcomes, and the preferences
the agent has with respect to these outcomes. In multiagent scenarios, where
an agent is required to interact with other agents, game theory has proved to
be a powerful predictive and analytic tool. However, valuable and important
x Preface
though tools such as decision theory and game theory are, they give us few
clues with respect to implementing rational agents.
This book focuses on a model of rational decision making as practical
reasoning, of the kind that humans engage in every day. The model is called
the belief-desire-intention (8DI) model, because it acknowledges the primacy
of beliefs, desires, and, crucially, intentions, in the practical reasoning process.
The 8DI model is particularly interesting because it combines three distinct
components:
• A philosophical component.
The 8DI model is based on a widely respected theory of rational action in
humans, developed by the philosopher Michael Bratman [20].
• A logical component.
The third component of the 8DI model is a family of logics. These logics
capture the key aspects of the 8DI model as a set of logical axioms. There
are many candidates for a formal theory of rational agency, but 8DI logics in
various forms have proved to be among the most useful, longest-lived, and
widely accepted.
CORA, the formal framework that will be used throughout the remainder of
the book. CORA - which stands for "Cogic Of Rational Agents" - is a 8DI
logic, which extends Rao and Georgeff's original formalism. CORA allows
us to represent and reason about the beliefs, desires, intentions, and actions of
agents within a system, and how these beliefs, desires, intentions, and actions
change over time.
Once the basic logical framework is introduced, the remainder of the book
is taken up largely with an investigation of how it can be used to capture a range
of important aspects of rational agency. These aspects can be divided into those
that relate to individual agents and those that relate to multiple agents. With
respect to individual agents, I show how CORA can be used to capture many
of our intuitions about the relationships among beliefs, desires, and intentions,
as well as other concepts such as ability. The major contribution of the book
comes from the focus on multiagent aspects. Specifically, I show how CORA
can be used to capture:
There is some tension between the desire to write a book that is rigorous from
the perspective of mathematical logic, and the desire to write a book that is
readable. Logical rigor all too often seems to preclude readability: the level of
detail required to pass muster with logicians can be daunting to the uninitiated.
In the event, I have done my best to compromise. Thus, as well as giving formal
definitions and complete proofs of all results, I have tried wherever possible
to explain at length the intuition behind the formalism, and to give extensive
pointers to further reading. Those sections that contain a significant proportion
of abstract mathematical material are separated out from the main text, and
indicated in the relevant section header by means of an asterisk ("*").
8DI is probably the most-implemented framework for building rational
agents. I hope that after reading this book, you will understand why so many
researchers believe it represents a powerful framework through which to un
derstand, implement, and reason about rational agency.
Acknowledgments
Michael Wooldridge
Liverpool, Spring 2000
Reasoning about Rational Agents
1 Rational Agents
AGENT
action
output
ENVIRONMENT
Figure 1.1
Agents and their environments. The agent takes sensory input from the environment, and
produces as output actions that affect it.
Note that in almost all realistic applications, agents have at best partial
control over their environment. Thus, while they can perform actions that
change their environment, they cannot in general completely control it. It
therefore makes sense to divide the environment, conceptually at least, into
those parts that the agent controls, those parts it partially controls, and those
parts over which it has no control. (If we regard an agent's internal state as
being part of the environment, then this would be controlled by the agent.)
Apart from being situated in an environment, what other properties do we
expect a rational agent to have? Wooldridge and Jennings [249] argue that
agents should have the following properties:
• autonomy;
• proactiveness;
• reactivity; and
• social ability.
At its simplest, autonomy means nothing more than being able to operate in
dependently. Thus, at the very least, an autonomous agent makes independent
decisions - its decisions (and hence its actions) are under its own control,
and are not driven by others. Autonomous agents are therefore the loci of de
cision making. However, autonomy is usually taken to have a slightly stronger
meaning than this. We generally assume that an autonomous agent is one that
has its own beliefs, desires, and intentions, which are not subservient to those
4 Chapter 1
of other agents. This is not to say that these beliefs, desires, and intentions are
necessarily represented within an agent - the point is that we regard a rational
agent as "having its own agenda," which may or may not concur with that of
other agents.
Proactiveness means being able to exhibit goal-directed behavior. If an
agent has a particular goal or intention, then we expect the agent to try to
achieve this intention. For example, if I have an intention to write a book,
then it is rational of me to actually act towards this intention, by eventually
putting pen to paper. Moreover, proactiveness means exploiting serendipity.
For example, if I have a desire to become rich, and an opportunity to make a
fortune arises, then it is only rational of me to try to exploit this opportunity,
perhaps by generating a new goal. Proactiveness rules out entirely passive
agents, who never try to do anything.
Being reactive means being responsive to changes in the environment.
As I noted above, in everyday life, our plans rarely run smoothly. They are
frequently thwarted, both by the vagaries of nature and by other agents fouling
them up. W hen we become aware that our plans have gone awry, we do not
ignore this fact. We respond, by choosing an alternative course of action.
Responses may be of the "stimulus ---+ response" style, or they may involve
further deliberation. For example, if I am driving my car and I realize I am
about to crash into something, I will swerve to avoid it. It is unlikely that this
kind of response involves much deliberation on my part; the behavior seems
to be "hardwired." In contrast, if! am traveling to Heathrow Airport for a 9.30
AM flight, and I discover that the train I was about to catch is not running, I
will actively deliberate in order to fix upon a course of action that will still
enable me to catch my flight. This deliberation typically involves at least some
reasoning about the alternatives available (catching a taxi or bus, for example).
Crucially, however, I fix upon an alternative sufficiently quickly that it will
deliver me to the airport in time - I will not deliberate for so long that it
becomes impossible to catch the flight.
Designing a purely reactive system, which simply responds to environ
mental stimuli, is not hard. We can implement such a system as a lookup table,
which simply maps environment states directly to actions. Similarly, devel
oping a purely goal-driven system is not hard. (After all, this is ultimately
what conventional computer programs are.) However, implementing a system
that achieves an effective balance between goal-directed and reactive behavior
turns out to be very hard. We elaborate on this problem in the next chapter.
Rational Agents 5
Finally, let us say something about social ability. In one sense, social
ability is trivial. After all, every day, millions of computers across the world
routinely exchange information with both humans and other computers. But
the ability to exchange bit streams is not really social ability. Consider that,
in the human world, comparatively few of our goals can be achieved without
interaction with other people and organizations, who cannot be assumed to
share our goals. These agents are themselves autonomous, with their own
agendas to pursue. To achieve our goals in such situations, we must negotiate
and cooperate with these agents. We may be required to understand and reason
about their beliefs and goals, and to perform actions (such as paying them
money) that we would not otherwise choose to perform, in order to get them
to cooperate with us, and achieve our goals. This type of social ability -
the ability to interact (through negotiation and cooperation) with other self
interested agents - is much more complex and much less understood than
simply the ability to exchange bit streams. In the later chapters of this book, I
focus on such interactions in detail.
1 There are at least three current usages of the term "reactive system" in computer science. The
6 Chapter 1
Reactive systems are systems that cannot adequately be described by the relational or
functional view. The relational view regards programs as functions ... from an initial
state to a terminal state. Typically, the main role of reactive systems is to maintain an
interaction with their environment, and therefore must be described (and specified) in
terms of their on-going behavior ... [E]very concurrent system ... must be studied by
behavioral means. This is because each individual module in a concurrent system is a
reactive subsystem, interacting with its own environment which consists of the other
modules. [ 177]
first, oldest usage is that by Pnueli and followers (see, e. g., [177], and the description above).
Second, researchers in AI planning take a reactive system to be one that is capable of responding
rapidly to changes in its environment - here the word "reactive" is taken to be synonymous
with "responsive" (see, e. g., [l12]). More recently, the term has been used to denote systems that
respond directly to their environment, rather than reason explicitly about it (see, e. g., [40]). I use
the adjective "Pnuelian" when referring to reactive systems in the sense that Pnueli describes.
Rational Agents 7
The 8DI theory of human rational action was originally developed by Michael
Bratman [20]. It is a theory of practical reasoning - the process of reasoning
that we all go through in our everyday lives, deciding moment by moment
which action to perform next. Bratman's theory focuses in particular on the
role that intentions play in practical reasoning. Bratman argues that intentions
are important because they constrain the reasoning an agent is required to do in
order to select an action to perform. For example, suppose I have an intention
to write a book. Then while deciding what to do, I need not expend any effort
considering actions that are incompatible with this intention (such as having
a summer holiday, or enjoying a social life). This reduction in the number
of possibilities I have to consider makes my decision making considerably
simpler than would otherwise be the case. Since any real agent we might care to
consider - and in particular, any agent that we can implement on a computer
- must have resource bounds, an intention-based model of agency, which
8 Chapter 1
2 In this description of the PRS, I have modified the original terminology somewhat, to be more
in line with contemporary usage; I have also simplified the control cycle of the PRS slightly.
Rational Agents 9
Here, (Int i <p) is a construction that means "agent i intends <p." It is not hard
to guess that (Bel i <p) means "agent i believes <p." A "complete" theory of
rational agency would be comprised of a number of formula schemas such as
(1.1), which would together axiomatize the properties of rational agency.
Unfortunately, giving anything like a complete account of the relationships
between an agent's mental states is extremely difficult. Part of the problem
is that the objects of study - beliefs, desires, and the like - are rather
different to phenomena that we observe in the physical world. In attempting
to develop formal theories of such notions, we are forced to rely very much on
our intuitions about them. As a consequence, such theories are hard to validate
(or invalidate) in the way that good scientific theories should be. Fortunately,
we have powerful tools available to help in our investigation. Mathematical
logic allows us to represent our theories in a transparent, readable form, and
examine (through the medium of formal proof) the predictions that our theories
make, in order to see whether or not their consequences make sense.
.cORA stands for ".cogic Of Rational Agents." .cORA is a 8DI logic:
originally developed by Anand Rao and Michael Georgeff [187, 186, 188,
189, 184, 185], 8DI logics allow us to represent the beliefs, desires, and
intentions of agents. In addition to the 8DI component, .cORA contains a
temporal component, which allows us to represent the dynamics of agents and
their environments - how they change over time. Finally, .cORA contains
an action component, which allows us to represent the actions that agents
10 Chapter 1
Certain questions are frequently asked about the work presented in this book,
and so it seems only appropriate that I should include a FAQ.
A rational agent is then one that chooses to perform an action a that maximizes
EU( ...). It is straightforward to define the behavior of such an agent. Let
the function !apt take as input a set of possible actions, a set of outcomes,
a probability distribution over possible outcomes given the performance of
actions, and a utility function, and let this function return an action. Then we
can define the desired behavior of !apt as follows.
!opt(Ac,n,p, U) = argmax
aEAc
L U(w)P(w I a) (1.3)
wEO
As Russell and Norvig point out, equations (1.2) and (1.3) could be seen in one
sense as defining the whole of artificial intelligence [198, pA72]. It seems that
in order to build a rational agent, all we need to do is implement the function
!opt.But while decision theory is a normative theory of rational action (it tells us
what an agent should in principle do) it has nothing to say about how we might
efficiently implement the function!opt. The problem is that!apt seems to require
Rational Agents 11
an unconstrained search over the space of all actions and their outcomes. Such
a search is prohibitively expensive, particularly in the case where an agent
needs to consider sequences of actions (i.e., plans).
Another problem is that it is hard in practice to obtain the probability
distribution P or utility function U. If we consider a domain defined by m
attributes, each of which may take n values, then the set n will contain
n
m different outcomes. Simply enumerating these outcomes is likely to be
impractical in many circumstances. Even if it is possible to enumerate the
outcomes, actually obtaining the required probabilities and utilities for them
is notoriously hard [198, pp.475--480]. See the "Notes and Further Reading"
section at the end of this chapter for references to how decision theory is
currently being used in artificial intelligence.
Why Logic?
There are some in the AI research community who believe that logic is (to put
it crudely) the work of the devil, and that the effort devoted to such problems
as logical knowledge representation and theorem proving over the years has
been, at best, a waste of time. At least a brief justification for the use of logic
therefore seems necessary.
12 Chapter 1
Finally, by adopting a logic-based approach, one makes available all the results
and techniques of what is arguably the oldest, richest, most fundamental, and
best-established branch of mathematics.
The final chapter in the main text of this book, chapter 9, considers in detail
the role of logic in the theory and practice of multiagent systems.
Those active in the area of logic for AI can be divided broadly into two
camps: those who make use of classical (usually first-order) logic, and those
who use non-classical logics (in particular, modal and temporal logics of the
kind used in this book) of some sort. This book makes use of a logic called
.cORA. From a technical point of view, .cORA is a first-order branching time
logic, containing modal connectives for representing the beliefs, desires, and
intentions of agents, as well as a dynamic logic-style apparatus for representing
and reasoning about the actions that agents perform.
Strong opinions are held in both camps on the relative merits of classical
versus non-classical logics. Those in favor of classical logic point to a number
of general arguments against modal logics:
propositional case [91]. This makes it doubtful that there will ever be practical
theorem-proving methods for such logics.
There is certainly some strength to the first argument. With sufficient ingenuity,
one can use first-order logic to encode anything that can be encoded using
a modal or temporal logic. In this sense, first-order logic is a truly generic
formalism. But this argument misses the point slightly. To see what I mean,
consider the following English-language statement.
3 If at this point you do not buy into the argument that (1.6) is more user-friendly than (1.5), then
you are not going to enjoy the rest of this book.
14 Chapter 1
will see how an agent's beliefs, desires, and intentions can also be understood
as relational structures.
With respect to the issue of theorem proving, it should be noted that first
order logic hardly lends itself to efficient theorem proving. After all, even for
propositional logic the satisfiability problem is Np-complete. Nobody would
argue that theorem proving for modal and temporal logics is computationally
easy. But with time, we will perhaps come to gain a much better understanding
of how to build theorem provers for such logics - just as we have with first
order logic.
For the purposes of this book, logic is a means to an end and not an end in
itself. In other words, this book is first and foremost about rational agents
and multiagent systems. It is not intended to be a book about logic. So,
although the book contains many formal results, comparatively few of these
are specifically about logic itself. There are no complexity or completeness
results, for example, and no results on the expressive power of the logic used.
Although the book is not primarily about logic, I have nevertheless attempted
to ensure that it is "respectable" from a logical standpoint. 4 Thus the syntax
and semantics of CORA are defined in as much detail as all but the most
fastidious would expect, and detailed proofs are given for all results.
Logics like CORA, which combine multiple modalities into a single
framework, are very much at the cutting edge of contemporary logic re
search [139]. I therefore hope that this book will provide a fertile source of
ideas and problems for researchers more interested in pure logic than its appli
cations to agent theory.
If you open a page of this book at random, there is a good chance that you will
be confronted with logical notation of some kind. If you are not familiar with
logic or comfortable with discrete mathematics, then this formalism will no
doubt be off-putting. In fact, the "entry level" for reading this book is actually
quite low. I do not presuppose anything more than some familiarity with basic
discrete math notation (sets, functions, and relations) and the ability to read
formulae of first-order logic. Almost all undergraduate courses in computer
4 A colleague who read a draft of this book quipped that no book about logic in AI could be
respectable these days. If you are inclined to agree, you should probably stop reading now.
Rational Agents 15
science will cover these prerequisites. If you have such a background, then
you should be able to read the book and gain an understanding of the main
ideas without delving into the formal details. Ultimately, all you need to know
to understand most of the book is how to read formulae of CORA. Chapter 3
explains how to read formulae of CORA without going into the details of the
logic at all. If you prefer not to read the mathematically oriented sections of
the book, then you should avoid chapter 4 completely, and all sections marked
with an asterisk ("*" ) in the section header. The appendices survey the logical
preliminaries required to understand the book.
I do not enjoy reading proofs, or indeed writing them, but they are "a necessary
evil" in the words of my editor at MIT Press. If you feel the same as I feel,
then my advice is as follows. If you simply want to become familiar with the
techniques used and the results in the book, then there is no reason to read any
of the proofs at all. However, if you want to use CORA yourself, to build on
any of the results presented in this book, or to gain a really deep understanding
of the book, then you will simply have to bite the bullet. In fact, most of
the proofs rely on a relatively small set of techniques, which will already be
familiar to readers with a grounding in modal, temporal, and first-order logic.
CORA is not an executable logic, and there is currently no simple way of au
tomating CORA so that it can be used directly as a knowledge representation
formalism or a programming language. The possible roles that logics such as
CORA might play in the engineering of agent systems are explored in detail
in chapter 9.
The remainder of this book can be broadly divided into three parts:
• The first part (chapters 2 and 3) is background material. This part sets the
scene, by introducing the basic concepts and formalism used throughout the
book.
• The second part (chapters 4 and 5) develops the formal model that is used
throughout the book, and shows how this framework can be used to capture
some properties of individual rational agents.
• The third part (chapters 6, 7, and 8) shows how agents can be used to capture
In more detail:
This chapter is intended for readers who do not have a strong background
in logic. After this chapter, readers should be able to understand formulae of
.cORA.
• Chapter 4 (".cORA Defined") gives a complete definition of the syntax
and semantics of .cORA, and investigates some of its properties. This chapter
presupposes some familiarity with quantified modal, temporal, and dynamic
logics, but is otherwise entirely self-contained.
• Chapter 5 ("Properties of Rational Agents") investigates how .cORA can
individual agents to groups of agents. It shows how .cORA can be used to for
malize collective mental states such as mutual beliefs, desires, and intentions,
Rational Agents 17
spective. It discusses the role that logical theories of agency can or should
play in the development of agent systems. Adopting a software engineering
perspective, where such theories are treated as specifications that an idealized
agent would satisfy, it investigates the extent to which they can be used in the
implementation or verification of practical agent systems.
• Appendix A contains a summary of the notation used in the main text of the
book.
• Appendix B contains a short, self-contained introduction to modal and
There are now many introductions to intelligent agents and multiagent sys
tems. Ferber [56] is an undergraduate textbook, although as its name suggests,
this volume focussed on multiagent aspects rather than on the theory and prac
tice of individual agents. A first-rate collection of articles introducing agent
18 Chapter 1
The 8DI model has its roots in the philosophical tradition of understanding
practical reasoning in humans. Put simply, practical reasoning is reasoning
directed towards actions - the process of figuring out what to do:
of deciding which career to aim for is deliberation. Once one has fixed upon a
career, there are further choices to be made; in particular, how to bring about
this career. Suppose that after deliberation, you choose to pursue a career as an
academic. The next step is to decide how to achieve this state of affairs. This
process is means-ends reasoning. The end result of means-ends reasoning is a
plan or recipe of some kind for achieving the chosen state of affairs. For the
career example, a plan might involve first applying to an appropriate university
for a Ph.D. place, and so on. After obtaining a plan, an agent will typically then
attempt to carry out (or execute) the plan, in order to bring about the chosen
state of affairs. If all goes well (the plan is sound, and the agent's environment
cooperates sufficiently), then after the plan has been executed, the chosen state
of affairs will be achieved.
Thus described, practical reasoning seems a straightforward process, and
in an ideal world, it would be. But there are several complications. The first is
that deliberation and means-ends reasoning are computational processes. In all
real agents (and in particular, artificial agents), such computational processes
will take place under resource bounds. By this I mean that an agent will only
have a fixed amount of memory and a fixed processor available to carry out
its computations. Together, these resource bounds impose a limit on the size
of computations that can be carried out in any given amount of time. No real
agent will be able to carry out arbitrarily large computations in a finite amount
of time. Since almost any real environment will also operate in the presence
of time constraints of some kind, this means that means-ends reasoning and
deliberation must be carried out in a fixed, finite number of processor cycles,
with a fixed, finite amount of memory space. From this discussion, we can see
that resource bounds have two important implications:
We refer to the states of affairs that an agent has chosen and committed to
as its intentions. The BDI model of agency is ultimately one that recognizes
the primacy of intentions in practical reasoning, and it is therefore worth
discussing the roles that they play in more detail.
From this discussion, we can identify the following closely related situa
tions:
• Having an intention to bring about <p, while believing that you will not
bring about <p is called intention-belief inconsistency, and is not rational (see,
e.g., [20, pp.37-38]).
• Having an intention to achieve <p without believing that <p will be the case
The distinction between these two cases is known as the asymmetry thesis [20,
pp.37--4 1].
Summarizing, we can see that intentions play the following important roles
in practical reasoning:
Notice from this discussion that intentions interact with an agent's beliefs and
other mental states. For example, having an intention to <p implies that I do not
believe <p is impossible, and moreover that I believe given the right circum
stances, <p will be achieved. However, satisfactorily capturing the interaction
between intention and belief tums out to be surprisingly hard: the way in which
intentions interact with other mental states is considered in chapter 5.
26 Chapter 2
Figure 2.1
A basic agent controi ioop.
Based on the discussion above, let us consider how we might go about building
a BDI agent. The strategy I use is to introduce progressively more complex
agent designs, and for each of these designs, to investigate the type of behavior
that such an agent would exhibit, compared to the desired behavior of a rational
agent as discussed above. This then motivates the introduction of a refined
agent design, and so on.
The first agent design is shown in Figure 2. 1. The agent continually exe
cutes a cycle of observing the world, deciding what intention to achieve next,
determining a plan of some kind to achieve this intention, and then executing
this plan.
The first point to note about this loop is that we will not be concerned with
stages ( 2) or (3). Observing the world and updating an internal model of it are
important processes, worthy of study in their own right; but they lie outside the
scope of this volume. Instead, we are concerned primarily with stages (4) to (6).
Readers interested in understanding the processes of observing and updating
can find some key references in the "further reading" section at the end of this
chapter.
One of the most important issues raised by this simple agent control loop
follows from the fact that the deliberation and means-ends reasoning processes
are not instantaneous. They have a time cost associated with them. Suppose
that the agent starts deliberating at time to, begins means-ends reasoning at t1,
and subsequently begins executing the newly formed plan at time t2. The time
taken to deliberate is thus
tdeliberate = t1 - to
The Belief-Desire-Intention Model 27
Further suppose that the deliberation process is optimal in the sense that if it
selects some intention to achieve, then the achievement of this intention at time
to would be the best thing for the agent. So at time t1, the agent has selected an
intention to achieve that would have been optimal if it had been achieved at to.
But unless tdeliberate is vanishingly small, then the agent runs the risk that the
intention selected is no longer optimal by the time the agent has fixed upon it.
Of course, selecting an intention to achieve is only part of the overall
practical reasoning problem; the agent still has to determine how to achieve
the intention, via means-ends reasoning.
As with deliberation, assume that the means-ends reasoning process enjoys
optimality in the sense that if it is given an intention to achieve and it starts
executing at time t1, then it will select the course of action to achieve this
intention such that this course of action would be optimal if executed at time t1.
Again, means-ends reasoning is not instantaneous: it takes time to find the best
course of action to achieve the intention. How long exactly might it take to find
the best action? Suppose the agent has n possible actions available to it at any
given time. Then there are n! possible sequences of these actions. Since n! has
exponential growth, this means that the most obvious technique for finding a
course of action (systematically searching through the space of possible action
sequences) will be impossible in practice for all but the most trivial n. The
problem is exacerbated by the fact that the plan is developed on the basis of an
observation made of the environment at time to. The environment may be very
different by time t2.
Assuming we have an agent with optimal deliberation and means-ends
reasoning components, in the sense described above, it should be clear that
this agent will have overall optimal behavior in the following circumstances:
time at which the agent has found a course of action to achieve the intention).
planning are a major research topic in their own right - see [2] for a detailed
survey. For our purposes, a simple model of plans will suffice. A plan is viewed
as a tuple consisting of:
We will use 7r (with decorations: 7r', 7rl, ...) to denote plans, and let Plan be
the set of all plans (over some set of actions Ac). We will make use of a number
of auxiliary definitions for manipulating plans (some of these will not actually
be required until later in this chapter):
• if 7r is a plan, then we write pre(7r) to denote the pre-condition of 7r, post( 7r)
to denote the post-condition of 7r, and body(7r) to denote the body of 7r;
• if 7r is plan, then we write empty(7r) to mean that plan 7r is the empty
the plan body of 7r; for example, if the body of 7r is al, ... , an, then the body
of hd(7r) contains only the action al;
• if 7r is a plan then by tail(7r) we mean the plan made up of all but the first
action in the plan body of 7r; for example, if the body of 7r is al, a2, ... , an,
then the body oftail(7r) contains actions a2, ... , an;
• if 7r is a plan, I � Int is a set of intentions, and B � Bel is a set of beliefs,
We can now define the components of an agent's control loop. An agent's belief
update process is formally modeled as a belief revision function. Such a belief
30 Chapter 2
In other words, on the basis of the current beliefs and current percept, the belief
revision function determines a new set of beliefs. (As noted above, in this book
we are not concerned with how belief revision might work; see [71].)
The agent's deliberation process is given by a function
which takes a set of beliefs and returns a set of intentions - those selected by
the agent to achieve, on the basis of its beliefs.
An agent's means-ends reasoning is represented by a function
which on the basis of an agent's current beliefs and current intentions, deter
mines a plan to achieve the intention. Note that there is nothing in the definition
of the plan(. . . ) function which requires an agent to engage in plan generation
- constructing a plan from scratch [2]. In most BDI systems, the plan( . . . )
function is implemented by giving the agent a plan library [78]. A plan li
brary is a pre-assembled collection of plans, which an agent designer gives to
an agent. Finding a plan to achieve an intention then simply involves a sin
gle pass through the plan library to find a plan that, when executed, will have
the intention as a post-condition, and will be sound given the agent's current
beliefs. In implemented BDI agents, pre- and post-conditions are often rep
resented as (lists of) atoms of first-order logic, and beliefs and intentions as
ground atoms of first-order logic. Finding a plan to achieve an intention then
reduces to finding a plan whose pre-condition unifies with the agent's beliefs,
and whose post-condition unifies with the intention.
The agent control loop is now as shown in Figure 2. 2. This algorithm high
lights some limitations of this simple approach to agent control. In particu
lar, steps (4) to (7) inclusive implicitly assume that the environment has not
changed since it was observed at stage (3). Assuming that the time taken to
actually execute the plan dominates the time taken to revise beliefs, deliberate,
or plan, then the crucial concern is that the environment might change while
the plan is being executed. The problem is that the agent remains committed to
the intention it forms at step (5) until it has executed the plan in step (7). If the
environment changes after step (3), then the assumptions upon which this plan
The Belief-Desire-Intention Model 31
Figure 2.2
A first refinement of the agent control loop.
depends may well be invalid by the time the plan is actually executed.
So far, we have glossed over the problem of exactly how an agent might go
about deliberating. In this section, we consider the process in more detail. It
is not hard to see that in real life, deliberation typically begins by trying to
understand what the options available to you are. Returning to the career choice
example introduced above, if you gain a good first degree, then one option is
that of becoming an academic; if you fail to obtain a good degree, this option is
not available to you. Another option is entering industry. After deciding what
the options are, you must choose between them, and commit to some. These
chosen options then become intentions.
From this discussion, we can see that the deliberate function as discussed
above can be decomposed into two distinct functional components:
We represent option generation via a function, options, which takes the agent's
current beliefs and current intentions, and from them determines a set of
options that we will hereafter refer to as desires. The intuitive interpretation of
a desire is that, in an "ideal world," an agent would like all its desires achieved.
In any moderately realistic scenario, however, an agent will not be able to
32 Chapter 2
Figure 2.3
Refining the deliberation process into option generation and filtering.
achieve all its desires. This is because desires are often mutually exclusive. For
example, in the OASIS air-traffic control system, which was implemented using
a BDI architecture, an agent was tasked with the problem of finding the optimal
sequence in which to land aircraft at an airport [138]. The option generation
process in OASIS might generate the options of landing two different aircraft
on the same runway at the same time. Clearly, such options are mutually
exclusive: it would be undesirable to land both aircraft simultaneously.
Formally, the signature of the option generation function options is as
follows.
When an option successfully passes through the filter function and is hence
chosen by the agent as an intention, we say that the agent has made a commit
ment to that option. Commitment implies temporal persistence an intention,
-
once adopted, should not immediately evaporate. A critical issue is just how
committed an agent should be to its intentions. That is, how long should an
intention persist? Under what circumstances should an intention vanish?
To motivate the discussion further, consider the following scenario:
Some time in the not-so-distant future, you are having trouble with your ne w household
robot. You say "Willie, bring me a beer." The robot replies "OK boss." Twenty minutes
later, you screech "Willie, why didn't you bring me that beer?" It ans wers "Well, I
intended to get you the beer, but I decided to do something else." Miffed, you send
the wise guy back to the manufacturer, complaining about a lack of commitment. After
retrofitting, Willie is returned, marked "Model C: The Committed Assistant." Again,
you ask Willie to bring you a beer. Again, it accedes, replying "Sure thing." Then you
ask: "What kind of beer did you buy?" It ans wers: "Genessee." You say "Never mind."
One minute later, Willie trundles over with a Genessee in its gripper. This time, you
angrily return Willie for overcommitment. After still more tinkering, the manufacturer
sends Willie back, promising no more problems with its commitments. So, being a
somewhat trusting customer, you accept the rascal back into your household, but as a
test, you ask it to bring you your last beer. Willie again accedes, saying "Yes, Sir." (Its
attitude problem seems to have been fixed.) The robot gets the beer and starts to wards
you. As it approaches, it lifts its arm, wheels around, deliberately smashes the bottle,
and trundles off. Back at the plant, when interrogated by customer service as to why it
had abandoned its commitments, the robot replies that according to its specifications,
it kept its commitments as long as required - commitments must be dropped when
fulfilled or impossible to achieve. By smashing the bottle, the commitment became
unachievable. [35, pp.213-214]
The mechanism an agent uses to determine when and how to drop inten
tions is known as a commitment strategy. The following three commitment
strategies are commonly discussed in the literature of rational agents [187]:
• Blind commitment
A blindly committed agent will continue to maintain an intention until it
believes the intention has actually been achieved. Blind commitment is also
sometimes referred to asfanatical commitment.
• Single-minded commitment
A single-minded agent will continue to maintain an intention until it believes
that either the intention has been achieved, or else that it is no longer possible
34 Chapter 2
Figure 2.4
Introducing reactivity: the agent will engage in means ends reasoning when it believes a plao has
(for whatever reason) failed.
Note that an agent has commitment both to ends (i.e., the state of affairs it
wishes to bring about), and means (i.e., the mechanism via which the agent
wishes to achieve the state of affairs). Currently, our agent control loop is over
committed, both to means and ends. It never stops to reconsider its intentions,
and it remains committed to plans until they have been fully executed. We will
now see how this basic control loop can be refined in various ways, in order to
obtain different types of commitment.
The first modification we make allows the agent to replan if ever a plan
goes wrong. This reduces the commitment that an agent has towards the means
to achieve its intentions. The revised control loop is illustrated in Figure 2.4.
Using this loop, the agent will be committed to a plan to achieve its
intentions only while it believes that the plan is sound given its beliefs about
The Belief-Desire-Intention Model 35
Figure 2.5
Dropping intentions that are either impossible or that have succeeded.
the current state of the world. If it ever detennines that its plan is no longer
appropriate in order to achieve the current intention, then it engages in further
means-ends reasoning in order to find an alternative plan. Given that its beliefs
are updated every time it executes an action, this implies at least some degree
of reactivity.
This version of the control loop is clearly more attuned to the environment
than previous versions, but it still remains overcommitted to intentions. This
is because although the agent will replan if ever it believes the plan is no
longer appropriate, it never stops to consider whether or not its intentions are
appropriate. This consideration motivates the next version of the control loop,
in which an agent explicitly stops to detennine whether or not its intentions
have succeeded or whether they are impossible. We write succeeded(I, B) to
mean that given beliefs B, the intentions I can be regarded as having been
satisfied. Similarly, we write impossible(I, B) to mean that intentions I are
impossible given beliefs B. The revised control loop is then illustrated in
Figure 2.5.
It is easy to see that this revised agent control loop implements single
minded commitment. The modifications required to implement open-minded
36 Chapter 2
In our current algorithm, an agent will get to reconsider its intentions once
every time around the outer control loop. This implies that it will reconsider its
intentions when one of the following three conditions arises:
Although this ensures that the agent is neither undercommitted nor overcom
mitted to its intentions, it is limited in the way that it permits an agent to re
consider its intentions. The main problem is that it does not allow an agent to
exploit serendipity. To see what I mean by this, consider the following scenario.
Sophie is a BDI soft ware agent whose task is to obtain documents on behalf of a user.
One day, the user instructs Sophie to obtain a soft copy of the Ph.D. thesis by A. N.
Other, and Sophie creates an intention to this effect. Sophie believes that the Ph.D. is
resident at A. N. Other's www site, and so generates an intention to do wnload it from
there. While she is planning ho w to achieve this intention, ho wever, she is told that a
local copy of the thesis exists. It would clearly be more efficient to obtain this version,
but since there is nothing wrong with the intention of do wnloading the Ph.D. remotely
(she believes it will succeed), she continues to do so.
In this scenario, Sophie would do better to reconsider her intentions while she
is executing the plan. A first attempt to modify the agent control loop would
involve reconsidering intentions every time the agent executed the inner loop
in Figure 2.5: see Figure 2.6. Such an agent is cautious, in the sense that it
always stops to reconsider its intentions before performing an action.
If option generation and filtering were computationally cheap processes,
then this would be an acceptable strategy. Unfortunately, we know that delib
eration is not cheap - it takes a considerable amount of time. While the agent
is deliberating, the environment in which the agent is working is changing,
possibly rendering its newly formed intentions irrelevant.
The Belief-Desire-Intention Model 37
Figure 2.6
A cautious agent, which stops to reconsider intentions before perfonning aoy action.
• an agent that does not stop to reconsider its intentions sufficiently often will
continue attempting to achieve its intentions even after it is clear that they
cannot be achieved, or that there is no longer any reason for achieving them;
• an agent that constantly reconsiders its attentions may spend insufficient
time actually working to achieve them, and hence runs the risk of never actually
achieving them.
Figure 2.7
An agent that attempts to strike a balance between boldness and caution: whether or not the agent
chooses to reconsider intentions is determined by the booleao-valued function reconsider(...) .
In this version of the agent control loop, the burden of deciding when to
expend effort by deliberating lies with the function reconsider( . . . ) . It is in
teresting to consider the circumstances under which this function can be said
to behave optimally. Suppose that the agent's deliberation and plan generation
functions are in some sense perfect: that deliberation always chooses the "best"
intentions (however that is defined for the application at hand), and planning al
ways produces an appropriate plan. Further suppose that time expended always
has a cost - the agent does not benefit by doing nothing. Then it is not diffi
cult to see that the function reconsider( . . . ) will be behaving optimally if, and
only if, whenever it chooses to deliberate, the agent changes intentions [25 1].
For if the agent chose to deliberate but did not change intentions, then the ef
fort expended on deliberation was wasted. Similarly, if an agent should have
changed intentions, but failed to do so, then the effort expended on attempting
to achieve its intentions was also wasted.
The Belief-Desire-Intention Model 39
Table 2.1
Practical reasoning situations (cf. [22, p.353]).
• In situation ( 1), the agent did not choose to deliberate, and as a consequence,
stop to reconsider after the execution of every action. These characteristics are
defined by a degree of boldness, which specifies the maximum number of plan
steps the agent executes before reconsidering its intentions. Dynamism in the
environment is represented by the rate of world change, 'Y. Put simply, the rate
of world change is the ratio of the speed of the agent's control loop to the rate
of change of the world. If'Y 1, then the world will change no more than once
=
for each time the agent can execute its control loop. If'Y 2, then the world
=
can change twice for each pass through the agent's control loop, and so on. The
performance of an agent is measured by the ratio of number of intentions that
the agent managed to achieve to the number of intentions that the agent had at
any time. Thus if effectiveness is 1, then the agent achieved all its intentions.
If effectiveness is 0, then the agent failed to achieve any of its intentions. The
main results of Kinny and Georgeff's experiments are shown in Figure 2. 8. 1
This graph shows the effectiveness of an agent on the y axis against the dy
namism of the world (log scale) on the x axis. The key results of Kinny and
Georgeff were as follows.
• If'Y is low (i.e., the environment does not change quickly), then bold agents
do well compared to cautious ones. This is because cautious ones waste time
reconsidering their commitments while bold agents are busy working towards
- and achieving - their intentions.
• If'Y is high (i.e., the environment changes frequently), then cautious agents
tend to outperform bold agents. This is because they are able to recognize when
intentions are doomed, and also to take advantage of serendipitous situations
and new opportunities when they arise.
The bottom line is that different environment types require different intention
reconsideration and commitment strategies. In static environments, agents that
are strongly committed to their intentions will perform well. But in dynamic
environments, the ability to react to changes by modifying intentions becomes
more important, and weakly committed agents will tend to outperform bold
agents.
Bold -
Cautious ----.
0.9
0.8
0.7
0.6
..
..
.,
"
.,
.<! 0.5
U
� 0.4
0.3
0.2
0.1
Figure 2.8
Kinny and Georgeff's intention reconsideration experiments.
moment to examine the justification for using such terms. It may seem strange
to think of computer programs in terms of mental states such as beliefs, desires,
and intentions. Is it either useful or legitimate to use mentalistic terminology to
characterize machines? As it turns out, there is an extensive literature on this
subject.
When explaining human activity, it is often useful to make statements such
as the following:
Janine took her umbrella because she believed it was going to rain.
Michael worked hard because he wanted to finish his book.
the intentional notions. 2 The philosopher Daniel Dennett has coined the term
intentional system to describe entities "whose behavior can be predicted by
the method of attributing belief, desires and rational acumen" [43, p.49], [42].
Dennett identifies different "levels" of intentional system:
Afirst-order intentional system has beliefs and desires (etc.) but no beliefs and desires
about beliefs and desires. [... ] A second-order intentional system is more sophisti
cated; it has beliefs and desires (and no doubt other intentional states) about beliefs and
desires (and other intentional states) -both those of others and its o wn. [43, p.243]
What objects can be described by the intentional stance? As it turns out, almost
any automaton can. For example, consider a light switch:
It is perfectly coherent to treat a light s witch as a (very cooperative) agent with the
capability of transmitting current at will, who invariably transmits current when it
believes that we want it transmitted and not otherwise; flicking the s witch is simply
our way of communicating our desires. [205, p.6]
And yet most adults in the modem world would find such a description absurd
- perhaps even infantile. Why is this? The answer seems to be that while
the intentional stance description is perfectly consistent with the observed
2 Unfortunately, the word "intention" is used in several different ways in logic and the philosophy
of mind. First, there is the BDI-like usage, as in "I intended to kill him." Second, an intentional
notion is one of the attitudes, as above. Finally, in logic, the word intension (with an "s") means the
internal content of a concept, as opposed to its extension. In what follows, the intended meaning
should always be clear from context.
The Belief-Desire-Intention Model 43
...it does not buy us anything, since we essentially understand the mechanism suffi
ciently to have a simpler, mechanistic description of its behavior. [205, p.6]
Put crudely, the more we know about a system, the less we need to rely
on animistic, intentional explanations of its behavior. 3 An obvious question
is then, if we have alternative, perhaps less contentious ways of explaining
systems, why should we bother with the intentional stance? Consider the
alternatives available to us. One possibility is to characterize the behavior of
a complex system by using the physical stance [44, p.36]. The idea of the
physical stance is to start with the original configuration of a system, and then
use the laws of physics to predict how this system will behave:
When I predict that a stone released from my hand will fall to the ground, I am using
the physical stance. I don't attribute beliefs and desires to the stone; I attribute mass, or
weight, to the stone, and rely on the la w of gravity to yield my prediction. [44, p.37]
Another alternative is the design stance. With the design stance, we use knowl
edge of what purpose a system is supposed to fulfill in order to predict how it
behaves. Dennett gives the example of an alarm clock [44, pp.37-39]. When
someone presents us with an alarm clock, we do not need to make use of phys
ical laws in order to understand its behavior. We can simply make use of the
fact that all alarm clocks are designed to wake people up if we set them with
a time. No understanding of the clock's mechanism is required to justify such
an understanding - we know that all alarm clocks have this behavior.
However, with very complex systems, even if a complete, accurate pic
ture of the system's architecture and working is available, a physical or design
stance explanation of its behavior may not be practicable. Consider a computer.
Although we might have a complete technical description of a computer avail
able, it is hardly practicable to appeal to such a description when explaining
why a menu appears when we click a mouse on an icon. In such situations,
it may be more appropriate to adopt an intentional stance description, if that
description is consistent, and simpler than the alternatives.
3 Shoham observes that the move from an intentional stance to a technical description of behavior
correlates well with Piaget's model of child development, and with the scientific development
of humankind generally [205]. Children will use animistic explanations of objects - such as
light switches - until they grasp the more abstract technical concepts involved. Similarly, the
evolution of science has been marked by a gradual move from theological/animistic explanations
to mathematical ones. The author's own experiences of teaching computer programming suggest
that, when faced with completely unknown phenomena, it is not only children who adopt animistic
explanations. Indeed, it often seems easier to teach some computer concepts by using explanations
such as: "the computer doesn't know. . . ," than to try to teach abstract principles first.
44 Chapter 2
Note that the intentional stance is, in computer science terms, nothing
more than an abstraction tool. It is a convenient shorthand for talking about
complex systems, which allows us to succinctly predict and explain their
behavior without having to understand how they actually work. Now, much of
computer science is concerned with looking for good abstraction mechanisms,
since these allow system developers to manage complexity with greater ease.
The history of programming languages illustrates a steady move away from
low-level machine-oriented views of programming towards abstractions that
are closer to human experience. Procedural abstraction, abstract data types,
and most recently, objects are examples of this progression. So, why not
use the intentional stance as an abstraction tool in computing - to explain,
understand, and, crucially, program complex computer systems?
There are other reasons for believing that an intentional stance will be use
ful for understanding and reasoning about computer programs [10 2]. First, and
perhaps most importantly, the ability of heterogeneous, self-interested agents
to communicate seems to imply the ability to talk about the beliefs, aspirations,
and intentions of individual agents. For example, in order to coordinate their
activities, agents must have information about the intentions of others [105].
This idea is closely related to Newell's knowledge level [166]. Later in this
book, we will see how mental states such as beliefs, desires, and the like are
used to give a semantics to speech acts [20 2, 35]. Second, mentalistic models
are a good candidate for representing information about end users. For exam
ple, imagine a tutoring system that works with students to teach them JAVA
programming. One way to build such a system is to give it a model of the
user. Beliefs, desires, and intentions seem appropriate for the makeup of such
models.
For many researchers in AI, this idea of programming computer systems
in terms of "mentalistic" notions such as belief, desire, and intention is the
key component of agent-based computing. The idea of programming computer
systems in terms of mental states was articulated most clearly by Yoav Shoham
in his agent-oriented programming (AOP) proposal [206]. BDI systems can be
viewed as a kind of AOP.
Some reflections on the origins of the BDI model, and on its relationship to
other models of agency, may be found in [74]. Belief-desire-intention archi-
The Belief-Desire-Intention Model 45
tectures originated in the work of the Rational Agency project at Stanford Re
search Institute in the mid- 1980s. Key figures were Michael Bratman, Phil
Cohen, Michael Georgeff, David Israel, Kurt Konolige, and Martha Pollack.
The origins of the model lie in the theory of human practical reasoning de
veloped by the philosopher Michael Bratman [20], which focuses particularly
on the role of intentions in practical reasoning. The conceptual framework of
the 8DI model is described in [2 2], which also describes a specific 8DI agent
architecture called IRM A .
The best-known implementation of the 8 D I model is the PRS system, devel
oped by Georgeff and colleagues [78, 77]. The PRS has been re-implemented
several times since the mid- 1980s, for example in the Australian AI Institute's
DMARS system [46], the University of Michigan's c + + implementation U M
PRS, and a JAVA version called JAM ! [100]. JACK is a commercially available
programming language, which extends the JAVA language with a number of
8DI features [26].
The description of the 8DI model given here draws upon [22] and [188],
but is not strictly faithful to either. The most obvious difference is that I
do not incorporate the notion of the "filter override" mechanism described
in [2 2], and I also assume that plans are linear sequences of actions (which
is a fairly "traditional" view of plans), rather than the hierarchically structured
collections of goals used by PRS .
Plans are central to the 8DI model of agency. An excellent discussion on
the 8DI model, focusing in particular on the role of plans in practical reasoning,
is Martha Pollack's 199 1 Computers and Thought award lecture, presented at
the IJCAI-9 1 conference in Sydney, Australia, and published as "The Uses of
Plans" [180]. Another article, which focuses on the distinction between "plans
as recipes" and "plans as mental states" is [179].
It is worth emphasizing that the 8DI model is only one solution to the prob
lem of building autonomous rational agents. Many other software architectures
for agent systems have been described in the literature [249, 24]. The so-called
"layered" architectures are currently very popular [24 2]; examples include Fer
guson's TOURING MACHINES [57, 58], Muller's INTERRAP [163, 16 2], and the
3T architecture [17]. I mentioned in passing that belief revision is not a concern
of this book: see Gardenfors [71] for further information.
Finally, although in this book I focus on what might be called the "ortho
dox" 8DI model, the 8DI model forms a central component of many other sys
tems, which either draw inspiration from it or implement parts of it. Examples
include [6 1, 1 1 1, 158, 26].
3 Introduction to CORA
From a logical point of view, combining these elements into a single frame
work makes .cORA rather complex. For this reason, the presentation of
.cORA is divided into two parts. The first part (this chapter), simply gives
an informal introduction to the logic: the main constructs it provides, the in
tuitive semantics of these constructs, how these constructs can be used to ex
press properties of agents and their environments, but most importantly, how to
readandunderstand formulae of .cORA. This chapter is intended for readers
whose logical background is not strong. If you are already familiar with the
principles of first-order, modal, temporal, and dynamic logic, then you may
wish to skim through this chapter and move quickly to the next chapter, which
contains a detailed formal presentation of the language.
48 Chapter 3
Table 3.1
First-order logic connectives and quantifiers.
Formula Interpretation
-' 'P 'P is not true
'P/\1/J 'P is true and 1/J is true
'PV1/J 'P is true or 1/J is true
'P�1/J if 'P is true then 1/J is true
'P{:}1/J 'P is true if, and only if, 1/J is true
( 7 = 7' ) 7 is the same as 7
'
This fonnula simply asserts that all objects x which satisfy property Man also
satisfy the property Mortal. The intended interpretation of the fonnula is that
all men are mortal.
Fonnally, the x in this fonnula is a variable. By default, we will use the
lowercase italic roman letters x, y, and z as variables throughout the book, in
order to give the reader some help in understanding fonnulae.
Man and Mortal are predicates. The Man and Mortal predicates each take
a single argument, and hence they have an arity of one. Predicates with arity
one (i.e., that take a single argument) are called properties, or unary predicates.
By default, predicate symbols are written as strings of roman letters, starting
with an uppercase letter. Where appropriate, predicates are InterCapped in the
interests of readability.
The symbol "\I" is the universal quantifier, and is read as "for all." The
symbol "=>" is the logical connective for implication. Any fonnula with the
shape cp => 'l/J is read as " cp implies 'l/J," or "if cp then 'l/J." Finally, the raised dot
". " and parentheses ") " and "( " are punctuation symbols.
Introduction to .cORA 49
This formula asserts that for every object x that satisfies the property Man,
there exists at least one object y such that y satisfies the property of being a
woman, and in addition, the MotherOf relationship exists between x and y. In
other words, for every man x, there is a woman y such that y is the mother of x.
In this example, x andy are variables, Man and Woman are predicate symbols
of arity one, and MotherOf is a predicate of arity two. Predicates of arity two
are often referred to as two-place predicates, or binary predicates.
The third example illustrates the use of constants.
This formula asserts that there is at least one objectx such that x is a Monitor
and the state of x is rea dy. Here, Monitor and MonitorState are predicates
of arity one and two respectively, x is a variable, and rea dy is a constant.
A constant is just a fixed name for a particular thing. Thus formula (3.3)
intuitively expresses the fact that some monitor is in a "ready" state.
This formula asserts that for all peoplex and y, x is not superior to y in other
-
This formula asserts that if x is u.s. President and y is u.s. President, then x
andy must be the same. In other words, there is only one u.s. President.
Examples (3.1}-{3.6) demonstrate some conventions that will be used
throughout the remainder of the book:
Table 3.2
Belief, desire, and intention modalities.
Formula Interpretation
(Bel i cp) agent i believes cp
(Des i cp) agent i desires cp
(Int i cp) agent i intends cp
Before proceeding, see if you can determine for yourself the intended
interpretation of the following formulae.
So far, all we have is ordinary first-order logic. But CORA extends first-order
logic in a number of important ways. First, CORA incorporates a whole class
of extra connectives, known as modal connectives or modalities, which allow
us to represent the beliefs, desires, and intentions of agents - see Table 3.2
for an overview. We will illustrate these modal connectives by way of example
at first, and then discuss some technicalities associated with their use.
We will start with belief. The basic idea is to have a class of formulae with
the following structure.
We can constrain the variable i so that it only refers to English people - the
intended reading of (3.11) is thus that every English person believes it is sunny
in Melbourne.
Note that, although Bel is written a little like an ordinary first-order logic
predicate that takes two arguments, it is actually very different. The most
obvious difference is that the arguments to an ordinary first-order predicate
must all be terms of first-order logic: variables, constants, or functions that
return some value. The first argument to the Bel modality is indeed a term,
although it is a special kind of term - one that stands for an agent. To see why
this is important, consider that although the first argument to the Bel modality
in the following formula is a term, the formula does not make much sense.
Just as we must be careful to ensure that the first argument to the Bel modality
is a term denoting an agent, so we must be careful to ensure that the second
argument is a formula. As the second argument in the following formula is a
52 Chapter 3
(Beljanine 2) (3.13)
3x . (Beljanine x) (3.14)
You might absentmindedly write this formula while trying to represent the fact
that there is something that Janine believes. As it turns out, statements like this
cannot be represented in our language. The following misguided attempt to
represent the statement "Janine believes everything Michael believes" is also
illegal in CORA.
Although some logics provide the machinery to represent such statements, they
are somewhat complex, and will not be necessary for us. (A short discussion
on the merits and drawbacks of such metalogics is provided in appendix B.)
Beliefs can be nested. The intended interpretation of the following formula
is that Janine believes Michael believes that London is rainy.
Of course, belief is just one of three modalities that we use to characterize the
state of 8DI agents - the other two are, not surprisingly, desires and intentions.
We introduce another two modal connectives, (Des i cp) and (Int i cp), to
represent desires and intentions respectively. The rules for making desire and
intention formulae are the same as for making belief formulae. Thus the
following formula is intended to say that Janine desires it to be sunny in
Melbourne.
Similarly, the following formula says that Michael intends to complete his
lecture slides.
As with beliefs, desires and intentions can be nested. Perhaps more interesting,
however, is the fact that we can nest belief, desire, and intention modalities
with one another. For example, consider the following formula, which is in
tended to express the fact that Michael intends that Janine believes it is sunny
in Melbourne.
The following formula says that Michael desires that everyone will intend to
own a book by Michael.
Before presenting the temporal component, we will deal with some slightly
more advanced issues connected with modalities and quantification. If you
found the material presented so far hard going, you may wish to skip this
section on a first reading.
One of the most difficult issues surrounding the combination of modal opera
tors and first-order logic is connected with the problem ofsubstitutin g terms in
the context of modal connectives. Essentially, the standardsubstitution rules of
first-order logic do not apply in the cont ext of modal operators. To understand
54 Chapter 3
Janine believes Keanu Reeves (an actor) is cute. In addition to being an actor, Keanu
Reeves is also bass-player for the grunge metal band "Dogstar." Although Janine has
heard of Dogstar, and knows they have a bass player, she has no idea that this bass
player is Keanu Reeves. Does Janine believe the bass-player of Dogstar is cute?
Combining quantification with modal operators can lead to some interesting (if
somewhat arcane) situations. Consider the following formula, which its author
intended to express the fact that Janine believes somewhere is sunny.
Are these two formulae expressing the same or different properties? In our
framework, they are different. Formula (3.24) expresses aweaker property than
(3.25). Specifically, it is expressing the fact that Janine believes somewhere is
sunny, but that she does not necessarily know where - she is not necessarily
aware of the identity of the sunny place. In contrast, (3.25) expresses a stronger
property. It says that there is a place x such that Janine believes of x that
it is sunny. Implicitly, (3.25) says that Janine is aware of the identity of the
sunny place. The terminology is that in (3.25), the variable x is quantified de
re, whereas in (3.24), it is quantified de dicto. The practical upshot of this is
that we need to be quite careful when quantifYing in to the scope of a modal
connective, to be sure that we get the interpretation we intend.
Quantifying in to modal contexts has long been recognized as one of the
trickier topics in modal logic; see [101, pp.170-21O] and [54, pp.83-86] for
discussions.
(Beljanine Sunny(melbourne))
t5
t8
Figure 3.1
An example of a branching temporal structure.
think of representing the choices available to agents with respect to the actions
they perform. Depending on which choices these agents make, the future may
unfold in different ways. But also, we assume there is inherently some non
determinism in the environment. That is, the result of an action performed by
an agent is not pre-determined - there will be a number of possible outcomes.
To summarize, while the past is seen as linear, the future is seen as branch
ing. Moreover, we assume that there is no "end of time." In our model, time
branches infinitely into the future. All this may sound rather abstract unless
you are familiar with temporal logics, that is, logics for reasoning about dy
namic environments. To make it more concrete, a simple temporal model is
presented in Figure 3.1 (more accurately, Figure 3.1 shows part of a temporal
model).
In this model, there are ten time points, labeled to to t9 respectively. Each
time point is shown as an oval. The arrows between ovals show the progression
of time, and so ovals to the right are "later" than those to the left. We take
"now" - our index into this model - to be t1. Thus the flow of time to the
left of t 1 (the past) is linear, and to the right of t 1 (the future) is branching.
Time points are labeled with the statements that are true in them. Thus
in t1, the statements q, r, and s are all true, and all other predicates are false.
Introduction to .cORA 57
Table 3.3
Path connectives.
Fonnula Interpretation
'P is true next
'P is eventually true
'P is alway s true
'P is true until 'I/J is true
'P is true unless 'I/J is true
• "0" means "next" - thus 0cp is satisfied now if cp is satisfied at the next
moment;
• "0" means "sometime" - thus Ocp is satisfied now if cp is satisfied either
now or at some future moment;
• "0" means "always" - thus 0 cp is satisfied now if cp is satisfied now and
With respect to the path (t1, t2, t6, . . .) it is easy to see that the formula
o(q 1\ r 1\ -,s 1\ -,t) is true, since q and r are both true in time point t2 (i.e., the
next time point along) and s and t are both false in t2. Similarly, the formula
O -,t is true on this path, since t is eventually false on this path (in fact, it is
false in time points t2 and t6). The formula Or is true on this path, because r
is true on every time point of the path. However, the formula Oq is not true
58 Chapter 3
Table 3.4
Path quantifiers.
Formula Interpretation
cp is true on all paths
cp is true on some path
when evaluated on this path, since while q is true in time points t1 and t2, it is
not true in time point t6. Similarly, the formula <It is not true when evaluated
on this path, since t is not true at any time point on this path.
With respect to the path (t1, t4, t9, . . .) , the formula 0(q 1\ r 1\ s) is true,
since q, r, and s are all true in time point t4. The formula qUt is true on this
path, because q is true at all time points until the time point where t is true
(time point t9).
We are allowed to combine temporal operators, so that <I(PUq) is an
allowable formula, for example. We refer to the formulae that may be built
up using these path connectives as path formulae.
The next connectives provided by .cORA allow us to quantifY over paths
- see Table 3.4. The idea is as follows. Consider the five paths that originate
in time point t1. Then the formula
Dr (3.26)
is true on all these paths. In other words, (3.26) is inevitable. We have a modal
connective "A" that allows us to express the fact that some path formula is
inevitable:
ADr
We interpret a formula Arp as "on all paths that emerge from now, rp is true."
We call "A" the universal path quantifier.
You might guess that, as well as having a universal path quantifier, we
have an existential path quantifier, and indeed we do: " E." A formula E rp is
interpreted as "on some path that emerges from now, rp is true." This formula
will be true in some time point t if there is at least one path (possibly more than
one) rooted at t such that the path formula rp is true on this path. Thus in time
point t1, the formula
E(qUt)
is true, since qUt is true on the path (t1,t4,t9, . . .) , which is rooted at t1.
Formulae that have no temporal operators, or that are prefixed with "A" or " E"
Introduction to .cORA 59
• ( AOp) A( E <)-p)
• A[(Op) A (0O -p )]
• A[(Op) A (O -p )]
• A[(P =? q) V (p =? O·r)]
We saw above that quantifying in to belief, desire, and intention contexts can
lead to complex situations. The temporal operators of .cORA are also modal
connectives, of a kind, and they also fall prey to these problems. To see what
I mean by this, consider the following (path) formula, which is intended to be
read as "Tony is and always will be Prime Minister."
Now consider the following two existentially quantified versions of this for
mula.
Formula (3. 28) asserts that there is always some Prime Minister. That is,
whatever time point we pick, there will be an individual that has the property
of being Prime Minister.
In contrast, (3. 29) asserts that there is some individual who is always Prime
Minister. The distinction is that in (3. 28), there could be a different Prime
Minister at every time point. In contrast, in (3. 29), there is just one individual
who is Prime Minister in every time point. It should be clear that (3. 29) implies
(3. 28), but the converse does not hold.
A similar situation arises when we consider the " <)" operator. Consider the
following example.
Formula (3. 30) asserts that at some point in the future, everybody will be
free. In other words, there will be some particular time in the future at which
60 Chapter 3
This example asserts that everybody will be free at some time in the future,
but it does not imply that everybody will simultaneously be free. Thus I could
be free at time tl, you could be free at time t2, and so on. Now (3.30) implies
(3.31), but the converse does not hold.
Dcp
A local invariance states that whenever cp holds, 'I/; must hold also. Such
invariances are specified by formulae with the following shape.
2 The material in this section has been adapted from [49, p.1049--1054].
Introduction to .cORA 61
This formula states that at most one of the properties 'Pi E {'Pl,···, 'Pn}
should hold at any one time. The � notation arises if one imagines that
truth is valued at 1, falsity at 0; the above formula is read "at most one
of 'Pi E {'Pl, ..., 'Pn} is true." Any formula written in �-notation can be
expanded into an ordinary formula if required; the �-notation may therefore
be regarded as an abbreviation.
A liveness property is one that states that "something good will eventually
happen." The simplest liveness properties have the following shape.
This states that every path that initially satisfies the property 'P eventually sat
isfies property X. Here X is the property that holds when a path has terminated.
Another useful liveness property is temporal implication.
Table 3.5
Operators for representing actions.
Formula Interpretation
(Happens 0) action expression 0 happens next
(Achvs 0 'P) action0 occurs, and achieves 'P
(Agts 0 g) group g is required to do action 0
effects of these actions. Before we do this, we need to say a little about how
actions fit into our temporal model.
The basic idea is that transitions between states are labeled with actions.
Intuitively, it is the perfonnance of an action by some agent that causes the
change in state. We assume that actions are atomic: only one action is ever
perfonned at any given time. However, we do allow for the same action
perfonned in the same state having multiple possible outcomes.
To illustrate these ideas, consider Figure 3. 2, in which the branching tem
poral structure of Figure 3. 1 has been augmented by labeling state transitions
with the actions that cause them. For simplicity, we will assume in this exam
ple that there is only one agent in the environment. From state to, the agent
perfonns action aI, which transfonns the environment to state tl. When the
environment is in state tl, the agent has a choice of two actions available to it.
It can either perfonn action a2 or it can perfonn a3. If it perfonns a2, then
either state t2 or state t3 can result. If instead it chooses to perfonn a3, then the
only possible outcome is state t4. From state t2, the agent has no choice about
what action to perfonn - it must perfonn a4, and either state t5 or state t6 will
result. From state t3, the agent can only perfonn action a5, and only state f7
can result. Finally, when the environment is in state t4, the agent has a choice
of perfonning either a6 or a3, with t8 or t9 resulting respectively.
.cORA provides a number of connectives that allow us to express the
properties of actions; these are summarized in Table 3. 5. In order to express the
fact that some action happens, we have a modal connective "Happens." This
connective is similar to 0, <>, and D in that it expresses a property of a path.
This operator takes a single argument, an action expression, and expresses the
fact that this action expression is the first thing that happens on the path. For
example, the fonnula
is true when evaluated on the path (tl, t2, t5, . . . ) , for the obvious reason that
a2 is the first action that happens on this path.
Introduction to .cORA 63
t5
t2
t6
a4
a2
t8
a3
a6
t9
a3
Figure 3.2
A branching temporal structure including actions that cause state transitions.
Table 3.6
Constructors for action expressions.
Expression Interpretation
Q;Q' a followed by a'
l
a a' either a or a'
a* a repeated more than once
cp? cp is satisfied
is true on this path, since a2 is the action that transforms t1 to t2, and a4
transforms t2 to t5.
The non-deterministic choice constructor, "I," simply means that one of its
arguments occurred. Thus the formula
is true on path ( t1' t2, t5, ...) , since one of a2 or a5 occurs on the first transi
tion. So (Happens a l a') means that either a happens or a' happens.
The iteration constructor, "*," means that its argument occurs zero or
more times in succession. With respect to Figure 3.2, consider the path
( t1' t2, t5, ...) . The formula
(Happens a 2*)
is trivially true on this path, since a2 transforms t1 to t2. On the path
( t1' t4, t9, ...) , the action a3 occurs twice in succession, and so the formula
Formula (3.32) is true when evaluated on path ( t1' t2, t5, ...) , since the formula
q is true on the first state of this path, t1. However, (3.32) is false when
evaluated on the path ( t3, t7 , ...) , since q is not true in t3.It may not be obvious
why we have the "test" construct. To see why, consider the following formula.
This formula says that either ('1'7; a) will happen or (""'1'7; a') will happen.
Thus if 'I' is true then a will happen, else if ""'1' is true then a' will happen. So
the action expression ('1'7; a) I (""'1'7; a') captures the sense of a statement
'
if 'I' then a else a .
while 'I' do a
Introduction to CORA 65
(Achvs a '1')
3a· (Happens a)
3'1' . (Happenscp?)
66 Chapter 3
CORA contains terms that denote groups of agents, and gives us a simple
but powerful set-theoretic apparatus to represent the properties of such groups.
The basic construct, with the obvious set-theoretic interpretation, is as follows.
(i E g)
This state formula asserts that the agent denoted by i is a member of the group
denoted by g.Here g is a term that stands for a (non-empty) set of agents.
As well as simply asserting that one agent is a member of a group, we have
the expected set-theoretic constructions (�, C) for expressing subset and other
relations between groups of agents.
4.1 Syntax
Associated with each predicate symbol is a natural number called its arity,
given by the arity function.
A sort is eitherAg, Ac, Gr, or U. If a is a sort, then the set Term,,, of terms
a/ sort a, is defined as follows.
4.2 Semantics
• discrete;
• bounded in the past (there is a "start of time");
72 Chapter 4
Figure 4.1
The syntax of CORA.
We let R � TxT be the branching temporal structure that encodes all ways in
which the system can evolve. Arcs in R will correspond to the performance of
atomic actions by agents within the system, and we therefore label these arcs
with the actions that they correspond to via the functionAct.
The state of an agent is defined by its beliefs, desires, and intentions. The
semantics of beliefs, desires, and intentions are given using possible worlds,
or Kripke semantics [31]. Thus an agent's beliefs in any given situation are
characterized by a set of situations - those that are consistent with the agent's
beliefs. An agent is then said to believe r.p if r.p is true in all these possible
situations. We refer to this set of "belief alternatives" as belief-accessible
situations. Similarly, an agent's desires in any given situation are characterized
as a set of situations - those that are compatible with the agent's desires. As
might be expected, we refer to these as desire-accessible situations. Finally, an
agent's intentions in a given situation are characterized by a set of intention
accessible situations, each of which represents a state of affairs compatible
with the agent's intentions.
At this point, the semantics of our framework appear to be quite conven
tional. However, worlds in CORA are not instantaneous states but are them
selves branching time structures. The intuition is that such structures represent
an agent's uncertainty not only about how the world actually is, but also about
how it will evolve.
Formally, a world is a pair (T', R'), where T' � T is a non-empty set of
time points, and R' � R is a branching time structure on T'. Let W be the set
of all worlds over T. Formally, W is defined as follows.
W = {(T', R') I T' � T, R' � R, and T' = ( dom R' U ran R'H
Sw = { (w, t) I wE W and t E Tw }
B : DAg -+ p( W x T x W ).
Belief accessibility relations are required to satisfy several properties. The first
is that if a world w' is accessible to an agent from situation (w, t), then t is
required to be a time point in bothwandw'. Formally, this requirement (which
we call world/time point compatibility) is captured as follows.
We also require that the relation that the function B assigns to every agent is
serial, transitive, and Euclidean. B is said to be:
• serial if for all situations (w, t), there is some worldw' such thatw' E B�(i);
• transitive ifw' E Br(i) andw" E B�' (i) impliesw" E B�(i); and
• Euclidean ifw' E B�(i) andw" E B�(i) impliesw' E B�" (i).
These requirements ensure that the logic of belief corresponds to the well
known modal logic system KD45 [31] we will see a proof of this later.
-
D : DAg -+ p( W x T x W)
I: DAg -+ p( W x T x W)
Both D and I are assumed to assign agents serial relations. This ensures that
the desire and intention modalities have a logic of KD [31]; we also require that
CORA Defined 75
Domains
We now need to identify the objects that we can refer to using CORA. The
language will contain terms that stand for these objects, and in particular, these
are the objects over which we can quantify. These objects represent the domain
of CORA the universe ofdiscourse.
-
The domain of CORA contains agents, given by the set DAg, as well as
actions (given by the set DAc). We will also allow quantification over sequences
of actions, i.e., the set DAc' groups of agents, given by the set DGr (where
DGr � p(DAg)), and other objects (pints of beer, chairs, pieces of string, etc.)
given by a set Du.
Putting these components together, a domain (of interpretation), D, is a
structure:
where:
• DGr = p(DAg) \ {0} is a set of non-empty subsets of DAg, i.e., the set of
(Notice thatD includes the set of sequences over DAc, rather than simply the
set DAc.) If D is a domain and u E IN, then byDU we mean the set of u-tuples
overD.
DU=Dx···xD
'-v-"
u times
Denotation
The function <I> is required to preserve arity. In other words, if the function
assigns a predicate symbol P a set of u-tuples, then the arity of P should be u.
Formally, this condition can be stated as follows.
C: Canstx T-tD
V: Var-tD
[T, t]v,C =
A { C(T, t) ifTE Const
V(T) otherwise.
Since V, C, and the time point in which we are evaluating formulae will always
be clear from context, reference to them will usually be suppressed: we simply
write [T] .
where:
The semantics of the language are defined in two parts, for path formulae
and state formulae respectively. The semantics of path formulae are given
via the path formula satisfaction relation, "FP", which holds between path
formulae interpretations and path formulae. A path formula interpretation is
a structure (M, V, w, p) , whereM is a model, V is a variable assignment, w is
78 Chapter 4
Figure 4.2
Rules defining the semantics of path formulae. Note that the rule for Happens makes use of the
occurs predicate, which is defined in the text.
a world in M, and p is a path through w. The rules defining the path formula
satisfaction relation are given in Figure 4.2. If (M, V, w,p) FP <p, then we say
(M, V, w,p) satisfies <p, or equivalently, that <p is true in (M, V, w,p).
The semantics of state formulae are given via the state formula satisfaction
relation, "Fs". This relation holds between state formulae interpretations
and state formulae. State formulae interpretations are structures of the form
(M, V, w,t), where M is a model, V is a variable assignment, w is a world
in M, and t E Tw is a time point in w. The rules defining this relation are
given in Figure 4.3. As with path formulae, if (M, V, w,t) FS <p, then we say
(M, V, w,t) satisfies <p, or <p is true in (M, V, w,t).
{
The rule for the Agts connective makes use of a function Agts, which
extends the Agt function to arbitrary action expressions.
{Agt(ad,...,Agt(ak)} where [a,t] = al,...,ak
( ) Agts(al,t)UAgts(a2,t) where a = al; a2 or a = al I a2
Agts a,t =
A
The semantic rules for path formulae make use of an important auxiliary
definition: occurs. This definition is used to define the Happens operator.
We write occurs(a,p,u,v ) to indicate that action a occurs between "times"
CORA Defined 79
(M, V, w, t) FS true
(M, V, w, t) FsP(Tl,... ,Tn) iff (h], ... , [Tn]) E <l>(P,t)
(M, V, w, t) FS -''P iff(M, V, w, t) ftos 'P
(M, V, w, t) FS 'P V 1/1 iff(M, V, w, t) FS 'P or (M, V, w, t) FS 1/1
(M, V, w, t) FS \Ix· 'P iff(M, V t {x t-+ d}, w, t) FS 'P
for all d ElJ such that x and d are of the same sort
(M, V, w, t) FS (Bel i 'P) iff\lw' E W, ifw' E B7([i]), then (M, V, w', t) FS 'P
(M, V, w, t) FS (Goal i 'P) iff\lw' E W, ifw' E 1J7([i]), then (M, V, w', t) FS 'P
(M, V, w, t) FS (Int i 1/1) iff\lw' E W, ifw' E:r;"([i]), then (M, V, w', t) FS 'P
(M, V, w, t) FS (Agts a g) iffAgts( a, t) = [g]
(M, V, w, t) FS (T T')
= iff[T] =[T']
(M, V, w, t) FS (i E g) iff[i] E [g]
(M, V, w, t) FS A'P iff\lp Epaths(w), ifp(O) = t, then (M, V, w, p) F1' 'P
Figure 4.3
Rules defining the semantics of state formulae.
Then:
• occurs ( ao,p, 0, 1) holds, as the arc (P( O) ,p ( l )) , i.e., ( to,t d , is labeled with
0.0;
• occurs ( ao; 0.1,p, 0,2) holds, as occurs ( ao,p, 0, 1) holds (this was the first
example), and occurs( a1,p, 1,2) holds, since the arc (P( 1) ,p(2)) , that is,
( t1' t2) , is labeled with the action 0.1;
• occurs ( ao; (0.1* ) ,p, 0,4) holds, as occurs ( ao,p, 0, 1) holds (this was the
first example), and occurs( a1*,p, 1,4) holds. To see that occurs( a1*,p, 1,4)
holds, note that occurs( a1,p, 1,2) holds and occurs( a1*,p,2,4) holds. To
see that occurs( a1*,p,2,4) holds, observe that occurs( a1,p,2, 3) holds and
occurs( a1*,p,3, 4) holds since occurs( a1,p,3, 4) holds.
80 Chapter 4
I leave it to the reader to use similar reasoning to show that the following
also hold.
occurs(a1*; a2,p, 1, 5)
Formally, the occurs predicate is defined inductively by five rules: one for each
of the action expression constructors, and one for the execution of primitive
actions. The first rule represents the base case, where a primitive action is
executed.
occurs(a,p,u,v ) iffv = u + k and [a,p(u)] = 0'.1,...,ak and
Act(p(u),p(u + 1)) = 0'.1,...,Act(p(u + k - l ),p(u + k)) = ak (4.2)
(where a E TermAc )
Thus primitive action a occurs on path p between u and u + 1 if the arc from
u to u + 1 is labeled with a.
The second rule captures the semantics of sequential composition. The
action expression a; a' will occur between times u and v iff there is some time
point n between u and v such that a is executed between u and n, and a' is
executed between n and v.
The semantics of iteration rely upon the fact that executing 0'.* is the same
as either: (i) doing nothing, or (ii) executing a once and then executing 0'.*.
This leads to the followingfixed point rule, where the right-hand side is defined
in terms of the left-hand side.
Finally, we have a rule that defines the semantics of test actions. The idea is that
action expression 'P? occurs between times u and v on path p if 'P is satisfied on
p at time u. This rule recursively makes use of the definition of whether or not
a formula is satisfied; in practice, the interpretation against which the formula
CORA Defined 81
Next, we introduce the existential path quantifier, "E", which is defined as the
dual of the universal path quantifier "A". Thus a formula Erp is interpreted as
"on some path, rp," or "optionally, rp":
� trueU 'P
"" O...,rp
(rpU'lj;) V D rp .
82 Chapter 4
Thus cp W 'lj; means that either: (i) cp is satisfied until 'lj; is satisfied; or else (ii) cp
is always satisfied. It is said to be weak because it does not require that 'lj; be
eventually satisfied.
CORA provides us with the ability to use simple set theory to relate the
properties of agents and groups of agents. The operators � and c relate groups
together, and have the obvious set-theoretic interpretation; (Singleton g i)
means g is a singleton group with i as the only member; (Singleton g) simply
means g is a singleton.
�
(g � g') Vi· (i E g) :::} (i E g')
�
(g C g') (g � g') A -,(g = g')
�
(Singleton g i) Vj· (j E g) :::} (j = i)
�
(Singleton g) :3i· (Singleton g i)
Derived Operators for Reasoning about Actions
We will abuse notation a little by writing (Agt a i) to mean that i is the only
agent required to perform action a.
If you are familiar with dynamic logic, you will recognize that (Poss a cp)
corresponds approximately to (a)cp. Similarly, we can capture the dynamic
logic [a]cp through the Nee operator.
Thus ( Nee a cp) simply means that on all paths where a occurs, cp is true
immediately after a. However, ( Nee a cp) does not imply that a occurs on any
path - it simply says that if it does, then cp follows.
The (Aehvs a cp) operator is defined as a combination of Nee and Poss.
(Aehvs a cp) means that a does indeed happen on some path, and after a
CORA Defined 83
After introducing a new logic by means of its syntax and semantics, it is usual
to illustrate the properties of the logic by means of a Hilbert-style axiom
system. However, no complete axiomatization is currently known for eTL * ,
the branching temporal logic that underpins CORA. 1 Completeness proofs for
temporal modal logics, even in the propositional case, are relatively few and far
between [54, p.307]. For these reasons, I stay primarily at the semantic level,
dealing with valid formulae, rather than attempt a traditional axiomatization.
We use conventional definitions of validity and satisfiability, complicated
slightly by the fact that we have essentially two languages, for path and state
formulae.
Formally, a path formula<p is said to be satisjiableifffor some (M, V, w,p),
we have (M, V, w,p) FP <p; it is said to be valid iff for all (M, V, w,p), we
have (M, V, w,p) FP <po We indicate that <p is a valid path formula by writing
Similarly, the state formula <p is said to be satisfiable iff for some (M, V, w,t) ,
we have (M, V, w,t) FS <p; it is said to be valid iff for all (M, V, w,t) , we have
(M, V, w,t) FS <po We indicate that <p is a valid state formula by writing
FS <P
It is easy to see that state formula validity implies path formula validity.
Proof State formulae are also path formulae, and the semantic rules for
evaluating them are identical. _
1 Proving completeness for an axiomatization of CTL * has been a major open problem in temporal
logic since the logic was first formulated in the mid-1980s. Stirling reported an axiomatization
in [227], though it subsequently transpired that the completeness proof contained a bug. Mark
Reynolds from Murdoch University in Australia reported a complete axiomatization in 1998,
though at the time of writing, the work was still under review. To find out more, I urge you to
contact Mark directly.
84 Chapter 4
This Lemma means that certain formulae will be valid by virtue of their shape,
irrespective of whether or not they are actually path formulae or state formulae.
For example, presented with a formula 'l/J that has the shapecp V -'cp, we do not
need to worry about whether 'l/J is a path formula or a state formula: whichever
it is, we know it will be valid. To indicate that a formula cp is valid in this
regard, we writeF cpo
We can establish a similar result with respect to satisfiability.
THEOREM 4.1:
Proof For (1), simply observe that the semantics of the propositional connec
tives "-," and "V" are identical to classical logic. Similarly, for (2) - which
is simply modus ponens - the reasoning is identical to classical propositional
or first-order logic. •
CORA also has the properties one would expect of a sorted first-order logic.
We use the normal form cp(x ) to mean that the variable x isfree in cp, where
"free" has its standard interpretation. Additionally, cp[x /y] is used to denote the
formula obtained from cp by systematically replacing every occurrence of yin
cp by x (i.e., normal first-order substitution - see, e.g., [52, pp.104-106]).
THEOREM 4.2:
1. F Vx ·cp(x ) => cp[T/X] (whereTis a term that does not occur free incp, x and
Tare the same sort, andcp does not contain any modal or temporal connectives).
2. F (T = T).
3. F (T = T' ) => (cp => cp[T' /TD (where T' does not occur in the scope of
any modal or temporal operator in cp).
tion. (2) and (3) follow immediately from the semantics of equality. _
Next, we tum to the belief operator, Bel. This is essentially a normal modal
necessity connective, with semantics given via a serial, Euclidean, and transi
tive accessibility relation [31]. Thus the logic of Bel corresponds to the well
known normal modal system "weak-S5," or KD45. Although the proofs for
Theorem 4.3 are readily available in the literature, they are included here for
completeness; see the further reading section for references.
THEOREM 4.3:
Proof For (1), suppose (M, V,w,t) F S (Bel i ('P:::} 'I/J)) and (M, V,w,t) F S
(Bel i 'P) for arbitrary (M, V,w,t). From the semantics of Bel, we know
that (M, V,w',t) F S 'P :::} 'I/J and (M, V,w',t) F S 'P for all w' such that
w' E B�([i]). Hence (M, V,w',t) F S 'I/J, and so (M, V,w,t) F S (Bel i 'I/J).
For (2), suppose not. Then for some (M, V,w,t) we have both (M, V,w,t) F S
(Bel i 'P) and (M, V,w,t) F S (Bel i ""'P). Since the belief accessibility
relation is serial, we know there will be at least one w' E Br([i]), and
from the semantics of Bel, we therefore know that (M, V,w',t) F S 'P and
(M, V,w',t) F S ""'P, hence (M, V,w',t) F S 'P and (M, V,w',t) �s 'P,
which is a contradiction. For (3), assume (M, V,w,t) F S (Bel i 'P) for ar
bitrary (M, V,w,t). We need to show that (M, V,w,t) F S (Bel i (Bel i 'P)),
which by the semantics of Bel amounts to showing that (M, V,w',t) F S
(Bel i 'P) for all w' E Br([i]), which in tum amounts to showing that
(M, V,w",t) F S (Bel i 'P) for all w" E B�'([i]). But since the belief ac
cessibility relation is transitive, if w' E Br([i]), and w" E B( ([i]), then
w" E Br([i]), and since (M, V,w,t) F S (Bel i 'P), then by the semantics
of Bel, we have (M, V,w",t) F S (Bel i 'P), and we are done. For (4), sup
pose (M, V,w,t) F S ..., (Bel i 'P). Then for some w' E Br([i]), we have
(M, V,w',t) F S ""'P. Now, consider any world w" E Br([i]). The belief ac
cessibility relation is Euclidean, and so since w' E Br([i]) and w" E Br([i])
we have w' E B( ([i]). Hence (M, V,w",t) F S ""'P, and since w" was ar-
86 Chapter 4
bitrary, we therefore have (M, V,w,t) F S (Bel i -,(Bel i cp)). For (5), as
sume that F S cp. We need to show that (M, V,w,t) F S (Bel i cp) for all
(M, V,w,t). But since F S cp, then by definition cp is satisfied by all interpre
tation structures, and in particular, (M, V,w',t) F S cp for all w' E Br([ i ]).
Hence (M, V,w,t) F S (Bel i cp). •
Note that (1) in Theorem 4.3 is usually known as the "K" axiom; (2) is known
as the "D" axiom; (3) as the "4" axiom, and (4) as the "5" axiom. Property
(5) is known as beliefnecessitation.
The Des and Int connectives have a logic that corresponds to the normal
modal system KD. (The proofs are identical to those of Theorem 4.3, and are
therefore omitted.)
THEOREM 4.4:
THEOREM 4.5:
Assume (M, V,w,t) F S Ecp for arbitrary (M, V,w,t). Then by the semantics
of E, we know that (M, V,w,p) F P cp for some p E paths(w) such that
CORA Defined 87
Assume (M, V,w,t) FS A<p for arbitrary (M, V,w,t). Then by the semantics
of A, we know that (M, V,w,p) FP <p for allp E paths(w) such thatp(O) = t.
Since the branching time relation is total, we know there is at least one such
path, and so we have (M, V,w,t) FS <po
The universal path quantifier A also behaves rather like a normal modal
necessity connective with logic S5.
THEOREM 4.7:
Proof For (1), assume (M, V,w,t) FS A(<p ::::} 'l/J) and (M, V,w,t) FS A<p
for arbitrary (M, V,w,t). Then (M, V,w,p) FP <p::::} 'l/J and (M, V,w,p) FP
<p for all p E paths(w) such that p(O) = t. Hence (M, V,w,p) FP 'l/J for
all p E paths(w) such that p(O) = t, and so (M, V,w,t) FS A('l/J) and we
are done. For (2), assume (M, V,w,t) FS A<p and (M, V,w,t) FS A-,<p for
arbitrary (M, V,w,t). Then from the semantics of A, we have (M, V,w,p) FP
<p and (M, V,w,p) FP -,<p for all p E paths(w) such that p(O) = t.
(Since the branching time relation is total, we know there will be at least
one such path.) Hence both (M, V,w,p) FP <p and (M, V,w,p) �p -'<p,
which is a contradiction. For (3), simply observe that this is one implication
of Theorem 4.6 (see above). For (4), assume (M, V,w,t) FS A<p for arbitrary
(M, V,w,t). We need to show that (M, V,w,t) FS AA<p. Since A<p is a state
formula, we know from Theorem 4.6 that FS A<p ¢:} AA<p, and so we have
(M, V,w,t) FS AA<p and we are done. For (5), assume (M, V,w,t) FS -,A<p.
88 Chapter 4
Then by definition, (M, V,w,t) FS E.<p. Hence from Theorem 4.6, we have
(M, V,w,t) FS A E.<p, and so (M, V,w,t) FS A.A<p. Finally, (6) is just a
version of necessitation, for which we have already seen proofs. _
THEOREM 4.8:
Proof For (1), assume (M, V,w,p) F'P (Happens a; a') for arbitrary
(M, V,w,p). Then by the semantics of Happens, we have some u,v E IN
such that occurs(a,p, 0, v ) and occurs(a',p,u,v ) . Hence (M, V,w,p) F'P
(Happens a; (Happens 0:')7), and we are done. For (2), start by assuming
(M, V,w,p) F'P (Happens alo:'). Then by the semantics of Happens, we
must have either occurs(a,p, 0, u) for some u E IN or else occurs(0:',p, 0, u)
for some u E IN. Hence by the semantics of V and Happens, we have
(M, V,w,p) F'P (Happens a)V(Happens a'). For (3), assume (M, V,w,p) F'P
(Happens <p7). Hence we have (M, V,w,p(O)) F'P <p, and since <p must be
a state formula, we have (M, V,w,p(O)) FS <p and so (M, V,w,p) F'P <p.
Part (4) follows trivially from the semantics of iteration: any action happens
zero or more times. For (5), observe that time is a total branching time rela
tion; hence there must be a path emerging from any situation, and the arcs that
make up this path will be labeled with actions. (Part (5) can also be Seen to be
implied by (4).) _
The fourth part of this Theorem may seem slightly strange; it makes sense
when one reads it as "every action occurs zero or more times."
CORA Defined 89
Preliminary proof methods for temporal logics of knowledge and belief are
described in [246, 47, 244]. With respect to 8DI logics, Rao reported proof
methods for linear-time 8DI logics in [184] and Rao and Georgeff reported
proof methods for branching time 8DI logic (where the branching temporal
component was restricted to CIL logic, rather than CIL*) in [185]. Klaus
Schild demonstrated that 8DI logic could be encoded in the J.l-calculus, and
established an exponential time upper bound on the satisfiability problem for
(cIL-based) propositional 8DI logic [200].
5 Properties of Rational Agents
In this chapter, we will see how CORA can be used to capture various
desirable (and undesirable) properties of rational agents. The chapter focuses in
particular on the possible interrelationships among the mental states of beliefs,
desires, and intentions. This study has two aspects:
various types of rational agents in terms of formulae of CORA, and discuss the
extent to which these formulae adequately capture our intuitive understanding
of the concepts in question. For example, we might ask whether the formula
schema (Inti 'P) => (Bel i E<>'P) (ifi intends 'P, theni believes 'P is possible)
is an appropriate characterization of the relationship between intentions and
beliefs.
• A pu relylog i cal aspect, whereby we investigate the possible interrelation
ships among beliefs, desires, and intentions from an abstract mathematical per
spective. With such a perspective, we simply view CORA as a formal system
that has certain properties.We pay little or no attention to the question of what
these properties mightmean. A classic question to ask in such a logical study
would be "what formula characterizes this interrelationship between these ac
cessibility relations."
It goes without saying that CORA will not be able to capture every nuance of
the mental states under discussion. Belief, desire, and intention are in reality
far too subtle, intricate, and fuzzy to be completely captured in a logic like
CORA. If such a theory was our goal, then the formalism would fail to satisfy
it. However, the logic is emphaticallynot intended to serve as such a theory.
Indeed, it seems certain that any formal theory which did fully capture all
nuances of belief, desire, and intention in humans would be of curiosity value
only: it would in all likelihood be too complex and involved to be of much use
for anything, let alone for actually building artificial agents. Instead of serving
as a "complete" theory of rational agency, therefore, the analysis in this chapter
is intended to investigate the properties that anidealized rational agent might
exhibit.
It is also worth noting that we are unable to answer many important
questions that deserve to be answered about the abstract properties of our logic.
In particular, complete axiomatizations - a rite of passage for any logic -
are not considered. The state of the art in multimodal logics is not sufficiently
92 Chapter 5
Correspondence theory is perhaps the main reason for the success of Kripke
style possible worlds semantics for modal logic [31]. Correspondence theory
investigates the relationships between properties of the accessibility relations
in Kripke models for modal logic, and axioms of the corresponding logic.
Most results take the form "formula schema 'P is valid in a model M iff the
accessibility relation R in M has property P." For example, in normal modal
logic, it is well-known that the formula schema
is valid in a model iff the accessibility relation R that is used to give a semantics
to the "0" connective is reflexive (see, e.g., [31, p.80]).We can draw upon this
work to establish some basic properties of CORA - indeed, we already did
so, in the preceding chapter, to establish properties of the belief, desire, and
Properties of Rational Agents 93
intention modalities.
For CORA, however, we can extend the usual correspondence results
in several ways. Most obviously, we have available to us not just one, but
three modalities - Bel , Des, and Int . Multimodal logics were not widely
studied in classical correspondence theory, although given their importance in
contemporary computer science, they are studied increasingly often [29, 139].
Also, classical correspondence results assume that the worlds over which
accessibility relations operate have no internal structure. For CORA, however,
this is not the case: worlds are themselves branching time structures. Because
of this, we can investigate st ru ctu ral correspondence results, which in addi
tion to incorporating interrelationships between the accessibility relations that
characterize the modal connectives, also incorporate structural properties of
worlds.
Subworlds
The most obvious structural relationship that can exist between two worlds
- and the most important for our purposes - is that of one world being a
sub wo rld of another. Intuitively, a world w is said to be a subworld of world
w' if w has the same structure as w' but has fewer paths. Formally, if w,w'
are worlds, then w is a subworld of w' iff paths ( w) � paths ( w'). If w is a
subworld ofw', then we indicate this by writingw�w'. The subworld relation
is illustrated in Figure 5.l.
It is not hard to see that ifw�w', then any A-formula that is true inw' will
also be true inw. Similarly, any E-formula that is true inw must also be true in
w'. These two facts tum out to be very useful in the analysis that follows, and
so we prove them in the following lemmas.
w � w' then p E paths ( w'). Hence (M,V,w',p) F'P cp, and since p(O) t, =
vv
vv'
vv"
("no",,")
Figure 5.1
' ' " '
The suhworld relationship: w is a suhworld of world w, that is, w � w; similarly, w � w.
(M,V, w', p) FP cp, for all p E paths ( w/) such that p (O) t, and so from the
=
THEOREM 5.1: Suppose M and IVI are two of the modal connectives Bel ,
Des , and Int such that M ¥- lVI, defined by accessibility relations R and R
respectively. Then if we have some model in which R ([i]) � R ([i]), then
(Mi cp) :::} (IVI i cp) is valid in that model.
P roof Assume R ([i]) � R ([i]), and (M,V, w,t) FS (M i cp) for arbitrary
(M,V, w,t). We need to show that (M,V, w,t) FS (IVI i cp). From the seman
tics of M, we know that (M,V, w',t) FS cp for all w' E R7 ([i]). Now since
R7 ([i]) � R7 ([i]), then (M,V, w",t) FS cp for all w" E W such that w" E
R7 ([i]). Hence from the semantics for lVI, we have (M,V, w,t) FS (IVI i cp)
and we are done. _
THEOREM 5.2: Suppose M and IVI are two of the modal connectives Bel ,
Des , and Int such that M ¥- lVI, defined by accessibility relations R and R
respectively. Then if we have some model in which R ([i]) =R ([i]), then
) )
(Mi cp ¢:} (IVI i cp is valid in that model.
P roof Observe that R ([i]) R ([i]) iff both R ([i]) � R ([i]) and R ([i])
= C
R ([i]). The result follows immediately from Theorem 5.1. _
96 Chapter 5
THEOREM 5.3: Suppose M andM are two of the modal connectives Bel ,
Des, and Int such that M "# M, defined by accessibility relations R and R
respectively, such that R7([i]) �sub R7([i]). Then for any A-formula A <p
( ),
we have M( i A <p
( )) => (M i A <p
( )) is valid in that model.
P roof If R7([i]) �sub R7([i]), then for every w' E R7([i]), there is some
"
w E R7([i]) such that w' � w". Now assume (M,V, w,t) FS M ( ( ))
i A <p
( )) for some (M,V, w,t). Then there must be
and (M,V, w,t) FS ...., (M i A <p
some w' E R7([i]) such that(M,V, w',t) FS ...., A <p
( ). But since R �sub R, then
" ' "
there is some w E R7([i]) such that w � w . Now since (M,V, w,t) FS
"
M
( ( )) then from the semantics ofM, it follows that (M,V, w ,t) FS
i A <p
'
( ) and thus by Lemma 5.2, (M,V, w ,t) FS A <p
A <p ( ). This is a contradiction,
so the assumption must be false. _
w'
, ?
----------- -
-
-
,
,
,
,
,
,
" -
- p
Figure 5.2
Illustrating structural subset/superset relationships: desire is a structural subset of belief
(D �sllb 8) and conversely, belief is a structural superset of desire (8 �SIIp D).
THEOREM 5.4: Suppose M and IVI are two of the modal connectives Bel ,
Des , and Int such that M ¥- lVI, defined by accessibility relations Rand R
respectively, such that R c;;,sup R. Then for any E-formula E('P) , we have
(IVI i E('P) ) => (M i E('P) ) is valid in that model.
Intersection-style Correspondences
This formula schema is an instance of the "D" axiom from normal modal
logic, which corresponds to the accessibility relation being serial [31, p.80].
It is usually understood as expressing the consistency of belief. If we tum our
attention to the multimodal setting of .cORA, then we can consider related
schemas, which capture consistencybet ween modalities. These axiom schemas
have the following general form.
It turns out that these schemas are captured by theinte rse ction of the respective
accessibility relations being non-empty.
THEOREM 5.5: Suppose M and rill are two of the modal connectives Bel ,
Des, and Int such that M "I- rill, defined by accessibility relations R and R
respectively. Then if we have some model in which R7 ([i]) n R7 ([i]) "I- 0,
then (M i 'P) ::::} -, (rill i -''P) is valid in that model, as is the contrapositive
(rilli 'P) ::::} -,(M h'P) .
P roof I only prove that (M i 'P) ::::} -, (rill i 'P) is valid; once we have
this, showing that (rill i 'P) ::::} -, (M i 'P) is valid is trivial (it is simply the
contrapositive). Start by assuming R7 ([i]) n R7 ([i]) "I- 0, and (M, V, w,t) FS
(Mi 'P) for arbitrary (M, V, w,t). Then for all worlds w' E R7 ([i]), we have
(M, V, w',t) FS 'P. We need to show that (M, V, w,t) FS -, ( riII i -''P) . So
assume the contrary, i.e., that (M, V, w,t) FS (rill i -''P) . Then for all worlds
w" E R7 ([i]), we have (M, V, w",t) FS -''P. But since R7 ([i]) n R7 ([i]) "I- 0,
then for some Will E W, such that Will E R7 ([i]) and Will E R7 ([i]), we
must have both (M, V, Will,t) FS 'P and (M, V, Will,t) FS -''P. This is a
contradiction, so the assumption must be false. _
B� ([i]) nsup 1J� ([i]) = 0. Formally, R7([i]) nsup R7([i]) is defined as follows.
R7([i]) nsup R7([i]) = {w' I w' E R7([i]) and3w" E R7([i]) s.t. w'� w"}
THEOREM 5.6: Suppose M and IVI are two of the modal connectives Bel ,
Des , and Int such that M "I- lVI, defined by accessibility relations R and R
respectively. Then if we have some model in which R7([i]) nsup R7([i]) "I- 0,
then (M i A( rp)) => ,(IVI hA(rp)) is valid in that model.
P roof Suppose not. Then for some(M,V, w,t) we have R7([i])nsupR7([i]) "I-
0, and (M,V, w,t) FS (M i A(rp)) and (M,V, w,t) FS (IVI i ,A(rp)). Now
since R7([i]) nsup R7([i]) "I- 0, there exists some w' E R7([i]) such that
there is some w" E R7([i]) where w' � w". Hence from the semantics of
M, we know (M,V, w",t) FS A(rp) and from the semantics of lVI, we know
(M,V, w',t) FS ,A(rp). But since w' � w", then from Lemma 5.2 we know
that (M,V, w',t) FS A(rp). This is a contradiction, so the assumption must be
false. _
R7 ([i]) nsub R7 ([i]) = {w' I w' E R7 ([i]) and3w" E R7([i]) s.t. w"� w'}
THEOREM 5.7: Suppose M and IVI are two of the modal connectives Bel ,
Des , and Int such that M "I- lVI, defined by accessibility relations R and R
respectively. Then if we have some model in which R7([i]) nsub R7([i]) "I- 0,
then (M i E(rp)) => ,(IVI i ,E(rp)) is valid in that model.
Table 5.1
Pairwise subset interrelationships between BD! modalities.
=?
Mi
( cp) Mi
( cp) (5.4)
{:::
Schema (5.5) says that if an agent intends something, then it desires it. Intu
itively, this schema makes sense for rational agents. If we return to the view
suggested in chapter 2, of desires as options, then (5.5) can be seen as a con
straint on the agent's deliberation process - an agent should only commit to
something as an intention if it considered it an option.
Schema (5.6) says that if an agent desires something, then it intends it. In
other words, an agent intends all its options. If we accept (5.5) as capturing
a property of rational agents, then if we also adopted (5.6), then desire and
intention would be equivalent. Formula (5.6) does not therefore appear to
capture any interesting properties of agents.
suppose I believe that the sun will definitely rise tomorrow. Then, one could
argue, it makes no sense for me to desire that the sun will not rise. For whatever
I do, the sun will indeed rise tomorrow. So I may as well accept this as a desire.
As a property of rational agents, realism seems too strong. Later in this chapter,
we see how a finer grained analysis of the interrelationships among beliefs,
desires, and intentions can lead to more reasonable types of realism.
Schema (5.8) says that if an agent desires something, then it believes it. To give
a concrete example, suppose I desire I am rich: should I then believe I am rich?
Clearly not.
Schema (5.9) says that if an agent intends something, then it believes it. Let us
make this example concrete. Suppose I have an intention to write a book; does
this imply I believe I will write it? One could argue that, in general, it is too
strong a requirement for a rational agent. For example, while I can envisage
many possible futures in which I proudly present my finished manuscript to a
grateful and generous publisher, I can envisage equally many others in which
this happy event does not take place. (The fact that you are reading this, of
course, suggests that I was successful in my intention.) For example, I might
win the lottery next week, in which case I would certainly reconsider my
intention to write a book. Alternatively, I might be run down by a speeding
bus, and so on. So while I certainly believe it is possible that I will succeed
in my intention to write the book, I do not believe it is inevitable that I will
do so. Bratman [20, p.31] argues that if an agent has an intention to do some
action, then it is rational of the agent to believe that it will achieve it, given
certain background conditions - he refers to this property asintention-belief
consistency.
Schema (5.10) says that if an agent believes something, then it intends it. Like
(5.7), this is a kind of realism property, although it should be immediately ap
parent that it expresses an even stronger, and arguably less desirable property.
To return to the example above, suppose that I believe that'P is true: should
I then adopt'P as an intention? Clearly not. This would imply that I would
choose and commit to everything that I believed was true. Intending some-
102 Chapter 5
Table 5.2
Pairwise structural subset interrelationships.
Attitudes to Inevitabilities
The six possible interaction schemas implied by Theorem 5.3 are summarized
in Table 5.2. Consider first (5.12).
(Inti A 'P
( )) =? (Desi A 'P))
( (5.12)
This says that if an agent intends that'P is inevitably true, then it desires that'P
is inevitably true. This schema, a variant of (5.5), is obviously an appropriate
property to demand of rational agents.
(Desi A 'P
( )) =? (Inti A 'P))
( (5.13)
Properties of Rational Agents 103
Schema (5.13) says that if an agent desires thatcp is inevitably true, then it
intends thatcp is inevitably true. In other words,cp is inevitable in all the options
considered by the agent. For example, suppose that in all the options that I
consider, it is inevitable that I am married. Then arguably, I should adopt an
intention to become inevitably married. So schema (5.13) seems to capture a
reasonable property of rational agents.
(Bel i A cp
( )) :::} ( ))
(Des i A cp (5.14)
(Des i A cp
( )) :::} ( ))
(Bel i A cp (5.15)
Schema (5.15) says that if an agent desires something is inevitably true, then
it believes it is inevitably true. To be concrete, suppose that in all the options
I consider, it is inevitable that I am married. Do I then believe I am inevitably
married? No. I may well believe there is some future in which I am not married,
even though in all the options I consider, it is inevitable that I am married.
(Int i A cp
( )) :::} ( ))
(Bel i A cp (5.16)
Schema (5.16) says that if an agent intends thatcp is inevitably true, then it
believes it is inevitably true. As we noted earlier, Bratman argues that intending
cp certainly provides some support for the belief thatcp [20, p.38]. Since
intentions are in some SenSe conduct-controlling, then all other things being
equal, my intention to achievecp must makecp more likely than it would be if I
did not intendcpo However, this is not to say that my intendingcp is inevitable
implies I believecp is inevitable. So while (5.16) is arguably more reasonable
than (5.9), it is still too strong to be a necessary property of rational agents.
(Bel i A cp
( )) :::} (Int i A cp
( )) (5.17)
Schema (5.17) says that if an agent believescp is inevitably true, then it intends
it is inevitably true. For the same reasons as (5.10), we reject this schema as a
property of rational agents.
104 Chapter 5
Table 5.3
Pairwise structural superset interrelationships between modalities.
Attitudes to Options
=?
(Mi E cp
( )) M
( i E cp
( )) (5.18)
{:::
As with Theorem 5.1, Theorem 5.4 immediately gives us six possible interac
tions, summarized in Table 5.3.
Consider first (5.19).
(Inti E cp
( )) =? (Desi E cp
( )) (5.19)
(Desi E cp
( )) =? (Inti E cp
( )) (5.20)
Properties of Rational Agents 105
Schema (5.20) says that if an agent desires that<p is true on at least one
future, then it intends that<p is true on at least one future. This formula can
be understood as characterizing an agent who wants to commit to all options;
in other words, an agent who will never rule out options. Such a property
might make sense in some situations. For example, suppose I have decided
what my options are, but have insufficient information to make an informed
choice among my options.
( ))
(Bel i E <p :::} ( ))
(Des i E <p (5.21)
Schema (5.21) says that if an agent believes<p is true on at least one future, then
it desires it is true on at least one future. This schema can be seen as character
izing a weaker variant of the realism property (5.7) from the preceding section.
However, it still seems in some sense too strong. For example, suppose I be
lieve there is some future in which there will be a nuclear war. Do I also desire
that there is some future in which there is a nuclear war? Clearly not. So, like
the realism schemas (5.7) and (5.10), we reject (5.21) as a desirable property
of rational agents.
( ))
(Des i E <p :::} ( ))
(Bel i E <p (5.22)
Schema (5.22) says that if an agent desires something is optionally true, then
it believes it is optionally true. This formula is a variant of (5.8). However,
unlike (5.8), schema (5.22) seems an entirely reasonable property for rational
agents. For if I desired that I was rich in some future, while not believing that
there was any possible future in which I was rich, then I would clearly be
irrational.
( ))
(Int i E <p :::} ( ))
(Bel i E <p (5.23)
Schema (5.23) says that if an agent intends that<p is optionally true, then it
believes it is optionally true. For similar reasons to (5.22), this schema is a
reasonable property of rational agents.
( ))
(Bel i E <p :::} ( ))
(Int i E <p (5.24)
Schema (5.24) says that if an agent believes<p is optionally true, then it intends
it is optionally true. As with (5.21), this is not a property we would demand of
rational agents.
106 Chapter 5
Table 5.4
Weak realism interactions.
Relationship Formula Schemas
W([i]) n1:;"([i]) i-0 (Int icp) => ,(Des i ,cp)
1:;"([i]) n W([i]) i-0 (Des icp) => ,(Int i ,cp)
B;"([i]) n W([i]) i-0 (Bel icp) => ,(Des i ,cp)
W([i]) nB7([i]) i-0 (Des icp) => ,(Bel i ,cp)
1:;"([i]) nB7([i]) i-0 (Int icp) => ,(Bel i ,cp)
B;"([i]) n1:;"([i]) i-0 (Bel icp) => ,(Int i ,cp)
We saw above that realism properties such as (Bel i r.p) => (Des i r.p) are in
general too strong to be regarded as reasonable properties of rational agents.
In this section we will consider some weaker realism properties.
As before, this general result enables a number of specific interaction
properties to be established - see Table 5.4.
The first of these properties, represented by schemas (5.25) and (5.26),
says that an agent's intentions are consistent with its desires, and conversely,
its desires are consistent with its intentions.
Strong realism, as discussed above, is the most general kind of realism that
we might consider. However, for the reasons we discussed above, most strong
types of realism are not acceptable properties of rational agents. In this and the
subsection that follows, we will discuss realism with respect toinevitable and
o ptional formulae.
Theorem 5.6 generates the results shown in Table 5.5.
The first of these properties, (5.31), says that if an agent intends to bring
about A rp ( ); schema (5.32) expresses the
( ), then it should not desire that..., A rp
same property for desires and intentions.
(Inti A rp
( )) => ...,(Desi..., A rp
( )) (5.31)
108 Chapter 5
Table 5.5
Inevitabilities and weak realism properties.
(Des i A 'P))
( :::} ,(Int i , A 'P
( )) (5.32)
Schema (5.33) says that if an agent believes'P is inevitable, then it should not
desire it is not inevitable. This captures an acceptable realism property.
(Bel i A 'P))
( :::} ,(Des i , A 'P
( )) (5.33)
(Des i A 'P))
( :::} ,(Bel i , A 'P
( )) (5.34)
Finally, schemas (5.35) and (5.36) capture weak realism between intentions
and beliefs.
(Int i A 'P))
( :::} ,(Bel i , A 'P
( )) (5.35)
(Bel i A 'P))
( :::} ,(Int i , A 'P
( )) (5.36)
(
(Int i E 'P)) :::} ( ))
,(Des i , E 'P (5.37)
Properties of Rational Agents 109
Table 5.6
Options and weak realism properties.
Schema (5.38) says that if an agent desires thatcp is optional, then it does
not intend thatcp is not optional.
(Desi E cp
( )) ::::} -,(Inti -,E cp
( )) (5.38)
Schema (5.39) says that if an agent believescp is optional, it does not desire
thatcp is not optional.
(Beli E cp
( )) ::::} -,(Desi -,E cp
( )) (5.39)
Schema (5.39) says that if an agent desires thatcp is optional, then it does not
believecp is optional. Earlier, we argued that schema (5.7), which said that if
an agent believes something it also desires it, was unacceptably strong for most
agents. Schema (5.39), which can be seen as a weak variant of (5.7), is clearly
more acceptable, as is (5.40).
(Desi E cp
( )) ::::} -,(Bel i -,E cp
( )) (5.40)
Schemas (5.41) and (5.42) say that an agent's optional intentions are consistent
with its beliefs, and as with the desire case, above, these schemas are clearly
more acceptable than either (5.9) or (5.10).
(Inti E cp
( )) ::::} -,(Bel i -,E cp
( )) (5.41)
(Bel i E cp
( )) ::::} -,(Inti -,E cp
( )) (5.42)
So far, we have only been concerned with binary relationships between modal
ities. But we can also consider ternary (i.e., three-way) relationships between
the modalities. Given the number of different binary relationships we have
1 10 Chapter 5
Table 5.7
Systems OfBOI logic. (Source: [185, p.321].)
looked at so far, there are clearly a great many ternary relationships that we
might possibly consider. However, most of these relationships are meaning
less (or at best capture obscure and frankly uninteresting situations). The most
important relationships for our purposes are those summarized in Table 5.7.
One of the most well-known problems in the theory of intention is that ofside
effe cts. The side-effect problem is illustrated by the following scenario.
Janine intends to visit the dentist in order to have a tooth pulled. She is aware that as a
consequence of having a tooth pulled, she will suffer pain. Does Janine intend to suffer
pain?
In this example, suffering pain is a side effect of having a tooth pulled; having
a tooth pulled and suffering pain come as a "package deal." However, it is
generally agreed (and in particular, Bratman convincingly argues [20, p.142]),
that rational agentsdo not have to intend the consequences of their intentions.
In other words, Janine can intend to have a tooth pulled, believing that this will
cause pain, without intending to suffer pain.
Properties of Rational Agents 111
We can prove the following general result about such consequential closure
schemas.
THEOREM 5.8: Suppose M and !VI are two of the modal connectives Bel ,
Des , and Int such that M -I- !VI, defined by accessibility relations R and R
respectively. Then if we have some model in which R ([i]) � R ([i]), then the
schema
P roof Assume (M,V, w,t) FS (Mi cp) 1\ (!VI i cp =>'lj;) for some arbitrary
(M,V, w,t). If R ([i]) � R ([i]), then by Theorem 5.1, the schema (!VI i X) =>
(Mi X) will be valid. Hence (M,V, w,t) FS (Mi cp =>'lj;). By the K axiom
for the M operator and propositional reasoning, (M,V, w,t) FS (Mi'lj;). This
contradicts the assumption. _
dence theory accounts in a large part for the continued success of this style of
semantics. Basic correspondence results are described in [101] and [31].
The study of interactions among multimodallogics, of the kind we under
take in this chapter, is a relatively recent development. Laurent Catach's Ph.D.
work, summarized in [29], was one of the first systematic, abstract studies to
receive a wide audience. Catach established a correspondence theorem analo
gous to the general d,l,m,n correspondence result of normal modal logic [31,
p.88]. More recently, multimodal logics have been found to have a wide variety
of applications, and this recognition has led to a rapid increase in the number
of systematic studies of multimodal systems. Logical systems with multiple
modalities of the same time are discussed in [54]. Alessio Lomuscio gives a
comprehensive study of interaction schemas in multimodal settings, generaliz
ing Catach's results [139, 140].
The specific properties discussed in this chapter were originally identified
in Rao and Georgeff's BDI papers. The paper that "introduced" BDI logics
is [187] - it showed how BDI logic could be used to capture many of our
intuitions about intentions, with particular reference to the work of Cohen and
Levesque [35]. Axiomatizations of the asymmetry thesis, and a justification
for the temporal branching structure of BDI logic were presented in [186].
The "definitive" paper on Rao and Georgeff's formalism is [185]. This paper
comprehensively studies possible axiomatizations ofBDI logic, and gives some
completeness results for propositionalBDI logic by means of semantic tableaux
systems.
6 Collective Mental States
(Bel me 'P)
In addition, however, since the act of me uttering the sentence was immediately
visible to both of us, and both of us were witness to the fact that both of us were
witness to it, it is only rational for me to believe that you believe 'P.
The situation is of course symmetric, so you will also believe that I believe 'P.
It is not hard to see that, if we both assume that the other observed the event,
then one must carry on this nesting of beliefs.
(Bel me (Bel you (Bel mecp) ) )
(Bel you (Bel me (Bel youcp) ) )
(Bel me (Bel you (Bel me (Bel youcp) ) ) )
(Bel you (Bel me (Bel you (Bel mecp) ) ) )
(Bel me (Bel you (Bel me (Bel you (Bel mecp) ) ) ) )
(Bel you (Bel me (Bel you (Bel me (Bel youcp) ) ) ) )
... and so on.
We refer to this state of affairs - where I believe, you believe, I believe that
you believe, you believe that I believe, I believe that you believe that I believe,
and so on - as mutual belief It follows that, in principle at least, mutual belief
is infinitary in nature. If we try to write down a formula that captures mutual
belief between two or more agents, then initially at least, it appears that this
formula must be infinitely long. (In fact, we will see that this is not necessarily
the case, as we can characterize mutual mental states in terms offixed points;
nevertheless, mutual beliefs are infinitary in nature.)
It is important to distinguish mutual belief from the (much simpler) case,
where we have simply I believe and you believe:
Mutual belief expresses a much stronger property, which implies this weaker
kind of collective mental state.
As the informal example given above illustrates, mutual mental states play
an important role in communication. But, more than this, they tum out to
be important in coordination problems. To illustrate what is meant by this,
consider the following scenario, from [54, p.176].
Two divisions of an army, each commanded by a general, are camped on two hilltops
overlooking a valley. In the valley awaits the enemy. It is clear that if both divisions
attack the enemy simultaneously they will win the battle, while if only one division at
tacks, it will be defeated. As a result, neither general will attack unless he is absolutely
sure that the other will attack with him. In particular, a general will not attack if he
receives no messages. The commanding general of the first division wishes to coordi
nate a simultaneous attack (at some time the next day). The generals can communicate
only by means of messengers. Normally, it takes a messenger one hour to get from one
encampment to the other. However, it is possible that he will get lost in the dark or,
worse yet, be captured by the enemy. Fortunately, on this particular night, everything
goes smoothly. How long will it take them to coordinate an attack?
Collective Mental States 115
Intuitively, the two generals are trying to bring about a state where it is
mutually believed (or known) between them that the message to attack was
delivered. Each successive round of communication, even if successful, only
adds one level to the depth of nested belief. No amount of communication
is sufficient to bring about the infinite nesting that mutual belief requires. As
it turns out, if communication delivery is not guaranteed, then mutual belief
can never arise in such a scenario. Ultimately, this is because, no matter how
many messages and acknowledgments are sent, at least one of the generals will
always be uncertain about whether or not the last message was received.
One might ask about whether irifinite nesting of mutual belief is required.
Could the two generals agree between themselves beforehand to attack after,
say, only two acknowledgments? Assuming that they could meet beforehand
to come to such an agreement, then this would be feasible. But the point is that
whoever sent the last acknowledgment would be uncertain as to whether this
was received, and would hence be attacking while unsure as to whether it was
a coordinated attack or a doomed solo effort.
More pragmatically, of course, it should be noted that - as with all the
formalizations of mental states that appear in this book - mutual belief and its
kin represent idealizations of true states of affairs. In all but the most unusual
of circumstances, humans are unlikely to make use of mental states that are
nested to a depth of more than a few levels.
In order to formally define mutual belief, we will make use of some
auxiliary definitions. First, we write (E-Bel g 'P) to represent the fact that
everyone in the group denoted by g believes 'P.
Vi· (i E g) =>
(Bel i <p)A
(Bel i (E-Bel g <p))A
(Bel i (E-Bel g (E-Bel g <p)))A
... and so on.
It turns out that there are several ways that we can characterize mutual belief.
We can adopt a model-theoretic approach, and characterize mutual belief
in terms of each agent's belief accessibility relation. Alternatively, we can
characterize mutual belief as afixed point.
THEOREM 6.1: (M, V, w,t) FS (E-Bd g <p) iff (M, V, w',t) FS <p for
'
every world w such that w' is B(g)-reachable from w in k steps.
(M, V, w', t) I=s cp for every world w'such that w'is B (g) -reachable from w
in m steps. We need to show that in this case, (M, V, w, t) I=s (E_Bel mH gcp)
iff (M, V, w', t) I=s cp for every world w'such that w'is B (g) -reachable from
w in m + 1 steps. This follows trivially from the definition of E-Bel and the
inductive assumption. _
We will also say that w'is B (g) -reachable from (w, t) if w'is B (g) -reachable
from (w, t) in k steps, for some k E IN such that k > O. We can then prove the
following.
THEOREM 6.2: (M, V, w, t) I=s (M-Bel g cp) iff (M, V, w', t) I=s cp for
every world w'such that w'is B (g) -reachable from w.
Proof Follows immediately from Theorem 6.1 and the definition of M-Bel . _
Theorems 6.1 and 6.2 characterize E-Bel k and M-Bel graph theoretically,
where each agent's accessibility relation is interpreted as a graph over possible
worlds.
x = f(x)
Fixed-point equations like this often cause confusion, because they appear to
be in some sense circular - the left-hand side appears to be defined in terms
of the right. But such equations can have quite natural solutions. For example,
the equation x = x2 has solutions x = 0 and x = 1. The following Theorem
tells us that mutual belief can be understood as a fixed point.
THEOREM 6.3: I=s (M-Bel gcp) ¢:} (E-Bel gcp /\ (M-Bel gcp) ) .
Proof For the left to right implication, assume (M, V, w, t) I=s (M-Bel gcp) .
We need to show that this implies (M, V, w, t) I=s (E-Bel gcp/\ (M-Bel gcp) ) .
From Theorem 6.2, we know that (M, V, w', t) I=s cp for each w'that is B (g)
reachable from w. Now consider an arbitrary w" E B7(i) for some i E g.
Then w" is B (g) -reachable from w in one step, thus (M, V, w", t) I=s cpo It
118 Chapter 6
This Theorem tells us that (M-Bel g <p) can be understood as a fixed point of
the function
f (x ) = (E-Bel g<pA x)
THEOREM 6.4:
Proof Parts (1) and (4) are trivial; for (2) and (3), notice that the B(g)
reachability relation will be serial and transitive. (See e.g., [54, p.34].) _
In the remainder of the book, I will assume that M-Int (mutual intention) and
M-Des (mutual desire) have been defined in an analogous way to M-Bel .
scenarios. In this section, we will consider the types of mutual mental states
that characterize real-world joint working scenarios, and in particular, the type
of mental states that characterize an agent engaged in teamwork. By teamwork,
we mean scenarios such as the following, where a group of agents work
together [133, 37, 250]:
What sort of mental state characterizes such cooperative efforts? One possi
bility would be to argue that there was a "team state" that was not reducible
to the individual beliefs, desires, and intentions of the participating agents. We
could easily formalize such a concept, by introducing (yet) another primitive
modal operator to represent team mental states, and then investigate its prop
erties using the same techniques employed throughout this book. The problem
is that intuition rejects such an approach. It seems almost superstitious to ar
gue that there is something about team action that exists independently of the
team members. I therefore adopt a reductionist approach, where teamwork is
analyzed in terms of the individual mental states of team members.
As a first attempt at defining team mental states, we might imagine that it
is sufficient for a team to have (say) a mutual intention (M-Int) towards some
particular goal. Suppose we have two agents i and 1 cooperatively working to
achieve some state of affairs <po Then (M-Int {i,l} <p)would expand to
heavy object, it seems reasonable that I intend to lift it, and I intend that you
intend to lift it, and I intend that you intend that I intend to lift it, and so on.
But is there more to cooperative action than this? Levesque, Cohen, and Nunes
argue that such models of mutual intention fail to capture some important
characteristics of teamwork [133, 37]. In particular, they fail to capture the
notion of joint commitment. To continue with the example of lifting a heavy
object, suppose that while we are lifting it I come to believe that we will be
unable to lift it for some reason. As we saw in chapter 5, a rational agent acting
alone in such circumstances would drop the intention: it would be irrational
for an agent to act towards an intention that was believed to be impossible.
But in the teamwork case, should I simply drop my intention to lift the object
with you, because I believe it is not achievable? You would hardly be inclined
to say I was "cooperative" if I did so. What appears to be missing is that
associated with team action is what Jennings calls responsibility toward the
team [104, 105, 106]. Responsibility in the context of teamwork is comprised
of two parts: a commitment and a convention.
A commitment is a pledge or promise that an agent makes to the group in
which it is working. A commitment must, by definition, persist over time [35,
pp.217-219].
A convention is a means of monitoring a commitment. A convention thus
specifies the circumstances under which a commitment can be abandoned
and how an agent should behave both locally and towards others when one
of these conditions arises [105]. Thus a convention identifies the conditions
under which the joint commitment can be dropped, and also describes how the
agent should behave towards its fellow team members. For example, if an agent
drops its joint commitment because it believes that the intention will never be
attained, then it is part of the notion of "cooperativeness" that it informs fellow
team members of this. Conventions thus provide a commonly understood
frame of reference in which agents can work. By adopting a convention, every
agent knows what is expected both of it, and of every other agent, as part of
the collective working towards the intention, and knows that every other agent
has a similar set of expectations. By adopting a particular convention, team
behavior becomes more predictable. Predictability is one of the most important
enablers of coordinated behavior [18].
We can formalize conventions quite simply. A convention is a set of rules,
where each rule r = (p, 'Y) is a pair consisting of a re-evaluation condition p
and an associated goal 'Y. A convention will be adopted by a group of agents g
when working towards some goal 'P. The idea is that if ever an agent i E g
Collective Mental States 121
believes p to be true, then it must adopt 'Y as an intention, and keep this
intention until the commitment becomes redundant.
Formally, a convention, c, is a finite indexed set of pairs:
where the termination condition is that one of the goal parts of the convention
rules is satisfied.
More formally, if
where
Xl � (Int i <p)
and
I
X3 � V"(k.
k=l
We saw in earlier chapters that a single agent can have various different kinds
of commitment towards its goals. We will now see how social variants of these
kinds of commitment can be encoded using our model of conventions and
social commitments.
Recall from chapter 2 that an agent with a blind commitment towards some
state of affairs <p will maintain <p as an intention until it believes this state
of affairs is achieved. The social convention Cblind corresponding to blind
commitment consists of a single rule.
'ljJblind�.(Bel i <p)
In other words, team members do not initially believe that the goal is satisfied.
Expanding out the definition of (Teamblind g <p'ljJ)gives the following.
Vi· (i E g) =>
.(Bel i <p)1\
A ((Int i <p)1\ ((Bel i <p) => A((lnt i xd U xd ) U xd
where
Xl � (M-Bel g <p).
Collective Mental States 123
Thus i should intend that g mutually believe cp until this state of affairs is
achieved.
• initially, every agent does not believe that the goalcp is satisfied, but believes
cp is possible;
• every agent i then has a goal of cp until the termination condition is satisfied
(see below);
• until the termination condition is satisfied, then:
-if any agent i believes that the goal is achieved, then it will have a
goal that this becomes a mutual belief, and will retain this goal until the
termination condition is satisfied;
-if any agent i believes that the goal is impossible, then it will have a
goal that this becomes a mutual belief, and will retain this goal until the
termination condition is satisfied;
• the termination condition is that it is mutually believed that either:
-the goal cp is satisfied; or
-the goal cp is impossible to achieve.
Let
and
((Bel i cp) , (M-Bel gcp) ) ,
{ }
'-v--' '-v-"
PI ,1
C soc �
((Bel i A D....,cp) , (M-Bel g A D....,cp) )
'-----v---- ' v
,
P2 ,2
124 Chapter 6
[(
Vi· (i E g) ::::}
...,(Bel i cp)/\ (Bel i E<)cp)/\
(Int i cp)/\
( ((Bel i cp) ::::} A((lnt i (M-Bel g cp))U xd ) /\
A
((Bel i A D...,cp )::::} A((lnt i (M-Bel g A D...,cp ))U xd )
where
The fact that mutual belief (or common knowledge) can never arise in a
communication scenario where message delivery is not guaranteed is one of
the most famous results in the modal logic of knowledge [89]. See [54, pp.175-
232] for proofs of this and related results, and [54, pp.230-232] for historical
notes on the result and related work.
The formal treatment of mutual beliefs, desires, and intentions presented in
this chapter is closely based on the presentation of common knowledge in [54].
In particular, the semantics and fixed-point treatments of mutual mental states
are very closely based on those of [54]. Chapters 6 and 11 of [54] are more or
less completely devoted to common knowledge and the associated coordinated
attack problem.
The distinction between mutually intending some state of affairs and the
kinds of mental state involved in teamwork have been noted by many re
searchers. Searle, in particular, makes a distinction between a group of agents
that are engaged in coordinated activity, but not teamwork (such as a group of
agents driving on a highway), and agents that are actively engaged in team ac
tion (such a group of ballet dancers) [203]. Early attempts to formalize "team"
mental states include [181, 230].
Following Levesque, Cohen, and Nunes' formalization of teamwork [133],
many attempts to formalize joint intentions appeared in the literature [118,
190]. Jennings demonstrated that such models could be usefully applied to
industrial coordination problems [104, 105, 106].
7 Communication
v, by saving some value in it. Whenp1 saves its modified value of v, the update
performed by P2 is thus lost, which is almost certainly not what was intended.
The lost update problem is a very real issue in the design of programs that
communicate through shared data structures.
Synchronization is, of course, still an issue when constructing multiagent
systems of the kind under consideration in this book: we must ensure that
agents do not interact with one another in damaging ways [ 194]. However,
such low-level communication problems are generally regarded as solved for
the purposes of multiagent systems research. We usually assume the presence
of some underlying communication platform, which provides appropriate fa
cilities for robust, synchronized communication between agents. This seems
to be a reasonable assumption: after all, the JAVA programming language pro
vides exactly such mechanisms.
So, if we do not treat communication in such a "low-level" way, then how
is communication treated by the agent community? In order to understand the
answer, it is helpful to first consider the way that communication is treated
in the object-oriented programming community, that is, communication as
method invocation. Suppose we have a JAVA system containing two objects,
01 and 02, and that 01 has a publicly available method m1. Object 02 can
12 6 Chapter 7
Of course, simply uttering the sentence "It is raining in London" is not usu
ally enough to bring about this state of affairs, for all the reasons that were
discussed above. You have control over your own beliefs (desires, intentions).
You may believe that I am notoriously unreliable on the subject of the weather,
or even that I am a pathological liar. But in performing the communication
action of uttering "It is raining in London," I am attempting to change your
internal state. Furthermore, since this utterance is an action that I perform, I
am performing it for some purpose - presumably because I intend that you
believe it is raining.
Speech act theory treats communication as action. It is predicated on
the assumption that speech actions are performed by agents just like other
actions, in the furtherance of their intentions. Speech act theory is thus broadly
consistent with our view of agents as practical reasoning systems, deciding
Communication 127
The theory of speech acts is generally recognized to have begun with the
work of the philosopher John Austin [6]. He 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 I 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
you man and wife." Stated in the appropriate circumstances, these utterances
clearly change the state of the world in a very tangible way.!
Austin identified a number of performative verbs, which correspond to
various different types of speech acts. Examples of such performative verbs are
request, iriform, and promise. In addition, Austin distinguished three different
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 effect of the act (e.g., "He got me to make tea").
Austin referred to the conditions required for the successful completion
of performatives asfelicity conditions. He recognized three important felicity
conditions:
Austin's work was extended by John Searle, in his 1969 book Speech
Acts [202]. Searle identified several properties that must hold for a speech act
performed between a hearer and a speaker to succeed. For example, consider
a request by SPEAKER to HEARER to perform ACTION:
1. Normal I/O conditions. Normal liD 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 film 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.
In the late 1960s and early 1970s, a number of researchers in 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,
Communication 12 9
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 [39] gave an account
of the semantics of speech acts by using techniques developed in AI planning
research [59]. The aim of their work was to develop a theory of speech acts
The formalism chosen by Cohen and Perrault was the STRIPS notation,
in which the properties of an action are characterized via pre- and post
conditions [59]. The idea is very similar to Hoare logic [97]. Cohen and
Perrault demonstrated how the pre- and post-conditions of speech acts such
as request could be represented in a multimodal 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 7. 1 defines 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 fulfilled, then the Request will be successful: the
result (defined by the "effect" part of the definition) will be that the hearer
believes the speaker believes it wants some action to be performed.
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 definition of
Request only models the illocutionary force of the act. It says nothing of the
perlocutionary force. What is required is a mediating act. Figure 7. 1 gives
a definition of CauseToWant, which is an example of such an act. By this
definition, an agent will come to believe it wants to do something if it believes
that another agent believes it wants to do it. This definition could clearly be
extended by adding more pre-conditions, perhaps to do with beliefs about
social relationships, power structures, etc.
The Inform act is as basic as Request. The aim of performing an Inform
130 Chapter 7
Request(S,H,a)
Preconditions Cando.pr (S BELIEVE (H CANDOa)) 1\
(S BELIEVE (H BELIEVE (H CANDOa)))
Want.pr (S BELIEVE (S WANT requestlnstance))
Effect (H BELIEVE (S BELIEVE (S WANTa)))
CauseToWant(Al ,A2,a)
Preconditions Cando.pr (Al BELIEVE (A2 BELIEVE (A2 WANTa)))
Want.pr x
Injorm(S,H, cp)
Preconditions Cando.pr (S BELIEVE cp)
Want.pr (S BELIEVE (S WANT iriformlnstance))
Effect (H BELIEVE (S BELIEVE cp))
Figure 7.1
Definitions from Cohen and Perrault's plan-based theory of speech acts.
will be for a speaker to get a hearer to believe some statement. Like Request,
the definition of Inform requires an associated mediating act to model the
perlocutionary force of the act. The cando.pr of Inform states that the speaker
must believe cp is true. The effect of the act will simply be to make the hearer
believe that the speaker believes cpo The cando.pr of Convince simply states
that the hearer must believe that the speaker believes cpo The effect is simply to
make the hearer believe cpo
While the plan-based theory of speech acts was a major step forward, it was
recognized 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 modeled as actions performed by rational
agents in the furtherance of their intentions [36]. The foundation upon which
they built this model of rational action was their theory of intention, described
in [35]. The formal theory is too complex to describe here, but as a flavor, here
is the Cohen-Levesque definition of requesting, paraphrased in English:
Communication 131
A request is an attempt on the part of spkr, by doing e, to bring about a state where,
ideally, (i) addr intends a, (relative to the spkr still having that goal, and addr still being
helpfully inclined to spkr), and (ii) addr actually eventually does a, or at least brings
about a state where addr believes it is mutually believed that it wants the ideal situation.
[36, p. 241]
(ask-one
: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 is needed. The various
other components of this message represent its attributes. The most important
of these is the :content field, which specifies the message content. In this
case, the content simply asks for the price of IBM shares. The :receiver at
tribute specifies the intended recipient of the message, the: language attribute
132 Chapter 7
specifies that the language in which the content is expressed is called LPROLOG
(the recipient is assumed to "understand" LPROLOG) , and the final: ontology
attribute defines the terminology used in the message.
Formal definitions of the syntax of KQML and KIF were developed by the
KSE, but KQML lacked any formal semantics until Labrou and Finin's [ 127].
These semantics were presented using a pre- and post-condition notation,
closely related to Cohen and Perrault's plan-based theory of speech acts [39].
These pre- and post-conditions were specified by Labrou and Finin using a
logical language containing modalities for belief, knowledge, wanting, and
intending.
The take-up of KQML by the multiagent systems community was signif
icant. However, Cohen and Levesque (among others) criticized KQML on a
number of grounds [38], 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
difficult to see how many multiagent scenarios could be implemented without
commissives, which appear to be important if agents are to coordinate their
actions with one another.
In 1995, the Foundation for Intelligent Physical Agents (FIPA) began its
work on developing standards for agent systems. The centerpiece of this initia
tive was the development of an ACL [60]. This ACL is superficially similar to
KQML: it defines an "outer" language for messages, it defines 20 performatives
(such as inform) for defining the intended interpretation of messages, and it
does not mandate any specific 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 [60, p.lO]):
(inform
: sender agent1
:receiver agent2
:language sl
:ontology hpl-auction
Table 7.1
Performatives provided by the FIPA communication language.
The FIPA ACL has been given a formal semantics, in terms of a Semantic
Language (SL). The approach adopted for defining these semantics draws
heavily on [36], but in particular on Sadek's enhancements to this work [23]. SL
is a quantified multimodal logic, which contains modal operators for referring
to the beliefs, desires, and uncertain beliefs of agents, 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 defines a
constraint that the sender of the message must satisfy if it is to be considered
as conforming to the FIPA ACL standard. FIPA refers to this constraint as the
feasibility condition. The semantics also map each message to an sL-formula
that defines the rational effect of the action - the "purpose" of the message:
what an agent will be attempting to achieve in sending the message (cf.
perlocutionary act). However, in a society of autonomous agents, the rational
effect of a message cannot (and should not) be guaranteed. Hence conformance
does not require the recipient of a message to respect the rational effect part of
the ACL semantics - only the feasibility condition.
To illustrate the FIPA approach, I give an example of the semantics of the
134 Chapter 7
The B; is a modal connective for referring to the beliefs of agents (rather like
Bel in .cORA); Bif is a modal connective that allows us to express whether
an agent has a definite opinion one way or the other about the truth or falsity
of its parameter; and Uif 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 <p to agent) will be respecting the semantics
of the FIPA ACL if it believes <p, and it is not the case that it believes of) either
that) believes whether <p is true or false, or that) is uncertain of the truth or
falsity of <po
In the remainder of this chapter, I use ideas from the work of Cohen and
Perrault [39], Cohen and Levesque [36], Bretier and Sadek [23], and from the
FIPA standard itself [60] to define the semantics of "inform" (representative)
and "request" (directive) speech acts. In the style of [60], I then show how
these two basic speech acts can be used to define a range of other possible
speech acts. I begin by defining what it means for one agent to attempt to bring
about some state of affairs.
7.2 Attempts
We will see below that when agents communicate with one another, they are in
fact attempting to bring about some state of affairs. The notion of an attempt
will thus be a central component of our formalization of communication. The
model of attempts I adopt is based that proposed by Cohen and Levesque [36,
p.240]. The idea is that an attempt by agent i to bring about a state <p is an
action a, which is performed by i with the desire that after a is performed, <p
is satisfied, but with the intention that at least 'l/J is satisfied. The ultimate aim
of the attempt - the thing that i hopes to bring about - is represented by <p,
whereas 'l/J represents "what it takes to make an honest effort" [36, p.240]. If i
is successful, then bringing about 'l/J will be sufficient to cause <po To make this
concrete, consider the following scenario.
believes will guarantee to bring about promotion. However, if the tenure committee
could somehow be convinced that Bob had been faking research results, then this may
be sufficient to scupper Bob's chances. To this end, she sends a letter to the tenure
committee stating that Bob had been faking his results.
In this scenario, Alice is performing an action (sending the letter to the tenure
committee) in an attempt to gain promotion. Alice intends that this action will
cause the tenure committee to believe that Bob is a cheat, and she desires that
this will be enough to foil Bob's chances. Whether or not it is enough will be
outside Alice's control.
Formally, an attempt by i to achieve rp by performing 0:, at least achieving
'ljJ, is written {Attempt i 0: rp 'ljJ}; following Cohen and Levesque, I use
curly brackets here to indicate that attempts are complex actions, rather than
predicates or modal operators [36, p.240].
[ (Bel hrp) /\ 1
(Agt 0: i) /\
{Attempt io: rp'ljJ} � ?; 0:
(Des i (Achvs 0: rp)) /\
(Int i (Achvs 0:'ljJ))
Returning to the scenario above, the action 0: is Alice sending the letter about
Bob faking his research results; the state of affairs rp that Alice wants to bring
about is being promoted, and'ljJ, what it takes to make a reasonable effort, is
the tenure committee believing Bob is a cheat.
We now prove some properties of attempts. First, if an agent attempts to
bring about some state of affairs rp by at least bringing about'ljJ, then it desires
that rp is at least possible.
Proof As Theorem 7. 1. •
7.3 Informing
Probably the simplest form of communication that can take place between
two agents involves the exchange of information. Such information exchange
will usually result in belief changes. Attempts to communicate information are
known as representative speech acts [202]. The paradigm example of repre
sentative acts involves agents uttering simple declarative sentences. Examples
include an agent saying "It is raining in London," or "Tony Blair is Prime Min
ister." I will say an agent performing a representative act is iriforming another
agent about some state of affairs.
It is possible to identify the following properties of inform actions that we
will capture in our model.
1. An inform speech act (and other speech acts) takes place between a
"speaker" agent and one or more "hearer" agents.
Most theories of speech acts presuppose that they take place between just two
agents: a "speaker" and a "hearer." The model of speech acts we will see below
is more general than this - it allows for speech acts where the "hearer" is a
group of agents. For example, consider somebody making a presentation to a
group of people. The speaker is attempting to bring about some mutual belief
in the mental state of the hearers.
2. Inform actions are actually actions that an agent may perform, just like any
other action.
The model of speech acts I present here does not presuppose any particular
"transport mechanism" for the communication. For example, it does not re
quire a FIPA-like communication language for messages. Instead, any action
that satisfies certain properties can be counted as an inform message. For exam
ple, uttering the sentence "The door is open," writing a note saying "The door
is open," and simply nodding in the direction of the door can all be counted
as attempts by an agent to inform a hearer that the door is open if the actor
satisfies certain properties.
3. The purpose of an inform action is to modify the beliefs of agent(s) hearing
the speech acts, and in particular, to cause them to believe some state of affairs.
The state of affairs that the agent performing the speech act desires to bring
Communication 137
about is known as the perlocutionary force in speech act theory [202], or the
rational effect of a message in FIPA [60]. The rational effect of an inform action
is to cause some particular belief in the hearer.
4. Since the speaker of the inform act cannot normally bring about the ultimate
intention of the speech act in the listener(s), they will attempt to bring about
some "lesser" belief, such that this will be sufficient, if the listener(s) are so
inclined, to cause the listener(s) to believe the ultimate belief.
There is something of a paradox here. If I am completely autonomous, and
exercise complete control over my mental state, then nothing you say will have
any effect on my mental state. But if nothing you say can change my state,
then how can we communicate? The answer I adopt here is that if you are
attempting to inform me of some state of affairs, then the best you can do is
convince me that you believe this state of affairs. If I am then appropriately
inclined, this will be sufficient to cause me to believe it.
5. Inform actions (and other speech acts) are attempts to bring about some
intended state of affairs - they may fail to bring this state of affairs.
A model of speech acts that in some sense required an agent to bring about
the intended change in mental state would be too strong. An agent can attempt
to bring about such a mental state, but may fail for at least two reasons. First,
the action itself may fail - for example, the communications medium may be
faulty. Second, for the reasons discussed above, the hearer(s) of the speech act
may simply choose to ignore it.
6. Inform actions (and other speech acts) cannot be performed accidentally.
To modify an example from [36, p.239], suppose a blindfolded person reaches
into a bowl of flashcards, pulls out three cards, and knowingly turns them
toward another person. The cards say "The door is open." One would not be
inclined to say that an inform speech act took place.
{Inform i g a 'P}
where
and
THEOREM 7.3: F'P (Happens {Inform i g a <p}) ::::} (Desi EO(M-Bel g<p))
Proof Assume (M, V, w,p) F'P (Happens {Inform i g a <p}) for arbi
trary (M, V, w,p). From the definition of Inform, we have (M, V, w,p) F'P
(Happens {Attempt i a 'lj; X}) where
and
We can also prove that the informant does not believe the hearers already have
a mutual belief of <po Notice that an agent can be informing a group of agents
of <p even though every agent in the group already individually believes <po In
informing the group of <p, the speaker is attempting to raise the status of this
Communication 139
belief to the mutual belief of cp, which is not implied simply by everyone in a
group believing cpo
THEOREM 7.4: FP (Happens {Inform i g a cp}) => ...., (Bel i (M-Bel g cp))
Note that the case of "one-to-one" inform speech acts is covered by the
multiagent definition given above. Where we wish to deal with an agent i
informing a single agent j of cp, we will abuse notation slightly and write
{Inform ij a cp} rather than the more cumbersome {Inform i {j} a cp}.
7.4 Requesting
Inform speech acts are attempts by a speaker to get the hearer to believe some
state of affairs. In contrast, request speech acts (directives) are attempts by a
speaker to modify the intentions of the hearer. However, we can identify at
least two different types of requests:
An example of such a request would be when one agent said "Keep the door
closed." We call such requests "requests-that."
• Requests to perform some particular action.
An example of such a request would be when one agent said "Lock the door."
We call such requests "requests-to."
Requests-that are more general than requests-to. In the former case (requests
that), the agent communicates an intended state of affairs, but does not com
municate the means to achieve this state of affairs. Me asking you to keep the
door closed does not tell you how I want you to keep the door closed - you
may lock it, prop it closed with a chair, or sit against it. In the case of request
ing to, however, the agent does not communicate the desired state of affairs
at all. Instead, it communicates an action to be performed, and the state of af
fairs to be achieved lies implicit within the action that was communicated. It is
useful to make a distinction between the two cases, and for this reason, I will
formalize both. (As it turns out, it is straightforward to encode requests-to as a
special case of requests-that.)
Just as we identified desirable properties of inform speech acts, so it is
possible to identify the following properties of request actions.
140 Chapter 7
1. A request speech act takes place between a "speaker" agent and one or more
"hearer" agents.
2. Request actions are actually actions that an agent may perform, just like
any other action.
3. The purpose of a request action is to modify the intentions of agent(s)
hearing the speech act, and in particular, to cause them to intend some state
of affairs (in the case of requesting-that), or to intend to perform some action
(in the case of requesting-to).
4. Since the speaker of the request act cannot normally bring about the ulti
mate intention of the speech act directly in the listener(s), they will attempt to
bring about a "lesser" belief, such that this will be sufficient, if the listener(s)
are so inclined, to cause the listener(s) to intend the ultimate state of affairs (in
the case of requesting-that), or to intend to perform the action (requesting-to).
5. Request actions are attempts to bring about some intended state of affairs
- they may fail to bring this state of affairs.
6. Request actions cannot be performed accidentally.
Given this discussion, it is easy to formally define the RequestTh speech act. I
write
where
and
We can prove that the speaker does not believe the hearer already intends cpo
THEOREM 7 .5: FP (Happens {RequestTh iga cp}) => ...., (Bel i (M-Intg cp))
Communication 141
We can define the request-to speech act as a special case of requesting that. A
request to perform a is thus simply a request that a is performed.
Inform and request speech acts are the basic mechanisms via which agents
will communicate: they define the possible ways in which agents can attempt
to modify one another's beliefs and intentions - their key mental states. In
this section, we will see how a number of different speech acts can be defined
in terms of inform and request acts. In particular, I will define some simple
conversation policies that make use of these primitives:
Language inter-operability requires more than simply that the agents agree on the
format and meaning of the various primitive [communication language] messages.
As a practical matter, agents must also agree on the range of possible sequences and
contexts of messages when they are interpreted in the context of larger [... ] dialogues,
or conversations. [8 3, p.1]
We have already seen that the Inform speech act is the basic mechanism via
which agents can exchange information. But consider: Why should one agent
inform another of anything? There are a number of possibilities why agenti
should inform agentj of rp, for example:
1. Agent i has an intention that agent j believe rp for its own reasons. For
example, returning to the Alice and Bob tenure example from earlier in this
chapter, Alice may intend that the tenure committee believe that Bob faked
research results because this will enable her intention of gaining tenure to be
satisfied.
142 Chapter 7
Figure 7.2
The conversation policy associated with Query.
The first case is simply an instance of the more general situation, where an
agent performs an action because the agent believes it is in its best interests.
We will therefore focus on the second case, where one agent explicitly asks
another about the truth status of some proposition.
We can easily define a Query speech act. The idea is that an agent i will
perform a Query action if it has an intention of knowing the truth status of some
statement r.p. For example, I may want to know whether or not it is raining, and
if I believe that you know whether or not it is raining, I can query you to this
effect. Formally, we write {Queryi) r.p} to denote a query action performed by
a speaker i to a hearer) with the intention of discovering whether or not r.p is
the case. Query is defined, in the terminology of FIPA, as a macro action:
In other words, a Query by agenti to) with respect to statement r.p is a request
fromi to) to bring about the belief ini that either r.p is true or that r.p is false.
The mechanism via which agent) can bring about such belief is the Inform
speech act. This leads to the conversation policy illustrated in Figure 7.2.
When I ask you to make a cup of tea, the conversation does not usually end
there. Whether or not you chose to accede to my request is up to you, but
hopefully you will either confirm to me that you will carry out the request, or
else explicitly tell me that you will not. To define this kind of dialogue, we will
make use of two auxiliary definitions. The first, Agree, will be used to capture
Communication 143
{Refuse j i a3 <X2}
Figure 7.3
The conversation policy associated with Req uest To.
the case where you explicitly state that you intend to perform some action.
Thus agent i agreeing to perform an action a' to agent) simply means that i
informs) that it is the agent of a' , and that it intends that a' is performed. (Note
that a is the action of informing, rather than the action being referred to in the
inform.)
The Refuse speech act is used to capture the situation where i is telling)
that it will not carry out an action.
Using these two speech acts, we can define a conversation policy for Request
speech acts. The policy is illustrated in Figure 7.3.
tivities, and algorithms for synchronizing multiagent plans that drew upon syn
chronization techniques developed in theoretical computer science [75, 76].
Rosenschein developed similar techniques, which combined work on speech
acts with eSP-like communication to synchronize multiagent plans [ 194]. Stu
art showed how multiagent plans could be encoded as formulae of temporal
logic: showing the plans were interference-free then reduced to a problem of
showing that the resulting formula was satisfiable, a well-understood (if some
what complex) logic problem [236].
The plan-based theory of speech acts developed by Cohen and Perrault
made speech act theory accessible and directly usable to the artificial intel
ligence community [39]. In the multiagent systems community, this work is
arguably the most influential single publication on the topic of speech act-like
communication. Many authors have built on its basic ideas. For example, bor
rowing a formalism for representing the mental state of agents that was devel
oped by Robert Moore [ 157], Douglas Appelt was able to implement a system
that was capable of planning to perform speech acts [3, 4].
Many other approaches to speech act semantics have appeared in the liter
ature. For example, Perrault [ 174] described how Reiter's default logic [ 193]
could be used to reason about speech acts. Appelt gave a critique of Per
rault's work [5, pp.l67-168], and Konolige proposed a related technique us
ing hierarchic auto-epistemic logic (HAEL) [ 12 1] for reasoning about speech
acts. Galliers emphasized the links between speech acts and AMG belief
revision [7 1]: she noted that the changes in a hearer's state caused by a
speech act could be understood as analogous to an agent revising its be
liefs in the presence of new information [69]. Singh developed a theory of
speech acts [2 14, 2 15] using his formal framework for representing ratio
nal agents [2 1 1, 2 10, 2 12, 2 18, 2 13, 2 16, 2 17]. He introduced a predicate
comm(i,), m) to represent the fact that agent i communicates message m to
agent), and then used this predicate to define the semantics of assertive, direc
tive, commissive, and permissive speech acts.
At the time of writing (Spring 2000), there is a great deal of industrial in
terest in agent technology. A lot of this interest is focussed on the development
of standardized agent communication languages, and in particular, on the FIPA
standardization effort [67]. As noted in the text, the FIPA communication lan
guage does have a formally defined semantics, based largely on the techniques
of Cohen and Levesque [36] and Sadek et al. [23]. One key issue for this work
is that of semantic conformance testing. The conformance testing problem can
be summarized as follows [241]: We are given program 7f;, and an agent com-
Communication 145
Agents - both human and artificial - can engage in many and varied types of
social interaction. Communicative acts, such as informing and requesting,are
probably the simplest. In this chapter, however, we will consider cooperative
problem solving, a much more sophisticated and structured form of social
interaction. Cooperative problem solving occurs when a group of autonomous
agents choose to work together to achieve a common goal. Note that we are
not interested in cases where the agents working together are not autonomous.
Client-server computing is an obvious example of non-cooperative problem
solving,as are all "master-slave" systems [194].
Examples of cooperative problem solving in everyday life include a group
of people working together to move a heavy object, play a symphony,build a
house, or write a joint paper. In this chapter, I show how CORA can be used
to construct a formal model of such cooperative problem solving. I begin by
informally discussing what cooperative problem solving is.
1. Recognition
The cooperative problem solving process begins when some agent recognizes
the potential for cooperative action. This recognition may come about because
an agent has a goal that it does not have the ability to achieve on its own, or
else because the agent prefers a cooperative solution.
2. Team formation
During this stage,the agent that recognized the potential for cooperative action
at stage (1) solicits assistance. If this stage is successful,then it will end with a
group of agents having some kind of nominal commitment to collective action.
3. Plan formation
During this stage,the agents attempt to negotiate a joint plan that they believe
will achieve the desired goal.
4. Team action
During this stage, the newly agreed plan of joint action is executed by the
agents, which maintain a close-knit relationship throughout. This relationship
is defined by a convention, which every agent follows.
The key theme in the model is that as cooperative problem solving progresses,
the group of participating agents build up increasingly greater commitment to
the process. When the process begins, there will in fact be no kind of group
commitment at all - cooperation will "exist" only in the mental state of the
agent that initiates the process. However,as the process proceeds,the team will
build up first a commitment to the principle of collective action, and then to
the practice of it.
A corollary of the fact that agents are autonomous is that cooperation may
fail. If agents are not required to cooperate, then sometimes they will not.
Even when initial cooperation is established,it can subsequently fail for many
different reasons. For example, a group of agents that agree to cooperate in
principle may discover that the assumptions upon which their choices were
made do not in fact hold. Alternatively,events beyond the control of the team
may make successful completion of their cooperation impossible. An adequate
theory of cooperation must recognize that such failure is possible,identify the
key points at which it may occur, and characterize the behavior of a rational
agent in such circumstances.
Another aspect of the model is that it assumes communication is the
main tool through which collective mental states will be assembled. Although
Cooperation 149
8.2 Recognition
Ability
In order to precisely define the conditions that characterize the potential for
cooperative action, it is necessary to introduce a number of subsidiary def-
150 Chapter 8
Figure 8.1
Agent A 1 recognizes the potential for cooperative action.
((an D i <p) � :30: . (Bel i (Agt 0: i) 1\ (Achvs 0: <p)) 1\ (Agt 0: i) 1\ (Achvs 0: <p)
Notice that the action 0: in this definition is quantified de re with respect to the
Bel modality [101, p.183]. The significance of this is that the agent must be
"aware of the identity" of the action - it must have a rigid designator for it.
Thus it is not enough for the agent to believe that there exists some action that
will achieve the goal. It must be aware of exactly which action will achieve it.
Before proceeding, we prove some results about first-order ability. First,
we show that if an agent has the first-order ability to bring about some state of
affairs,then that state of affairs is actually possible.
Cooperation 15 1
Proof Assume (M, V,w, t) FS ((an D i <p) for arbitrary (M, V,w, t). By
expanding out the definition of (an D, we get (M, V,w, t) FS 3a· (Achvs a <p).
From this and the definition of Achvs we get (M, V,w, t) FS E (Happens a) /\
A (Happens a; <p?), and hence (M, V,w, t) FS E¢ <p. _
Proof We need to show that if (M, V,w, t) FS ((an D i <p) for arbitrary
(M, V,w,t), then (M, V,w',t) FS ((an D i <p) for all w' E W such that
w' E 8� ([i]). Start by assuming that (M, V,w, t) FS ((an D i <p) for arbitrary
(M, V,w, t). Hence (M, V,w, t) FS 3a · (Bel i (Agt a i) /\ (Achvs a <p)),
and so for all w' E W such that w' E 8� ([i]), we have (M, V,w', t) FS
3a· (Agt a i)/\ (Achvs a <p). We want to show that (M, V,w", t) FS (Agt a i)/\
'
(Achvs a <p) for all w" E W such that w" E 8� ([i]). But since the belief
accessibility relation 8 is transitive, it must be that if w' E 87 ([i]), and w" E
8�' ([i]), then w" E 87 ([i]). Hence (M, V,w", t) FS (Agt a i) /\ (Achvs a <p),
so (M, V,w', t) FS 3a · (Bel i (Agt a i) /\ (Achvs a <p)) /\ (Agt a i) /\
(Achvs a <p), and hence (M, V,w', t) FS ((an D i <p), and we are done. _
If an agent has the first-order ability to bring about some state of affairs, then
it believes this state of affairs is possible.
Proof Assume that (M, V,w, t) FS ((an D i <p) for arbitrary (M, V,w, t). By
Theorem 8.2, we therefore have (M, V,w', t) FS ((an D i <p) for all w' E W
such that w' E 87 ([i]). From Theorem 8.1, we thus have (M, V,w', t) FS
E¢ <p, and we are done. _
in the phone book) that will furnish me with the relevant information.
This motivates a definition of k order ability, (k E IN, k > 0), which allows
for the possibility of an agent performing an action in order to find out how to
bring about a state of affairs. The idea is that an agent will have the k order
ability to bring about a state of affairs cp if it has the first-order ability to bring
about k 1 order ability to bring about cpo We formalize this as follows.
-
Thus
We can also prove results analogous to Theorems 8.1, 8.2, and 8.3 for Can.
(Proofs for Theorems 8.5 and 8.6 are straightforward,and are therefore omit
ted.)
Proof The proof is by induction on the degree of ability,k. We show that for
all k E IN, FS (Cank i cp) => (Bel i (Cank i cp)). The inductive base (k 0) =
We can now formally define potential for cooperation. With respect to agent
i's desire <p, there is potential for cooperation iff:
1. there is some groupg such that i believes thatg can jointly achieve <p;
and either
Note that in clause (1), an agent needs to know the identity of the group that
it believes can cooperate to achieve its desire. This is perhaps an over-strong
assumption. It precludes an agent attempting to find out the identity of a group
that can achieve the desire, and it does not allow an agent to simply broadcast
its desire in the hope of attracting help (as in the Contract Net protocol [222]).
I leave such refinements to future work. Clause (2) represents the paradigm
reason for an agent considering a cooperative solution: because it is unable to
achieve the desire on its own. Clause (3) defines the alternative reason for an
agent considering cooperation: it prefers not to perform any of the actions that
might achieve the desire. (I do not consider the reasons why an agent will not
want to perform a particular action - these will be domain-specific.)
To simplify the presentation that follows slightly, we will make use of an
abbreviation Doesn't, to capture the sense of "something doesn't happen."
(Doesn'ta) � A D-,(Happensa)
Using the various definitions above, we can now formally state the condi
tions that characterize the potential for cooperation.
Proof Assume (M, V,w, t) FS (PfC i 'P) for arbitrary (M, V,w, t). By ex
panding the definition of Pfc, we get (M, V,w, t) FS :3 g . (Bel i (J-Cang'P)).
So for all w' E W such that w' E B7 ([i]), we have (M, V,w', t) FS
'
(J-Can g'P), and so from Theorem 8.12, we have (M, V,w , t) F EO'P. Thus
(M, V,w, t) FS (Bel i EO'P). _
THEOREM 8. 16: FS (Pfc i 'P) => (Bel i (Pfc i 'P)) (assuming agent i is
aware of its desires).
Proof Assume (M, V,w, t) FS (Pfc i 'P), for arbitrary (M, V,w, t). We need
to show that (M, V,w, t) FS (Bel i X), for each conjunct in the definition of
potential for cooperation:
Figure 8.2
Agent Al attempts to build a team to help with its problem.
Having identified the potential for cooperative action with respect to one of its
desires, what is a rational agent to do? Such an agent should attempt to solicit
assistance from a group of agents that it believes can achieve the desire. If the
agent is successful, then at the conclusion of this team formation stage, the
agent will have brought about in such a group a mental state wherein each
member of the group has a nominal commitment to collective action. The
group will not yet have fixed upon an action to perform, and in fact will not
share any kind of commitment other than to the principle of joint action. In
particular, there will not yet be a joint intention: this comes later.
How does an agent go about forming a team? The most important point to
note is that it cannotguarantee that it will be successful in forming a team: it
can only attempt it; see Figure 8.2.
The team formation stage can then be characterized as the following as
sumption about rational agents: an agent i, who believes that there is potential
for cooperative action with respect to its desire cp, will attempt to bring about
in some groupg (which it believes can jointly achieve cp):
Cooperation 157
In other words,agent i will requestg to carry out rp, and iriformg that they are
able to do it.
It is implicit within this assumption that agents are veracious with respect
to their desires, i.e., that they will try to influence the group by revealing their
true desire. I do not consider cases where agents are mendacious (i.e.,they lie
about their desires), or when agents do not reveal their desires. The interested
reader is referred to [68, pp.159-165] for a discussion and formalization of
such considerations.
It is useful to introduce a definition that captures the commitment that
agents have to collective action if team formation is successful. We write
(PreTeamg rp)
to indicate that: (i) it is mutually believed ing thatg can jointly achieve rp; and
(ii)g mutually intend rp.
Proof Assume that (M, V,w, t) FS (PreTeamgrp) for arbitrary (M, V,w, t).
The definition of PreTeam gives (M, V,w, t) FS (M-Bel g (J-Can g rp)).
Theorem 8.12 tells us that F (J-Can g rp) => EO rp, and from necessitation
for M-Bel operators, we therefore know that FS (M-Bel g ( (J-Can g rp) =>
EO rp)). From the K axiom for M-Bel and propositional reasoning, we can
therefore conclude that (M, V,w, t) FS (M-Belg EO rp). •
Using this composite speech act, we can give the assumption that charac
terizes the behavior of an agent who recognizes the potential for cooperative
action with respect to one of its desires.
FS Vi· (PfC i cp) => A3g· 3a· (Happens {FormTeam iga cp}) (8.2)
If team formation is successful, then for the first time there will be a social
commitment: a commitment by a group of agents on behalf of another agent.
1 It may also involve agents lying, though we shall not consider such cases here.
Cooperation 159
What can we say about negotiating a plan? First, we note that negotiation
may fail: the collective may simply be unable to reach agreement,due to some
irreconcilable differences.
In this case, the minimum condition required for us to be able to say that
negotiation occurred at all is that at least one agent proposed a course of
action that it believed would take the collective closer to the goal. However,
negotiation may also succeed. In this case, we expect a team action stage to
follow immediately - we shall say no more about team action here, as this is
the subject of the next section.
We shall now make the above discussion more precise. First, we define
joint attempts: what it means for a group of agents to collectively attempt
something. As might be expected,joint attempts are a generalization of single
agent attempts. An attempt by a group of agentsg to bring about a state 'P is
an action 0:, of whichg are the agents, performed with the mutual desire that
after0: is performed,'P is satisfied,or at least'l/J is satisfied (where'l/J represents
what it takes to make a reasonable effort).
r (M-Belg ""'P) A
(Agts 0:g) A
{J-Attemptgo:'P'l/J}
A
=
(M- D esg (AchvSO:'P)) A
(M-Intg (Achvs 0:;'l/J?))
We can now state the minimum conditions required for negotiation to have
occurred. Intuitively,the group will try to bring about a state where they have
agreed on a common plan,and intend to act on it. Failing that, they will bring
about a state where at least one of them has proposed a plan that it believed
would achieve the desired goal. More formally,if groupg are a pre-team with
respect to agent i's desire 'P, then g will eventually jointly attempt to bring
about a state in whichg are a team with respect to i's desire 'P, or,failing that,
to at least bring about a state where some agent j E g has made g mutually
aware of its belief that some action0: can be performed byg in order to achieve
'P. Formally,this assumption is as follows:
where
'l/J � (Teamsocg'P'l/Jsoc)
160 Chapter 8
and
Recall that Teamsoc was defined in chapter 6,to capture the notion of a "team"
mental state.
We can make some other assumptions about agent behavior during nego
tiation. Most importantly, we assume that agents will attempt to bring about
their preferences. For example,if an agent has an objection to some plan,then
it will attempt to prevent this plan being carried out. Similarly,if it has a prefer
ence for some plan,then it will attempt to bring this plan about. More precisely,
if groupg are a pre-team with respect to agent i's desire <p, and there is some
actiona such that it is mutually believed ing thata achieves <p, and thatg are
the agents ofa, then every agentj E g that has a preference thata does/does
not occur will attempt to ensure thata does/does not occur,by at least making
g mutually aware of its preference for/againsta. Note that we are once again
assuming that agents are veracious; that they attempt to influence the team by
revealing their true preferences, rather than by lying about their preferences,
or not revealing their true preferences. An agent can attempt to cause a team
to perform some action by simply making use of the RequestTh speech act,as
defined in chapter 7.
If the plan formation phase is successful then the team will have a full joint
commitment to the joint goal,and will have agreed to the means by which they
will pursue their joint goal. Ideally,we would also like to specify that the group
negotiate a convention for monitoring progress of the team action, but this is
beyond the scope of this book.
If a collective is successful in its attempt to negotiate a plan,then we expect
that collective to follow up negotiation with action. This gives us the fourth,
and final stage in our model: team action. Team action will take place when
the group of agents have a joint intention towards some state of affairs, have
a mutually agreed action that will achieve this state of affairs, and have some
convention in place to monitor the progress of the team action. We have already
seen examples of this type of team action in chapter 6.
Many attempts to formally define ability have appeared in the literature. The
earliest discussion on the subject in the artificial intelligence literature is prob-
Cooperation 16 1
ably that by McCarthy and Hayes, in their well-known work [151]. The best
known definition of ability,(and the one upon which the definition in this book
is based) is that developed by Robert Moore [156, 157]. Other examples in
clude the work of Brown [25], Singh's definitions of ability and cooperative
ability [212,216],and the work of Werner [234] and Morgenstern [160,161].
The model of cooperative problem solving presented here is based on
one I developed jointly with Nick Jennings [247, 248, 250]. These papers
were the first to present the four-stage model of cooperative problem solving,
and the first to formally define such notions as potential for cooperation.
The logic used in this earlier work is an ancestor of .cORA, with the main
difference being that .cORA uses the BOI model of Rao and Georgeff; in
the original formulation, the logic more closely resembled that of Cohen and
Levesque [35,36].
Afsaneh Haddadi, building on [247,248,250], developed a formalization
of cooperation plans [86,87]. She further developed the concept of potential
for cooperation that was presented in [247, 248, 250], and discussed how
cooperation plans specified in a BOI logic might be implemented in a practical
BOI system.
A number of attempts have appeared in the literature to formalize multi
agent argumentation. One of the first was [124]; since then, Parsons and col
leagues have presented several such models [169,207]. Kraus et al. present a
detailed logical formalization of argumentation using a BOI-like logic in [125].
The best-developed alternative to the model of cooperative action pre
sented in this chapter is the "SharedPlans" model developed by Grosz and
Kraus [84, 85]. Expressed in a rich logic that combines multimodal and first
order elements, the primary emphasis in SharedPlans is on giving an account
of how the plans of individual agents can be reconciled with those of a team.
9 Logic and Agent Theory
• as a specification language;
• as a programming language; and
• as a verification language.
In the sections that follow, we will discuss the use of logics such as CORA in
these three processes.
9.1 Specification
properties. It does not dictate how agent i should go about makingj aware that
valve 32 is open. We simply expect i to behave as a rational agent given such
an intention.
There are a number of problems with the use of languages such as CORA
for specification. The most worrying of these is with respect to their semantics.
The semantics for the modal connectives (for beliefs, desires, and intentions)
are given in the normal modal logic tradition of possible worlds [31]. So, for
example, an agent's beliefs in some state are characterized by a set of different
states, each of which represents one possibility for how the world could actu
ally be, given the information available to the agent. In much the same way,
an agent's desires in some state are characterized by a set of states that are
consistent with the agent's desires. Intentions are represented similarly. There
are several advantages to the possible worlds model: it is well studied and well
understood, and the associated mathematics of correspondence theory is ex
tremely elegant. These attractive features make possible worlds the semantics
of choice for almost every researcher in formal agent theory. However, there
are also a number of serious drawbacks to possible worlds semantics. First,
possible worlds semantics imply that agents are logically perfect reasoners, (in
that their deductive capabilities are sound and complete), and they have infi
nite resources available for reasoning. No real agent, artificial or otherwise, has
these properties. (See appendix B for a discussion of this.)
Second, possible worlds semantics are generally ungrounded. That is, there
is usually no precise relationship between the abstract accessibility relations
that are used to characterize an agent's state, and any concrete computational
model. As we shall see in later sections, this makes it difficult to go from
a formal specification of a system in terms of beliefs, desires, and so on, to
a concrete computational system. Similarly, given a concrete computational
system, there is generally no way to determine what the beliefs, desires, and
intentions of that system are. If temporal modal logics such as CORA are to
be taken seriously as specification languages, then this is a significant problem.
9.2 Implementation
1. manually refine the specification into an executable form via some princi
pled but informal refinement process (as is the norm in most current software
development);
2. directly execute or animate the abstract specification; or
3. translate or compile the specification into a concrete computational form
using an automatic translation technique.
Refinement
At the time of writing, most software developers use structured but informal
techniques to transform specifications into concrete implementations. Probably
the most common techniques in widespread use are based on the idea of top
down refinement. In this approach, an abstract system specification is refined
into a number of smaller, less abstract subsystem specifications, which together
satisfy the original specification. If these subsystems are still too abstract to be
implemented directly, then they are also refined. The process recurses until the
derived subsystems are simple enough to be directly implemented. Through
out, we are obliged to demonstrate that each step represents a true refinement of
the more abstract specification that preceded it. This demonstration may take
the form of a formal proof, if our specification is presented in, say, Z [224]
or VDM [110]. More usually, justification is by informal argument. Object
oriented analysis and design techniques, which also tend to be structured but
informal, are also increasingly playing a role in the development of systems
(see, e.g., [19]).
For functional systems, which simply compute a function of some input
and then terminate, the refinement process is well understood, and compar
atively straightforward. Such systems can be specified in terms of pre- and
post-conditions (e.g., using Hoare logic [97]). Refinement calculi exist, which
enable the system developer to take a pre- and post-condition specification,
and from it systematically derive an implementation through the use of proof
rules [159]. Part of the reason for this comparative simplicity is that there is of
ten an easily understandable relationship between the pre- and post-conditions
that characterize an operation and the program structures required to imple
ment it.
166 Chapter 9
For agent systems, which fall into the category of Pnuelian reactive sys
tems (see the discussion in chapter 1), refinement is not so straightforward.
This is because such systems must be specified in terms of their ongoing be
havior - they cannot be specified simply in terms of pre- and post-conditions.
In contrast to pre- and post-condition formalisms, it is not so easy to determine
what program structures are required to realize such specifications. As a conse
quence, researchers have only just begun to investigate refinement and design
technique for agent-based systems.
1. Identify the relevant roles in the application domain, and on the basis of
these, develop an agent class hierarchy. An example role might be weather
monitor, whereby agent i is required to make agent j aware of the prevailing
weather conditions every hour.
2. Identify the responsibilities associated with each role, the services required
by and provided by the role, and then determine the goals associated with each
service. With respect to the above example, the goals would be to find out the
current weather, and to make agentj aware of this information.
3. For each goal, determine the plans that may be used to achieve it, and the
context conditions under which each plan is appropriate. With respect to the
above example, a plan for the goal of making agent j aware of the weather
conditions might involve sending a message toj.
4. Determine the belief structure of the system - the information require
ments for each plan and goal. With respect to the above example, we might
propose a unary predicate WindSpeed(x) to represent the fact that the current
wind speed is x. A plan to determine the current weather conditions would
need to be able to represent this information.
Note that the analysis process will be iterative, as in more traditional method
ologies. The outcome will be a model that closely corresponds to the PRS agent
architecture. As a result, the move from end-design to implementation using
PRS is relatively simple.
Logic and Agent Theory 167
One major disadvantage with manual refinement methods is that they intro
duce the possibility of error. If no proofs are provided, to demonstrate that
each refinement step is indeed a true refinement, then the correctness of the
implementation process depends upon little more than the intuitions of the de
veloper. This is clearly an undesirable state of affairs for applications in which
correctness is a major issue. One possible way of circumventing this problem,
which has been widely investigated in mainstream computer science, is to get
rid of the refinement process altogether, and directly execute the specification.
It might seem that suggesting the direct execution of complex agent speci
fication languages is naive - it is exactly the kind of suggestion that detractors
of logic-based AI hate. One should therefore be very careful about what claims
or proposals one makes. However, in certain circumstances, the direct execu
tion of agent specification languages is possible.
What does it mean, to execute a formula <p of logic L? It means generating
a logical model, M, for <p, such that M F <p [64]. If this could be done without
interference from the environment - if the agent had complete control over its
environment - then execution would reduce to constructive theorem-proving,
where we show that <p is satisfiable by building a model for <po In reality, of
course, agents are not interference-free: they must iteratively construct a model
in the presence of input from the environment. Execution can then be seen as
a two-way iterative process:
model;
• environment responds, making something else true;
•
false in the (partial) model, then the agent loses. In real reactive systems,
the game is never over: the agent must continue to play forever. Of course,
some specifications (logically inconsistent ones) cannot ever be satisfied. A
winning strategy for building models from (satisfiable) agent specifications in
the presence of arbitrary input from the environment is an execution algorithm
for the logic.
tions. The goal of their work is to generate reactive systems, which share many
of the properties of our agents (the main difference being that reactive systems
are not generally required to be capable of rational decision making in the way
we described above). To do this, they specify a reactive system in terms of a
first-order branching time temporal logic formula \:Ix 3y Acp ( x,y) : the predicate
cp characterizes the relationship between inputs to the system (x) and outputs
(y). Inputs may be thought of as sequences of environment states, and outputs
as corresponding sequences of actions. The A is the universal path quantifier.
The specification is intended to express the fact that in all possible futures, the
desired relationship cp holds between the inputs to the system, x, and its out
puts, y. The synthesis process itself is rather complex: it involves generating a
Rabin tree automaton, and then checking this automaton for emptiness. Pnueli
and Rosner show that the time complexity of the synthesis process is double
exponential in the size of the specification, i.e., 0(22cOn), where c is a constant
and n = Icpl is the size of the specification cpo The size of the synthesized
program (the number of states it contains) is of the same complexity.
The Pnueli-Rosner technique is rather similar to (and in fact depends upon)
techniques developed by Wolper, Vardi, and colleagues for synthesizing Biichi
automata from linear temporal logic specifications [232]. Biichi automata are
those that can recognize w-regular expressions: regular expressions that may
contain infinite repetition. A standard result in temporal logic theory is that a
formula cp of linear time temporal logic is satisfiable if and only if there exists
a Biichi automaton that accepts just the sequences that satisfy cpo Intuitively,
this is because the sequences over which linear time temporal logic is inter
preted can be viewed as w-regular expressions. This result yields a decision
procedure for linear time temporal logic: to determine whether a formula cp
is satisfiable, construct an automaton that accepts just the (infinite) sequences
that correspond to models of cp; if the set of such sequences is empty, then cp
is unsatisfiable. The technique for constructing an automaton from the corre
sponding formula is closely based on Wolper's tableau proof method for tem
poral logic [236].
Similar automatic synthesis techniques have also been deployed to develop
concurrent system skeletons from temporal logic specifications. Manna and
Wolper present an algorithm that takes as input a linear time temporal logic
specification of the synchronization part of a concurrent system, and generates
as output a program skeleton (based upon Hoare's csp formalism [98]) that re
alizes the specification [146]. The idea is that the functionality of a concurrent
system can generally be divided into two parts: a functional part, which actu-
Logic and Agent Theory 17 1
9.3 Verification
Once we have developed a concrete system, we need to show that this sys
tem is correct with respect to our original specification. This process is known
as verification, and it is particularly important if we have introduced any in
formality into the development process. For example, any manual refinement,
done without a formal proof of refinement correctness, creates the possibility
of a faulty transformation from specification to implementation. Verification
is the process of convincing ourselves that the transformation was sound. We
can divide approaches to the verification of systems into two broad classes:
(1) axiomatic; and (2) semantic (model checking). In the subsections that fol
low, we shall look at the way in which these two approaches have evidenced
themselves in agent-based systems.
Axiomatic Approaches
Axiomatic approaches to program verification were the first to enter the main
stream of computer science, with the work of Hoare in the late 1960s [97].
Axiomatic verification requires that we can take our concrete program, and
from this program systematically derive a logical theory that represents the be
havior of the program. Call this the program theory. If the program theory is
expressed in the same logical language as the original specification, then veri
fication reduces to a proof problem: show that the specification is a theorem of
(equivalently, is a logical consequence of) the program theory.
The development of a program theory is made feasible by axiomatizing
the programming language in which the system is implemented. For example,
Hoare logic gives us more or less an axiom for every statement type in a simple
PASCAL-like language. Once given the axiomatization, the program theory can
be derived from the program text in a systematic way.
Perhaps the most relevant work from mainstream computer science is the
specification and verification of reactive systems using temporal logic, in the
way pioneered by Pnueli, Manna, and colleagues [145]. The idea is that the
computations of reactive systems are infinite sequences, which correspond
to models for linear temporal logic.! Temporal logic can be used both to
develop a system specification, and to axiomatize a programming language.
This axiomatization can then be used to systematically derive the theory of a
1 The set of all computations of a reactive system is a tree-like structure, corresponding to a model
for branching time temporal logic [50].
Logic and Agent Theory 173
program from the program text. Both the specification and the program theory
will then be encoded in temporal logic, and verification hence becomes a proof
problem in temporal logic.
Comparatively little work has been carried out within the agent-based
systems community on axiomatizing multiagent environments. I shall review
just one approach.
Note that this approach relies on the operation of agents being sufficiently
simple that their properties can be axiomatized in the logic. It works for
Shoham's AGENTO and Fisher's Concurrent METATEM largely because these
languages have a simple semantics, closely related to rule-based systems,
which in turn have a simple logical semantics. For more complex agents,
an axiomatization is not so straightforward. Also, capturing the semantics of
concurrent execution of agents is not easy (it is, of course, an area of ongoing
research in computer science generally).
• take 1f, and from it generate a model M7r that corresponds to 1f, in the sense
of states it contains.
In [189], Rao and Georgeff present an algorithm for model checking 8DI sys
tems. More precisely, they give an algorithm for taking a logical model for
their (propositional) 8DI logic, and a formula of the language, and determin
ing whether the formula is valid in the model. The technique is closely based
on model-checking algorithms for normal modal logics [92]. They show that
despite the inclusion of three extra modalities (for beliefs, desires, and inten
tions) into the CTL branching time framework, the algorithm is still quite effi
cient, running in polynomial time. So the second step of the two-stage model
checking process described above can still be done efficiently. Similar algo
rithms have been reported for 8DI-like logics in [13].
The main problem with model-checking approaches for 8DI is that it is
not clear how the first step might be realized for 8DI logics. Where does the
logical model characterizing an agent actually come from? Can it be derived
from an arbitrary program 7r, as in mainstream computer science? To do this,
we would need to take a program implemented in, say, PASCAL, and from it
derive the belief-, desire-, and intention-accessibility relations that are used
to give a semantics to the 8DI component of the logic. Because, as we noted
earlier, there is no clear relationship between the 8DI logic and the concrete
computational models used to implement agents, it is not clear how such a
model could be derived.
The fonnal tools used in this book are loosely based on the YDM specification
language: the first seven chapters of Jones [110] cover all the necessary ma
terial. However, anyone familiar with basic set notation and logic should have
no difficulty.
A central idea is that of the type: for the purposes of this book, a type can
be thought of as a (possibly infinite) set. Two "standard " types are assumed:
The set of subsets of a type T (Le., the powerset of T) is given by p( T). Thus
p({1,2,3}) = {0,{1},{2},{3},{1,2},{1,3},{2,3},{1,2,3}}
The set T of all ordered n-tuples whose first element is of type T1, second
element is of type T2, ... , dh element is of type Tn, may be defined in two
ways. The first is to define it as the cross product of its component types:
T = Tl X ... x Tn
where tl E T1, t2 E T2, ..., tn E Tn. In general, the latter method is used for
large or complex types.
Functions are specified by giving their signature:
f : Dl x . . . x Dn ---+ R
This says that the function f takes n arguments, the first of type (or from
domain) D1, . . . , the dh from domain Dn, and returns a value of type (orfrom
the range) R.
The symbol
f(x) � e(x)
means that the left hand sidef(x) is defined as the right hand side e(x). For
180 Appendix A
This definition tells us that a formula with the structure 'P ::::} 'l/J should be
understood as an abbreviation for ''P V 'l/J. It may be useful to think of such
definitions as behaving like macro definitions in a programming language like
c.
A useful operator on functions is to overwrite them. To do this, we use the
dagger operator, "f' Thus by the expressionft {x I-t y} we mean the function
that is the same asf except that it maps x to y. Thus if
f(2) = 3
and
g�ft {2 I-t 7}
then g(2) = 7.
Two standard operations on functions and relations are assumed: dom
takes a function or relation and returns the set of elements in its domain for
which it is defined; ran takes a function or relation and returns the set of
elements in its range for which the corresponding elements in the domain are
defined.
A sequence can be thought of simply as a list of objects, each of which is
of the same type. We denote the set of (possibly empty) sequences over a set T
by T*.
Finally, in this book, we deal with several languages: the symbols 'P, 'l/J,
and X are used as meta-variables, ranging over formulae of these languages.
B
Appendix:
Formal Foundations
A naive attempt to translate (B.1) into first-order logic might result in the
following:
Unfortunately, this naive translation does not work, for at least two reasons.
The first is syntactic: the second argument to the Bel predicate is aformula of
first-order logic, and is not, therefore, a tenn. So (B.2) is not a well-fonned
fonnula of classical first-order logic. The second problem is semantic. The
constants Zeus and Jupiter, by any reasonable interpretation, denote the same
individual: the supreme deity of the classical world. It is therefore acceptable
to write, in first-order logic:
Given (B.2) and (B.3 ), the standard rules of first-order logic would allow the
derivation of the following:
But intuition rejects this derivation as invalid: believing that the father of Zeus
is Cronos is not the same as believing that the father of Jupiter is Cronos.
So what is the problem? Why does first-order logic fail here? The problem
is that the intentional notions - such as belief and desire - are referentially
opaque, in that they set up opaque contexts, in which the standard substitution
rules of first-order logic do not apply. In classical (propositional or first-order)
logic, the denotation, or semantic value, of an expression is dependent solely
182 Appendix B
l
is dependent solely on the truth-value of p. So substituting equivalents into
opaque contexts is not going to preserve meaning. This is what is meant by
referential opacity. The existence of referentially opaque contexts has been
known since the time of Frege. He suggested a distinction between sense and
reference. In ordinary formulae, the "reference" of a term/formula (i.e., its
denotation) is needed, whereas in opaque contexts, the "sense" of a formula
is needed (see also [204, p.3 ]).
Clearly, classical logics are not suitable in their standard form for reason
ing about intentional notions: alternative formalisms are required. A vast en
terprise has sprung up devoted to developing such formalisms.
The field of formal methods for reasoning about intentional notions is
widely reckoned to have begun with the publication, in 1962, of Jaakko Hin
tikka's book K nowledge and Belief[96]. At that time, the subject was consid
ered fairly esoteric, of interest to comparatively few researchers in logic and
the philosophy of mind. Since then, however, it has become an important re
search area in its own right, with contributions from researchers in AI, formal
philosophy, linguistics, and economics. There is now an enormous literature on
the subject, and with a major biannual international conference devoted solely
to theoretical aspects of reasoning about knowledge, as well as the input from
numerous other, less specialized conferences, this literature is growing ever
larger [ 5 4].
Despite the diversity of interests and applications, the number of basic
techniques in use is quite small. Recall, from the discussion above, that there
are two problems to be addressed in developing a logical formalism for inten
tional notions: a syntactic one, and a semantic one. It follows that any formal
ism can be characterized in terms of two independent attributes: its language
offormulation, and semantic model[120, p.83 ].
1 Note, however, that the sentence (B.5) is itself a proposition, in that its denotation is the value
"true" or "false."
Formal Foundations 183
There are two fundamental approaches to the syntactic problem. The first
is to use a modal language, which contains non-truth-functional modal op
erators, which are applied to formulae. An alternative approach involves the
use of a meta-language: a many-sorted first-order language containing terms
that denote formulae of some other object-language. Intentional notions can
be represented using a meta-language predicate, and given whatever axiomati
zation is deemed appropriate. Both of these approaches have their advantages
and disadvantages, and will be discussed at length in what follows.
As with the syntactic problem, there are two basic approaches to the se
mantic problem. The first, best-known, and probably most widely used ap
proach is to adopt a possible worlds semantics, where an agent's beliefs,
knowledge, goals, etc. are characterized as a set of so-called possible worlds,
with an accessibility relation holding between them. Possible worlds seman
tics have an associated correspondence theory, which makes them an attractive
mathematical tool to work with [3 1]. However, they also have many associated
difficulties, notably the well-known logical omniscience problem, which im
plies that agents are perfect reasoners. A number of minor variations on the
possible worlds theme have been proposed, in an attempt to retain the corre
spondence theory, but without logical omniscience.
The most common alternative to the possible worlds model for belief
is to use a sentential, or interpreted symbolic structures approach. In this
scheme, beliefs are viewed as symbolic formulae explicitly represented in a
data structure associated with an agent. An agent then believes <p if <p is present
in the agent's belief structure. Despite its simplicity, the sentential model works
well under certain circumstances [120].
The next part of this appendix contains detailed reviews of some of these
formalisms. First, the idea of possible worlds semantics is discussed, and then
a detailed analysis of normal modal logics is presented, along with some
variants on the possible worlds theme. Next, some meta-language approaches
are discussed, and one hybrid formalism is described. Finally, some alternative
formalisms are described.
Before the detailed presentations, a note on terminology. Strictly speaking,
an epistemic logic is a logic of knowledge, a doxastic logic is a logic of belief,
and a conative logic is a logic of desires or goals. However, it is common
practice to use "epistemic" as a blanket term for logics of knowledge and
belief. This practice is adopted in this book; a distinction is only made where
it is considered significant.
184 Appendix B
The possible worlds model for epistemic logics was originally proposed by
Hintikka [96], and is now most commonly formulated in a normal modal logic
using the techniques developed by Kripke [126].2
Hintikka's insight was to see that an agent's beliefs could be characterized
in terms of a set of possible worlds, in the following way. Consider an agent
playing the card game Gin Rummy.3 In this game, the more one knows about
the cards possessed by one's opponents, the better one is able to play. And
yet complete knowledge of an opponent's cards is generally impossible if one
excludes cheating. The ability to play Gin Rummy well thus depends, at least
in part, on the ability to deduce what cards are held by an opponent, given
the limited information available. Now suppose our agent possessed the ace of
spades. Assuming the agent's sensory equipment was functioning normally, it
would be rational of her to believe that she possessed this card. Now suppose
she were to try to deduce what cards were held by her opponents. This could
be done by first calculating all the various different ways that the cards in the
pack could possibly have been distributed among the various players. (This
is not being proposed as an actual card-playing strategy, but for illustration! )
For argument's sake, suppose that each possible configuration is described on
a separate piece of paper. Once the process was complete, our agent can then
begin to systematically eliminate from this large pile of paper all those con
figurations which are not possible, given what she knows. For example, any
configuration in which she did not possess the ace of spades could be rejected
immediately as impossible. Call each piece of paper remaining after this pro
cess a world. Each world represents one state of affairs considered possible,
given what she knows. Hintikka coined the term epistemic alternatives to de
scribe the worlds possible given one's beliefs. Something true in all our agent's
epistemic alternatives could be said to be believed by the agent. For example,
it will be true in all our agent's epistemic alternatives that she has the ace of
spades.
On a first reading, this technique seems a peculiarly roundabout way
of characterizing belief, but it has two advantages. First, it remains neutral
on the subject of the cognitive structure of agents. It certainly doesn't posit
2 In Hintikka's original work, he used a technique based on "model sets," which is equivalent to
Kripke's formalism, though less elegant. See [101, Appendix Five, pp.351-352] for a comparison
and discussion of the two techniques.
3 This example was adapted from [88].
Formal Foundations 185
Epistemic logics are usually formulated as normal modal logics using the se
mantics developed by Kripke [126]. Before moving on to explicitly epistemic
logics, this section describes normal modal logics in general.
Modal logics were originally developed by philosophers interested in the
distinction between necessary truths and mere contingent truths. Intuitively,
a necessary truth is something that is true because it could not have been
otherwise, whereas a contingent truth is something that could plausibly have
been otherwise. For example, it is a fact that as I write, the Labour Party of
Great Britain hold a majority in the House of Commons. But although this is
true, it is not a necessary truth; it could quite easily have turned out that the
Conservative Party won a majority at the last general election. This fact is thus
only a contingent truth.
Contrast this with the following statement: the square root of 2 is not a
rational number. There seems no earthly way that this could be anything but
true, given the standard reading of the sentence. This latter fact is an example
of a necessary truth. Necessary truth is usually defined as something true in all
possible worlds. It is actually quite difficult to think of any necessary truths
other than mathematical laws (those with strong religious views may well
disagree).
To illustrate the principles of modal epistemic logics, a normal proposi
tional modal logic is defined.
DEFINITION B.l: Let Prop {p, q,...} be a countable set of atomic propo
=
sitions. The syntax of normal propositional modal logic is defined by the fol
lowing rules:
The operators "-," (not) and "V" (or) have their standard meaning; true is a
logical constant, (sometimes called verum), that is always true. The remaining
connectives of propositional logic can be defined as abbreviations in the usual
way. The formula Dcp is read: "necessarily cp, " and the formula <) cp is read:
"possibly cp." Now to the semantics of the language.
Normal modal logics are concerned with truth at worlds; models for such
logics therefore contain a set of worlds, W, and a binary relation, R, on
W, saying which worlds are considered possible relative to other worlds.
Additionally, a valuation function 7f is required, saying what propositions are
true at each world.
A model for a normal propositional modal logic is a triple (W, R, 7f) , where
W is a non-empty set of worlds, R � W x W, and
7f : W --t p( Prop)
though the rules defining the semantics of the language would then have to be
changed slightly.
The semantics of the language are given via the satisfaction relation, "F , "
which holds between pairs of the form (M,w) (where M is a model, and w is
a reference world), and formulae of the language. The semantic rules defining
this relation are given in Figure B.I. The definition of satisfaction for atomic
propositions thus captures the idea of truth in the "current" world, which
appears on the left of " F ". The semantic rules for "true," "-'," and "V" are
standard. The rule for " D" captures the idea of truth in all accessible worlds,
and the rule for "<)" captures the idea of truth in at least one possible world.
Formal Foundations 187
(M,w) F= true
(M,w) F= p wherep E Prop, iffp E 7r(w)
(M,w) F= -''P iff (M,w) fto 'P
(M,w) F= 'PV'lj; iff (M,w) F= 'P or (M,w) F= 'Ij;
(M,w) F= D'P iff\iw' E W· if (w,w') E Rthen (M,w') F= 'P
(M,w) F= O'P iff:Jw' E W· (w,w') E Rand (M,w') F= 'P
Figure B.1
The semantics of normal modal logic.
Note that the two modal operators are duals of each other, in the sense that
the universal and existential quantifiers of first-order logic are duals:
It would thus have been possible to take either one as primitive, and introduce
the other as a derived operator.
Correspondence Theory
if F cp then F Dcp
Proofs of these properties are trivial, and are left as an exercise for the reader.
Now, since K is valid, it will be a theorem of any complete axiomatization
of normal modal logic. Similarly, the second property will appear as a rule
of inference in any axiomatization of normal modal logic; it is generally
called the necessitation rule. These two properties turn out to be the most
problematic features of normal modal logics when they are used as logics of
knowledgelbelief (this point will be examined later).
188 Appendix B
Table B.1
Some correspondence theory.
The most intriguing properties of normal modal logics follow from the
properties of the accessibility relation, R, in models. To illustrate these proper
ties, consider the following axiom schema.
Dcp=>cp
It turns out that this axiom is characteristic of the class of models with a
reflexive accessibility relation. (By characteristic, we mean that it is true in
all and only those models in the class.) There are a host of axioms that
correspond to certain properties of R: the study of the way that properties of
R correspond to axioms is called correspondence theory. In Table B.l, we list
some axioms along with their characteristic property on R, and a first-order
formula describing the property. Note that the table only lists those axioms of
specific interest to this book; see [3 1] for others. The names of axioms follow
historical tradition.
The results of correspondence theory make it straightforward to derive
completeness results for a range of simple normal modal logics. These results
provide a useful point of comparison for normal modal logics, and account in
a large part for the popularity of this style of semantics.
A system of logic can be thought of as a set of formulae valid in some
class of models; a member of the set is called a theorem of the logic (if cp is
a theorem, this is usually denoted by f- cp). The notation K�l . . . �n is often
used to denote the smallest normal modal logic containing axioms �l' . . . , �n
(any normal modal logic will contain K; cf. [81, p.25]).
For the axioms T, D, 4, and 5, it would seem that there ought to be sixteen
distinct systems of logic (since 24 16). However, some of these systems tum
=
out to be equivalent (in that they contain the same theorems), and as a result
Formal Foundations 189
K4 K5 KD ---_I KT=KDT
�/ KD45
KT45
--------. KT5= KDT5
KDT45
Figure B.2
The normal modal logic systems based on axioms T, D, 4, and 5.
there are only eleven distinct systems. The relationships among these systems
are described in Figure B.2 (after [120, p.99], and [3 1, p.13 2]). In this diagram,
an arc from A to B means that B is a strict superset of A: every theorem of A is
a theorem of B, but not vice versa ; A B means that A and B contain precisely
=
• KT is known as T;
• KT4 is known as S4;
• KD45 is known as weak-S5; and
• KT5 is known as S5.
To use the logic developed above as an epistemic logic, the formula D<p is read
as: "it is known that <p." The worlds in the model are interpreted as epistemic
190 Appendix B
alternatives, the accessibility relation defines what the alternatives are from
any given world. The logic deals with the knowledge of a single agent. To deal
with multiagent knowledge, one adds to a model structure an indexed set of
accessibility relations, one for each agent. A model is then a structure:
Each operator K;thus has exactly the same properties as D." Corresponding
"
{CPI, . . . ,CP n }, then in every world where all of � are true, cp must also be true,
and hence
and an unthinkable amount of hard work before Andrew Wiles was able to
prove it. But if our agent's beliefs are closed under logical consequence, then
our agent must know it. So consequential closure, implied by necessitation and
the K axiom, seems an overstrong property for resource-bounded reasoners.
These two problems - that of knowing all valid formulae, and that of know1-
edgelbelief being closed under logical consequence - together constitute the
famous logical omniscience problem. This problem has some damaging corol
laries.
The first concerns consistency. Human believers are rarely consistent in the
logical sense of the word; they will often have beliefs rp and 'ljJ, where rp f- -,'ljJ,
without being aware of the implicit inconsistency. However, the ideal reason
ers implied by possible worlds semantics cannot have such inconsistent beliefs
without believing every formula of the logical language (because the conse
quential closure of an inconsistent set of formulae is the set of all formulae).
Konolige has argued that logical consistency is much too strong a property
for resource-bounded reasoners: he argues that a lesser property - that of be
ing non-contradictory - is the most one can reasonably demand [120]. Non
contradiction means that an agent would not simultaneously believe rp and -'rp,
although the agent might have logically inconsistent beliefs.
The second corollary is more subtle. Consider the following propositions
(this example is from [120, p.88]):
The second conjunct of (2) is valid, and will thus be believed. This means
that (1) and (2) are logically equivalent; (2) is true just when (1) is. Since agents
are ideal reasoners, they will believe that the two propositions are logically
equivalent. This is yet another counter-intuitive property implied by possible
worlds semantics, as: "equivalent propositions are not equivalent as beliefs"
[120, p.88]. Yet this is just what possible worlds semantics implies. It has been
suggested that propositions are thus too coarse-grained to serve as the objects
of belief in this way.
The logical omniscience problem is a serious one. In the words of
Levesque:
Any one of these [problems] might cause one to reject a possible-world formalization
19 2 Appendix B
We now consider the appropriateness of the axioms Dn, Tn, 4n, and 5n for
logics of knowledgelbelief.
The axiom Dn says that an agent's beliefs are non-contradictory; it can be
rewritten in the following form:
which is read: "if i knows <p, then i doesn't know '<p." This axiom seems a
reasonable property of both knowledge and belief.
The axiom Tn is often called the knowledge axiom, since it says that what is
known is true. It is usually accepted as the axiom that distinguishes knowledge
from belief: it seems reasonable that one could believe something that is false,
but one would hesitate to say that one could know something false. Knowledge
is thus often defined as true belief: i knows <p if i believes <p and <p is true. So
defined, knowledge satisfies Tn.
Axiom 4n is called the positive introspection axiom. Introspection is the
process of examining one's own beliefs, and is discussed in detail in [120,
Chapter S]. The positive introspection axiom says that an agent knows what it
knows. Similarly, axiom 5n is the negative introspection axiom, which says that
an agent is aware of what it doesn't know. Positive and negative introspection
together imply an agent has perfect knowledge about what it does and doesn't
know (cf. [120, Equation (S.l1), p.79]). Whether or not the two types of
introspection are appropriate properties for knowledgelbelief is the subject
of some debate. However, it is generally accepted that positive introspection
is a less demanding property than negative introspection, and is thus a more
reasonable property for resource-bounded reasoners.
Given the comments above, the modal system SSn is often chosen as a
logic of knowledge, and weak-SSn is often chosen as a logic of belief
Computational Aspects
1. The satisfiability problem for each of the key systems Kn, Tn, S4n, weak
SSn, and SSn is decidable.
Formal Foundations 193
2. The satisfiability and validity problems for Kn, Tn, S4n (where n � 1), and
S5n, weak-S5n (where n � 2) are P SPACE complete.
The first result is encouraging, as it holds out at least some hope of automation.
Unfortunately, the second result is extremely discouraging: in simple terms,
it means that in the worst case, automation of these logics is not a practical
proposition.
Discussion
To sum up, the basic possible worlds approach described above has the follow
ing disadvantages as a multiagent epistemic logic:
Despite these serious disadvantages, possible worlds are still the semantics
of choice for many researchers, and a number of variations on the basic possi
ble worlds theme have been proposed to get around some of the difficulties.
(W, R, D, I, 7r)
where W and R are a set of worlds and a binary relation on W (as before), and:
and IY' is the set of n-tuples over D; the function 7r gives the extension of each
predicate symbol in each world.
ifT E Canst
otherwise.
So, despite the added complexity of predicates and terms, the model theory for
quantified modal logics remains straightforward.
Now consider such a system as an epistemic logic. The semantics can
easily be extended to the multiagent case, as in propositional modal logic, by
the addition of multiple accessibility relations, etc. One unfortunate property
of quantified modal logics, as defined above, is that they make the Barcan
formulae valid. The Barcan formula is:
DCricketFan( PM)
Here, PM is a constant which in the actual world denotes the individual Tony
196 Appendix B
Blair (Prime Minister of the U.K. at the time of writing). But suppose our
agent had been on a desert island since November 1990, and was somehow
unaware that Margaret Thatcher was no longer Prime Minister. For this agent,
the constant PM would denote someone entirely different to that which it
denotes for us, and it is unlikely that a rational agent would believe of the
individual Margaret Thatcher that she was a cricket fan. Note that the agent
could still believe that the individual Tony Blair was a cricket fan, but in its
ignorance, it would use a different constant for this individual. The point is
that the constant PM has a different denotation for us and the agent, and, more
generally, a different denotation in different worlds. Such constants are said to
befluent expressions; non-fluent expressions are called rigid designators.
To deal with fluent expressions, Konolige has proposed the technical de
vice of the bullet operator, ("e" ) . Suppose a is a constant, then ea is an expres
sion returning a constant that always denotes what a denotes for us. The use
of the bullet operator is somewhat complex, and is described in detail in [120,
pp.3 8--42 and pp.l00-104].
One difficult issue in the philosophy of modal logics is quantifYing-in to
modal contexts. Consider the following English sentence:
Now consider the following quantified modal logic formulae, each represent
ing one attempt to formalize (B.6):
3x . DUnicorn(x) (B.7)
D:3x· Unicorn(x) (B.8)
1. Expressive power.
The following meta-language formulae have no quantified modal logic coun
terparts:
:3x . Bel(i, x) "i believes something"
\:Ix· Bel(i, x) ::::} BeIU, x) "i believes everything) believes"
2. Computational tractability.
Meta-languages are just many-sorted first-order languages, for which auto
mated theorem provers exist. It should therefore be possible - in principle
at least - to use existing theorem provers for meta-languages. However, this
claim has yet to be satisfactorily demonstrated.
The key difficulty with meta-language approaches is that many naive at
tempts to treat meta-language predicates as syntactic modalities run into in
consistency. These difficulties arise, for the large part, from the issue of self
reference. 4
Suppose one wished to use a meta-language approach to represent and
reason about knowledge and belief. Following "standard" practice, knowledge
may be defined as true belief. One might begin by setting object-language =
meta-language, so that the object- and meta-language are the same; in such
circumstances, the meta-language is said to be self-referential, since it may
contain terms that refer to its own formulae. A truth predicate can then be
defined.
(B.lI)
(B.12)
The Bel predicate can then be given whatever axiomatization is deemed appro
priate. This approach seems simple, intuitive, and satisfactory. Unfortunately,
in general, any first-order meta-language theory containing axiom (B.II) turns
out to be inconsistent. This problem was first recognized by Tarski; the diffi
culty is with the possibility of formulae asserting their own falsity (as in the
famous "liar" paradox).
4 A good discussion of these issues may be found in [173]; the issue of self reference is examined
in detail in [171] and [172].
Formal Foundations 199
Several proposals have been put forward to remedy the problem. One
possibility is to define True and False predicates, such that for some formulae
1 1
<p, neither True( r <p ) nor False( r <p ) hold; in effect, one axiomatizes a system
in which the law of the excluded middle does not hold. This solution is
unintuitive, however, and seems rather ad hoc.
Another solution, due to Perlis [171], is to replace (B.ll) with an axiom of
the form:
(B.13 )
*
where <p is the formula obtained from <p by replacing every occurrence of
-, True(r 'lj; 1) in <p by True(r -,'lj; 1) . This simple expedient prevents inconsistency
(see [171, pp.3 12-315] for proof). This proposal has been criticized by Kono
lige, on a number of grounds, however: see [120, p.116] for details.
A problem not alleviated by Perlis' schema was first recognized by Mon
tague [155]. Consider the following axiom:
(cf. the modal system KT). Montague showed that any moderately sophis
ticated first-order theory (and in particular, basic arithmetic) containing the
above axiom and inference rule is inconsistent. This result appears to be dev
astating, and for a long time dampened down research into first-order meta
languages. A similar result by Thomason ([229]) is also discouraging.
However, des Rivieres and Levesque have recently shown that, while
Montague's results are technically correct, a careful reworking, with slightly
different assumptions, leads back to consistency [45].5 Also, Perlis has shown
how a similar technique to that proposed by him for recovering from Tarski's
result can be used to recover from Montague's results [172].
If nothing else, the above discussion illustrates that the whole issue of self
referential languages is a difficult one. It is hardly surprising, therefore, that
some researchers have rejected self reference entirely. One critic is Konolige,
who suggests that an observer of a system of agents can hardly have any use
for a self-referential language. He argues that the logical puzzles caused by
5 In fact, they showed that it was a naive translation from a modal to meta-language that was
causing difficulties.
200 Appendix B
self-reference are just that: puzzles, which an agent will never usually need to
consider (unless she is a philosophy or logic student) [120, p.llS].
One "standard" alternative to self-referential languages is to use an hierar
chicallanguage structure. Consider a "tower" of languages:
Lo - L1 - L2 - ... - Lk - ...
No matter how far we climb up the object/meta-language hierarchy, we will not be able
to capture the intuitive content of [(B. 14)]. [23 1, pp. 7-8]
Other objections to the hierarchical approach have been raised. For exam
ple, Morgenstern points out that the truth predicate paradox is only resolved
by positing an infinite number of truth predicates, one for each language in the
hierarchy. She argues that this is not a satisfactory solution, for two reasons:
In the first place, it is implausible that people are consciously aware of using different
truth predicates when they speak. Secondly, we often do not know which truth predicate
to use when we utter a particular statement. Finally, it is impossible . . . to construct a
pair of sentences, each of which refers to the other, although such sentences may make
perfect sense. [160, p. 104]
Formal Foundations 20 1
There seem to be almost as many different temporal logics as there are people
using temporal logics to reason about programs. In this section, we briefly
describe some important developments in temporal logics.
The earliest temporal logic studied in detail was the modal logic Kt, cor
responding to a modal system with two basic modal operators (often written
"[P]" or "H" - "heretofore," or "always past," and "[F ] " or "G" - "hence
forth," or "always") [182]. The semantics of these operators are given via two
ordering relations Rp and RF on the set of worlds, such that the two relations
are the inverse of each other. The usual "was" and "sometime" operators (writ
ten "( P)" or " P " and "(F ) " or "F") are defined as the duals of these operators.
This logic is discussed at length in [81, Chapter 6].
Although such a system can be used to crudely reason about programs, it
cannot describe the "fine structure" of the state sequences generated by exe
cuting programs (see below). For this reason, a "next time" operator was used
by Pnueli in his original proposal [176]. Also, the standard heretofore/always
combination of operators was discovered to be inadequate for expressing many
properties, and so the basic temporal logic was augmented by the since and un
til operators (written " S" and " U "). In his 1968 doctoral thesis, Kamp demon
strated that the logic with since and until operators was expressively complete
over continuous linear orders [115].6
The "standard" linear discrete temporal logic is based on until/since and
next/last [144, 145]. In the propositional case, this logic is decidable (though
the problem is P SPACE complete - see [219]), and is generally regarded as
expressive enough to capture many interesting properties of reactive systems.
Gough has developed tableaux-based decision procedures for this logic [82];
Fisher has developed resolution methods [62].
6 The since/until operators are assumed to be strict: the since operator refers strictly to the past,
the until operator refers strictly to the future.
20 2 Appendix B
In the first-order case, temporal logics containing these operators are not
decidable, but this should come as no surprise! Perhaps more worrying is that
first-order temporal logic is not finitely axiomatizable [1].
A temporal logic based solely on these operators does have its limitations,
however. Sistla et al. showed that it could not be used to describe an unbounded
FIFO buffer [221].
Many variations on this basic temporal logic theme exist. For example, the
use offixpoint operators has been discussed. Banieqbal and Barringer describe
a logic that keeps the next operator as basic, but then defines two fixpoint
operators from which the other standard operators of linear discrete temporal
logic can be derived [ 7]. Wolper has described a logic ETL, which extends the
standard temporal logic with a set of grammar operators [23 5]. Yet another
variation is to add a chop operator, C, which "composes" two finite sequences
[9].
All of the logics mentioned above have assumed the model of time is
discrete (i.e., that for any time point, there exists a time such that no other
time point occurs between them) and linear (i.e., that each point in time has at
most one successor). But these assumptions are not essential: a temporal logic
of reals (where the worlds are isomorphic with the real numbers) has been
developed; however, such logics are complex and uncommon.
Much more common are branching time logics. Briefly, a branching time
structure is one where each time point may have a number of "successor"
times, each one intuitively corresponding to one way things could turn out.
The repertoire of operators in linear temporal logic is not sufficient to express
all the properties of such structures (despite Lamport's claims in his famous
1980 paper [129]).
The earliest branching time logic to be studied at length was UB (unified
system of branching time) [12]. This logic extended linear time temporal logic
by the addition of two operators, "A" ("on all paths . . . ") and "E" ("on some
path . . . "), called path quantifiers, which could be prefixed to any formula
containing at most one occurrence of the usual linear time temporal operators.
This introduces an obvious restriction on the expressibility of UB.
UB does not contain an "until" operator; this omission was rectified in a
logic CTL (computation tree logic). However, CTL is still not expressive enough
to capture many interesting properties of branching time structures. The most
expressive branching time logic so far studied in any detail is called CTL * [50].
This logic allows path quantifiers to be prefixed to arbitrary formulae of the
language: intermixing of path quantifiers and standard temporal logic operators
Formal Foundations 203
[1] M. Abadi. Temporal Logic Theorem Proving. PhD thesis, Computer Science
Department, Stanford University, Stanford, CA 94305, 1987.
[5] D. E. Appelt and K. Konolige. A nonmonotonic logic for reasoning about speech
acts and belief revision. In M. Reinfrank, 1. de Kleer, M. L. Ginsberg, and
E. Sandewall, editors,
Non-Monotonic Reasoning - Proceedings of the Second
International Workshop (LNAI Volume 346), pages 164-175. Springer-Verlag:
Berlin, Germany, 1988.
[6] J. L. Austin. How to Do Things With Words. Oxford University Press: Oxford,
England, 1962.
[10] H. Barringer, R. Kuiper, and A. Pnueli. A really abstract concurrent model and
its temporal logic. In Proceedings of the Thirteenth ACM Symposium on the
Principles of Programming Languages, pages 173-183, 1986.
[11] M. Ben-Ari. Principles of Concurrent and Distributed Programming. Prentice
Hall, 1990.
[12] M. Ben-Ari, Z. Manna, and A. Pnueli. The temporal logic of branching time. In
Proceedings of the Eighth ACM Symposium on the Principles of Programming
Languages (POPL), pages 164-176, 1981.
[13] M. Benerecetti, F. Giunchiglia, and L. Serafini. A model checking algorithm
for multiagent systems. In J. P. MUller, M. P. Singh, and A. S. Rao, editors,
Intelligent Agents V (LNAI Volume 1555). Springer-Verlag: Berlin, Germany,
1999.
[14] K. Binmore. Fun and Games: A Text on Game Theory. D. C. Heath and
Company: Lexington, MA, 1992.
206 References
[23] P. Bretier and D. Sadek. A rational agent as the kernel of a cooperative spoken
dialogue system: Implementing a logical theory of interaction. In J. P. Miiller,
M. Wooldridge, and N. R. Jennings, editors, Intelligent Agents III (LNAI Volume
1193), pages 189-204. Springer-Verlag: Berlin, Germany, 1997.
[30] L. Catach. TABLEAUX: A general theorem prover for modal logics. Journal of
Automated Reasoning, 7:489-510, 1991.
[33] E. M. Clarke, o. Grumberg, and D. A. Peled. Model Checking. The MIT Press:
Cambridge, MA 2000.,
[36] P. R. Cohen and H. 1. Levesque. Rational interaction as the basis for commu
nication. In P. R. Cohen, 1. Morgan, and M. E. Pollack, editors, Intentions in
Communication, pages 221-256. The MIT Press: Cambridge, MA 1990. ,
[43] D. C. Dennett. The Intentional Stance. The MIT Press: Cambridge, MA 1987. ,
[49] E. A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Hand
book of Theoretical Computer Science Volume B: Formal Models and Semantics,
pages 996-1072. Elsevier Science Publishers B. Y.: Amsterdam, The Nether
lands, 1990.
[58] I. A. Ferguson. Integrated control and coordinated behaviour: A case for agent
models. In M. Wooldridge and N. R. Jennings, editors, Intelligent Agents:
Theories, Architectures, and Languages (LNAI Volume 890), pages 203-218.
Springer-Verlag: Berlin, Germany, January 1995.
[60] FIPA. Specification part 2 - Agent communication language, 1999. The text
refers to the specification dated 16 April 1999.
References 209
[62] M. Fisher. A resolution method for temporal logic. In Proceedings of the Twelfth
International Joint Coriference on Artificial Intelligence (IJCAI-91), Sydney,
Australia, August 1991.
[63] M. Fisher. A survey of Concurrent METATEM - the language and its applica
tions. In D. M. Gabbay and H. 1. Ohlbach, editors, Temporal Logic - Proceed
ings of the First International Conference (LNAI Volume 827), pages 480-505.
Springer-Verlag: Berlin, Germany, July 1994.
[65] M. Fisher and M. Wooldridge. Executable temporal logic for distributed AI.
In Proceedings of the Twelfth International Workshop on Distributed Artificial
Intelligence (I WDAI-93), pages 131-142, Hidden Valley, PA, May 1993.
[66] M. Fitting. Proof Methods for Modal and Intuitionistic Logics. D. Reidel
Publishing Company: Dordrecht, The Netherlands, 1983. (Synthese library
volume 169).
[67] The Foundation for Intelligent Physical Agents. See http://www. fipa. org/.
[71] P. Giirdenfors. Knowledge in Flux. The MIT Press: Cambridge, MA, 1988.
[72] C. Geissler and K. Konolige. A resolution method for quantified modal logics
of knowledge and belief. In J. Y. Halpern, editor,
Proceedings of the 1986
Conference on Theoretical Aspects of Reasoning About Knowledge, pages 309-
324. Morgan Kaufmann Publishers: San Mateo, CA, 1986.
[81] R. Goldblatt. Logics of Time and Computation (CSLI Lecture Notes Number 7).
Center for the Study of Language and Information, Ventura Hall, Stanford, CA
94305, 1987. (Distributed by Chicago University Press).
[82] G. D. Gough. Decision procedures for temporal logic. Master's thesis, De
partment of Computer Science, Manchester University, Oxford Rd. , Manchester
M13 9PL, UK, October 1984.
[84] B. 1. Grosz and S. Kraus. Collaborative plans for complex group action. Artificial
Intelligence, 86(2):269-357, 1996.
[90] J. Y. Halpern and Y. Moses. A guide to completeness and complexity for modal
logics of knowledge and belief. Artificial Intelligence, 54:319-379, 1992.
[91] J. Y. Halpern and M. Y. Vardi. The complexity of reasoning about knowledge and
time. I. Lower bounds. Journal of Computer and System Sciences, 38:195-237,
1989.
[94] K. V. Hindriks, F. S. de Boer, W. van der Hoek, and J. -J. Ch. Meyer. Formal
semantics for an abstract agent programming language. In M. P. Singh, A. Rao,
and M. J. Wooldridge, editors, Intelligent Agents I V (LNAI Volume 1365), pages
215-230. Springer-Verlag: Berlin, Germany, 1998.
[95] K. V. Hindriks, F. S. de Boer, W. van der Hoek, and J. -J. Ch. Meyer. Control
structures of rule-based agent languages. In J. P. MUller, M. P. Singh, and A. S.
Rao, editors, Intelligent Agents V (LNAI Volume 1555). Springer-Verlag: Berlin,
Germany, 1999.
[96] J. Hintikka. Knowledge and Belief Cornell University Press: Ithaca, NY, 1962.
[99] W. van der Hoek, B. van Linder, and J. -J. Ch. Meyer. An integrated modal
approach to rational agents. In M. Wooldridge and A. Rao, editors, Foundations
of Rational Agency, pages 133-168. Kluwer Academic Publishers: Boston, MA,
1999.
[115] J. A. W. Kamp. Tense Logic and the Theory of Linear Order. PhD thesis,
University of California, 1968.
[127] Y. Labrou and T. Finin. Semantics and conversations for an agent communica
tion language. In Proceedings of the Fifteenth International Joint Conference on
Artificial Intelligence (IJCAI-97), pages 584-591, Nagoya, Japan, 1997.
[128] Y. Labrou and T. Finin. Agent communication languages: The current landscape.
IEEE Intelligent Systems, 14(2):45-52, 1999.
214 References
[129] L. Lamport. Sometimes is sometimes not never - but not always. In Proceed
ings of the Seventh ACM Symposium on the Principles of Programming Lan
guages (POPL), 1980.
[130] Y. Lesperance, H. J. Levesque, F. Lin, D. Marcu, R. Reiter, and R. B. Scher!.
Foundations of a logical approach to agent programming. In M. Wooldridge,
J. P. Miiller, and M. Tambe, editors, Intelligent Agents II (LNAI Volume 1037),
pages 331-346. Springer-Verlag: Berlin, Germany, 1996.
[137] B. van Linder, W. van der Hoek, and 1. -J. Ch. Meyer. How to motivate your
agents. In M. Wooldridge, J. P. Miiller, and M. Tambe, editors, Intelligent Agents
II (LNAI Volume 1037), pages 17-32. Springer-Verlag: Berlin, Germany, 1996.
[138] M. Ljunberg and A. Lucas. The OASIS air traffic management system. In
Proceedings of the Second Pacific Rim International Conference on AI (PRICAI-
92), Seoul, Korea, 1992.
[139] A. Lomuscio. Knowledge Sharing among Ideal Agents. PhD thesis, School of
Computer Science, University of Birmingham, Birmingham, UK, June 1999.
[141] M. Luck, N. Griffiths, and M. d'Invemo. From agent theory to agent construc
tion: A case study. In 1. P. Miiller, M. Wooldridge, and N. R. Jennings, editors,
Intelligent Agents III (LNAI Volume 1193), pages 49-64. Springer-Verlag: Berlin,
Germany, 1997.
References 215
[142] P. Maes. Agents that reduce work and information overload. Communications
of the ACM, 37(7):31-40, July 1994.
[144] Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent
Systems. Springer-Verlag: Berlin, Germany, 1992.
[150] J. McCarthy. Modality, Si! Modal logic, No! Studia Logica, 59:29-32, 1997.
[151] J. McCarthy and P. I. Hayes. Some philosophical problems from the standpoint
of artificial intelligence. In B. Meltzer and D. Michie, editors, Machine Intelli
gence 4. Edinburgh University Press, 1969.
[152] J. -I. Ch. Meyer and W. van der Hoek. Epistemic Logic for AI and Computer
Science. Cambridge University Press: Cambridge, England, 1995.
[153] J.-I. Ch. Meyer, W. van der Hoek, and B. van Linder. A logical approach to the
dynamics of commitments. Artificial Intelligence, 113:1-40, 1999.
[156] R. C. Moore. Reasoning about knowledge and action. In Proceedings of the Fifth
International Joint Conference on Artificial Intelligence (/JCAI-77), Cambridge,
MA, 1977.
[158] M. Mora, 1. G. Lopes, R. Viccari, and H. Coelho. BD! models and systems:
reducing the gap. In J. P. MUller, M. P. Singh, and A. S. Rao, editors, Intelligent
Agents V (LNAI Volume 1555). Springer-Verlag: Berlin, Germany, 1999.
[162] J. P. MUller. The Design of Intelligent Agents (LNAI Volume 1177). Springer
Verlag: Berlin, Germany, 1997.
[167] N. 1. Nilsson. Towards agent programs with circuit semantics. Technical Re
port STAN-CS-92-1412, Computer Science Department, Stanford University,
Stanford, CA 94305, January 1992.
[168] P. Noriega and C. Sierra, editors. Agent Mediated Electronic Commerce (LNAI
Volume 1571). Springer-Verlag: Berlin, Germany, 1999.
[169] S. Parsons, C. A. Sierra, and N. R. Jennings. Agents that reason and negotiate
by arguing. Journal of Logic and Computation, 8(3):261-292, 1998.
[172] D. Perlis. Languages with self reference II: Knowledge, belief, and modality.
Artificial Intelligence, 34:179-212, 1988.
References 217
[173] D. Perlis. Meta in logic. In P. Maes and D. Nardi, editors, Meta-Level Architec
tures and Reflection, pages 37-49. Elsevier Science Publishers B. Y.: Amsterdam,
The Netherlands, 1988.
[181] R. Power. Mutual intention. Journal for the Theory of Social Behaviour, 14:85-
102, March 1984.
[182] A. Prior. Past, Present and Future. Oxford University Press: Oxford, England,
1967.
[183] A. S. Rao. AgentSpeak(L): BDI agents speak out in a logical computable lan
guage. In W. Van de Velde and 1. W. Perram, editors, Agents Breaking Away:
Proceedings of the Seventh European Workshop on Modelling Autonomous
Agents in a Multi-Agent World, (LNAI Volume 1038), pages 42-55. Springer
Verlag: Berlin, Germany, 1996.
[185] A. S. Rao and M. Georgeff. Decision procedures for BDI logics. Journal of
Logic and Computation, 8(3):293-344, 1998.
[192] H. Reichgelt. Logics for reasoning about knowledge and belief. The Knowledge
Engineering Review, 4(2):119-139, 1989.
[193] R. Reiter. A logic for default reasoning. Artificial Intelligence, 13:81-132, 1980.
1994.
[200] K. Schild. On the relationship between BD! logics and standard logics of
concurrency. In 1. P. Muller, M. P. Singh, and A. S. Rao, editors, Intelligent
Agents V (LNAI Volume 1555). Springer-Verlag: Berlin, Germany, 1999.
[204] N. See!. Agent Theories and Architectures. PhD thesis, Surrey University,
Guildford, UK, 1989.
[207] Carles Sierra, Nick R. Jennings, Pablo Noriega, and Simon Parsons. A frame
work for argumentation-based negotiation. In M. P. Singh, A. Rao, and M. J.
Wooldridge, editors, Intelligent Agents IV (LNAI Volume 1365), pages 177-192.
Springer-Verlag: Berlin, Germany, 1998.
[208] H. A. Simon. The Sciences of the Artificial (second edition). The MIT Press:
Cambridge, MA 1981.
,
[212] M. P. Singh. Group ability and structure. In Y. Demazeau and J. -P. Muller,
editors,
Decentralized AI 2 Proceedings of the Second European Workshop
-
[215] M. P. Singh. A semantics for speech acts. Annals of Mathematics and Artificial
Intelligence, 8(1-11):47-71, 1993.
[217] M. P. Singh. The intentions of teams: Team structure, endodeixis, and exodeixis.
In Proceedings of the Thirteenth European Conference on Artificial Intelligence
(ECAI-98), pages 303-307, Brighton, United Kingdom, 1998.
[218] M. P. Singh and N. M. Asher. Towards a formal theory of intentions. In J. van
Eijck, editor,
Logics in AI - Proceedings of the European Workshop JELIA-90
(LNAI Volume 478), pages 472-486. Springer-Verlag: Berlin, Germany, 1991.
[219] A. Sistla. Theoretical issues in the design and verification of distributed systems.
Technical Report CMU-CS-83-146, School of Computer Science, Carnegie
Mellon University, Pittsburgh, PA, 1983.
[224] M. Spivey. The Z Notation (second edition). Prentice Hall International: Hemel
Hempstead, England, 1992.
[226] S. P. Stich. From Folk Psychology to Cognitive Science. The MIT Press:
Cambridge, MA, 1983.
[227] C. Stirling. Completeness results for full branching time logic. In REX School
Workshop on Linear Time, Branching Time, and Partial Order in Logics and
Models for Concurrency, Noordwijkerhout, Netherlands, 1988.
[228] K. P. Sycara. Multiagent compromise via negotiation. In L. Gasser and
M. Huhns, editors, Distributed Artificial Intelligence Volume II, pages 119-138.
Pitman Publishing: London and Morgan Kaufmann: San Mateo, CA, 1989.
[231] R. Turner. Truth and Modality for Knowledge Representation. Pitman Publish
ing: London, 1990.
[233] G. WeiB, editor. Multi-Agent Systems. The MIT Press: Cambridge, MA 1999.
,
[236] P. Wolper. The tableau method for temporal logic: An overview. Logique et
Analyse, 110-111, 1985.
[249] M. Wooldridge and N. R. Jennings. Intelligent agents: Theory and practice. The
Knowledge Engineering Review, 10(2):115-152, 1995.
A c
G J
Tate, A. 18
team formation 156
teamwork 119-124
temporal implication 61
temporal logic 13, 56--61, 143, 201-203
terms, logical 70
test operator 63
Thatcher, M. 195
theoretical reasoning 21
time constrained decision making 22
total correctness 61
total relation 72
TOURINGMACHINES agent architecture 45
transitive relations 74
truth functional operators 181
truth predicate 198
Turner, R. 200
V-z
Vardi, M. 170
variables
assignment for 76
logical 48
VDM specification language 165
verification 172
weak realism 106-110
Weiss, G. 18
Werner, E.
Wolper, P. 170, 202
Wooldridge, M. 3, 18
world change, rate of 40
z specification language 165