John-Jules Ch

Jan Meyer

Andreas Broersen

Herzig

Chapter 10 BDI Logics

This paper presents an overview of so-called BDI logics, logics where the notion of Beliefs, Desires and Intentions play a central role. Starting out from the basic ideas about BDI by Bratman, we consider various formalizations in logic, such as the approach of Cohen and Levesque, slightly remodelled in dynamic logic, Rao & Georgeff's influential BDI logic based on the branching-time temporal logic CTL ⇤ , the KARO framework and BDI logic based on STIT (seeing to it that) logics.

Introduction

In this chapter we present an overview of so-called BDI (for Beliefs, Desires, and Intentions) logics, that is, logics that describe the mental attitudes of intelligent agents in terms of folk-psychological notions of beliefs, desires and intentions. This theory is based on the work of the philosopher Michael Bratman -as with all chapters in his book, references to the literature are provided in the final section. The chapter is organized as follows: we start with some of the basic ideas in Bratman's philosophy, which is about practical reasoning (the reasoning about performing actions) on the basis of the agent's beliefs, desires and, very importantly, intentions, which are special desires to which the agent is committed. Then a number of formalizations of BDI theory in logic is reviewed, the so-called BDI logics. Starting out with Cohen & Levesque's approach, slightly reworked in a dynamic logic setting by Herzig and colleagues. Then we look at Rao & Georgeff's BDI logic, based on the branching-time temporal logic CTL ⇤ . Next we discuss the KARO framework which is based on dynamic logic since its conception. We sketch as a small excursion how the KARO framework, which is devised to capture the behaviour of (rational) intelligent agents, also can be used for describing emotional behaviour of agents. We then present a relatively new approach to BDI, based on so-called STIT (seeing to it that) logic. We finally round off with a conclusion section and a section containing the pointers to all bibliographical references.

Bratman's theory of Belief-Desire-Intention

"What happens to our conception of mind and rational agency when we take seriously future-directed intentions and plans and their roles as inputs into further practical reasoning? This question drives much of this book." This is how the preface of Michael E. Bratman's famous book "Intention, Plans, and Practical Reason" starts. In this book the author lays down the foundations of what later would be called the BDI (Belief-Desire-Intention) theory of agency, a folk-psychological theory of how humans make decisions and take action (referred to as practical reasoning after Aristotle), and which would lead to a new computing paradigm, agent-oriented programming or agent technology more in general, when AI researchers started to apply it to the specification and implementation of artificial agents.

The main new ingredient in Bratman's theory is that of intention. Beliefs and desires were already known to be of importance in human behaviour. For instance, Daniel Dennett's intentional stance, the strategy of interpreting the behaviour of an entity by treating it as if it were a rational agent that governed its choice of action by a consideration of its beliefs and desires, already mentions the role of beliefs and desires in 1987. But Bratman claims that to fully understand the practical reasoning of humans also the notion of intention is needed. An intention is not just a mere desire but something the agent is committed to, that is, not given up too soon by the agent. For instance, if I have an intention to give a lecture in Amsterdam tomorrow, it is not a mere wish to do so, but I'm really taking measures (making plans, e.g., cancelling other plans or making sure my laptop will be in my bag) to do it and unless something happens that seriously interferes with my intention to give that lecture tomorrow, I really will do so. Thus Bratman takes intention to be a first-class citizen, and not something that can be reduced to beliefs and desires. In other words, a reduction of intention to a theory of only beliefs and desires is rejected by Bratman. Another important notion in Bratman's theory is that of a plan. As he explains, rational agents need plans for two reasons. First of all, agents need to "allow deliberation and rational reflection to influence action beyond the present", since agents have only limited resources (including time) to deliberate at the time of action. Secondly agents need to coordinate their actions, both on an intrapersonal and a interpersonal level, and plans help agents with that, too. As to the relation between plans and intentions, Bratman says that 'our intentions concerning our future actions are typically elements in larger plans'. Bratman focuses on future-oriented intentions.Suchintentionsdifferfrompresent-directedintentions, alias intentions-in-action, which accompany an agent's actions (more precisely, an agent's intentional actions), and pertain to what to do beginning now.

To explain the differences between beliefs, desires and intentions Bratman introduces the notion of a pro-attitude.Apro-attitudeis anagent's mentalattitude directed toward an action under a certain description. It plays a motivational role. So desires and intentions are both pro-attitudes while beliefs typically are not. But although desires and intentions are both pro-attitudes they differ. Intentions are conduct-controlling pro-attitudes, while ordinary desires are merely potential influences of action. The 'volitional'dimensionof the commitmentinvolved in future-directed intentions comes from the conduct-controlling nature of intentions: as a conduct-controlling pro-attitude an intention involves a special commitment to action that ordinary desires do not.

Besides identifying intentions as conduct-controlling pro-attitudes, Bratman argues that intentions also have other properties: they have inertia and they serve as inputs into further practical reasoning. By the former is meant that intentions resist reconsideration. This has to do again with the resource-boundedness of realistic cognitive agents. The agent normally simply lacks the time to compute, at any given time, the optimal plan of action given his beliefs and desires, so it has to form future-directed intentions and store them in his mental agenda and use them to avoid computing plans all the time. Once an intention has been formed (and a commitment to action has been made) the intention will normally remain intact until the time of action: it has a characteristic stability / inertia. By this Bratman means that intentions made influence further reasoning about (decisions about) action, where also refinements of intentions (intentions to do more concrete actions) may play a role. For example, if I have the intention to speak in Amsterdam tomorrow, I can form a more refined intention to take the car driving to Amsterdam in order to speak. As a consequence after the second intention it won't be rational anymore to consider time tables for trains going to Amsterdam, while it was so after the first intention. All this has led to seeing intentions as distinctive states of mind, distinct from beliefs and desires, and to a belief-desire-intention model rather than a desire-belief model of practical reasoning.

As we have seen, Bratman describes how prior intentions and plans provide a filter of admissibility on options. This is what later by Cohen & Levesque has been called a 'screen of admissibility'. The basis of this role of intentions in further practical reasoning is the need for consistency in one's web of intentions and beliefs, as Bratman calls it: other things being equal, it should be possible for me to do all that I intend in a world in which my beliefs are true. But as Bratman explains this is not as simple as it looks. In particular "not every option that is incompatible with what the agent already intends and believes is inadmissible." In short, it depends on whether beliefs can be forced to be changed by the new intention so that the inconsistency disappears or not. In the former case the new intention is admissible, in the latter it is not.

In Bratman's view there is an intrinsic relation between intentions and plans. Plans are intentions. They share the properties of intentions: they resist reconsideration and have inertia, they are conduct controllers and not merely conduct influencers, and they provide crucial inputs for further practical reasoning and planning. But they have increased complexity as compared to simple intentions: they are typically partial in the sense of incomplete (typically I have a partial plan to do something and fill in the details later) and have a hierarchical structure (plans concerning ends embed plans concerning means and preliminary steps, and more general intentions embed more specific ones).

To sum it up, according to Bratman, future-oriented intentions have the following characteristics:

• An intention is a high-level plan.

• An intention guides deliberation and triggers further planning: it typically leads to the refinement of a high-level plan into a more and more precise plan.

• An intention comes with the agent's commitment to achieve it.

• An agent abandons an intention only under the following conditions:

the intention has been achieved;

he believes it is impossible to achieve it;

he abandons another intention for which it is instrumental.

Let us illustrate Bratman's future-oriented intentions by an example. Suppose we are in autumn and I desire to go to Paris next spring. Under certain conditions -such as the importance of that desire and my beliefs about its feasibility-, that desire will make me form an intention to travel to Paris next spring. This is a very high-level plan: I do not settle the exact dates, I do not decide by which means of transportation I am going to go to Paris, and I do not know where to stay yet. I am however committed to that plan: during the following months I will stick to my intention to go to Paris, unless I learn that it is impossible to go to Paris in spring (say because my wife wants to spend our spring holidays in Spain, or because I changed my mind due to an invitation to give a talk at an important conference).

During the next months I am going to refine my high-level plan: I will decide to go on a particular weekend, I will decide to go by train and not by plane, and I will book a hotel for the weekend under concern. This more elaborated plan is going to be refined further as time goes by: I decide to take the 7am train and not the 9am train, and I decide to go to the train station by metro and not by taxi, etc. Finally, once I have spent that weekend in Paris I no longer pursue that goal and drop it. Bratman's theory might be called semi-formal: while he isolates the fundamental concepts and relates them, he does not provide a formal semantics. This was both undertaken by Phil Cohen and Hector Levesque and, more or less at the same time, by Anand Rao and Michael Georgeff. In the next section we will go into the details of how they casted Bratman's theory into a logic of intention and we presen t some subsequen t modifications and extensions of their original logic. This will be followed by a section on Rao and Georgeff's approach.

Cohen and Levesque's approach to intentions

We have seen that the concepts of belief, desire, time and action play an important role in Bratman's theory of intention. A logical analysis of that theory should involve combining a logic of belief, a logic of desire, a logic of time and a logic of action.

Belief, time, and action play a fundamental role in Cohen and Levesque's logic. However, the concept of desire is somewhat neglected: Cohen and Levesque rather base their logic on the concept of realistic preference. The latter can be viewed as adesirethat has alreadybeenfiltered bytheagent'sbeliefsaboutits realisability. This is highlighted by the property that belief implies realistic preference: when Iam convinced that ' is true then I also have to prefer that ' is true. (I might however prefer that ' be false at some point in the future.)

Cohen and Levesque's analysis amounts to a reduction of the concept of intention to those of belief, realistic preference, time and action: they define intention in terms of the latter four concepts. The reader may note that this is actually asurprisingmove, giventhat Bratman had stronglyargued that intentionsare independent of desires and cannot be reduced to them.

In the next two sections we present the four building blocks of Cohen and Levesque's logic, grouping together action and time on the one hand, and belief and realistic preference on the other.

Action and time

The basic building block of Cohen and Levesque's logic is a linear version of propositional dynamic logic PDL. The semantics of linear PDL allows to also interpret the temporal operators of linear-time temporal logic LTL. where ⇡ is an action. The formula Poss ⇡ ' reads "there is a possible execution of ⇡ after which ' is true". 1 This reading highlights that the standard version of PDL allows for several possible executions of ⇡ in order to account for indeterminism.

Standard PDL

While Poss ⇡ quantifies existentially over the executions of ⇡,thedualmodal operator After ⇡ quantifies universally. It is definable from Poss ⇡ as follows:

After ⇡ ' = def ¬Poss ⇡ ¬'
Let us consider the case where ' is truth > or falsity ?: Poss ⇡ > has to be read "⇡ is executable", while After ⇡ ? has to be read "' is inexecutable". The semantics of PDL is based on transition systems where an atomic action i:↵ can be interpreted as a set of edges. Such a transition system is a pair hW, Ri where W is a non-empty set of possible worlds and R maps every action ⇡ to an accessibility relation R ⇡ ✓ W ⇥ W relating possible worlds. An edge from world w to world u that is labeled ⇡ means that it is possible to execute ⇡ in w and that u is a possible outcome world when ⇡ is executed. The set of all these ⇡ edges makes up the accessibility relation R ⇡ interpreting the action ⇡.

A PDL model is a transition system together with a valuation V mapping atomic formulas p from the set of propositional variables P to their extension V (p) ✓ W , i.e., to the set of worlds V (p) where p is true.

Models allow to give truth values to formulas. In particular, Poss ⇡ ' is true at a world w if there is a couple (w, w 0 ) in R ⇡ such that ' is true at world w 0 :

M, w |= Poss ⇡ ' iff there is a u 2 W such that wR ⇡ u and M, u |= '
The formula Poss ⇡ ' therefore expresses a weak notion of ability: the action ⇡ might occur and ' could be true afterwards.

Linear PDL Probably Cohen and Levesque were the first to adapt PDL in order to model actual agency. The modalities are interpreted in linear PDL models. In such models, for every possible world w there is at most one successor world u that is temporally related to w. The accessibility relation linking w to u may be labelled by several atomic actions. Formally, a transition system hW, Ri is linear if for every world w 2 W such that hw, u 1 i 2 R ⇡1 and hw, u 2 i 2 R ⇡2 we have u 1 = u 2 . An edge from world w to world u that is labeled ⇡ means that ⇡ is executed in w and that u will be the result. (The reader might note the difference with the above standard PDL.) This allows for the simultaneous performance of two different actions; they must however lead to the same outcome world. The models of linear PDL are the class of linear transition systems.

In order to distinguish the modal operators of actual action from the modal operators of possible action we write the former as Happ ⇡ ', read "⇡ is going to be performed, and ' is true afterwards". Just as After ⇡ is the dual of Poss ⇡ , we define a modal operator IfHapp ⇡ that is the dual of Happ ⇡ by stipulating:

IfHapp ⇡ ' def = ¬Happ ⇡ ¬'
Happ ⇡ ' and IfHapp ⇡ ' say different things: the first formula says that ⇡ is executable and that ' is true after it, while the second says that if ⇡ is executable then ' is true after it. The former should therefore imply the latter.

The truth condition for Happ ⇡ is:

M, w |= Happ ⇡ ' iff there is a u 2 W such that wR ⇡ u and M, u |= '
So it has exactly the same form as that for Poss ⇡ . We changed the name of the modal operator in order to better suit the linearity of the models.

The following axiom schema characterises linear PDL models:

(Happ i:↵ > ^Happ j:↵ 0 ') ! Happ i:↵ ' (10.1)
Beyond atomic events, PDL also has complex events such as sequential and nondeterministic composition, test, and iteration. We will however not refer to them in our present introduction.

Cohen and Levesque's logic has the temporal operators "eventually" (noted F), "henceforth" (noted G), and "until" (noted U). These operators are interpreted in linear PDL models in the obvious way. Let us give the truth condition for the 'eventually" operator, for example: M, w |= F' iff there is an integer n and there are v

1 , . . . , v n 2 W such that v 1 = w, hv k , v k+1 i 2 R ⇡ k for some ⇡ k , and M, v n |= '
Cohen and Levesque also need existential quantification over actions. We here present their account in terms of an operator fusing existential quantification 9 over events ↵ with the dynamic operator Happ i:↵ . Its truth condition is as follows:

M, w |= 9↵Happ i:↵ ' iff there are ↵ 2 A, u 2 W such that hw, ui 2 R i:↵ and M, u |= '

Belief and preference

Cohen and Levesque's account of belief is standard, while their account of preference is in terms of the somewhat unusual notion of strong realistic preference.

Belief Cohen and Levesque have modal operators of belief Bel i , one per agent i.

The modal logic of each of these operators is the standard logic of belief KD45 (see also Chapter 1 of this handbook). Such operators can be interpreted if we add accessibility relations B i to the transition systems of linear PDL, one per agent i. The set of worlds B i (w) = {u : hw, ui 2 B i } is the set of those worlds that are possible for agent i at world w: the set of worlds that are compatible with his beliefs at w. In order to be an accessibility relation for KD45, each of these relations has to satisfy the following constraints:

• for every w 2 W there is at least one u 2 W such that hw, ui 2 B i (seriality);

• if hw, ui 2 B i and hu, vi 2 B i then hw, vi 2 B i (transitivity);

• if hw, ui 2 B i and hw, vi 2 B i then hu, vi 2 B i (Euclideaness).
These constraints make that the following implications become valid:

• Bel i ' ! ¬Bel i ¬' (consistency of belief, axiom D) • Bel i ' ! Bel i Bel i ' (positive introspection, axiom 4) • ¬Bel i ' ! Bel i ¬Bel i ' (negative introspection, axiom 5)
Preference For Cohen and Levesque, intentions are particular strong realistic preferences. The latter are true in a subset of the worlds that are doxastically possible for an agent. There is a modal operator Pref i , one per agent i, and the formula Pref i ' reads "i chooses ' to be true". 2 Such a notion of preference is strongly realistic in the sense that belief logically implies preference. Semantically, strong realistic preference can be modelled by accessibility relations P i , one per agent i 2 I, such that P i ✓ B i . The latter constraint implements realism: a world that is compatible with agent i's preferences cannot be incompatible with i' beliefs. In other words, at world w agents have to select their preferred worlds among the worlds that are epistemically possible for them at w.

The logic of action, time, belief, and preference

Let us sum up Cohen and Levesque's semantics. A frame is a quadruple M = hW, R, B, Pi where

• W is a non-empty set of possible worlds;

• R : (I ⇥ A) ! (W ⇥ W ) maps actions ⇡ to accessibility relations R ⇡ ;

• B : I ! (W ⇥ W ) maps agents i to accessibility relations B i ;

• P : I ! (W ⇥ W ) maps agents i to accessibility relations P i ;

These frames have to satisfy the following constraints:

• hW, Ri is a linear transition system;

• every B i is serial, transitive and Euclidean;

• P i ✓ B i , for every i 2 I.
Let us call CL that class of frames. As usual, a model is a frame together with a valuation V : P ! 2 W mapping atomic formulas p to their extension V (p) ✓ W . Validity and satisfiability in CL frames are defined as usual.

We are now ready to formulate Cohen and Levesque's reduction of intention.

Defining intention

Cohen and Levesque define a modal operator of intention by means of a cascade of definitions. We here reproduce them in a slightly simplified form. We then discuss them and finally comment on the modifications.

1. i has the achievement goal that ' if i prefers that ' is eventually true and believes that ' is currently false. Formally:

AGoal i ' def = Pref i F' ^Bel i ¬'
2 Cohen and Levesque's original notation is Goali instead of Prefi (while they actually refer to it in their title as 'choice'). We moved to our notation in order to avoid confusion with the concept of choice in STIT theory.

BRATMAN'S THEORY OF BELIEF-DESIRE-INTENTION

2. i has the persistent goal that ' if i has the achievement goal that ' and will keep that goal until it is either fulfilled or believed to be out of reach. Formally:

PGoal i ' def = AGoal i ' ^(AGoal i ') U (Bel i ' _ Bel i G¬')
3. i has the intention that ' if i has the persistent goal that ' and believes he can achieve ' by an action of his. This requires to quantify over i's actions by means of the fused operator quantifying over events. Formally:

Intend i ' def = PGoal i ' ^Bel i F 9↵ Happ i:↵ '
Some valid and invalid principles for intention Cohen and Levesque's construction guarantees several desirable properties and avoids some that are unwanted. Here are two of them. First, i's intention that ' logically implies i's belief that ¬'. Formally this writes:

Intend i ' ! Bel i ¬' Second, the formula schema Bel i (' ! ) ! (Intend i ' ! Intend i ) is in- valid: i's intention
that ' together with i's belief that ' implies does not logically imply i's intention that . This is crucial both for Bratman and for Cohen and Levesque. Here is a famous example illustrating why the principle should not be valid: if I intend to go to the dentist and believe that going to the dentist will cause pain then I do not necessarily intend to have pain. This is called the Side-Effect-Free Principle by Su et al. They have proposed a logic with a semantics in terms of linear neighbourhood structures (instead of accessibility relations) in order to interpret a modal operator of preference. Such structures allow to validate the principle of consistency of beliefs and intentions (Bel i ' ! ¬Pref i ¬') while guaranteeing the Side-Effect-Free Principle. The price for that is that preference no longer satisfy the monotony axiom Pref i (' ^ ) ! (Pref i ' ^Pref i ).

Comments on the simplifications

We have simplified the definition of a persistent goal. Cohen and Levesque's original definition allows agents to abandon a persistent goal for some other, superior reason. Their definition is

PGoal i ' def = AGoal i ' ^(AGoal i ') U (Bel i ' _ Bel i G¬' _ )
where is an unspecified condition accounting for that other reason.

This definition stipulates that a persistent goal ' is also abandoned if some other condition becomes true. This leaves room for the abandonment of persistent goals that are instrumental for some goal that obtains without the agent's intervention. A classical example is a student i coming back late in the night to the dorms who forgot to take the key of the entrance door: his overall goal is to be able to get into the building and he starts to plan to climb over the wall ('), but then some other student who also comes home late happens to pass just in front of him and opens the door ( ), thus enabling i to drop '. Hence, i abandons his persistent goal ' although it has neither been achieved nor turned out to be impossible.

Dealing with such a general condition however makes it difficult to go beyond specific cases.

Variants and extensions

We now overview an extension of the basic logic, together with several alternatives to Cohen and Levesque's incremental definition of intention.

Introspection of intention Cohen and Levesque do not assume principles of positive and negative introspection of preference. However, they seem natural in the following form

• Pref i ' ! Bel i Pref i ' • ¬Pref i ' ! Bel i ¬Pref i '
They correspond to the following constraints on the accessibility relations for preference and belief:

• if hw, ui 2 B i and hu, vi 2 P i then hw, vi 2 P i ;

• if hw, ui 2 B i and hw, vi 2 P i then hu, vi 2 P i . This allows to prove principles of positive and negative introspection of goals, achievement goals, persistent goals, and intention. For instance, they validate Intend i ' ! Bel i Intend i ' and ¬Intend i ' ! Bel i ¬Intend i '. For example, both when I intend to go to Paris and when I don't intend to go to Paris then I am aware of this.

Weakly realistic preference Sadek has argues for a slightly different notion of realistic preference. The latter does not demand that all preference-accessible worlds be in the set of belief-accessible worlds, but only requires that they have a non-empty intersection. (This is sometimes called weak realism, as opposed to Cohen and Levesque's strong realism.) In frames that are weakened in this way the somewhat counterintuitive principle Bel i ' ! Pref i ' is no longer valid. Instead, the weaker Bel i ' ! ¬Pref i ¬' is valid, which can be reformulated as

¬(Bel i ' ^Pref i ¬')
It says that one cannot simultaneously believe that ' and prefer that ¬'.

An epistemic version of achievement goals Herzig and Longin have advocated a different definition of an achievement goal. It is weaker than Cohen and Levesque's in that they only require that i does not believe that ' is currently true (instead of i's belief that ' is currently false). It is stronger in that they replace i's goal that ' will be true by i's goal that ' will be believed. This gives the following definition:

AGoal w i ' def = Pref i F Bel i ' ^¬Bel i '

BRATMAN'S THEORY OF BELIEF-DESIRE-INTENTION

They start by arguing for the replacement of Pref i F' by Pref i FBel i '.Asthey point out, it is the raison d'être of an intention to be abandoned at some stage, and an agent can only do so if he believes that he has achieved that goal. So the agent's goal cannot just be that ' be true, but should be that he bel ieves that ' is true.

Using the same reasons they then argue for the replacement of Bel i ¬' by ¬Bel i ': as long as ' is not believed to be true the agent should stick to his achievement goal ',so¬Bel i ' is better in line with this than Bel i ¬'. They illustrate the first replacement by a variant of the Byzantine generals example. Let r mean that a message of general i has been received by general j.Supposei initially believes that j has not received the message yet, i.e., Bel i ¬r.Supposemoreoverthati believes that he will actually never know whether j received the message or not, i.e., Bel i G(¬Bel i r ^¬Bel i ¬r). (This differs from the original Byzantine generals example, where it is possible that the messengers get through and where it is just possible for i that he will never know.) If we express i's achievement goal that r as Pref i F r then Cohen and Levesque make us conclude that AGoal i r,i.e.,i has the achievement goal that ' although he believes that he will never be able to abandon that goal. In contrast, if we express i's achievement goal that r as Pref i F Bel i r then we have ¬AGoal i w r: i cannot have the achievement goal that r. 3

Weaker link between action and goal Sadek and Bretier point out that the definition of intention is too strong in particular in cooperative situations where agent i's action need not directly achieve his goal ':itis enoughthati triggers a subsequent action of another agent j which will achieve i's goal. Their modification can be formulated as follows:

Intend i ' = def PGoal i ' ^ Pref i F(9↵Happ i:↵ F')
Stronger commitment Sadek and Bretier also discuss a stronger definition of intention where the agent is committed to do all he can to achieve his goal.

They express this by a universal quantification over events. 4 We formulate their definition as follows:

Intend i ' = def PGoal i ' ^ Pref i 8↵(Bel i Happ i:↵ F' ! Pref i F Happ i:↵ >)
That definition was criticised in the literature, in particular by Herzig and Long, as being too strong. Indeed, it postulates that agents want to achieve their intentions by all possible means, including illegal actions and actions with a huge cost for them. For example, it might commit me to steal a car if this is the only means to go to Paris on that spring weekend (say because there is a train strike).

Attempts Lorini and Herzig complement Cohen and Levesque's approach by integrating the concept of an attempt to perform an action. The motivation is that

Bel ditio r n ) ¬ imp Bel lies i' bec Pref ause t Bel he r lo ,w gic hic of h bel iG ¬ i ^ ¬ i¬ ¬ iF i
is the negation of the first condition.

intentions typically make an agent try to perform an action, while the successful performance of that action is not guaranteed. The central principle there is "can and attempts implies does" : if i intends to (attempt to) perform ↵ and ↵ is feasible then ↵ will indeed take place. This requires a logic with both modal operators of possible action Poss ⇡ and modal operators of actual action Happ ⇡ .

Conclusion

Cohen and Levesque succeeded in providing a fine-grained analysis of intention by relating that concept to action, belief and realistic preference. A central point in Bratman's theory their logic does not account for is the refinement of intentions.

According to Bratman, an agent starts by forming high-level intentions such as going to Paris in a month, and as time goes by he makes that intention more precise: he first starts to intend to go to Paris by train and not by plane; at a later stage he decomposes the intention to go to Paris by train into the intention to take a taxi to the train station (instead of a bus), then take the TGV to Paris, and then take the metro. It is probably an interesting direction of future research to integrate intention refinement mechanisms e.g. by resorting to dynamic epistemic logics (see Chapter 6).

Rao & Georgeff 's BDI logic

As mentioned earlier, besides Cohen and Levesque, also Rao and Georgeff, more or less at the same time, published a formalisation of the ground-breaking work of Bratman on the philosophy of intelligent (human) agents. As we have seen, Bratman made a case for the notion of intention besides belief and desire, to describe the behaviour of rational agents. Intentions force the agent to commit to certain desires and to really 'go for them'. So focus of attention is an important aspect here, which also enables the agent to monitor how s/he is doing and take measures if things go wrong. Rao & Georgeff stress that in the case of resourcebounded agents it is imperative to focus on desires / goals and make choices. This was also observed by Cohen & Levesque, who try to formalize the notion of intention in a linear-time temporal logic (or, as we have seen in the previous section, a linear version of dynamic logic) in terms of the notion of a (persistent) goal.

Here we treat Rao & Georgeff's approach who base it on branching-time temporal logic framework CTL ⇤ to give a formal-logical account of BDI theory. The reader may also like to look at Chapter 5 of this book, the chapter that relates knowledge and time. Like Cohen & Levesque's approach, BDI logic has influenced many researchers (including Rao & Georgeff themselves) to think about architectures of agent-based systems in order to realize these systems. Rao & Georgeff's BDI logic is more liberal than that of Cohen & Levesque in the sense that they a priori regard each of the three attitudes of belief, desire and intention as primitive: they introduce separate modal operators for belief, desire and intention, and then study possible relations between them.

(The language of) BDI logic is constructed as follows. Two types of formulas are distinguished: state formulas and path formulas. We assume some given first-order signature. Furthermore, we assume a set E of event types with typical element e. The operators BEL, GOAL, INTEND have as obvious intended reading the belief, goal and intention of an agent, respectively, while U, ⇧, O are the usual temporal operators, viz. until, eventually and next, respectively. Definition 10.1 (State and path formulas)

1. The set of state formulas is the smallest closed under:

• any first-order formula w.r.t. the given signature is a state formula

• if ' 1 and ' 2 are state formulas then also ¬' 1 , ' 1 _ ' 2 , 9x' 1 (x) are state formulas
• if e is an event type, then succeeded(e), failed(e) are state formulas

• if ' is a state formula, then BEL('), GOAL('), INT END(') are state formulas • if is a path formula, then optional( ) is a state formula 2.
The set of path formulas is the smallest set closed under:

• any state formula is a path formula

• if 1 , 2 are path formulas, then ¬ 1 , 1 _ 2 , 1 U 2 , ⇧ 1 , O 1 are path formulas a
State formulas are interpreted over a state, that is a (state of the) world at a particular point in time, while path formulas are interpreted over a path of a time tree (representing the evolution of a world). In the sequel we will see how this will be done formally. Here we just give the informal readings of the operators.

The operators succeeded and failed are used to express that events have (just) succeeded and failed, respectively. Next there are the modal operators for belief, goal and intend. (In the original version of BDI theory, desires are represented by goals, or rather a GOAL operator. In a later paper the GOAL operator was replaced by DES for desire.) The optional operator states that there is a future (represented by a path) where the argument of the operator holds. Finally, there are the familiar (linear-time) temporal operators, such as the 'until', 'eventually' and 'nexttime', which are to be interpreted along a linear time path.

Definition 10.2

The following abbreviations are defined: The 'always' operator is the familiar one from (linear-time) temporal logic. The 'inevitability' operator expresses that its argument holds along all possible futures (paths from the current time). The 'done' operator states that an event occurs (action is done) no matter whether it is succeeding or not. The final three operators state that an event succeeds, fails, or is done iff it is inevitable (i.e. in any possible future) it is the case that at the next instance the event has succeeded, failed, or has been done, respectively (note that this means that an event, succeeding or failing, is supposed to take one unit of time).

1. 2 = ¬ ⇧ ¬ (always) 2. inevitable( ) = ¬optional(¬ )

Definition 10.3 (Semantics)

The semantics is given w.r.t. models of the form M = hW, E, T, , U , B, G, I, i, where

• W is a set of possible worlds • E is a set of primitive event types • T is a set of time points
• is a binary relation on time points, which is serial, transitive and backwards linear The semantics of BDI logic, Rao & Georgeff-style, is rather complicated. Of course, we have possible worlds again, but as we will see below, these are not just unstructured elements, but they are each time trees, describing possible flows of time. So, we also need time points and an ordering on them. As BDI logic is based on branching time, the ordering need not be linear in the sense that all time points are related in this ordering. However, it is stipulated that the time ordering is serial (every time point has a successor in the time ordering), the ordering is transitive and backwards-linear, which means that every time point has only one direct predecessor. The accessibility relations for the 'BDI'-modalities are standard apart from the fact that they are also time-related, that is to say that worlds are (belief/goal/intend-)accessible with respect to a time point. Another way of viewing this is that -for all three modalities -for every time point there is a distinct accessibility relation between worlds.

• U is the universe of discourse
In order to obtain reasonable properties for beliefs, desires and intentions, a number of constraints on the accessibility relations are stipulated. First of all, a world / time point compatibility requirement is assumed for all of the B, G, I accessibility relations: for R = B, G, I: If w 0 2 R(w , t) then t 2 w and t 2 w 0 where R(w, t) = {w 0 | R(w, t, w 0 )} for R = B, G, I. This requirement is needed for the semantic clauses for the BEL, GOAL and INTEND modalities that we will give below to work. And next there are the usual requirements of the B accessibility relation to satisfy seriality, transitivity and Euclideaness in order to obtain the familiar KD45 properties of belief: beliefs are consistent, and satisfy positive and negative introspection. As to the G and I accessibility relations we require seriality in order to obtain the well-known KD property of consistent goals and intentions.

Next we elaborate on the structure of the possible worlds. As announced before, a possible world itself is a time tree, a temporal structure representing possible flows of time. The definition above is just a technical one stating that the time relation within a possible world derives naturally from the a priori given relation on time points. Furthermore it is indicated by means of the functions S w and F w how events are associated with adjacent time points. Now we come to the formal interpretation of formulas on the above models. Naturally we distinguish state formulas and path formulas, since the former should be interpreted on states whereas the latter are interpreted on paths. In the sequel we use the notion of a fullpath: a fullpath in a world w is an infinite sequence of time points such that, for all i, (t i , t i+1 ) 2 A w . We denote a fullpath in w by (w t0 , w t1 , . . .), and define fullpaths(w) as the set of all fullpaths occurring in world w (i.e., all fullpaths that start somewhere in the time tree w).

Definition 10.5 (Interpretation of formulas)

The interpretation of formulas w.r.t. a model M = hW, E, T, , U , B, G, I, i is now given by: 1. (state formulas)

• M, v, w t |= q(y 1 , . . . , y n ) iff (v(y 1 ), . . . , v(y n )) 2 (q, w, t) • M, v, w t |= ¬' iff M, v, w t 6 |= ' • M, v, w t |= ' 1 _ ' 2 iff M, v, w t |= ' 1 or M, v, w t |= ' 2 • M, v, w t |= 9x' iff M, v{d/x}, w t |= ' for some d 2 U • M, v, w t0 |= optional( ) iff exists fullpath (w t0 , w t1 , . . .) such that M, v, (w t0 , w t1 , . . .) |= • M, v, w t |= BEL(') iff for all w 0 2 B(w, t) : M, v, w 0 t |= ' • M, v, w t |= GOAL(') iff for all w 0 2 G(w, t) : M, v, w 0 t |= ' • M, v, w t |= IN T EN D(') iff for all w 0 2 I(w, t) : M, v, w 0 t |= ' • M, v,
• M, v, (w t0 , w t1 , . . .) |= ' iff M, v, w t0 |= ', for ' state formula • M, v, (w t0 , w t1 , . . .) |= O' iff M, v, (w t1 , w t2 , . . .) |= ' • M, v, (w t0 , w t1 , . . .) |= ⇧' iff M, v, (w tk , . . .) |= ' for some k 0 • M, v, (w t0 , w t1 , . . .) |= 1 U 2 iff
either there exists k 0 such that M, v, (w tk , . . .) |= 2 and for all 0  j < k : M, v, (w tj , . . .) |= 1 , or for all j 0 : M, v, (w tj , . . .) |= 1 Most of the above clauses should be clear, including those concerning the modal operators for belief, goal and intention. The clause for the 'optional' operator expresses exactly that optionally is true if is true in one of the possible futures represented by fullpaths starting at the present time point. The interpretation of the temporal operators is as usual.

Rao & Georgeff now discuss a number of properties that may be desirable to have as axioms. In the following we use ↵ to denote so-called O-formulas, which are formulas that contain no positive occurrences of the 'inevitable' operator (or negative occurrences of 'optional") outside the scope of the modal operators BEL, GOAL and IN T EN D.

1. GOAL(↵) ! BEL(↵) 2. IN T EN D(↵) ! GOAL(↵) 3. IN T EN D(does(e)) ! does(e) 4. IN T EN D(') ! BEL(IN T EN D(')) 5. GOAL(') ! BEL(GOAL(')) 6. IN T EN D(') ! GOAL(IN T EN D(')) 7. done(e) ! BEL(done(e)) 8. IN T EN D(') ! inevitable ⇧ (¬IN T EN D('))
In order to render these formulas validities further constraints should be put on the models, since in the general setting above these are not yet valid.

For reasons of space we only consider the first two. In order to define constraints on the models such that these two become valid, we introduce the relation on worlds, as follows: w 00 w 0 , fullpaths(w 00 ) ✓ fullpaths(w 0 ). So w 00 w 0 means that there the world (time tree) w 00 represents less choices than w 0 .

BRATMAN'S THEORY OF BELIEF-DESIRE-INTENTION

Now we define the B-G condition as the property that the following holds: 8w 0 2 B(w, t)9w 00 2 G(w, t):w 00 w 0 Informally, this condition says that for any belief accessible world there is a goal accessible world that contains less choices. It is now easy to show the following proposition. Let us now consider the properties deemed desirable by Rao & Georgeff again. The first formula describes Rao & Georgeff's notion of 'strong realism' and constitutes a kind of belief-goal compatibility: it says that the agent believes he can optionally achieve his goals. There is some controversy on this. Interestingly, but confusingly, Cohen & Levesque adhere to a form of realism that renders more or less the converse formula BELp ! GOALp. But we should be careful and realize that Cohen & Levesque have a different logic in which one cannot express options as in the branching-time framework of Rao & Georgeff. Furthermore, it seems that in the two frameworks there is a different understanding of goals (and beliefs) due to the very difference in ontologies of time employed: Cohen & Levesque's notion of time could be called 'epistemically nondeterministic' or 'epistemically branching', while 'real' time is linear: the agents envisage several future courses of time, each of them being a linear history, while in Rao & Georgeff's approach also 'real' time is branching, representing options that are available to the agent.

The second formula is a similar one to the first. This one is called goal-intention compatibility, and is defended by Rao & Georgeff by stating that if an optionality is intended it should also be wished (a goal in their terms). So, Rao & Georgeff have a kind of selection filter in mind: intentions (or rather intended options) are filtered / selected goals (or rather goal (wished) options), and goal options are selected believed options. If one views it this way, it looks rather close to Cohen & Levesque's 'Intention is choice (chosen / selected wishes) with commitment', or loosely, wishes that are committed to. Here the commitment acts as a filter.

The third one says that the agent really does the primitive actions that s/he intends to do. This means that if one adopts this as an axiom the agent is not allowed to do something else (first). (In our opinion this is rather strict on the agent, since it may well be that postponing its intention for a while is also an option.) On the other hand, as Rao & Georgeff say, the agent may also do things that are not intended since the converse does not hold. And also nothing is said about the intention to do complex actions.

The fourth, fifth and seventh express that the agent is conscious of its intentions, goals and what primitive action he has done in the sense that he believes what he intends, has as a goal and what primitive action he has just done.

The sixth one says something like that intentions are really wished for: if something is an intention then it is a goal that it is an intention.

The eighth formula states that intentions will inevitably (in every possible future) be dropped eventually, so there is no infinite deferral of its intentions. This leaves open, whether the intention will be fulfilled eventually, or will be given up for other reasons. Below we will discuss several possibilities of giving up intentions according to different types of commitment an agent may have.

BDI-logical expressions can be used to characterize different types of agents. Rao & Georgeff mention the following possibilities:

1. (blindly committed agent) IN T EN D(inevitable ⇧ ') ! inevitable(IN T EN D(inevitable ⇧ ')UBEL(')) 2. (single-minded committed agent) IN T EN D(inevitable ⇧ ') ! inevitable(IN T EN D(inevitable ⇧ ')U(BEL(') _ ¬BEL(optional ⇧ '))) 3. (open minded committed agent) IN T EN D(inevitable ⇧ ') ! inevitable(IN T EN D(inevitable ⇧ ')U(BEL(') _ ¬GOAL(optional ⇧ ')))
A blindly committed agent maintains his intentions to inevitably obtaining eventually something until he actually believes that that something has been fulfilled. A single-minded committed agent is somewhat more flexible: he maintains his intention until he believes he has achieved it or he does not believe that it can be reached (i.e. that it is still an option in some future) anymore. Finally, the open minded committed agent is even more flexible: he can also drop his intention if it is not a goal (desire) anymore.

Rao & Georgeff are then able to obtain results under which conditions the various types of committed agents will reach their intentions. For example, for a blindly committed agent it holds that under the assumption of the axioms we have discussed earlier plus an axiom that expresses no infinite deferral of intentions:

IN T EN D(') ! inevitable ⇧ ¬IN T EN D(') that IN T EN D(inevitable(⇧')) ! inevitable(⇧BEL('))
expressing that if the agent intends to eventually obtain ' it will inevitably eventually believe that it has succeeded in achieving '.

The branching-time setup of the approach as opposed to a linear-time one is much more expressive and is shown to solve problems such as the Little Nell problem. This is about a girl, Little Nell, that is in mortal peril, and a rescue agent that reasons like this: I intend to rescue Little Nell, and therefore I believe (because I'm confident that my actions will succeed) that she will be safe, but then I can drop my intention to rescue her just because she will be safe...! In a lineartime approach -if one is not very careful -this scenario results in a contradictory 10.3. KARO LOGIC (or unintuitive) representation (basically because there is only one future in which apparently Little Nell will be safe), while in a branching-time approach such as Rao and Georgeff's this presents no problem at all. In fact in CTL BDI the scenario comes down to something like (here ' stands for "Little Nell is safe")

IN T EN D(inevitable ⇧ ') ! inevitable(IN T EN D(inevitable ⇧ ')UBEL(optional ⇧ '))
informally saying that since the agent believes that there is a way (by performing its plan) to eventually reaching the goal ', it may drop its intention to perform the plan to achieve eventually ', which is definitely not valid in CTL BDI ! Intuitively, this is the case, because there may be other branches along which Little Nell will not be safe, so that there is no reason to give up the intention to rescue her.

In the next section we will look at yet another approach, based on (nonlinear) dynamic logic, which may perhaps be viewed as an amalgam of those of Cohen & Levesque (using dynamic logic) but allowing for non-linear, i.e. branching, structures.

KARO Logic

In this section we review the KARO formalism, in which action, together with knowledge / belief, is the primary concept, on which other agent notions are built. Historically, the KARO approach was the first approach truly based on dynamic logic, although as we have seen, in retrospect, we may view Cohen & Levesque's approach as being based on a linear variant of PDL (Propositional Dynamic Logic). There are differences, though. We will see that in KARO the fact that it is based on a logic of action is even more employed than in Cohen & Levesque: besides BDIlike notions such as knowledge, belief, desires, and goals that are operators that take formulas as arguments, and are quite similar in nature as the notions that are in Cohen & Levesque's approach, in KARO there are also operators taking actions as arguments such as ability and commitment, and operators that take both actions and formulas as arguments, such as a Can operator and a (possible) intention operator. All these operators are used to describe the mental state of the agent. But even more importantly, in the KARO framework (dedicated) actions are used to change the mental state of the agent. So there are revise, commit and uncommit actions to revise beliefs and update the agenda (the commitments) of the agent. In this sense KARO is related to dynamic epistemic logic, the topic of Chapter 6 in this handbook.

KARO logic for rational agents

The KARO formalism is an amalgam of dynamic logic and epistemic / doxastic logic, augmented with several additional (modal) operators in order to deal with the motivational aspects of agents. So, besides operators for knowledge (K), belief (B) and action ([↵], "after performance of ↵ it holds that"), there are additional operators for ability (A) and desires (D).

Assume a set A of atomic actions and a set P of atomic propositions.

Definition 10.6 (Language)

The language L KARO of KARO-formulas is given by the BNF grammar:

' ::= p(2 P) | ¬' | ' 1 ^'2 | . . . K' | B' | D' | [↵]' | A↵ ↵ ::= a(2 A) | '? | ↵ 1 ; ↵ 2 | ↵ 1 + ↵ 2 | ↵ ⇤ a
Here the formulas generated by the second (↵) part are referred to as actions (or rather action expressions). We use the abbreviations tt ⌘ p _ ¬p (for some fixed p 2 P) and ff ⌘ ¬tt. Conditional and while-action are introduced by the usual abbreviations: if ' then ↵ 1 else ↵ 2 fi ⌘ ('?; ↵ 1 ) + (¬'?; ↵ 2 ) and while ' do ↵ od ⌘ ('?; ↵) ⇤ ; ¬'?.

Thus formulas are built by means of the familiar propositional connectives and the modal operators for knowledge, belief, desire, action and ability. Actions are the familiar ones from imperative programming: atomic ones, tests, sequential composition, (nondeterministic) choice and repetition.

Definition 10.7 (KARO models)

1. The semantics of the knowledge, belief and desires operators is given by means of Kripke structures of the following form:

M = hW, #, R K , R B , R D i
, where

• W is a non-empty set of states (or worlds)

• # is a truth assignment function per state • R K , R B , R D are accessibility relations for interpreting the modal operators K, B, D. The relation R K is assumed to be an equivalence relation, while the relation R B is assumed to be euclidean, transitive and serial. Furthermore we assume that R B ✓ R K . No special constraints are assumed for the relations R D .

2. The semantics of actions is given by means of structures of type h⌃, {R a | a 2 A}, C, Agi, where

• ⌃ is the set of possible model/state pairs (i.e. models of the above form, together with a state appearing in that model) • R a (a 2 A) are relations on ⌃ encoding the behaviour of atomic actions • C is a function that gives the set of actions that the agent is able to do per model/state pair • Ag is a function that yields the set of actions that the agent is committed to (the agent's 'agenda') per model/state pair. a

We have elements in the structures for interpreting the operators for knowledge, belief, and desire. Actions are modelled as model/state pair transformers to emphasize their influence on the mental state (that is, the complex of knowledge, belief and desires) of the agent rather than just the state of the world. Both (cap)abilities and commitments are given by functions that yield the relevant information per model / state pair.

KARO LOGIC

Definition 10.8 (Interpretation of formulas in KARO) In order to determine whether a formula ' 2 L is true in a model/state pair (M, w) (if so, we write (M, w) |= '), we stipulate:

• M, w |= p iff #(w)(p) = true, for p 2 P

• The logical connectives are interpreted as usual.

• M, w |= K' iff M, w 0 |= ' for all w 0 with R K (w, w 0 ) • M, w |= B' iff M, w 0 |= ' for all w 0 with R B (w, w 0 ) • M, w |= D' iff M, w 0 |= ' for all w 0 with R D (w, w 0 ) • M, w |= [↵]' iff M 0 , w 0 |= ' for all M 0 , w 0 with R ↵ ((M, w), (M 0 , w 0 )) • M, w |= A↵ iff ↵ 2 C(M, w) 5 • M, w |= Com(↵) iff ↵ 2 Ag(M, w ) 6 a
Here R ↵ is defined as usual in dynamic logic by induction from the basic case R a , but now on model/state pairs rather than just states. So, e.g.

R ↵1+↵2 = R ↵1 [ R ↵2 , R ↵ ⇤ = R ⇤
↵ , the reflective transitive closure of R ↵ , and R ↵1;↵2 is the relational product of R ↵1 and R ↵2 . Likewise the function C is lifted to complex actions. We call an action ↵ deterministic if #{w 0 | R ↵ (w, w 0 )} 6 1 for any w 2 W , and strongly deterministic if #{w 0 | R ↵ (w, w 0 )} 6 1. (Here # stands for cardinality.)

We have clauses for knowledge, belief and desire. The action modality gets a similar interpretation: something (necessarily) holds after the performance / execution of action ↵ if it holds in all the situations that are accessible from the current one by doing the action ↵. The only thing which is slightly nonstandard is that, as stated above, a situation is characterised here as a model / state pair. The interpretations of the ability and commitment operators are rather trivial in this setting (but see the footnotes): an action is enabled (or rather: the agent is able to do the action) if it is indicated so by the function C, and, likewise, an agent is committed to an action ↵ if it is recorded so in the agent's agenda.

Furthermore, we will make use of the following syntactic abbreviations serving as auxiliary operators: Definition 10.9

• (dual) h↵i' = ¬[↵]¬', expressing that the agent has the opportunity to perform ↵ resulting in a state where ' holds.

• (opportunity) O↵ = h↵itt, i.e., an agent has the opportunity to do an action iff there is a successor state w.r.t. the R ↵ -relation;

• (practical possibility) P(↵, ') = A↵ ^O↵ ^h↵i', i.e., an agent has the practical possibility to do an action with result ' iff it is both able and has the opportunity to do that action and the result of actually doing that action leads to a state where ' holds;

• (can) Can(↵, ') = KP(↵, '), i.e., an agent can do an action with a certain result iff it knows it has the practical possibility to do so;

• (realisability) 3' = 9a 1 , . . . , a n P(a 1 ; . . . ; a n , ') 7 , i.e., a state property ' is realisable iff there is a finite sequence of atomic actions of which the agent has the practical possibility to perform it with the result ';

• (goal) G' = ¬'^D'^3', i.e., a goal is a formula that is not (yet) satisfied, but desired and realisable.8

• (possible intend) I(↵, ') = Can(↵, ') ^KG', i.e., an agent (possibly) intends an action with a certain result iff the agent can do the action with that result and it moreover knows that this result is one of its goals. a

Remark 10.1

• The dual of the (box-type) action modality expresses that there is at least a resulting state where a formula ' holds. It is important to note that in the context of deterministic actions, i.e. actions that have at most one successor state, this means that the only state satisfies ', and is thus in this particular case a stronger assertion than its dual formula [↵]', which merely states that if there are any successor states they will (all) satisfy '.

Note also that if atomic actions are assumed to be deterministic all actions including the complex ones will be deterministic.

• Opportunity to do an action is modelled by having at least one successor state according to the accessibility relation associated with the action.

• Practical possibility to to an action with a certain result is modelled as having both ability and opportunity to do the action with the appropriate result. Note that O↵ in the formula A↵ ^O↵ ^h↵i' is actually redundant since it already follows from h↵i'. However, to stress the opportunity aspect it is added.

• The Can predicate applied to an action and formula expresses that the agent is 'conscious' of its practical possibility to do the action resulting in a state where the formula holds.

• A formula ' is realisable if there is a 'plan' consisting of (a sequence of) atomic actions of which the agent has the practical possibility to do them with ' as a result.

• A formula ' is a goal in the KARO framework if it is not true yet, but desired and realisable in the above meaning, that is, there is a plan of which the agent has the practical possibility to realise it with ' as a result.

• An agent is said to (possibly) intend an action ↵ with result ' if it 'Can' do this (knows that it has the practical possibility to do so), and, moreover, knows that ' is a goal. a

In order to manipulate both knowledge / belief and motivational matters special actions revise, commit and uncommit are added to the language. (We assume that we cannot nest these operators. So, e.g., commit(uncommit↵) is not a wellformed action expression.) The semantics of these are again given as model/state transformers (We only do this here in a very abstract manner, viewing the accessibility relations associated with these actions as functions. For further details we refer the reader to inspect some of the KARO references mentioned in Section 10.6. Definition 10.10 (Accessibility of revise, commit and uncommit actions) ↵,') for all formulas ', that is, an agent is able to uncommit to an action if it is not intended to do it (any longer) for any purpose. a

1. R revise' (M, w) = update_belief (', (M, w)). 2. R commit↵ (M, w) = update_agenda + (↵, (M, w)), if M, w |= I(↵, ') for some ', otherwise R commit↵ (M, w) = ; (
Here update_belief , update_agenda + and update_agenda are functions that update the agent's belief and agenda (by adding or removing an action), respectively. Details are omitted here, but essentially these actions are model/state transformers again, representing a change of the mental state of the agent (regarding beliefs and commitments, respectively). The update_belief (', (M, w)) function changes the model M in such a way that the agent's belief is updated with the formula ', while update_agenda + (↵, (M, w)) changes the model M such that ↵ is added to the agenda, and likewise for the update_agenda function, but now with respect to removing an action from the agenda. The revise operator can be used to cater for revisions due to observations and communication with other agents, which we will not go into further here.

The interpretation of formulas containing revise and (un)commit actions is now done using the accessibility relations above. One can now define validity as usual with respect to the KARO-models. One then obtains the following validities (of course, in order to be able to verify these one should use the proper model and not the abstraction / simplification we have presented here.) Typical properties of this framework, called the KARO logic, include:

The first of these properties says that all the modalities mentioned are 'normal' in the sense that they are closed under implication. The second states that the dual operator h↵i is stronger than the operator [↵] in case the action ↵ is deterministic: if there is at most one successor state after performing ↵ and we know that there is at least one successor state satisfying ' then all successor states satisfy '. The third and fourth properties are the so-called introspection properties for knowledge and belief. The fifth property says that knowledge is true, while the sixth states that belief (may not be true but) is not inconsistent. The seventh property states that having the opportunity to do a sequential composition of two actions amounts to having the opportunity of doing the first action first and then having the opportunity to do the second. The eighth states that an agent that can do a sequential composition of two actions with result ' iff the agent can do the first actions resulting in a state where it has the practical possibility to do the second with ' as result. The ninth states that if one possibly intends to do ↵ with result ' then one knows that there is a possibility of performing ↵ resulting in a state where ' holds. The tenth asserts that if an agent possibly intends to do ↵ with some result ', it has the opportunity to commit to ↵ with result that it is committed to ↵ (i.e. ↵ is put into its agenda). The eleventh says that if an agent intends to do ↵ with a certain purpose, then it is unable to uncommit to it (so, if it is committed to ↵ it has to persevere with it). This is the way persistence of commitment is represented in KARO. Note that this is much more 'concrete' (also in the sense of computability) than the persistence notions in the other approaches we have seen, where temporal operators pertaining to a possibly infinite future were employed to capture them...! We think it is no coincidence that Hindriks et al. established an almost perfect match in the sense of a correspondence between the agent programming language GOAL and Cohen & Levesque's logic of intention, the main difference being the inability of GOAL to express the persistence properties of intentions in this logic...!) In KARO we have the advantage of having dedicated actions in the action language dealing with the change of commitment that can be used to express persistence without referring to the (infinite) future, rendering the notion of persistence much 'more computable'. The twelfth property says that if an agent is committed to an action and it has the opportunity to uncommit to it, as result then indeed the commitment is removed. The thirteenth says that whenever an agent is committed to an action that is no longer known to be practically possible, it knows that it can undo this impossible commitment. The fourteenth property states that commitments are known to the agent. The last four properties have to do with commitments to complex actions. For instance, the fifteenth says that if an agent is committed to a sequential composition of two actions then it is committed to the first one, and it knows that after doing the first action it will be committed to the second action.

KARO logic for emotional agents

In this subsection we look at a recent application of BDI logic that deals with agent behaviour that is strictly beyond the scope of the original aim of BDI logic, viz. describing the behaviour of rational agents. We will sketch how the KARO framework can be used for describing emotional agents. Although it is perhaps a bit paradoxical to describe emotions and emotional behaviour with logic, one should bear in mind that we are dealing with behaviour here, and this can be described in logic, especially a logic that deals with actions such as the KARO framework. Furthermore, as we shall see, emotional behaviour will turn out to be complimentary rather than opposed to rational behaviour of agents, something that is also acknowledged by recent work in cognitive science through the work of for instance Damasio. Our presentation here is inspired by two psychological theories: that of Oatley & Jenkins and that of OCC. Since the latter is much more involved (treating 22 emotions, while the former only treats 4 basic emotions), we here mainly follow the ideas of Oatley & Jenkins, and say a few words on modelling OCC later.

According to Oatley & Jenkins, the 4 basic emotions, happiness, sadness, anger and fear, have the following characteristics:

• Happiness results when in the process of trying to achieve a goal, things go 'right', as expected, i.e., subgoals are achieved thus far.

• Sadness results when in the process of trying to achieve a goal, things go 'wrong', i.e., not as expected, i.e., subgoals are not being achieved.

• Anger is the result of frustration about not being able to execute the current plan, and makes the agent try harder to execute the plan.

• Fear results when a 'maintenance goal' is threatened, so that the agent will make sure that this maintenance goal is restored before going on with other activities.

It is directly obvious from these descriptions that these emotions are BDI-related notions! So it is not so strange to use a BDI-logic like KARO to describe them, which is what Meyer did.

Let us take sadness as an example. For simplicity, assume that plans consist of sequences of atomic actions. In KARO we can then express the trigger condition for sadness as follows:

I(⇡, ') ^Com(⇡) ^B([↵] ) ! [↵]((B¬ ^Com(⇡\↵)) ! sad(⇡\↵, '))
where ↵ is a prefix of plan ⇡. Intuitively, this says that if the agent has the (possible) intention to perform plan ⇡ with goal ', it is committed to ⇡ (so it has a true intention to do ⇡), and it believes that after doing the initial fragment ↵ of the plan ⇡ it holds that , then after doing ↵ if it believes that does not hold while it is still committed to the rest of the plan, it is sad (with respect to the rest of the plan and goal '). In a similar way the trigger conditions of the other emotions can be formalised.

Also, together with Steunebrink and Dastani, Meyer looked at modeling OCC. Particularly, they show how to formalise the (trigger conditions of) emotions in OCC in three steps: first by presenting a more general logical structure of the emotions, which are later refined in terms of doxastic logic and finally in the full-blown BDI logic KARO again. The way emotions get a semantics based on BDI models is quite intricate and beyond the scope of this chapter, but one of the properties that can be proven valid in this approach is the following, using KARO's (possible) intend operator (here parametrized by an agent):

I i (↵, ') ! [i : ↵](P ride T j (i : ↵) ^Joy T i (') ^Gratif ication T i (i : ↵, '))
(Here i : ↵ in the dynamic logic box refers to the action of i performing ↵, and the superscript T placed at the emotion operators pertains to the idea that we are considering triggering / elicitation forms of the emotions concerned.) Informally this reads that if the agent i has the possible intention to do ↵ with goal ', then if he has performed ↵ he is proud (triggered pride) of his action, has (triggered) joy about the achievement of the goal ' and has (triggered) gratification with respect to action i : ↵ and goal '.

Finally, let us also mention here the strongly related work by Adam et al. Also this work is devoted to a formalisation of OCC emotions in BDI terms. There are differences with the work of Steunebrink et al., though. For instance, Adam simply defines joy as a conjunction of belief and desire: Joy ' = def Bel ' ^Des '. This seems to express a 'state of joy' (experience) rather than a trigger for joy. This raises a confusion of emotion elicitation (triggering) and experience, which is kept separately in the approach of Steunebrink. This confusion also appears at other places in the work of Adam, e.g. where she defines gratification as the conjunction of pride (which pertains to triggering) and joy (which is about experience as we saw earlier). In later work by Adam, this issue is improved upon and it is explained that the above definition of Joy is solely about the triggering of joy, not the experience. However, the confusion of triggering versus experience is still not resolved completely since it is still present in the introspective properties of emotional awareness Emotion' $ BelEmotion' and ¬Emotion' $ Bel¬Emotion', which hold in Adam's framework, for any Emotion. This is counterintuitive if Emotion should capture the triggering of the associated emotion, since an agent may not be aware of this triggering.

BDI-modalities in STIT logic

The principles of BDI logics reflect rationality postulates for agent modalities. In particular, the BDI principles model how B, D and I modalities interact with each other over time (well known are the so called 'commitment strategies' of Cohen & Levesque, stating under which belief and desire conditions intentions have to be dropped, see Section 10.2.1). BDI logics are not meant for knowledge representation but for agent specification: ideally concretely built agents will some day be verified against the logic principles of BDI-logics (how exactly this could ever be done is a question we set aside here).

An essential component of any BDI logic is then its dynamic part. Traditionally, either the dynamic part is formed by a dynamic logic fragment (Cohen & Levesque, KARO) or a temporal fragment (Rao & Georgeff). Recently a third alternative has been considered: STIT (seeing to it that) logic. STIT logics can be said to be in between dynamic logic and temporal logic. Where dynamic logic sees actions as the steps of a program, and temporal logic leaves actions entirely out of the picture, STIT logic sees action as a relation between agents and the effects they can see to. STIT logic achieves this by generalizing temporal structures to choice structures. The most distinguishing feature of STIT logic is that truth of formulas often expresses information about the dynamics of the world. For instance, the STIT logic formula [ag stit]X(at_station)) says that agent ag currently sees to it that next it is at the station. But, it does not say that the agent can see to it that next it is at the station (this is however a logical consequence). Abilities are truths about static conditions, and not about dynamic conditions.

In the present section we will discuss how in recent years several authors have aimed to combine STIT logic and BDI notions. There are two parts. In the first part, Section 10.4.1, we focus on classical instantaneous STIT logics and the BDI extensions that have been suggested for them. In the second part, Section 10.4.2, we consider dynamic variants of the BDI modalities and discuss the notion of 'knowingly doing' within a version of STIT where effects of actions take effect in next states: XSTIT.

There is a strong connection, both conceptually and technically, between the family of logics STIT and Alternating-time Temporal Logic, which is at the center of attention in Chapter 11.

BDI modalities in instantaneous stit

Traditionally STIT logics encompass operators for agency that assume that an agentive choice performance is something that takes no time. So, an instantaneous stit operator [ag stit]' typically obeys the success axiom [ag stit]' ! ' to capture the intuition concerning instantaneity saying that if ag now sees to it that ' holds, then ' must be true now. Before putting forward an alternative to this view, where the central agency operator has a built-in step to a next moment in time, we give the formal definition of standard (Chellas) instantaneous STIT logic and discuss its logical properties. We will here use a slightly different syntax and semantics than used by Chellas himself and also different from that of Horty, but, the logic is the same.

CSTIT

Definition 10.11 Given a countable set of propositions P and p 2 P , and given a finite set Ags of agent names, and ag 2 Ags, the formal language L CSTIT is:

' := p | ¬' | ' ^' | 2' | [ag Cstit]' a
Besides the usual propositional connectives, the syntax of CSTIT comprises two modal operators. The operator 2' expresses 'historical necessity', and plays the same role as the well-known path quantifiers in logics such as CTL and CTL ⇤ . Another way of talking about this operator is to say that it expresses that ' is 'settled'. We abbreviate ¬2¬' by 3'. The operator [ag Cstit]' stands for 'agent ag sees to it that '' (the 'C' referring to Chellas). hag Cstiti' abbreviates ¬[ag Cstit]¬'.

The semantics given in Definition 10.12 below is an alternative to the semantics given by Belnap and colleagues in terms of BT+AC structures (Branching Time + Agentive Choice structures). The differences are not essential. Where the branching of time in BT + AC structures is represented by tree-like orderings of moments, the structures below use 'bundles' of linearly ordered sets of moments. We use the latter to be uniform in the semantic structures across different STIT formalisms in this section. Definition 10.12 A CSTIT-frame is a tuple hS, H, R ag i such that9 :

1. S is a non-empty set of static states. Elements of S are denoted s, s 0 , etc.

2.

H is a non-empty set of possible system histories . . . s 2 , s 1 , s 0 , s 1 , s 2 , . . . with s x 2 S for x 2 Z. Elements of H are denoted h, h 0 , etc.

3. Dynamic states are tuples hs, hi, where s 2 S, h 2 H and s appears on h. Now the relations R ag are 'effectivity' equivalence classes over dynamic states such that hs, hiR ag hs 0 , h 0 i only if s = s 0 . For any state s and agent ag, the relation R ag defines a partition of the dynamic states built with s.

Definition 10.17 (Truth conditions BDI operators) Relative to a model hS, H, R ag , N b , N d , N i , V i, truth of belief, desire and intention operators is defined as ( J'K is the truth set of ', that is, the subset of all dynamic elements in S ⇥ H satisfying '):

hs, hi |= h[ag bel]i' , J'K 2 N b (s, h, ag) hs, hi |= h[ag des]i' , J'K 2 N d (s, h, ag) hs, hi |= h[ag int]i' , J'K 2 N i (s, h, ag) a
An axiomatization of a probabilistic epistemic logic is obtained by formulating axioms corresponding to the conditions on neighborhood functions.

Theorem 10.3 (Hilbert system BDI operators) Relative to the semantics following from definitions 10.16 and 10.17 we define the following Hilbert system. We assume the standard derivation rules for the weak modalities, like closure under logical equivalence.

(BelPos) ¬h[ag bel]i? (BelWk) h[ag bel]i' ! h[ag bel]i(' _ ) (DesPos) ¬h[ag des]i? (DesWk) h[ag des]i' ! h[ag des]i(' _ ) (IntPos) ¬h[ag int]i? (IntWk) h[ag int]i' ! h[ag int]i(' _ ) (IntD) h[ag int]i' ! ¬h[ag int]i¬' a
Relative to their own version of the semantics, Semmling & Wansing prove completeness of their logic. Here the completeness of the axiomatization relative to the frames of Definition 10.16 follows from general results in neighborhood semantics and monotonic modal logic. One can check that the conditions on the frames correspond one-to-one with the axioms in the axiomatization.

As can be seen from the axioms and conditions we have shown above, Semmling and Wansing chose to make their BDI-stit logic rather weak, trying to commit only to a minimum of logical properties. But even with this minimalistic approach there is room for debate. For instance, the condition on intentions only looks at pairwise consistency of intentions, but conflicts are still possible in case there is a combination of three intentions: {h[ag int]i', h[ag int]i(' ! ), h[ag int]i¬ } is satisfiable. If we do not want that, it is straightforward to adapt the condition on neighborhood functions (demand that any finite number of neighborhoods has a state in common), but it is unclear how to axiomatise it.

Even though the STIT framework's notion of truth refers to the dynamics of a system of agents (which is why we talk about 'dynamic states'), Semmling and Wansing do not focus on dynamic interpretations of the BDI attitudes. A formula like h[ag bel]i[ag Cstit]' must express something like "ag believes that it sees to it that '", but the inherent dynamic aspect of this notion is not analyzed. In particular, no interactions between STIT and BDI modalities are studied. This is likely to be due to the fact that explicit dynamic temporal operators are absent in the logic and because agency is instantaneous. In Section 10.4.2 we will report on the study of the inherent dynamic aspect of such combinations of operators.

BDI, STIT and regret

Lorini and Schwarzentruber use STIT logic as the basis for investigations into what they call counterfactual emotions10 . The typical counterfactual emotion is 'regret'. Regret can be described as a discrepancy between what actually occurs and what could have happened. Based on this they argue that for a definition of regret in the STIT framework, it needs to be extended with modalities for knowledge and desire. They consider three different STIT formalisms to base their definitions on, but here it will suffice to discuss their ideas using the Chellas STIT logic given earlier.

Knowledge is added to their STIT framework in a straightforward way: a normal S5 knowledge operator [ag i kno] is added for every agent ag i in the system. The interpretation is in terms of equivalence classes over the basic units of evaluation (for the stit language we consider here: dynamic states). So, for knowledge we get the truth condition hs, hi |= [ag i kno]' iff for all s 0 , h 0 such that hs, hi ⇠ hs 0 , h 0 i we have hs 0 , h 0 i |= '. The second operator we take from their system is an operator for desire, which is defined using propositional constants.

Definition 10.18

Let good agi denote a propositional constant, one for each agent ag i in the system, whose truth expresses that a state is good for that agent. Now the modal operators [ag i good]' and [ag i des]' are defined by:

[ag i good]' ⌘ def 2(good agi ! ') [ag i des]' ⌘ def [ag i kno][ag i good]' a
The counterfactual aspect is introduced by the definition of the notion of "could have prevented" (CHP). For definitions of such counterfactual properties, the STIT framework is more suited than dynamic logic or situation calculus frameworks, since in STIT we reason about actual performances of actions which also makes it possible to reason about choices that are not (f)actual. Lorini and Schwarzentruber define their notion of CHP in a group stit framework. Here we have only defined individual agency. Therefore we will only consider the two agent case, for which there is no essential difference between group operators and operators for individual agents. The two agent case will enable us to discuss the ideas properly.

In the two agent setting, Lorini and Schwarzentruber's intuition can be described as follows: agent ag 1 could have prevented ' if and only if (1) ' is currently true, and (2) agent ag 2 does not see to it that '. They reformulate the second condition as 'provided that agent ag 2 sticks to its choice, for agent ag 1 there is the possibility to act otherwise in a way that does not guarantee the outcome '' 11 . by the operator [ag xstit]' where the effect ' is not instantaneous but occurs in a next state. Further explanations and motivations can be found elsewhere (see Section 10.6).

Definition 10.21 Given a countable set of propositions P and p 2 P , and given a finite set Ags of agent names, and ag 2 Ags, the formal language L XSTIT is:

' := p | ¬' | ' ^' | 2' | [ag xstit]' | X' a
The operator [ag xstit]' stands for 'agent ag sees to it that ' in the next state'. The operator X' is a standard next time operator. 2 is again the operator for historical necessity (settledness).

Definition 10.22

An XSTIT-frame is a tuple hS, H, Ei such that:

1. S is a non-empty set of static states. Elements of S are denoted s, s 0 , etc.

2. H is a non-empty set of possible system histories . . . s 2 , s 1 , s 0 , s 1 , s 2 , . . . with s x 2 S for x 2 Z. Elements of H are denoted h, h 0 , etc. We denote that s 0 succeeds s on the history h by s 0 = succ(s, h) and by s = prec(s 0 , h).

We have the following bundling constraint on the set H: a. if s 2 h and s 0 2 h 0 and s = s 0 then prec(s, h) = prec(s 0 , h 0 )

3. E : S ⇥H ⇥Ags 7 ! 2 S is an h-effectivity function yielding for an agent ag the set of next static states allowed by the choice performed by the agent relative to a history. We have the following constraints on h-effectivity functions: a. if s 6 2 h then E(s, h, ag) = ; b. if s 0 2 E(s, h, ag) then 9h 0 : s 0 = succ(s, h 0 ) c. if s 0 = succ(s, h 0 ) and s 0 2 h then s 0 2 E(s, h, ag)

d. E(s, h, ag 1 ) \ E(s, h 0 , ag 2 ) 6 = ; for ag 1 6 = ag 2 Condition 2.a is the 'backwards-linear' requirement that we have seen in Section 10.2.2. Condition 3.b ensures that next state effectivity as seen from a current state s does not contain states s 0 that are not reachable from the current state through some history. Condition 3.c expresses the STIT condition of 'no choice between undivided histories'. Condition 3.d above states that simultaneous choices of different agents never have an empty intersection. This is the central condition of 'independence of agency'. It reflects that a choice performance of one agent can never have as a consequence that some other agent is limited in the choices it can exercise simultaneously.

Again, we evaluate truth with respect to dynamic states.

Knowingly doing

To study the notion of knowingly doing, like before, in Section 10.4.1, a normal S5 knowledge operator [ag i kno]' is added for every agent ag i in the system. The equivalence classes, or 'information sets' of these operators contain state-history pairs, which means knowledge concerns information about the dynamics of the system of agents. Now knowingly doing is suitably modeled by the combination of operators [ag i kno][ag i xstit]'. For the logic of this notion we can consider several interactions between the contributing modalities. Here we only briefly mention some of the possibilities.

It is a fundamental property of agency that an agent cannot know what other agents choose simultaneously. This is expressed by the following axiom.

Definition 10.24

The property of ignorance about concurrent choices of others is defined by the axiom:

(IgnCC) [ag 1 kno][ag 2 xstit]' ! [ag 1 kno]2[ag 2 xstit]' for ag 1 6 = ag 2 a
(IgnCC) expresses that if an agent knows that something results from the choice of another agent, it can only be that the agent knows it is settled that that something results from a choice of the other agent.

Definition 10.25

The property of knowledge about the next state is defined by the axiom:

(XK) [ag kno]X' ! [ag kno][ag xstit]' a
The (XK) property expresses that the only things an agent can know about the next state are the things it knows to be seeing to it itself.

Definition 10.26

The property of effect recollection is defined by the axiom:

(Rec-Eff ) [ag kno][ag xstit]' ! [ag xstit][ag kno]' a
(Rec-Eff) expresses that if agents knowingly see to something, then they know that something is the case in the resulting state.

The above three properties for knowingly doing just exemplify some of the possibilities. More properties have been studied. Also the theory on these dynamic attitudes has been extended to beliefs and to intentions. The case of intentional action is particularly interesting because there is an extensive philosophical literature on this notion. One of the philosophical scenario's discussed by Broersen for instance is the side effect problem. Here we can only point to the fact that XSTIT, after addition of the right BDI modalities, seems to be a suitable base logic for the study of such notions.

Conclusion

In this chapter we have reviewed the use of epistemic logic, extended with other modalities for motivational attitudes such as desires and intentions, for describing (the behaviour of) intelligent agents. What is immediately clear is that although all logical approaches are based on and inspired by Bratman's seminal work on BDI theory for practical reasoning, the formalizations themselves are quite different in nature. They also enjoy different (and sometimes even on first sight contradictory) properties. In our view this means that although Bratman did his uttermost to present a clear philosophy, as is often the case when formalizing these kind of philosophical theories, there is still a lot of ambiguity or, put more positively, freedom to formalise these matters. We have even seen that quite different base logics may be used, such as (branching-time) temporal logic, dynamic logic and also stit logic. This makes the formal logics in themselves hard to compare. We think it depends on the purpose of the formalisation (is it used for better understanding, or does it serve as a basis for computational and executable frameworks) which of the BDI logics will be most appropriate. The latter is especially important for designers and programmers of agent systems.

Notes

Pointers to the theory of Bratman and colleagues include the work on practical reasoning by [START_REF] Bratman | Intentions, Plans, and Practical Reason[END_REF] and by [START_REF] Bratman | Plans and resourcebounded practical reasoning[END_REF], as well as the paper on intentions by [START_REF] Bratman | What is intention?[END_REF]. The concept of pro-attitude is also introduced by [START_REF] Bratman | Intentions, Plans, and Practical Reason[END_REF]. The term 'Practical Reasoning' dates back to Aristotle: For further reading and a contemporary reference list the reader is also advised to read the short introduction 'Practical Reason' in the Stanford Encyclopedia of Philosophy ( 2013), or to consult work on 'Practical Syllogism'. The term 'screen of admissibility' to describe Bratman's theory of how intentions filter admissible options was coined by [START_REF] Cohen | Intention is choice with commitment[END_REF]. For more on the subtle issue of admissible intentions and inconsistent beliefs and an elaborate example, see pp. 41-42 of the paper by [START_REF] Bratman | Intentions, Plans, and Practical Reason[END_REF]. Daniel Dennett set out his work on the intentional stance (based on the notions of desire and belief) in [START_REF] Dennett | The Intentional Stance[END_REF]. A reduction of intention to beliefs and desires alone is rejected (pp. 6-9) by [START_REF] Bratman | Intentions, Plans, and Practical Reason[END_REF].

A pioneering paper on intelligent agents is by Wooldridge and Jennings (1995), and also by [START_REF] Wooldridge | Intelligent agents[END_REF]. The latter for instance addresses the issue of how logics like those studied in this chapter may eventually be realised in agent-based systems. The area of agents and multi-agent systems is now a mature and still active area: a good start for further orientation is provided by the website of IFAAMAS (IFAAMAS), which hosts proceedings of the Autonomous Agents and Multi-Agent Systems conference since 2007. As mentioned in the text, Bratman's semi-formal theory on intentions was further formalised by [START_REF] Cohen | Intention is choice with commitment[END_REF], and, more or less at the same time, by [START_REF] Rao | Modeling rational agents within a BDIarchitecture[END_REF]. In fact their work won, respectively, the 2006 and 2007 IFAAMAS Awards for Influential Papers in Autonomous Agents and Multiagent Systems. [START_REF] Cohen | Intention is choice with commitment[END_REF] were among the first to adapt PDL to model agency. Many responses, extensions and variations of this logic have been proposed. For instance, the Side-Effect-Free Principle was coined by [START_REF] Su | A modal logic for beliefs and pro attitudes[END_REF], while the study of introspective properties of preferences was undertaken by [START_REF] Herzig | C&L intention revisited[END_REF], [START_REF] Lorini | Trust and norms in the context of computer security: toward a logical formalization[END_REF], and by [START_REF] Herzig | A logic of trust and reputation[END_REF]. The first of those three references also put forward a definition of epistemic achievement goal. Weakening the link between action and goals, and at the same time allowing for a stronger commitment (a notion criticised by [START_REF] Herzig | C&L intention revisited[END_REF]) was undertaken by [START_REF] Sadek | Dialogue acts are rational plans[END_REF] and by [START_REF] Bretier | La communication orale coopérative: contribution à la modélisation logique et à la mise en oeuvre d'un agent rationnel dialoguant[END_REF]. [START_REF] Sadek | A study in the logic of intention[END_REF] moreover argues for a notion of realistic preference, also called weak realism. The notion of attempting to do an action was formalised by [START_REF] Lorini | A logic of intention and attempt[END_REF].

Our treatment of Rao and Georgeff's BDI logic is mainly based on [START_REF] Rao | Modeling rational agents within a BDIarchitecture[END_REF] (which includes the GOAL-operator) and [START_REF] Rao | Decision procedures for BDI logics[END_REF] (where this operator is replaced by an operator DES for desire). Their approach, in turn, is for its formal model heavily inspired by the framework on branching time logic put forward by [START_REF] Emerson | Temporal and modal logic[END_REF]. The abbreviation CTL stands for Computation-Tree Logic, in which one can quantify over branches, and, given a branch, over its points. CTL ⇤ is an extension of CTL where some of CTL's restrictions on the occurrences of branching and linear time quantifiers, are lifted. The semantic constraints that make some of the desirable axioms of Section 10.2.2 valid, are discussed by Rao andGeorgeff (1991, 1998) and by [START_REF] Wooldridge | Reasoning about Rational Agents[END_REF]. In particular, the world/time point compatibility requirement is taken from [START_REF] Wooldridge | Reasoning about Rational Agents[END_REF]. We have used the little Nell problem as an advocate to use branching time logic, rather than linear time logic. This problem was discussed by [START_REF] Mcdermott | A temporal logic for reasoning about processes and plans[END_REF], and also addressed by the papers of Cohen & Levesque and Rao & Georgeff. It is interesting to note that in a series of talks and papers however, Moshe Vardi has argue that from a computer science perspective, it is far from clear that branching time provides a superior model over that of linear time (see for instance the paper by [START_REF] Vardi | Branching vs. linear time: Final showdown[END_REF]).

KARO stands for Knowledge, Ability, Result and Opportunity. The KARO framework was developed in a number of papers by van Linder, van der Hoek, and [START_REF] Van Linder | Actions that make you change your mind: belief revision in an agent-oriented setting[END_REF][START_REF] Van Linder | Seeing is believing (and so are hearing and jumping)[END_REF][START_REF] Van Der Hoek | An integrated modal approach to rational agents[END_REF] and [START_REF] Meyer | A logical approach to the dynamics of commitments[END_REF] and the thesis by [START_REF] Van Linder | Modal Logics for Rational Agents[END_REF]. All the basic operators of KARO can be interpreted as modal operators, cf. also footnote 5, which was proven by van der Hoek, [START_REF] Van Der Hoek | Formalizing potential of agents: the KARO framework revisited[END_REF]. Adding a notion of agenda to KARO, in order to deal with commitments, was proposed and studied by [START_REF] Meyer | A logical approach to the dynamics of commitments[END_REF] (see also footnote 6). Readers interested in knowing the details of our simplification as mentioned in footnote 8 are referred to the paper by [START_REF] Meyer | A logical approach to the dynamics of commitments[END_REF]. One of KARO's foundations is dynamic logic, for which the book by [START_REF] Harel | Dynamic logic[END_REF] is a standard reference. An early reference to the agent programming language GOAL (Goal-Oriented Agent Language) is provided by [START_REF] Hindriks | Agent programming with declarative goals[END_REF], while de Boer, [START_REF] De Boer | A verification framework for agent programming with declarative goals[END_REF] provide, rather than the language for declarative goals itself, both a programming framework and a programming logic for such computational agents. The connection with intention logic of Cohen & Levesque was given by [START_REF] Hindriks | GOAL agents instantiate intention logic[END_REF]. A starting point to get familiar with the software platform for GOAL is (2013). As an example of how logic frameworks can be beneficial for designers and programmers of agent systems, the KARO framework played an important role in devising the agent programming language 3APL by [START_REF] Hindriks | Agent programming in 3APL[END_REF]. Moreover, by formalising the relations between the KARO framework and the 3APL language, [START_REF] Hindriks | Agent logics as program logics: grounding KARO[END_REF] and Meyer (2007) were able to propose a verification logic for 3APL and its derivatives. As a proper treatment of this aspect of BDI logics goes beyond the scope of this chapter we refer to the literature on this issue, e.g., the work by van der Hoek and [START_REF] Van Der Hoek | Towards a logic of rational agency[END_REF], [START_REF] Dastani | A grounded specification language for agent programs[END_REF], [START_REF] Alechina | A logic of agent programs[END_REF], Dastani, Hindriks, and Meyer (2010), and by [START_REF] Hindriks | GOAL agents instantiate intention logic[END_REF].

Adding emotions to the mix of agents' attitudes is by now a well-respected avenue in agent-based modeling. Emotions are now regarded to complement rationality, rather than being in tension with it. This was acknowledged in for instance cognitive science through the work of [START_REF] Damasio | Descartes' Error: Emotion, Reason, and the Human Brain[END_REF], and is comparable with the rise of 'behavioural economics' complementing 'classical game theory' (for the latter, see also Chapter 9 of this book). See for instance 'Emotions and Economic Theory' by [START_REF] Elster | Emotions and economic theory[END_REF]. The work that we presented on emotions was inspired by two psychological theories: that of [START_REF] Oatley | Understanding Emotions[END_REF] and that of [START_REF] Ortony | The Cognitive Structure of Emotions[END_REF] (also referred to as OCC). More specifi-10.6. NOTES cally, KARO logic for emotional agents as based on Oatley & Jenkins' framework is worked out by Meyer (2006), while the formalisation of OCC theories is done by Steunebrink, Dastani, andMeyer (2007, 2012). References to the work of Adam et al. on emotions include the papers by [START_REF] Adam | Emotions: from psychological theories to logical formalization and implementation in a BDI agent[END_REF] and by [START_REF] Adam | A logical formalization of the OCC theory of emotion[END_REF]. Their introspective properties for emotion presented at the end of Section 10.3 are taken from Theorem 13 of the latter reference.

STIT (Seeing To It That) logics are an attempt of treating agency as a modality in an approach originating in a series of papers, beginning with the paper by [START_REF] Belnap | Seeing to it that: a canonical form for gentiles[END_REF]. Other important contributions in this field are by [START_REF] Chellas | On bringing it about[END_REF] and by [START_REF] Horty | Agency and Deontic Logic[END_REF]. A semantics for STIT based on worlds (rather than state-history pairs) was given by [START_REF] Balbiani | Alternative axiomatics and complexity of deliberative stit theories[END_REF]. The work of [START_REF] Semmling | From BDI and stit to bdi-stit logic[END_REF] adds BDI modalities to STIT logic. [START_REF] Lorini | A logic for reasoning about counterfactual emotions[END_REF] use STIT logic to analyse emotions. For further details and motivation for next-state STIT logic XSTIT we refer to work by [START_REF] Broersen | A complete stit logic for knowledge and action, and some of its application[END_REF]Broersen ( , 2011a)). The latter, together with Broersen (2011b) (which, among other things, discusses the side effect problem), is the place to further read on knowingly doing. Monotonic modal logic is presented in [START_REF] Hansen | Monotonic modal logics[END_REF]. Theorem 10.2 is taken from [START_REF] Xu | Axioms for deliberative stit[END_REF], and Theorem 10.4 from Broersen (2011a).

There have been a number of further developments, which can be seen as consequences of BDI logics. First of all we mention that on the basis of a BDI logic, [START_REF] Shoham | Agent-oriented programming[END_REF] initiated the field of agent-oriented programming (AOP), which is basically a way of programming the (BDI-like) mental states of agents as a new paradigm of programming. It could be viewed as a successor (or even refinement) of the well-known Object-Oriented (OO) Programming paradigm. Momentarily there is a host of such dedicated agent cognitive (BDI) programming languages (see the work by Bordini, Dastani, Dix, andSeghrouchni (2005, 2009)), including 2APL//3APL by [START_REF] Hindriks | Agent programming in 3APL[END_REF] and [START_REF] Dastani | 2APL: a practical agent programming language[END_REF] which is inspired by KARO.

Another extension that is made in the literature is a combination with reasoning with uncertainty. [START_REF] Casali | A graded BDI agent model to represent and reason about preferences[END_REF] propose a so-called Graded BDI logic. This means that beliefs, desires and intentions are not crisp anymore, but fuzzy. This is done by using a multi-valued base logic. In particular, a fuzzy modal operator D + is introduced with as reading "' is positively desired". Its truth degree corresponds to the agent's level of satisfaction would ' become true. It satisfies the principle D + (' _ ) $ (D + ' ^D+ ). There is also an analogous operator D , read "' is negatively desired". Intention is then defined from this. Their logic combines Rational Pavelka Logic (an extension of Lukasiewicz's manyvalued logic with infinitely many truth values by rational truth degree constants) as described by [START_REF] Hájek | Metamathematics of Fuzzy Logic[END_REF] with a multi-context logic of [START_REF] Giunchiglia | Multilanguage hierarchical logics (or: how we can do without modal logics)[END_REF] in order to account for the agents' mental attitudes. The approach allows for a much more fine-grained deliberation process. In particular, the process of deriving intentions can now be formally expressed as follows: the intention degree to reach a desire ' by means of a plan ↵ is taken as a trade-off between the benefit of reaching this desire and the cost of the plan, weighted by the belief degree r. [START_REF] Lorini | Trust and norms in the context of computer security: toward a logical formalization[END_REF] and [START_REF] Lorini | A dynamic logic of knowledge, graded beliefs and graded goals and its application to emotion modelling[END_REF] propose a similar graded approach to BDI, but now based on a sense of plausibility (non-exceptionality) as proposed by [START_REF] Spohn | Ordinal conditional functions: a dynamic theory of epistemic states[END_REF]. In this logic both the belief and the goal attitude are graded. Beyond modal operators of knowledge Know i , the logic of [START_REF] Lorini | A dynamic logic of knowledge, graded beliefs and graded goals and its application to emotion modelling[END_REF] has special atoms exc h indicating that the degree of exceptionality of the current state is h, where h ranges over a finite set of natural numbers Num. Then graded belief is defined as

Bel h i ' def = _ k h ⇣ ¬Know i (exc k ! ') ^l<k Know i (exc l ! ')

⌘

Graded goals Goal h i ' are defined in a similar way from special atoms des h indicating that the degree of desirability of the current state is h. This theory is next applied to the modelling of expectation-based emotions such as hope, fear, disappointment and relief, and their intensity.

Finally, in analogy to the area of belief revision, also a lot of work has appeared on the revision of the other mental states in BDI, notably intentions. In fact, intention reconsideration is already part of the first implementation of Bratman's theory as set out by [START_REF] Bratman | Plans and resourcebounded practical reasoning[END_REF] and is present in the BDI architecture of [START_REF] Rao | An abstract architecture for rational agents[END_REF] via the so-called BDI control loop. It also is present in the logical theory KARO of van Linder et al. (1995) and [START_REF] Meyer | A logical approach to the dynamics of commitments[END_REF] that we have seen earlier. Using a dynamic logic it is very natural to also incorporate actions in KARO that are mental state-revising such as belief revision as proposed by [START_REF] Van Linder | Actions that make you change your mind: belief revision in an agent-oriented setting[END_REF] and changes in commitments as studied by [START_REF] Meyer | A logical approach to the dynamics of commitments[END_REF]. But recently there have appeared more fundamental theories of intention revision, such as by van der Hoek, Jamroga, and [START_REF] Van Der Hoek | Towards a theory of intention revision[END_REF], where a logic of intention dynamics is developed based on dynamic logic and a dynamic update operator of the form [⌦]', meaning after the agent has updated on the basis of observations ⌦, it must be the case that '. The approach of beliefs, desires and intentions is rather syntactical (set of sentences without modalities for these mental attitudes interpreted by model structures). Contrary to this, van Ditmarsch, de Lima, and Lorini (2010) present a model-theoretic approach of intentions and intention dynamics. It uses modal operators for time, belief and choice as basis, and intention as a derived operator, and for intention change it employs a dynamic operator called local assignment. This is an operation on the model that changes the truth value of atomic formulae at specific time points. [START_REF] Shoham | Logical theories of intention and the database perspective[END_REF] discusses the interaction of belief revision and intention revision. This is done more in a traditional AGM sense as put forward by [START_REF] Alchourrón | On the logic of theory change: Partial meet contractions and revision functions[END_REF], than in a dynamic epistemic modal sense.

  Standard PDL is not about actions but about events. It has a set A of atomic event names. Cohen and Levesque add agents to the picture and provide an agentive version of PDL. Let us write i, j,etc.foragentsfromsomeset of and atomic actions by means of modal operators Poss ⇡ ,

  3. done(e) = succeeded(e) _ failed(e) 4. succeeds(e) = inevitableO(succeeded(e)) 5. fails(e) = inevitableO(failed(e)) 6. does(e) = inevitableO(done(e)) a

•

  is a mapping of first-order entities to U , for any world and time point • B, G, I ✓ W ⇥T ⇥W are accessibility relations for BEL, GOAL, IN T EN D, respectively a

  time trees:an elementw 2 W has the h w w w w i • T w ✓ T is the set of time points in world w • A w is the restriction of the relation to T w • S w : T w ⇥ T w ! E maps adjacent time points to (successful) events • F w : T w ⇥ T w ! E maps adjacent time points to (failing) events • the domains of the functions S w and F w are disjoint a

Proposition 10. 1

 1 Let BG be the class of models of the above form that satisfy the B-G condition. Then: BG |= GOAL(↵) ! BEL(↵) for O-formulas ↵. a Similarly one can define the G-I condition as 8w 0 2 G(w, t)9w 00 2 I(w, t) : w 00 w 0 and obtain: Proposition 10.2 Let GI be the class of models of the above form that satisfy the G-I condition. Then: GI |= IN T EN D(↵) ! GOAL(↵) for O-formulas ↵. a

  indicating failure of the commit action). 3. R uncommit↵ (M, w) = update_agenda (↵, (M, w)), if M, w |= Com(↵), otherwise R uncommit↵ (M, w) = ; (indicating failure of the uncommit action); 4. uncommit↵ 2 C(M, w) iff M, w |= ¬I(

  Definition 10.23 Relative to a model M = hS, H, E, V i, truth hs, hi |= ' of a formula ' in a dynamic state hs, hi, with s 2 h, is defined as: 10.4. BDI-MODALITIES IN STIT LOGIC hs, hi |= p , s 2 V (p) hs, hi |= ¬' , not hs, hi |= ' hs, hi |= ' ^, hs, hi |= ' and hs, hi |= hs, hi |= 2' , 8h 0 : if s 2 h 0 then hs, h 0 i |= ' hs, hi |= X' , if s 0 = succ(s, h) then hs 0 , hi |= ' hs, hi |= [ag xstit]' , 8s 0 , h 0 : if s 0 2 E(s, h, ag) and s 0 2 h 0 then hs 0 , h 0 i |= ' a Satisfiability, validity on a frame and general validity are defined as usual. xstit]' ^. . . ^3[ag n xstit] ! 3([ag 1 xstit]' ^. . . ^[ag n xstit] ) for Ags = {ag 1 , . . . , ag n } a

	Now we proceed with the axiomatization.
	Theorem 10.4
	The following axiom schemes, in combination with a standard axiomatization for
	propositional logic, and the standard rules ( like necessitation) for the normal
	modal operators, define a complete Hilbert system for XSTIT:
	S5 for 2
	For each ag, KD for [ag xstit]
	(Lin) (Sett) (XSett) [ag xstit]' ! X2' ¬X¬' $ X' 2X' ! [ag xstit]' (Indep) 3[ag 1

The standard notation is h⇡i';weheredeviatein ordertobeable todistinguish actual action from potential action.

This is therefore not a fused operator. In order to save space we do not give the the details of the semantics of that quantifier and rely on the reader's intuitions about it.

In fact, the ability operator can alternatively defined by means of a second accessibility relation for actions, in a way analogous to the opportunity operator below

.6 The agenda is assumed to be closed under certain conditions such as taking 'prefixes' of actions (representing initial computations). Details are omitted here, but see Section 10.6 for references.

We abuse our language here slightly, since strictly speaking we do not have quantification in our object language. See our references to KARO in Section 10.6 for a proper definition

.8 In fact, here we simplify matters slightly. One might stipulate that a goal should be explicitly selected somehow from the desires it has, which could be modelled by means of an additional modal operator. Here we leave this out for simplicity's sake.

In the meta-language we use the same symbols both as constant names and as variable names, and we assume universal quantification of unbound meta-variables.

However, it is not the emotions that are counterfactual; the theory is about factual emotions based on beliefs about counterfactual conditions

The reformulation is equivalent, but suggests a meaning of group action that is not standard: if ag1 only has an alternative under the provision that the choice of ag2 is kept fixed, then a standard interpretation would be that ag1 and ag2 have an alternative in cooperation. But, then the possibility to prevent also relies on cooperation. What seems needed for a notion of 'could have prevented' for individual agents, is that such agents have alternatives individually.

Acknowledgement

Thanks to Emiliano Lorini for his useful comments on an earlier version of this chapter.

The partition models the possible choices C s ag , C 0 s ag , C 00 s ag , . . . of ag in s. A choice profile hC s ag1 , C s ag2 . . . C s agn i at s is a particular combination of choices C s agi at s, one for each agent ag i in the system. For any s the intersection of choices in any choice profile is non-empty: T agi2Ags C s agi 6 = ;

In Definition 10.12 above, we refer to the states s as 'static states'. This is to distinguish them from 'dynamic states', which are combinations hs, hi of a static state and a history. Dynamic states function as the elementary units of evaluation of the logic. This means that the basic notion of 'truth' in the semantics of this logic is about dynamic conditions concerning choice performances.

We now define models by adding a valuation of propositional atoms to the frames of Definition 10.12. Definition 10.13 A frame F = hS, H, R ag i is extended to a model M = hS, H, R ag , V i by adding a valuation V of atomic propositions:

• V is a valuation function V : P ! 2 S⇥H assigning to each atomic proposition the set of state history pairs relative to which they are true.

We evaluate truth with respect to dynamic states. Now we proceed with the axiomatization.

Theorem 10.2

The following axiom schemes, in combination with a standard axiomatization for propositional logic, and the standard rules ( like necessitation) for the normal modal operators, define a complete Hilbert system for CSTIT:

The S5 axioms for 2 For each ag the S5 axioms for

propose an alternative axiomatization and a semantics whose units of evaluation are not two dimensional pairs hs, hi but one dimensional worlds w. Here we have chosen to give a two-dimensional semantics to emphasize the relation with the XSTIT semantics in section 10.4.2.

BDI-stit

Semmling and Wansing add BDI modalities to a basic Chellas stit logic as the one just defined. Their BDI-stit formalism extends the syntax as follows (we take the liberty of using our own notation for the BDI operators and to define an alternative but equivalent semantics).

Definition 10.15 Given a countable set of propositions P and p 2 P , and given a finite set Ags of agent names, and ag 2 Ags, the formal language L bdi-stit is:

To emphasize their weak modal character, we denote the introduced belief, desire, intention and possibility operators with a combination of sharp and square brackets. This alludes to the combination of first order existential and universal quantifications that is present in any first order simulation of a weak modal operator. The reading of the operators speaks for itself; they express belief, desire and intention concerning a proposition '.

The intuition underlying neighborhood functions is the following. N b (s, h, ag) gives for agent ag in situation hs, hi the clusters of possible worlds (situations / dynamic states) the joint possibility of which it believes in. Since clusters and propositions correspond to each other one-to-one (modulo logic equivalence of the propositions), it will also be convenient to look at the clusters or neighborhoods as propositions and to say that if N 2 N b (s, h, ag) the agent ag believes the proposition (modulo logical equivalence) corresponding to N , that N 2 N d (s, h, ag) holds if ag desires the proposition and that N 2 N i (s, h, ag) holds if ag intends the proposition. Now a. says that there is no belief, desire or intention for impossible states of affairs. b. says that belief, desire and intention are closed under weakening of the propositions believed, desired or intended. c. says that intentions are consistent in the sense that it is not possible to hold at the same time an intention for a proposition and for its negation.

CHP is not a normal modality (which is why we use the combination of sharp and square brackets, as explained before). Lorini and Schwarzentruber argue that their notion of CHP obeys agglomeration 'h

But, agglomeration is not necessarily an intuitive property for a notion of 'could have prevented': if the guard could have prevented prisoner 1 to escape through exit 1 and if the guard could have prevented prisoner 2 to escape through exit 2, it does not follow that the guard could have prevented both prisoner 1 to escape though exit 1 and prisoner 2 to escape through exit 2. We believe alternative definitions of the notion of 'could have prevented' are possible. In particular it seems promising to look for notions where the counterfactual conditions concerning alternatives are made explicit using the 3 operator.

With the right concepts in place, finally we are able to define the notion of regret for a proposition ' as the desire for ¬' in conjunction with knowledge about the fact that ' could have been prevented.

Definition 10.20 h[ag

Definitions like the one above for regret hinge on the possibility to express that certain actions or choices are actually performed. This type of expressivity is not provided by many other action formalisms.

BDI modalities in XSTIT: dynamic attitudes

In the systems discussed in Section 10.4.1, BDI notions were combined with STIT operators. However, in both approaches there was no special attention for a dynamic interpretation of the combination of BDI and STIT operators. Yet this interpretation strongly suggests itself. If an operator like [ag Cstit]' expresses that agent ag now exercises his choice to ensure that ', and a knowledge operator like [ag kno]' also has a dynamic reading (note that the truth condition of knowledge is not with respect to static states s but with respect to dynamic states hs, hi, cf. the clause for [ag kno]' just above Definition 10.18), then a natural interpretation of a combination like [ag kno][ag Cstit]' is that agent ag "knowingly sees to it that '". We suspect that this dynamic reading was not suggested by the authors of the discussed systems because these systems do not contain temporal modalities and because the used version of STIT has instantaneous effects. In this section we report on work studying the notions of knowingly and intentionally doing that is based on a version of STIT where agency inherently involves a move to some next state: XSTIT.

XSTIT

We give here the basic definitions for XSTIT. XSTIT enriches the CSTIT language of Section 10.4.1 with a temporal next operator and replaces the operator [ag Cstit]'