A Classification of First-Order Progressable Action Theories in Situation Calculus

1 Introduction

The situation calculus is a logical language that is designed for reasoning about action and change [McCarthy and Hayes, 1969]. A basic action theory (BAT) [Reiter, 2001] is a wellstudied type of theory in this language that describes what holds in the initial state in a given domain, as well as how the domain evolves under the effects of the available actions. Such theories have been used to model various application domains, including the environment that a robotic assistant operates in, in order to provide deliberation capabilities as the basis for pro-active or goal-oriented behavior, e.g., [Reiter, 1993; Levesque et al., 1997; De Giacomo et al., 2009].

One of the main reasoning tasks that BATs facilitate is different versions of the so-called projection problem, that is, using entailment over this logical theory to answer queries about the future evolutions of the initial state. For example, one can formalize queries of the form "Is it true that condition c will be true after actions a1, . . . , an have been performed?" or "Is it true that c′ can never be true after action a′ is performed?". As BATs are based on first-order logic, this task is quite difficult, in fact not decidable in the general case.

The so-called progression problem is the problem of updating the logical theory when actions are actually executed in the world. Essentially, a BAT is like an elaborate database that holds static information about the initial state and its possible evolutions. When a particular action a1 is actually executed, the BAT can be still used to answer queries about the current state using queries of the form "Is it true that c is true after a1 is executed?", and similarly for queries about the future of the current state. Nonetheless, as more and more actions are executed this quickly becomes impractical. For example, consider a robotic assistant that after a few hours or days of operation may have to answer queries of the form "is it true that c is true after a1, . . . , a10,000 are performed?", only to talk about its current state. Progression is concerned with updating the description of the initial state in a way that is logically correct. This is also a very difficult task as in general second-order logic is required [Lin and Reiter, 1997].

Most of the work in this area lies within the two extremes of the trade-off between expressiveness and efficiency in the following sense. (i) On the one hand, work related to the theoretical framework of unrestricted action theories has been able to facilitate advanced knowledge representation features including accounts of time and concurrency, (e.g., [Reiter, 2001, Chapter 7]), epistemic states (e.g., [Scherl and Levesque, 2003; Claßen and Lakemeyer, 2006]), online action-based agent programming languages for behavior and control (e.g, [Levesque et al., 1997; De Giacomo et al., 2009]), and more, with the price that the reasoning methods are impractical or even undecidable in the most general case. (ii) On the other hand, the practical approaches for implemented deliberation systems based on the situation calculus have been very much restricted in expressiveness, where typically either complete information or a finite domain is assumed in order to provide a realistic approach to reasoning.

Nonetheless, some recent results have explored approaches that lie closer to a middle ground between these two extremes. Regarding projection, the recent work of [De Giacomo et al., 2012] investigates a boundedness assumption that allows expressing rich action theories, while also ensuring the decidability of query answering through evaluation methods based on model checking. Similarly, wrt progression there has been a series of results about theories with actions that have a limited range of effects, such as local-effect and normal actions [Vassos et al., 2008; Liu and Lakemeyer, 2009], thus allowing for a first-order progression.

In this paper we follow the intuitions of [De Giacomo et al., 2012] to introduce a new type of restriction that limits incomplete information expressed in the theory to a bounded number of unknowns (acting similarly to conditional tables in database theory), but allows any type of action to be expressed. In particular we contribute with the following:

1. a major result showing that for a large class of action theories with bounded unknowns a first-order progression always exists and can be effectively computed;
2. a comprehensive classification of the known classes that can be progressed in first-order, also explaining their representational differences using an intuitive example;
3. a newapproach tomodeling non-deterministic actions in basic action theories, that is based on the intuitions from the account of unknowns in 1.

2 Situation calculus

The situation calculus as presented by Reiter [2001] is a three-sorted first-order language L with equality. The sorts are used to distinguish between actions, situations, and objects (everything else). A situation represents a world history as a sequence of actions. The constant S0 is used to denote the initial situation where no actions have occurred. Sequences of actions are built using the function symbol do, such that do(a, s) denotes the successor situation resulting from performing action a in situation s. Actions need not be executable in all situations, and the predicate Poss(a, s) states that action a is executable in situation s. We will typically use a to denote a variable of sort action and α to denote a term of sort action, and similarly s and σ for situations.

A relational fluent is a predicate whose last argument is a situation, and thus whose value can change from situation to situation. We do not consider functional fluents as well as non-fluent predicates and functions, but note that they can be represented as relational fluents with some extra axioms. We also assume a finite number of fluent and action symbols, F and A, and an infinite number of constants C.

Often we need to restrict our attention to sentences in L that refer to a particular situation. For example, the initial knowledge base (KB) is a finite set of sentences in L that do not mention any situation terms except for S0. For this purpose, for any situation term σ, we define Lσ to be the subset of L that does not mention any other situation terms except for σ, does not mention Poss, and where σ is not bound by any quantifier [Lin and Reiter, 1997]. When a formula φ(σ) is in Lσ we say that it is uniform in σ [Reiter, 2001].

Also, we will use L2 to denote the second-order extension of L that only allows predicate variables that take arguments of sort object. L2σ then denotes the second-order extension of Lσ by predicate variables with arguments of sort object.

2.1 Basic action theories

We will be dealing with a specific kind of L-theory, the socalled basic action theory D which has the following form (for readability, we often omit leading universal quantifiers):

1. Dap is a set of action precondition axioms (APs), one for each action function symbol Ai ∈ A, of the form Poss(Ai(⃗x), s) ≡ Πi(⃗x, s), where Πi(⃗x, s) is in Ls.
2. Dss is a set of successor state axioms (SSAs), one per fluent symbol Fi ∈ F, of the form Fi(⃗x, do(a, s)) ≡ Φi(⃗x, a, s), with Φi(⃗x, a, s) ∈ Ls. SSAs characterize the conditions under which Fi has a specific value at situation do(a, s) as a function of situation s and action a.
3. Duna is the set of unique-names axioms for actions: Ai(⃗x) ̸=Aj(⃗y), and Ai(⃗x) =Ai(⃗y) ⊃ ⃗x= ⃗y, for each pair of distinct action symbols Ai and Aj in A.
4. D0 is uniform in S0 and describes the initial situation.
5. Σ is a set of domain independent foundational axioms which formally define legal situations also using a second-order inductive axiom in L2 .

2.2 The problem of progression

The progression of a basic action theory (BAT) is the problem of updating the initial KB so that it reflects the current state of the world after some actions have been performed, instead of the initial state of the world. In other words, in order to do a one-step progression of the BAT D with respect to the ground action α we need to replace D0 in D by a suitable set Dα of sentences so that the original theory D and the theory (D - D0) ∪ Dα are equivalent with respect to how they describe the situation do(α, S0) and the situations in the future of do(α, S0). In a seminal paper, Lin and Reiter [1997] gave a model-theoretic definition for the progression Dα of D0 wrt α and D that achieves this goal. Note that we will be using Sα to denote the situation term do(α, S0).

Definition 1. Let M and M ′ be structures with the same domains for sorts action and object. We write M ∼Sα M ′ if the following two conditions hold: (i) M and M ′ have the same interpretation of all situation-independent predicate and function symbols; (ii) M andM ′ agree on all fluents at Sα, that is, for every relational fluent F , and every variable assignment µ, M, µ |= F (⃗x, Sα) iff M ′ , µ |= F (⃗x, Sα).

Definition 2. Let Dα be a set of sentences in L2Sα. Dα is a progression of D0 wrt α if for any structure M, M is a model of Dα iff there is a model M ′ of D such that M ∼Sα M ′ .

We now proceed to identify an extension of the relatively complete theories of [Lin and Reiter, 1997] that can be progressed using first-order logic. In Section 4 we will show that they indeed capture some natural cases that existing classes of first-order progressable theories cannot encode.

3 Bounded unknowns

First we briefly review the notion of a relatively complete initial KB D0 [Lin and Reiter, 1997]. The idea is that for each Fi ∈F there is an axiom in D0 of the form:

where φi(⃗x) is situation-independent and whose free variables are in ⃗x. In this way D0 characterizes the truth value for all atoms of Fi in S0 relatively to formulas that do not mention situations; in our case, in terms of formulas φi built on constants and equality (and possibly quantifiers). In the typical case when we assume uniqueness of names for constants, D0 is a complete theory. For example the following axiom states that there exactly two atoms true for In(x1, x2, S0):

There is a very simple way to progress a relatively complete D0 wrt a ground action α as follows. For each Fi ∈ F, we start from the SSA for Fi, instantiated for α and S0: ∀⃗x(Fi(⃗x, Sα) ≡ Φi(⃗x, α, S0)). Then for every occurrence of fluent atom Fj(⃗o, S0) in Φi(⃗x, α, S0), we replace the atom by φj(⃗o). Essentially, the form of D0 allows us to replace fluent atoms about S0 by their definition, and obtain a set of sentences uniform in Sα that qualifies as a progression.

We propose a simple yet powerful extension of this type of D0 that introduces existentially quantified variables to model incomplete information, while also preserving the intuitive progression strategy by substitution. The following states that there are exactly two atoms true for In(x1, x2, S0), namely In(purse, keys, S0) and In(purse, w, S0) for some w̸=keys.

Note that (1) completely characterizes In(x, y, S0) relatively to the formula on the right hand side, in which case w acts almost like a "null" value of normal databases along with possible constraints. As L includes infinitely many constants, incomplete information over an infinite domain is implied.

We can build similar axioms about more than one fluent.

In this case we use w1,w2 to specify disjunctive information between fluent atoms of RobotAt(x, S0) and RobotDir(x, S0). For instance, (2) could be used to represent a state where a robot has only partial high-level knowledge of its location and direction due to sensor interference.

We now formalize a new class of initial KBs based on using a single axiom for all (finitely many) fluent symbols in L. This type of D0 is relatively complete but also allows a rich form of incomplete information by means of existentially quantified variables that we call unknowns. Unknowns behave as Skolem constants but without departing from the original language L. Also, as we will shortly see, this type of KB allows a progression by substitution in the manner discussed at the beginning of the section.

Definition 3. An initial KB D0 is relatively complete with bounded unknowns iff it is a sentence of the following form:

where b is the bound on unknowns, ⃗ xi is a tuple of variables of size equal to the number of Fi object arguments, and e, φi are first-order situation-independent formulas whose free variables are all in {w1, . . . ,wb}, {⃗ xi,w1, . . . ,wb}, respectively. Definition 4. A BAT D over a language L with finitely many fluent and action symbols and infinitely many constant symbols is relatively complete with bounded unknowns iff D0 is a consistent sentence of the form described in Definition 3 for some bound b, and mentions all fluent symbols in L.

Note that no other constraint is imposed on any other part of D except for D0, in particular, there is no restriction on the actions described in the successor state axioms (SSAs) in Dss. We now proceed to show that a first-order progression can be obtained by means of a simple syntactic transformation.

Definition 5. Let D0 be as in Definition 3 with bound b. We define T [ψ, ⃗w] as the transformation that replaces occurrences of fluent atoms of the form Fi(⃗o, S0) in ψ by the formula φi(⃗o, ⃗w), where ⃗o is a tuple of terms of sort object, ⃗w is tuple of variables of sort object of size b, and φi is the corresponding formula characterizing Fi in D0.

The intuition is that by applying T to the right-hand side Φi of the SSA for each Fi in L, we obtain a progression similarly to the case investigated by Lin and Reiter [1997]. In our case each of the fluent atoms is replaced by a formula that also introduces new variables not mentioned in the SSA, i.e., variables ⃗w that capture the unknowns. In order then for the substitution to make sense, these unknowns need to be referenced consistently by the same variable names in all occurrences, and this is why they are given as input to T .

Theorem 1. Let D be a BAT over language L that is relatively complete with bounded unknowns as in Definition 4, and α a ground action term. Let ψ be the following sentence:

where ⃗w is a set of variables of sort object distinct from all ⃗ xi , formulas e, φi characterize the constraints among unknowns and the fluent atoms Fi in D0, Φi is the right-hand side of the SSA for Fi, and T the transformation of Definition 5. Then ψ is a progression of D0 wrt to α and D.

Proof. Let M be an arbitrary structure of L. By Definition 2 it suffices to show that M is a model of ψ iff there is a model M ′ of D such that M ∼Sα M ′ .

(⇒): We construct the model M ′ starting fromM and replacing the truth value for all Fi ∈F s.t. M ′, µ ⃗ xi ⃗o ⃗w ⃗c |= Fi(⃗ xi, S0) iff M ′, µ ⃗ xi ⃗o ⃗w ⃗c |= φi(⃗ xi) for all tuples of objects ⃗o in the domain, where ⃗c is a tuple of objects such that M ′, µ ⃗w ⃗c |= e(⃗w). By the form of D0 and the construction of ψ it follows that M ′ models D0 and the SSAs when instantiated with α, S0. We then use the SSAs in Dss to replace the truth value for fluents in all situations other than S0, Sα, and axioms in Dap to replace the extension of Poss. It follows that M ′ models D. (⇐): It suffices to show that D |= ψ. Let M be an arbitrary model of D. M models D0, therefore there exists an object vector ⃗c in the domain s.t. M,µ ⃗w ⃗c |= e(⃗w) (I) and for all i, M,µ ⃗w ⃗c |= ∀⃗ xi(Fi( ⃗ xi, S0) ≡ φi(⃗ xi, ⃗w)) (II). M also models Dss, therefore for all i, M,µ ⃗w ⃗c |= ∀⃗ xi(Fi( ⃗ xi, Sα) ≡ Φi( ⃗ xi, α, S0)) (III). By (II),(III), and the definition of T it follows that M,µ ⃗w ⃗c |= ∀⃗ xi(Fi( ⃗ xi, Sα) ≡ T [Φi(⃗ xi, α, S0), ⃗w]), which along with (I) implies that M |= ψ.

This form of D0 essentially limits all incomplete information in D to what can be expressed in terms of the unknowns ⃗w and the global constraints in e(⃗w). Observe that this is true not only for D0 and S0 but in fact for all future situations. This may seem a little unintuitive, but indeed this is a property of all BATs that comes from the structure of the SSAs.

That is, SSAs being definitions of the form "Fi in do(a, s) is true iff condition Φi about s holds", they cannot introduce disjunctive or existential information; any incomplete information about the truth value of fluents in any situation s has to "link back" to S0 by means of conditions expressed in the right-hand side of SSAs. This is also true for a normal unrestricted D0. The difference is that this form of D0 makes it explicit that there is only a fixed number of variables that can be used to formalize incomplete information at any time. We use this observation in Section 5, to suggest a novel account for representing nondeterministic actions in normal BATs.

4 Amap of first-order progressable theories

We now categorize the known classes for first-order progressable BATs into two incomparable hierarchies: one that relies on limiting the effects of actions by imposing syntactic restrictions on the SSAs, and one that relies on imposing a progression-friendly structure on the D0 that can be maintained. We compare two classes C1 and C2 based on expressive power, by writing: C1 ⪯ C2, if for every theory D1 ∈ C1 there exists a D2 ∈ C2 (over the same language as D1) s.t. the set of models of D1 and D2 coincide; C1 ≈ C2, if C1 ⪯ C2 and C2 ⪯ C1; and C1 ≺ C2, if C1 ⪯ C2 and C1 ̸≈ C2.

We start by introducing a motivating example.

A simple robot scenario that challenges progression

Consider an assistant robot capable of navigating and moving objects around in a grid-like world, where some objects such as bags and boxes may contain other objects. We use the fluents introduced in Section 3 along with fluents Holding, Connected and action moveFwd with the intuitive meaning. We assume that the SSA for any fluent F has the form: F(⃗x, do(a, s)) ≡ γ+ F (⃗x, a, s)∨F (⃗x, s)∧¬γF (⃗x, a, s).

For RobotAt(x, s), γ+ RobAt and γRobAt are as follows:

γ-

RobAt : a =moveFwd .

Similarly for At(x, y, s), γ+ At and γAt are as follows:

Note that when the robot moves, all the objects it carries move, too. The SSAs for RobotDir, Holding, and In have the intuitive formalization, while Connected is static, i.e., its SSA copies the truth of atoms in S0 to all situations.

4.1 Restricting the effects of actions

The main intuition behind the approaches restricting the effects of actions is that by appropriately characterizing all fluent atoms that may be affected by an action α, we can rely on forgetting [Lin and Reiter, 1994] to unset the old truth value for them, and then use Dss[α, S0] (the instantiated SSAs)

to set the new one; the rest of the fluent atoms remain unchanged. The characterization of the affected fluents is made possible by imposing a syntactic structure on SSAs.

Class BAT-SCF: BATs with strongly context-free actions

In strongly context-free actions [Lin and Reiter, 1997], each of the γ ∗ (⃗x, a, s) formulas of SSAs (i.e., γ+ and γ-) is a disjunction, whose disjuncts have the form ∃⃗z(a = A(⃗y)), where ⃗x is included in ⃗y, and ⃗z are the remaining variables of ⃗y. This has the effect that a ground action A(⃗o) essentially dictates all the fluents that get affected by the execution of the action. More formally, for a strongly context-free SSA it follows by the uniqueness of names for actions that:

A method for computing a first-order progression for BATSCF is described in [Lin and Reiter, 1997]. Note that the SSA for RobotAt is clearly not strongly context-free.

Class BAT-LE: BATs with local-effect actions

Local-effect actions [Liu and Levesque, 2005] imply a finite number of affected atoms, but in a more expressive way. The trick is similar to that for strongly context-free actions: every γ ∗ (⃗x, a, s) is a disjunction, with disjuncts of the form ∃⃗z(a= A(⃗y) ∧ φ(⃗y)), ⃗x included in ⃗y, and ⃗z the remaining variables of ⃗y; however a context formula φ can be specified along with every disjunct. The arguments of fluents that may be affected by a ground action α still need to occur as arguments of α, but this form of SSA allows for instance the following:

As above, the uniqueness of action names implies:

Since SSAs in BAT-SCF are special cases of BAT-LE's, BAT-SCF⪯BAT-LE. To prove that BAT-SCF≺BAT-LE, it suffices to show some D in BAT-LE that cannot be "transformed" into a D′ (over the same language as D) in BAT-SCF with the same meaning in terms of models. The SSA above can be used for this, as there is no way to "compile away" the context formula for moveFwd(o1, o2, o3):

The context formula could be compiled into the action precondition axiom, allowing execution of valid actions only, thus resulting in a strongly-context free version of the SSA. This, however, would work only with complete information about RobotAt and RobotDir. If this is not the case, as, e.g., in (2), a conditional effect through a context formula is needed to allow each class of models to evolve appropriately.

The result that theories in BAT-LE admit a first-order progression was shown in [Vassos et al., 2008], while an extension of the result wrt computing the progression can be found in [Liu and Lakemeyer, 2009]. Also note that the SSA for RobotAt of our running example is not local-effect either.

Class BAT-NR: Normal actions

Normal actions [Liu and Lakemeyer, 2009] explore the idea of characterizing the affected fluents from a logical perspective, taking advantage of the connection between progression and forgetting. In particular, a normal action may affect infinitely many fluent atoms but in a way that progression amounts to forgetting a predicate (i.e., not just a finite number of atoms). Under some conditions the result of forgetting, which in general is second-order, can be expressed in first-order logic by means of quantifier elimination.

The intuition behind normal actions is that a ground action α is allowed to have non-local effects on a fluent F as long as it has local effects on all fluents appearing in the effect formulas γ ∗F . For instance, consider the ground action move(purse, loc1, loc2) for moving object purse together with every object inside it from loc1 to loc2. Such action has non-local effects on At(x, y, s), as it affects the location of the objects inside purse, but these are not action arguments. Nonetheless, assuming that In(x, y, s) is the only fluent mentioned in γ ∗ At , the action is normal, as it trivially has localeffects on In(x, y, s), i.e., no effects on it whatsoever.

It is straightforward to show that BAT-LE⪯BAT-NR as local-effect actions are a special case of normal actions by their definition. To see why BAT-LE≺BAT-NR, consider action move(purse, loc1, loc2) and case (1). When performing the action, also the fluent atoms corresponding to items inside purse, e.g., At(keys, loc1, Sα) and At(keys, loc2, Sα), are affected. In order for a local-effect version of the action to be able to set these atoms to true and false respectively, the object keys needs to be included in the action arguments. This is even more problematic for arguments that are not known, such as the other item w in the purse, implied by (1).

As a final note, observe that moveFwd in our motivating example is not normal. Indeed, the action has non-local effects on RobotAt(x, s), which is mentioned in γ+ RobAt . To see this, one has to look at the technical details of Definition 4.4 in [Liu and Lakemeyer, 2009]: a ground action has localeffects on fluent F if, using Duna and the action, γ+ F and γF can be simplified into a disjunction that explicitly states all potentially affected ground atoms of F. Since in general the agent may not know a-priori the boundaries of the world it is situated in, the number of potential locations is not bounded, hence such a simplification is not possible by only using Duna.

BAT-CF: Context-free actions

We can now look into a generalization of BAT-SCF. BATs with context-free effects, which we refer to as BAT-CF, allow the use of any γ ∗ formula in SSAs, as long as it does not mention situations, i.e., it is of the form γ ∗F (⃗x, a) for a fluent F(⃗x, s). Note that this goes beyond local-effects as it allows, e.g., making all F atoms false by setting γ ∗F to a = A ∧ false. On the other hand, actions with local-effects can express conditional effects with a γ ∗ that depends on s. As a result BAT-CF and BAT-LE are incomparable. It is also straightforward that BAT-SCF ≺ BAT-CF. The final piece of information missing is that BAT-CF ≺ BAT-NR. This follows from the definition of normal actions: even though a contextfree axiom may have non-local effects on some fluent F, by definition it trivially has local-effects on all fluents mentioned in γ ∗F as it cannot mention situations.

We can now state the main result of this section.

Theorem 2. BAT-SCF≺{BAT-LE, BAT-CF}≺BAT-NR.

BAT-SCF and BAT-CF were investigated in combination with restrictions on the initial KB in [Lin and Reiter, 1997]. This result also clarifies that just the restriction on the SSAs is adequate for ensuring a first-order progression.

4.2 Restricting the initial KB

The class of BATs with a relatively complete KB, referred to as BAT-RC, characterizes the truth value of all fluent atoms in S0, in terms of formulas φi not mentioning situations. In general L can include non-fluent predicates and functions, and formulas φi can mention them. Similarly to the case of theories with bounded unknowns, referred to as BAT-BU, the initial KB can express incomplete information through rigid symbols. In this sense the effect of an unknown w s.t. w= c1 ∨ w= c2 can be encoded in a BAT-RC by using a predicate P such that P(c1)∨P(c2) is included in the KB and is not mentioned elsewhere in the KB.

Nonetheless, it is typical to consider BATs that do not include functions and functional symbols in order to avoid some of the complications that arise in the treatment of terms, and also encode predicates as static relational fluents. In this setting, BAT-BU theories force incomplete information to be treated at the level of variables as unknown values. In any case, in the scope of BATs without predicates and functions (adopted in this paper) BAT-RC express complete information about all fluents, while BAT-BU allow for a bounded number of unknowns, in which sense BAT-RC ≺ BAT-BU.

Finally, BAT-BU is the only class (of those known to admit a first-order progression) able to capture the simple motivating example we introduced in the beginning of the section.

4.3 Combining action and KB restrictions

The restriction on bounded unknowns is inspired by a recent result about decidability of verification -which includes projection as a special case- over the class of the so-called bounded BATs (BAT-BD) [De Giacomo et al., 2012]. A BAT-BD theory entails that in all situations the number of true fluent atoms is bounded by some fixed number. This requires appropriate restrictions both on the initial KB and the actions' specification. Concerning actions, [De Giacomo et al., 2012] introduce SSAs that either ensure a balance between "adding" and "removing" constants in the extension of a fluent, or discard facts when a given bound is reached. These intuitive restrictions are fairly common in applications either because facts do not persist indefinitely or because one eventually discards some facts. The BAT-BU class, on the other hand, provides an intuitive syntactic structure for the initial KB, ensuring that a first-order progression always exists and can be effectively computed. The term "bounded" here is used to limit the number of "unknowns" instead of that of known facts, as in BAT-BD.

The results on BAT-BD and BAT-BU suggest that combinations of restrictions from both classes can be used to provide a solid ground for investigating practical deliberation systems based on the situation calculus. Indeed, it is not hard to see that the intersection of BAT-BU and BAT-BD includes a wide range of theories that constitute a well-behaved class, for which projection is decidable and a first-order progression is always effectively computable. Moreover, these theories make a direct link between representing dynamic domains in the situation calculus and reasoning by means of methods developed in the theory of databases: (i) the proof of decidability for bounded theories relies on abstractions based on the notion of active domain; (ii) the form of the initial KB for theories with bounded unknowns is essentially equivalent to a conditional table [Imielinski and Lipski, 1984] when the formulas in the KB are also quantifier-free.

5 Nondeterministic actions using unknowns

We now show the power of BAT-BU theories in modeling nondeterministic actions. For simplicity we fix a number b of coins, and use b different fluent symbols (Coin1-Coinb) to represent their state and b different actions (flip1-flipb ) to capture flipping. The idea is for each Coini to use one unknown wi to characterize Coini(x, do(flipi , s)). In order to do this we need to set wi to have two possible values, namely heads or tails, and use an extra fluent Ndeti as a placeholder of disjunctive information. The next sentence is a D0 that models this and also sets all coins to be "heads" in S0.

The next SSAs then shows that we can "assign" Ndeti to Coini(x, do(flipi , s)) to make it capture disjunctive information about its state in the situation after flipping the coin:

Note that executing flipi has the effect of Coini not having complete information any more:

Observe also that as we discussed in Section 3, the disjunctive information about Coini links back to that of Ndeti in S0. Finally, an appropriate account for sensing (e.g., via a sensing fluent SF(a, s) [Levesque, 1996]) can be used to settle the fluent in being true for exactly one of the two outcomes.

6 Related work

The notion of progression for BATs was first introduced by Lin and Reiter [1997]. They were also first to investigate restrictions that guarantee a first-order progression.

Liu and Levesque [2005] introduced the local-effect assumption for actions when they proposed a weaker version of progression that is logically incomplete, but remains practical. Vassos et al. [2008] showed that, under this assumption, a logically correct first-order progression can actually be computed by updating a finite D0. Liu and Lakemeyer [2009] showed how the result of [Vassos et al., 2008] on local-effect progression relates to the notion of forgetting, and examined the more expressive normal actions.

A different approach to first-order progression involves identifying wide classes of queries that can be performed over a basic action theory wrt which a first-order progression is guaranteed to be correct (even though it may be incorrect in the general case). This was also first investigated by Lin and Reiter [1997] who showed that for answering projection queries that are uniform in some situation σ, a first-order progression is always adequate. Shirazi and Amir [2005] proved a similar result in the context of logical filtering. Vassos et al [2008] extended this result showing that un-nested quantification over situations may also be allowed.

Outside of the situation calculus, Thielscher [1999] defined a dual representation for basic action theories based on state update axioms that explicitly define the direct effects of each action, and investigated progression in this setting. In this work the update relies on expressing the changes using constraints which may need to be conjoined to the original database, which is similar to the idea of replacing fluent atoms by their definition in the relatively complete initial KBs.

Perhaps the most relevant work related to nondeterministic actions in situation calculus is the use of a disjunction of SSAs, introduced by [Lin, 1996] in the context of nonmonotonic logics. Unlike our approach though, their account operates at the level of meta-theory and cannot be used to reason about future situations by means of regular entailment.

7 Conclusions

In this paper we created a map of all known theories that admit a first-order progression and, inspired by recent results about decidability of verification for BAT-BD, extended it with the class BAT-BU of theories with bounded unknowns for which we proved that a first-order progression always exists and can be effectively computed. We also showed that BAT-BU theories generalize BATs with a relatively complete KB, and that they can capture nondeterministic actions. Further, we argued that the theories falling into the intersection of BAT-BU and BAT-BD form a well-behaved class of practical interest, which guarantees decidability of projection and effective computability of first-order progression. This is a major advancement, since until now such properties were guaranteed for special (less intuitive) classes, and only for the two problems separately. Finally, we pointed out that such a class builds a link between the situation calculus as a representation formalism and reasoning techniques developed in the context of database systems, a link that we intend to exploit in future work, to devise efficient methods for projection and progression, under restrictions inspired by pragmatic approaches in the database context.

Acknowledgments

The authors acknowledge the support of EU Projects FP7ICT 257593 (ACSI) and FP7-ICT 318338 (OPTIQUE).