This work introduces CT LAgentSpeak(L), a logic to specify and verify expected properties of rational agents implemented in the AgentSpeak(L) agent oriented programming language. Our approach is similar to the classic BDICT L modal logic, used to reason about agents modelled in terms of belief (BEL), desires (DES), intentions (INTEND). A new interpretation for the temporal operators in CT L: next ( ), eventually ( ), until(U), inevitable(A), etc., is proposed in terms of the transition system induced by the operational semantics of AgentSpeak(L). The main contribution of the approach is a better understanding of the relation between the programming language and its logical speci cation, enabling us to proof expected or desired properties for any agent programmed in AgentSpeak(L), e.g., commitment strategies.
The theory of practical reasoning proposed by Bratman [
Agent oriented programming languages, such as AgentSpeak(L) [13], have
been proposed to reduce the gap between theory (logical speci cation) and
practice (implementation) of rational agents. Even when this programming language
has a well de ned operational semantics, the veri cation of rational properties
of the programmed agents is not evident, since intentional and time modalities
are abandoned for the sake of e ciency. In order to reason about such
properties, we propose CT LAgentSpeak(L) as a logic for speci cation and veri cation of
AgentSpeak(L) agents. The approach is similar to the classic BDICT L [14] logic,
de ned as a BKD45DKDIKD modal system, with temporal operators: next ( ),
eventually ( ), until(U), inevitable(A), etc., de ned after the computational tree
logic (CTL) [
Our main contribution is the de nition of the semantics of the CT L
temporal operators in terms of a Kripke structure, produced by a transition system
de ning the operational semantics of AgentSpeak(L). The semantics of the
intentional operators is adopted from the work of Bordini et al. [
The paper is organized as follows: Section 2 exempli es the speci cation of rational properties in BDICT L [14] with the de nition of commitment strategies. Section 3 introduces the syntax and the semantics of the AgentSpeak(L) agent oriented programming language. Section 4 presents the main contribution of the paper: a logic framework to reason about AgentSpeak(L) agents, with semantics based on the operational semantics of the programming language. Section 5 shows how the commitment strategies introduced in section 2 can be veri ed for AgentSpeak(L). Section 6 o ers concluding remarks and discusses future work. 2
As mentioned, di erent computational theories have been proposed to capture
the theory of Bratman [
Di erent types of commitment strategies de ne di erent types of agents.
Three of them have been extensively studied in the context of BDICT L [14],
where CT L denotes computational tree logic [
) =)
) U BEL( )) (1) { Single-minded commitment. An agent maintains his intentions as long as he believes they are achieved or optionally (E) eventually achievable:
) =)
) U (BEL( ) _ :BEL(E )) (2) { Open-minded commitment. An agent maintains his intentions as long as they are achieved or they are still desired:
) =)
) U (BEL( ) _ :DES(A ))) (3)
For example, a blind agent intending eventually to go to Paris, will maintain his intention, for any possible course of action (inevitable), until he believes he is going to Paris. A single-minded agent can drop such intention if he believes it is not possible any more to go to Paris. An open-minded agent can drop the intention if he does not desire anymore going to Paris. An interesting question is what kind of commitment strategy is followed by AgentSpeak(L) agents?
Furthermore, how can we relate commitment with policy-based
reconsideration in AgentSpeak(L)? Bratman argues that there are three cases of
reconsideration ([
AgentSpeak(L)
In this section, the syntax and semantics of AgentSpeak(L) [13], as de ned for its
interpreter Jason [
ag ::= bs ps bs ::= b1 : : : bn ps ::= p1 : : : pn p ::= te : ct h te ::= +at j at j + g j ct ::= ct1 j > ct1 ::= at j :at j ct1 ^ ct1 h ::= h1; > j > h1 ::= a j g j u j h1; h1 g (n (n 0) 1) at ::= P (t1; : : : ; tn) (n a ::= A(t1; : : : ; tn) (n g ::= !at j ?at u ::= +b j b 0) 0) { ag is an agent program formed by beliefs bs and plans ps. { An agent circumstance C is a tuple hI; E; Ai where I is the set of intentions fi; i0; : : : ; ng s.t. i 2 I is a stack of partially instantiated plans p 2 ps; E is a set of events fhte; ii ; hte0; i0i ; : : : ; ng, s.t. te is a triggerEvent and each i is an intention (internal event) or an empty intention > (external event); and A is a set of actions to be performed by the agent in the environment. { M is a tuple hIn; Out; SIi that works as a mailbox, where In is the mailbox of the agent, Out is a list of messages to be delivered by the agent and SI is a register of suspended intentions (intentions that wait for an answer message). It is not relevant for the purposes of this paper. { T is a tuple hR; Ap; ; ; i that registers temporal information: R is the set of relevant plans given certain triggerEvent; Ap is the set of applicable plans (the subset of R s.t. bs j= ctx); , y register, respectively, the intention, the event and the current plan during an agent execution. { The con guration label s 2 fSelEv; RelP l; AppP l; SelAppl; SelInt; AddIM; ExecInt; ClrInt; P rocM sgg indicates the current step in the reasoning cycle of the agent.
Transitions are de ned in terms of semantic rules of the form: cond (rule id)
C ! C0 where C = hag; C; M; T; si is an AgentSpeak(L) con guration that can be transformed to a new one C0, if the conditions cond hold. Table 2 shows the semantic rules that are relevant for the purposes of this paper (communication processing rules are omitted for simplicity).
SE (CE)=hte;ii (SelEv1) hag;C;M;T;SelEvi !hag;C0;M;T 0;RelP li
T =hte;ii;RelP lans(agps;te)6=fg (Rel1) hag;C;M;T;RelP li !hag;C;M;T 0;AppP li
RelP lans(ps;te)=fg (Rel2) hag;C;M;T;RelP li !hag;C;M;T;SelEvi
ApplP lans(agbs;TR)6=fg (Appl1) hag;C;M;T;ApplP li !hag;C;M;T 0;SelAppli
SO(TAp)=(p; ) (SelAppl) hag;C;M;T;SelAppli !hag;C;M;T 0;AddIMi
T =hte;>i;T =(p; ) (ExtEv) hag;C;M;T;AddIMi !hag;C0;M;T;SelInti
CI 6=fg;SI(CI )=i (SelInt1) hag;C;M;T;SelInti !hag;C;M;T 0;ExecInti
CI =f g (SelInt2) hag;C;M;T;SelInti !hag;C;M;T;P rocMsgi s.t. CE0 = CE n fhte; iig
T 0 = hte; ii s.t. T R0 = RelP lans(agps; te) s.t. T A0p = AppP lans(agbs; TR) s.t. T 0 = (p; ) s.t. CI0 = CI [ f[p ]g s.t. T 0 = i
T =i[head !at;h] (AchvGl) hag;C;M;T;ExecInti !hag;C0;M;T;P rocMsgi s.t. CE0 = CE [ fh+!at; T ig CI0 = CI n fT g
T =[head >] (ClrInt1) hag;C;M;T;ClrInti !hag;C0;M;T;P rocMsgi s.t. CI0 = CI n fT g
T =i[head >] (ClrInt2) hag;C;M;T;ClrInti !hag;C0;M;T;ClrInti s.t. CI0 = (CI n fT g) [ fk[(head0 h) ]g if i = k[head0 g; h] and g = T rEv(head)
T 6=[head >]^T 6=i[head >] (ClrInt3) hag;C;M;T;ClrInti !hag;C;M;T;P rocMsgi
The reasoning cycle of an AgentSpeak(L) agent starts processing messages and updating perception (s = P rocM sg). This adds events to CE (C denotes the element of circumstance C, the same for other element of con gurations) to be processed by the agent. One of these events is selected (SE (CE ) = hte; ii), and relevant and applicable plans are generated using the following de nitions: De nition 1 (Relevant plans) Given a set of plans agps, the subset of relevant plans for a selected event hte; ii 2 CE , is de ned as:
RelP lans(ps; te) = f(p; )jp 2 ps ^ = mgu(te; T rEv(p))g where T rEv(te0 : ctxt h) = te0 gets the trigger event te of a plan, CE denotes the events E in a given circumstance C, and mgu is the most general uni er. De nition 2 (Applicable plans) Given a set of relevant plans TR and a set of beliefs agbs, the set of applicable plans is de ned as:
AppP lans(bs; R) = f(p; 0)j(p; ) 2 R ^ 0 is s.t. bs j= Ctxt(p) 0g where 0 is the substitution computed when verifying if the context of relevant plan p (Ctxt(p)), a ected by its relevant substitution , is a logical consequence of the beliefs of the agent bs.
Then the agent proceeds selecting a relevant plan to form an intention (Appl1 and SelAppl) or, if no relevant plans were found, selecting an intention to be executed (Appl2 and SelInt1). The execution of an intention changes the environment and the mental attitudes of the agent (including the abandoning of accomplished intentions in ClrInt). P rocM sg generates the new events, and so on. Figure 1 shows the transition system induced by these semantic rules. States are labeled with possible values for s. Transitions correspond to the semantic rules identi ers. The initial state is s = P rocM sg.
Although the operational semantics of AgentSpeak(L) clearly de nes the practical reasoning performed by an agent, it is di cult to prove BDI properties, such as the commitment strategies, for any given agent. This is due to the abandon of intentional and temporal modalities in AgentSpeak(L), the main reason to propose CT LAgentSpeak(L). 4
CT LAgentSpeak(L)
CT LAgentSpeak(L) may be seen as an instance of BDICT L. Similar approaches
have been explored for other instances of agent oriented programming languages,
e.g, a simpli ed version of 3APL [
ProcMsg
AchvGl ClrInt3 ClrInt
AddBel DelBel Rel2
Action SelInt
ExecInt
ExtEv IntEv
SelAppl SelAppl
AddIM SelEv
RelPl De nition 3 (BDI syntax) If is an atomic formula in AgentSpeak(L), then , BEL( ), DES( ), INTEND( ) are CT LAgentSpeak(L) well formed formulae (BDI formulae).
De nition 4 (Temporal syntax) Temporal formulae are divided, as usual, in state and path formulae. State formulae are de ned as: s1 Each well formed BDI formula is a state formula. s2 If and are state formulae, ^ and : are state formulae. s3 If is a path formula, then E and A are state formulae.
Path formulae are de ned as: p1 Each state formula is also a path formula. p2 If and are path formulae, then : , formulae. ^ , and
U are path
For example, INTEND(A go(paris)) U :BEL(go(paris; summer), expressing
that the agent will intend inevitably (A) for every course of action, eventually
( ) going to Paris until (U) he does not believe go to Paris in summer, is a well
formed formula.
The semantics of the intentional operators BEL, DES and INTEND is adopted
from Bordini et al. [
BELhag;Ci( )
agbs j= INTENDhag;Ci( ) 2 [ agoals(i) _ i2CI
[ hte;ii2CE agoals(i) DEShag;Ci( )
h+! ; ii 2 CE _ INTEND( )
If the agent ag and his circumstance C are explicit, we simply write BEL( ), DES( ), and INTEND( ). So an agent ag is said to believe the atomic formula , if is a logical consequence of the beliefs bs of ag. An agent is said to intend the atomic formula , if is the subject of an achieve goal in the active intentions of the agent (CI ) or in his suspended intentions associated to events to be processed (CE ). An agent is said to desire the atomic formula , if there is an event in CE which trigger is an achieve goal about or if is intended.
The semantics of the temporal operators: next( ), eventually ( ), and until (U), as well as the path quanti er inevitable (A), required a Kripke structure hS; R; Li where S is a set of states, R is a serial relation on S S and L is a labelling or a valuation function for formulae in the states. The transition system of AgentSpeak(L) induce a Kripke structure: De nition 6 (AgentSpeak(L) Kripke structure) K = hS; R; V i is a Kripke structure speci ed by the transition system ( ) de ning the AgentSpeak(L) operational semantics rules: { S is a set of agent con gurations hag; C; M; T; si. { R S2 is a serial relation s.t. for all (ci; cj ) 2 R, (ci; cj ) 2 or ci = cj . { V is a valuation function over the intentional and temporal operators, de ned after their semantics (see de nitions 5 and 7), e.g., VBEL(c; ) BEL(phi) at the con guration c = hag; C; M; T; si, etc.
As usual, x = c0; : : : ; cn denotes a path in the Kripke structure, i.e., a sequence of con gurations s.t. for all ci 2 S, (ci; ci+1) 2 R. The expression xi denotes the su x of path x starting at con guration ci.
De nition 7 (Temporal semantics) The semantic of the state formulae is de ned for a given current con guration ci 2 K:
K; ci j= BEL( ) ,
2 VBEL(ci; ) K; ci j= INTEND( ) , K; ci j= DES( ) ,
2 VINTEND(ci; ) 2 VDES(ci; ) K; ci j= E K; ci j= A , 9xi9cj i 2 xi s.t. K; cj j= , 8xi9cj i 2 xi s.t. K; cj j= The semantic of the path formulae is de ned as follows:
K; ci j= K; ci j= K; ci j= K; ci j= , K; xi j= ; where U , K; xi+1 j= , 9cj i 2 xi s.t. K; cj j=
, (9ck i s.t. K; xk j= _ (9cj i
K; xj j= ): is a state formula ^ 8ci j<k
K; xj j= )
Observe that the semantics of until corresponds to weak until ( can never occur). Once satisfaction over state and path formulae has been de ned, we can de ne satisfaction and validity over AgentSpeak(L) runs.
De nition 8 (Run) Given an initial AgentSpeak(L) con guration c0, the run K0 denotes the sequence of con gurations c0; c1; : : : such that 8i 1; ci = (ci 1).
De nition 9 (Satisfaction over runs) Given an AgentSpeak(L) run K0 the property 2 CT LAgentSpeak(L) is satis ed if 8i 0; K0 ; ci j= . De nition 10 (Validity) A property 2 CT LAgentSpeak(L) is valid if for any initial con guration K0 ; c0 j= , e.g., if it is satis ed for any run of any agent. 5
Now we proceed to show some properties that expressed in the logical speci cation hold for any AgentSpeak(L) agent. We choose to verify blind and singleminded commitment strategies. In principle, open-minded commitment can be veri ed in a similar way to the single-minded one, but since it is related to emotional aspects of agency more than to policy-based reconsideration (see section 2), it has not been included here. First the no-in nite deferral axiom is veri ed. It expresses that there is no agent that maintains forever his intentions. Proposition 1 An AgentSpeak(L) agent satis es the axiom of no-in nite deferral: INTEND( ) ) A (:INTEND( )).
Proof. Assume K; c0 j= INTEND( ), then given the de nition for INTEND
(de nition 5), there is a plan p 2 CI [ CE with head +! at c0. The
nonin nite deferral axiom expresses that for all runs K0 eventually this plan will
be removed from CI (active intentions) and CE (suspended intentions). While p
is being executed successfully, three runs are possible given the transition rules
ClrIntX 2 (table 2): i) ClrInt3 applies when the body of p is not empty,
nothing is cleaned; ii) ClrInt2 applies when the plan p, with an empty body, is
at the top of an intention i, then p is dropped from i; ClearInt1 applies when
the intention i has only a plan p with and empty body, the whole intention i
is dropped. Given the nite nature of the plans (section 3.1), if everything goes
right, conditions (ii) or (iii) are eventually reached. If something goes wrong with
p, a failure mechanism is activated by an event of the form h ! ; i[p]i resulting
in p being dropped. Although [
Proposition 2 An AgentSpeak(L) agent does not satisfy the axiom of blind commitment.
Proof. Given that AgentSpeak(L) agents satisfy the no-in nite deferral property (proposition 1) and the weak until semantics, the blind commitment axiom is reduced to (a similar reduction is used in Rao et al. [14]):
) ) A BEL( )
Consider an initial con guration c0 s.t. ag = hbs; psi where bs = fg and ps = f+b(t1) : > p(t2): +!p(t2) : > +b(t3):g. Suppose that from perception of the environment a is added agbs = fb(t1)g. An event is generated by this belief update, so that CE = fh+b(t1); >ig. Then following the semantic rules de ning , SelEv1, Rel1, ApplP l1, are applied obtaining a con guration where CI = f[+b(t1) : > !p(t2):]g and CE = fg. Then proceeding with the rules SelAppl, ExtEv, SelInt1, AchvGl a con guration where CE h+!p(t2); +b(t1) : > >i, CI = fg is obtained. At this con guration c0, K; c0 j= DES(p(t2)) (De nition. 5). If we apply then SelEv1, Rel1, AppP l1, SelAppl, a con guration where CI = f[+!p(t2) : > +b(t3):]g and CE = fg, is obtained. In this con guration c00 K; c00 j= INTEND(p(t2)) (De nition. 5). Then proceeding with IntEv, SelInt1, AddBel gets CE = h+b(t3); >i, agbs = fb(t1)g and CI = f[+b(t1) : > > z +!p(t2) : > >] and bs = fb(t1); b(t3)g. The intention about p(t2) is maintained. Observe that the plan bodies in the intention are empty, so the ClrInt rules will discard the whole intention, so that at the next con guration c000, K; c000 j= :INTEND(p(t2)) and K; c000 j= :BEL(p(t2)). By counter-example INTEND(A ( )) =) (A (BEL( )) is not valid.
In fact, our agents do neither satisfy the extended blind commitment axiom
(eq. 1), since the agent did not keep its intention about p(t2) until she believed it.
This reasoning is similar to the demonstration of intention-belief incompleteness
(AT2) for AgentSpeak(L) [
Proposition 3 AgentSpeak(L) agents satisfy a limited single-minded commitment: INTEND(A ) =) A(INTEND(A ) U :BEL(E )).
Proof. This case is similar to the no-in nite deferral demonstration. Assume the agent INTEND(A ) at c0, then there is a plan p 2 CI [ CE with head +! at c0. If there is a con guration ck 0 where :BEL(E ) (the weak until de nition has been adopted), then K; x0;:::;k j= INTEND(A ). Following the no-in nite-deferral demonstration, in the failure cases the agent will eventually satisfy :INTEND( ) because Rel2 which means that for an event hte; i[+! : c h:]i there were not relevant plans and the associated intention will be discarded, e.g., there is not a path of con gurations where eventually , so that it is rational to drop INTENDhag;Ci( ). The case of no-in nite deferral by successful execution of intentions covers the second condition of the weak until :BEL(E ) does not occur.
This is a limited form of single-minded commitement because :BEL(E )
is not represented explicitly by the agent. In fact, the agent can not continue
intending because there are no plans to do it and the full intention fails. It
is also limited because of intention-belief incompleteness that can be avoided
dropping the close world assumption [
Given that, AgentSpeak(L) agents are not blind committed, intentional learning [7{10] provides a third alternative approach to achieve a full singleminded commitment. The idea is that the agents can learn, in the same way they learn the successful adoption of plans as intentions, the reasons behind a plan adoption that lead to an intention failure. In this way a policy-based reconsideration can be approached. 6
We have extended the methodology proposed by Bordini et al. [
Interestingly, the degree of boldness and cautiousness for a given agent is
something hard to de ne. It is well known [
As the example of commitment, reconsideration and learning illustrates, the properties veri ed in this paper are not arbitrary ones. Proving these properties using CT LAgentSpeak(L), prove that they hold for any AgentSpeak(L) agent. This also illustrates the relevance of the speci cation language proposed in this paper, to bring AgentSpeak(L) closer to its philosophical foundation and to extend our computational theories of practical reasoning.
Acknowledgments. The rst and third authors are supported by Conacyt CB2007-1 (project 78910) funding for this research. The second author is supported by Conacyt scholarship 214783. 12. Rao, A.S., George , M.P.: Modelling Rational Agents within a BDI-Architecture.
In: Huhns, M.N., Singh, M.P., (eds.) Readings in Agents, pp. 317{328. Morgan Kaufmann (1998) 13. Rao, A.S.: AgentSpeak(L): BDI agents speak out in a logical computable language.
In: de Velde, W.V., Perram, J.W. (eds.) MAAMAW. LNCS, vol. 1038, pp. 42{55.
Springer, Heidelberg (1996) 14. Rao, A.S., George , M.P.: Decision procedures for BDI logics. Journal of Logic and Computation 8(3), pp. 293{342 (1998) 15. Singh, M.P.: A critical examination of the Cohen-Levesque Theory of Intentions.
In: Proceedings of the European Conference on Arti cial Intelligence (1992). 16. Singh, M.P., Rao, A.S., George , M.P.: Formal Methods in DAI: Logic-Based Representation and Reasoning. In: Multiagent Systems: A Modern Approach to Distributed Arti cial Intelligence, pp. 331{376. MIT Press, Cambridge (1999) 17. Wooldridge, M.: Reasoning about Rational Agents. MIT Press, Cambridge (2000)