Programming Resource-Bounded Deliberative Agents

1 Introduction

The METATEM [Barringer et al., 1995] and Concurrent METATEM [Fisher, 1995] languages have been used as high­ level mechanisms for specifying and executing individual agents and multi-agent systems, respectively. Both are based upon the principle of specifying an agent using temporal logic, and then directly executing this specification in order to provide the agent's behaviour. This approach provides a high-level programming notation, while maintaining a close link between the program and its specification.

· Visiting Research Fellow from University of Trento, Italy, sup­ ported by the Italian National Research Council (CNR)

While this approach has provided a useful basis for experi­ mentation with both the logical representation and animation of agents, it has become clear that a more refined versio.n of the specification language is required if this framework 1s to be used for 'real world' agents. In particular, the METATEM family of programming languages originally contained no so­ phisticated mechanisms for representing deliberation within an agent, i.e. the process that an agent carries out in order to decide which goaVaction/plan to attempt.

Thus, inspired by the success of the BDI framework [R~o and Georgeff, 1991] in representing deliberation, the bas1c METATEM system was extended, in [Fisher, 1997b], with ex­ plicit mechanisms for ordering goals. Goals, corresp.onding to both desires and intentions in the BDI model were, m turn, represented by temporal eventualities. This then allowed de­ liberation to be represented using user defined functions pro­ viding an ordering on the satisfaction of eventualities.

While this provides a simple and concise mechanism for representing and implementing deliberative agents, it does not deal with a further important aspect of 'real' agents, namely their resource-bounded nature [Bratman et al., 1988]. In particular, the representation of belief was given .by ex­ tending the temporal basis with a standard modal log1.c hav­ ing Kripke semantics [Halpern and Moses, 1992]. As IS well known, this does not match the resource-bounded nature of 'real' reasoners [Giunchiglia et al., 1993]. Indeed modal logics generally model logically omniscent agents which are forced to believe (and compute) all the logical consequences of their own beliefs.

Thus, in this paper we modify the logic used in [Fisher, 1997b] by replacing the standard KD45 modal logic with a multi-context representation of belief [Giunchiglia and Ser­ afini, 1994; Benerecetti et al., 1997]. This logic is a modifi­ cation of KD45 which permits a simple execution mechanism to be employed over belief contexts. Consequently, it allows us to tightly control the use of belief contexts within deliber­ ative agents and so to represent resource-bounded reasoning. In addition, we also investigate the resource-bounded aspects of temporal reasoning. Thus, rather than allowing the agent to reason about the full underlying temporal logic, we exam­ ine how the agent can be restricted so that it reasons with an abstraction of the underlying temporal model.

The paper is structured as follows. In §2, we define the syntax and semantics of the particular logic used to represent agents. This will combine a simple temporal logic [Emer­ son, 1990] with a multi-context logic of belief [Benerecetti et al., 1997]. In order to provide the basis for the direct exe­ cution of this logic, we introduce, in §3, a particular normal form, that extends the Separated Normal Form used in the METATEM [Fisher, l997a]. An algorithm which can be used to directly execute formulae in this normal form is defined in §4, while an example of such execution is given in §5. The correctness of the execution algorithm is considered in §6. In §7, we consider the effects of restricting both the hypothet­ ical doxastic and temporal reasoning that can be carried out by an agent. Finally, in §8, we provide conclusions from this research and consider future work.

2 Temporal Logic of Bounded Belief

In this section, we give the syntax and semantics of our base logic (called a Temporal Logic of Bounded Belief, or TLBB for short) which combines propositional linear tem­ poral logic, with a multi-context belief logic. While temporal reasoning is essentially infinite, reasoning about beliefs can be bounded. In this sense, the logic allows the representation of bounded reasoning.

Syntax We are considering a situation with an agent, a, ob­ serving and representing beliefs about a set I = { 1, . .. , n} of agents. Formulae of TLBB are constructed using the fol­ lowing connectives and proposition symbols.

• A set, P , of propositional symbols.
• Propositional connectives, true, false, -,, V, 1\, and =>.
• Temporal connectives, 0, (), 0, U , and W .
• A set, { B1 , B2, ... , Bn}, of belief operators.

Let Jk be the set the set of (possibly empty) strings of the form i1 .. . ih with li1 .. . ihl :S k. We call any o: E Jk a view. Intuitively, each view in Jk represents a possible nesting of the belief operators. The empty string represents the view of the external agent a. The views 1 that a can build can be organized in a structure such as that presented in Figure 1.

We associate a logical language Lo: with each view. The set of well-formed formulae of Lo:, denoted by WFFo:, is inductively defined as the smallest set satisfying:

1 A more detailed description of the structure of views we are using can be found in [Benerecetti et al., 19971.

• Any element of Pis in WFFo:
• If 'ljJ and <pare in WFFo: then so are

• Bi'l/J [for all 1 :S i ::; n] is an atomic formula in WFFo: if, and only if, ¢is in WFFo:i

The set of well-formed formulae ofTLBB comprises the sets of well-formed formulae contained in each Lo:.

Semantics The semantics of the TLBB language is based on the semantics for contextual reasoning proposed in [Giunchiglia and Ghidini, 1998; Benerecetti et al., 1997]. Following this approach, the semantics of every formula is local to th.e view where we consider it. Therefore, we asso­ ciate to each view o: a discrete linear temporal model of time mo: with finite past and infinite future, e.g. (N, <),in order to interpret the temporal component of each language Lo:. Each of these moments in time, represented by a temporal index u E N, provides also a valuation 1r o: for the propositional part of the language and for (atomic) formulae of the form Bi'l/J· As usual, we define the semantics of each Lo: via the satisfia­ bility relation:

Satisfiability and validity are defined in the usual way.

The second step in defining the semantics for TLBB is to formalize the relation existing among different views. Indeed only a certain combinations of temporal models are compati­ ble and provide a model for TLBB. A model M for TLBB is a set M = { mo:} o:EJk such that for all o: E Jk :

1. if mo: f= Bi¢ then moi f= ¢;
2. if mo:i f= ¢then mo: f= Bi¢;
3. if mo: f= Bi¢ and Bi¢ E Lo:i then mo:i f= Bi¢;
4. if mo: f= ·Bi¢ and Bi¢ E Loi then mo:i f= ·Bi¢;

M satisfies a formula¢ E Lo: if mo: satisfies it.

Let us write o:: ¢to mean that¢ is a formula in Lo:. Each model M for TLBB satisfies the formulae o: : Bi ( ¢ => 'ljJ) => (Bi¢ => Bi'l/J), o:: Bi¢ => BiBi¢ and o: : ·Bi¢ => Bi'Bi¢· They are the TLBB versions of modal axioms K, 4, and 5, re­ spectively, and are obtained from conditions 1-4 in the defini­ tion of M. Moreover M satisfies the formulae o:: ·Bi·¢ => Bi¢ and o:: Bi¢ => ·Bi·¢. These are a consequence of the fact that M associates a unique temporal model mo: to each view and ensures that '·B;·' and 'B;' are equivalent. While the fact that each view has exactly one B;-accessible view en­ forces that each agent must either believe, or disbelieve, every atom, it does simplify the model structure, and hence the ex­ ecution, required. As we will see in §5, typical examples of agent reasoning are not affected by this addition.

3 Normal Form for TLBB

Formulae in TLBB can be transformed into a normal form SNFBB (Separated Normal Form for temporal logics of bounded belief). Separated Normal Form (SNF) is used as the basic normal form for linear-time temporal logics [Fisher, 1997a] and has been extended, for example to temporal log­ ics of knowledge in [Dixon et al., 1998]. The translation to SNF BB uses the renaming technique [Plaisted and Green­ baum, 1986] where complex subformulae are replaced by new propositions and then the truth value of these proposi­ tions are linked, in all states, to the formulae they replaced. In linear time temporal logic this is achieved by ensuring that such formulae are in the scope of a ' 0' operator, i.e. they hold at all reachable states. For TLBB we introduce the 0* operator, which allows arbitrary nesting of B; and 0 oper­ ators to achieve the same effect. As in the case of temporal logics of knowledge, the 0 * operator can be defined using fixpoints [Dixon et al., 1998].

Formulae in SNF BB are of the general form

where each T;, known as a rule, must be in one of the varieties described in Figure 2. Note that ka, lb, and l are all literals,

and the outer ' 0 *' operator that surrounds the conjunction of rules is usually omitted.

Example 3.1 Consider the TLBB formula

We can go through the following stages to transform this into SNFBB:

1. rename (OB21/J) by p and add ·P => O·B21/J;
2. rename ·B21/J above by q and add q => B2· 1/J ;
3. rename B2tp in (1) by rand add r => B2<p;
4. rename B1 (1/J V B2~) in (1) by sand add s => B1 (1/J V B2~);
5. rename (1/J V B20 in the above formula by t and add (ti\·1/J) => B2f

The original formula is now p => B1r 1\ Os, which can be split giving the final set of rules in SNF BB as:

1. p => B1r
2. p => Os
3. ·p => Oq
4. q => B2·1/J
5. r => B2<p
6. s => B1t
7. (t 1\ ·1/J) => B2X·

The key properties of the translation to SNF BB, characterised by the function 'r' are as in the temporal case [Fisher, 1997a].

Theorem 1 If TLBB formula <p is satisfiable, then r( <p) is satisfiable.

Theorem 2 If M is a model for r(<p) then M is also a model for <p.

Consequently, as execution is essentially model building in our framework, then we can execute r( <p) in place of <p.

4 Execution of SNF BB

In this section we give an algorithm for executing a set of SNF BB rules. Since lack of space precludes us from pro­ viding the algorithm in full detail, we will first present an outline of the execution mechanism for temporal logic, based on [Barringer et al., 1995] and [Fisher, 1997b], and will fol­ low this with a more detailed account of the execution of the belief element of the logic.

4.1 Executing Temporal Logic

The basic idea underlying METATEM [Barringer et al., 1995] is to directly execute a temporal formula, by attempting to build a model for the formula in a simple forward-chaining fashion. This is extended, in [Fisher, 1997b], whereby the choice of which formulae to satisfy is provided by user de­ fined deliberation functions, rather than by a fixed ordering heuristic. An outline of the basic approach, assuming that we are executing the set of rules, R, is given below.

1. By examining the initial rules, constraints on the possi­ ble start states for the temporal model can be generated. We choose one of these possible start states, deriving its valuation from the initial rules.

If all the possible start states have been explored, then we terminate stating that the set of rules, R, is unsatisfiable.

1. Generate constraints on next states, Cn, and constraints state of step and sometime rules, respectively.
2. onfuture states, c,, by checking applicability in current Cn represents all the possible choices of valuations for the next state, while c, provides the set of eventualities that must be satisfied at some time in the future.

1. Make a choice from Cn and check that the chosen val­ uation is consistent. If there are no unexplored choices, return to a choice point in a previous state.

The choice mechanism takes into account a combination of C 1, the outstanding eventualities, and the deliberation ordering functions [Fisher, 1997b].

1. Generate a new state, s, from the choice made in (3). Note that, by default, if propositions are not constrained
2. we choose to leave them unsatisfied.

Define s as being a successor to the current state and record the eventualities that are still outstanding (i .e. previously generated eventualities that were not satisfied in s); call this set of eventualities Evs.

If any member of Evs has been continuously outstand­ ing for more than 2 5 1RI states, then return to a previous choice point and select a different alternative.

1. With current state, s, and the set of outstanding eventualities, E vs, go to (2).

The key result here is that, under certain constraints on the choice mechanism within (3), this execution algorithm rep­ resents a decision procedure (previously presented in [Bar­ ringer et al., 1995]).

Theorem 3 If a set of SNF rules, R, is executed using the above algorithm, with the proviso that the choice in ( 3) en­ sures that the oldest outstanding eventualities are attempted first at each step, then a model for R will be generated if, and only if, R is satisfiable.

The above proviso ensures that, if an eventuality is outstand­ ing for an infinite number of steps, then it will be attempted an infinite number of times. Once the choice mechanism is ex­ tended to include arbitrary ordering functions, as in [Fisher, 1997b], then a more general version of the above theorem can be given wherein we only require a form of fairness on the choice mechanism. While the above proviso effectively means that we can potentially explore every possibility, the incorporation in the algorithm of a bound on the number of states that eventualities can remain outstanding, together with the finite model property of the logic, ensures that all of the possible states in the model will be explored if necessary.

4.2 Extending Execution

We now extend the above algorithm to handle the execution of SNF B B. The two main elements of the algorithm affected by this are that the execution process now builds a labelled tree, rather than a sequence, and that once a new belief state is built it must be checked for equivalence with previously generated states. Thus, rather than just generating a set of choices based upon temporal rules, we must now consider both temporal and belief rules. This will (often) lead to the construction of a number of belief contexts and (simulated) temporal sequences in order to derive these choices. For ex­ ample, in Figure 3 the basic temporal sequence (labelled by 'TL') is being constructed. However, at certain points, belief contexts (e.g. B 1 and B2) must be explored in order to de­ cide how to proceed. In addition, within these belief contexts, temporal execution itself can be simulated, e.g. B2(TL). Note that exploration of everything within a belief context will be carried out within a finite amount of time.

In order to incorporate the execution of belief operators into the algorithm described in §4.1, we add the following to the end of step (4).

For all belief operators, Bi, if expand(B;, R , s, 0) returns false, then return to a previous choice point and select a different alternative.

The function 'expand' explores belief contexts and attempts to build a model for the multi-context beliefs as follows.

expand(B; , R , s , D) : Boolean

1. Let CB, = /\ F, where (P => B;F) E Rands f= P ; if there are no such rules P => B;F, return true. Let C8, be DNF version of CB,, and remove all incon­ sistent disjuncts from C8, .
2. Choose a disjunct, d, from C8, ; if no unexplored dis­ juncts are available then immediately return false.
3. If D ::j:. 0, then conjoin the formulae in D with d to give d'; otherwise, let d' = d. Note that D contains the belief constraints from the last state and this operation corresponds to the persistence of beliefs given by axioms 4 and 5, e.g. f- Bicp => B ;B;cp.
4. Generate a new state, t, with valuation based on d'. If a state equivalent to t has occurred previously within this exploration from a basic temporal state, then make a Bi edge from s to this previous state and return true.

If no such equivalent state exists, then make a Bi edge from s tot

1. For all belief operators, B;, if any of expand(Bi, R , t , { d'}) returns false, then return to (2) and select a different alternative.
2. If tLexpand(R, t , 0) returns false, then return to choice point (2) and select a different alternative.
3. Return true.

The function tLexpand(Rules , State, E ventualities) ef­ fectively carries out temporal reasoning in a belief context. However, rather than continuing indefinitely, as the base-level algorithm does, it uses a tableau-like produce to ensure that a finite structure is constructed if the formula is satisfiable.

Rather than giving the detail of tLexpand, we note that it is very similar to the base-level temporal execution algorithm, although it does try to recognise repeated temporal states and so construct a finite graph rather than an infinite sequence. We will consider this temporal reasoning aspect further in §7.2.

5 Example

Consider the following example of an agent acting as a travel information provider (note that, for reasons of space, the ex­ ample is represented in predicate logic where variables range over finite domains).

1. ask(you,x) => BmeOgo(you,x) i.e., "if you ask for information about destination x, then I believe that you will holiday in x in the future"
2. Bme[Ogo(you, x) => ()buy(you, holiday, x)] i.e., "I believe that, if you will holiday in x in the future, then you will buy a holiday for x in the future"
3. BmeObuy(you, holiday, x) => Osend_info(you, x) i.e., "if I believe that you will buy a holiday for x in the future, I will send you information about holidays at x":

D) ask(you,x)

i.e., "you ask for information on destination x":

These translate to the following SNF BB rules.

Execution begins by ensuring that ask(you, x) is true in the initial temporal state and then exploring other choices. Thus, if we choose b to be false here, then we get a contradiction in the Bme(TL) simulation with (effectively) O·go(you,x) (from rules B5-B8) and ()go(you, x) (from rule A2).

Similarly, if we choose e to be false, we get a contradiction in the Bme (T L) simulation with ( effec­ tively) O·buy(you, holx) (from rules C10-C13) and ()buy(you, holx) (from rule B4) .

Thus, we eventually choose to satisfy ask(you, x), band e together in the initial state, which in turn leads to the execu­ tion of send_info(you, x) in the next state.

The model eventually produced is given in Figure 4.

6 Correctness

As in the case with the basic METATEM system, we can show that the extended system can be used as a decision procedure for TLBB if necessary.

Theorem 4 If a set of SNFBB rules, R, is executed using the above algorithm, and the choices made by the temporal component ensure that the oldest outstanding eventualities are attempted first at each step, then a model for R will be generated if, and only if, R is satisfiable.

The proof follows by showing that the above execution mech­ anism will (eventually) explore all the tableau structure for TLBB [Ghidini, 1998; Wooldridge et al. , 1998]. In particu­ lar, the execution within belief contexts explores potential lin­ ear sequences of such contexts until either a model is found, or until no unexplored possibilities remain and so the belief formula is unsatisfiable.

In general, the mechanisation of such a logic is relatively easy since there are no axioms defining interactions between the different belief/temporal operators. Thus, the sub-logics within TLBB can effectively be treated separately, and decid­ ability of TLBB is retained [Blackburn and de Rijke, 1997].

7 Resource-Bounded Reasoning

In §4.2, we considered the execution of the temporal logic of bounded belief with (effectively) infinite bounds on belief reasoning capabilities. Now we will examine how the effect that introducing resource bounds of various kinds will have on this execution mechanism.

7.1 Bounded Reasoning

The most obvious thing to do (and indeed this was the main motivation for this work) is to set an explicit bound on the depth of belief reasoning allowed. In order to modify the ex­ ecution mechanism, we just need to add an extra argument to the expand and tl_expand functions. This argument will represent the depth of nesting of belief contexts. Thus, in the first call to expand (from the basic temporal execution), the depth is 0. In the definition of the expand function itself, the depth is incremented when the function is invoked recur­ sively. Finally, we require an additional condition in expand stating that backtracking will occur if the depth bound reaches its limit (i.e. the maximum depth of nested beliefs allowed).

Given that we can bound the agent's ability to reason about belief, then can we do the same with temporal reasoning? In principle, yes. However, a bounded multi-context semantics for the type of temporal logic we use is quite complex, and we have not yet considered restricting the logic in this way.

7.2 Abstract Temporal Reasoning

From a practical point of view, carrying out hypothetical reasoning within propositional linear-time temporal logic is quite expensive. While the logic is decidable, the decision problem is PSPACE-complete [Emerson, 1990]. Also, al­ though the execution mechanism for METATEM is complete, and thus could be used as a (naive) theorem-prover for the logic, the execution mechanism is not at all efficient in this respect. We propose a modified logical framework which consists of three elements: (full) propositional linear tem­ poral logic for the agent's basic· execution; bounded (multi­ context) belief; and 'simulated' temporal logic, comprising only '<)', but no '0' operator (this logic is only used within belief contexts and is equivalent to KDT4 modal logic). The tl_expand function described in §4.2 now executes the KDT4 logic, rather than temporal logic.

While the restriction of the capability of an agent to reason only about 'abstract' elements of time in a belief context may seem too extreme, it does significantly reduce the complex­ ity of the execution mechanism. In addition, it is debatable whether an agent should be able to reason about the exact detail of the time structure in which it is situated. Further, if an agent wishes to reason about the temporal behaviour of another agent, then the asynchronous nature of agent execu­ tion means that a step in one agent will not necessarily match a step in the other. Thus, perhaps an agent should only be able to reason about another agent reaching a certain state at some point in the future. Hence the use, within hypothetical temporal reasoning, of just the '<)' operator.

8 Conclusions and Future Work

We have considered the extension of basic executable tem­ poral logic (of the METATEM style) with bounded reasoning about belief and time. In particular, we have proposed the ver­ sion of the logic in §7 .2 as a practical basis for the high-level logic-based programming of resource-bounded agents.

It is important to note that we are not interested in generat­ ing alternative mechanisms for undertaking temporal/modal proof. The main element we are concerned with is the exe­ cution of temporal formulae in order to generate an infinite sequence. However, at certain points hypothetical reason­ ing needs to be carried out and belief contexts must be ex­ plored. We could have used standard proof mechanisms for non-interacting temporal and doxastic logics [Wooldridge et at. , 1998] at this point (and, indeed, our intention is to provide this possibility within the full implementation). However, (a) we would like to retain the common execution mechanism throughout, (b) by representing belief exploration in terms of execution the whole process should be more amenable to meta-level control, and (c) while belief exploration is neither very common nor very complex, it makes sense to keep the execution mechanism simple.

Finally, the execution mechanism described in this pa­ per provides a way to execute multi-context logics of this form [ Giunchiglia and Serafini, 1994] using the Imperative Future [Barringer et at., 1996] style of executable logics.

Future work includes testing a full implementation on larger examples, incorporating belief revision and persis­ tence, and investigating the addition of real-time aspects.