A Logic for Acting, Sensing and Planning

1 Introduction

The idea of using logic for reasoning about actions and plans has been extensively studied in the past. So far, most of this research has mainly focused on two issues. The first is the problem of providing an adequate ax­ iomatization of actions that a system can perform in the external environment. The second is the problem of providing a powerful and efficient deductive planning mechanism able to generate plans automatically. The idea underlying most of this research is that a logic can be used to predict action executability and effects, and therefore to generate "good" plans, i.e. plans that when executed are likely to achieve the desired goals.

Our research is related but different in focus . Our work starts from an analysis of planning systems that work in real world applications. Most of these systems, beyond plan generation, need to perform many different activities. For instance, they have to monitor executions, react to environmental changes, interleave planning, ex­ ecution and perception, recover from failures, e.g. by replanning or by executing exception handling routines. In order to perform these activities, they need three ba­ sic capabilities: acting, sensing and planning. Acting capabilities are usually provided by a repertoire of ac­ tuators which perform actions in the external environ­ ment (e.g. wheels, gripper fingers and hands). Sens­ ing capabilities are usually provided by a set of sensory devices which acquire information from the real world (e.g. sonars, odometers, cameras, microphones) . Plan-

Luca Spalazzi

Istituto di Informatica University of Ancona Via Breece Bianche, 60131 Ancona Italy

ning capabilities are usually provided by planning mod­ ules which generate plans to achieve given goals (e.g. modules for plan search, interactive systems for plan reuse) and execute plans. A planning system has to activate, coordinate and control all these devices and modules. Several systems which control acting, sensing and planning have been proposed so far (see for instance [Beetz and McDermott, 1994; Georgeff and Lansky, 1986; Simmons, 1990]) and have been successfully applied in particular application domains (like mobile robots and fault diagnosis for real time systems). In spite of this fact, no principled and theoretical account has been given of the behaviours of these systems.

The goal of this paper is to provide a logic which al­ lows us to represent and reason about acting, sensing and planning. The motivation is twofold. First , the logic can be used to provide a specification of real systems which allows us to understand their requirements. Second, the logic can be used as a basic formal framework for build­ ing reasoning modules within real world applications . It can in fact be used to plan to act, plan to sense and plan to plan, and therefore to decide how to interleave acting, sensing and planning. We see this work as a first step towards a formal account of systems which are able to integrate reasoning, perception and action.

In order to achieve this goal, the logic we propose has some novel features. First, it is based upon an extended notion of action. The logic represents explicitly sensing actions, i.e. actions that acquire information and mod­ ify the state of knowledge of the agent, and planning actions, i.e. actions that generate and execute plans of actions. As a consequence, not only can the logic rea­ son about the effects of actions in the real world, but also about the fact that a sensor has (not) been used to update the knowledge of the system about the world and the fact that the system has (not) a proper plan at hand which can be executed to try to achieve a given goal. Second, in real systems, no action, even if appar­ ently simple, is guaranteed to succeed. This is mainly due to the intrinsic complexity of reality, to the fact that the external environment is usually incompletely known and unpredictable, and to the fact that actua­ tors, sensors and models of the world are not perfect. As a consequence, neither acting, nor sensing, nor plan­ ning is guaranteed to succeed. The logic we propose has in its language the basic operations for failure handling and can therefore reason about failure detection and re­ covery in acting, sensing and planning.

The paper is structured as follows. We describe the language of the logic in section 2 and its semantics in sectiob 3. We give some axioms and theorems of the logic in section 4. We discuss some related work in section 5.

2 Language

The logic is a variation of process lo_gic [Harel et al., 1982], an extension of dynamic logic lHarel, 1984]. In section 2.1 we describe a language for action. In sections 2.2 and 2.3 we extend the language to represent sensing and planning actions, respectively.

2.1 Acting

The syntax of the logic is based upon two sets of symbols: Po, the set of atomic (or basic) propositions and To, the set of atomic (or basic) tactics. From Po and To we inductively construct the set P of propositions and the set T of tactics. P and T are the smallest sets such that:

1. Po~ P; True E P;

2. If p, q E P, then -.p, p 1\ q E P.

3. WEP;

4. If p, q E P then p chop q E P.

5. To~T; E,«l>ET;

6. If a, {3, r E 7, then iffail a then {3 else r E 7.

7. If pEP, a E 7, then [a]p E P.

8. If a E 7, then Fail( a), Succ(a) E P.

We use V, - and ,...... as abbreviations in the standard way and, in addition, we abbreviate -.[a]-.p to (a)p as in dynamic logic 1 ·

Propositions are either true or false in behaviours (we say that they are behaviour propositions), where, intu­ itively, a behaviour is a finite sequence of states of the world. For example, if w1, w2, wa, w4 and w5 are states, then w1 w2 wa w4 w5 is a behaviour. A single state is a particular case of behaviour. W is the proposition which holds over any behaviour which consists of a sin­ gle state. The operator chop is applied to propositions p and q to yield a new proposition p chop q. chop is used to reason about concatenations of behaviours, where, for example, the concatenation of w1 w2 wa and wa W4 ws is w1 w2 wa w4 ws. p chop q holds in a behaviour b iff there exist two behaviours b1 and b2 such that the con­ catenation of b1 and b2 is b, p holds in b1 and q holds in b2. We extend the language with the operator last which is applied to a proposition p to yield a new proposition last(p ).

last(p) holds in a behaviour b iff p holds in the final state of b.

Tactics represent actions. For instance, goto(A) can be a basic (even if very complex) action which moves a robot to a position A, e.g. by means of an in-door navi­ gation system 2 · E and «<>represent the primitive actions that generate success and failure, respectively. E (ell) does nothing but terminate execution with success (fail­ ure). The intended meaning of iffail a then {3 else 'Y is: "do a, if a fails do {3, otherwise do 'Y". The intended meaning of [a]p is "every possible execution of a leads to a behaviour in which p holds". Fail( a) and Succ(a) hold iff a fails and succeeds, respectively. For any a E T, we extend the language with the proposition Ex( a), de­ fined as follows:

1 Actually, the language allows for tactics that include con­ ditional expressions of the form if p then a else (3 and loops of the form while p do a. For lack of space, in this paper we do not describe the full syntax. The language, as well as its semantics, can be easily extended.

A proposition p can be seen ,as a goal to be achieved. Notice that success/failure of a tactic does not coincide necessarily with the achievement/not-achievement of a related goal. The former is a property of tactics, the latter is a relation between tactics and goals. A tactic may fail and, nevertheless, achieve the goal the tactic has been executed for. Vice versa, a tactic may succeed and may not achieve the goal. For example, let put-on( a, b) be a tactic that moves the block a on the block b. If a is on the block c, put-on( a, b) may fail, e.g. by moving a on the table, and nevertheless achieve the goal Clear( c). If c is near b, put-on( a, b) may succeed and not achieve the goal Far-from( a, c).

Constructs for failure handling are definable using E, «<> and iffail. For instance, we extend the language with the following definitions.

a; {3 = iffail a then {3 else {3,

then( a, {3) = iffail a then«<> else {3,

orelse(a, {3) = iffail a then {3 else E,

repeat( a)= orelse(then(a, repeat( a)), E)

We define the usual construct ; for sequences of actions. In a; {3 the second action is executed anyway, indepen­ dently of the failure/success of the first action. Notice that ; is a primitive construct in most of the logics pro­ posed so far, e.g. in dynamic logic [Harel, 1984], in pro­ cess logic [Harel et al., 1982], in (extended versions oi) situation calculus [Lesperance et al., 1994] and in all the­ ories of actions, e.g. in [Lifschitz, 1993]. This is due to the fact that ; constructs sequences without handling failure and these logics do not take into account failure. A sequential composition which takes into account fail­ ure is then. If the first action fails, then does not execute the second, but simply terminates execution with failure. then captures the behaviour of sequential executions in real systems where, if the first action fails, the second is not executed and control is passed to a module for fail­ ure recovery. orelse is the construct for failure recovery. orelse( a, /3) reacts to failure of a by executing {3. repeat controls failure over the repeated execution of a tactic. It is recursively defined. It repeats the execution of a till a fails. If a never fails, execution does not terminate. Notice that if it terminates, repeat( a) always succeeds, since orelse in the definition of repeat reacts to failure by executing E, which always succeeds.

2 More precisely, basic tactics are constructed from a set of terms, e.g. A, and a set of tactic symbols, that, intuitively represent action types, e.g. goto. For lack of space we skip the formal definition of the syntax of basic tactics.

2.2 Sensing

We extend the language with a set C of symbols that we call sensors. For any sensor, we add a tactic and a proposition to the set of basic tactics and propositions.

If c E C, then sense( c) E To.

If c E C, then Sensed( c) E Po .

Intuitively, sensors denote values which can be acquired through sensory devices. For instance, wall-distance can be the sensor which gets the value of the distance of the robot from the wall. We call sense(c) a sensing action (for c). Its intended meaning is "acquire the value of tl~e sensor c". For example, sense( wall-distance) can activate a sonar and/or a camera to acquire the value of wall-distance .

Sensing actions formalize activities that real systems have to perform extensively. Indeed, while most theories of actions are based on the assumption that, after act­ ing is performed, the agent has at hand all the desired information about the new state of the world, this is not what happens in real systems. Most often, in real sys­ tems, the only way to get to know some facts about the state of affairs is to activate sensory devices and acquire information from the external environment, i.e. to exe­ cute sensing actions. Suppose for instance that a robot moves successfully to a given position A. At this point, the world around the robot has changed: its position has changed, as well as the distance from the wall, the distance from the nearest window, and so on. It is not realistic that the robot gets to know all these facts au­ tomatically after execution. For instance, after acting, knowledge about its position might be updated auto­ matically, but it may have instead to measure (e.g. by a sonar or a camera) the distances from the wall, objects and landmarks to get to know their new values. Real systems have therefore to execute sensing actions explic­ itly. For instance, suppose that goto(A) is a tactic which does not update the value of the sensor wall-distance. A possible tactic which moves the robot to A and then acquires the value of the distance from the wall is the following.

A sensing action may fail. For instance,

sense( wall-distance) may fail since the sonar may not work or the camera may fail to detect the wall. In exam­ ple (1), if sensing fails then the value of wall-distance is not updated.

Successful sensing actions update the state of knowl­ edge of the agent since, at the end of their execution, the value of the sensor is acquired. This knowledge is expressed by the proposition Sensed(c), which holds in any behaviour which is the final state of a successful sens­ ing action for c. The idea here is that Sensed( c) holds if we have just executed a successful sensing action for c and therefore the value of c is "up to date". For instance, consider the following propositions.

Proposition (2) states that goto(A) does not update au­ tomatically the distance from the wall, i.e. after e~ecut­ ing goto(A) either with success or failure (Ex(goto(A))), then we get to a final state where wall-distance is not up to date (-.last(Sensed(wall-distance))). Proposition (3) is the analogous statement for the tactic goto(B). The value of the sensor is up to date if the sensing action succeeds (proposition ( 4)) . If we execute goto(B) after sensing, then the value is not up to date (proposition (5)). Indeed, the last action might change the actual distance from the wall. Notice that the fact that the truth value of Sensed(c) changes does not depend on the fact that the value of c changes or not. For instance, propositions (2)-(5) may hold even if wall-distance is constantly the same before and after the executions of goto(A), goto(B) and sense(wall-distance).

2.3 Planning

We add to the language a set II of symbols, that we call names of tactics, which is based upon an initial set of symbols II0 , and we extend the set of basic tactics and propositions as follows.

ITo ~II.

If 1r E IIo and pEP, then planfor(7r,p) E To.

If 1r E II, then exec( 1r) E To;

If 1r E IIo and p E P, then Planned( 1r, p) E Po.

If a E T, then "a" E II .

We call "a" the name of the tactic a. Names of tac­ tics denote tactics. For example, the name of goto(A) denotes the syntactic expression goto(A) . The idea here is that planning generates a syntactic expression denot­ ing a plan which can thereafter be executed. We call planfor(1r,p) a plan generation action {of 1r for p). Its intended meaning is: "generate a plan denoted by 7r to achieve the goal p". For example, if Robot-at-A is a proposition whose intended meaning is "the robot is in position A", then planfor(7r, Robot-at-A) can be a tac­ tic that generates the name 1r which denotes the sim­ ple plan goto(A) . We call exec(1r) a (plan) execution action {of 7r ) . Its intended meaning is: "execute the plan denoted by 1r". For example, the intended mean­ ing of exec( "goto(A)") is: "execute the plan denoted by "goto(A)"". We call plan generation and execution ac­ tions, planning actions. As an example of combination of planning actions, consider the following tactic which generates a plan and then executes it.

Since plan execution actions may perform actions in the real world, they may fail. Failure in plan execution can be handled in different ways. Most classical plan­ ners (e.g. [Wilkins, 1985)) handle failure by replanning, i.e. by searching for a new plan. Reactive planners (e.g.

[Georgeff and Lansky, 1986; Simmons, 1990]) sometimes have no time for replanning, and therefore handle fail­ ure by executing precompiled special purpose exception handling routines. Our logic is expressive enough to rep­ resent these different failure handling mechanisms. For instance, tactic (7) reacts to failure of exec( 7r1) by re­ planning (planfor( 7r1, p) ), while tactic (8) reacts to fail­ ure by executing the plan denoted by 7r2 , which can be a precompiled exception handling routine.

In most classical planners, plan generation searches for a plan by using an internal model and does not operate in the real world. This is not what happens in most of the reactive planners (e.g. in [Georgeff and Lansky, 1986; Beetz and McDermott, 1994)) where, sometimes, tpe only way to decide for a plan is to do something in t~e world. For instance, a mobile robot which has to look for something in a building and does not know the map may have to "turn around the corner and open a door" in order to decide what to do next. In order to capture this extended notion of plan generation, planfor has to be thought simply as a tactic which constructs a plan, with no constraints on whether it operates in the real world or not. As a consequence, in our view, plan generation may fail in the same way as acting, sensing and plan execution may fail. The constructs for failure handling defined in section 2.1 can be used to handle failure in plan generation. For instance, in example (6), if plan for fails, then captures failure and does not execute 7r1·

Successful plan generation actions update the state of knowledge of the agent since they produce a plan that is available for execution. This knowledge is ex­ pressed by the proposition Planned(7r,p), which holds in any behaviour which is the final state of a success­ ful plan generation action of 7r for p. The idea here is that Planned(7r,p) holds ifwe have just executed a plan generation action of 7r for p and therefore the plan at hand, i.e. the plan denoted by 'IT, is "the proper plan for that situation". For instance, consider the following propositions.

Proposition (9) states that moving the robot to A makes the plan denoted by 7r1 obsolete. Proposition (10) states that success in planning leads to a final state where the plan at hand is "the proper plan for that situation". Proposition (11) states that after planning and executing goto( A), the plan denoted by 7r1 may be obsolete (even if still available for execution). Indeed, acting in the world may change the world and invalidate old plans. Proposition (12) states that after plan generation, plan execution, and finally plan generation again, the plan at hand is "the plan for that situation".

Two remarks are in order. First, having at hand "the plan for that situation" does not mean that the execution of the plan will actually achieve the goal. This is not re­ alistic in presence of uncertainty. The knowledge of the agent is relative to its (possibly incomplete or wrong) model of the world. Only the execution of the plan will determine whether the plan has achieved the goal or not. Second, the second occurrence of planfor(7r1,p) in (12) might or might not generate a new tactic dif­ ferent from the one generated by the first occurrence of plan for( 7r1, p ), i.e. the tactic denoted by 7r1 might or might not change. This depends on how planfor be­ haves and, for instance, on whether the execution of 1r1 changes the world in a way that influences the second plan generation action.

3 Semantics

The semantics of the language is defined relative to a given structure U, of the form

where V is the domain of interpretation, W is an ab­ stract set of states and I is the interpretation func­ tion. V = 1J0 U Tu. V 0 is used to interpret sen­ sors and Tu is used to interpret names of tactics. The set of behaviours B is the set of all finite-length se­ quences of states, repetitions allowed, i.e. B = w+. Be­ haviour concatenation is defined as follows: if w; E W, i= 1, ... ,j-1,j,j+1, ... n, b1,b2 E B, b1 = w1 ···wj, b2 = Wj ... Wn, then b1·b2 = W1 ... Wj-1 Wj Wj+l· .. Wn. Concatenation is extended over sets of behaviours in the usual way.

I assigns interpretations to sensors and names de­ pending on behaviours. For any b E B, we write Cb and 7rb the interpretation of c E C and 7r E II in the behaviour b, respectively. For any c E C, Cb E V 0 , i.e. in any behaviour, a sensor denotes an element of V 0 , that we call the value of the sensor. For any 7r E II, 7Tb E Tu, i.e. a name of a tactic denotes an element of Tu, where Tu is the set of tactics in U. Notice that we have the set of tactics T in the language and the set of tactics Tu in the structure U. T and Tu contain exactly the same elements. We need Tu in order to interpret names of tactics. For any behaviour b, "a" b = a.

I assigns subsets of B to propositions and tactics. We write p(p) and n( a) the sets of behaviours assigned by I to p E P and a E 7. We write b f= p iff b E p(p) . n( a) is divided into two subsets:

S( a) is the set of successful behaviours, that we call the success set of a, and :F( a) is the set of behaviours that fail, that we call the failure set of a. I assigns an arbitrary subset of B to each basic proposition p and arbitrary disjoint success and failure sets to basic tactics, I.e.

We have the following condition over n( a) of basic tac­ tics:

This condition states that we cannot have a behaviour of an action whose final state is the same as the inter­ mediate state of a behaviour of the same action. This corresponds to the fact that the agent, in a given state of its computation machinery, always stops or always con­ tinues execution. Conditions (14) and (15) allow us to prove that success and failure sets are mutually exclus1ve:

and that condition (15) holds for any tactic.

I is extended inductively to supply meanings for the full sets P and T.

Some remarks. W is interpreted into W. Notice that W is the identity w.r.t. concatenation, i.e. if B is any set of behaviours, then B · W = W · B =B. The failure set of E is empty. This corresponds to the fact that it always succeeds. Its success set is W. This corresponds to the fact that E does nothing else but succeeding. Vice versa, the success set of~ is empty while its failure set is W.

The constructs ;, then, orelse and repeat inherit their meanings from their definitions in terms of E, ~ and iffail. For lack of space we do not describe the semantics of repeat, which is recursively defined and interpreted by building a fix point. We give below the success and failure sets for ;, then and orelse.

Notice that, in case both o: and f3 succeed, then( a:, {3) behaves like o:; {3. In case of failure of the first ac­ tion, the failure set of then( o:, /3) is the failure set of the first action, i.e. F(o:). This captures the idea that when the first action fails, the second is not executed. Analogously, notice that when the first action succeeds, S( orelse( o:, /3) is the success set of o:, i.e. S( o:), since no recovery from failure is needed. When o: fails, f3 is executed and orelse(o:, {3)' might either fail or succeed, depending on the failure/success of {3.

In the following, we give interpretation to Sensed(c) and Planned(1r,p).

Sensed(c) holds in all and only the states which are final states of successful behaviours of sense( c). Planned(1r,p) holds in all and only the states which are final states of successful behaviours ofplanfor(7r,p).

Notice that, in order to keep the semantics general, we have not given any condition on the interpretations of sensing and planning actions. They are basic tactics, and as such they are assigned arbitrary disjoint success and failure sets. Their semantics depends on the partic­ ular sensing, planning and execution mechanisms which are available to the system. Nevertheless, there are con­ ditions on planning that seem reasonable. We give some of these conditions below.

Condition I states that execution, given a name denot­ ing a tactic, does nothing but executing the tactic it­ self. Condition II states that there must exist at least one behaviour b' in the execution of a tactic denoted by 1r (i.e. 7rb) and generated by the planning action planfor(7r,p), such that behaviours in the successful set of plan for( 1r, p) concatenated with b' achieve the goal p we have planned for (i.e. b · b' f= p). This condition al­ lows only for plan generations that produce a plan that, when executed, has at least a possibility of achieving the desired goal.

4 Some theorems

Given the language and its semantics, the goal is to pro­ vide a deductive system which is complete and correct. In the following, we give some axiom schemas which we have proved correct w. r. t. the given semantics and which allow us to prove some interesting theorems about act­ ing, sensing and planning. We start with axioms inher­ ited from dynamic and process logic:

Some basic properties of W and chop:

Some axioms to reason about failure and success:

(A5) W-> [o:]Ex(o:). (A6) --.(Succ(o:) 1\ Fail( a:)). (A7) Ex(o:)-> --.(Ex(o:) chop --.W) (A8) (--.Fai/(E)) 1\ (Succ(E) +-+ W) (A9) (--.Succ(~)) 1\ (Fail(~)+-+ W) (A10) ([E)p +-+ p) 1\ ([~]p ..... p) (All) Succ(iffail o: then f3 else 'Y) +-+ ((Fail(o:) chop Succ(f3)) V ( Succ( o:) chop Succ( 'Y)))

(A5) states that, if we are in the initial state of a be­ haviour of a, then the execution of a either leads to success or failure. (A6) states that success and failure are mutually exclusive. It corresponds to the condition S(a) n F(a) = 0. (A7) states condition (15) for any tactic. Indeed, for any p E P, for any b = w1 .. . Wn, b I= p chop ·W iff w1 ... Wk I= p with 1 ~ k ~ n- 1. (A 7) states therefore that, if wl ... Wn E n( a) then Wl .. · Wk ¢ n(a), with 1 ~ k ~ n- 1. (AS) and (A9) state that E (<I>) never fails (succeeds) and that the suc­ cess (failure) set of E (<I>) is W. (A10) states that E and <I> do not change the world, i.e. the set of proper­ ties which hold before the execution of E and <I> also hold after their execution and vice versa. (All) and (A12) de­ scribe the success and failure set of iffail. (A13) states that p holds after iffail a then f3 else 1 iff it holds after a and f3 if a fails, and after a and 1 if a succeeds.

The following axioms describe sensing and planning.

• (A14) Succ(sense(c)) +-+ (Succ(sense(c)) chop Sensed(c))
• (A15) Succ(planfor( 1r, p)) +--+ (Succ(planfor( 1r, p)) chop Planned( 1r, p))

(A14) and (A15) state that sensing and planning with success end up in a final state where Sensed(c) and Planned(1r,p) hold, respectively.

Conditions I and II (section 3) are stated as follows.

• (A17) Succ(planjor(1r,p))--+ (exec(1r))p

(A16) states that the effects of exec("a") are the same as the effects of a. (A17) states that plan generation gener­ ates a plan that has at least one possibility of achieving the desired goal.

From (A1)- (A13), we can prove the following theo­ rems which can be used to reason about success and failure of the constructs ;, then and orelse.

• (T1) Succ(a;f3) +-+ ((Fail(a) chop Succ(f3)) V ( Succ( a) chop Succ(,B)))
• (T2) Fail(a;f3) +-+ ((Fail(a) chop Fai/({3)) V (Succ(a) chop Fai/({3)))
• (T3) Succ(then(a, {3)) +--+ ( Succ( a) chop Succ(,B))
• (T4) Fail(then(a, {3)) +-+ (Fail(a) V (Succ(a) chop Fail(,B)))
• (T5) Succ(orelse(a , {3)) +--+ (Succ(a) V (Fail(a) chop Succ(f3)))
• (T6) Fail(orelse(a,f3)) +-+ (Fail(a) chop Fai/({3))

From (A1)-(A14), we prove the following theorems.

• (T7) Succ(sense(c)) -+last(Sensed(c))

Moreover, from (T8) we can prove (4) and, given (3) as an axiom, we can prove {5) from (T1) and (T2) . From (A1)-(A13) and (A15), we prove the following theorems.

which can be used to prove propositions (10) and (12). (9), (T1) and (T2) can be used to prove proposition (11).

5 Related work

This paper is an elaboration and extension of the intu­ itions originally presented in [Giunchiglia et al., 1994).

Compared to the previous research in theories of ac­ tions, the work described in this paper is limited in at least three respects. First, we do not allow for variables and quantifiers in our logic. Second, we do not deal with asynchronous and parallel events and actions. Third, we do not discuss how our logic deals with the frame problem. Major future goals include these issues. How­ ever, these issues, though very important, are somehow orthogonal to the main message of this paper, which is about describing a theory of acting, sensing, and plan­ ning, i.e. a theory which integrates in a uniform frame­ work important basic features of planning systems for real world applications. As far as we know, the approach presented in this paper has never been proposed before.

The closest work on failure is that described in [Rao and Georgeff, 1991]. [Rao and Georgeff, 1991] presents a formal framework for BDI-architectures and commit­ ment (we do not deal with these issues in this paper) which represents explicitly failure and success of events. succeeds(e), fails(e), succeeded(e) and failed(e) are state formulas (of a propositional branching time logic) which express immediate future and past performance, respectively successfully and unsuccessfully, of event e. Semantically, arc functions Sw and Fw map adjacent time points to the event that occurred with success or with failure. Technically, our approach is different since Succ(a) and Fail(a) are behaviour propositions. This captures the fact that the execution of an action may re­ sult in different sequences of states, and the fact that its failure and success may depend on the whole sequence and not only on a single state. The main conceptual dif­ ference is in the focus and objectives of the two works. We are interested in a framework for failure handling, i.e. in how actions can be composed through constructs which capture and react to failure, since we see flexible failure recovery as one of the major activities that real planning systems have to perform. For this reason we have a; logic which combines actions through <I>, E, iffail, f' then, orelse and repeat. While the theory proposed in LRao and Georgeff, 1991] does not deal with action com­ position, and more important, with constructs for failure handling. Moreover, our logic allows us to express and reason about sensing and planning actions, while [Rao and Georgeff, 1991] does not.

In [Lesperance et al., 1994], situation calculus is ex­ tended with complex actions, e.g. sequences, condition­ als and loops, and with "perception actions" , or "knowl­ edge producing actions", ofthe form SENSEp and READr, where P and T are a fluent and a term, respectively. Knowledge about perception is expressed by means of wffs of the form Knows(P,s) and Kref(r,s), where sis a situation. Technically, our approach is different since we have no situations in the logic. Moreover, in this pa­ per we have described a class of sensing actions which is less expressive than the class of perception actions de­ fined in [Lesperance et al., 1994]. However, the given language, semantics and axiomatization can be easily extended to include sensing actions about propositions and terms. Conceptually, our work differs mainly in two aspects. First, our logic captures the fact that percep­ tion is a complex task that, when it has to be performed by real systems, is not guaranteed to succeed. Actions of the form sense( c) may actually fail to acquire infor­ mation and therefore fail to produce knowledge. As a consequence, in our logic we do not have theorems anal­ ogous to I(ref(r, do(READT, s)) , which can be read as "after doing READT the agent knows the denotation of r", but we can prove theorem (T7), i.e. "if sensing suc­ ceeds, then the agent has sensed c". Second, our logic allows us to express and reason about planning actions, while [Lesperance et al. , 1994] does not .

The closest work on planning actions is that described in [Steel, 1994b] (see also [Steel, 1994a]), where dynamic and epistemic logic are used to express formulas of the form "plan to do an action that achieves a goal , then do it". The main differences with our work are the fol­ lowing. First, in [Steel, 1994b] plan generation is seen as "specialization" of "non operational" actions, i.e. ac­ tions which cannot be executed. We see instead plan generation as an executable action which constructs a plan. This corresponds to the fact that systems have planning modules which can be activated to generate plans. Second, in [Steel, 1994b], planning is seen as an action which does not affect the external environment while we do not rely on this assumption since many re­ active planners have to generate plans by acting in the world. Finally, our logic deals explicitly with failure han­ dling in plan generations and executions.

The logic we have proposed· is based on work on MRG [Giunchiglia et al., 1991; Traverso et al. , 1992], a reactive planning system which executes tactics. At the moment, MRG is used in a large scale, real world application under development at IRST. This application aims at the de­ velopment of a system that has to control and coordinate mobile robots, navigating in unpredictable environments inhabited by humans and performing high level tasks, like transportation tasks in hospitals and offices. MRG tactics are executed by means of systems that perform sensing and acting, e.g. a reactive sensor and actuator controller for navigation tasks and a system for speech recognition, and by means of systems that generate and execute plans, e.g. path planners and activity sched­ ulers. We plan to use the formal framework to extend the functionalities of MRG and t.o specify the requirements of the application under development .

Acknowledgments

We thank Fausto Giunchiglia for his invaluable support, and for all his many conceptual and technical comments on early drafts of this paper. They have contributed to improve the paper significantly. We also thank Luciano Serafini for fruitful discussions.