Representing Concurrent Actions in Extended Logic Programming

1 Introduction

Gelfond and Lifschitz [3] introduce a declarative lan­ guage A for describing effects of actions and define the semantics of this language based on the notion of a finite automata. The simplicity of the language and its seman­ tics makes it easier to describe the ontology of actions and contributes to establishing correctness (and some­ times completeness) of various logical formalizations of their effects. In particular, a theory of action stated in a language of extended logic programs(ELP's) [2] was described in [3] as a translation from a subset of A and proven to be sound w.r.t. the automata based seman­ tics. Soundness and completeness w.r .t . this semantics of the approaches to formalizing actions proposed earlier by Pednault [11], Reiter [13] and Baker [1] was recently proved by Kartha [5] .

Although the language A is adequate for formalizing several interesting domains, its expressive power is rather limited. In particular, every action is assumed to be ex­ ecutable in any situation and only one action can be performed at a time. In this paper we expand the syn­ tax and semantics of A to remove these limitations and to allow for a representation of concurrent actions. As in [3], we translate theories in the resulting language Ac into ELP's and prove correctness of this translation. The translation can be viewed as a logic programming coun­ terpart of situation calculus [9] and is interesting in its own right. The paper is organized as follows: In section two we define the syntax and semantics of the language Ac. Section three describes the translation of theories from Ac into ELP's while section four illustrates the translation by the way of examples. Due to space lim­ itations the proof of correctness of the translation and other results will be presented in the full paper.

2 A language Ac

2.1 Syntax

First let us recall the syntax of language A from [3]. The alphabet of A consists of two disjoint nonempty sets E1 and E2 of symbols, called fluent names and action names. A fluent literal is a fluent name possibly preceded by ...,, A v-proposition is an expression of the form

where F is a fluent literal, and A1, ... , Am (m ~ 0) are action names. If m = 0, (1) is written as

initially F.

An e-proposition is an expression of the form

where A is an action name, and each of F, P1 , ... , Pn ( n ~ 0) is a fluent literal. P1 , ... , Pn are called precon­ ditions of (2). If n = 0, we write this proposition as

A causes F.

A domain description in A is a set of propositions.

The syntax of Ac differ from the syntax of A only in the definition of action names. By an action name of Ac we mean an arbitrary finite set { a1, .. . , an} of elements of E2. Intuitively, an action name {ai} denotes a unit action while an action name A= {a1, .. . , an} where n > 1 denotes a compound action- a set of unit actions which are performed concurrently and which start and stop cotemporaneously. For simplicity we will often identify a unit action name {a;} with a; . To illustrate the notion of a domain description in Ac let us consider the following examples from l4]:

Example 1. Mary is lifting a bowl of soup from the kitchen table, while John is opening the door to the din­ ing room.

To represent this story in Ac let us consider an alpha­ bet consisting of a fluent name Lifted and Opened and two unit actions Lift and Open . The initial situation is described by v-propositions:

initially -.Lifted

The effects of the actions can be described by the axioms:

The resulting domain description will be denoted by Dt. Intuitively, the effects of the two actions of Dt are com­ pletely independent and so both Lifted and Opened should hold after the execution of the compound ac­ tion {Lift, Open}. The next example describes actions whose effects are mutually dependent.

Example 2. Whenever Mary tries to lift the bowl with one hand, she spills the soup. When she uses both hands, she does not spill the soup.

This time let us consider an alphabet consisting of a flu­ ent name Spilled and two unit actions LifU and LifLr. The initial situation may be described by a proposition:

initially-. Spilled

and the effects of actions are represented by propositions:

{LifU} causes Spilled

{ LifLr} causes Spilled

{ LifU, Lift_r} causes ..., Spilled

The resulting domain description will be denoted by D2 .

2.2 Semantics

To describe the semantics of Ac, we will define "models" of a domain description, and when a v-proposition is "true" in a model. If a v-proposition P is true in all models of a domain description D, we say that D entails P. As defined in [3], a state is a set of fluent names; given a fluent name F and a state u, we say that F holds in u ifF E u; ·F holds in u ifF ~ u .

A transition function is a mapping <I> of a subset of the set of pairs (A, u), where A is an action name and u is a state, into the set of states.t As in [3], a structure is a pair (u0 , <I>), where uo is a state (the initial state of the structure), and <I> is a transition function. We say that a sequence of action names At, ... , Am is executable in a structure M = ( uo, <I>) if for every 1 ~ k ~ m

is defined. The resulting state will be denoted by M(At , ... ,Am)

We say that a v-proposition (1) is true (false) in a struc­ ture M if

1. At, ... , Am is executable in M,

2. F holds (does not hold) in M(A., ... ,Am).

In particular, the proposition "initially F" is true in M iff F holds in the initial state of M.

1 Recall that in the definition of a transition function in the semantics of A, <I> must be defined on the set of all such pairs.

We say that execution of an action A in a state u immediately causes a fluent literal F if

There is an e-proposition "A causes F if Pt, ... , Pn" from the domain D such that for every i, 1 ~ i ~ n, Pi holds in u.

We say that execution of an action A in a state u causes a fluent literal F if

1. A immediately causes F, or

2. There is a B ~ A, such that execution of B in u immediately causes F and there is no C such that B C C ~A where execution of C in u causes -.F.

Let A be an action and u be a state and consider:

BJ(A, u) = {! : f is a fluent name and execution of A in u causes !} ,

Bj(A, u) = {f : f is a fluent name and execution of A in u causes -.f } .

A structure (uo , <I>) will be called a model of a domain description D if the following conditions are satisfied:

1. Every v-proposition from D is true in ( u0 , <I>);

2. For every action A = {at, ... , an} and every state u

• (i) if BJ(A, u) n Bj(A, u) = 0 then <I>(A, u) is defined and

(ii) otherwise <I>( A, u) is undefined.

It is clear that there can be at most one transition func­ tion <I> satisfying conditions (i)-(ii) . Consequently, dif­ ferent models of the same domain description can differ only by their initial states.

Example 3. Consider the domain description Dt from Example 1, the initial state u0 = 0 and the transition function <I> defined as follows :

It is easy to see that the structure ( uo, <I>) is the only model of the domain description Dt and therefore Dt entails v-propositions Opened after {Open , Lift} and Lifted after {Open, Lift} .

Example 4. Consider a domain description D3 con­ taining three unit actions Paint, Close and Open, and two fluents, Opened and Painted. The effects of these actions are defined by the following e-propositions:

Close causes -.Opened

Open causes Opened

Paint causes Painted.

Let a transition function <I> be defined as follows:

Notice, that for a pair (A, u) where u is an arbitrary state and A = {Open, Close} or A = {Open, Close, Paint}, ifl is undefined.

It is easy to see that any structure { u, ifl} where u C {Opened, Painted} is a model of D3 and that D3 has no other models.

A domain description is consistent if it has a model, and complete if it has exactly one model. For instance, do­ main descriptions D1 and D3 from Examples 1 and 4 are consistent, D1 is complete, and a domain description containing the v-propositions initially F and initially -.F is inconsistent.

It is interesting to compare a new semantics with that defined in [3] . The comparison of course is only pos­ sible for the domain descriptions not containing names for compound actions. But, as demonstrated by the fol­ lowing example, even in this case the new semantics is somewhat more powerful than the old one.

Example 5. Consider a domain description D4 con­ taining an action name A, a fluent name F and two e-propositions

A causes F A causes -,p

According to the semantics from [3] D is inconsistent while it is easy to check that M = (0, ifl) where ifl(0, u) = u is a model of D.

The following proposition shows that for descriptions consistent in the sense of [3] both semantics coincide. Models of D in the sense of [3] will be called s-models.

Proposition 1. Let D be a domain description not containing compound actions and assume that D has an s-model. Let M = ( u, ifl) be a structure of M, and M* = ( u, ifl*) where ifl* is ifl restricted to unit actions.

Then M is a model of F iff M* is an s-model of D and for every s-model N of D there is a model M of D such that N = M*. 0

3 From Ac to Extended Logic Programs

3.1 Extended Logic Programs

Extended logic programs were introduced in [2] (see also [10]) as a tool for reasoning in the presence of incomplete information. They are defined as collections of rules of the form

where each Li is a literal, i.e. an atom possibly preceded by -., and not is the negation as failure. Intuitively the rule can be read as: if £1 , ... , Lm are believed and it is not true that Lm+l, ... , Ln are believed then Lo is be­ lieved. A program determines a collection of answer sets - sets of ground literals representing possible beliefs of the program. A program is consistent if it has an an­ swer set not containing contradictory literals. A ground literal L is entailed by an ELP if it belongs to all of its answer sets. The rules of ELP's can be identified with defaults [12]

(L stands for the literal complementary to L.) As was shown in [2] a literal L is entailed by a program II iff it belongs to all extensions of the corresponding default theory.

In our further discussion we will need the following sim­ ple Lemma aboui ELP's:

Lemma 1. For any answer set A of an ELP II :

• (a) For any ground instance of rule from II, if {£1 , ... , Lm} ~A and

(b) If A is consistent and £0 E A then there ex­ ist a ground instance of a rule from II such that {£1, ... ,Lm} ~A and {Lm+l, .. . ,Ln} nA = 0.

3.2 The translation 1r

In this section we describe the translation 1r from domain descriptions to ELP's and prove the soundness of this translation.

The ELP 1r D, corresponding to a domain descrip­ tion D, uses variables of three sorts: situation variables s , s', . . . , fluent variables /, f', .. . , and action variables a, a', . . . 2 . We also need a sort for fluent literals whose terms are of the form For F where F is a term of the type fluent . Its language includes the situation constant So , and the fluent names and action names of D, that be­ come object constants of the corresponding sorts. There are also some predicate and function symbols; their sorts will be clear from their use in the rules below. Of special importance is a function symbol {} which will be used to form terms of the action type and a function result used to form the terms of the type situation.

The program 1r D will consist of the translations of the individual propositions from D along with other axioms.

1. Inertia Axioms:

2 Using a sorted language implies, that all atoms in the program are formed in accordance with the syntax of sorted predicate logic. Moreover, when we speak of an instance of a rule, we assume that the terms substituted for variables are of the appropriate sorts.

These rules are motivated by the "commonsense law of inertia," according to which fluents normally are not changed by actions. The rules l(a) allow us to apply the law of inertia in reasoning ''from the past to the future" : The first-when a fluent is known to be true in the past, and the second-when it is known to be false. The rules l(b) play the same role for reasoning "from the future to the past." The auxiliary predicate Noninert is essen­ tially an "abnormality predicate" [8]. The axioms differ from those suggested in [3] only in the use of predicate "atomic" to restrict the inertia rules to unit actions.

2. Translating v-propositions:

The translation of a v-proposition "F after A1 , ... , Am" 1S

where [A1, ... , Am] stands for the ground term

Result(Am, Result(Am-1, ... , Result(A1, So) ... )).

3. Translating e-propositions:

The translation of an e-proposition "A causes F if P1, ... , Pn" consists of the rules:

• (a) Effect Axiom:

It allows us to prove that F will hold after A, if the preconditions are satisfied.

• (b) Cancellation axiom for inertia:

Holds(P;, s) is a literal complementary to Holds(P;, s) . For any fluent F, IFI = F and I...,FI =F.

The rule disables the inertia rules (1) in the cases when F can be affected by A.

• (c) Forward Reasoning Axioms:

The above rules justify the following form of reasoning: If the value ofF has changed after performing A, then we can conclude that the preconditions were satisfied when A was performed.

• ( d)Backward Reasoning Axioms:

The above rules allow us to conclude that a precon­ dition was false from the fact that performing an action did not lead to the result described by an effect axiom, and all other preconditions were true.

The axioms above differ from those suggested in [3] only by allowing terms for compound actions. The next ax­ ioms are new. They describe how the effects of indi­ vidual actions are related to the effects of these actions performed concurrently.

4. Inheritance axioms:

• (a) Holds(f,Result(a,s)) +- subsetof(b,a), H olds(f, Result(b, s )), not Non inherit(!, a, b, s)

where Non inherit( e, a, b, s) means "action a does not inherit fluent literal e from subaction b in situation s." According to these axioms compound actions normally inherit the effects of their components.

The next collection of axioms is concerned with can­ cellation of Inheritance axiom. For every e-proposition A causes F if P1, .. . , Pn, we introduce a rule

5. Defining subsetof and atomic:

For any two actions A and B we add subsetoi(A, B) if A ~ B, ...,subsetoi(A, B) if A rJ, B and atomic(A) if A is a singleton and -,atomic(A) otherwise.

The noninheritance axiom in 4 (c) is essential for the correct treatment of concurrent actions and is one of the major contribution of this paper. It may be instructive to consider several weaker forms of this axiom.

• (a) Consider an e-proposition A causes F if P1, ... , Pn The rule

says that if preconditions of A may be satisfied then A does not inherit from its subactions.

• (b) Inheriting the non-inheritance

This rule states that if b does not inherit I from c then any superset a of b does not inherit I from c.

• (c) Taking care of any inconsistency that may arise due to inheritance:

Consider a pair of e-propositions

The rules

say that for any action a containing A and B if precon­ ditions of A (B) may hold than a does not inherit ...,p (F) from B (A).

The following proposition guarantees that the above rules are subsumed by the axiom 4(c).

Proposition 2. Let II1 = 1r D be the translation of a domain description D and let II2 be an extension of II1 by the rules of the form (a)-( c) above. Then, A is an answer set of II1 iff it is an answer set of II2. 0

The following theorem is the main technical result of this paper.

Soundness Theorem. For any v-proposition P = F after A1 , ... , An and arbitrary domain description D such that A1 , ·.. , An is executable in any model of D then if 1r D entails 1r P, then D entails P. 0

The inheritance axioms do not contribute to the incom­ pleteness which is caused by the incompleteness of the theory of atomic actions [3].

4 Examples

Example 6 Independent Actions

Consider the domain description D1 from Example 1. The translation 1r D1 of this domain consists of the In­ ertia and Inheritance axioms and the following axioms obtained from propositions of D1 :

X1 -,Holds(Lifted,So) (2)

X2 ...,H olds(Opened, So) (2)

X3 H olds(Lifted, [Lift]) (3.a)

X4 H olds(Opened, [Open]) (3.a)

X5 Noninert(Opened,Open,s) ~ (3.b)

X6 Noninert(Lifted,Lift,s) ~ (3.b)

X7 N oninherit(-,Opened, x, y, S) ~ subsetof(y, x), subsetof({Open},x), ...,subsetof({Open} , y) (4.c)

X8 Noninherit(-,Lifted,x,y,S) ~ subsetof(y,x), subsetof( {Lift}, x), ...,subsetof( {Lift}, y) (4.c)

In Example 3 we have shown that the domain descrip­ tion D1 entails the v-propositions "Lifted after {Lift, Open}" and "Opened after {Lift, Open}". Let us demonstrate that the translation of these propositions is entailed by 1r D1 .

Let A be an arbitrary answer set of 1r D1 . According to the inheritance axiom 4.a and Lemma 1, to show that Holds(Lifted,[{Lift,Open}]) E A it suffices to show that

• (a) Holds(Lifted, [Lift]) E A
• while
• (b) Noninherit(Lifted, {Lift, Open}, {Lift}, So)¢ A .
• (a) follows immediately from X3. To prove (b) recall that D1 is consistent (see Example 3) and therefore, by the Soundness Theorem, 1r D1 has a consistent answer set . Now (b) is the immedi­ ate consequence of Lemma 1, and the fact that Noninherit(Lifted, {Lift, Open}, {Lift}, So) does not occur in the head of any ground instance of a rule from 1r D1. Similar argument can be used to show that 1r D1 entails Holds( Opened, [ {Lift, Open}]) .

In the following example we show how our formalism handles the case when the effect of a compound action cancels the effect of the atomic actions.

Example 7 Dependent Actions: Cancellation Consider the domain description D2 of Example 2. It is easy to see that D2 entails

(a) ..., Spilled after {LifLr, LifLl}.

1r D2 entails the translation of (a) since it contains the rule

Holds(..., Spilled, [{LifLr, LifU}]) ~

obtained from e--proposition

{LifLl, LifLr} causes ...,Spilled

from D2 .

To see why the Inheritance axiom does not cause incon­ sistency by inheriting, say, Holds(Spilled, [{LifU}]) as the result of the action [{LiftJ, Lift..r}] it suffices to no­ tice that the rule

N oninherit(Spilled, {LifU, LifLr }, LifLl, s) ~ subsetof(Lift_Left, {LifU, LifLr} ), subsetof( {LifU, Lift_r }, {LifLl, Lift_r} ) , -,subsetof( {LifLr, LifLl}, LifLl)

belongs to 1r D2 as a ground instance of 4.c., therefore Noninherit(Spilled,{LifLl,LifLr} , LifU, s) is en­ tailed by 1r D2 for any situation s.

The effects of compound actions are cancelled in essen­ tially the same way. Consider a domain description D2.1 obtained from D2 by adding an e--proposition

{Flip, LifLr, LifU} causes Spilled.

1rD2.1 will contain the rules:

H olds(Spilled, [{Flip, Lift_r, LifU}])

Non inherit( -,Spilled, x, y, s) ~ subsetof(y, x),

subsetof( {Flip, LifLr, LifU}, x) , · ...,subsetof( {Flip, Lift_r, LifU}, y) (4.c)

These rules entail

Noninherit(-,Spilled, {Flip, Lift_r, LifU}, {LifLr, LifU}, s)

which blocks the inheritance axioms ( 4.b) and hence {Flip, Lift_r, LifU} does not inherit "...,Spilled'' from {LifLr, LifU} .

In the next example we show how to repr~se_nt a com­ pound action whose subactions have conflicting eff~cts. ,

Example 8 Conflicting Subactions

Consider the domain description Da of Example 4. Since for any state u the transition function <I> of Da is un­ defined on ( {Open, C 1 ose}, u) the effect of performing "Close" and "Open" concurrently is unknown. Accord­ ingly, no information about the state [{Open, Close}] is entailed by 1r Da. To show that this is indeed the case let us notice that the following rules belong to 1r D3 :

Z1 -,Holds( Opened, [ {Close}]) (3.a)

Z2 Holds( Opened, [ {Open}]) (3.a)

• Z3 Noninherit(-.Opened, x, y, s) +- subsetof(y, x), subsetof( {Open}, x ), -.subsetof( {Open}, y) ( 4.c)
• Z4 N oninherit(Opened, x, y, s) +- subsetof(y, x), subsetof( {Close}, x), -.subset of( {Close}, y) ( 4.c)

By instantiating Z4 with x = {Open, Close} and y = {Open} we obtain the clause:

N oninherit( Opened, {Open, Close}, {Open}, s)

Similarly, from Z3 we obtain the clause

N oninherit( -.Opened, {Open, Close}, {Close}, s)

Hence, neither Holds( Opened, [ {Open, Close}]) nor -.Holds(Opened,[{Open,Ciose}]) can be derived from 1rD3 using (4.b). From Lemma 1 and consis­ tency of 1r Da we can conclude that it is un­ known if "Opened" holds or does not hold in [ {Open, Close}]. Notice however, that our program en­ tails H olds(Painted, [ {Open, Close, Paint}]) -

a translation of the v-proposition

Painted after {Open, Close, Paint} not entailed by D. (since {Open, Close, Paint} is not executable in models of D). This explains the executability condition in the Soundness Theorem.

5 Relation to other work.

The language Ac and the translation of domain descrip­ tions in this language builds on the ideas from [3] . The treatment of concurrency in the languag_e of situation calculus follows the lines suggested in [4]. The use of the syntax and semantics of ELP's instead of predicate calculus and circumscription allows us to come up with a more complete and computationally superior system of axiom. Another recent paper addressing the possi­ bility of expressing the results of concurrent actions in situation calculus is [7]. The precise relationship be­ tween the two approaches is yet to be investigated. The important difference is again in the choice of the for­ malisms- the. nonmonotonic approach of [7] seems tore­ quire combining two different non-monotonic formalisms - circumscription and default logic. In contrast our ap­ proaches use single formalisms of domain descriptions or that of ELP's. There are some other differences: for instance, in Example 8 expanded by a v-proposition "initially Open", the formalism of Lin and Shoham uses inertia to entail Holds( Open, {Open, Close}) while we believe that "unknown" (produced by our systems) is the more intuitive answer . The nice feature of Lin and Shoham's formalization is so called epistemological com­ pleteness of their system [6]. Intuitively, a theory of a (deterministic) action is epistemologically complete if, given a complete description of the initial situation, the theory enables us to predict a complete description of the resulting situation when the action is performed. Since some of our actions are not executable we can not ex­ pect to have precisely this property but it is possible to suitably modify the notion and show that both our for­ malisms are epistemologically complete w.r.t. executable actions. This will be done in the full version of this pa­ per, in which we will also elaborate on our treatment of non-executable and unknown actions.

Acknowledgement

We would like to acknowledge the grants NSF-IRI-92-11662, NSF-CDA 90-15-006 and NSF-IRI 91-03-112. We also thank V. Lifschitz, G. Kartha and the anonymous referees for their valuable comments.