Property Persistence in the Situation Calculus

1 Introduction

The situation calculus [Pirri and Reiter, 1999] has long been one of the most popular formalisms for reasoning about dynamic worlds. It has more recently become a popular choice for implementing systems situated in a dynamic world, as it offers, among other advantages: a formalism based in firstorder logic; an elegant monotonic solution to the frame problem; and an effective reasoning procedure for the projection problem [Reiter, 1991]. Coupled with logic programming languages such as Prolog, it has facilitated the implementation of a wide range of systems.

The foundational axioms of the situation calculus include a second-order induction axiom defining the set of all situations [Reiter, 1993]. Sentences that contain only existential quantification over situation terms can be proven without the induction axiom and so are more amenable to automated reasoning [Pirri and Reiter, 1999]. It is therefore important for systems built on a situation calculus theory of action to limit queries to existential form. Much of the work on implementing systems with the situation calculus has been on reducing the number of axioms required to answer a given query, to allowmore efficient reasoning.

∗This research was supported by a grant from the Australian Research Councils (ARCs) Centre for Perceptive and Intelligent Machines in Complex Environments (PIMCE).

Unfortunately there are many reasoning tasks that require universal quantification over situations. For example, it is often desirable to show that no situation can satisfy a particular goal. In this paper we are interested in a subset of such queries which we refer to as persistence queries: under a particular situation calculus theory D, and given some property φ and situation s, determine whether φ will hold in all situations in the future of s:

The need for second-order logic has traditionally limited automated reasoning about such queries. We introduce a new approach that is similar in spirit to the regression operator of [Reiter, 1991]: define an operator that transforms a formula φ into a formula PD[φ], such that φ persists in s if and only if PD[φ] holds in s. We term this the persistence condition of φ, and show how to calculate it in a form suitable for effective automated reasoning.

To determine PD[φ], we first define an operator P 1D [φ] that holds in s whenever φ holds in s and all its immediate successors. The persistence condition is shown to be a fixed-point of this operator, which can be sought using a straightforward iterative algorithm. Since this requires only first-order reasoning with a limited number of axioms, the result is an effective procedure with which to answer a family of queries that universally quantify over situations.

The paper is organized as follows: Section 2 gives a brief introduction to the situation calculus, formally defines the persistence problem, discusses related work and gives several examples of important persistence queries; Section 3 formally defines the persistence condition, presents an algorithm that calculates it, shows that the algorithm is correct and discusses the conditions necessary for completeness; and Section 4 concludes with a summary of our results.

2 Background

The situation calculus is a many-sorted language of first-order logic augmented with a second-order induction axiom. It has the following sorts: Action terms are functions denoting individual instantaneous events that can cause the state of the world to change; Situation terms are histories of the actions that have occurred in the world, with the initial situation represented by S0 and successive situations built up using the function do : Action × Situation → Situation; Object terms represent any other object in the domain. It further distinguishes Fluents as predicates or functions representing properties of the world that may change from one situation to another, and so take a situation term as their final argument. For a detailed description consult [Pirri and Reiter, 1999].

A basic action theory is a set D of situation calculus sentences (with a specific syntactic form as specified in [Pirri and Reiter, 1999]) that describes a particular dynamic world. Queries about the behavior or evolution of the world are posed as logical entailment queries relative to this theory. It consists of the following disjoint sets: the foundational axioms of the situation calculus (Σ); successor state axioms describing how fluents change between situations (Dss); precondition axioms indicating when actions can be performed (Dap); unique names axioms ensuring that action terms are distinct (Duna); and axioms describing the value of fluents in the initial situation (DS0 ):

The foundational axiom of most import for this paper is the induction axiom, which defines the set of all situations as the least set containing S0 and closed under application of the do function, as follows:

The fundamental importance of this axiom is described in [Reiter, 1993]. Much research has focused on identifying sentences of the situation calculus that can be proven without this axiom, and thus require only first-order logic. Our work continues this tradition.

There is a distinguished predicate P oss(a, s) that indicates when it is possible to perform an action in a given situation. The set of action precondition axioms Dap contains one axiom for each type of action A, of the general form:

Here ΠA represents a uniform formula (see below) defining action possibility on a per-action basis.

It is often useful to introduce analogous predicates to describe different aspects of action performance. For example, a predicate CantObs(agt, a, s) could indicate when an agent will be unable to observe the occurrence of an action. Such predicates are easily incorporated into a basic action theory by axiomatizing them in Dap in the same manner as Poss. We refer to these predicates in general as action description predicates, and use the meta-variable α to represent an arbitrary such predicate.

The uniform formulae as defined in [Pirri and Reiter, 1999] can be thought of as properties of the state of the world. They are basically logical combinations of fluents referring to a common situation term, which cannot mention action description predicates nor compare situation terms. We will use the meta-variable φ to refer to an arbitrary uniform formula.

It is often useful to determine the truth of a property at a given situation. The formula φ[s] represents the uniform formula φ with all occurrences of its unique situation term replaced by the situation s.

2.1 Ordering over Situations

Situations form a tree with S0 at the root and do constructing child situations from parents. There is a basic ordering relation ⊏ defined by the following foundational axioms:

Where s ⊑ s′ is the standard abbreviation of s ⊏ s′ ∨ s = s′ . It is frequently useful to restrict the situations under consideration to those possible in the real world, by defining an ordering relation < over only these "executable" situations:

Many results of the situation calculus are derived relative to the executable situations - for example, [Reiter, 1993] develops an induction principle for all situations where S0 ≤ s. This notation is so useful that we propose a parametrization of it: let α be an action description predicate specifying the actions of interest, then define the "α-ordering" over situations as follows:

The standard ordering over executable situations is clearly <Poss. If s is thought of as the "current situation", then s <α s′ means that s′ is one potential future, and all actions that will occur in that future satisfy α.

2.2 Effective Reasoning

Answering an arbitrary situation calculus query ψ involves, in general, an entailment problem in second-order logic (SOL):

This can be problematic for efficient automated reasoning. Fortunately, there exist particular syntactic forms for which some of the axioms in D are not required. In [Pirri and Reiter, 1999] the "∃s sentences" are defined as those in which every situation variable is in the scope of a positive existential quantifier. They show that such sentences can always be proven without the induction axiom (I) and hence are answerable by first-order logical entailment (FOL):

Such queries can be approached with standard first-order reasoning systems. To increase the efficiency of reasoning it is desirable to eliminate further axioms from D, which [Pirri and Reiter, 1999] show possible for several syntactic forms.

Axiom reduction is also the key idea behind the regression operator, the principal tool for effective reasoning in the situation calculus [Reiter, 1991]. The regression operator RD is a syntactic manipulation whose behavior can be summarized 1

1 The full behavior of RD is beyond the scope of this paper. Experienced readers please note that we use the single-step version of the regression operator, as in [Lin and Reiter, 1994]. Since any formula uniform in do(a, s) is by definition single-step regressable, the development below omits the traditional qualification that formulae must be regressable.

for our purposes as follows: given a formula φ uniform in do(a, s), regression transforms it into a formula RD[φ] that is uniform in s and is equivalent to φ under the theory of action D:

Regression also replaces instances of the P oss predicate with appropriate instantiations of the corresponding uniform formula from the axioms in Dap, and other action description predicates can easily be treated in the same way. In order to regress such a predicate over an action variable one must assume that there are only a finite number of action types, so that it can be replaced with the disjunctive closure of its definitional axioms. We assume this restriction throughout.

If φ refers to a situation that is rooted at S0, repeated applications of the regression operator (denoted by R∗D ) can transform it into an equivalent formula uniform in the initial situation. The successor state and action precondition axioms are "compiled into" the regressed formula, and so are not required for the reasoning task:

The trade-off is that the length of R∗D [φ] may be exponential in the length of φ. In practice this is typically more than compensated for by the reduction in the number of axioms required, and regression has proven a very effective technique.

2.3 Property Persistence

One important form of situation calculus query is to ask whether a given property φ will hold in all future situations of a given situation s, as well as at s itself:

More generally, one may wish to limit the futures considered to those brought about by a certain class of actions α:

In words this states "given that all subsequent actions satisfy α, φ will remain true" or, more succinctly, "φ persists under α". We term queries of this form property persistence queries, and they are involved in many useful reasoning tasks. The following are a small selection:

Goal Impossibility: Given a goal G, establish that there is no possible situation in which that goal is satisfied:

Goal Futility: Given a goal G and situation s, establish that the goal cannot be satisfied in any possible situation in the future of s:

Note how this is different from goal impossibility: while the agent may have initially been able to achieve its goal, the actions that have subsequently been performed have rendered the goal unachievable. Agents would be well advised to avoid such situations.

Checking State Constraints: This is a variant of goal impossibility - show that the constraint can never be violated.

Need for Cooperation: To establish that it is absolutely necessary to cooperate with another agent, an agent must determine persistence under actions performed by itself:

Assuming that the action description predicate OwnAction has been defined to identify actions performed by the agent in question, this states that no situation in the future of s in which all actions were performed by that agent can satisfy G. If this is the case, it will need to cooperate with another agent in order to achieve its goal.

Knowledge under Partial Observability: In recent unpublished work we develop a new account of knowledge in the situation calculus when not all actions are observable by all agents. To facilitate reasoning in this formalism, agents must be able to reason about what cannot be changed by actions that they cannot observe, a form of persistence query.

Due to the universal quantification over situations, the techniques for effective automated reasoning in Section 2.2 cannot be applied to persistence queries. This paper is devoted to developing of a complementary technique for handling such queries.

2.4 RelatedWork

While there is a rich and diverse literature base for the situation calculus, there appears to have been little work dealing with universally quantified queries. The work of [Reiter, 1993] shows how to handle such queries by hand using an appropriate instantiation of the induction axiom, but makes no mention of automating this reasoning.

Other work considering persistence focuses exclusively on verifying state constraints. These are uniform formulae that must hold in every possible situation, a highly specialized form of persistence query. The work of [Lin and Reiter, 1994] "compiles away" the induction axiom when verifying a state constraint, by means of the following equivalence:

Verification of a state constraint can thus be reduced to reasoning about a universally quantified uniform formula using only the unique names axioms, a comparatively straightforward reasoning task. This problem is also approached by [Bertossi et al., 1996], who develop a system for automatically verifying state constraints based on an induction theorem prover.

However, there are many issues related to persistence that are not addressed by such work, including: persistence at situations other than S0; action description predicates other than Poss; how to combine notions of persistence and regression; and determining what additional conditions may be necessary to guarantee the persistence of φ. As our treatment of persistence can provide a concrete basis for these considerations, it is significantly more general than existing work.

3 The Persistence Condition

For implementing persistence queries in practical systems, we clearly need to transform the query into a form suitable for effective reasoning. Specifically, we will transform a persistence query based at s into the evaluation of a uniform formula at s, which can be done effectively using the regression operator. We need some transformation of a property φ and action description predicate α into a uniform formula PD[φ, α] that is true at precisely the situations in which φ persists under α, given a particular action theory D. We call PD the persistence condition of φ under α.

Definition 1. The persistence condition PD[φ, α] is a uniform formula that is the weakest precondition for the persistence of φ under α, given a basic action theory D without the initial situation axioms. That is:

Defining PD to be independent of the initial world state allows an agent to calculate it regardless of what (if anything) is known about the actual state of the world. To see how PD may be calculated, consider the weaker notion of a formula persisting to depth n in a situation:

Definition 2. A uniform formula φ persists to depth 1 under α in situation s when the formula P 1D [φ, α] holds in s, as defined by:

More generally, for any n ≥ 0, a uniform formula φ persists to depth n under α in situation s when the formula P nD [φ, α] holds in s, as defined by:

Note that P 1D is a literal encoding of the requirement "φ holds in s and in all its direct successors". Since α is an action description predicate and φ is a uniform formula, the expression α(a, s) → φ[do(a, s)] can always be regressed and the result will always be uniform in s. Successive applications of P 1D assert persistence to greater depths.

Intuitively, one would expect PD[φ, α] to be a fixed-point of P 1D [φ, α], since PD[φ, α] implies persistence up to any depth. Such a fixed-point can then be calculated using standard iterative approximation techniques. To show that this is in fact the case we require a number of theoretical results, presented below.

3.1 Formal Development

We begin by adapting two existing results involving induction to operate with our generalized ≤α notation, and be based at situations other than S0:

Proposition 1. For any action description predicate α, the foundational axioms of the situation calculus entail the following induction principle:

Proof. A trivial adaptation of theorem 1 in [Reiter, 1993].

Proposition 2. For any basic action theory D, uniform formula φ and action description predicate α:

Proof. A straightforward generalization of Lemma 5 in [Lin and Reiter, 1994], utilizing Proposition 1.

Proposition 2 will be key in our algorithm for calculating the persistence condition. It allows one to establish the result "if φ holds in s, then φ persists in s" by checking entailment of a uniform formula by the unique names axioms, a straightforward first-order reasoning task.

Next we must formalize some basic relationships between PD and P nD , as follows:

Lemma 1. Given a basic action theory D, uniform formula φ and action description predicate α, then for any n:

That is, φ persists under α iff P nD [φ, α] persists under α.

Proof. By the definition of P nD , any s′ that falsifies the righthand side of this equivalence will also falsify the left-hand side, and vice-versa.

Lemma 2. Given a basic action theory D, uniform formula φ and action description predicate α, then for any n:

Proof. PD[φ, α] implies the persistence of φ by definition, which implies P nD [φ, α] by Lemma 1.

We are now equipped to prove the major theorem of this paper: that if P nD [φ, α] implies P n+1 D [φ, α], then P nD [φ, α] is equivalent to the persistence condition for φ under α.

Theorem 1. Given a basic action theory D, uniform formula φ and action description predicate α, then for any n:

Proof. For the if direction, we first see by the definition of P 1D that equation (1) is equivalent to:

which by Proposition 2 implies the persistence of P nD [φ, α] under α. By Lemma 1 this implies the persistence of φ under α, which in turn implies PD[φ, α], giving:

By Lemma 2 this implication is in fact an equivalence, yielding equation (2) as required.

The only if direction is a straightforward reversal of this reasoning: PD[φ, α] implies the persistence of φ, which implies the persistence of P nD [φ, α], which implies (1) by Proposition 2.

Since P n+1 D [φ, α] → P nD [φ, α] by definition, equation (1) identifies P nD [φ, α] as a fixed-point of the P 1D operator, as our initial intuition suggested.

3.2 Algorithm for the Persistence Condition

Since we can easily calculate P nD [φ, α] for any n, we have a straightforward algorithm for determining PD[φ, α]: search for an n such that

Since we expect P nD [φ, α] to be simpler than P n+1 D [φ, α], we should look for the smallest such n. Algorithm 1 presents an iterative procedure for doing just that.

Algorithm 1 Calculate PD[φ, α]

pn ⇐ φ pn1 ⇐ P 1D [pn, α] while Duna ̸|= ∀s . pn[s] → pn1[s] do pn ⇐ pn1 pn1 ⇐ P 1D [pn, α] end while return pn

Note that the calculation of P 1D [φ, α] is a straightforward syntactic transformation and so requires no further treatment.

Correctness

If algorithm 1 terminates, it terminates returning a value of pn for which equation (1) holds. By Theorem 1 this value of pn is equivalent to the persistence condition for φ under α. The algorithm therefore correctly calculates the persistence condition.

Note that equation (1) holds when P nD [φ, α] is unsatisfiable for any situation, as it appears in the antecedent of the implication. The algorithm thus correctly returns an unsatisfiable condition (equivalent to false) when φ can never persist under α.

Completeness

As Theorem 1 is an equivalence, the only source of incompleteness will be failure to terminate. Algorithm 1 may fail to terminate for two reasons: the loop condition may never be satisfied, or the first-order logical inference in the loop condition may be undecidable and fail to terminate.

The later indicates that the basic action theory D is undecidable. While this is a concern, it affects more than just our algorithm - any system implemented around such an action theory will be incomplete. Thus, with respect to this source of incompleteness, our algorithm is no more incomplete than any larger system it would form a part of.

The former is of more direct consequence to our work, and raises two questions: is the persistence condition guaranteed to exist, and is it guaranteed to be reachable in a finite number of iterations? Since P 1D is clearly monotone, the constructive proof of Tarski's fixed-point theorem [Cousot and Cousot, 1979] guarantees the existence of a fixed-point that can be calculated via transfinite iteration, as performed by our algorithm. Moreover, this will be the least fixed-point greater than φ, a satisfying confirmation of correctness since the persistence condition must be the weakest precondition for the persistence of φ.

Unfortunately, there is no guarantee that this fixed-point can be reached via finite iteration, which is required for termination. Indeed, it is straightforward to construct a fluent for which the algorithm never terminates: consider a fluent Fp(x, s) taking integers x, that is affected by a single action that makes it false whenever Fp(x + 1, s) is false. Letting α be vacuously true, the sequence of iterations produced by our algorithm would be:

The persistence condition in this case is PD[Fp(x, s)] ≡ ∀y . x ≤ y → Fp(y, s), and while this is the limit of the iteration it is clearly unachievable in any finite number of steps.

P 1D operates over the set of equivalence classes of formulae uniform in s, and the theory of fixed-points requires that this set be a well-founded partial order to guarantee termination of an iterative approximation algorithm. There are certain classes of basic action theory for which this well-foundedness can be guaranteed. The most obvious is theories with finite action and object domains, in which the set of equivalence classes is finite. Another is the case where successor-state axioms refer only to the direct arguments of their fluents, in which case repeated applications of P 1D will pick out a subset of the equivalence classes that refers to a finite number of objects, giving the same guarantee.

In general, termination requires that repeated applications of the successor-state axioms (via the regression operator) do not construct infinite chains. We are currently investigating syntactic restrictions on successor state axioms that can enforce this requirement, and have found it to be easily met in practice. We are also investigating more advanced fixedpoint algorithms that may give better efficiency and termination guarantees.

Effectiveness

Our algorithm replaces a single reasoning task based on the full action theory D with a series of reasoning tasks based on the unique names axioms Duna. Is this a worthwhile tradeoff in practice? The following points weigh strongly in favor of our approach:

First and foremost, we avoid the need for the second-order induction axiom. All the reasoning tasks can be performed using standard first-order reasoning, for which there are many high-quality automated provers. Second, the calculation of PD only reasons based on the unique names axioms, which as discussed is a comparatively straightforward task. Third, PD[φ, α][s] is in a form amenable to regression, a standard tool for effective reasoning in the situation calculus. Fourth, the persistence condition for a given φ and α can be cached and re-used for a series of related queries about different situations, a significant gain in amortized efficiency. Finally, in realistic domains we expect many properties to fail to persist beyond a few situations into the future, meaning that our algorithmwill require few iterations in a large number of cases.

Of course, we also inherit the potential disadvantage of the regression operator: the length of PD[φ, α] may be exponential in the length of φ. As with regression, our experience thus far has been that this is more than compensated for by the reduced number of axioms required for reasoning.

3.3 Applications

The persistence condition is readily applicable to the persistence query problems given in Section 2.3. Since PD yields a uniform formula, the techniques outlined in Section 2.2 can be directly applied to the following transformed queries.

Goal Impossibility: Given a goal G, establish that there is no possible situation in which that goal is satisfied:

The persistence condition of ¬G with respect to action possibility allows goal impossibility to be checked easily.

Goal Futility: Given a goal G and situation s, establish that the goal cannot be satisfied in any possible situation in the future of s:

Precisely the same formula is required for checking goal impossibility and goal futility. This highlights the advantage of re-using the persistence condition at multiple situations. Our approach makes it feasible for an agent to check for goal futility each time it considers performing an action, and avoid situations that would make its goals unachievable.

Checking State Constraints: This can be handled as per goal impossibility above. A state constraint φ must satisfy:

If this is not the case then PD[φ, Poss] indicates the additional conditions that are necessary to ensure that φ persists, which may be useful in adjusting the action theory to accommodate the constraint.

Need for Cooperation: To establish that it is absolutely necessary to cooperate with another agent, an agent must determine persistence under actions performed by itself:

Knowledge under Partial Observability: To know φ in a world where actions may be unobservable, an agent must know that φ will persist under any actions that it would be unable to observe. This results in a regression rule for knowledge of the form:

4 Conclusions

We have developed an algorithm that transforms persistence queries, a very general and useful class of situation calculus query, to a form that is amenable to standard techniques for effective reasoning in the situation calculus. The algorithm is based on iterative application of the standard regression operator, and uses only first-order reasoning with a small number of axioms. Our algorithm is shown to be correct, and complete given some basic restrictions on the theory of action.

Our approach generalizes previous work on persistence in several important ways. It can consider sequences of actions satisfying a range of conditions, not just the standard ordering over possibility, enabling us to treat problems such as need for cooperation and knowledge under partial observability. It can establish that properties persist in the future of an arbitrary situation, not necessarily the initial situation, enabling us to answer the question of goal futility. The results of calculating the persistence condition can be cached, allowing for example the goal futility question to be efficiently posed on a large number of situations once the persistence condition has been calculated. Finally, the fact that PD operates similarly to the standard regression operator RD allows them to interact in non-trivial ways, such as in the regression of knowledge formulae under partial observability of actions.

As a result, we have significantly increased the scope of queries that can be effectively posed in practical systems built on the situation calculus.