A Model-Theoretic Approach to the Verification of Situated Reasoning Systems

1 Introduction

The study of systems that are situated or embedded in a changing environment has been receiving considerable attention within the knowledge representation and plan­ ning communities. The primary characteristic of these systems is their dynamic and resource-bounded nature. In particular, situated systems need to provide an ap­ propriate balance between time spent deliberating and time spent acting. If the time spent on deliberation is too long, the ability of the system to complete its tasks may be seriously affected. On the other hand, too little deliberation may lead to a system that is short-sighted and reactive.

A number of different architectures have emerged as a possible basis for such systems [Bratman et al., 1988; Rao and Georgeff, 1991b; Rosenschein and Kaelbling, 1986; Shoham, 1991]. Some of the most interesting of these are agent-oriented architectures, in which the sys­ tem is viewed as a rational agent having certain men­ tal attitudes that influence its decision making and de­ termine its behaviour. The simplest of these architec­ tures, called a BDI architecture, is based on attitudes of belief, desire, and intention. The first two attitudes represent, respectively, the information and evaluative states of the agent. The last represents decisions the agent has made at a previous time, and is critical for achieving adequate or optimal performance when delib­ eration is subject to resource bounds [Bratman, 1987; Kinny and Georgeff, 1991]. Recently, a number of attempts have been made to formalize these mental attitudes and to show how these attitudes determine the actions of an agent [Cohen and Levesque, 1990; Rao and Georgeff, 1991b; .Singh, 1991].

Most of these studies on agent-oriented systems con­ centrate on the specification or characterization of ratio­ nal agents and their behaviours under different environ­ mental conditions. They introduce logics that use linear or branching temporal structures, are often first-order, and tend to have a rich repertoire of modal operators to model beliefs, desires, goals, intentions, commitment, ability, actions, and plans.

However, the design of agent-oriented systems has so far had little connection with these formalisms. Al­ though some systems have been designed and built upon the philosophy of rational agents [Georgeff and Lansky, 1986], the linkage between the formal specification and the design is weak. Similarly, little has been done in the verification of agent-oriented systems. As more and more of these systems are being tested and installed in safety-critical applications, such as air-traffic manage­ ment, real-time network management , and power-system management, the need to verify and validate such sys­ tems is becoming increasingly important.

This paper addresses the issue of verification of situ­ ated systems based on the the theory of rational agents. Issues related to the specification and practical design of agent-oriented systems are dealt with elsewhere [Rao and Georgeff, 1991b; Rao and Georgeff, 1992]. The out­ line of the paper is as follows. Section 2 describes the semantic model. Section 3 presents three branching-time BDI logics with increasing expressive power and intro­ duces the notion of commitment. The problem of veri­ fication in these logics and their complexity is described in Section 4. Using an example, Section 5 shows how one can verify temporal and commitment properties of agent-oriented systems in polynomial time. Finally, we conclude in Section 6 by comparing our work with re­ lated effort and highlighting the contributions of this paper.

2 Overview

Situated agents can be viewed as concurrent systems of processes. The execution of such processes can be mod­ eled by the nondeterministic interleaving of the atomic actions of each process. In such a model, the nondeter­ ministic choice of a concurrent program is represented as a time point with multiple successors in a branching-time tree structure. Each possibly infinite execution sequence of a concurrent program is represented as a computation path of the tree structure.

For systems based on the notion of a rational agent, however, such a model of the system's behaviour is too abstract. In this case, one is interested in analyzing how such agents choose to bring about the future that they desire. In so doing, the agent needs to model the un­ certainty or chance inherent in the environment as well as the choice of actions available to it at each and every time point. As the agent does not have direct control over the environment, but has direct control over the ac­ tions it can perform, it is desirable to separate the agent's choice of action (over which it has control) from its view of the environment (over which it has no control). Also, unlike concurrency theory, there is no single view of the environment; each agent can have its own view of the en­ vironment and of other agents' mental states which may not coincide with the actual environment nor the ac­ tual mental states of these agents. These different views of the world can be more effectively modeled within a possible-worlds framework.

Hence, we adopt a possible worlds branching-time tree structure in which there are multiple possible worlds and each possible world is a branching-time tree structure. Multiple possible worlds model the chance inherent in the environment as viewed by the agent and are a result of the agent's lack of knowledge about the environment. But within each of these possible worlds, the branching future represents the choice of actions available to the agent.

A particular time point in a particular world is called a situation. For each situation we associate a set of belief-accessible, desire-accessible, and intention­ accessible worlds - intuitively, those worlds that the agent believes to be possible, desires to bring about, and commits to achieving, respectively. We require that an agent's intentions be consistent with its adopted desires, and that its desires be believed to be achievable [Rao and Georgeff, 1991a].

One of the important properties in reasoning about concurrent programs is the notion of fairness . Fairness or fair scheduling assumptions specify when an individ­ ual process in a family of concurrent processes must be scheduled to execute next. A number of different fair­ ness assumptions have been analyzed in the literature. 1 A commonly used fairness assumption is that a process must be executed infinitely often. A concurrent program can thus be viewed as a branching-time tree structure, with fairness and starting conditions. The verification of a property is equivalent to checking if the property is satisfied in the model corresponding to the concurrent program under the fairness and starting conditions. As described by Emerson [1990], concurrency can be ex­ pressed by the following equation: concurrency = non­ determinism + fairness.

1 See Emerson [1990] for an overview on this topic.

Analogously, an important aspect of rational agency is the notion of commitment. The commitment condition specifies when and for how long an agent should pursue a chosen course of action and under what conditions it should give up its commitment. Thus, a commitment condition embodies the balance between reactivity and goal-directedness of an agent-oriented system. An ab­ stract agent-oriented system can thus be viewed as a possible worlds branching-time tree structure with com­ mitment and starting conditions. The verification of a property of the agent-oriented system is equivalent to checking if the property is satisfied in the model cor­ responding to the system under the commitment and starting conditions. We could therefore express agent­ oriented reasoning as follows: agent-oriented reasoning = chance + choice + commitment. In the next two sec­ tions we formalize these notions.

3 Propositional BDI Logics

3.1 Syntax

We define three languages CTLsm, CCTLsm (Com­ mitted CTLsm), and CTL8m, which are propositional modal logics based on the branching temporal logics CTL, Fair CTL, and CTL* [Emerson and Lei, 1987], re­ spectively, with increasing expressive power. The prim­ itives of these languages include a non-empty set ~ of primitive propositions; propositional connectives V and ...,; modal operators BEL (agent believes), DESIRE (agent desires), and INTEND (agent intends); and temporal op­ erators X (next), U (until), F (sometime in the future or eventually), E (some path in the future or optionally), and E€ (some committed path € in the future). Other connectives and operators such as /1., :::>, =:, G (all times in the future or always), A (all paths in the future or 00 inevitably), A€ (all committed paths € in the future), F

00 (infinitely often), and G (almost always) can be defined in terms of the above primitives. The last two operators are defined only for CTL8m.

There are two types of well-formed formulas in these languages: state formulas (which are true in a partic­ ular world at a particular time point) and path formu­ las (which are true in a particular world along a certain path) . State formulas are defined in the standard way as propositional formulas, modal formulas, and their con­ junctions and negations. The objects of E and A are path formulas. Path formulas for CTL8m can be any arbitrary combination of a linear-time temporal formula, containing negation, disjunction, and the linear-time op­ erators X and U. Path formulas of CTLsm are restricted to be primitive linear-time temporal formulas, with no negations or disjunctions and no nesting of linear-time temporal operators. For example, AF(p V q) is a state formula and GFp is a path formula of CTL8m but not ofCTLsm.

In contrast to the language CTLsm, Committed CTLsm uses the path operators Ee and Ae followed by one of the linear-time temporal operators X, U, F, and G. The symbol { is used to emphasize the fact that these operators range over paths that meet a commit­ ment constraint; namely, that e is of the canonical form n oo oo A= 1(F(ai) V G(.Bi)), where O'i and .Bi are commitment formulas (described in Section 3.3). The formula Ae{t can be viewed as a CTL001 formula A({ :::> 6) and similarly Ee6 can be viewed as a CTL001 formulaE({ 1\ 6). We shall call the above conversion *-conversion.

The length of a formula </> is denoted by 1<1>1 and is defined recursively as follows [Emerson and Lei, 1987]: (a) the length of a primitive proposition is zero; and (b) the length of conjunctive, negated, modal, and temporal formulas is one more than the sum of the sizes of their component formulas. The formula t/J is said to be a sub­ formula of </> if t/J is a substring of </>. Let Sub(</>) be the set of all subformulas of </>.

For example, the formula -.p 1\ BEL(p 1\ q) has a length of 4. The subformulas of the above formula is given by {-.p 1\ BEL(p 1\ q), -.p, BEL(p 1\ q), p, p 1\ q, q}.

3.2 Possible-Worlds Semantics

We define a structure M to be a tuple, M = (W, T, n, 8, Q, I, L) where Tis a set of time points; n ~ T x T is a total binary temporal accessibility relation; ~ is the set of primitive propositions; W is a set of possible worlds, where each world w is a tuple of the form (Tw, 'Rw, Lw) in which Tw E Tis a set of time points in w, 'Rw is a restriction of n to the time points Tw, and Lw is the truth assignment function that assigns to each time point in w a set of propositional formulas, i.e., Lw: Tw - 2~ . Finally, 8 ~ W x T x W is a belief accessibility relation; and g and I are desire and intention accessibil­ ity relations, respectively, that are defined in the same way as 8.

Sometimes, we shall view the arcs of the· time tree as being labeled with a primitive event, i.e., n ~ T X E X T, where E is the set of primitive events that is added to the structure M.

A fullpath, x =(so, St, ... ) in w is an infinite sequence of time points such that (si, Si+d E nw for all i. The suffix full path ( Si, Si+l, ... ) is denoted by xi . Satisfaction of a state formula </> is given with respect to a structure M, a world wand a time point t, denoted by M, w, t f: </>. Satisfaction of path formulas is given with respect to a structure M, world w, and a fullpath x in world w.

M, w, t f: BEl(¢) iff M, w', t f: </>for all w' satisfying (w, t, w') E 8;

M, w, t F= E(e) iff M, w, x F= e where x is a fullpath in world w starting at t ;

M, w, x f: X(¢) iff M, w, x 1 f: </>;

M, w, x f: </>tU</>2 iff for some i ~ 0, M, w, xi f: <1>2 and for all 0 ~ j < i, M, w, xi f: </>1;

The semantics of primitive propositions, negations, and conjunctions of formulas are defined in a standard manner and the semantics of temporal formulas are as defined for CTL * [Emerson, 1990]. Semantics of formu­ las in CCTLsm containing committed path operators Ee and A{ is given by converting them into CTL001 for­ mulas and then using the above satisfaction conditions. We use M, w, t f=e </> as an abbreviation for M, w, t f: </>*, where </>* is a CTL001 formula obtained from </> using the *-conversion.

Desires and intentions are defined as for beliefs but with respect to their corresponding accessibility rela­ tions. The relationships between beliefs, desires, and intentions impose different restrictions on these acces­ sibility relations. These relationships have been dis­ cussed by us elsewhere [Rao and Georgeff, 1991a; Rao and Georgeff, 1991b]. Finally, using the above basic modal operators we can define the additional modal op­ erators as follows: F</> as true U </>; G</> as -.F-.¢; A</> as 00 00 -.E-.{; F</> as GF¢; and G</> as FG¢.

3.3 Commitment

Commitment plays an important role in agent-oriented reasoning. In a continuously changing environment, commitment lends a certain sense of stability to the rea­ soning process of an agent . For example, if John is com­ mitted to going to the bank at 2pm, he is unlikely to re-evaluate this decision at every clock tick; instead, he would probably re-evaluate his decision (or give up his commitment) only if there were a significant change in circumstances. In other words, commitment and its rela­ tive stability with respect to changes in beliefs results in savings in computational effort and hence better overall performance [Bratman, 1987; Kinny and Georgeff, 1991; Rao and Georgeff, 1991b].

A commitment usually has two parts to it: one is the condition that the agent is committed to maintain, called the commitment condition, and the second is the condi­ tion under which the agent gives up the commitment, called the termination condition. More formally, we de­ fine a commitment operator C as follows:

</>tC</>2:: A(<f>t U </>2);

where </>1 is a commitment condition and </>2 is a termi­ nation condition. The commitment formula </>1 C</>2 (read as </>1 is inevitably committed until </>2) states that, if the commitment condition <f>t is true, in all future paths the agent will commit to (or maintain) <f>t until the termi­ nation condition </>2 is true. Note that </>1 and </>2 can be arbitrary state formulas of the language CTLsm and the commitment formulas also belong to CTLsm. Within this basic framework one can express a number of differ­ ent types of commitment in the language CTLsm.

As the agent has no direct control over its beliefs and desires, there is no way that it can adopt or effectively re­ alize a commitment strategy over these attitudes. How­ ever, an agent can choose what to do with its intentions. Thus, we restrict the commitment condition ¢1 to be of the form INTEND(A{) or INTEND(E{). The former we call full commitment and the latter a partial com­ mitment. The exact form of the termination condition yields different types of commitment. We review three types of commitment that were described elsewhere [Rao and Georgeff, 1991b]: blind commitment in which the termination condition </>2 is of the form BEL(</>); single­ minded commitment in which ¢2 is of the form BEL(</>)

V ~BEL(EF(</>)); and open-minded commitment in which </>2 is of the form BEL(</>) V ~DESIRE(EF(</>)).

An agent that is blindly committed will give up its commitment only when it believes in </>, where </> is usu­ ally a proposition that the agent is striving to achieve. In addition to this, an agent who is single-mindedly com­ mitted will give up its commitment when it no longer be­ lieves that there exists an option of satisfying the propo­ sition some time in the future. An agent that is open­ mindedly committed will give up its commitment either when it believes in the proposition or when it no longer has the desire to eventually achieve the proposition.

One can combine the above forms of commit­ ment in various ways. For example, the for­ mula (INTENO(Afp))C(BEL(p)) denotes an agent that is blindly and fully committed to achieving p until it believes in p. Similarly, the formula (INTEND(EFp))C(BEL(p) V ~BEL(EFp)) is an example of an agent that is single-mindedly partially committed to achieving p (i.e., has decided not to rule out the posi­ ibility of not being able to achieve pin the future).

For an agent to eventually achieve its desires, it needs to maintain its commitment to bring about these desires. Although an agent that only occasionally maintains its commitment may serendipitously fulfill its desires, as de­ signers of these systems we cannot guarantee this. To do so, we need to impose stronger maintenance condi­ tions; namely, that the commitment formula is true "in­ finitely often" or "almost always". Hence, in Committed CTLam we take the commitment constraint e to be of h . n oo oo t e canomcal form/\; = 1 ( F (a;) V G(,B;)), where a; and ,8; are commitment formulas .

4 Verification

Our interest is in determining what properties hold of a given agent, in a given environment, under certain initial conditions and under certain commitment condi­ tions. For example, given a robot that is programmed to single-mindedly commit to a certain set of intentions, we may need to prove that, in a particular environment and under particular initial conditions, it will never harm a human.

Given some specification of the agent and the envi­ ronment, we can generate the branching-tree structure corresponding to all possible evolutions of that agent in that environment.2 This structure represents the model M of the agent and its environment. For the purposes of this paper, we consider only finite structures. The size of a finite structure M is given by the size of the differ­ ent components of the structure. More formally, IMI = O(IWI · (I'R.I + IBI + lgl + III)). The size of W is equal to the number of worlds and the size of the relations is equal to the number of elements in the relation.

2 We do not address this process of model generation in this paper. Methods for generating models used in concur­ rency t·heory [Emerson, 1990] can be extended for this pur­ pose. The notion of plans as abstract sp·ecifications [Rao and Georgeff, 1992] is similar to that of finite-state transitions and can be used to generate a partial model.

We assume that the initial environment-agent configu­ ration of the system is given by a state formula </>sTART· We shall refer to the tuple (M, </>sTART) as an abstract agent-oriented system. As designers of these systems, we want to be able to verify that given an abstract agent­ oriented system, certain properties of the system, ex­ pressed as state formulas, are true. The abstract system and the properties can be expressed in either CTL801 or CTLrmi· More formally we have the following definition.

Definition 1:

Verification of abstract agent-oriented systems (M, </>sTART) F= </> iff'v' w, tin M such that M, w, t F= </>sTART we have M, w, t }= </>.

Hence, the verification problem for CTLam reduces to the Model Checking Problem for CTLam (MCP), de­ fined as follows: Given a structure M = (W, T, 'R., B, g, I, L) and a state formula</>, determine for each world w and time point t whether M, w, t f= </>.

Informally, an algorithm, AMCP for solving the Model Checking Problem can be given as follows: Start with subformulas of </> that are of length 0, determine the worlds and time points where they are true, and then progressively process subformulas of length greater than 0. After i such steps where I <PI ~ i, the set of worlds and time points where </> and all its subformulas are true will be known.

This algorithm is a modification of the algorithm given by Emerson and Lei [1987] for their Fair Computation Tree Logic (FCTL). The main difference in model check­ ing is the presence of multiple possible worlds. The com­ plexity of the algorithm AMCP is stated below; its de­ tails can be found elsewhere [Rao and Georgeff, 1993].

Theorem 1 Algorithm AMCP correctly solves MCP by labeling each world w and time point t of the structure M with the set of subformulas of</> true at w and t, and takes O{l</>1 . IMIJ time to run.

Although CTLam can capture different forms of com­ mitment, it is still not expressive enough for our pur­ poses. For example, the language is not expressive enough to state that if a robot is always committed to serving its master, then no matter what tasks it does it will in all cases eventually satisfy its master. In par­ ticular, we cannot state that in all paths that satisfy a certain commitment formula, say 6, a property, say 6, holds. More formally, we cannot express A[6 :::> 6].

As was discussed earlier, Committed CTLam can ex­ press such statements. Now we analyze the complex­ ity of verifying abstract agent-oriented systems based on Committed CTLam. In CCTLam, an abstract agent­ oriented system is taken to be a tuple (M, tPSTART 1 e), where M and tPST ART are as defined before and e is a commitment constraint. More formally, verification of these systems can be defined as follows:

Definition 2:

Verification of abstract agent-oriented systems (M, ¢sTART, e) F= </> iff'v' w 'tin M such that M, w, t F= <l>sT ART we have M, w, t F=e </> .

Similar to the model checking problem of CTL801 , one can analogously define the Model Checking Problem for Committed CTLom (CMCP). Complexity results given for FCTL by Emerson and Lei [1987] can be extended to CMCP. In particular, CMCP can be reduced to the problem of model checking for committed states. This reduction exploits the nature of the commitment conoo 00 straint e; namely, the fact that F and G are oblivious to the addition and deletion of finite prefixes. Also, formu­ las of the form EeX¢, Ee[4>U,P), Ee[...,(¢U,P)), and ¢C,P can be reduced to model checking of primitive proposi­ tions, formulas of the form EeX true and Ee G( ,P) lRao and Georgeff, 1993].

The details of the algorithm ACMCP are given else­ where [Rao and Georgeff, 1993]. Its complexity is given below.

Theorem 2 Solving the model checking problem for committed branching temporal BDI logic, CCTLom will take 0(14>1 . IWI. IMI . lel 2 } time to run.

The extensions of CCTLom over FCTL are twofold: (i) the introduction of possible worlds extends the ex­ pressive power of CTL and results in a complex struc­ ture on which to perform model checking; and (ii) the commitment constraint is more complex involving modal operators and path quantifiers.

The language CTL~01 subsumes the language CTL *, which in turn subsumes the linear-time temporal lan­ guage LTL. Hence, the complexity of model checking for CTL~ 01 has to be the same or greater than that of the model checking for LTL. It has been shown [Lichtenstein and Pnueli, 1985] that the complexity of model checking in LTL is linear in the size of the structure and exponen­ tial in the size of the given formula.

5 Example

Consider a robot, Mark I, that can perform two tasks, each involving two actions. For the first task, the robot can go to the refrigerator and take out ·a can of beer (denoted by gf) and bring it to the living room (bb) . For the second task, the robot can go to the main door of the house (gd) and open the door ( od). The only uncertainty in the environment is the presence or absence of a beer can in the refrigerator. For simplicity, we assume that the act of going to the refrigerator also involves opening the door and checking for the can of beer. If there is no can in the refrigerator, the act gf is said to have failed and the next act of bringing beer cannot be performed. We assume that all other acts succeed when executed.

Given appropriate specifications of such a robot and its environment and some commitment constraint, as de­ signers of these robots we will need to guarantee that they satisfy certain properties. For example, we may need to guarantee that (a) when the robot has a desire to serve beer it will inevitably eventually serve beer; or (b) when the robot has a desire to serve beer and a de­ sire to answer the door, and there is beer in the fridge, it will inevitably eventually realize both desires, rather than shifting from one task to the other without com­ pleting either of them. 3

3 This could happen if the tasks of going to the refrigerator

We consider two model structures M1 and M2 . First, we start by specifying directly the external model struc­ ture M1 . Generation of the external model structure from the agent and environment specifications is beyond the scope of this paper. A partial description of the structure M1 is shown in Figure 1. World vl depicts the alternatives available to the robot when it can choose to perform both the tasks and the environment is such that there is a beer can in the refrigerator. The dotted lines refer to additional future paths, which can be described in an analogous manner. One can view worlds v2 and v3 as world vl after the agent has executed the act of ei­ ther going to the refrigerator or going towards the door , respectively. Similarly, v4 and v5 are evolutions of v2; v6 and v7 are evolutions of v3.

We introduce two propositions:

beer-in-refrigerator and served-beer. The propo­ sition beer-in-refrigerator is true at all times in the worlds v1-v7. The proposition served-beer will be true in worlds v1-v7 after the act of bringing the beer (bb).

Next we examine the belief, desire, and intention re­ lations of the agent. The world vl of Figure 1 shows the various time points. The belief relations for world vl at various time points are given as follows: (vl, tl, vl), (vl, t2, v2), (vl, t3, v3), (vl, t4, v4), (vl, t5, v5) , (vl, t6, v6), (vl, t7, v7), ... E B. Desire and intention relations can be defined similarly. Further, we assume that the belief relations do not change when actions are performed. In other words, we also have (v2, t2, v2) , (v2, t4, v4), (v2, t5, vs), ... E B. Similar relationships hold for worlds v3-v7. This completes our description of the structure M1.

Consider a starting state in which the robot believes that there is beer in the refrigerator and has the intention to inevitably eventually have served beer. 4

We consider two instances of the commitment con­ straint; the first instance is a blind commitment towards an intention to have served beer sometime in the future and the other is a single-minded commitment towards the same intention. More formally, we have:

Using Definition 4 and algorithm ACMCP we can show that in all paths where the robot is blindly or single-mindedly committed to its intention, it will achieve its desire of serving beer . More formally,

and going to the door involve taking multiple steps; the agent could then take one step towards the door, change its mind, take the next step towards the refrigerator, again change its mind and keep alternating between these tasks forever.

4 We assume that the agent has the desire to have in­ evitably eventually served beer and to have inevitably even­ tually opened the door. In this example, we consider the case where the agent has only adopted an intention to serve beer; in the full paper [Rao and Georgeff, 1993], we consider the intention to open the door as well.

Next, consider two robots, Mark I and Mark II, and the situation in which there is no beer in the refrigerator. 5 Intuitively, Mark I does not change its belief about there being beer in the refrigerator at some time point in the future, even if it notices at this time point that there is no beer in the refrigerator. On the other hand, Mark II changes its belief about the beer being in the refrigerator as soon as it notices that there 1s none.

Now consider the structure M2 which consists of worlds w1-w7 shown in Figure 1 and additional worlds where the proposition beer-in-rdrigerator is false at all time points. Transitions between these worlds are similar to worlds w1-w7 except that the act gf fails (as there is no beer can in the refrigerator) and is followed by the act of going to the main door, namely gd, rather than the act of bringing the beer, namely bb.

With the structure M2 we can show that a single­ mindedly committed Mark II agent will drop its com­ mitment to maintain the intention of inevitably eventu­ ally serving beer. On the other hand, a single-mindedly committed Mark I agent will maintain this commitment forever. More formally, we can show the following:

In summary, we have considered two different model structures, one where the robot completes its task, the second where it is impossible for the robot to complete its task, but yet one of the robots maintains its commitment to this task forever, while the other robot reconciles itself to the impossibility of completing the task and gives it up. The purpose of this exercise has been to show how global properties of agent-oriented systems can be veri­ fied under a variety of rational behaviours obtained by varying the model structure and the commitment con­ straint.

5 Although we have not described a multi-agent CTLaoi logic, the modifications required to do so are straightforward. Also, as long as we do not introduce common knowledge op­ erators, the complexity of model checking in such multi-agent modal logics will be of the same order as single-agent modal logics [Halpern and Moses, 1992].

6 Comparisons and Conclusions

Cohen and Levesque [1990] describe agents by adopting a possible worlds structure in which each world is a linear­ time temporal structure and consider fanatical and rel­ ativized forms of commitment. A fanatical commitment is similar to our definition of a single-minded agent com­ mitted to its intention, i.e., {INTEND{AF4>))C(BEL(4>) V BEL{AG...,q, )) . A relativized commitment is one in which the agent has a persistent intention towards a proposi­ tion until it believes in the proposition or until some other proposition is believed. This can be expressed as {INTEND(AF4>))C(BEL(4>) V BEL(AG...,q,) V BEL{t/1)). Cohen and Levesque do not address the issue of model checking in their logic. However, as their logic subsumes linear-time temporal logic (LTL), the process of model checking in their logic will be at least as hard as the model checking for LTL; namely, linear in the size of the structure and exponential in the size of the given formula [Lichtenstein and Pnueli, 1985] .

Singh [1991] presents a branching-time intention logic based on CTL · . Various rationality postulates relating to beliefs, intentions, and actions are analyzed. Also, like Cohen and Levesque, Singh uses his logic only as a specification to characterize different behaviours and does not provide any guidelines for the design or verifi­ cation of such rational agents. Shoham's work [Shoham, 1991] spans both theory and language design, but does not address the issue of verification either.

This paper goes beyond this earlier work and provides a methodology for formally verifying properties of agent­ oriented systems. Starting from a reasonably rich model structure, we have described three propositional logics and analyzed their relative expressive power. Further­ more, the linear time and polynomial time complexity of model checking in two of these logics makes them potentially useful for verifying practical agent-oriented systems.

Our work draws its inspiration from the field of con­ currency theory [Emerson, 1990], especially that field's contribution to the techniques of model checking. We have extended the results of Emerson and Lei [1987] by showing that the linear time and polynomial time com­ plexities of model checking hold for logics more expres­ sive than CTL and Fair CTL logics. Also, the complex­ ities are not greatly affected by the number of different modalities - the complexity seems to be dependent on the underlying temporal structure. More importantly, this paper demonstrates the generality of the model­ checking technique [Halpern and Vardi, 1991] and ex­ tends it to a new domain; namely, the verification of agent-oriented systems. The close correspondence be­ tween fairness and commitment, and concurrency theory and rational agency, lays a strong theoretical foundation for the design and verification of agent-oriented systems.

However, a number of open problems with respect to this approach remain. First, we need to address the pro­ cess of model generation whereby, given an agent speci­ fication and/or environment specification, the appropri­ ate model structure is automatically generated. Second, we have used model checking as a means of verifying global properties, i.e., from an external observer view­ point. Similar techniques can be used by the agent in­ ternally. In this case, we may want to build the model in­ crementally, rather than assuming that the entire model structure is given to us. Third, the size of the structures we are dealing with is likely to be large and techniques to reduce this would be valuable.

Although a number of issues in the model-theoretic design and verification of agent-oriented systems are yet to be resolved, our work indicates, for the first time, that the expressive multi-modal, branching-time logics can possibly be used in practice to verify the properties of these systems.

Acknowledgements

This research was supported by the Cooperative Re­ search Centre for Intelligent Decision Systems under the Australian Government's Cooperative Research Centres Program.