Expressive Reasoning about Action in Nondeterministic Polynomial Time

1 Introduction

The rapid development of efficient heuristics for decid­ ing satisfiability for propositional logic (GSAT and sim­ ilar heuristics [Selman et al., 1992]) motivates thorough investigations of the usability of NP-complete problems in general. In this paper we introduce a logic of ac­ tion and change which is expressive in the sense that it can represent most propositionatl benchmark exam­ ples in the literature, and some new examples involving parallel composition of actions, and actions that may or may not be executed. We prove that this logic extends a previous formalism, where sati 'lability for scenarios is NP-complete, and for which reasoning could be done in polynomial time in a fragment of the logic [Drakengren and Bjareland, 1997]. Although the polynomial class they characterize is nontrivial, its expressiveness is very limited. This also holds for the tractable fragments of the action description language A [Gelfond and Lifschitz, 1993], found by Liberatore [1997]. In that work, Libera­ tore showed that satisfiability of A is NP-complete, and Marcus Bjareland*

*This research has been supported in parts by the Swedish Research Council for Engineering Sciences (TFR), the Knut and Alice Wallenberg Foundation, and ASEA Brown Bovery (dept ISY / AMC).

1 This means that fluents are propositional.

Dept of Compand Info Science Linkoping U ni versi ty S-581 83 Linkoping, Sweden

marbj<Oida.liu.se

he provided an encoding of A into propositional logic in order to able to use e.g. GSAT. There seems to be no other analyses of computational complexity for sim­ ilar formalisms, for instance for the Situation Calculus [McCarthy and Hayes, 1969].

2 Overview

We will develop a logic for action and change in similar spirit as in Drakengren and Bjareland [1997] (henceforth, for convenience we shall denote this paper DB97) , i.e. we will define the syntax and semantics of a temporal propo­ sitionallo~ic (syntactically, but not sem~ntically rel~t~d to TPTL lAlur and Henzinger, 1989]) w1th the possibil­ ity of expressing time points as linear polynomials with rational coefficients. Then we introduce the notion of a scenario description, which is basically a set of for­ mulae in the temporal logic, and formulae that describe the change of fluent values over time. An interpreta­ tion of a scenario description is a function, which given a set of formulae yields the possibilities as to what com­ binations of changes are allowed by the set of formulae. For instance, a scenario description may allow either the combination of changes that the feature loaded and alive both are set to false at time 3, or the combination that gunnerSleeps is set to true at time 3. A model of a sce­ nario description is defined as an interpretation such that for some possible combination of changes, fluents change values iff they are explicitly stated to change by this com­ bination of changes. This way of defining interpretations enables us to (semantically) model composition of ac­ tions as operations on sets of combinations of changes, and to (syntactically) model them on the object-level. In fact, we will view every Boolean combination of changes as an object-level composition of separate actions, in an arbitrary number of levels. The basis case is then the change features, which are syntactical constructs that state that the value of one feature changes to true or false .

For the results regarding computation, the NP­ hardness of satisfiability in our logic is obvious, since we can encode propositional logic in it . NP-membership, on the other hand, is more tricky to prove: the obvi­ ous way of guessing an interpretation and a combina­ tion of changes and verifying that the interpretation is a model using this combination of changes in polyno­ mial time fails, since the set of combinations of changes can be exponentially large. Instead, we guess also how a combination of changes is obtained from the interpre­ tation, and this solves the problem. However, this proof technique fails if we introduce quantification over time points, which is used in approaches to ramification (see e.g. Gustafsson and Doherty [1996]).

3 Scenario Descriptions

This section defines syntax and semantics of the logic together with some illustrating examples.

3.1 Syntax

We begin by defining a slight (syntactical) extension of the temporal logic in DB97. What differs is that the binary operator V x for exclusive or is included, but it is straightforward to check that all relevant results of DB97 hold with this extension.

Definition 1 A signature is a tuple f7 = (T, F), where T is a finite set of time point variables and F is a finite set of propositional features . A time point expression is a linear polynomial over T with rational coefficients. We denote the set of time point expressions over T by T*. 0

Definition 2 Let f7 = (T, F) be a signature, let a, (3 E T *, f E F, R E {=,:S,<,2:, >}, EB E {A,V,Vx,-+,+-+}, and define the scenario description language ~ over f7 by ~ ::= T I F I f I aR(3 I ·~ I ~1 EB ~2 I [a]~.

A formula [ah expresses that at time a, 1 is true. The remaining connectives are standard (the notation for ex­ clusive or, Vx, is however nonstandard). Whenever we say "formula", we mean a formula in ~'for a given f7.

Let 1 be a formula. A feature f E :F occurs free in 1 iff it does not occur within the scope of a [a] expression in f. If no feature occurs free in /, 1 is closed.

The size of a set of formulae is the sum of the lengths of the formulae in the set. 0

We shall be informal with respect to specifying over what signature the language~ is defined, when it is clear what signature is intended.

In DB97 a special language for expressing action sce­ narios, extending the basic temporal logic, is defined. In this paper, we shall not need that; we just modify the semantics of the temporal logic, and identify a distin­ guished set of features which designate change of another feature. This is the natural generalisation of Sandewall's concept of occlusion, which in turn is equivalent to what is accomplished by a release statement in the language AR [Giunchiglia et al., 1997].

Definition 3 (Scenario description) Let f7 = (T , F ) be a signature, I~ :F, !::.. = { o(f, T), o(f, F) I f E F}, r7 1 = (T, :F u !::..) (that is, we consider o(f, T) and o(f, F) to be features themselves), and f a finite set of closed formulae over r7 1 · Then T = (r7, r, I) is said to be a scenario description. We will call features of the form o(f,T) and c5(f,F) change features . Given T, the set D. is denoted D.(T). 0

The set I consists of all fluents that are supposed to be inert, i.e. features that will not change value over time, unless explicitly stated. The fluents not in I are non-inert. Intuitively, the set !::.. of features is intended to model that the corresponding features in I can be subject to change, and remain unchanged otherwise.

We now present some examples in order to present some properties of our formalism, and to try to convince the reader that most propositional benchmark examples in the literature (see e.g. Sandewall [1994] for a list) can be represented.

Example 4 We take an example, the Russian Turkey Shoot (RTS), by Sandewall [1994], where we initially (at time point 0) assume that a turkey is alive, and that a gun is unloaded. Then we load the gun (at time point 1), spin the chamber (at 3), and fire the gun (between 4 and 5). The intended conclusion of this scenario is that we cannot prove that the turkey is alive, or dead, after the firing action has been executed. Semantically we want one model where the turkey is dead, and one where it is alive, after the execution of the firing action. We now formalise the scenario:

TRTS = ((0, {alive, loaded}), fRTS, {alive, loaded}), where {[OJ alive A ·loaded, [1 Jc5 (loaded, T), [3]o(loaded, T) V o(loaded, F), [4Jloaded-+ [5Jo(alive,F) A o(loaded,F)}.

0

Example 5 As an example of parallel composition we use the Balls and Boxes Scenario (BBS): We have two non-empty boxes on the ground, standing side by side. Our first action, a1 is to drop a ball between the boxes, so that it is unknown in which box the ball will end up. The second action, a2 , is to throw a ball into the left box. Initially both boxes are empty. We are interested in the case when both a1 and a2 happen. We use the features leftEmpty, and rightEmpty, which are true if the left, or the right box is empty, respectively.

fBoxes {[OJleftEmpty A rightEmpty, [t]c5( leftEmpty, F)V x o(rightEmpty, F), [t]o(leftEmpty, F)}.

The effect of both a1 and a2 happening, as described by the second and third formulae in the set above, as we will see below, will be

[t ]( o(lejtEmpty' F) v X o( rightEmpty, F)) A o(leftEmpty, F).

The intended conclusion is that either only the right box is empty, or both boxes are nonempty. We cannot get the second case by formulating the composite action in a straightforward manner in e.g. PMON 2 [Doherty, 1994], since is equivalent to

((·H(t, leftEmpty) Vx ·H(t, rightEmpty))/\ ·H(t, leftEmpty))/\ Occlude ( t, leftEmpty) 1\ Occlude ( t, rightEmpty) (·H(t, leftEmpty) 1\ H(t, rightEmpty))/\ Occlude(t, leftEmpty) 1\ Occlude(t, rightEmpty),

i.e. the box to the right will be empty. 0

Example 6 Finally, we model actions that may or may not be executed as [t](A V T), where A is decribes an action, and T the truth value true. When we define the semantics of scenario descriptions, the intuition behind this syntax will be clear. Logics like PMON will have similar problems with this construct, but for reasons of space, an example of that is omitted. 0

For an example with interactions between concurrently executed actions, see DB97 (which is the soup bowl lifting example of [Baral and Gelfond, 1997]).

3.2 Semantics

We now define the semantics of the temporal logic. The semantics will be directly defined in terms of scenario descriptions; note however that the semantics will be identical to the standard semantics of the basic temporal logic of DB97 if we set I = 0.

Definition 7 Let a = (7, :F) be a signature. A state over a is a function from F to the set {T, F} of truth values. A history over a is a function h from IR to the set of states. A valuation ¢ is a function from T to JR. It is extended in a natural way, giving e.g. ¢(3t + 4.3) = 3¢(t) +4.3. An interpretation over a is a tuple I= (h, ¢) where h is a history and ¢ is a valuation.

Similarly for a scenario description Y with signature a, I is an interpretation for Y iff I is an interpretation over a . 0

In ordinary logic, we use the notion of truth value for a formula in a model. Here we shall genereralise this, so that we instead obtain a set of possible combinations of changes, where an empty such set corresponds to F, and a nonempty set corresponds toT, but with possibly several alternatives for changes of actions (this is nonde­ terminism on the semanticallevel).

Definition 8 (Combination of changes, possible combinations of changes) Let Y = (a, r, I) be a scenario description, "f = 1\ r, and let I = (h, ¢) be an interpretation over a. A set e of tuples (t, J, T), where t E IR, f E I and T E {T, F} is said to be a combination of changes (one tuple therein is said to be a change), and a set E of such combinations is said to be a set o'f possible combinations of changes.

2 It seems that most other logics of action and change would have similar problems.

Given r, I and t, the set of possible combinations of changes of r in I for a time point t E IR, denoted I(r, t) , is a set E (note that this is a set of sets) of possible combinations of changes is defined below. For this we first need an auxiliary function condeff ( B, E), taking a truth value B and a set E of possible combinations of changes, returning E if B is true, and 0 otherwise.

Let f E F, R E {=,:=:;,<,;:::,>}, a.,(3 E /* , "f , E E I;, ffi E {/\, V, Vx, -+,++},and T E {T,F}. Now define

where the operators ·, 1\, V, V x, -+ and ++ on sets E1 , E2 of possible combinations of changes as follows.

Since the result of I does not depend on t when "f is closed, we can write I("f) in these cases. If I("f) =j:. 0, we say that "( is true in I.

With this definition of interpretations, it is clear that we model any Boolean combination of combinations of changes as composition. For example, disjunction is non-deterministic composition, and conjunction is par­ allel composition (with "parallel" here, we denote that the changes could possibly be simultaneous). However, note that negated change features (e.g. as antecedents in implication) do not affect the resulting set of combina­ tions of changes. For example, the formula [t]8(h, T) -+ 8(/2, T) is equivalent to T -+ 8(/2, T), since a negated change is interpreted to 0 or {0}: that is, we do not model that something should not change. This of course means that implication is causal and not material (see e.g. McCain and Turner [1995]).

Intuitively, we should interpret the empty set of possi­ ble combinations of changes so that there is no possible combination of effects that could have taken place, and the set containing only the empty set as its possible com­ bination of changes that the only possibility with respect to changes is that nothing changes. This is coherent with how the truth value is defined above.

We will briefly discuss how our three examples are inter­ preted:

• For RTS, the interesting part to interpret is the spin­ ning action, which yields:

Thus, we have three possibilities of change due to the spinning action, that loaded becomes true, that it becomes false, or that it becomes both true and false (this is, of course, impossible, and it is taken care of by the histories, as we will see below).

• For BBS, we focus on the composite action a1 1\ a2, i.e.

for which we get the following possible combinations of changes:

By definition of the operator V x on sets of possible combinations of changes, we get the following:

There are two possibilities: in the first combination of changes, only the right box will be empty, whereas in the second, both boxes are nonempty.

• For the "maybe" action, we note that

The resulting set will include {0}, which means that it is possible that the resulting action has no effects at all, which is what we intended.

Proposition 9 Let r be a set of formulae over a sig­ nature a containing no formulae of the type J(f, T) or J(f, F) . Then I is a model of r in the sense of DB97 iff I(1) =f. 0 for the scenario description 1 = (a, r, 0) .

Proof: An easy induction shows first that I('"y) E {0, {0} }, and then that 0 corresponds to F and {0} to T according to the definitions of DB97. 0

Finally, we need to code the fact that actions succeed, and inertia (the frame problem) into the formalism. This is done by identifying all time points where a feature f can possibly change its value, exactly as in DB97. Dur­ ing every interval where no such change time point exists, f has to have the same value throughout the interval.

When looking at the following definition, it is instruc­ tive to look at the corresponding definition in DB97.

Definition 10 Let 1 = (a, r, I) be a scenario descrip­ tion. A mode£" of 1 is an interpretation I = (h, ¢) for which there exists an e E I(r) such that

• for each f E I and s, t E lR with s < t such that for no t' E (s, t] (half-open interval) (t', j, r) E e holds (for some T E {T, F} ), we have h(t)(f) = h(s)(f)
• for each (t,f,r) E e, it holds that h(t)(f) = T.

Intuitively, this definition ensures that no change in the value of a feature occurs in an interval if nothing changes it explicitly, and all specified changes have effect. Note that e is always a finite set, so this definition makes sense 4 .

Denote by Mod(1) the set of all models for a scenario description 1.

A formula r E :E is entailed by a scenario description 1, denoted 1 l= r, iff r is true in all models of 1. 1 is satisfiable iff Mod (1) =f. 0. 0

Fact 11 If 1 = (a, r, I) is a scenario description and r E :E a formula, then 1 l:= r iff (a, r U { 'r }, I) is un­ satisfiable. 0

Next we establish that this formalism indeed subsumes that of DB97. An auxiliary result is needed 5 .

Definition 12 (Corresponding action formula) Let a be the action expression ¢ ::::7 [o:]'I/Jlnfl (in the sense of DB97). Then the formula

is said to be the action formula corresponding to a. 0

The subsumption result follows.

Proposition 13 Let 1' = (a, sco, OBS) be a scenario description in the sense of DB97, let A be the set of ac­ tion formlae corresponding to action expressions in sco, and define the scenario description 1 = (a, OBS U A, :F), where a = (7, :F). Then the set of models of 1' is iden­ tical to the set of models of 1 .

Proof: Just compare the definitions. 0

4 Complexity Results

The following result is easy.

Theorem 14 Deciding satisfiability of a scenario de­ scription is NP-hard.

Proof: NP-hardness follows, since we can express satis­ fiability of propositional logic formulae. 0

3 0ften, the term intended model is used for models of sce­ nario descriptions. However, it seems more philosophically correct to name it just model. We shall also name the in­ tended models in DB97 just models.

4 Infinite sets of changes could express open intervals of changes, which would require some more machinery to obtain a suitable definition.

5 Due to space limitations, we refer the reader to the orig­ inal paper instead of repeating the definitions here.

NP-membership, on the other hand, is more involved to prove. For instance, the obvious method of guessing a combination of changes and verifying that this set is a member of the set of possible combinations of changes, fails, since the set of sets can be exponentially large. We need some auxiliary notions.

Definition 15 Let r be a set of formulae. Then define time(f) to be the set of time point expressions used in r. Also, for a scenario description Y = (0', r,I), de­ fine time(Y) = time(r), and changes(Y) to be the set time(Y) x I x {T, F}.

Let I be an interpretation over 0' and suppose that e E I(Y). For each (t, f, r) E e, find an a E time(Y) such that I(a) = t (such an a always exists); collect these tuples (a, f, r) in the set U. Now let synteff be a function taking Y, I and e, returning such an U, that is, synteff(Y, I, e) = U (such a function clearly exists).

The function thus makes a syntactic representation of a set of changes, relative to a scenario description and an interpretation. Such a set is said to be a syntactic combination of changes. D

Next, we shall show how to represent an interpretation I in terms of a set of formulae.

Definition 16 (A(T), intrep) Let 0' = (T, F) be a signature, T ~ T*, and set A(T) = {[a]f, aR/3 I a, f3 E T,f E F,R E {<, :S,=, 2::,>}}.

Let I = (h, ¢)be an interpretation over 0'. Then define intrep(I, T) = {r E A(T) I I('y) =f:. 0}. Note that the sizes of A and thus intrep(I, T) are polynomial in the sizes of T and F. D

Thus intrep(I, T) represents the interpretation I, given that only the time point expressions in T are important.

Proposition 17 Verifying for an arbitrary subset B ~ A(T) whether B = intrep(I, T) for some I and T can be done in time polynomial in the size of A(T).

Proof: We use a result of DB97, saying that satisfiabil­ ity of a set of Horn formulae can be solved in polynomial time. For this proof, it is enough to know that formulae in A(T) and negations of such formulae are Horn formu­ lae.

Construct the set B' = B U { '/ II E A(T), 1 rf. B}. Now it is clear that B' has a model I iff B = intrep(I, T), and the result follows. D

Corollary 18 Let I be an interpretation over 0' = (T, F), T ~ T*, and let W = intrep(I, T). Then query­ ing whether I('y) =f:. 0 for 1 E A(T) can be done in time polynomial in the size of A(T).

Proof: Just check whether 1 E W. D

Definition 19 (Annotated formula) Let Y = (O",f,I) be a scenario description, 1 = 1\f, and let the formula 1' (which is never a member of~) be obtained from 1 by replacing every subformula f3 of 1 ( 1 is counted as a subformula of itself) by the expression (/3, E, a), for E ~ {e}, with some arbitrarily chosen e ~ changes(Y), and a E time(Y). Then 1' is said to be an annotated formula for Y. Note that the size of 1' is polynomial in the size of Y, and that 1 can always easily be recovered from 1'· Then we write 1 = unannotate('y'). D

Definition 20 (Syntactic scenario interpretation, syntactic scenario model) Let Y = (0', r, I ) be a scenario description, T = time(Y), Sa pair (W, 1'), with W ~ A(T) and 1' = (!, E, a) an annotated formula for Y. Then S is said to be a syntactic scenario interpreta­ tion for Y.

For the definition of a syntactic scenario model , we need an auxiliary definition: define the function condeff 5 (B, E) (a syntactic variant of the function condeff), taking a truth value B and a set E of pos­ sible syntactic combinations of changes, returning E if B is true, and 0 otherwise.

Furthermore, for a syntactic scenario interpretation S = (W, 1'), we define a predicate S on 1' as fol­ lows, letting EB E {A, V, Vx, --+, +-t }, R E { =, :::;, <, 2::, > }, a,/3 E T*, a,a',a;,/3 E T*, and T E {T,F} . F should be a previously unused variable.

where the operators ·, A, V, V x, --+ and +-t on sets E1 , E2 of possible syntactic combinations of changes are defined by

where the relation ~s is defined such that e1 ~s e2 iff for each (a, f, r) E e1 , there exists a (a', f, r) E e2 , with a = a' E W. The relation models inclusion of syntactic combinations of changes, taking into account which syn­ tactically differing time points are semantically equal. Note that this relation can be computed in polynomial time, due to our assumptions.

Now, if the following conditions hold, then S is said to be a syntactic scenario model of Y:

• W = intrep(I, T) for some interpretation I
• S({3) is true for every subformula {3 of 1'
• there exists an e E E such that
• for each (a, j, T) E e, [a]f E W {::} T
• for each f E I and a, {3 E time(Y) with a < {3 E W such that for no a' for which a< a',a' < {3 E W, (a',j,T) E e holds (for some T E {T, F} ), we have that [{J]f E W {::} [a] j E W.

It is clear that S can be computed in polynomial time, and_ similarly for the remaining checks, so checking wheter a syntactic scenario interpretation is a syntac­ tic scenario model can be-checked in polynomial time. 0

Theorem 21 Deciding satisfiability of a scenario de­ scription is NP-complete.

Proof (sketch): It remains to prove NP-membership, by Theorem 14. Now, we can use a syntactic scenario interpretation as a guess, and then verify whether it is a scenario model or not in polynomial time, by the previ­ ous results. The existence of a syntactical scenario model and the existence of a model of the scenario description can easily proved to be equivalent. 0

5 Discussion

We have expanded the expressivity boundaries for rea­ soning about action in NP time. This is a proof that a polynomial-time reduction exists to propositional logic, making stochastic search procedures like GSAT appli­ cable to the problem. The formalism presented here is clearly more expressive than e.g. A in all aspects ex­ cept that we do not have branching time (we can han­ dle explicit , continuous time, nondeterministic actions, "maybe" actions and so on), so the result that computa­ tional complexity of satisfiability in the two formalisms is equivalent is somewhat surprising. Then a question is: how much further can one go? Since there is no pre- · cise measure for expressivity, this is a difficult question. Moreover, some extensions of the logic presented in this paper will not prove to be NP-complete with the proof technique we have employed. A basic tool in the NP­ membership proof is to find a polynomially-sized rep­ resentation of an interpretation. Now, if would extend the logic to allow quantification over time points (which could represent causal rules), we could have a scenario description y = (u, r) {!}) where

This scenario description has uncountably many mod­ els, so the method of representing interpretations and changes in polynomial space will fail (there are only countably many representations of whatever needs to be represented). Thus, some new proof technique would have to be employed.

6 Conclusions

We have introduced a logic of action and change which is expressive in the sense that it can represent most propo­ sitional benchmark examples in the literature, and some new examples involving parallel composition of actions, and actions that may or may not be executed. We have proved that satisfiability of a scenario in this logic is NP­ complete, and that it subsumes an NP-complete logic introduced by Drakengren and Bjiireland [1997]