scribing autonomous decision-making.
But, how can rational agents be programmed? Typically, programming
languages for rational agents provide:
˲ a set of beliefs, representing information the agent has;
˲ a set of goals, representing motivations the agent has;
˲ a set of rules/plans, representing
the agent’s mechanisms for achieving
˲ a set of actions, corresponding to
the agent’s external acts (delegated to
other parts of the system); and
A typical agent rule/plan in such a
Goal(eat) : Belief(has_money),
The meaning of this rule is that, if the
agent’s goal is to “eat” and if the agent
believes it has money but does not have
food, then it will set up a new goal to go
to the shop. Once that goal has been
achieved, it will buy some food (
delegated to a subsystem) and then set up
a new goal to get home. Once at home
it will eat and then update its beliefs to
record that it believes it has eaten.
Such languages are essentially rule-based, goal-reduction languages, with
the extra aspect that deliberation, the
ability to change between goals and
change between plan selection strategies at any time, is a core component.
Almost all of these languages are implemented on top of Java, and the large
number of agent platforms now available5, 6 has meant the industrial uptake
of this technology is continually increasing. The key ancestor of most of
today’s agent programming languages
is AgentSpeak, 30 which introduced
the programming of BDI agents using
a modification of Logic Programming.
Of the many descendants of AgentSpeak, we use Gwendolen, 19 which
is based upon Jason, 8 for programming
our rational agents. Consequently, it is
such programs that we directly verify.
A full operational semantics for
Gwendolen is presented in Dennis
and Farwer. 15 Key components of a
Gwendolen agent are a set, Σ, of be-
liefs that are ground first order formu-
lae and a set, I, of intentions that are
stacks of deeds associated with some
event. Deeds include (among other
things) the addition or removal of be-
liefs, the establishment of new goals,
and the execution of primitive actions.
Gwendolen is event driven and events
include the acquisition of new beliefs
(typically via perception), messages,
A programmer supplies plans that
describe how to react to events by extending the deed stack of the intention associated with the event. The
main task of a programmer working in
Gwendolen is defining the system’s
initial beliefs and plans; these then
describe the dynamic behavior of the
agent. A Gwendolen agent executes
within a reasoning cycle that includes
the addition of beliefs from perception, the processing of messages, the
selection of intentions and plans, and
the execution of deeds.
Model Checking Agent Programs.
We begin with program model checking, specifically the Java PathFinder 2
system (JPF2), an open source explic-it-state model checker for Java programs. 26, 36 Since the vast majority of
agent languages are built on top of
Java, we have extended JPF2 to the
Agent JPF (AJPF) system19 incorporating the checking of agent properties.
However, in order to achieve this the
semantics of the agent constructs
used must be precisely defined. Such
semantics can be given using the
Agent Infrastructure Layer (AIL), 16 a
toolkit for providing formal semantics
for agent languages (in particular BDI
languages) built on Java. Thus, AJPF is
essentially JPF2 with the theory of AIL
built in; see Dennis et al. 19
The whole verification and programming system is called MCAPL and
is freely available on Sourceforge.a As
the model checker is based on JPF2,
the modified virtual machine is used to
exhaustively explore all executions of
the system. As each one is explored it is
checked against the required property.
If any violation is found, that execution
is returned as a counterexample.
the key ancestor
of most of today’s
of BDi agents
using a modification