Projection Using Regression and Sensors

1 Introduction

One of the most fundamental tasks concerned with reasoning about action and change is the projection task: determining whether a fluent 1 does or does not hold after performing a se­ quence of actions. In the usual formulation, we are given a characterization of the initial state of the world and a specifi­ cation of some sort of what each action does. The projection task requires us to determine the cumulative effects (and non­ effects) of sequences of actions.

Projection is clearly a prerequisite to planning: we cannot figure out if a given goal is achieved by a sequence of actions if we cannot determine what holds after doing the sequence. Similarly, the high-level program execution task [6], which is that of finding a sequence of actions constituting a legal execution of a high-level program, also requires projection: to execute a program like "while there is a block on the table, pick up a block and put it away," one needs to be able to determine after various sequences of actions if there is still a block on the table.

A perennial stumbling block in the specification of the pro­ jection task 'is the frame problem [ 4]: for each action, we need to specify somehow not only what changes as the result of performing the action, but the much larger number of flu­ ents unaffected by the action. One solution to this difficulty is

1 By a fluent, we mean a property of the world that changes as the result of performing actions.

Hector J, Levesque

Department of Computer Science

University of Toronto

Toronto, ON, Canada M5S 3H5

hector@cs.toronto.edu

make a STRIPS assumption [2]: what will be known about a state of the world will be representable as a database of sim­ ple atomic facts, and we specify actions as operators on such a database, adding or removing just what changes.

A much more expressive and declarative solution to the frame problem is presented in [10]. There, the situation calcu­ lus is used to specify the effects of actions, and then a simple syntactic procedure is provided for combining the effects for each fluent into a so-called successor state axiom that logi­ cally entails not only the effect axioms, but all the frame ax­ ioms for that fluent as well.

However, this solution to the frame problem makes a strong completeness assumption: after specifying the (perhaps con­ ditional) effects of the given actions on fluents, and then al­ lowing for possible ramifications of these actions (e.g., [7]), it is then assumed that a fluent changes only if it has been af­ fected in one of these ways. Thus, it is assumed that each flu­ ent can be regressed in the sense that whether or not it holds after performing an action can be determined by considering the action in question and what was true just before.

What is not allowed, in other words, are cases where the value of a fluent does not depend in this way on the previous state. This can arise in at least two ways. First, a fluent might change as the result of an action that is exogenous to the sys­ tem, i.e., not represented in the action theory. If a robot ~ns a door in a building, then when nobody else is around, it is justified in concluding that the door remains open until the robot closes it. But in a building with other occupants, doors will be opened and closed unpredictably. Similarly, the robot may be able to determine that a warning light is on simply because it was on in the previous state and the robot is the only one who can tum it off; but it may not be able to predict when the warning light goes on. Secondly, the robot might have incomplete knowledge of the fluent in question. For ex­ ample, a robot normally would not be able to infer the current temperature outdoors, since this is the result of a large num­ ber of unknown events and properties. Even when a fluent is expected to stay relatively constant, like the depth of water in a swimming pool, the robot may not know what that value is.

In cases such as these, the only way we can expect a robot to be able to perform the projection task is if it has some other way of determining the current value of certain fluents in the world. To this effect, we assume that not only can the robot use regression, it can use a collection of onboard sensors. In [5], sensing is modeled as an action performed by a robot that returns a binary measurement. The robot then uses so-called sensed fluent axioms to correlate the value returned with the state of various fluents. However, in this account, no attempt is made to be precise about the exact relation between sens­ ing and regression. Moreover, there is no possibility of saying that only under certain conditions can regression be used, and in others, sensing. On the other hand, the knowledge or be­ lief of an agent is modeled explicitly in [5] as a fluent that can be changed by sensing actions, while for our purposes, knowledge will be left implicit.

What we propose in this paper is this: a formal spec­ ification of a changing world that generalizes Reiter's so­ lution to the frame problem (and hence STRIPS also) to allow conditional successor state axioms, and generalizes Levesque and others' treatment of sensors (e.g., [1; 3; 9; 12]) to allow conditional sensing axioms. Our specification will be sufficiently general that in some cases, there will sim­ ply not be enough information to perform the projection task even with sensing. However, in many cases, we will be able to do projection using a combination of sensing and regres­ sion. In addition to this specification, we propose a reason­ ing method for performing projection under these general cir­ cumstances which is guaranteed to be sound, and in many cases of interest, complete. We provide a Prolog evaluation procedure for the projection task and prove its soundness and under suitable circumstances its completeness.

2 Basic action theories

Our account of action, sensing, and change is formulated in the language of the situation calculus [4; 11]. We will not go over the language here except to note the following compo­ nents: there is a special constant So used to denote the ini­ tial situation, namely the one in which no actions have yet occurred; there is a distinguished binary function symbol do where do( a, s) denotes the successor situation to s resulting from performing action a; relations whose truth values vary from situation to situation, are called (relational) fluents, and are denoted by predicate symbols taking a situation term as their last argument; and there is a special predicate Poss( a, s) used to state that action a is executable in situations.

Within this language, we can formulate action theories that describe how the world changes as the result of the available actions. One such is a theory of the following form [ 1 0; 11]:

• Axioms describing the initial situation So, and axioms not mentioning situations at all, which form together the initial database.
• Action precondition axioms, one for each primitive ac­ tion a, characterizing Poss( a, s) .
• Successor state axioms, one for each fluent F, stating under what conditions F(x, do( a, s)) holds as function of what holds in situations. These take the place of the so-called effect axioms, but also provide a solution to the frame problem [10].
• Unique names axioms for the primitive actions.
• Some foundational, domain independent axioms.

For example, the successor state axiom 2

states that an object x is broken after doing action a if a is dropping it and x is fragile, a is exploding a bomb near it, or it was already broken, and a is not the action of repairing it.

In [5], to characterize the result of sensing, it is assumed that each primitive action can return a binary sensing result, and that there is a special predicate SF( a, s) used to state that action a returns value 1 in situations. To relate this sensing result to fluents, the following are added to basic action theo­ ries:

• Sensed fluent axioms, one for each primitive action a, characterizing SF.

For example, the sensed fluent axiom

states that reading the heat gauge returns 1 iff the temperature around the robot exceeds 25 degrees.

3 Guarded action theories

In what follows we will be replacing successor state and sensed fluent axioms by more general versions. To this effect, instead of assuming that actions return a binary sensing value, we assume that a robot has a number of onboard sensors that provide sensing readings at any time. Thus, we drop SF from the language of the situation calculus, and introduce instead a finite number of sensing functions: unary functions whose only argument is a situation. For example, thermometer(s), sonar( s), depthGauge( s), might all be real-valued sensing functions. 3

We then define a sensor-fluent formula to be a formula of the language (without Poss, for simplicity) that uses at most a single situation term, which is a variable, and that this term only appears as the final argument of a fluent or sensor func­ tion. We write <j>(x, s) when 4> is a sensor-fluent formula with free variables among the x and s, and ¢(f, t 8 ) for the formula that results after the substitution of x by the vector of terms t and s by the situation terrri t8 · A sensor formula is a sensor­ fluent formula that mentions no fluents, and a fluent formula is one that mentions no sensor functions.

We then define our generalized version of successor state and sensed fluent axioms as follows:

A guarded successor state axiom (GSSA) is a for­ mula of the form

and a guarded sensed fluent axiom (GSFA) is a for­ mula of the form

2 Here and below, formulas should be read as universally quanti­ fied from the outside.

3 Syntactically, these look like functional ftuents, so to avoid con­ fusion, we only deal with relational ftuents in this paper.

where a is a sensor-fluent formula called the guard of the axiom, F is a relational fluent, 1 is a fluent formula, and p is a sensor formula.

An action theory can contain any number of GSSAs and GS­ FAs for each fluent. We can handle a universally applicable successor state axiom like the one for Broken above by using the guard True. We no longer have sensing actions, but we can achieve much the same effect using a GSFA with guard True. For example,

says that the on board thermometer always measures the tem­ perature around the robot.

3.1 Some examples

We now proceed to consider examples that cannot be repre­ sented in the basic action theories from Section 2.

1. The outdoor temperature is unpredictable from state to state. However, when the robot is outdoors, its onboard thermometer measures that temperature.

Note that when the guard is false, i.e., when the robot is indoors, nothing can be concluded regarding the outdoor temperature.

1. The indoor temperature is constant when the climate control is active, and otherwise unpredictable. However, when the robot is indoors, its on board thermometer mea­ sures that temperature:

Note that in this case, if the climate control remains ac­ tive, then a robot that goes first indoors and then out­ doors will still be able to infer the current indoor temper­ ature using both sensing and regressing. To our knowl­ edge, no other representation for reasoning about action and change can accommodate this combination.

1. The distance between a (!-dimensional) robot and the wall is affected only by the moving actions. Also, the onboard sonar correctly measures the distance to the wall, but only when the reading is within a certain in­ terval.

In this case, the successor state axiom is universally ap­ plicable, meaning we can always regress all the way to So to determine the distance to the wall. However, if the distance to the wall in So is unknown, we would still not know the current value, and so it much more useful to be able to regress to a situation where the sonar reading was within its operating range.

1. If the robot is alone in the building, the state of the door is completely determined by the robot's open and close actions. Either way, any time the robot is in front of the door, its onboard door sensor correctly determines the state of the door.

One intriguing possibility offered by this example is that on closing a door, and later coming back in front of the door to find it open, a security guard robot would be able to infer that ·Alone.

1. A warning light for an alarm can go on unpredictably. Once it is on, however, it will stay on until the robot turns it off. Also, the robot can determine the state of the warning using its on board light sensor, provided it is looking at the light.

In this case, we need a complex guard for the successor state axiom, since we can only regress when the light was on previously or when the action is to turn it off.

3.2 Histories and the projection task

We are now ready to define the projection task formally. Ob­ viously, to be able to determine if a fluent holds at some point, it is no longer sufficient to know just the actions that have occurred; we also need to know the readings of the sen­ sors along the way. Consequently, we define a history as a sequence of the form (p,0) · (A1 , p,i) · · · (An, p,-;,) where Ai (1 :=:; i :=:; n) is a ground action term and p,i = (J.Lil, ... , /.Lim) (0 ::; i ::; n) is a vector of values, with /.Lij understood as the reading of the j-th sensor after the i-th action. If>. is such a history, we then recursively define a ground situation term end[>.] by end[(p,0)] = So and end[>. · (A, J7)] = do( A, t) where t = end~]. W~ also define a ground sensor fo~mula Sensed[>.] as 1\i=O /\j=l hj ( end[>.i]) = P,ij where Ai ts the subhistory up to action i, (p,0) · · · (Ai, JI;), and hi is the j-th sensor function. So end[>.] is the situation that results from doing the actions in>. and Sensed[>.] is the formula that states that the sensors had the values specified by >. 4 . The projection task, then, is this:

Given an action theory 'E as above, a history >., and a formula ¢>( s) with a single free variable s, deter­ minewhetherornot'EUSensed[>.] f= ¢>(end[>.]).

4 0bviously interesting histories >. have to satisfy certain legality criteria such as consistency of E U Sensed[>.] and conformance to Pass.

4 Generalized regression

In principle, the projection task as formulated can be solved using a general first-order theorem prover. But the ineffec­ tiveness of this approach in an even simpler setting is ar­ guably what led many to abandon the situation calculus and take up STRIPS. Our goal here is to keep the logical frame­ work. but show that in common cases, projection can be re­ duced using a form of regression to reasoning about the initial situation, as done in [11] . The reduction is tricky, however, because of the interaction between the various GSFAs and GSSAs, requiring us to solve (auxiliary) projection tasks at each step.

What we propose is a generalized form of regression that is a sensible compromise between syntactic transformations and logical reasoning. Specifically we require the latter only in evaluating the guards to decide which GSFAs and GSSAs to apply (see Section 4.1 where regression is again used).

In the following we assume that 2:: is an action theory as above,,\ is a history, and cf>(x, s) and 'if;(x, s) are sensor-fluent formulas, p(x, s) is a sensor formula, and r(x, s) is a fluent formula. We use the notation ¢\A to mean the formula that results from replacing every sensor function hi ( s) in ¢> by the j-th component of the final sensor reading in.-\. We denote by :Eo the part of 2:: formed by the initial database and the unique name axioms for actions as above.

Lemma 1 Let p(x, s) be a sensor formula. Then for every history ,\ the following statement is valid: 5

Proof: By induction on the structure of p(x, s). ·

To begin, we consider simplifications to formulas resulting from sensing, using the guarded sensed fluent axioms.

Definition 4.1 cf>(x, s) simplifies to 'if;(x, s) at,\ iff there are fluents F1 (t~, s), .. . Fk(t:, s) in cf>(x, s) with k 2 0, and for every 1 :::; i :::; k, there is a GSFA in 2::

where 2:: U Sensed[ .X] f= 'Va;(t:; end[ .X]), and 'if;(x, s) is the result of replacing each F; ( t:, s) in ¢>( x, s) by p; ( ( s) \,\.

Definition4.2 cf>(x,s) fully simplifies to 'if;(x,s) at,\ iff ¢>( x, s) simplifies to 'if;' ( x, s) at .-\, 'if;' ( x, s) simplifies only to itself at.-\, and 'if;(x, s) ='if;' (x, s)\,\.

Lemma 2 If cf>(x, s) simplifies to 'if;(x, s) at,\, then

2:: u Sensed[ .X] f= 'Vx.cf>(x, end[.-\]) = 'if;(x, end[ .X])

Proof: By logical manipulation and Lemma l. ·

Next, we consider simplifications involving reasoning backwards using the guarded successor state axioms.

Definition4.3 cf>(x,s) rolls back to 'if;(x,s) from a non­ empty history ,\ = ,\' · (A, jt) iff¢>( x, s) fully simplifies to ¢>' ( x, s) at ,\, and for every fluent Fl( t~, s), ... Fk (t:, s) in ¢/ ( x, s) with k 2 0, there is a GSSA in 2::

5 We assume a logic with equality.

where 2:: U Sensed[.-\'] f= 'Va;(t:, A, end[N]), and 'if;(x, s) is the result of replacing each Fi(t:, s) in cf>'(x, s) by /;(( A,s).

Lemma 3 If cf>(x, s) rolls back to 'if;(x, s) from a nonempty history,\ = ,\' · (A, jt), then

Proof: By logical manipulation and Lemma 2. ·

Putting both forms of simplification together we get: Definition 4.4 ¢>( x, s) regresses to 'if;( x, s) from ,\ iff either:

• ,\ = (J-Lo) and cf>(x, s)fully simplifies to 'if;(x, s) at.-\.
• ,\ = ,\' · (A, jt) and ¢>( x, s) rolls back to 'if;' ( x, s) from ,\, and 'if;' (x, s) regresses to 'if;(x, s) from A'.

Theorem 4 If cf>(x, s) regresses to 'if;(x, s) from,\ then

Proof: By induction on the number of actions in ,\ using Lemma 2 and Lemma 3. ·

Observe that a formula cf>(x, s) can regress to zero, one, or more formulas 'if;(x, s) from,\, depending on how many entailed guards we can find for the fluents at each stage.

When a formula with a single free variable does regress, then, as a consequence of Theorem 4, we get the following:

Corollary 5 Under plausible consistency conditions for 2:: U Sensed[.-\], 6 ifcf>(s) regresses to 'if;(s)from ,\then

This provides a soundness result for regression: to perform the projection task, it is sufficient to regress the formula, and check the result against the initial database.

Unfortunately, regression in general cannot be complete. To see why, suppose nothing is known about fluent F; then a formula like (F(s) V ·F(s)) will not regress even though it will be entailed at any history. In Section 5, we show that for certain histories (namely those where enough useful sensing information is available), regression will be complete.

The other drawback of regression as defined is that we need to evaluate guards. However, evaluating a guard is just a sub­ projection task, and so for certain "well structured" action theories, we can again apply regression, as we now show.

4.1 Acyclic action theories and g-regression

We now restrict our interest to action theories 2:: that are acyclic, in the following sense. Let-<. called the dependency relation, be a binary relations over fluents s.t. F' -< F iff thereisaGSFA{a(z,s) :::::> [F(z,s) :=p(z,s)]}inl::where F' occurs in a(z, s) . An action theory 2:: is acyclic iff the de­ pendency relation -< is well-founded. When it is, we call the level of a fluent F the maximal distance in terms of -<-chains from a bottom element of -<.

Definition 4.5 Let 2:: be acyclic. The sensor-fluent formula cf>(x, s) g-regresses to 'if;(x, s) from,\ iff cf>(x, s) regresses to 'if;(x, s) and

6 We will elaborate on this in a longer version of the paper.

• for every simplification step, where a GSFA in I:

is used to replace F(~ s) by p(~ s)\X for some sub­ history X, we have that the guard a(~ s) g-regresses to some a' ( ~ s) from >..' s. t. I:o f= If a' ( ~ So);

• for every roll back step, where a GSSA in I:

is used to replace F(~ s) by 'Y(~ A , s) for a subhistory >.'·(A, j1) , we have that the guard a(~ A, s) g-regresses to some a'(~ A, s)from >..' s.t. I:o f= \fa'(~ A, So) .

The trickiest aspect of this definition is to show that the re­ cursion is indeed well-founded. This is done by simultane­ ous induction on the length of)... and the level of the fluents. Clearly, if a formula g-regresses to another, then it regresses also (although not vice-versa). The main point however is that we only ever need to evaluate formulas at S0 :

Theorem 6 For an acyclic I:, under plausible consistency conditions for I: U Sensed[>.], if ¢(s) g-regresses to some formula from>., then the only theorem-proving needed to per­ form projection is to evaluate formulas in I:0 .

Proof: By induction on the total number of simplification and roll back steps used tog-regress¢, using Corollary 5. ·

5 JIT-histories

As noted above, we cannot expect to use regression to eval­ uate sensor-fluent formulas in general: a tautology might be entailed even though nothing is entailed about the component fluents. However, in a practical setting, we can imagine never asking the robot to evaluate a formula unless the history is such that it knows enough about the component fluents, using the given GSSAs and GSFAs, and their component fluents.

For example, assume we have the indoor temperature ax­ ioms from Section 3.1. We might only ask the robot to evalu­ ate a formula that mentions the indoor temperature for those histories where the climate control is known to have remained on from some earlier point in the history where the robot was known to be indoors. We do not require the robot to know whether the climate control was on before then (since this may have required going to a control panel), or even whether it is indoors now. In general , we call a history just-in-time for a formula, if the actions and sensi1 _; readings it contains are enough to guarantee that suitable formulas (including guards) can be evaluated at appropriate points to determine the truth value of all the fluents in the formula. More precisely:

Definition 5.1 An history )... is a just-in-time-history (liT­ history) for a sensor-fluent formula ¢( x, s) iff:

• ¢(x,s) = ·¢1(x,s) I ¢I(i,s) 1\ ¢2(i,s) and .X is a liT-history for ¢1 ( x , s) and ¢2 ( x , s);
• ¢(i,s) = 3y.¢1(y,x, s) and>. is a liT-history for the (open) formula ¢1 (y, x, s);
• ¢(x, s) is a sensor formula;
• ¢(x,s) = F(~s), where F is a fluent, and for some GSFA {a(z, s) ::J [F(z, s) = p(z, s)]}, >. is a liT­ history fora(~ s), and I: U Sensed[>.] f= \fa(~ end[>.]) ;
• ¢(i, s) = F(~ s), a fluent, .X is an empty history (p0), and either I:o f= IfF(~ So) or I:o f= lf·F(~ So) ;
• ¢(i, s) = F(~ s), a fluent, .X =>..' ·(A , j1) , and for some GSSA {a(z,a,s) ::J [F(z, do(a,s)) = 'Y(z, a, s)]}, >..'is a liT-history both for a(~ A, s) andfor'Y(f, A , s), and I: U Sensed[>.'] f= Va(f, A, end[>.']).

For JIT-histories we have the following theorem:

Theorem 7 Let I: be an action theory as above, and ¢(i, s) a sensor-fluent formula. If .X is a liT-history for¢( x, s ), then there exists a formula 7/J(x, s) such that:

1. ¢(x, s) regresses to 7/J(x, s)from >.,and
2. if I: is acyclic, then ¢(x, s) g-regresses to 7/J (x, s) from >., and either I:o f= \fx.?jJ(i, So) · or I:o f= Vx.·7/J(x, So).

Proof: (I) is proven by induction on the length of .X and induction on the structure of ¢( x, s); (2) is proven by simultaneous induction on the length of)... and the (max) level of the fluents in the ¢(i, s), and induction on the structure of ¢(x, s) .·

This theorem shows that for JIT-histories, regression is both a sound and complete way of performing projection.

6 An evaluation procedure for projection

Although our action theories are assumed to be open-world, a JIT-history provides a sort of dynamic closed world assump­ tion in that it ensures that the truth value of any fluent will be known whenever it is part of a formula whose truth value we need to determine. This allows us to evaluate complex formu­ las as we would if we had a normal closed world assumption. We now consider a Prolog procedure that does this.

We assume the user provides the following clauses: 7

• fluent(F), for each fluent F,
• sensor( h), for each sensor function h,
• ini(F), for each fluent F such that I:0 f= F(So),
• closed( F), for each fluent F such that I:0 f= F(So) or I:o f= ·F(So),
• gsfa(a, F, p), for each GSFA,
• gssa(a, a, F, 7), for each GSSA, where a is the distinguished action term quantified in a and 'Y

Formulas are expressed using and(¢, 7/J). neg(¢), equ(t, t'), and some(v, ¢) where v is a Prolog constant. We drop the situation arguments from fluents and sensor functions in for­ mulas (and keep track of the situation in the history).

Histories are represented as lists. For brevity, we assume a predicate last(>., h, r) which extracts the last valuer for sensor function h in history .X. We assume also a predicate sub(v, x, ¢, ¢') with the meaning that ¢' is the formula ob­ tained by substituting x forv in the formula¢ (see [6]). Now we define eval(>., ¢,b) , with the intended meaning that the formula¢ evaluates to the truth-value b (tt/ff) for the his­ tory >., as follows:

7 For simplicity in what follows, we do not distinguish between situation calculus formulas and their representations as Pro log terms.

eval(H,and(Pl,P2) ,ttl :­ eval(H,Pl,tt), eval(H,P2,tt). eval (H, and(Pl, P2), ff) :- eval(H,Pl,ff); eval(H,P2,ff). eval(H,neg(P) ,ttl :- eval(H,P,ff). eval(H,neg(P) ,ff) :- eval(H,P,tt). eval(H,some(V,Pv) ,ttl :- sub(V,_,Pv,Px), eval(H,Px,tt). eval(H,some(V,Pv) ,ff) :­ not(sub(V,.,Pv,Px), not eval(H,Px,ff)). I* double negation for ''for all'' *I I* so not eval(H,Px,ff) flounders! *I eval(H, equ(E,V) ,ttl :- sensor(E), last(H,E,R), R=V. eval(H,equ(E,V) ,ff) :- I* Neg as failure *I sensor(E), last(H,E,R), not R=V. eval([(Mu)),F,tt) :- fluent(F), ini(F). eval([(Mu)] ,F,ff) :-I* Neg as failure*/ fluent(F), closed(F), not ini(F). eval(H,F,B) :- fluent(F) , gsfa(Alpha,F,Rho), eval(H,Alpha,tt), eval(H,Rho,B). eval([(A,MuliHJ,F,B) :- fluent(F), gssa(A,Alpha,F,Gamma), eval(H,Alpha,tt), eval(H,Gamma,B).

Observe that a formula eval(.A, ¢,b) can either succeed re­ turning tt, succeed returning ff, fail, or not terminate. Un­ der the assumption that all the auxiliary predicates are correct and terminating, we get the following soundness and a weak form of completeness for eval:

Theorem 8 Assume that eval(.A, ¢(i, s), B) succeeds with computed answer i=i', B=b. If b=tt, then ~ U Sensed[.AJ f= V¢(f, end[.A]); ifb=ff then~ U Sensed[.AJ f= V·¢(f, end[.A]).

Proof: By induction on the structure of ¢(i, s). ·

Theorem 9 Let .A be a liT-history for ¢(i, s). Then, eval(.A, ¢(i, s), B) does not finitely fail.

Proof: By induction on the structure of ¢(i, s). ·

Note that we cannot guarantee termination since we can get into a loop evaluating guards of GSFAs or GSSAs, or by floundering in trying to evaluate to f f an existential. We can eliminate the first problem by using acyclic action theories. For the second, we can close the domain. Let domain( o) be a user-defined predicate over a finite domain. We can then change the definition of eval for existentials as follows:

eval(H,some(V,Pv),tt) :- domain(O), sub(V,O,Pv,Po), eval(H,Po,tt). eval(H,some(V,Pv),ff) :- not(domain(O), sub(V,O,Pv,Po), not eval(H,Po,ff)).

For this new version of eval we get a completeness result:

Theorem 10 Let~ be acyclic, let ¢(s) be a sensor-fluent for­ mula with no free variables except the situation argument s, and let .A be a liT-history for ¢(s). Then, eval(.A, ¢(s), B) always succeeds, returning either t t or f f.

So under these circumstances, eval is a sound and complete implementation of projection.

7 Conclusions

We have given a formal definition of projection for a gener­ alized action theory where successor state axioms and sens­ ing information are only conditionally applicable. We also showed that in certain circumstances, a regression-based eval­ uation procedure could correctly perform the task.

Many open problems remain, however. How can we de­ cide in an automated but practical way when regression can be used? It may be expecting too much of a conditional plan­ ner to determine what actions it should perform now to permit it to later use sensing information in this way. An interest­ ing alternative is offered by the high-level program execution model. Given a program like "if¢ then do <h else do o2 ," the user can take the responsibility of inserting a prior program ensuring that the resulting history is just in time for ¢.

Another related problem is the projection of initial databases. Once a robot actually performs a sequence of ac­ tions in the world, we would prefer to no longer regress all the way back to the initial situation, but instead to project the database forward to the current state [8]. How this can be done for the action theories we are proposing remains to be seen.