Reasoning by Regression: Pre- and Postdiction Procedures for Logics of Action and Change

1 Introduction

The co_ntributions of this paper are the following: RegressiOn-based pre- and postdiction procedures for PMON with metric time, and an in depth analysis of problems with regression that occur when nondetermin­ istic actions are introduced. We also identify and deal with problems in previous work by Lin (1996].

Lin [1996] proposes a causal minimization framework in SitCalc (Situation Calculus), where effects of nonde­ terministic actions can be specified. He then identifies a class of such actions for which regression can be used as a reasoning mechanism. Within the constraints of t?e SitCalc formalism, Lin provides an elegant exten­ SIOn to handle nondeterminism, but one can probably do somewhat better. We will show this, using PMON as a vehicle.

PMON is a logic for action and change proposed by S~ndewall [1994]. PMON is proven to be correctly ap­ phcable to problems involving explicit time, context­ dependent actions, nondeterministic actions and actions with duration. Doherty [1994] gives a first-order formu­ lat_ion of PMON, with a second-order circumscription axiom and shows that it is always possible to reduce the second-order theory to first-order logic. In [Gustafsson and Doherty, 1996] PMON is further extended to handle causal constraints. In this paper we will use a subset of PMON with metric time (natural numbers) and propo­ sitional fluents.

·This research has been supported by the Swedish Re­ search Council for Engineering Sciences (TFR) grants 93-183 and 96-728.

There are three problems with Lin's proposal: First, he needs to explicitly enumerate all nondeterministic ef­ fects of an action in syntax, thus encountering a possible combinatorial explosion. Secondly, he has to introduce an "oracle" predicate Case, which "knows" the outcome of a nondeterministic action before it has occurred. The intuitive meaning of this oracle is unclear. Thirdly, the effects of nondeterministic actions are not allowed to de­ pend on the situation in which the action is invoked for regression to work properly. '

In PMON, we deal with each of the three problems in the following manner: The first is taken care of by the formalism, since nondeterministic effects can be repre­ sented succinctly. For the the second and third problem we rely on our minimization of change policy, which only allows an action to have certain effects if the correspond­ ing condition is satisfied. This behavior is similar to the behavior of conditional statements in programming languages, which enables us to use a classical computer science tool, Dijkstra's weakest liberal precondition op­ er_ator, wlp, for regression, which, as it turns out, deals with the problems.

The comparison between our and and Lin's approach will be informal due to the use of different time struc­ tures. We will, however, let Lin's work guide the devel­ opment of the results presented in this paper.

2 Goal Regression in Sit Calc and Lin's Proposal

Initially, goal regression was developed as a plan synthe­ sis method ([Waldinger, 1977], [Pednault, 1986]) . Reiter [1991] provided a situation calculus account for goal re­ gression with a completeness proof. Reiter relies on his solution to the frame problem, in particular the successor state axioms, which are biconditional relations between the values of a fluent after the execution of an action, and the states before the action. The general form of these axioms, for every fluent R, is

where Poss( a, s) is true if the action a is possible to execute in situations, and h(R, s) denotes that the fluent R is true in situation s. The formula rf{(a, s) denotes the conditions under which action a will makeR true in situation s, and rjl (a, s) the conditions that will make R false .

By substituting fluents in the goal with the right hand side of the biconditional in the successor state axioms, the nesting of the do function can be reduced until there finally is a formula only mentioning the situation So, on which a classical atemporal theorem prover can be used. For planning purposes, Reiter's approach relies on completely specified initial states, and cannot handle nondeterministic actions.

Lin introduces a predicate Caused which "assigns" truth values to fluents . In the minimization policy, the extension of Caused is minimized and a no change premise is added to the theory. To illustrate his approach Lin uses the dropping-a-pin-on-a-checkerboard example: There are three fluents, white (to denote that the pin is partially or completely within a white square), black, and holding (to denote that the pin is not on the checker­ board). There are two actions, drop (the pin is drop onto the checkerboard) and pickup. In this paper we will only consider the drop action (which is the only one with non­ deterministic effects), which is formalized as follows:

The Poss predicate is defined, with an action precondi­ tion axiom, as

A problem with this is that the effects of the action have to be explicitly enumerated in the action definition. The number of disjuncts will grow exponentially in the num­ ber of fluents; and may become problematic in imple­ mentations.

3 PMON

In PMON it is possible to model nondeterminism in a more succinct manner. We will present the parts of PMON relevant for this paper. Extensions and details can be found in [Doherty, 1996].

We will use the language £ which is a many-sorted first-order language. For the purpose of this paper we assume two sorts: A sort T for time and a sort F for propositional fluents. The sort T will be the set of nat­ ural numbers.

The language includes two predicate symbols H 1 and Occlude , both of type T x F. The numerals 0, 1, 2, . .. and the symbols s and t, possibly subscripted, denote natural numbers, i.e. constants of type T (time points).

PMON is based on action scenario descriptions (sce­ narios), which are narratives with three components: OBS, a set of observations stating the values of fluents at particular time points, ACT, a set of action laws, and SCD, a set of schedule statements that state which and when (in time) actions occur in the scenario.

Example 3.1 A scenario where the pin initially was held over the checkerboard, then dropped and finally ob­ served to be on a white square (and not on a black) is formalized as

OBS 1 H(O, over JJOard) 1\ -,fl(O, white) 1\ -,fl(O, black)

ACT [s, t]Drop ~ H(s, over _board)--> [s, t]r

SCD (3, 5]Drop

OBS2 H(6, white) 1\ -,fl(6, black),

where [s, t]r is the formula

0

Below, in (3), we will show how [s, t]r can be presented in a succinct way.

In Lin's formalism h(holding, s) is a qualification of the action drop. To illustrate conditions for the action to have effects (context depency), we introduce over _board, that denotes that Drop only has effects if the pin is dropped on the board. Such conditions can be mod­ elled in SitCalc, but not in Lin's framework. This will be further discussed below.

H formulae and Observations

Boolean combinations of H literals (i.e. possibly negated atomic formulae), where every literal mentions the same time point, are called H formulae. An H formula, 6, where every literal only mentions time points, will some­ times be written [s]6. An observation is an H formulae.

Action Laws

A reassignment is a statement [s, t]f:=b, where f E F and b is a truth value symbol (T for true, and F for false) . The statement [s, t]f:=T is an abbreviation of H(t, f) 1\ Vt.s < t ~ t --> Occlude(t, f), and [s, t]f:=F expands to -,fl(t, f) 1\ Vt.s < t ~ t --> Occlude(t, f). A reassignment formula [s, t]a, is a boolean combina­ tion of reassignments, all mentioning the same temporal constants s and t .

1 Not to be confused with h which is the corresponding situation calculus predicate.

An action law is a statement

where A is an action designator (the name of the ac­ tion), s and t are variables (temporal variables) over the natural numbers, each precondf is either a conjunction of H literals only mentioning the temporal variables, or the symbol T, such that the precondf 's are mutually ex­ clusive, and every postcondf is a reassignment formula. Intuitively, ACT contains rules for expanding schedule statements into action axioms, in which the temporal variables are instantiated.

An action is said to be deterministic iff none of its postconditions include disjunctions. An action is ad­ missible if no precondition or postcondition is a con­ tradiction. We will call the conjuncts of an action law branches.

It is necessary that the reassignments in the postcon­ ditions are on a form logically equivalent to a special disjunctive normal form, where each disjunct contains the same ftuents, e.g. for the formula (2) above. Of course, this looks suspiciously similar to Lin's formula­ tion, which was criticised above. But (2) is an abbrevi­ ation of a formula equivalent to

which deals with the problem of compact and intuitive representation. We will use the abbreviated form for readability reasons, but all the constructions in this pa­ per could easily be redone for action effects of the type in (3).

Schedule Statements

A schedule statement is a statement, [s, t]A, such that s and t are natural numbers, s < t, and A is an action designator for which there exists an action law in ACT.

No Change Premises

The occlusion of ftuents that are reassigned captures the intuition of possible change, but we also need a syntac­ tic component that captures the intuition that a fluent cannot change value unless it is occluded. This is taken care of by the no change premise, NCH, formulated as

Action Scenario Description

An action scenario description (scenario) is a triple (oss, ACT, sco), where OBS is a set of observations, ACT a set of action laws, and SCD a set of schedule statements. Furthermore, let seD( ACT) denote a set offormulae such that we for every schedule statement in seD instantiate the temporal variables of the corresponding action law (in ACT) with the two time points in the schedule state­ ment. We will call such formulae action instances.

PMON Circumscription Policy

To minimize change, the action instances are circum­ scribed (by second-order circumscription), i.e. by mini­ mizing the Occlude predicate, and then by filtering with the observations and no change premises . For a scenario description 1 = (oss, ACT, sen) we have

where r is the set of unique names axioms. Doherty [1994] shows that this second-order theory always can be reduced to a first-order theory that provide a completion (or, definition) of the Occlude predicate. For the needle dropping scenario the completion will be the following:

for every combination of t' E { 4, 5} and f' E {over _board, white, black}.

A classical model for a circumscribed scenario will be called an intended model. A scenario is consistent if it has an intended model, else it is inconsistent. We say that a scenario 1 entails a statement [t]lf', and writes 1 f--- [t]<p, iff PMON(1) 1- [t]lf', where 1- denotes classical deduc­ tive inference. Furthermore, a schedule statement [s, t]A is said to entail a statement [t]lf', written [s, t]A f--- [t]<p, iff (0, ACT, (s, t]A) f"v (t]lf'.

The completion of Occlude has a useful ramification: It conditionalizes the branches of the actions in the sce­ nario, i.e. when the completion axiom is added to the theory, it is no longer possible for a precondition to be false while its postconditions are true. This behavior is similar to the behavior of if-then statements in program­ ming languages, and makes it possible to use Dijkstra's wlp formula transformer.

4 Lin's Proposal (Cont'd)

To be able to use goal regression, Lin has to generate successor state axioms. However, this cannot be done in a straightforward way for nondeterministic scenarios. The reason for this is that there are no constraints before a nondeterministic action in a biconditional relation with what holds after the action has taken effect.

Lin deals with this by introducing an "oracle 2 " pred­ icate, Case(n, a, s), which is true iff the nth disjunct of action a has an effect (is true) in situation s . The drop action is, thus, defined as

Lin shows that the new theory is a conservative extension of the previous circumscribed one.

2 A term used by Sandewall for constructs that "know" in advance what the effect of nondeterministic actions will be.

The key here is that a previously nondeterministic ac­ tion is transformed · into a deterministic action, where nondeterminism is simulated by the oracles. Lin sug­ gests that the oracles could be viewed as probabilities of certain effects to take place. However, since he does not develop this idea, the introduction of oracles is not completely convincing, at least not from a knowledge representation point of view. We will, below, present a vehicle to avoid the use of oracles.

Since the actions now are deterministic it is possible to generate successor state axioms, e.g. for white:

Unfortunately, this approach is not as general as it may seem. In fact, goal regression is not possible unless we restrict the problem by disallowing the effects of non­ deterministic action to be conditional. We cannot, e.g., introduce the over _board condition on the effects of the drop action.

5 Dijkstra's Semantics Applied to PMON

Since we cannot generate the desired biconditionals, we would like to automatically generate the "best" possi­ ble condition before the action. Also, such an approach should be able to handle conditional nondeterministic actions, to deal with this particular problem of Lin's proposal. We achieve the result by using a classical com­ puter science approach, the weakest liberal precondition operator, wlp.

In this section we briefly introduce Dijkstra's seman­ tics for programming languages, but in the setting of PMON. We also present theorems which connect the states before and after the execution of actions. Orig­ inally, the theory was developed to give semantics to small programming languages with a higher ordered function . This function was a predicate transformer, that given a command, S, in the language and a machine state, s;, returned a set, W, of machine states such that all states in which S could be executed and terminate in s;, if it at all terminated, belonged to W. This predicate transformer was called weakest liberal precondition, wlp.

Dijkstra's semantic has previously been used in an ac­ tion and change setting in [Lukaszewicz and Madalinska­ Bugaj, 1995] . The language used in there is a small pro­ gramming language, without a notion of explicit time. They do not specifically deal with regression.

Let <p be a H formula, f a fluent and bE {T, F} . We write [s]<p[f <- b] to denote that all H statements (Note: Not the possible negation in front of them) mentioning the fluent f are simultaneously replaced by b, and where the time argument of the H statements is change to s. As a consequence, [s]<pO denotes the replacement of all time arguments in <p with s .

We will informally use the term state for a proposi­ tional interpretation of all fluents at a specific time point.

Definition 5.1 (Weakest liberal precondition, wlp)

Let a and {3 be reassignment formulae, <p a H formula, we define wlp inductively so that, for all fluents f E :F

Furthermore, let [s, t]A be a schedule statement for which the corresponding law has n branches. Then

The second conjunct encodes that if none of the precon­ ditions were true then <p had to be true at the begin­ ning of the action. We define wlp's conjugate, wlp*, as wlp*(S, a)= -,wlp(S, ...,a).D

Example 5.2 We briefly illustrate wlp by computing the weakest liberal precondition for white or black to hold after the Drop action (from example 3.1) . Obvi­ ously, the only way in which we can be guaranteed that white or black is true after Drop is if over _board, or white or black, was true before the action.

Now, we compute wlp([3, 5]1, H(5, white)V H(5, black)). The first conjunct of [3, 5]1, [3, 5]over ..board:=F, will not have any effect on H(5,white)V H(5,black). When wlp is applied to the three disjuncts of [3, 5]1 they will all be computed to T. Thus, wlp([3, 5]1, H(5, white) V H(5, black))= T, and (9) will be equivalent to

(H(3, over ..board)--+ T) 1\ ( ...,fl(3, over ..board) --+ H(3, white) V H(3, black)) = ...,fl(3, over ..board)--+ H(3, white) V H(3, black),

which is what we wanted.D

Note that wlp is applied to the possible effects of an action in ( 4) - (7), and is generalized to complete action instances in (8) .

The correctness of wlp is proven in [Dijkstra and Scholten, 1990]. We will, however, give intuitions for definitions (6) - (8).

Definition (6) is based on a sequential underlying com­ putational model. If we implement wlp we will have to perform the reassignments in some order, and here we choose to first apply a and then {3.

Definition (7) handles norideterminism. It guarantees that no matter which of a or f3 is executed, we will end up in a state satisfying cp. The only states that can guarantee this are those that can start in a and f3 and end in cp.

For (8) we can note that wlp should generate every state, u, such that if a precondition is true in u, wlp applied to the corresponding postcondition and some cp should be true in u too. This excludes every action branch that would not terminate in a state satisfying cp. The second conjunct of (8) makes wlp work exhaus­ tively, i.e. if none of the preconditions are true then cp was true before the action.

The conjugate w/p*([s, t]A, [t]cp) should, analogously to wlp, be interpreted as: "The set of all states at s such that the execution of A in any of them does not end in a state at t satisfying ·cp."

For all the theorems below we assume that the actions are admissible.

Proposition 5.3 [s, t]A f---wlp([s, t]A, [t]cp)--+ [t]cp. Proof (sketch): Follows from the correctness of wlp.D

Corollary 5.4 [s, t]A f-.- [t]cp--+ wlp*([s, t]A, [t]cp).

Proof: Contraposition of the implication yield a for­ mula to which proposition 5.3 is applicable.D

Proposition 5.5 wlp(S, cp) = wlp*(S, cp) hold for de­ terministic actions S.

Proof (sketch): Structural induction over the parts of wlp's definition. For the application of wlp to actions, we heavily rely on the fact that the preconditions are mutually exclusive, and that wlp adds exhaustiveness.D

Proposition 5.6 Let [s, t]A be a deterministic action. Then

for arbitrary formulae cp.

Proof: Follows immediately from propositions 5.3, 5.5, and corollary 5.4.0

Proposition 5.5 provide means for an elegant and straightforward definition of successor state axioms in PMON. We can simply apply wlp to every action and fluent, and thus get the biconditional. However, this does not solve the problem of regression for nondeter­ ministic actions.

6 Regression

With our definition wlp we can now construct regression procedures for pre- and postdiction in PMON. One single procedure for both pre- and postdiction does not exist, and we will argue that wlp is applicable for prediction, while wlp* should be used for postdiction. The way in which observations are handled also differs between the two.

With prediction we mean that, given a scenario, 1, we want to know if a formula, cp, holds after the actions of the scenario are executed. For postdiction we want to know if cp holds at the initial time point of the sce­ nario. For readability, we only consider the cases where no observations occur after the query for prediction and before the query for postdiction.

Algorithm 6.1 (Prediction)

Input is a formula, [t]cp, a scenario, 1, and a time points, such that no observation, or starting point of an action, in 1 occurs at a time point < s. Output is a formula {3 such that 1 f-.- [0]/3--+ [t]cp holds. f3 describes all initial states such that, if the action sequence is started in either of them, the sequence terminates in a state satisfying t.p.

1. r +- t and a +- cp.
2. Repeat the following steps until a formula is re­ turned.
3. (a) If there is an observation [r]8 in 1, then a+­ (8--+ a).
4. (b) If r = s then return a.
5. (c) If there is an schedule statement [t, r]A in 1, then a +- wlp([t, r]A, [r]a) and r +- t, else r +- r- 1 and a+- [r- 1]a0.

D

If 1 is deterministic, then 1 f-.- [0]/3 = [t]cp holds for any f3 returned by the algorithm.

Correctness follows from proposition 5.3.

We illustrate algorithm 6.1 briefly with the scenario in example 3.1 slightly changed: We do not include OBS2. Our goal is to prove that H ( 6, white) is a consequent of the scenario.

Input: cp = H(6, white), 1 =the changed scenario, and s = 0.

First Iteration: r = 6 and a= H(6, white) .

Second Iteration: r = 5 and a= H(5, white).

Third Iteration: The schedule statement [3, r]Drop is found, and wlp([3, 5]Drop, H olds(5, white)) is com­ puted. After the iteration r 3 and a = ·H(3, over ..board) 1\ H(3, white).

Sixth Iteration r = 0 and a = ·H(O, over ..board) !I H(O, white).

In the sixth iteration the observation at time point 0 is considered, so

which is returned by the algorithm.

The returned formula is a contradiction, which tells us that the goal, H(6,white), is not a consequence of the scenario. If the returned formula is a tautology, the goal is a consequent. The third case, when the formula is neither a contradiction, nor a tautology, implies that the formula is a condition at the initial time point for the scenario to entail the goal.

For the postdiction case, we start by taking the last observation and regress back to the initial time point. We are now interested in regression results that are im­ plied by the conditions after the action is performed, since the observations are parts of the axiomatization. We will therefore make use of corollary 5.4 for this algo­ rithm.

Algorithm 6.2 (Postdiction)

Input is a formula, [O]<p, a consistent action scenario de­ scription, 1, and a time point s, where an observation, [s]6 , occurs, and no observation occurs at any time point > s . Output is a formula f3 such that every initial state that is consistent with the scenario, and no other state, is a model of {3.

1. Repeat the following steps until a formula is re­ turned.
2. (a) If there is an observation [r]6 in 1, then a +­ (6Aa) .
3. (b) If r = 0 then return a.
4. (c) If there is a schedule statement [t, r]A in 1, then a +- wlp*([t, r]A, [r]a) and r +- t , else r +- r- 1 and a+- [r- 1)a0.

0

When a formula f3 has been generated we can choose if we want to prove that the scenario is consistent with the initial states l.p by proving that <p ---+ f3 holds. If we want to prove that 1 f"-- [O)<p, we prove that f3 ---+ <p holds.

Correctness follows from corollary 5.4.

To illustrate algorithm 6.2, we again look at exam­ ple 3.1. This time we remove OBSl, and input OBS2, H(6 , white) A ·H(6, black) , to the algorithm. Without going into details, we can note that

which coincide with our intuition.

The intuition for the difference of how observations are handled by the algorithms is that for prediction, we want observations to verify the computation results, i.e. to described state sets that are subsets of the regression result, and, for postdiction, the observation should filter out all state not being consistent with it.

7 Conclusion and Future Work

We have presented a computational strategy for predic­ tion and postdiction for a large subset of PMON. The strategy is based on Dijkstra's weakest liberal precondi­ tion operator. We have shown that wlp and its conjugate wlp* have different properties for nondeterministic sce­ narios and that the former is applicable for prediction, and the latter for postdiction. For deterministic scenar­ ios, the two operators coincide, thus providing a formal foundation for generating successor state axioms.

The formalism used and the results provided in this paper deals with three problems identified in recent work by Fangzhen Lin. First, the choice of PMON deals with the problem of explicit enumeration of effects of nondeterministic actions. Secondly, wlp enables re­ gression over nondeterministic actions without any ora­ cle features or transformations to deterministic action. Thirdly, wlp handles nondeterministic actions with con­ ditional effects properly.

We think that this approach is promising, and we will use wlp for implementations of a PMON planner, soon to appear online.

Acknowledgements

Thanks to Patrick Doherty, Thomas Drakengren, Silvia Coradeschi, and Joakim Gustafsson for help and com­ ments.