Belief Update Revisited

1 Introduction

In papers about belief change, one often reads sentences such as "belief revision consists in incorporating some new information about a static world, while belief update consists in incorporating into a belief base about an old state of the world a notification of some change in the world". However, the distinction is not so simple. To assess the scope of belief change operators, we need to be able to talk about the properties of the system (the world and the available actions) and the properties of the agent's state of knowledge, as in the taxonomy for reasoning about action and change from [Sandewall, 1995]. However, unlike reasoning about action, belief change processes have never (as far as we know) been analyzed from the point of view of such a taxonomy. A first step is taken towards this direction (for belief revision only) in [Friedman and Halpern, 1996].

Elaborating a full taxonomy for belief change and assessing the scope of each approach is an ambitious project that definitely needs more than one short article. Here we focus on a specific class of belief change operators, namely belief update. This paper aims at identifying its precise scope, i.e. the conditions (expressed by properties of the world and of the agent's beliefs) under which update is a suitable process for belief change. The main claim of the paper (discussed in Section 3) is that updating a knowledge base by α corresponds to progressing it by a specific "purely physical", feedbackfree action "make α true" whose precise meaning depends on the chosen update operator. This in turn raises the following question, addressed in Section 4: if update is progression, are there belief change operators corresponding to regression? Section 5 briefly considers the question of whether updates can be compiled into propositional action theories. Related issues are discussed in Section 6.

2 Background on belief update

Let LV be the propositional language generated from a finite set of propositional variables V , the usual connectives and the Boolean constants ⊤, ⊥. S = 2V is the set of states (i.e., propositional interpretations). For any ϕ ∈ LV , Mod(ϕ) is the set of states satisfying ϕ. For any X ⊆ S, for(X) is the formula of LV (unique up to logical equivalence) such that Mod(for(X)) = X. If X = {s}, we write for(s) instead of for({s}). We use ϕ ⊕ ψ as a shorthand for ϕ ↔ ¬ψ.

A belief update operator ⋄ is a mapping from LV × LV to LV , i.e., it maps two propositional formulas ϕ (the initial belief state) and α (the "input") to a propositional formula ϕ ⋄ α (the resulting belief state). We recall here the KatsunoMendelzon (KM for short) postulates for belief update [Katsuno and Mendelzon, 1991].

• U1 ϕ ⋄ α |= α.
• U2 If ϕ |= α then ϕ ⋄ α ≡ ϕ.
• U3 If ϕ and α are both satisfiable then ϕ ⋄ α is satisfiable.
• U4 If ϕ ≡ ψ and α ≡ β then ϕ ⋄ α ≡ ψ ⋄ β.
• U5 (ϕ ⋄ α) ∧ β |= ϕ ⋄ (α∧ β).
• U6 If ϕ ⋄ α |= β and ϕ ⋄ β |= α then ϕ ⋄ α ≡ ϕ ⋄ β.
• U7 If ϕ is complete then (ϕ ⋄ α) ∧ (ϕ ⋄ β) |= ϕ ⋄ (α ∨ β).
• U8 (ϕ∨ψ) ⋄ α ≡ (ϕ ⋄ α) ∨ (ψ ⋄ α).

Although we have recalled all postulates for the sake of completeness, we should not accept them unconditionally. They have been discussed in several papers, including [Herzig and Rifi, 1999] in which it was argued that not all these postulates should be required, and that the "uncontroversial" ones (those deeply entrenched in the very notion of update and satisfied by most operators studied in the literature) are (U1), (U3), (U8), and (U4) to a lesser extent. We therefore call a basic update operator any operator ⋄ from LV ×LV to LV satisfying at least (U1), (U3), (U4) and (U8). In addition, ⋄ is said to be inertial if it also satisfies (U2), and ⋄ is a KM update operator if it satisfies (U1)-(U8) 1 . In the paper we refer to some specific update operators such as the PMA [Winslett, 1990] that we have no space to recall (see for instance [Herzig and Rifi, 1999]).

1 (U5), (U6) and (U7) are much more controversial than the other

3 Belief update as action progression

The difference between the scope of revision and that of update is often expressed as a static vs. dynamic opposition. However, nothing in the AGM theory of belief revision implies that we should restrict its application to static worlds. As remarked in [Friedman and Halpern, 1999], what is essential in belief revision is not that the world is static, but that the language used to describe the world is static. Thus, if an evolving world is represented using time-stamped propositional variables of the form vt (v true at time t), we can perfectly revise a belief set by some new information about the past or the present, and infer some new beliefs about the past, the present, or even the future.

Example 1 On Monday, Alice is the head of the computer science lab while Bob is the head of the math lab. On Tuesday I learned that one of them resigned (but I don't know which one). On Wednesday I learn that Charles is now the head of the math lab, which implies that Bob isn't. (It is implicit that heads of labs tend to keep their position for quite a long time.) What do I believe now?

Example 1 contains a sequence of two "changes". Both are detected by observations, and the whole example can be expressed as a revision process (with time-stamped variables). Let us identify Monday, Tuesday and Wednesday by the time stamps 1, 2 and 3. On Monday I believe A1,B1, as well as the persistency laws A1 ↔ A2,A2 ↔ A3,B1 ↔ B2 etc., therefore I also believe A2,B2 etc.: I expect that Alice and Bob will remain the heads of their respective labs on Tuesday and Wednesday. The revision by ¬A2 ∨ ¬B2 (provided that the revision operator minimizes change) leads me to believe A1,B1,A2 ⊕ B2,A3 ⊕ B3 etc.: on Tuesday, I still believe that Alice and Bob were heads of their labs on Monday, and that now exactly one of them is. Then the revision by ¬B3 (at time 3) makes me believe A1, B1, A2, ¬B2, A3, ¬B3: on Wednesday, I understand that Bob was the one to resign on Tuesday, and therefore that Alice was still head of the CS lab on Tuesday, and is still now 2 .

Now, the fact that belief revision can deal with (some) evolving worlds suggests that claiming that belief update is the right belief change operation for dealing with evolving worlds is unsufficient and ambiguous. The literature on belief update abounds in ambiguous explanations such as "update consists in bringing the knowledge base up to date when the world is described by its changes" 3 . There is a first ambiguity in the expressions "describing the world by its changes"

ones (see [Herzig and Rifi, 1999]); they characterize the specific class of updates based on a similarity-based minimization process (which is known to lead to several counterintuitive results).

2 Note that this scenario is also a case for belief extrapolation [Dupin de Saint-Cyr and Lang, 2002], which is a particular form of time-stamped revision.

3 This formulation appears in [Katsuno and Mendelzon, 1991], which may be one of the explanations for such a long-lasting ambiguity.

or "notification of a change", as "change" actually has to be understood as "possibility of change" (we'll come back to this point). But the main problem is the status of the input formula α. To make things clear, here is an example.

Example 2 My initial belief is that either Alice or Bob is in the office (but not both). Both tend to stay in the office when they are in. Now I see Bob going out of the office. What do I believe now?

Trying to use belief update to model this example is hopeless. For all common update operators seen in the literature, updating A⊕B by ¬B leads to ¬B, and not to ¬A∧¬B. Indeed, because of (U8), we have (A⊕B)⋄¬B ≡ [(A∧¬B)⋄ ¬B] ∨ [(¬A ∧ B) ⋄ ¬B] ≡ (A ∧ ¬B) ∨ (¬A ∧ ¬B) ≡ ¬B. The only way to have ¬A∧¬B as the result would be to have (A ∧ ¬B) ⋄ ¬B ≡ ¬A ∧ ¬B, which can hold only if there is a causal relationship between A and B, such as B becoming false entails A becoming false - which is not the case here.

Example 2 definitely deals with an evolving world and contains a "notification of change", and still it cannot be formulated as a belief update process. On the other hand, like Example 1, it can be perfectly expressed as is a time-stamped belief revision process 4 .

The key point is (U8) which, by requiring that all models of the initial belief set be updated separately, forbids us from inferring new beliefs about the past from later observations: indeed, in Example 2, belief update provides no way of eliminating the world (A, ¬B) from the set of previously possible worlds, which in turn, does not allow for eliminating (A, ¬B) from the list of possible worlds after the update: if (A, ¬B) is a possible world at time t, then its update by ¬B must be in the set of possible worlds at time t+1. In other terms, update fails to infer that Alice wasn't in the office and still isn't.

Belief update fails as well on Example 1: updating A ∧ B ∧ ¬C by ¬A ∨ ¬B gives the intended result, but only by chance (because the agent's initial belief state is complete). The second step fails: with most common update operators, updating (A ⊕ B) ∧ ¬C by ¬B ∧ C leads to ¬B ∧ C, while we'd expect to believe A as well.

The diagnosis should now be clear: the input formula α is not a mere observation. An observation made at time t + 1 leads to filter out some possible states at time t + 1, which in turn leads to filter out some possible states at time t, because the state of the world at time t and the state of the world at time t + 1 are correlated (by persistence rules or other dynamic rules 5 .) And finally, the successor worlds (at time t+1) of these worlds at time t that update failed to eliminate can not be eliminated either. Such a backward-forward reasoning needs a proper generalization of update (and of revision), unsurprisingly called generalized update [Boutilier, 1998].

4 Note that without time stamps (and in particular within the framework of belief update), we cannot distinguish between "B has become false" (as in "I see Bob go out of the office") and "the world has evolved in such a way that B is now false" (as in "I now see Bob out of his office"). Anyway, for Example 2, the expected outcome is the same in both cases (provided that A and B are expected to persist with respect to the granularity of time considered).

5 The only case where belief update could be compatible with interpreting α as an observation would therefore be the case where not the faintest correlation exists between the state of the world at different time points; in this case, we would have ϕ ⋄ α ≡ α whenever α is consistent - a totally degenerate and uninteresting case.

Now, α has to be understood as an action effect, and update is a particular form of action progression for feedback-free actions. Action progression (as considered in the literature of reasoning about action and logic-based planning) consists in determining the belief state obtained from an initial belief state after a given action is performed.

This connection between belief update and action progression was first mentioned in [del Val and Shoham, 1994], who argue that updating an initial belief state ϕ by a formula α corresponds to one particular action; they formalize such actions in a formal theory of actions based on circumscription, and their framework for reasoning action is then used to derive a semantics for belief update. The relationship between update and action progression appears (more or less explicitly) in several other papers, including [Liberatore, 2000b], who expresses several belief update operators in a specific action language. Still, the relationship between update and action progression still needs to be investigated in more detail.

We first need to give some background on reasoning about action. Generally speaking, an action A has two types of effects: an ontic (or physical) effect and an epistemic effect. For instance, if the action consists in tossing a coin, its ontic effect is that the next value of the fluent heads may change, whereas its epistemic effect is that the new value of the fluent is observed (this distinction between ontic and epistemic effects is classical in most settings). Complex actions (with both kinds of effects) can be decomposed into two actions, one being ontic and feedback-free, the other one being a purely epistemic (sensing) action.

The simplest model for a purely ontic (i.e., feedbackfree) action A consists of a transition graph RA on S. 6 RA(s, s′ ) means that s′ is accessible from s after A. RA(s) = {s′ | RA(s, s′ )} is the set of states that can obtain after performing A in s. If RA(s) is a singleton for all s then A is deterministic. If RA(s) = ∅ then A is inexecutable in s. A is fully executable iff RA(s) ̸= ∅ for every s.

Let A be a purely ontic action modelled by a transition graph RA on S. For any formula ϕ ∈ LV , the progression of ϕ by A is the propositional formula (unique up to logical equivalence) whose models are the states that can obtain after performing A in a state of Mod(ϕ): prog(ϕ, A) is defined by

Lastly, for any action A, Inv(A) is the set of invariant states for A, i.e. the set of all states s such that RA(s) = {s}.

Clearly enough, (1) is identical to (U8). Therefore, for any update operator (and more generally any operator satisfying (U8)) and any input formula α, updating by α is an action progression operator. This raises several questions: (a) Which action is this exactly? (b) What is the class of actions that correspond to updates? (c) If update is progression, are there belief change operators corresponding to regression?

6 More sophisticated models may involve graded uncertainty such as probabilities, delayed effects etc.

Question (a) first. As argued above, (U8) and (1) mean that the action is feedback-free. This comes down to saying that belief update assumes unobservability: the set of possible states after A is performed is totally determined by the set of possible states before it is performed and the transition system corresponding to A. In other words, what you foresee is what you get: once we have decided to perform A, waiting until it has actually been performed will not bring us any new information. Note that using update in Example 2 would correspond to performing an action whose effect is to make Bob go out of his office (when he is initially not in the office, this action has no effect). Likewise, in Example 1, updating A⊕B∧¬C by ¬B∧C corresponds to performing the action "demote Bob from his position and appoint Charles instead".

Therefore, updating by α is a purely ontic (feedback-free) action. Can we now describe this action in more detail? (U1) means that the action of updating by α has to be understood as "make α true". More precisely, due to the absence of feedback reflected by (U8), updating ϕ by α could be understood as a dialogue between an agent and a robot: "All I know about the state of the world is that is satisfies ϕ. Please, go to the real world, see its real state, and whatever this state, act so as to change it into a world satisfying α, following some rules" (given that the robot does not communicate with the agent once it is the real world.) The rules to be followed by the robot are dictated by the choice of the update operator ⋄. If ⋄ satisfies (U2), then the rules state that if the α is already true then the robot must leave the world as it is. If ⋄ is the PMA [Winslett, 1990], then the rules are "make α true, without changing more variables than necessary". More generally, when ⋄ is a Katsuno-Mendelzon operator, associated with a collection of similarity preorders (one for each world), the robot should make α true by changing s into one of the states that are most similar to it 7 . When ⋄ is WSS [Winslett, 1990; Herzig, 1996] or the MPMA [Doherty et al., 1998], then the rules are "make α true, without changing the truth values of a given set of variables (those that do not appear in α, or those that play no role in α)." And so on.

Writing things more formally: given an update operator ⋄ and a formula α, let update(⋄, α) be the ontic action whose transition graph is defined by: for all s, s′ ∈ S,

The following characterizations are straightforward, but worth mentioning (and they will be useful later).

Proposition 1 Let ⋄ satisfy (U8).

1. ϕ ⋄ α ≡ prog(ϕ, update(⋄, α));
2. ⋄ satisfies (U1) if and only if for any formula α ∈ LV and any s ∈ S, Rupdate(⋄,α)(s) ⊆ Mod(α);
3. ⋄ satisfies (U2) if and only if for any formula α ∈ LV , Inv(update(⋄, α)) ⊇ Mod(α);

7 Note that, as argued in [Peppas et al., 1996], this similarity has here be understood as an ontological notion (s being closer to s1 than to s2 may, in practice, reflect that from s it is easier to go to s1 than to s2) and not as an epistemic notion of similarity, as it would be the case for belief revision. This agrees with our view of update(⋄, α) as an ontic action.

1. ⋄ satisfies (U3) if and only if for any satisfiable formula α ∈ LV , update(⋄, α) is fully executable.

Note that (U1) and (U2) imply that for all s ∈ S, Rupdate(⋄,α)(s) ⊆ Inv(update(⋄, α)). The other postulates do not have any direct effect on the properties of update(⋄, α) considered as an isolated action, but they relate different actions of the form update(⋄, α). Noticeably, requiring (U4) corresponds to the equality between update(⋄, α) and update(⋄, β) when α and β are logically equivalent. The characterizations of (U5), (U6) and (U7) in terms of reasoning about action do not present any particular interest.

Let us now consider question (b). Obviously, given a fixed update operator ⋄ satisfying (U1), (U3), (U4) and (U8), some fully executable actions are not of the form update(⋄, α) (this is obvious because there are 22n actions of the form update(⋄, α) and 2n+2n-1 fully executable actions, where n = |V |.) Now, what happens if we allow ⋄ to vary? The question now is, what are the actions that can be expressed as update(⋄, α), for some update operator ⋄ and some α?

Proposition 2 Let A be a fully executable ontic action such that RA(s) ⊆ Inv(A) for all s ∈ S. Then there exists a KM-update operator, and a formula α, such that A = update(⋄, α).

The proof is constructive: α is taken such that Mod(α) = Inv(A), and the collection of faithful orderings in the sense of [Katsuno and Mendelzon, 1991] is defined by s1 <s s2 if and only if s = s1 ̸= s2 or (s ̸= s1, s ̸= s2, s1 ∈ RA(s), s2 ̸∈ RA(s)); and s1 ≤s s2 iff not (s2 <s s1).

From Propositions 1 and 2 we get

Corollary 1 Let A be an ontic action. There exists a KM-update operator ⋄, and a formula α such that A = update(⋄, α), if and only if A is fully executable and RA(s) ⊆ Inv(A) for all s ∈ S.

A variant of Proposition 2 (and Corollary 1) can be obtained by not requiring RA(s) ⊆ Inv(A): in that case there exists an update operator ⋄ satisfying all the KM postulates except (U3), and a formula α such that A = update(⋄, α). α can be taken as ⊤ and s ≤s s2 iff s1 ∈ RA(s) or s2 ̸∈ RA(s).

4 Reverse update

Now, question (c). Is there a natural notion which is to action regression what update is to progression? The point is that we do not have one, but two notions of action regression. The weak progression regression (or weak preimage) of ψ by A is the formula whose models are the states from which the execution of A possibly leads to a model of ψ, while the strong regression regression (or strong preimage) of ψ by A is the formula whose models are the states from which the execution of A certainly leads to a model of ψ:

See for instance [Lang et al., 2003] for the interpretation of these two notions of regression in reasoning about action. This naturally leads to two notions of reverse update.

Definition 1 Let ⋄ be an update operator.

• the weak reverse update ⊙ associated with ⋄ is defined by: for all ψ, α ∈ LV , for all s ∈ S,

• the strong reverse update ⊗ associated with ⋄ is defined by: for all ψ, α ∈ LV , for all s ∈ S,

Intuitively, weak reverse update corresponds to (deductive) postdiction: given that the action "make α true" has been performed and that we now know that ψ holds, what we can say about the state of the world before the update was performed is that it satisfied ψ ⊙α. As to strong reverse update, it is an abductive form of postdiction, better interpreted as goal regression: given that a rational agent has a goal ψ, the states of the world in which performing the action "make α true" is guaranteed to lead to a goal states are those satisfying ψ ⊗α.

The following result shows that ⊙ and ⊗ can be characterized in terms of ⋄:

Proposition 3

1. ψ ⊙α |= ϕ iff ¬ϕ ⋄ α |= ¬ψ;

As a consequence of Proposition 3, ψ ⊙ α is the weakest formula ϕ such that ¬ϕ⋄α |= ¬ψ, and ψ⊗α is the strongest formula ϕ such that ϕ ⋄ α |= ψ.

Example 3 Let ⋄ = ⋄PMA [Winslett, 1990]. Let b and m stand for "the book is on the floor" and "the magazine is on the floor". The action update(⋄, b ∨ m) can be described in linguistic terms by "make sure that the book or the magazine is on the floor". Then b⊙(b∨m) ≡ b∨(¬b∧¬m) ≡ b∨¬m, which can be interpreted as follows: if we know that the book is on the floor after update(⋄, b ∨ m) has been performed, then what we can say about the previous state of the world is that either the book was already on the floor (in which case nothing changed) or that neither the book nor the magazine was on the floor (and then the update has resulted in the book being on the floor). On the other hand, b ⊗ (b ∨ m) ≡ b: if our goal is to have the book on the floor, the necessary and sufficient condition for the action update(⋄, b ∨m) to be guaranteed to succeed is that the book is already on the floor (if neither of them is, the update might well leave the book where it is and move the magazine onto the floor).

An interesting question is whether weak and strong reverse update can be characterized by some properties (which then would play the role that the basic postulates play for "forward" update). Here is the answer (recall that a basic update operator satisfies U1, U3, U4 and U8).

Proposition 4 ⊙ is the weak reverse update associated with a basic update operator ⋄ if and only if ⊙ satisfies the following properties:

• W1 ¬α⊙α ≡ ⊥;
• W3 if α is satisfiable then ⊤⊙α ≡ ⊤;
• W4 if ψ ≡ ψ′ and α ≡ α′ then ψ ⊙α ≡ ψ′ ⊙α′ ;
• W8 (ψ ∨ψ′ ) ⊙α ≡ (ψ ⊙α) ∨ (ψ′ ⊙α).

In addition to this, ⋄ satisfies (U2) if and only if ⊙ satisfies

Note that (W4) and (W8) are exactly the same properties as (U4) and (U8), replacing ⋄ by ⊙. Properties (U5), (U6) and (U7) do not seem seem to have meaningful counterparts for ⊙ (and anyway, as already argued, these three postulates are too controversial).

We have a similar result for strong reverse update:

Proposition 5 ⊗ is the strong reverse update associated with a basic update operator ⋄ if and only if ⊗ satisfies the following properties:

• S1 α⊗α ≡ ⊤;
• S3 if α is satisfiable then ⊥⊗α ≡ ⊥;
• S4 if ψ ≡ ψ′ and α ≡ α′ then ψ ⊗α ≡ ψ′ ⊗α′ ;
• S8 (ψ ∧ψ′ ) ⊗α ≡ (ψ ⊗α) ∧ (ψ′ ⊗α).

In addition to this, ⋄ satisfies (U2) if and only if ⊗ satisfies

• S2 if ψ |= α then ψ |= ψ ⊗α.

Note that, unlike weak reverse update, strong reverse update does generally not satisfy modelwise decomposability (U8/W8), but a symmetric, conjunctive decomposability property (S8).

Moreover, if ⋄ is a basic update operator then

SIW if α is satisfiable then ψ ⊗ α |= ψ ⊙ α

Note that (SIW) fails without (U3). Example 3 shows that the converse implication of (SIW) does not hold in general. Finally, ⊗ and ⊙ coincide if and only if update(⋄, α) is deterministic.

One may wonder whether reverse update has something to do with erasure [Katsuno and Mendelzon, 1991]. An erasure operator ♦ is defined from an update operator ⋄ by ψ♦α ≡ ψ ∨ (ψ ⋄ ¬α). Erasing by α intuitively consists in making the world evolve (following some rules) such that after this evolution, the agent no longer believes α. A quick look suffices to understand that erasure has nothing to do with weak and strong reverse update. Erasure corresponds to action progression for an action erase(α) whose effect is be epistemically negative (make α disbelieved). This implies in particular that ⊤♦⊤ is always unsatisfiable (⊤ cannot be made disbelieved) whereas ⊤ ⊙ ⊤ ≡ ⊤ ⊗ ⊤ ≡ ⊤.

Pursuing the investigation on reverse update does not only have a theoretical interest: weak (deductive) reverse update allows for postdiction, and strong (abuctive) reverse update allows for goal regression (when the actions performed are updates) and is therefore crucial if we want to use an updatebased formalism for planning (see [Herzig et al., 2001]).

5 Update and propositional action theories

Now that we know that update(⋄, α) is an action progression operator, can it be described by a propositional action theory such as those described in [Giunchiglia et al., 2004]? Recall that a propositional action theory ΣA for action A is a propositional formula ΣA built on the language generated by the time-stamped propositional variables Vt ∪Vt+1, where Vt = {vt|v ∈ V } and Vt+1 = {vt+1|v ∈ V }, such that, for each st ∈ 2Vt and s′t+1 ∈ 2Vt+1 , st ∪ s′t+1 holds if and only if s′ ∈ RA(s).

If we don't care about the size of the action theory, the answer is obviously positive: just take

Then for all st, s′t+1 , we have st ∪ st+1 |= Σα if and only if for(s′ ) |= for(s) ⋄ α, and, equivalently, ϕ ⋄ α |= ψ if and only if ϕt ∧ Σα |= ψt+1.

The question is now whether update(⋄, α) can be described by a succinct action theories. The answer depends on the update operator. Existing complexity results on belief update enable us to give a quick negative answer for many update operators. Note first that prog(ϕ, α) |= ψ if and only if ϕt ∧ Σα |= ψt+1; therefore, given a propositional action theory ΣA and two formulas ϕ, ψ, deciding whether prog(ϕ, α) |= ψ is in coNP (actually coNP-complete). Now, for many update operators, including the PMA, deciding whether ϕ ⋄ α |= ψ is Πp2 -complete [Eiter and Gottlob, 1992; Liberatore, 2000a]. Let ⋄ be one of these update operators. If there were a way of expressing update(⋄, α) (for all α) by a polynomially large action theory, then we would have Πp2 = coNP, and the polynomial hierarchy would collapse at the first level, which is very unlikely.

On the other hand, a positive answer is obtained for the following update operators, for which deciding whether prog(ϕ, α) |= ψ is only coNP-complete: the MPMA [Doherty et al., 1998], WSS [Winslett, 1990], WSS↓ and WSS↓dep [Herzig and Rifi, 1999]. All those update operators consists first in forgetting a set of variables (for instance, those that appear in the input formula α, or those in which α depends etc.), and then expanding the result by α. For instance, for ⋄ = ⋄WSS: Σ(α) = αt+1 ∧ ∧v̸∈V ar(α) vt ↔ vt+1.

6 Summary and conclusion

Let us try to summarize what we have said so far. Both revision and update deal with dynamic worlds, but they strongly differ in the nature of the information they process. Belief revision (together with the introduction of time stamps in the propositional language) aims at correcting some initial beliefs about the past, the present, and even the future state of the world by some newly observed information about the past or the present state of the world. Belief update is suitable only for (some specific) action progression without feedback: updating ϕ by α corresponds to progressing (or projecting forward) ϕ by the action update(⋄, α), to be interpreted as make α true. The "input formula" α is the effect of the action update(⋄, α), and definitely not an observation. Expressed in the terminology of [Sandewall, 1995], the range of applicability of update is the class Kp-IA: correct knowledge 8 , no observations after the initial time point, inertia if (U2) is assumed, and alternative results of actions.

Assessing the scope of belief update is all the more important as several variations on belief update have recently appeared in the literature. [Liu et al., 2006] lift belief update to description logics. [Eiter et al., 2005] gives a framework for changing action descriptions, which is actually closer to a revision process than to update; however, updating an action by changing physically its transition graph would be meaningful as well, and deserves further study.

8 However, this point is somewhat debatable: update would work as well if we don't assume that the agent's initial beliefs is correct - of course, in this case the final beliefs may be wrong as well.

In complex environments, especially planning under incomplete knowledge, actions are complex and have both ontic and epistemic effects; the belief change process then is very much like the feedback loop in partially observable planning and control theory: perform an action, project its effects on the current belief state, then get the feedback, and revise the projected belief state by the feedback. Clearly, update allows for projection only. Or, equivalently, if one chooses to separate the ontic and the epistemic effects of actions, by having two disjoint sets of actions (ontic and epistemic), then ontic actions lead to projection only, while epistemic actions lead to revision only. Therefore, if one wants to extend belief update so as to handle feedback, there is no choice but integrating some kind of revision process, as in several recent works [Boutilier, 1998; Shapiro and Pagnucco, 2004; Jin and Thielscher, 2004; Hunter and Delgrande, 2005]. Another possibility is to generalize update so that it works in a language that distinguishes facts and knowledge, such as epistemic logic S5: this knowledge update process is investigated in [Baral and Zhang, 2005]. Here, effects of sensing actions are handled by updating (and not revising) formulas describing the agent's knowledge. Such a framework takes the point of view of a modelling agent O who reasons an the state of knowledge of another agent ag. Thus, for instance, updating a S5 model by Kagϕ means that the O updates her beliefs about ag's knowledge; considering ag's mental state as part of the outside world for agent O, this suits our view of update as a feedback-free action for O (updating by Kagϕ corresponds as "make Kagϕ true", which can for instance be implemented by telling ag that ϕ is true).

Acknowledgements

Thanks to Andreas Herzig for years of discussions about the very meaning of belief update (without which I would never have thought of writing this paper). Thanks as well to Meghyn Bienvenu, Florence Dupin de Saint-Cyr, S´ebastien Konieczny, Fangzhen Lin, and Pierre Marquis.