Causal Theories of Action: A Computational Core

1 Introduction

While there are abundance of formalisms for writing ac­ tion theories that incorporate explicit causal rules not only between actions and fluents but also between fluents (e.g. [Baral , 1995; Lin, 1995; Thielscher, 1995; Gustafsson and Doherty, 1996; McCain and Turner, 1997; Zhang and Foo, 2001; Kakas et a!., 2001 ]), and there are some implemen­ tations of causal action theories [Lin, 2000; McCain and Turner, 1998; Kakas et al., 2001], there have been few formal studies of complexities of various reasoning tasks in these causal action theories. In this paper, we investigate this is­ sue. We first study various reasoning tasks such as comput­ ing the precondition of an action, checking if an action theory specifies a deterministic action, performing temporal projec­ tion, and computing regression in a very simple causal action framework that is primarily aimed at representing determin­ istic actions. Basically, an action theory for action a in this framework is just a finite set of action effect rules of the form

if 11 1\ · · · 1\ ln is true, then action a causes l to be true

and causal rules of the form

where l's are literals.

Surprisingly, even in this simple framework, one-step tem­ poral projection problem with complete initial state in the following form: given a set of literals that completely deter­ mines the initial state, and an action a, determine if a given fluent will hold in the state resulted from doing a in the initial state, is intractable. This compares with STRIPS and ADL, CRIL/Universite d' Artois F-62307 Lens Cedex, France marquis@ cril. univ-artois.fr which are like this simple framework except that they do not allow causal rules, where problems like temporal projection and regression are easy.

As simple as this framework may be, it nonetheless cap­ tures the computational core of causal action theories. In­ deed, we show that if one extends it to allow arbitrary formu­ las in both the right and left hand sides of the effect and causal rules: ( 1) this extends the expressiveness of the language, but (2) it does not affect the complexities of any of the reasoning tasks considered here.

The rest of this paper is organized as follows. After some formal preliminaries (Section 2), we present a framework for simple action theories in Section 3. Complexity results are presented in Section 4. Before presenting some related work and concluding, we briefly show in Section 5 how our simple action theories can be generalized, without questioning the complexity results (in the general case). For space reasons, proofs are only sketched or omitted.

2 Formal preliminaries

Let PROPps be a propositional language defined induc­ tively from a finite set P S of propositional symbols (atoms), the boolean constants T (true) and l_ (false), and the con­ nectives ...,, V, /\, => and {::}. Lps is the set of all literals generated from P S . For each formula ¢, V ar ( ¢) denotes the set of atoms occurring in ¢.

We shall also consider two isomorphic copies of PROPps: PROPps, and PR0Pps,+ 1 · Each formula c/Jt (resp. ¢t+l) from PROPps, (resp. P ROPps,+J is obtained by substituting in a uniform way in the formula ¢ E PROPps every atom p E P S by the atom Pt (resp. Pt+d· Propositions indexed by t are used to express condi­ tions about current situation, and those indexed by t + 1 about the situation resulted from doing action a in the current situ­ ation. In the following, by an initial state formula we mean a formula from PROPps,, and by a successor state formula we mean a formula from P R0Pps,+ 1 · Finally, we shall con­ sider the language P ROPps, uPs,+ 1 and take advantage of it to characterize the effects of action a.

A truth assignment over PSis called a complete state. A truth assignment over P St is called a complete initial state, while a truth assignment over P St+l is called a complete suc­ cessor state. In order to avoid heavy notations, we shall iden­ tify each complete states with the conjunction of literals s is the unique model of it.

3 Simple action theories

We shall first consider simple causal action theories.

Definition I (simple action theory) A simple action theory for action a is an ordered pair T01 = (Ef f(a), Causal) where

• E f f (a) is a finite set of effect rules, of the following form:

where l 's are literals from L ps, and l can also be .1. The left side is understood to be a tautology when n = 0. When l = .1, the effect rule is really an action precondi­ tion axiom about a . Notice that for our purpose in this paper, we assume that a is the only action.

• Causal is a finite set of causal rules of the following form:

where l 's are literals from Lps. Again, the left side is understood to be a tautology when n = 0.

Such simple action theories are sufficient to encode ac­ tions with conditional effects. The ramification problem is addressed through causal rules, which represent static laws and express how ftuents are related. While primarily targeted at representing deterministic actions, they can sometimes give rise to indeterministic effects when there are cyclic causal rules such asp ----+ p.

Causal theories of this form are special cases of causal the­ ories in situation calculus [Lin, 1995], domain descriptions in action languages [Giunchiglia and Lifschitz, 1998], and other more general formalisms (e.g. [McCain and Turner, 1997; Zhang and Foo, 200 1]). While these formalisms do not al­ ways agree on their semantics in the general case, most of them coincide on this special class.

Definition 2 (completion) The completion cl(T01) of a (simple) action theory T01 is the formula defined by

• T(a) = 1\{pret => postt+J I Eff(a) contains pre~ post};
• T( Causal) 1\ { le ftt => rightt, le ftt+l => rightt+l I Causal contains left ----+ right};
• for each literal! E Lps, let <l> 01 (l) = V{pret I Eff(a) contains pre~ l}, q, c (l) = V { le ftt+l I Causal contains left ----+ l}, <I>(l) = <l> 01 (l) v <I>c (l),

frame(l) = (lt 1\ -.<I>(Z)) => lt+l· where i, the comple­ ment of l is defined as follows: for any atom p, p = ·P and ...;p = p;

• cl(T01 ) = T(a) 1\ T(Causal) 1\ 1\tELps frame(l).

We assume that T 01 mentions each atom of P S (otherwise some atoms of P S would be useless); under this assumption, the size of cl(T01 ) is polynomial in the size ofT01 .

Given a simple action theory T01 , a truth assignment over PROPps,uPs,+ 1 is said to be a model ofT01 if and only if it satisfies cl(T01 ). Each model ofT01 is formed by the union ( St, s~+J) of a complete initial state St and a complete suc­ cessor state s;+l ·

As one can see, the construction of cl(T01 ) from T01 is simi­ lar to the way a causal theory is transformed to classical logic in [Lin, 1995] and to literal completions [McCain and Turner, 1997; Lifschitz, 1997]. In fact, all these approaches yield log­ ically equivalent theories.

4 Complexity issues

4.1 Executability and determinism

Several properties are of interest when dealing with action theories. First of all, there is the question of whether an action is executable in a given initial situation.

Definition 3 (executability) Let T01 be an action theory for action a and let <p be a formula from PROPps . (T01, <p) is a positive instance of EXECUTABILITY (the executability problem) if and only if for any complete state s that satisfies <p, there is a states' such that (st, s;+1) I= cl(TOi) .

Whenever (T01 , <p) is a positive instance of EXECUTABIL­ ITY, a is said to be executable under <p; a is said to be fully executable if and only if it is executable under T.

Proposition I

1. In the general case, EXECUTABILITY is IT~-complete.
2. Under the restriction where <p is a complete state, EXE­ CUTABILITY is NP-complete.

Proof:

• I . Membership is easy. Hardness comes from the following poly­ nomial reduction from the E~-complete problem QBF2 ,3 to the problem of checking that a is not executable under T. Let Q = ( { a1, ... , an}, {b1, ... , bp}, ,B) be an instance of QBF2,3 1 . Wlog, we assume that ,B is a DNF formula D1 V ... V Dm. We now define M(Q) = T0 = (0, Causal) where Causal = { Di ----+ new, Di ----+ -.new I i = 1 ... m} U { bi ----+ bi, -.bi ----+ -.bi I i = 1 ... p} and new is a new atom, not occurring in ,B. Q is a positive instance of QBF2 ,3 if and only if a (as given by M(Q)) is not executable under T.
• Comes directly from the fact that, when cp is complete, then a is executable under it iff the propositional theory { cp} U cl(To) is consistent. ·

Another important property is determinism. Intuitively, an action is deterministic if there is at most one successor state corresponding to any initial state.

Definition 4 (determinism) An action theory T01 jor action a is a positive instance of DETERMINISM (the determinism problem) if and only if a is deterministic, i.e., for all St E 2Ps, and for all s;+l, s~'+ 1 E 2P 5 ·+ 1 such that (st. s;+ 1 ) I= cl(T01 ) and(st,s~'+ 1 ) I= cl(T01 ), thens;+l = s;~ 1 .

Proposition 2 DETERMINISM is coNP-complete.

1 Let us recall that Q is a positive instance of QBF2 ,3 if and only if it is valid, i.e., there exists an assignment a of variables a1, ... , an such that for all assignments b of variables b1, . .. , bp we have (a, b) I= ,B (where ,B is a formula from PROPps s.t. Var(,B) = {a1, ... , an, b1, . . . , bp}). QBF2 ,3 is still E~-complete when ,B is under DNF.

Proof Membership is easy. Hardness comes from the following polynomial reduction from DNF-YALIDITY. Let~ = D1 V ... V Dm be any formula from P RQPps under DNF and let M(~) be the instance of DETERMINISM defined by T0 = (Ef f( a), Causal) withE!f(a) = {D1 ~ new, . .. ,Dm ~ new}and Causal = {new ----+ new, · new ----+ ·new }, where new is a new atom not mentioned in ~ - ~ is valid if and only if M(~) is deterministic. ·

4.2 Progression

There are two forms of the progression problem, also referred to as (one-step) temporal projection. The simpler one, in the form of a query about the effects of an action given some information about the current situation, can be described as a triple (Tc, ¢ , 'lj;) where

• To: is an action theory;
• ¢ is a formula from PROPps representing the knowl­ edge state before the action is performed; we assume that the action a is executable under ¢;
• 'ljJ is a formula from PROPps we are interested in the truth value of which after the action has been performed.

Definition 5 (progression) Let To: be an action theory and ¢ a formula from PROPps such that a is executable un­ der ¢. Let 'lj;bea formulafromPROPps . (To:,¢,'1j;) isa positive instance ofPROGRESSION (the progression problem) if and only if'lj;t+l holds in any possible complete successor state by action a of any complete initial state s1 satisfying ¢1; equivalently:

According to this definition, progression is really a two­ step process: first make sure that the action is executable un­ der the given condition about the initial state, and then com­ pute the changes that the action will have under the given initial condition. We have shown that the first step is II~-hard in the worst case. The following proposition shows the com­ plexity of the second step under various assumptions.

Proposition 3 We have identified the following complexity results ("coNP-c" stands for coNP-complete).

Proof

1. Membership to coNP comes easily from the fact that (To,¢;, 1/;) is a positive instance of PROGRESS ION if and only if ¢;t 1\ cl(To) f= 1/;t+I holds.
2. In the case where ¢;1 is a complete initial state and there are no causal rules, cl(To) = {(l;) t+I <=> Xi ,t ll; E Lps U {.L}} , where for each i, Var(x;, 1) ~ PSt- When ¢;t is a complete initial state, each Xi,t can be evaluated in linear time to a truth value. This truth value is given to the corresponding (l;)t+I· Since a is executable under ¢;, this will not lead to a contra­ diction, and a complete successor state St+ I is characterized by the values given to the literals (l;)t+I· It remains to check in linear time whether St+ I f= 1/;t+I to determine whether the instance is positive or not.
3. What remains to be done is showing coNP-hardness in these two cases:
4. (a) there are no causal rules and 1/; is a literal;
5. (b) ¢; is a complete state and 1/; is a literal;

Case 1: no causal rules, 1/; is a literal.

The proof comes from the following polynomial reduction from DNF-VALIDITY. Let~ = D1 V .. . V Dm be any DNF formula and let M(O be the instance of PROGRESSION de­ fined by

• To = (Eff(a) , Causal) where Eff(a) = {D1 ~ new, ... , Dm ~ new} and Causal= 0;
• ¢; = T; 1/; = new, where new is a new atom not mentioned in~-

Clearly a is executable under T, and ~ is valid itl M(O is a posi tive instance of PROGRESSION.

Case 2: ¢; is a complete state, 1/; is a literal

The proof comes from the following polynomial reduction from DNF-VALIDITY. Let~ = D1 V ... V Dm be any DNF formula, and let Var(~) = {x1 , ... , xp} be the set of variables appearing in~ - We then define M(O = (To ,¢;,1/;) where To = (E ff (a) , Causal) is given by E ff (a) = {T ~ new'} and

and new, new' are new atoms (not appearing in 0- Let¢; = s, s being any complete state satisfying ·new 1\ ·new', and 1/; = new. It can be seen that a is executable in (under) s, and ~is valid iff M(~) is a positive instance of PROGRESSION. ·

Our results about the complexity of executability and pro­ gression, taken together, are strongly related to a result in [Turner, 2002] (namely Theorem 8(i)) which says that one-stage conformant planning (without concurrency) is II~­ complete. Indeed, checking that a is a valid plan in this con­ text amounts to checking that a is executable in all possible initial states and that its progression sati sfies the goal. By considering executability and progression separately, we see more clearly that II~-hardness in Turner's result is solely due to the hardness of executability.

A second, perhaps a more difficult way of seeing the pro­ gression problem, is the following: given some information about the current situation, compute all possible successor states. Formally, this looks like consequence finding: given a formula ¢ E PROPps, compute the strongest successor state formula '11 E PROPps such that ¢1 1\ cl(To: ) I= 'llt+l· Model-theoretically, this corresponds to finding all complete successor states s~+l such that there is a complete initial state s1 that satisfies ¢1 for which s1 1\ cl(To:) 1\ s;+l is consistent. As it turns out, this formula '11 t+l is the strongest necessary condition of ¢1 under cl(To:) on P R0Pps,+ 1 [Lin, 2001] :

Definition 6 (Pro(To:, ¢) ) Given an action theory Ta and a formula ¢ from PROPps such that a is executable un­ der ¢, the progression formula Pro(T o: , ¢) is the formula \II from PROPps (unique up to logical equivalence) such that (Ta, ¢, 'lj;) is a positive instance of PROGRESSION if and only if '11 I= 'ljJ holds.

Pro(To: , ¢) can be characterized equivalently by:

Proposition 4

1. Lets be any complete state. We haves I= Pro(Ta, ¢) iff3s; E 2Ps,, (( (s;, St+l) I= cl (Ta) and s; I= ¢t), i.e., there exists a complete initial state s; such that s; I= ¢1 and (s;, St+d I= cl(Ta) (or equivalently, cPt !\ cl(Ta) !\ St+l is consistent).
2. Pro(Ta, ¢) t+l = 3PSd¢t !\ cl(Ta)).

4.3 Regression

There are (at least) two possible definitions for regression, each of which corresponds to a given need: deductive re­ gression (also referred to as temporal explanation or weak preimage) and abductive regression (also referred to as strong preimage).

Definition 7 (deductive regression) Let Ta be an ac­ tion theory and let ¢, 'ljJ be two formulas from PROPps. (Ta, ¢, 'l/J) is a positive instance ofDEDUCTIVE REGRESSION (the deductive regression problem) if and only if

Similar to progression formulas, we can define deductive regression formulas:

Definition 8 (RegD(Ta, 'lj; )) Given an action theory Ta and a formula 'ljJ from PROPps, the deductive regression for­ mula RegD(Ta, 'l/J) is the formula~ from PROPps (unique up to logical equivalence) such that (T a, ¢, 'ljJ) is a positive instance of DEDUCTIVE REGRESSION if and only if~ F ¢.

We immediately get that for any two formulas ¢, 'ljJ from PROPps, (Ta, ¢, 'l/;) is a positive instance of DEDUCTIVE REGRESSION if and only if (Tcr , -,¢, -,'lj;) is a positive in­ stance of PROGRESSION. We also have:

Proposition 5

• I . Lets be any complete state. We haves I= RegD(Ta, 'l/J) if and only if3s;+l E 2P 5 '+ 1 , (((st,s;+1 ) I= cl(Ta) and s;+l I= 'l/;1+1), i.e., there exists a complete succes­ sor state s~+l such that s~+l I= 'l/Jt+l and (s~, s~+ 1 ) I= cl (Ta) (or equivalently, 'l/Jt+l 1\cl (Ta) !\ St is consistent).
• RegD(Ta,'l/J)t := 3PSt+l ·('l/Jt+l 1\cl(Ta)).

This characterization helps understanding deductive re­ gression: it intuitively means that we are interested in find­ ing the set of states which could be possible states before the action, knowing that 'ljJ holds after the action. This type of regression is useful for postdiction, i.e., reasoning about the past state of the system.

Since deductive regression is expressed as a deduction problem, its complexity is easy to find out.

Proposition 6 DEDUCTIVE REGRESSION is coNPcomplete.

Definition 9 (abductive regression) Let Ta be an ac­ tion theory and let ¢, 'ljJ be two formulas from PROPps. (Ta, ¢, 'lj;) is a positive instance of ABDUCTIVE REGRESSION (the abductive regression problem) if and only if for any com­ plete states, St !\ cl(Ta) I= 'l/Jt+l implies s I= ¢.

The corresponding search problem is defined by:

Definition 10 Given an action theory Ta and a for­ mula 'ljJ from PROPps, the abductive regression formula R egA(Ta ,'l/J) is the formula~ (unique up to logical equiv­ alence) such that (Ta, ¢, 'l/;) is a positive instance of ABDUC­ TIVE REGRESSION if and only if¢ F ~.

In other words, ~~ is the weakest sufficient condition of 'l/Jt+l under cl(Ta) on PROPps, [Lin, 2001].

Proposition 7

1. Let s be any complete state. s I= R eg A (T a, 'ljJ) if and only if'Vs~+l E 2P 5 '+ 1 , if(st ,S~+ 1 ) I= cl(Ta) then s~+l I= 'l/Jt+l (or, equivalently, St !\ cl(Ta) I= 1/Jt+J ).

Thus, abductive regression amounts to finding the set of all complete initial states s1 for which all possible complete successor states s~+I w.r.t. Ta satisfy 1/J. This means that we are interested in finding the set of states in which performing the action leads to states necessarily satisfying 'ljJ - provided that the action can be performed in them. This type of regres­ sion is useful for planning, i.e., reasoning about the minimal conditions under which an action succeeds in reaching the goals. Thus, (Ta, ¢, 'lj;) is a positive instance of ABDUCTIVE REGRESSION if and only if¢ implies the minimal conditions under which the action leads to the goal.

This shows that the qualifications "deductive" and "abduc­ tive" are only related to the way initial states can be inferred, and not to the confidence we have in them to be satisfied . Indeed, as far as reasoning is concerned, deductive conclu­ sions can be taken for sure since deduction is truth-preserving while abductive conclusions cannot be taken for sure in gen­ eral since abduction is only falsity-preserving. Contrariwise to such a reasoning situation, initial states St obtained through deductive regression are only possible ones given 'ljJ and a: it could be the case that performing action a in s leads to a suc­ cessor state in which 'ljJ does not hold. Contrastingly, initial states s1 obtained through abductive regression lead to suc­ cessor states where 'ljJ necessarily holds.

The following proposition makes precise the links between both forms of regression:

Proposition 8

1. RegA(Ta , 'l/J) = RegD(Ta, 'l/J) if and only if a is fully executable and deterministic.
2. I . RegA(Ta,'l/J) I= RegD(Ta,'l/J) if and only if a is fully executable.

Proof We give the proof of the first point:

RegA(Tc, 'lj;) f= RegD(Ta, 'lj;)

iff V'PSt+t·(-d(Ta )) is inconsistent

iff 3PSt.(V'PSt+t·(·cl(Ta ))) is inconsistent

iff V'PSt-(3PSt+t·cl(Ta)) is valid

iff a is fully executable.

·

Abductive regression is computationally more expensive than deductive regression:

Proposition 9 ABDUCTIVE REGRESSION is IT~-complete.

Proof Membership is easy. Hardness comes from the following polynomial reduction from the I:~-complete problem QBF2,3 to ABDUCTIVE REGRESSION. Let Q = ({at , ... , an} , {bt, ... , bp} ,,B) be an instance ofQBF2,3· Wlog, we assume that ,8 is a DNF formula D 1 V ... V Dm. We now defineM(Q) = (T0 ,¢,'1j;) where

• T0 is concerned by the fluents built over {a1, ... ,an,b1 , ... ,bp,new} (where new is a new atom, not appearing in {3) and the following set of static causal rules:

(and no effect rule);

• ¢=new;
• 'ljJ =new.

Q is a positive instance of QBF2,3 iff M( Q) is a positive instance of ABDUCTIVE REGRESSION. ·

5 Generalized action theories

Here we want to extend causal and effect rules so as to allow for any possible consequents, including disjunctions, while keeping the framework simple enough.

Definition 11 (generalized action theory) A generalized action theory To. for action a is an ordered pair (Ef f(a) , Causal) where

• E f f (a) is a finite set of effect rules of the form pre ~ post[L]) where pre, post are formulas from PROPps and L ~ Lps.
• Causal is a finite set of causal rules of the form le ft ~ right[L] where left and right are formulas from PROPps and L ~ Lps.

The completion consists now in writing down that every literal l persists if and only if there is no effect (action or causal) whose precondition is verified and on which l de­ pends. More generally, rather than writing "there is no ef­ fect (action or causal) whose precondition is verified and on which l depends", we specify for each action rule the fluents L that are influenced and for which there should not be any frame axiom if the action rule is enabled.

Definition 12 (completion) The completion cl(Ta.) of gen­ eralized action theory To. is the formula defined by

• T(a) = 1\ {pre1 :::::} posit+ I I Ef f(a) contains pre ~ post[L]} ;
• T( Causal) 1\ { leftt :::::} rightt, leftt+l :::::} rightt+l I Causal contains left ~ right[L]};
• for each literal[ E Lps, let ~o.(l) = V {pret I Ef f(a) contains pre ~ post[L] and l E L}, ~c (l) = V{leftt+l I Causal contains left ~ right[L] and l E L}, ~(l) = ~a.(z) v ~c(l), frame(l) = (lt 1\ ·~(l)):::::} lt+1;
• cl(Ta.) = T(a) 1\ T(Causal) 1\ I\ 1 ELPs frame(l).

As for simple action theories, we assume that each symbol of PS occurs in To. so that the size of cl(Ta.) is polynomial in the size of To..

In the previous definition, ~a (l) gathers the preconditions of effect rules whose postcondition influences positively l (and similarly for ~c (l)); the completion frame(l) means that if l is initially true and there is no active action rule nor any causal rule whose consequent part influences negatively l, then l persists after a is performed.

By default, the set L associated with an action rule (resp. a causal rule) is the set of literals Lit(post) (resp. Lit( right)) positively mentioned in the negation normal form of post (resp. of right) -an alternative, more refined possibility be­ ing the set of literals DepLit(post) (resp. DepLit(right)) on which post (resp. right) semantically depends [Lang and Marquis, 1998]. It is easy to show that the completion of To. as defined above (Definition 12) is equivalent to the com­ pletion given at Definition 2 whenever T a. is simple (in that case, the default choice for L in each rule is considered, i.e., L = { l} whenever the consequent part of the rule is l) .

For instance, so to say that flipping a coin release head, we simply write holdingCoinl..!i:!+true[head, ·head], i.e., if one is holding the coin initially, then after the action of flip­ ping it, we can neither infer head nor ·head using inertia.

Due to space limitation, we cannot provide the full details here. In a nutshell, the main reasons why generalized action theories are interesting are twofold. On the one hand, we can prove that generalized action theories can be used to repre­ sent any nondeterministic action (associating a nonempty set of successor states to any initial state), while such a com­ pleteness property is not satisfied by simple action theories. On the other hand, the complexity of EXECUTABILITY, DE­ TERMINISM, PROGRESSION, DEDUCTIVE/ABDUCTIVE RE­ GRESSION, from generalized action theories coincide with the corresponding complexity result for simple action the­ ories in the general case. This shows that the gain in ex­ pressiveness offered by generalized action theories is not bal­ anced by a complexity increase for any of these reasoning tasks. Furthermore, this suggests that the simple action the­ ories considered here constitute the computational core of causal action theories.

6 Other related work

[Liberatore, 1997] investigates the complexity of reason­ ing about action in the language A [Gelfond and Lifschitz, 1993], therefore he considers only deterministic actions with­ out static causal rules. He shows the coNP-completeness of the progression problem in language A, to be related to the right-upmost square in our Proposition 3. [Eiter et al., 2001] study the computational of many planning problems (includ­ ing the progression problem as a particular case) using an ac­ tion description language based on answer set semantics.

[Drakengren and Bjareland, 1997; 1999] investigate the complexity of checking the consistency of a scenario descrip­ tion in a temporal logic in the style of [Sandewall, 1994] which shares some similarities with causal theories of action, although both the syntax and the semantics are different. No static causal rules are considered (but on the other hand, the language allows for explicit time and concurrency). Check­ ing the consistency of a scenario description is NP-complete and falls in P under specific syntactical restrictions.

Reasoning about action has strong connections with be­ lief update, and therefore, the complexity study of belief up­ date operators is relevant to our concern. The update opera­ tors whose complexity is studied in [Eiter and Gottlob, 1992;

Herzig and Rifi, 1999; Liberatore, 2000] do not consider static causal rules, but allow for expressing any effects, es­ pecially di sjunctions. The complexity of checking whether 'ljJ E K B o r.p - where o is the update operator, mapping a logical theory and a formula to a logical theory- corresponds to the progression problem 2 .

7 Conclusions and future work

The main contribution of this paper is the identification of complexity results corresponding to many reasoning tasks considered when dealing with causal action theories. It re­ mains to be checked to what extent these results are changed when considering additional capabilities such as concurrency (as in [Giunchiglia and Lifschitz, 1998]) or resources.

Because of the way the progression problem is stated, it was expected that for arbitrary description r.p of the initial sit­ uation and arbitrary query 'ljJ about the successor situation, the problem is coNP-complete. But when we first started study­ ing the problem, we were really expecting that when r.p is a complete state, the problem would be easier; we were sur­ prised that even in this case it turned out to be intractable. In retrospect, what happens is that even though both action effect rules and causal rules have very restricted form, the complete action theory cl(Ta) can be complex, and may not always be deterministic. An interesting question is then if we already know that the action theory is deterministic, would progression with complete initial state still be intractable? We do not know the answer at that stage.

Acknowledgements

Tha authors would like to thank the anonymous referees for helpful comments. The second author's work was supported in part by HK RGC CERG HKUST6182/01E. The third au­ thor has been partly supported by the IUT de Lens, the Uni­ versite d' Artois, the Region Nord I Pas-de-Calais under the TACT-TIC project, and by the European Community FEDER Program.