Reasoning about Action in Polynomial Time

1 Introduction

Although many formalisms for reasoning about action exist, surprisingly few approaches have taken computa­ tional complexity into consideration. One explanation for this might be that many interesting AI problems are (at least) NP-hard, and that tractable subproblems that are easily extracted, tend to lack expressiveness. This has led a large part of the AI community to rely on heuristics and incomplete systems to solve the problems (see e.g. [Ginsberg, 1996] for a discussion). This holds, in particular, for the area of reasoning about action, where the very expressive logical formalisms provide difficult obstacles when it comes to efficient implementation.

We feel, however, that the tractability boundary for sound and complete reasoning about action has not yet been satisfactorily investigated. We prove this by in­ troducing a nontrivial subset of a logic with semantics closely related to the trajectory semantics of Sandewall [1994], for which satisfiability is tractable. Our logic can handle examples involving not only nondeterminism, but continuous time, concurrency and memory of actions as well, thus providing a conceptual extension of Sande­ wall's framework. The reader should note that our main concern is computation, as opposed to modelling.

This paper is organised as follows: Section 2 is an informal overview of the technical results, where also two examples are presented. In Section 3 we present the syntax and semantics of the basic temporal logic and the extension for reasoning about action, and in Section 4, we present the following: three intractability results for these formalisms, and the main results: the tractable subclasses of the temporal logic and its extension 1 .

2 Overview

In Section 3 we develop a temporal logic, A, which is syntactically related to the propositional temporal logic TPTL [Alur and Henzinger, 1989]. The temporal do­ main is the set of real numbers and temporal expressions are based on relations=, ~' <, ~and > between linear polynomials with rational coefficients over a set of tem­ poral variables. The semantics of this temporal logic is standard. The formalism for reasoning about action is narrative based, which means that scenario descriptions are used to model the real world. Scenario descriptions consist of formulae in the temporal logic (observations) and action expressions which are constructs that state that certain changes in values of the features (proposi­ tions, fluents) may occur. We write action expressions as 1r ~ [a]t Infl, where 1r is the precondition for the action, t the effects, a a temporal expression denoting when the effects are taking place, and Infl is the set of all features that are influenced by the action. The in­ fluenced features are not subject to the assumption of inertia, i.e. we allow them, and only them, to change during the execution of the action.

It turns out that deciding satisfiability is NP-complete, both for the temporal logic and the scenario descriptions. Interestingly, the problem is NP-complete for scenario descriptions that only include Horn clause observations, unconditional and unary action expressions (this termi­ nology is explained later), and no stated relations be­ tween temporal expressions.

To extract a tractable subset from our formalism we rely on a recent result in temporal constraint reasoning by Jonsson and Backstrom in [1996] (also discovered in­ dependently by Koubarakis [1996]). They have identified a large tractable class of temporal constraint reasoning, using Horn Disjunctive Linear Relations (Horn DLR's)

1 Due to lack of space, proofs of most theorems are omit­ ted. However, they can all be obtained from the authors (until published) .

which are relations between linear polynomials with ra­ tional coefficients. We make use of their result by re­ stricting formulae in our scenario descriptions to be Horn and then by encoding scenario descriptions into Horn DLR's. For the temporal logic this is fairly straightfor­ ward. For the scenario descriptions, it turns out that we have to put some constraints on the temporal relations and actions in the scenario descriptions.

We will use the following two examples: Jump into a Lake with a Hat [Giunchiglia and Lifschitz, 1995] and Soup Bowl Lifting [Gelfond et al., 1991]. Below we in­ formally describe the examples.

Example 1 (Jump into a Lake with a Hat, JLH) If you jump into the lake you will get wet . If you have been in the water at some time point it is unclear if you still have your hat on. This is an example of nondeterminism and of memory of actions. 0

Example 2 (Soup Bowl Lifting, SBL) If we lift ei­ ther side of a soup bowl at some time points, the content will be spilled, unless we lift both sides at the same time point. This is an example of simultaneous concurrency. 0

Both examples stated above can be handled by the tractable subset of our formalism. Note that we are not confined to simultaneous concurrency; actions may partly overlap.

3 Scenario Descriptions

We introduce a semantics that is a simpler variant of Sandewall's Features and Fluents Framework [Sande­ wall, 1994], in that the effects of an action can only occur at one and the same time point for a given action, and we use only propositional values of features (similar to the work of Doherty [1994]) However, in some respects this formalism is more flexible than Sandewall's: we use a continuous time domain, we allow concurrently execut­ ing actions, and effects of actions can depend on other states in the history than the state at the starting time point of the action (this implies memory of actions, in Sandewall's [1994] terminology). One example of a for­ malism having memory is that of Gustafsson and Do­ herty [1996].

Initially, a basic temporal logic is defined. The compu­ tational properties of this logic will be exploited by the scenario description logic, i.e. ultimately (in Section 4) the scenario descriptions will be transformed into formu­ lae of the basic temporal logic.

3.1 Syntax

We begin by defining the basic temporal logic.

We assume that we have a set T of time point vari­ ables intended to take real values, and a set :F of features intended to take propositional values.

Definition 3 A signature is a tuple u = (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 overT with rational coefficients. We denote the set of time point expressions over T by T*. 0

Definition 4 Let u = (T, :F) be a signature, let a, f3 E T* , f E :F, R E { =, ~, <, 2:, >}, EB E {A, V, --+, ...... } , and define the scenario description language A over u by

A formula that does not contain any connectives (any of the constructs A, V, --+, ...... , ..., and [·]) is atomic. If; is atomic and a E T*, then the formulae ;, [a];, ·;, [a]·; and ·[a]; are literals. (A formula [a]; expresses that at time a, 1 is true.) A literal I is negative iff it contains ..., and its corresponding atomic formula ; is not of the form aR/3 for R E { <, ~' >, 2:}. A literal that is not negative is positive. Disjunctions of literals are clauses. A formula ; E A is in conjunctive normal form, CNF, iff it is a conjunction of clauses. A formula; is Horn iff it is a clause with at most one positive literal. A set f of formulae is Horn iff every 1 E f is Horn. Syntactical identity between formulae is written =:, and when ambiguity is to be avoided, we denote formulae 1 E A by '1,·

Let 1 be a formula. A feature f E :F occurs free in ; iff it does not occur within the scope of a [a] expression in f. a E T* binds f in ; if a formula [a]¢ occurs as a subformula of 1, and f is free in ¢ . If no feature occurs free in 1, 1 is closed. If 1 does not contain any occurrence of [a] for some a E T*, then 1 is propositional. 0

Using A, we can thus express propositions being true at time points, and express relations between time points. Next we define the extension of the basic temporal logic by introducing action expressions, i.e. constructs that enable modelling of change.

Definition 5 Let u = (T, :F) be a signature. An action expression over u is a tuple A= (a, 1r, Infl, t), a E T*, 1r a closed formula in A, Infl ~ F, and fa propositional formula, where all features occurring in f are in Infl. a is the result time point of A, 1r is the precondition of A, Infl is the set of influenced features of A, and f is the effects of A. A is unconditional iff 1r = T, and unary iff IInfll = 1.

For convenience, we write action expressions as 1r ~ [a]f Infl; for example we have [3]/oaded ~ [4]·alive{ alive} for an action shoot. If 1r = T, we remove it and the ~ symbol, and if f = T, we re­ move it. An example is an unconditional loading action [2]/oaded{ loaded}, and the action of spinning the cham­ ber of a gun [3] {loaded} .

An observation over u is a closed formula in A. 0

Next, we combine the concepts defined so far into one.

Definition 6 A scenario description is a tuple 1 = (u, sen, OBS), where u = (T, :F) is a signature, sen (the schedule) is a finite set of action expressions over u, and OBS is a finite set of observations over u . The size of a scenario description is defined as the sum of lengths of all formulae in sen and OBS. 0

Now, we formalise the examples from Section 2.

Example 7 ( JLH) The intended conclusion of the fol­ lowing scenario is that the person is wet at time c1 , and we do not know if the hat is on at time point c2 , occur­ ring after the person jumps.

OBSl [O]haLon 1\ dry 1\ on_land

scol [ci]·onJand{ onJand} sco2 [c1]·onJand ~ [c1]·dry{dry} sco3 [c1]·onJand ~ [c2]{haLon} OBS4 C1 2: 0 1\ c2 2: C1 0

Example 8 (SBL) We have two actions: one for lift­ ing the left side of the soup bowl and one for lifting the right side. Ifthe actions are not executed simultaneously, the table cloth will no longer be dry. The intended con­ clusion here, is that c2 = c1.

3.2 Semantics

For the presentation of the semantics we proceed sim­ ilarly to the presentation of the syntax. We begin by defining the semantics of the basic temporal logic.

Definition 9 Let u = (T, :F} be a signature. A state over u is a function from :F to the set {T, F} of truth values. A history over u is a function h from R to the set of states. A valuation ¢; is a function from T to R. It is extended in a natural way (as a homomorphism from T* to R), giving e.g. ¢;(3t + 4.3) = 3cf;(t) + 4.3. A development, or interpretation, over u is a tuple (h, ¢;} where h is a history and ¢; is a valuation. D

Definition 10 Let 1 E A, and let D = (h, ¢;} be a de­ velopment. Define the truth value of 1 in D for a time point t E R, denoted D(!, t), as follows (here we overload T and F to denote both formulae and truth values). As­ sume f E :F, R E {=,::;,<,2:,>}, 01,/3 E T*, 1,6 E A, EB E {/\, V, ...... , -},andrE {T,F}. Now define

D(r, t) = r D(f, t) = h(t)(f)

D(01Rj3, t) = cf;(01)Rcf;(j3)

D( '/, t) = ·D( /, t)

D(! EB 6, t) = D(!, t) EB D(6, t) D([01]!, t) = D(!, c/;(01)).

Two formulae 11 and 12 are equivalent iff D( 11 , t) = D(12 , t) for all D and t. A set f ~ A of formulae is satisfiable iff there exists a development D and a time point t E R such that D( 1, t) is true for every 1 E f. A development D is a model of a set r ~ A of closed formulae iff D( 1, t) is true for every t E R and 1 E r. D

Fact 11 For 1 E A and 01 E T*, ·[01]1 is equivalent to [01]·1. For a closed formula/, D(1,t) = D(1,t') for any t, t' E R and development D. D

Thus, if 1 is closed, we can write D( 1) instead of D( /, t). Now we define the semantics of the action expressions based on models for the basic temporal logic. Inertia (the frame problem) is handled by identifying all time points where a feature f possibly can change its value.

Then during every interval where no such change time point exists, f has to have the same value throughout the interval.

Definition 12 Let D = (h, ¢;} be a development. An action expression A= (01,7r,Infl,t} has effects in D iff D(1r) = T. Let f E :F, and define Chg(D, sen,/, t) to be true for a time point t E R iff f E Infl for some action expression A = (01, 1r, Infl, t} E SCD that has effects in D, with c/;(01) = t. Note that we can only have Chg(D, sen,/, t) true for a finite number of time points for fixed sen and f.

Let 1 = (u, sen, OBS} be a scenario description. An intended model of 1 is a development D = (h, ¢;} where

• D is a model of OBS
• For each A = (01, 1r, Infl, t} E sen that has effects in D, D(t, c/;(01)) = T
• For each f E :F and s, t E R with s < t such that for not' E (s, t) (open interval), Chg(D, SCD, f, t') holds, we have h(t')(f) = h(s)(f) for every t' E (s, t).

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

A formula 1 E A is entailed by a scenario description 1, denoted 1 f= /,iff 1 is true in all intended models of 1. 1 is satisfiable iff Mod(!) f; 0. D

Fact 13 If 1 = (u, sen, OBS} is a scenario description and 1 E A a formula, then 1 f= 1 iff (u, sen, OBS U { '/}} is unsatisfiable. D

We comment how this is used in our two examples:

• It is intended that JLH is unsatisfiable adding the observation [cl]dry, and that neither adding [c2]haLon nor [c2]·haLon will make it unsatisfi­ able.
• For SBL, adding c2 f; c1 as an observation will make the scenario unsatisfiable.

4 Complexity Results

4.1 Basic Results

It is no surprise that deciding satisfiability for the basic temporal logic is NP-hard. Proofs of NP-completeness, on the other hand, depend on the tractability results.

Proposition 14 Deciding satisfiability of a set r ~ A is NP-hard.

Proof: Propositional logic is a subset of A. D

Corollary 15 Deciding whether a scenario description is satisfiable is NP-hard. D

That these problems are in NP, and thus are NP­ complete, is proved in Theorem 22 and Theorem 23.

Interestingly, we can strengthen the result consider­ ably.

Theorem 16 Deciding whether a scenario description is satisfiable is NP-hard, even if action expressions are unconditional and unary, only Horn observations are al­ lowed, and no relations between time points may be stated.

Proof (sketch): A reduction from 3SAT. 0

We now present the key to tractability, which is a linear­ programming approach to temporal constraint reason­ ing, by Jonsson and Backstrom [1996] .

Definition 17 Let a and f3 be linear polynomials with rational coefficients over some set X of variables. Then a disjunctive linear relation, DLR, is a disjunction of one or more expressions of the form a = /3, a # /3, a ~ /3, a < /3. A DLR is Horn iff it contains at most one disjunct with the relation=, < or ~ ·

An assigment m of variables in X to real numbers is a model of a set r of DLR's iff all formulae in r are true when taking the values of variables in the DLR's. A set of DLR's is satisfiable iff it has a model. 0

The following result is the main result of Jonsson and Backstrom [1996].

Proposition 18 Deciding satisfiability of a set of Horn DLR's is polynomial. 0

Now we restrict the scenario description language and the form of actions. Furthermore, a structural restriction on scenario descriptions, verifiable in polynomial time, is imposed. We shall define an encoding function that takes a Horn scenario description T and returns a set r of Horn DLR's such that f is satisfiable iff T is satisfiable.

4.2 Satisfiability of Horn Formulae is Tractable

First, we code Horn formulae as Horn DLR's.

Definition 19 Let I be a closed literal, and assume the existence offresh, unique time point variables t'} for each f E :F and a E T*. Then C(/) is defined as follows, as­

suming R E {=, ~~ <,~~>}and f E :F.

Let 1 E A be a closed Horn formula, and let 1' be ob­ tained from 1 by simplifying away occurrences of T .and F. Now 1' = V; I; . Then define C(1) to be the DLR 8 = V; C(/;). Note that 8 is always a Horn DLR:

Let r ~ A be a set of closed Horn formulae, and T the set of all time point expressions occurring in r. Then C(f) is defined by

The second set is called the correspondence equations. Note that the argument of C in a correspondence equa­ tion is equivalent to [a]f 1\ f3 = a--+ [/3]/. 0

The following result is crucial.

Theorem 20 Let r c A be a set of closed Horn formu­ lae. Then r is satisfiable iff C(f) is satisfiable.

Proof (sketch): Straightforward: the key is to use the correspondence equations. 0

Corollary 21 Deciding satisfiability of sets of closed Horn formulae is polynomial.

Proof: It is clear that the transformation C is polyno­ mial. The result follows from Proposition 18. 0

Now we have the results for the proofs of membership in NP for the satisfiability problems of A and of scenario descriptions.

Theorem 22 Deciding satisfiability of a set r ~ A is NP-complete.

Proof (sketch): By Proposition 14, it remains to prove that the problem is in NP. This is done by letting the set of all literals used in r which are true in a model serve as a polynomial representation of the model. Furthermore, satisfiability of such a set is polynomial, by Corollary 21. 0

Theorem 23 Deciding whether a scenario description is satisfiable is NP-complete.

Proof (sketch): By Corollary 15, it remains to prove that the problem is in NP. As a polynomial representa­ tion of a model, we use the set of literals used in the scenario description that are true in it, and additional atomic formulae expressing temporal relations. Then checking satisfiability of such sets will be polynomial, like in Theorem 22. 0

4.3 Tractable Scenario Descriptions

Using Corollary 21, we see that if we can code scenario descriptions into sets of Horn formulae, we will have a polynomial algorithm for reasoning with scenario de­ scriptions. In order to obtain such a result, we need to restrict what scenario descriptions are allowed.

The strategy can briefly be described as follows: we identify all observation time points which bind a feature value and all time points where an action expression pos­ sibly can change a feature value. Then we connect bound literals with biconditionals, between time points where the literal value should not change. E.g. if some action expression changes the value of the feature f at time point a, there exists a 1 E OBS which binds f at a time point /3, a < /3, and no changes of the value off occurs between a and /3, then [a]f +-+ [/3]! should be added to the theory. This formula can be rewritten in Horn form. The example represents one of the six cases (case 3). The other cases are similar.

The restrictions are basically two: First we will have to represent action expressions as Horn formulae (restricted action expressions). Second, the scenario descriptions must be ordered, we could, e.g., not remove the restric­ tion a < f3 in the example above.

Definition 24 Let T (u, SCD, oss) be a scenario description. For each f E :F, define Ej {al(a,1l',Infl,f) E SCD 1\ f E Infl} and c, = {ala binds f in 111 E 0}, for 0 = OBS U

{1rl(a', 1r, Infl, t-} E SCD }. EJ is ordered iff for a, f3 E Ej, exactly one of a < /3, a = f3 and a > f3 is consistent with 2 OBS. For a,/3 E E1, E1 ordered, we define a -<1 f3 iff a < f3 is consistent with OBS, -oo -<1 a iff for no {3 E Ej, f3 < a is consistent with OBS, and a -<1 oo iff for no f3 E EJ, a < f3 is consistent with OBS .

Let a E EJ, f3 E T*, and define a <t:.1 f3 iff a ~ f3 is consistent with oss, a > f3 is inconsistent with oss, and for every 'Y E E 1, a < 'Y ~ f3 is inconsistent with OBS. Also define -oo <t:.1 f3 iff for every a E E1 a ~ f3 is inconsistent with OBS.

If for all f E :F, Ej is ordered, and for all w E CJ, a <t:.1 w for some a E E 1 U { -oo}, then T is ordered. The last condition says that for each observation of a feature / , there is a unique change of f which sets its value, or it precedes all changes of f. 0

Proposition 25 Testing if a scenario description T is ordered is polynomial, if OBS is Horn. 0

Definition 26 Let A = (a, 1r, Infl, c} be an action ex­ pression. Then A is restricted iff either of the following holds:

• 1r is T and E is a conjunction of propositional Horn formulae
• 1r is a disjunction of negative literals, and E is either T, or a conjunction of negative literals.

An ordered scenario description T = (a, sco, oss} is re­ stricted iff every action expression in seD is restricted and OBS is Horn. A restricted scenario description is normal iff it is ordered, and for every action expression A E sco, the following holds:

• 1r is T and E is a propositional Horn formula
• 1r is a negative literal and E is either T or a negative literal.

0

Both the examples previously stated (Example 7 and Example 8) are restricted, which is easy to verify.

The following result will make the forthcoming proofs easier.

Proposition 27 Let T be a restricted scenario descrip­ tion. Then we can in polynomial time construct an equivalent normal scenario description T'.

Proof (sketch): It is easy to replace the action ex­ pressions of T by normal action expressions which are equivalent. 0

Thus, we can assume that our restricted scenario de­ scriptions are normal. Next, we define the function <I> which transforms scenario descriptions into sets of Horn formulae.

Definition 28 First let A= (a, 1r, Infl, c} be a normal action expression. We have three cases for <I>:

• If 7r = T and E = h for h = V; I; propositional Horn, then define <I>(A) = {V;[a]l;}

2 A formula -y is consistent with a set f iff r u { -y} is sat­ isfiable.

• If 1r = ...,[ and E = T, then define <I>(A) = 0
• If 1r = ...,[ and E = ...,m, then define <I>(A) {/V [a]-,m}.

The restriction to normal action expressions should be clear; it implies that <I>( A) is Horn. For a set S of action expressions, define <I>(S) = UAEs <I>(A).

Let T = (a, SCD, oss} be a restricted scenario descrip­ tion with a = (T, :F}, and without loss of generality, assume that each feature in :F occurs in SCD or OBS. Also let b be a fresh time point variable (b standing for "beginning"), and for each f E :F, add a new feature f'. A few construction steps (basically corresponding to the possible relations between time points in E1 and C1) are necessary. We provide the intuitions of the constructions

in connection to them.

1. f1 = OBS U <l>(sco) U {b <alaE EJ U Cj, f E :F}.

The observations, the transformed action expressions, and an initial time point, are added.

2. f2 = {...,[a]/ V [b]/, [a]f V -,[blfl/ E :F, a E Cj,-OO<t:.J a}.

No action expression influences f before a where it is bound by an observation, therefore f should have the same value at b as at a . Note that the members of f2 can be rewritten to [a]f +-+ [b]f .

3. f3 = {-,[a]/ V [/3]/, [a]/ V ...,[/3]/1/ E :F, a E EJ, f3 E c,, a <t:.1 !3}.

f is influenced at a and bound by an observation at a later time point /3. No actions have effects between a and /3, therefore f should have the same value at f3 as it had at a.

4. f 4 = {-,[a]/' V [b]/, [a]/' V -,[blfl/ E :F, a E Ef, -oo -<1 a}.

This case resembles case 2, with the difference that f is influenced at a. Therefore, we introduce a new feature symbol f' which has the same value at a as f has at b. The new symbols will be handled properly below, in case 6.

5. fs = {-,[a]/ V [/3]/', [a]/ V ...,[/3]/'1/ E :F, a, f3 E EJ,a -<1 /3}.

This relates to case 3, as case 4 relates to case 2.

6. Since E 1 is ordered, we can form equivalence classes T/ of time points for a E E1 by

T/ = {/3 E E1la = f3 is consistent with OBS} .

For each a E E 1, define

P'f = {7rl(/3, 1r, Infl, c} E SCD 1\ f E Infl/\ f3 E T/}­ Now set f6 =

{VPj V -,[a]/V [a]/', VPj V -,[a]f' V [alfla E E1 }.

First note that this set is equivalent to the set {..., VP'f --+([a]/+-+ [a]f')la E EJ }.

Here we ensure that when actions do not have effects, f will have the same value as it had the last time it was changed. This value is held by the feature f'.

Now set <I>(T) = U; f; . It is clear that the transfor­ mation performed by <I> is polynomial. 0

Theorem 29 Let T be a restricted scenario description, and set r = C(<I>(T)). Then T is satisfiable iff f is satisfiable.

Proof (sketch): The key is that the sets f; force features to have values being satisfied in any intended model, and vice versa. 0

Theorem 30 Deciding satisfiability (and entailment) for restricted scenario descriptions is polynomial. 0

5 Discussion

One piece of related work is the approach by Schwalb et al. [1994] to reasoning about propositions being true at time points. Their choice for obtaining an algorithm is to code both propositions and temporal relations into propositional logic, whereas we do the opposite. How­ ever, their tractable inference algorithm is not complete, and they define no measure on when the correct infer­ ences will be obtained, so it is very difficult to relate it to our approach. Furthermore they cannot handle inertia adequately: there, propositions may always change when actions are performed, but certainly this is undesirable if actions which do not affect all features are used.

In this paper our concern has been computational complexity for reasoning about action. It is important to note that although we have provided polynomial al­ gorithms for the reasoning tasks, these can hardly be considered efficient. The important results, however, are that there exist polynomial algorithms; the next obvious step is to also make them fast. For efficient implementation, there is one direction we are partic­ ularly interested in investigating: since the technique used for achieving tractability can be described as an encoding of our logic as temporal constraints for which there is a tractable algorithm for determining satisfi­ ability, it should be possible to do something similar for other tractable temporal algebras, for example those identified in the papers [Drakengren and Jonsson, 1996; 1997]. Also, an algorithm for a purely qualitative sce­ nario description language (i .e. not involving metric time) would probably have a faster satisfiability-checker.

We have shown that satisfiability of scenario descrip­ tions is NP-complete within our formalism. We feel that it would be a mistake to interpret this negatively. On the contrary, one could argue (in lines with [Gottlob, 1996]) that this would imply that many approximations, powerful heuristics and non-trivial tractable subsets of problems for reasoning about action remain to be found . This paper is a step on the way in this endeavour.

6 Conclusions

We have presented a temporal logic and an extension for reasoning about action from which tractable subsets have been extracted. This has been done with an en­ coding of the logic to Horn DLR's. The formalism is narrative based with continuous time, and the world is modelled with scenario descriptions consisting of action expressions and observations. It is possible to model nondeterminism, concurrency and memory of actions. Time is represented with linear polynomials with ratio­ nal coefficients over real valued variables.

Acknowledgements

Thanks to Simin Nadjm-Tehrani, Peter Jonsson, Patrick Doherty, Lars Karlsson and Erik Sandewall for help and comments.