Reasoning about Action and Change Using Dijkstra's Semantics for Programming Languages: Preliminary Report

1 Introduction

We apply Dijkstra's semantics for programming lan­ guages [Dijkstra, 1976; Dijkstra and Scholten, 1990] to formalization of reasoning about action and change. The basic idea is to specify effects of actions in terms of for­ mula transformers, i.e. functions from formulae into for­ mulae. More specifically, with each action A we associate two formula transformers, called the strongest postcondi­ tion for A and the weakest liberal precondition for A. The former, when applied to a formula a, returns a formula representing the set of all states that can be achieved by starting execution of A in some state satisfying a . The latter, when applied to a formula a, returns a formula providing a description of all states such that whenever execution of A starts in any one of them and terminates, the output state satisfies a . 1

The idea of employing formula transformers to spec­ ify effects of actions is not new in the AI literature. Waldinger [1977], in the context of STRIPS system [Fikes and Nilsson, 1971], introduces a notion of a re­ gression operat_or which corresponds closely to the weak­ est precondition transformer. Pednault [1986; 1988;

·This research was supported in part by the ESPRIT Ba­ sic Research Action No. 6156- DRUMS II and by KBN grant 3 P406 019 06.

1 We do not use the weakest precondition transformer ( wp) which plays a prominent role in reasoning about programs. The reason is that, in general, the wp transformer is slightly too strong for our purposes.

1989] employes regression operators for plan synthesis. In [Pednault, 1986] a notion of progression operator, corresponding to Dijkstra's strongest postcondition, is introduced and analysed.

Formula transformers approach to reasoning about ac­ tion and change has one major advantage and one major weakness when compared to purely logical formalisms such as Situation Calculus [Hayes and McCarthy, 1969; Lifschitz, 1988; Lifschitz and Rabinov, 1989; Gelfand et al., 1991; Baker, 1991] or Features and Fluents [Sande­ wall, 1994]. On the positive side, describing effects of actions in terms of formula transformers decreases com­ putational complexity. The price to pay for it is the loss of expressibility.

Our proposal combines computational effectiveness with expressibility. Although not so expressible as Sit­ uation Calculus or Feature and Fluents, the formalism specified here allows to deal with a broad class of ac­ tions, including those with random and indirect effects. Also, both temporal prediction and postdiction reason­ ing tasks can be solved without restricting initial nor final states to completely specified. 2

The paper is organized as follows . Section 2 is a brief introduction to Dijkstra's semantics for a simple pro­ gramming language. In section 3, we outline a general procedure to define action languages using Dijkstra's methodology, illustrate this procedure by specifying a simple "shooting" language, and introduce a notion of an action scenario. Section 4 defines the kind of rea­ soning we shall be interested in , and provides a simple method of realizing this type of inference. In section 5, we illustrate this method by considering a number of ex­ amples, well-known from the AI literature. Section 6 is devoted to actions with indirect effects. Finally, section 7 contains discussion and ideas for future work.

For lack of space, we omit proofs of the results pro­ vided here. The full version of the paper is available in pubjpapers/CRIT/Dijkstra/ijcai95.ps by anonymous ftp to ftp.mimuw.edu .pl.

2 This paper is part of a general programme of applying Dijkstra's approach to reasoning about action and change. In [Lukaszewicz and Madalinska-Bugaj , 1994], we used this methodology to formalize deterministic actions without indi­ rect effects. In [Lukaszewicz and Madalinska-Bugaj, 1995], we combined Dijkstra's semantics with Reiter's default logic to deal with actions where abnormal effects are allowed.

2 Introduction to Dijkstra's semantics

In [Dijkstra and Scholten, 1990] we are provided with a simple programming language whose semantics is spec­ ified in terms of formula trasformers. More specifically, with each command S there are associated three such transformers, called the weakest precondition, the weak­ est liberal precondition and the strongest postcondition, denoted by wp.S, wlp.S and sp.S, respectively. Before providing the meaning of these transformers, we have to make some remarks and introduce some terminology.

We assume here that the programming language under consideration contains one type of variables only, namely Boolean variables. This assumption may seem overly restrictive, but no other variables will be needed for our purpose.

Let V be a set of Boolean variables. A state over V is any function u from V into the truth-values { 0, 1} .

An assertion language over a set V of Boolean vari­ ables, denoted by .C(V), is the set of all formulae con­ structable in the usual way from members of V, truth­ constants T and F , sentential connectives(...., , :J, A, V, =:) and quantifiers (V, 3) . 3 In what follows, the term 'for­ mula' refers always to a formula of some fixed asser­ tion language. A formula a is said to be a Boolean ex­ pression if it contains no quantifiers. If f3 is a formula, a1, ... , an are Boolean expressions and x1, . .. , Xn are variables, then we write f3[x1 +-- a1, . .. , Xn +--an] to de­ note the formula which obtains from f3 by simultaneously replacing all free occurrences of x1, ... , Xn by a1, .. . , an, respectively.

The value of a formula a E .C(V) in a state u, written II a llu, is an element from {0, 1} specified by the usual rules for classi<;al propositional logic, together with:

• (i) II Vx.a llu= 1 iff II a llu'= 1, for each u' identical to u except on the variable x .
• (ii) II 3x .a llu= 1 iff II a llu'= 1, for some u' identical to u except on the variable x . 4

A state u is said to satisfy a formula a iff II a llu= 1 . If u satisfies a, then u is called a model of a . When we say that u satisfies a, we always implicitly assume that u provides an interpretation for all Boolean variables occurring in a.

The formula transformers mentioned above are to be understood as follows. For each command S and each formula a : (1) wp.S(a) is the formula whose models are precisely the states such that execution of S begun in any one of them is guaranteed to terminate in a state satisfying a. (2) wlp.S( a) is the formula whose models are precisely the states such that whenever execution of S starts in any one of them and terminates, the out­ put state satisfies a. (3) sp.S( a) is the formula whose models are precisely the states such that each of them can be reached by starting execution of S in some state satisfying a .

3 Note that quantifiers can be applied to Boolean variables only.

4 Note that quantified formulae can be reduced into equiva­ lent Boolean expressions. Namely, formulae of the form 'Vx.a can be replaced by a[x +- T] 1\ a[x +- F], whereas formu­ lae of the form 3x.a by a[x +- T] V a[x +- F]. Accordingly, assertion languages we consider here are in fact propositional.

In what follows, for each formula transformer X E {wp,wlp,sp}, we shall write X(S,a) instead of X.S(a) .

2.1 List of commands

The considered language consists of skip command, as­ signment to simple variables, alternative command and sequential composition of commands 5 . Semantics of these commands is specified as follows. 6

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

1. The assignment command. This command is of the form x := e , where xis a (Boolean) variable and e is a (Boolean) expression. The weakest liberal precondition of this command is given by

The strongest postcondition for assignment command is more complex. In general, it is given by

or equivalently

In the sequel we shall often deal with assignment com­ mands, x := e, where e is T or F . In this case, sp(x := e,a) can be reduced to

3. The sequential composition command. This com­ mand is of the form s1; s2, where s1 and s2 are any commands . Its semantics is given by

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

where B1 , .. . , Bn · are Boolean expressions and S1 , ... , Sn are any commands. In the sequel , we refer to (4) as IF. The command is executed as follows . If none of B; is true, then the execution aborts. Other­ wise, one command S; with true B; is randomly selected and executed. 7 The semantics of IF is given by

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

6 In what follows, we do not specify the wp formula tran­ formers for the considered language, because they will not be needed in the sequel.

7 Note that when more than one of B; is true, the selection of a command to execute is nondeterministic.

2.2 Main results

Dijkstra and Scholten [1990] consider various classes of computations. The class we are primarily interested in here is called by these authors initially a and finally /3 under control of S, where a and f3 are formulae and S is a command. -r:his class, which will be denoted by [S]$, represents the set of all computations under control of S that start in a state satisfying a and terminate in a state satisfying /3.

Suppose that c E [S]$ . Obviously, since S terminates in a state satisfying f3 and wlp(S, -.j3) represents the set of all states such that S begun in any of them ei­ ther terminates in a state satisfying -.j3 or loops forever, it must be the case that the initial state of c satisfies a 1\ -.wlp(S, -.j3). Similarly, since S starts in a state sat­ isfying a and sp( S, a) represents the set of all states such that any of them can be reached by starting execution of S in some state satisfying a, we conclude that the final state of c satisfies j31\ sp( S, a). An interesting question is whether the formulae a 1\ -.wlp(S, -.j3) and /31\ sp(S, a) provide a complete description of the initial and final states of the computations from the class [S]$. That the answer is positive follows from the following result which can be found in [Dijkstra and Scholten, 1990].

Theorem 1 The formula al\-.wlp(S, -.j3) (resp. /3 1\ sp( S, a)) holds in a state u iff there exists a computation c from [S]$ such that u is the initial (resp. final) state of c. ·

Consider now the class of computations C= [S]$, where S is the sequence S1; S2; ... ; Sn. Let STc(i), 0 ~ i ~ n, be the set of all states satisfying the fol­ lowing condition: for each u E STc(i), there exists a computation c E C such that u is reached by c after executing S1 ; ... ; S;. In what follows, the members of STc ( i) will be referred to as i-states of C. Clearly, 0states are initial states and n-states are final states. The following theorem provides a complete characterization of i-states.

Theorem 2 The formula sp( S1 ; ... ; S;, a) 1\ -.w/p( S;+l; ... ; Sn, -.j3) holds in a state u iff there ex­ ists a computation from the class C= [S1;S2; ... ;Sn]$ such that u E STc(i), 0 ~ i ~ n. 8 ·

There is another class of computations that we shall be interested in. This class, denoted by [S1; ... ; Sn]$('r), represents the set of all computations under control of S 1 ; ... ; Sn that start in a state satisfying a, terminate in a state satisfying f3 and, in addition, any state of any computation from this class that can be reached after executing S1 ; ... ; S; (0 ~ i ~ n) satisfies 'Y· The class [S1; ... ; Sn]$(1) will be referred to as initially a, finally /3 and always 1 under control of S1 ; ... ; Sn. 9

The next theorem provides a complete characteriza­ tion of i-states of the introduced class of computations.

8 We assume here that sp(51 ; .·. ; 5;, a) is a if i = 0 and -.wlp(5i+1; ... ; 5n, -.(3) is f3 if i = n.

9 Note that if -y is T, then the class (51 ; ··. ; 5n]~(-y) reduces to the class (51 ; ... ; 5n];3 .

Theorem 3 The formula sp'Y ( S1; ... ; S;, a 1\ 1) 1\ -.w/p'Y ( S;+l; ... ; Sn, -.(j31\ 1)) holds in a state u iff there exists a computation from the class C= [S1; ... ; Sn]$(1) such that u E STc(i). Here sp'Y and w/p'Y are specified by the following recursive definitions (6 is any formula).

3 Action languages and action scenarios

To define an action language one proceeds in three steps.

1. First, we choose an assertion language to represent the effect of actions. The "shooting language" we use in the sequel uses two Boolean variables: a and /, standing for alive and loaded, respectively. To be in accord with the AI terminology, these variables will be referred to as fiuents.
2. The next step is to provide action symbols repre­ senting the actions under consideration. In the shooting language we have four such symbols: load (a gun), wait, spin (a chamber) and shoot (a turkey). The intention is that load makes the gun loaded, wait does not cause any changes in the world, the effect of spin is that randomly the gun is loaded or not after the action, regardless of whether it was loaded before or not, and shoot makes the gun unloaded and the turkey dead, provided that the gun was loaded before.
3. The final step is to define Dijkstra-style seman­ tics for the choosen actions. To perform this step for the shooting language, it suffices to note that the con­ sidered actions can be easily translated into the pro­ gramming language specified in the previous section. More specifically, load corresponds to the assignment command I := T, wait is just the skip command, whereas spin and shoot are translated into alternative commands if I -+ a := F; I := F ~ -./ -+ skip fi and if T -+ I := T ~ T -+ l := F fi, respectively. 10 Given the above translations, the chosen actions can be pro­ vided with Dijkstra-style semantics. Performing routine calculations one easily obtains:
4. wlp(load, a)= a[/<-- T];

• wlp(wait, a)= sp(wait , a)= a;

10 0bviously, not every action can be translated into Dijk­ stra's programming language. However, most of the actions that can be found in the AI literature enjoy this property.

The objects we shall be primarily interested in are action scenarios. These are expressions of the form

where a and {3 are formulae and A1, ... , An are actions. The scenario has the following intuitive interpretation: a was observed to hold in the initial state, then the ac­ tions A1, ... , An were sequentially performed, and then {3 was observed to hold in the final state. Formally, the scenario (9) is to be viewed as representing the class of computations initially a and finally {3 under control of A1; ... ;An.

Example 1 (Yale Shooting Scenario) Below is Hank and McDermot's Yale Shooting Scenario [1987].

[a 1\ -,/]load; wait; shoot[T] ·

4 Reasoning about scenarios

We shall be interested in the following reasoning task: "Given a scenario [a] A1 ; ... ; An [{3], a formula rand an integer k such that 0 ~ k ~ n, determine whether r is assured to hold after performing the actions A1, ... , Ak". Viewing a scenario as representing a class of computa­ tions, the above reasoning task can be stated more for­ mally: "Given a scenario [a] A1; ... ; An [{3], a formula r and an integer k such that 0 ~ k ~ n, determine whether r is true in all k-states of the class of computa­ tions [A1; ... ; An]p.

In what follows, the symbol f- stands for the provabil­ ity relation of classical propositional logic.

Let SC= [a} A1 ; ... ; An [{3] be a scenario and let 0 ~ k ~ n. The description of the kth_state of SC, written DSk(SC), is the formula given by

The next result follows immediately from Theorem 2.

Theorem 4 Let SC= [a] A1; ... ; An [{3] be a scenario. A formula r is assured to hold after performing the ac­ tions A1; ... ; Ak (0 ~ k ~ n) iff DSk(SC) f- r. ·

Remark 1 All actions considered in this paper are guaranteed to terminate. If A1 ; ... ; Ak is any sequence of such actions, then wlp(A1; ... ; Ak, F) = F. Accord­ ingly, if SC ·is a scenario of the form [a] A1; ... ; An [T], then DSo(SC) = a and, for 0 < k < n, DSk(SC)= sp( A1 ; ... ; Ak, a). We shall often make use of this fact in the sequel.

5 Examples

Example 1 (continued) The Yale Shooting Scenario (YSS, for short) is an example of the temporal predic­ tion. The intended conclusion is that after performing the actions the turkey is dead and the gun is unloaded.

We calculate DS3 (YSS) . 11 DS3 (Y SS) = sp(load; wait; shoot, a 1\ -,/) = sp( shoot, sp( wait, sp( load, a 1\ -,/))) = sp(shoot, sp(wait, II\ ((a 1\ T) V (a 1\ F)))) = sp( shoot, sp( wait, II\ a)) = sp(shoot, II\ a) =(...,a 1\ -,/1\T 1\T)v(-,a 1\ -,[I\ T 1\ F)v(-,/1\ II\ a) :=-,af\-,1.

Since DS3(Y SS) f- -,a 1\ ...,[, we conclude that in the final state the turkey is dead and the gun is unloaded. ·

Example 2 (Russian Turkey Scenario)

The Russian Turkey Scenario (RTS, for short) is an ex­ ample of the temporal prediction, where actions with random effects are allowed. 12 The world of the sce­ nario is the same as for the Yale Shooting Scenario, but wait is replaced by spin. The scenario is given by [a 1\ -,/]load; spin; shoot [T]. The intended conclusion is that nothing can be said whether the turkey is alive or not in the final state. We calculate

DSa(RTS) = sp(load; spin; shoot, a 1\ -,/) = sp(shoot, sp(spin, sp(load, a 1\ -,/))) = sp(shoot, sp(spin, II\ ((a 1\ T) V (a 1\ F)))) = sp(shoot, sp(spin, II\ a)) = sp(shoot, (II\ a)[l +-- T] V (1/\ a)[l +-- F]) = sp(shoot, a) = (-,a 1\ -,[ 1\ T) V (-,a 1\ -,[ 1\ F) V ( ...,[ 1\ a) = -,[,

Since DSa(RTS) If a and DSa(RTS) If -,a, no conclu­ sion can be derived with respect to whether a or -,a holds in the final state. ·

Example 3 (Stanford Murder Mystery) Con­ sider the following problem (SM M). 13 The turkey is alive in the initial state, and after the actions shoot and wait are successively performed, it is dead. The story can be represented by the following scenario: [a] shoot; wait [-,a]. The question we are interested in is when the turkey died and whether the gun was orig­ inally loaded (the temporal postdiction). The intended conclusion is that the gun was loaded in the initial state and the turkey died during the shooting. We calculate

DS0 (SM M) a 1\ -,w/p(shoot; wait, a) a 1\ -,w/p(shoot, wlp(wait, a)) a 1\ -,w/p(shoot, a) a 1\ ...,( (I :::> F) 1\ ( ...,[ :::> a)) a 1\ I.

Since DS0 (SM M)f- I, we immediately conclude that the gun was loaded in the initial state.

Now, we calculate DS1(SMM).

Since DS1 (SM M)f- -,a, we infer that the turkey was dead after performing the action shoot. ·

11 Note the use of the symbols "=" and "=" during the calculation. We write X= Y if Y is obtained from X by em­ ploying the semantics of wlp or sp, whereas X = Y indicates that X and Y are logically equivalent.

12 This example is from [Sandewall, 1994].

13 This example is from [Baker, 1991].

6 Ramification problem

The ramification problem concerns efficient representa­ tion of the indirect effects of actions. In this paper we limit ourselves to the simplest class of ramifications, namely those introduced by domain constraint axioms.

The domain constraint axioms describe general facts that are assumed to hold in any state of the dynami­ cally changing world under consideration. If o: is such an axiom, then some fluents occurring in o: may change their values even if these fluents are not included in the action's description. Consider, for instance, the Yale Shooting Scenario, augmented with the domain con­ straint axiom a = ·d, where d stands for dead. Given this axiom, the action shoot makes the turkey not only not alive, but also dead (provided, of course, that the gun is loaded) .

Clearly, when the domain constraint axioms are in­ volved, a scenario [o:] A1; . . . ; An [,8] should not be re­ garded as representing the class of computations initially o: and finally ,8 under control of A1; . .. ; An, but rather as the class initially o:, finally ,8 and always 1 under control of A1; . . . ; An, where 1 is the conjunction of all domain constraint axioms associated with the scenario. Unfortunately, changing the class of computations only is not always sufficient to properly deal with the domain constraint axioms. To see why, consider an illustrating example.

E:xample 4 Consider the shooting language supplied wtth a new fluent w, standing for walking. Let DC be a domain constraint axiom given by w :J a. Let W SS be the scenario [w 1\ I] shoot [T] .

The intended conclusion is that the turkey is not alive and not walking in the final state. We calculate:

The description of the final state is inconsistent. ·

The inconsistency we have arrived at is due to the fact that the fluent w obeys the law of inertia. In our approach, all fluents that are not explicitly affected by an action retain their values when the action is performed. While this is a nice property from the standpoint of the frame problem, it leads to some difficulties when actions with indirect effects are involved.

To deal with domain constraint axioms, we need a mechanism which, for a given action A, releases chosen fluents from obeying the law of inertia when the action A is executed. Fortunately, the release mechanism can be easily implemented in our formalism. Suppose that !I, ... ! fn are flu.ents which are to be released during executmg an act10n A. To achieve the desired effect A should be replaced by A; release(ft); ... ; release(fn) where release(!;) is the command

----- 14The release pseudo-command corresponds closely to

Example 4 (new solution) To properly deal with WSS scenario, the fluent w should be released when the action shoot is performed. Thus, we replace shoot by shoot* given by shoot; release(w). The description of the initial state is w 1\ II\ DC. We calculate:

Since DS1 (Y SS) 1\DC 1- ·a 1\ ·w, we conclude that the turkey is not alive and not walking in the final state. ·

We now provide a general method to reason about action scenarios with domain constraint axioms. We assume here that the number of these axioms is finite so that they can be always regarded as a single formul~.

Let SC [o:] A1; . .. ; An [,8] be an action scenario and suppose that DC is the conjunction of all domain constraint axioms assiociated with SC. As­ sume further that the fluents fl, .. . , f;m; are to be re­ leased from the law of inertia when the action A; is executed. We write A* to denote the sequential com­ position A;; release(fl ); ... ; release (Jim;). The descrip­ tion of the kth_state of SC with respect to DC written DS{!c (SC), is the formula given by '

where spDC and wlpDC are defined by the equations (5) - (8), wtth 1 replaced by DC and S; (0 < i < n) replaced byAt. -

Theorem 3 immediately implies:

Th.eorem 5. Let SC = [o:] A1 ; · .. ; An [,8] be an act10n scenano, DC be the conjunction of domain con­ ~train axioms and suppose that Ai (0 :::; i :::; n) is spec­ tfied as before. A formula 1 is assured to hold after performing the actions A1; . .. ; Ak if DS{!c (SC) 1- 'Y· ·

Example 5 Consider a variant of the Yale Shooting Scenano. There are four fluents: a, /, d and u, standing for a~ive, loaded, damaged (gun) and usable (gun), re­ spectively. The actions are: load, and shoot. Finally, we have a domain constraint axiom DC given by I 1\ ·d :::: u. The meaning of the actions is as before with one proviso: to successfully perform the action shoot, the gun must be usable. The translation of the new version of shoot is if u ---+ a := F; I := F ~ ·u ---+ skip fi and its semantics is given by

• wlp(shoot, o:) = (u :J o:[a +- F, l +- F]) 1\ (·u :J o:)
• sp(shoot,o:) = sp(shoot,o:) = ·a/\·l/\3a,l.(u/\ 0:) V ·U 1\ 0:.

Beca~se the fluent u is indirectly affected by load and shoot, 1t must be released when any of these actions is performed.

Sandewall's [1994] occlusion device. See also [Kartha and Lifschitz, 1994].

Let VY SS be the scenario [-.d) load; shoot [T]. The intended conclusion is that the turkey is not alive and the gun is unloaded, unusable and not damaged in the final state.

Since the fluent u is released during performing the ac­ tions load and shoot, we define load· = load; release( u) and shoot· = shoot; release(u). Performing straight­ forward calculations, one gets

In view of (10), we immediately conclude that the turkey is not alive an~ the gun is unloaded, unusable and not damaged in the final state. ·

7 Conclusions

We have applied Dijkstra's semantics for programming languages to formalization of reasoning about action and change. We believe that the results reported here are interesting and worth of further investigation. The pre­ sented approach can be employed to represent a broad class of action scenarios, including those where actions with random and indirect effects are permitted. In ad­ dition, both temporal prediction and postdiction tasks can be properly dealt with, without requiring initial or final situations to be completely specified. The major advantage of our proposal is that it is very simple and more effective than many other approaches directed at formalizing reasoning about action and change.

As we remarked earlier, recent work of Sandewall [1994] provides a very general framework to study log­ ics of action and change. Obviously, the question of how our proposal fits in this framework should be investigated and will be pursued in the future. It is also interesting to compare our approch with Ano language introduced recently by Kartha and Lifschitz [1994].

The task of. implementation is another point of in­ terest. Calculating DSk(SC), for a given scenario SC, amounts to simple syntactic manipulations on formulae and can be performed very efficiently. The only compu­ tational problem is to determine whether a given formula can be derived from the description of the state under consideration. This task can be realized by a theorem prover appropriate for the logic in which the effects of actions are described.

Acknowledgements

We would like to thank Wladyslaw M. Turski, Wlodek Drabent and Andrzej Szalas for their comments on the previous draft of this paper.