Reasoning about Plans

1 Introduction

In classical planning we are faced with the following for­ mal task: Given a set A of admissible actions, a formula a describing the set of initial states and a formula f3 rep­ resenting a goal to be achieved, construct a plan II, i.e. a finite sequence of actions from A, such that execution of II begun in any state satisfying a is guaranteed to terminate in a state satisfying (3.

This classical model of planning is oversimplified. In many practical settings it is reasonable to construct and execute plans that are not assured to succeed. There are two basic reasons for that. Firstly, it may happen that a plan that always achieves a final state does not exist. Secondly, even if such a plan exists, it may be better to choose a simpler, although uncertain plan. An example will help to illustrate this.

Suppose I want to contact John. All information I have is his phone number and the fact that he is at home. Given this, the only plan I can choose is to call him. Of course, the plan may fail, if John's phone line is busy, but there is no better possibility. To guarantee the success of the plan, I have to know that John's line is not busy at the moment. Unfortunately, this information is hardly available.

*This research was partially supported by the KBN grant 8Tl1C 001 11.

Assume now that, in addition, I know John's address. In this case, I can assure my goal by visiting him. How­ ever, it may still be much more reasonable to give up this ironclad plan and to choose the previous one.

In this paper, we extend the classical model of plan­ ning by permitting plans that are not assured to succeed. Such a plan is just a sequence of actions, considered rel­ atively to some specification. A specification consists of a description of the initial states and a goal to achieve.

Plans that need not behave according to their speci­ fications can be naturally divided into three categories: (1) Those that always achieve their goals (valid plans). (2) Those that may achieve their goals or not, depend­ ing on some additional information (admissible plans) . 1 (3) Those that never achieve their goals (inadmissible plans).

As an example, suppose that all we know about the initial state is that a turkey is alive and the goal is to make it dead. There are two actions: load (loads a gun) and shoot (kills the turkey, provided that the gun is loaded) . Consider three plans: (1) load; shoot; (2) shoot; (3) load. The first of these plans is valid, the second one is admissible, whereas the third one is inadmissible.

It is important to note that an admissible plan can be often validated (i.e. made valid) or falsified (i.e. made inadmissible) by providing new observations. Reconsider the plan (2) stated above. The observation that the gun is initially loaded (resp. unloaded) validates (resp. falsi­ fies) the plan.

This paper addresses two problems:

1. How to determine whether a given plan is valid, ad­ missible or inadmissible.
2. Given an admissible plan, determine a minimal set of observations that are to be made in the initial

1 1t should be emphasized that admissible plans differ from what is called uncertain plans in the AI literature. This latter notion corresponds to plans that may fail not because some information is missing, but rather because they involve ac­ tions that succeed with some probability. (See [Boutilier et al., 1995], for a good survey concerning uncertain plans.)

state (or in some intermediate state, if the plan is in progress) to validate or falsify the plan.

To represent actions occurring in plans, we use Dijk­ stra's a~proach originally developed to deal with pro­ grams [Dijkstra, 1976; Dijkstra, Scholten, 1990]. The advantage of Dijkstra's formalism for reasoning about action and change, when compared with purely logi­ cal approaches such as Situation Calculus [McCarthy, Hayes, 1969; Lifschitz, 1988; Gelfond et a/., 1991] or Fea­ tures and Fluents [Sandewall, 1994], is its simplicity. It has been shown in [Lukaszewiczj Madalinska, 1994; 1995; 1995a; Jablonowski et a/., 1996 .

The paper is organized as follows. We start with a brief summary of Dijkstra's semantics for a very sim­ ple programming language. Section 3 is devoted to the theory of prime implicants that play an important role in plan analysis. In section 4, we show how action lan­ guages are to be formalized using Dijkstra's methodol­ ogy. In section 5, we provide a number of results allowing to analyse plans before their executions, whereas, in sec­ tion 6, these results are generalized for plans in progress. Finally, in section 7, we provide conclude remarks and future work.

Proofs of all stated results can be found in the full version of this paper.

2 Introduction to Dijkstra's semantics

In [Dijkstra, Scholten, 1990] we are provided with a very simple programming language whose semantics is speci­ fied in terms of formula transformers. More specifically, with each command S there are associated two formula transformers, called the weakest precondition and the strongest postcondition, denoted by wp and sp, respec­ tively. Before providing the meanin~ of these transform­ ers we introduce some terminology.

First of all, we assume here that the programming language under consideration contains one type of vari­ ables only, namely Boolean variables. This assumption may seem overly restrictive, but as a matter of fact no other variables will be needed for our purpose. In the rest of this paper Boolean variables will be referred to as fiuents.

Let :F be a set offluents. A state over :F is any function u from the members of :F into the truth-values {0, 1}. A state u is said to be a model of a formula a iff a is true mu.

An assertion language over a set :F of fluents is the set of all formulae constructable in the usual way from members of :F, sentential connectives(...,,~. 1\, V, ::) and truth-constants T (true) and F (false). In what follows, the term 'formula' refers always to a formula of some fixed assertion language. If f3 and a are formulae and x is a fluent, then we write f3[x +-a] to denote the formula which obtains from f3 by replacing all occurrences of x by a. If x is a fluent and a is a formula, then we write 3x.a as an abbreviation for a[x +- T] V a[x +- F].

2 We ignore the weakest liberal precondition transformer, considered in [Dijkstra, Scholten, 1990], because it will not be used in the sequel.

The formula transformers mentioned above are to be understood as follows. For each command S and each formula a:

• wp(S, a) is the formula whose models are precisely all states such that execution of S begun in any one of them is guaranteed to terminate in a state satisfying a.
• sp(S, a) is the formula whose models are precisely all states such that each of them can be reached by starting execution of S in some state satisfying a.

For a detailed discussion of Dijkstra's methodology the reader should consult [Apt, Olderog, 1991].

2.1 List of commands

The considered language consists of skip command, as­ signment to simple variables, alternative command and sequential composition of commands 3 . Semantics of these commands is specified in terms of formula t.rans­ formers explained above.

1. The skip command. This is the "empty" com­ mand in that its execution does not change the com­ putation state. The semantics of skip is thus given by

wp(skip, a)= sp(skip, a)= a.

1. The assignment command. This command is of the form x := e, where x is a fluent and e is a (propositional) formula. The effect of the command is to replace the value of x by the value of e. Its semantics is given by

If the fluent x does not occur in the expression e, the equation (1) can be simplified. In this case

In the sequel we shall often deal with assignment commands, x := e, where e is Tor F . In this case the equation (2) can be replaced by

1. The sequential composition command. This com­ mand is of the form sl; s2' where sl and s2 are any commands. It is executed by first executing S1 and then executing s2. Its semantics is given by

1. The alternative command. This command is of the form

where B1, ... , Bn are formulae and S1, ... , Sn are commands. B1 , ... , Bn are called guards and ex­ pressions of the form B; - S; are called guarded commands. In the sequel, we refer to the general command (4) as IF. The command is executed as follows. If none of the guards is true, then the ex­ ecution aborts. Otherwise, one guarded command B; -+ S; with true B; is randomly selected and S; is executed. 4 The semantics of IF is given by

3 The original Dijkstra's language contains abort command and iterative commands as well, but they are not needed for our purpose.

3 Prime implicants

In this section we provide a brief introduction to the theory of prime implicants that will play the crucial role in the rest of this paper. Our presentation is partially based on [Brown, 1990].

We start with some preliminary terminology.

A literal is a fluent or its negation. A term is either T or F or a conjunction of literals in which no fluent ap­ pears more than once. A formula is said to be in disjunc­ tive normal form (DNF, for short) if it is a disjunction of different terms. 5 It is well-known that each formula can be constructively transformed into its equivalent in DN F. We say that a term t1 absorbs a term t2 if either t1 is Tor t2 is For t 1 is a subterm of t2. For instance, the term a absorbs the term a A /. Let a be a formula in DNF. We write ABS(a) to denote the formula ob­ tained from a by deleting all absorbed terms. Clearly, a and ABS(a) are equivalent.

Let t be a term different from F and suppose that a is any formula. We say that t is an implicant of a iff the formula t ~ a is a tautology. An implicant t of a is said to be prime iff no proper subterm oft is an implicant of a.

The problem of finding all prime implicants of a given (propositional) formula has been extensively studied in the Switching Circuits Theory. 6 Actually, there exist a number of algorithms solving this task. One of them, usually referred to as iterated consensus, is given below.

Two terms are said to have an opposition if one of them contains the fluent f and the other the fluent ...,f. For instance, the terms ...,a A I and a A d have a single opposition, in the fluent a.

Suppose that two terms, t 1 and t2, have exactly one opposition. Then the consensus of t1 and t2 , written c(t1, t2) , is the term obtained from the conjunction t1 At2 by deleting the opposed fluents as well as any repeated fluents. For example, c(...,a A/, a A d) is I A d.

Let a be a formula. The Blake canonical form of a, written BCF(a), is the formula obtained from a by the following construction.

4 Note that when more than one guard is true, the selection of a guarded command is nondeterministic.

~In the logical literature D N F is often defined as a dis­ junction of terms where a term is understood as either T or For any conjunction of literals. Note, however, that we can always restrict ourselves to terms in which no fluent appears more than once: each repeated occurence of a fluent I can be removed from a term, whereas any term including I and -.1 can be replaced by· F .

6 It should be stressed that this problem is N P-complete.

1. Replace a by its disjunctive normal form. Denote the resulting formula by {3.
2. Repeat as long as possible: if {3 contains a pair t1 and t2 of terms whose con­ sensus exists and no term of {3 is a subformula of c(t1 , t2), then {3 := {3 V c(t1 , t2).
3. Take ABS({3). This is BCF(a) .

Theorem 1 ([Brown, 1990]) Formulae a and BCF(a) are equivalent. ·

Theorem 2 ([Brown, 1990]) BCF(a) is the disjunc­ tion of all prime implicants of a . ·

Example 1 Let a be (...,aAd)V(at\bA-,c)V(at\...,ct\...,d) . Since a is in disjunctive normal form, f3 = a. After performing step (2) , we get

(...,a A d) V (at\ b t\ -,c) V (at\ ...,c t\ ...,d) V (b t\ d A ...,c).(5) Since ABS((5)) = (5), the formula (5) is the Blake canonical form of a. ·

Classically, a prime implicant of a formula a is a min­ imal satisfiable term logically implying a . In what fol­ lows, we shall be interested in finding minimal satisfiable terms logically implying a given formula a , under the as­ sumption that a given formula {3 holds. This motivates the following definition.

Definition 1 Let a and {3 be formulae. A term t is an implicant of a wrt {3 iff (1) {3 At is satisfiable; (2) {3 t\ t ~ a is a tautology. A term t is said to be a prime implicant of a wrt f3 iff t is an implicant of a wrt {3 and no proper subterm oft is an implicant of a wrt {3. ·

The following theorem holds.

Theorem 3 A term t is a prime implicant of a wrt f3 iff t is a prime implicant of {3 ~ a such that {3 t\ t is satisfiable. ·

The application of Theorem 3 requires satifiability check. This check can be effectively done if {3 is in DN F . The details follow.

Lett be a term different from F and let {3 = t1 V · · · Vtn be a formula in DN F . The quotient of f3 wrt t , written {3 jt, is the formula (also in D N F) obtained from {3 by the following construction: (1) Replace each t; containing a fluent whose negation occurs in t by F . (2) In the remaining terms delete all fluents occurring in t (if all fluents are deleted, replace the term by T). For instance, if t is ...,p A q and {3 is ...,q t\ r V ...,p t\ s, then {3 jt is F V s.

The following result is straightforward.

Theorem 4 Let t be a term different from F and sup­ pose that {3 is any formula in D N F. The formula t A {3 is satisfiable iff f3 jt contains at least one term different from F . ·

4 Action languages and plans

Specification of an action language is a three-step pro­ cess.

1. The first step is to choose an underlying asser­ tion language L serving to represent the considered world. In this paper, Lis always the classical propo­ sitional logic based on a finite set of fluents.

1. The next step is to provide action symbols repre­ senting actions. For instance, we can have the action symbol load, representing the action that makes a gun loaded.
2. The final step is to provide action symbols with Dijkstra-style semantics. This is done by first trans­ lating these symbols into commands of program­ ming language described in section 2, and then cal­ culating the weakest precondition and the strongest postcondition for the chosen actions. The action load can be naturally translated into the assignment command I := T, where I is the fluent standing for loaded. The semantics of load is given by

The objects we are primarily interested in are plans. These are expressions of the form At; . . . ; An, where At, . .. , An are action symbols. Each plan is always con­ sidered wrt a specification, i.e. a pair (a, {3}, where a and f3 are satifiable formulae 7 . The plan At; .. . ; An , considered wrt a specification (a, {3}, has the following interpretation: the actions At, .. . , An are to be sequen­ tially performed to achieve a goal {3, provided that the initial state satisfies a. As remarked earlier, we never as­ sume that the execution of the plan activated in a state satisfying a guarantees {3.

5 Analysis of plans

Let II = At; . .. ; An be a plan. We say that II is valid wrt a specification (a, {3} iff II terminates in a state satisfying f3 whenever it is activated in a state satisfying a. II is said to be inadmissible wrt (a, {3} iff II terminates in a state satisfying -.{3 whenever it is activated in a state satisfying a. Finally, II is called admissible wrt (a, {3} iff it is neither valid wrt (a, {3} nor inadmissible wrt (a, {3} .

Formally, a plan II = At; ... ; An is a program in Di­ jkstra's language. Accordingly, wp( At ; .. . ; An, {3) is the formula whose models are precisely all states u such that whenever II is activated in u, it is guaranted to termi­ nate in a state satisfying the goal {3. On the other hand, if wp(At; .. . ; An, -.{3) holds in the initial state, then the plan II never achieves the goal {3. Thus we have:

Theorem 5 A plan II =At; .. . ; An is valid (resp . . in­ admissible) wrt (a,f3} iff the formula a=> wp(At; ... ; An,f3) (resp. a=> wp(At; ... ;An,-.f3)) is a tautology. Otherwise, i.e. if neither a=> wp(At; ... ;An,f3) nor a=> wp(At; .. . ;An , -.f3) is a tautology, the plan II is admissible wrt (a, {3}. ·

As we remarked earlier, admissible plans can be often validated or falsified by providing new information. The details are these.

Let II = At ; . . . ; An be a plan admissible wrt (a, {3} . A term t = It 1\ . .. 1\ lk ( k > 1) such that a 1\ t is satisfiable is called a support (resp. counter-support) for II wrt (a,f3} iff II is valid (resp. inadmissible) wrt (a 1\ t,{3}. A support (resp. counter-support) t for II is said to be minimal iff no proper subterm oft is a support (resp. counter-support) for II. Intuitively, a minimal support t for a plan can be viewed as a minimal set of additional observations (literals oft) whose truth in the initial state validates the plan. Similarly, a minimal counter-support for the plan can be viewed as a minimal set of additional observations whose truth in the initial state falsifies the plan.

7 The assumption that a and f3 are satisfiable is not nec­ essary. However, specifications violating this assumption are of no practical interest.

The next theorem provides a method of finding all minimal supports and counter-supports for a given plan.

Theorem 6 Let II = At; .. . ; An be a plan admissi­ ble wrt (a, {3}. A term t is a minimal support (resp. counter-support) for II iff t is a prime implicant of wp(At; ... ;An,f3) (resp. wp(At; ... ;An,-.f3) wrt a.

· Example 2 We have four fluents a, 1, h, d standing for alive (a turkey), loaded (a gun), hidden (a turkey) and deaf (a turkey), respectively. There are two actions, load and shoot, specified as follows.

load: if d -+ I := T ~ -.d -+ I := T; h := T fi

shoot: ifl/\-.h-+ l:=F;a:=F~-.lVh-+ l:=Ffi.

Consider the plan II = load; shoot, regarded wrt the specification (a 1\ -.h, -.a}. It is easily verified that

wp(load; shoot, -.a)= -.h 1\ d V -.a

wp(load; shoot, a)= a 1\ ( -.d V h).

Since neither a 1\ -.h => wp( load; shoot, -.a) nor a 1\ -.h => wp(load; shoot, a) is a tautology, we infer that the plan II is admissible wrt (a 1\ -.h, -.a} .

To find all minimal supports for II wrt (a 1\ -.h, -.a}, we calculate all prime implicants of wp(load; shoot, ·a) wrt a 1\ -.h. By Theorem 3, these are the prime impli­ cants of a 1\ -.h => wp(load; shoot, -.a) which are con­ sistent with a 1\ -.h. Applying the algorithm stated in section 3, it is readily verified that the BCF of a 1\ -.h => wp(load; shoot, -.a) is -.a V h V d. Since ·a and h are both inconsistent with a 1\ -.h, we conclude that there is one prime implicant of wp(load; shoot , ·a) wrt a 1\ -.h, namely d. Accordingly, dis the only minimal support for II wrt (a 1\ -.h, -.a) .

We leave it to the reader to check that the term ·d is the only minimal counter-support for II wrt (a/\ -.h, ·a}.

· The following theorem provides a partial relationship between supports and counter-supports.

Theorem 7 Let II = At; ... ; An be a plan admissible wrt (a, {3) . Suppose further that the commands corre­ sponding to At, . . . , An are all deterministic. If all the minimal supports for II wrt (a, {3) are false in the initial state, then at least one counter-support for II wrt (a, {3} is true in this state. ·

Theorem 7 allows us to falsify a deterministic plan when all its supports are false. However, the theorem does not generally hold for non-deterministic plans.

6 Plans in progress

In the previous section we have provided a number of results allowing to analyse a plan before its execution.

Sometimes however it is reasonable to provide a similar analysis when a pia~ is in progress. To ill~strate this, reconsider the plan from Example 2. To vahdate or fal­ sify this plan, we have to establish whether the tur~ey is deaf or not in the initial state. Unfortunately, th1s ob­ servation is hardly available. On the other hand, we can start the plan and try to figure out whether the turkey is hidden after performing the action load. If so, we know that the plan will fail and should be given up. Other­ wise the plan will succeed. Clearly, it is much easier to dete;mine whether the turkey is hidden or not than to determine whether it is deaf or not.

A plan in progress is any expression of the form

where A1 , ... , A~;, A~:+J, ... , An are action symbols and 1 < k < n . Such a plan, considered wrt a specification (a~ {3), has the following intuitive interpretation: the _ac­ tions A1 , ... , A~: have been already performed, startmg in a state satisfying a, and now the actions AI:+ I, ... , An are to be performed to achieve a state satisfying {3.

The only difference between a plan in progress of the form (6) and the ordinary plan A1;: .. ; A~:; Ak+J; ... ; A_n is that the former has been partially executed. Th1s motivates the following definition.

Let II = A1 ; ·.. ; A~; ~ Ak+J; ... ; An be a plan in progress. II is said to be valid (resp. admissible, in­ admissible) wrt a specification (a, {3) iff the (ordinary) plan A1 ; .. . ; A~:; A~;+ 1 ; .. . ; An is valid (resp. admissible, inadmissible) wrt (a, {3). .

Let II=A1; ... ;A~: ~Ak+J ; ... ;An be a plan m progress, considered wrt (a, {3). Obv~ously, II can be reduced to the plan A~;+1 ; ... ; An, considered wrt (1, {3), where 1 is a formula characterizing. all states rea_cha?le after performing A1 ; ... ; A~: begun m a state sat1~f~mg a. By the definition of sp (the strongest postcond1t1?n) transformer, 1 is just sp(AJ; ... ; A~:, a) . Thus, we Im­ mediately have:

Theorem 8 Let II = A1; ... ; A~: ~ A~;+J; ... ; An be a plan in progress. II is valid (resp. admiss~ble, ~nadmis­ sible) wrt (a, {3) iff the plan AI:+ I; ... ; An JS vahd (resp. admissible, inadmissible) wrt (sp(AJ; ... ; A~;, a), {3). ·

Let II = A1; . . . ; A~: ~ Ak+J; ... ; An be a plan in progress, admissible wrt (sp(AJ; . .. ;A~;,a),f3). ~ minimal support (resp. counter-support) for II Js any minimal support (resp. counter-sup~o~t) for Akt1; . .. ;An wrt {sp(AJ; .. . ;A~;,a),f3}. IntmtJvely, a minimal support (resp. counter-support) for a plan A1; ... ; A~: ~ A1:+1; ... ; An is a minimal set of observa­ tions whose truth in the state being the result of per­ forming the actions A1 ; ... ; A.1: validates (resp. falsifies) the plan.

Example 2 (continued) To validate or falsify the plan II we have to establish the value of the fluent d in the initial state. Suppose that this information is unavail­ able. All we can do in this case is to start the plan by ·performing the action load, i.e. to replace II by a plan in progress II1 = load ~ shoot. Since II is admissible wrt (a 1\ ·h , ·a), II1 is also admissible wrt {a 1\ ·h, ·a). To find minimal supports for II1 wrt {a 1\ ·h, ·a), we calculate all minimal supports for the plan shoot wrt

(sp(load , a 1\ ·h), ·a). In view of Theorem 6, these are prime implicants of wp(shoot, ·a) wrt sp(load, a 1\ ·h). It is readily verified that

Performing the algorithm from section 3, we get BC F( (7) => (8)) := ·a V ·I V ·h V d.. It is ~asy to check that implicants ·h and d are consistent w1th (7), whereas ·a and --,[ are not. Thus, II1 has two minimal supports wrt (a 1\ ·h, ·a), namely d and ·h. In other words if we observe that the turkey is either deaf or not hidde~, after performing the action load, we can safetely continue the plan to achieve its goal.

To find all minimal counter-supports for Il1 wrt (a 1\ ·h, ·a), we calculate prime implicants of wp( shoot, a) wrt sp( I oad, a 1\ ·h). It is easily checked that these a~e h and ·d. Accordingly, if we observe that the turkey IS hidden or not deaf, after executing the action load, we know that our plan will fail and hence should be given up. ·

The next example illustrates an interesting phe­ nomenon: there are plans that can be validated or falsi­ fied only when they are in progress.

Example 3 There are two fluents, a (alive) and I (loaded), and two actions spin and shootl, defined by the commands

Consider the plan II = spin; shootl, regarded wrt the specification {a, ·a) .

Since neither a => (9) nor a => (10) is a tautology, we conclude that II is admissible wrt (a, ·a) .

Since ·a is inconsistent with a, there are neither minimal supports nor minimal counter-supports for II wrt (a, ·a) . This intuitively means that no additional observation in the initial state can validate or falsify the plan II.

To validate/falsify the plan II, we have to consider it in progress. Assume therefore, that we started th~ plan by performing the action spin. Denote the resultmg plan, spin ~ shoot1, by II1. Since II is admissible wrt (a , ·a), II1 is also admissible wrt (a, ·a) .

Since ·a is inconsistent with a, whereas I is consistent with a, we conclude that there is one minimal support for II1 wrt (a, ·a), namely/. Accor~ingly, if w~ obser.ve that the gun is loaded after performmg the actwn spm, we know that the plan will succeed.

Since -.a is inconsistent with a, whereas -.1 is consis­ tent with a, we infer that there is one minimal counter­ support for 111 wrt (a, -.a), namely -.1. Thus, if we ob­ serve that the gun is unloaded after performing the ac­ tion spin, we know that the plan will fail and should be given up. ·

7 Conclusions

In this paper, we have argued that it makes sense to consider and execute plans that are not guaranteed to succeed. We have adressed two fundamental problems related to such plans:

1. How to determine whether a given plan is valid (i.e. always succeeds), admissible (i.e. succeeds or fails depending on some additional information) or inad­ missible (i.e. always fails).
2. Given an admissible plan, determine a minimal set of observations that are to be made in the initial state (or in some intermediate state, if the plan is in progress) to validate or falsify the plan.

To formalize actions occurring in plans, we· have em­ ployed Dijkstra's semantics for programming languages. This allows us to represent a broad class of plans, in par­ ticular those including actions with non-deterministic ef­ fects. In addition, we do not require that initial or final states are to be completely specified.

We believe that technical results stated in sections 5 and 6 can be used while constructing plans. We would like to pursue this topic in the future.

Ackow ledgements

We would like to thank Wladyslaw M. Turski for his comments on the earlier draft of this paper.