BDIOCTL: Obligations and the Specification of Agent Behavior

1 Introduction

Recently several agent architectures have been proposed that incorporate obligations. However, agent specification or ver­ ification languages that take obligations into account have re­ ceived less attention. Our research question is how properties involving obligations can be specified or verified in an exten­ sion of Rao and Georgeff's BDicrL· In Section 2 we extend BDlcrL with so-called Standard Deontic Logic, and in Sec­ tion 3 and 4 we introduce various single agent and multiagent properties.

2 BDIOcTL

We use an equivalent reformulation of Rao and Georgeff's formalism [1991] presented by Schild [2000], which we ex­ tend with Standard Deontic Logic (SDL, Von Wright [ 1951 ]). We only consider the semantics.

Definition 1 (Syntax BDIOcTd Assume n agents. The ad­ missable formulae of BDI en are categorized into two classes, state formulae and path formulae.

• Sf Each primitive proposition is a state formula.
• S2 If a and fJ are state formulae, then so are a 1\ fJ and ·a.
• S3 If a is a path formula, Ea and A a are state formulae.
• S4 If a is a state formula and 1 ::; i ::; n, then B ;(a), D;(a), I;(a), O;(a) are state formulae as well.
• P If a and fJ are state formulae, then X a and aU fJ are path formulae.

The semantics of BDicTL involves two dimensions. The truth of a formula depends on both the world w and the tem­ poral state s. A pair (w, s) is called a situation in which BDicTL formulae are evaluated.

Definition 2 (Situation structure BDIOcTd Assume n agents. A structure M = (6., R, 81, D1,I1 , 01 , ... , On , L) forms a situation structure if 6. is a set of situations, R ~ 6. x 6. is a binary relation such that w = w' whenever (w, s)R (w', s'), Z; ~ 6. x 6. for Z E {B, D , I , 0} and 1 ::; i ::; n are binary relations such that s = s' whenever (w, s)Z;(w',s'), and L an interpretation function that assigns a particular set of situations to each primitive proposition. L(p) contains all those situations in which p holds.

Mehdi Dastani

ICS, Utrecht University The Netherlands mehdi @cs.uu.nl

Leendert van der Torre

CWI Amsterdam The Netherlands torre@cwi .nl

A speciality of CTL is that some formulae - called path formulae- are not interpreted relative to a particular situation. What is relevant here are full paths. The reference to M is omitted whenever it is understood.

Definition 3 (Semantics BDIOcn) Assume n agents. A full path in situation structure M is a sequence x = c50 , c51 , c52 , ... such that for every i :::0: 0, c5; is an element of 6. and c5iRc5i+1, and if X is finite with c5n its final situation, then there is no situation c5n+l in 6. such that c5nRc5n+l· We say that ajitll path starts at c5 iff c5o = c5. If X = c5o, c51 , 62, ... is a full path in M, then we denote c5; by xi (i :::0: 0).

Let M be a situation structure, c5 a situation, and x a full path. The semantic relation f= for BDIOcn is then defined as follows:

• SJ c5 f= p iff c5 E L(p) and p is a primitive proposition
• S2 c5 f= a 1\ fJ iff c5 f= a and c5 f= fJ c5 f= ·a iff c5 f= a does not hold
• S3 c5 f= E a iff 3 full path X in M starting at c5 s. t. X f= a

c5 f= Aa iff't/ full path X in M starting at c5, X f= a

• S4 c5 f= B ;(a) iff for every c5' E 6. such that c5B;c5', c5' f= a
• c5 f= D; (a) iff for every c5' E 6. such that c5D;c5', c5' f= a

c5 f= l;(a) iffforeveryc5' E 6. suchthat c5I ;c5', c5' f= a

• c5 f= O;(a) iff for every c5' E 6. such that c50;c5', (j' f= a
• Pxf=Xaiffx 1 f=a

X f= aU fJ iff there is at least one i :::0: 0 such that xi f= fJ and for all j(O ::; j < i), x1 f= a

As usual 'globally a' (on a path) is defined as G(a) aU _1_ and 'at some future moment a holds' as F(a) = · G(·a).

We do not discuss the correspondence between modal properties and conditions on binary relations B;, D;, I ;, and 0; , but discuss possible specification properties expressible as modal formulae.

Rao and Georgeff discuss realism properties

and commitment strategies, e.g.:

3 Single agent properties

The following properties characterize the relation between mental attitudes of a single agent.

3.1 Regimentation

A main question when developing a normative system is whether the norms can be violated or not, i.e. whether the norms are soft or hard constraints. In the latter case, the norms are said to be regimented. Regimented norms corre­ spond to preventative control systems in computer security. For example, in the metro in Paris it is not possible to travel without a ticket, because there is a preventative control sys­ tem, whereas it is possible to travel without a ticket on the French trains, because there is a detective control system. Norm regimentation for agent i is characterized by:

Strong and weak epistemic norm regimentation are:

And intentional norm regimentation is:

A variant of the latter regimentation is conditional to a con­ flict between agent i's internal and external motivations. For example, if an agent is obliged to work but desires to go to the beach, then it intends to go to work. Or at least it does not intend to go to the beach. An agent is called strongly or weakly respectful if:

Moreover, a respectful agent can internalize its obligations in the sense that they tum into desires, or at least it cannot decide to violate the obligation. For example, if an agent is obliged to work then it also desires to work, or at least it cannot desire not to work.

Instead of respectful, agents may also be egocentric, which can be characterized by similar properties:

3.2 Persistence

Obligations typically persist until a deadline, e.g. deliver the goods before noon, or they persist forever, e.g. don't kill. We denote a deadline obligation by Oi(p, d), where achieve­ ment of the proposition d is the deadline for the obligation to achieve p. A deadline obligation Oi (p, d) persists until it is fulfilled or becomes obsolete because the deadline is reached:

A deadline obligation Oi(p,p), for which the only dead­ line is the achievement of the obligation itself, is called an 'achievement obligation'. We may characterize that Oip is an achievement obligation by:

Alternatively, we may characterize that Oip persists for­ ever, i.e. that it is a 'maintenance obligation', by:

4 Multi-agent Obligations

In a multi-agent setting agents interact with each other, thereby creating obligations. For example, in an electronic market where agents interact to buy and sell goods, sending a confirmation to buy an item creates the obligation of payment by the buyer and the obligation of shipment of the item by the seller. Social systems may be designed in which obligations are related to the mental attitudes of other agents. For exam­ ple, there may be communities in which agent i may adopt all the obligations of agent j.

The following property characterizes that agent i adopts the desires of agent j as its obligations. For example, if agent j desires to eat then agent i is obliged to see to it that he gets something to eat.

In a master slave relationship, the intentions of the master become the obligations of the slave.

Agent i is a dictator if for every other agent j it holds that:

Finally, a particular kind of dictator i is one whose desires immediately turn into obligations of another agent j.

5 Summary

In this paper we have introduced the BDIOCTL logic; a com­ bination of Rao and Georgeff's BDicTL formalism and stan­ dard deontic logic SDL. We have defined several specification and verification properties in this logic. The formalization of other properties is the subject of further research. The option most discussed in deontic logic is whether violations of norms can trigger new obligations, i.e. whether there is contrary-to­ duty reasoning. For example, it is often assumed that the legal code does not contain contrary-to-duty norms. Properties re­ lated to contrary-to-do reasoning are therefore of particular interest.