On the Semantics of Knowledge Update

1 Introduction andMotivation

The well-studied issues of belief updates and belief revision [Katsuno and Mendelzon, 1991] are concerned with the update and revision aspects of an agent's belief with respect to new beliefs. The notion of belief update has been used, and often serves as a guideline [Kartha and Lifschitz, 1994], in reasoning about the effect of (world altering) actions on the state of the world. Thus if a0 represents the agent's belief about the world and the agent does an action that is supposed to make ✁ true in the resulting world, then the agent's belief about the resulting world can be described by a0 ✂ ✁ , where ✂ is the update operator of choice.

Now let us consider reasoning about sensing actions [Scherl and Levesque, 1993; Son and Baral, 2000], which in their pure form, when executed, do not change the world, but change the agent's knowledge about the world. Let ☎ ✆ ✞ ☎ ✆ ✡ be a sensing action whose effect is that after it is executed the agent knows whether ☞ is true or not. This can be expressed as ✌ ☞ ✎ ✌ ✒ ☞ , where ✌ is the modal operator ✌ ✞ ✔ ✕ ☎ . The current theory of belief updates does not tell us how to do updates with respect to such gain in knowledge due to a sensing action. (Note that we can not just have ✁ ✘ ☞ ✎ ✒ ☞ and use the the notion of belief update, as ☞ ✎ ✒ ☞ is a tautology). One of our goals in this paper is to define a notion of knowledge update, analogous to belief update, where the original theory ( a0 ) and the new theory ( ✁ ) are in a language that can express knowledge. Such a notion would not only serve as a guideline to reason about pure and mixed sensing actions

Yan Zhang

School of Computing & IT

University of Western Sydney Penrith South DC, NSW 1797, Australia

E-mail: yan@cit.uws.edu.au

in presence of constraints, but also allow us to reason about actions corresponding to forgetting, and ignorance.

The structure of the rest of the paper is as follows. In Section 2 we start with describing the particular modal logic that we plan to use in expressing knowledge, and describe the notion of k-models analogous to 'models' in classical logic. We then define closeness between k-models and use it to define a particular notion of knowledge update. In Section 3 we present alternative characterizations of four particular knowledge update cases - gaining knowledge, ignorance, sensing, and forgetting, and show their equivalence to our original notion of knowledge update. Some of these alternative characterizations are based on the formulation of reasoning about sensing actions, and thus our equivalence results serve as justification of the intuitiveness of our definition of knowledge update. In Section 4 we explore sufficiency conditions that guarantee persistence of knowledge (or ignorance) during a knowledge update. In Section 5, we conclude and discuss future directions.

2 Closeness between k-models and Knowledge Update

In this section, we describe formal definitions for knowledge update. Our formalization will be based on the semantics of the propositional modal logic S5 with a single agent. In general, under Kripke semantics, a Kripke structure is a triple ✢ ✣ ✥ ✧ ✥ ✩ ✫ , where ✣ is a set of possibleworlds, ✧ is an equivalence relation on ✣ , and ✩ is a truth assignment function that assigns a propositional valuation to each world in ✣ . Given a Kripke structure ✬ ✭ ✢ ✣ ✥ ✧ ✥ ✩ ✫ , a Kripke interpretation is a pair ✱ ✭ ✢ ✬ ✥ ✕ ✫ , where ✕ ✲ ✣ is referred to the actual world of ✱ . The entailment relation ✴ ✭ between Kripke interpretations and formulas is defined to provide semantics for formulas of S5 [Fagin and et al, 1995].

In the case of single agent, however, we may restrict ourselves to those S5 structures in which the relation ✧ is universal, i.e. each world is accessible from every world, and worlds are identified with the set of atoms true at the worlds [Meyer and van der Hoek, 1995]. To simplify a comparison between two worlds (e.g. Definition 2), we may view an atom ✵ ✲ ✕ iff ✕ ✴ ✭ ✵ . Therefore, in our context a Kripke structure ✢ ✣ ✥ ✧ ✥ ✩ ✫ is uniquely characterized by ✣ and we may simplify a Kripke interpretation as a pair ✢ ✣ ✥ ✕ ✫ which we call a a0 -model, where ✕ indicates the actual world of the agent and ✣ presents all possible worlds that the agent may access. Note that ✕ is in ✣ for any a0 -model ✢ ✣ ✥ ✕ ✫ .

In our followingdescription, we use ✁ ✥ ✂ ✥ ☎ ✥ ✵ ✥ ✆ ✆ ✆ to denote primitive propositional atoms; a0 ✥ ✁ ✥ ✟ ✥ ✆ ✆ ✆ to denote propositional formulas without including modalities (we also call them objective formulas); and ☛ ✥ ☞ ✥ ✍ ✥ ✆ ✆ ✆ and ✎ to denote formulas that may contain modal operator ✌ . For convenience, we also use ✎ ✘ ☛ ✑ ✓ ✆ ✆ ✆ ✓ ☛ ✖ to represent a finite set of formulas ✘ ☛ ✑ ✥ ✆ ✆ ✆ ✥ ☛ ✖ ✚ and call ✎ a (knowledge) set.

Definition 1 (S5 Semantics) Let ✜ be the set of all primitive propositions in the language. The entailment relation ✴ ✭ under normal S5 semantics is defined as follows:

1. ✢ ✣ ✥ ✕ ✫ ✴ ✭ ✵ iff ✵ is primitive (i.e. ✵ ✲ ✜ ) and ✕ ✴ ✭ ✵ ;
2. ✢ ✣ ✥ ✕ ✫ ✴ ✭ ☛ ✓ ☞ iff ✢ ✣ ✥ ✕ ✫ ✴ ✭ ☛ and ✢ ✣ ✥ ✕ ✫ ✴ ✭ ☞ ;
3. ✢ ✣ ✥ ✕ ✫ ✴ ✭ ✒ ☛ iff it is not the case that ✢ ✣ ✥ ✕ ✫ ✴ ✭ ☛ ;
4. ✢ ✣ ✥ ✕ ✫ ✴ ✭ ✌ ☛ iff ✢ ✣ ✥ ✕ ★ ✫ ✴ ✭ ☛ for all ✕ ★ ✲ ✣ .

Given a formula ✎ , ✱ ✭ ✢ ✣ ✥ ✕ ✫ is called a a0 -model of ✎ if ✱ ✴ ✭ ✎ . We use ✌ ✱ ✔ ✬ ✢ ✎ ✫ to denote the set of all a0 - models of ✎ . For objective formulas a0 , ✱ ✔ ✬ ✢ a0 ✫ denotes the set of models of a0 , and ✕ ✴ ✭ a0 denotes that ✕ is a model of a0 . For a formula ☛ , we say that ✎ entails ☛ , denoted as ✎ ✴ ✭ ☛ , if for every a0 -model ✱ of ✎ , ✱ ✴ ✭ ☛ .

Now the basic problem of knowledge update that we would like to investigate is formally described as follows: given a a0 - model ✱ ✭ ✢ ✣ ✥ ✕ ✫ , that is usually viewed as a knowledge state of an agent, and a formula ✍ - the agent's new knowledge that may contain modal operator ✌ , how do we update ✱ to another a0 -model ✱ ★ ✭ ✢ ✣ ★ ✥ ✕ ★ ✫ such that ✱ ★ ✴ ✭ ✍ and ✱ ★ is minimally different from ✱ with respect to some criterion. To approach this problem, we first need to provide a definition of closeness between two a0 -models with respect to a given a0 -model.

Definition 2 ( a0 -model Closeness) Let ✱ ✭ ✢ ✣ ✥ ✕ ✫ , ✱ ✑ ✭ ✢ ✣ ✑ ✥ ✕ ✑ ✫ and ✱ ✰ ✭ ✢ ✣ ✰ ✥ ✕ ✰ ✫ be three k-models. We say ✱ ✑ is as close to ✱ as ✱ ✰ , denoted as ✱ ✑ ✳ ✴ ✱ ✰ , if:

1. ✢ ✕ ✑ ✶ ✕ ✸ ✕ ✶ ✕ ✑ ✫ ✻ ✢ ✕ ✰ ✶ ✕ ✸ ✕ ✶ ✕ ✰ ✫ ; or
2. ✕ ✑ ✭ ✕ ✰ and one of the following conditions holds:
3. (i) if ✣ ✻ ✣ ✑ , then (a) there exist some a0 and ✁ such that ✱ ✴ ✭ ✌ a0 and ✱ ✰ ✾ ✴ ✭ ✌ a0 and ✱ ✾ ✴ ✭ ✌ ✁ and ✱ ✰ ✴ ✭ ✌ ✁ , or (b) for any a0 if ✱ ✴ ✭ ✌ a0 and ✱ ✑ ✾ ✴ ✭ ✌ a0 , then ✱ ✰ ✾ ✴ ✭ ✌ a0 ;
4. (ii) if ✣ ✑ ❀ ✣ , then condition (a) above is satisfied, or (c) for any a0 if ✱ ✾ ✴ ✭ ✌ a0 and ✱ ✑ ✴ ✭ ✌ a0 , then ✱ ✰ ✴ ✭ ✌ a0 ;
5. (iii) if ✣ ✾ ❀ ✣ ✑ and ✣ ✑ ✾ ❀ ✣ , then conditions (b) and (c) above are satisfied.

We denote ✱ ✑ ❄ ✴ ✱ ✰ if ✱ ✑ ✳ ✴ ✱ ✰ and ✱ ✰ ✾ ✳ ✴ ✱ ✑ .

In the above definition, condition 1 simply says that the symmetric differences between ✕ and ✕ ✑ is not bigger than that between ✕ and ✕ ✰ , while in condition 2, (i), (ii) and (iii) express that different preferences are applied to compare knowledge between ✱ ✑ and ✱ ✰ with respect to ✱ . For convenience, given a a0 -model ✱ , if we denote ✌ ✱ ✭

✘ a0 ✴ for all ✕ ✲ ✣ ✥ ✕ ✴ ✭ a0 ✚ , then (a) is equivalent to ✌ ✱ ✶ ✌ ✱ ✰ ✾ ✭ ❉ and ✌ ✱ ✰ ✶ ✌ ✱ ✾ ✭ ❉ ; (b) is equivalent to ✌ ✱ ✶ ✌ ✱ ✑ ✻ ✌ ✱ ✶ ✌ ✱ ✰ ; and (c) is equivalent to ✌ ✱ ✑ ✶ ✌ ✱ ✻ ✌ ✱ ✰ ✶ ✌ ✱ . Also (b) and (c) together present a difference on both knowledge decrease and increase between ✱ ✑ and ✱ ✰ in terms of ✱ . It is also easy to see that ✳ ✴ is a partial ordering.

Note that during the comparison between two a0 -models, we give preference to the change of the actual world over the change of the knowledge about the world. (The closeness criterion between actual worlds that we use is the commonly used criterion [Winslett, 1988] based on symmetric difference). For instance, if the actual world of a a0 -model ✱ ✑ is closer to the actual world of ✱ than the actual world of another a0 -model ✱ ✰ , we will think ✱ ✑ is closer to ✱ and the comparison of knowledge between ✱ ✑ and ✱ ✰ is ignored. Only when both ✱ ✑ and ✱ ✰ have the same actual world, we will compare the knowledge of ✱ ✑ and ✱ ✰ in terms of ✱ . This seems to be intuitive to us. In fact, the comparison between actual worlds determines the actual distance between two a0 -models to the given a0 -model ✱ . If ✱ ✑ and ✱ ✰ have the same actual distance to ✱ , the knowledge distance is then taken into account.

Basically, condition (i) (or (ii) resp.) in Definition 2 defines a knowledge preference based on knowledge decrease (or increase resp). That is, if ✱ ✑ only looses knowledge from ✱ (or only gains some knowledge to ✱ , resp.), then ✱ ✑ is preferred over those a0 -models that have both knowledge decrease and increase from ✱ , i.e. (a), and also preferred over those a0 -models that only loose more knowledge from ✱ (or addmore knowledge to ✱ , resp.) than ✱ ✑ does, i.e. (b) or (c) respectively. Condition (iii), on the other hand, deals with the mixed situation that ✱ ✑ has both knowledge decrease and increase from ✱ . In this case, a combined difference on knowledge decrease and increase is applied to determine the knowledge distance, i.e. (b) and (c). Conditions (i), (ii) and (iii) can be illustrated by the following figures respectively.

Definition 3 ( a0 -model Update) Let ✱ ✭ ✢ ✣ ✥ ✕ ✫ be a kmodel and ✍ a formula. A k-model ✱ ★ ✭ ✢ ✣ ★ ✥ ✕ ★ ✫ is called a possible resulting a0 -model after updating ✱ with ✍ if and only if the following conditions hold:

1. ✱ ★ ✴ ✭ ✍ ;
2. there does not exist another k-model ✱ ★ ★ ✭ ✢ ✣ ★ ★ ✥ ✕ ★ ★ ✫ such that ✱ ★ ★ ✴ ✭ ✍ and ✱ ★ ★ ❄ ✴ ✱ ★ .

We denote the set of all possible resulting a0 -models after updating ✱ with ✍ as ✧ ✆ ☎ ✢ ✱ ✥ ✍ ✫ .

Example 1 Let ✎ ✘ ✌ ☎ ✓ ✒ ✌ ✁ ✓ ✒ ✌ ✂ ✓ ✌ ✢ ✁ ✎ ✂ ✫ and ✍ ✘ ✌ ✒ ☎ . We denote

Clearly, ✱ a0 ✭ ✢ ✘ ✕ a0 ✥ ✕ ✑ ✥ ✕ ✰ ✚ ✥ ✕ a0 ✫ is a a0 -model of ✎ . Consider the update of ✱ a0 with ✍ . Let ✱ ✑ ✭ ✢ ✘ ✕ ✄ ✥ ✕ ☎ ✥ ✕ ✝ ✚ ✥ ✕ ✄ ✫ . Now we show that ✱ ✑ is a possible resulting a0 -model after updating ✱ a0 with ✍ .

Since ✢ ✕ a0 ✶ ✕ ✄ ✸ ✕ ✄ ✶ ✕ a0 ✫ ✭ ✘ ☎ ✚ , we first consider any possible a0 -model ✱ ★ ✭ ✢ ✣ ★ ✥ ✕ ★ ✫ such that ✢ ✕ a0 ✶ ✕ ★ ✸ ✕ ★ ✶ ✕ a0 ✫ ❀ ✘ ☎ ✚ . Clearly, the only possible ✕ ★ would be ✕ a0 itself. Let ✱ ★ ✭ ✢ ✣ ★ ✥ ✕ a0 ✫ , where ✣ ★ is a subset of ✘ ✕ a0 ✥ ✆ ✆ ✆ ✥ ✕ ✞ ✚ . However, since ☎ ✲ ✕ a0 , there does not exist any ✣ ★ such that ✱ ★ ✴ ✭ ✌ ✒ ☎ . Therefore, from Definition 2, only condition 2 can be used to find a possible ✱ ★ such that ✱ ★ ❄ ✴ ✱ ✑ . So we assume ✱ ★ ✭ ✢ ✣ ★ ✥ ✕ ✄ ✫ . On the other hand, from ✱ a0 and ✱ ✑ , it is easy to see that ✌ ✱ a0 ✭ ✘ ☎ ✥ ✁ ✎ ✂ ✚ and ✌ ✱ ✑ ✭ ✘ ✒ ☎ ✥ ✁ ✎ ✂ ✚ 1 . Then we have ✌ ✱ a0 ✶ ✌ ✱ ✑ ✭ ✘ ☎ ✚ and ✌ ✱ ✑ ✶ ✌ ✱ a0 ✭ ✘ ✒ ☎ ✚ . Ignoring the detailed verifications, we can show that there does not exist such ✱ ★ ✭ ✢ ✣ ★ ✥ ✕ ✄ ✫ satisfying ✌ ✱ a0 ✶ ✌ ✱ ★ ✭ ✌ ✱ ★ ✶ ✌ ✱ a0 ✭ ❉ .

Based on the a0 -model update, updating a formula (knowledge set) ✎ in terms of another formula ✍ is then achieved by updating every a0 -model of ✎ with ✍ .

1 For simplicity, here we only consider the prime formulas ✟ in ✠ ✡ in the sense that if ✟ ☞ ✠ ✡ , then there is not another ✌ such that ✍ ✎ ✌ ✑ ✟ and ✌ ☞ ✠ ✡ .

Definition 4 (Knowledge Update) Let ✎ and ✍ be two formulas. The update of ✎ with ✍ , denoted as ✎ ✂ ✍ , is defined by ✌ ✱ ✔ ✬ ✢ ✎ ✂ ✍ ✫ ✭ ✕ ✴ ✗ ✙ ✴ ✛ ✜ ✣ ✥ ✧ ✧ ✆ ☎ ✢ ✱ ✥ ✍ ✫ .

3 Characterizing Knowledge Update

In this section, we first investigate basic properties of a0 - models, then provide alternative characterizations for different types of knowledge update and then show their equivalence with respect to our original characterization.

Proposition 1 Let ✱ ✑ ✭ ✢ ✣ ✑ ✥ ✕ ✑ ✫ and ✱ ✰ ✭ ✢ ✣ ✰ ✥ ✕ ✰ ✫ be two a0 -models. Then the following properties hold:

1. a0 ✲ ✌ ✱ ✑ iff ✣ ✑ ✻ ✱ ✔ ✬ ✢ a0 ✫ ;
2. ✣ ✑ ✻ ✣ ✰ iff ✌ ✱ ✰ ✻ ✌ ✱ ✑ ;
3. ✌ ✱ ✑ ✭ ✌ ✱ ✰ iff ✣ ✑ ✭ ✣ ✰ ;
4. Let ✱ ★ ✭ ✢ ✣ ✑ ✸ ✣ ✰ ✥ ✕ ★ ✫ , then ✌ ✱ ★ ✭ ✌ ✱ ✑ ✩ ✌ ✱ ✰ ;
5. Let ✕ ★ ✲ ✣ ✑ ✩ ✣ ✰ and ✱ ★ ✭ ✢ ✣ ✑ ✩ ✣ ✰ ✥ ✕ ★ ✫ , then ✌ ✱ ✑ ✸ ✌ ✱ ✰ ✻ ✌ ✱ ★ .

Given a set of a0 -models ✫ and a a0 -model ✱ , let ✳ ✴ be an orderingon ✫ as we defined inDefinition2. By ✱ ✬ ✞ ✢ ✫ ✥ ✳ ✴ ✫ we mean the set of all elements in ✫ that are minimal with respect to ordering ✳ ✴ . The following theorem shows that our knowledge update can be characterized by a minimal change criterion based on an ordering on a0 -models.

Theorem 1 Let ✎ and ✍ be two formulas. Then ✌ ✱ ✔ ✬ ✢ ✎ ✂ ✍ ✫ ✭ ✕ ✴ ✗ ✙ ✴ ✛ ✜ ✣ ✥ ✧ ✱ ✬ ✞ ✢ ✌ ✱ ✔ ✬ ✢ ✍ ✫ ✥ ✳ ✴ ✫ .

Proof: To prove the result, we only need to show that for each a0 -model ✱ of ✎ , ✧ ✆ ☎ ✢ ✱ ✥ ✍ ✫ ✭ ✱ ✬ ✞ ✢ ✌ ✱ ✔ ✬ ✢ ✍ ✫ ✥ ✳ ✴ ✫ . Let ✱ ★ ✲ ✧ ✆ ☎ ✢ ✱ ✥ ✍ ✫ . Since ✱ ★ ✴ ✭ ✍ , ✱ ★ ✲ ✌ ✱ ✔ ✬ ✢ ✍ ✫ . On the other hand, according to Definition 3, for any ✱ ★ ★ ✲ ✌ ✱ ✔ ✬ ✢ ✍ ✫ , we have ✱ ★ ✳ ✴ ✱ ★ ★ . That is, ✱ ★ ✲ ✱ ✬ ✞ ✢ ✌ ✱ ✔ ✬ ✢ ✍ ✫ ✥ ✳ ✴ ✫ . So ✧ ✆ ☎ ✢ ✱ ✥ ✍ ✫ ✻ ✱ ✬ ✞ ✢ ✌ ✱ ✔ ✬ ✢ ✍ ✫ ✥ ✳ ✴ ✫ . Similarly, we can show ✱ ✬ ✞ ✢ ✌ ✱ ✔ ✬ ✢ ✍ ✫ ✥ ✳ ✴ ✫ ✻ ✧ ✆ ☎ ✢ ✱ ✥ ✍ ✫ .

While the above theorem presents a general minimal change property of our knowledge update, we now give alternative characterizations of the update of ✎ with ✍ when ✍ has some specific forms. These specific forms present some of the important features of knowledge update, and their alternative characterization is handy when the use of the notion of knowledge update becomes an overkill. For example, the alternative characterization of sensing update below is a much simpler characterization that is used in reasoning about sensing actions [Scherl and Levesque, 1993; Son and Baral, 2000]. We now introduce a notation that will be useful in our following discussions. Let ✣ be a set of worlds and ✕ ✲ ✣ . By ✣ ✣ ✱ ✳ ✵ ✧ , we denote the set ✘ ✕ ★ ✴ ✕ ★ ✲ ✣ and ✕ ★ ✴ ✭ a0 iff ✕ ✴ ✭ a0 ✚ .

Proposition 2 Given ✎ and ✌ a0 where a0 is objective and ✎ ✴ ✭ a0 . Then ✱ ★ ✭ ✢ ✣ ★ ✥ ✕ ★ ✫ is a a0 -model of ✎ ✂ ✌ a0 if and only if there exists a a0 -model ✱ ✭ ✢ ✣ ✥ ✕ ✫ of ✎ such that ✕ ✭ ✕ ★ and ✣ ★ ✭ ✣ ✣ ✱ ✳ ✵ ✧

The above proposition reveals an important property about knowledge update: to know some fact, the agent only needs to restrict the current possibleworlds in each of her a0 -models, if this fact itself is already entailed by her current knowledge set. We call this kind of knowledge update gaining knowledge update.

Example 2 Let ✎ ✘ ✁ ✓ ✒ ✌ ✁ ✓ ✌ ✂ . Suppose ✕ a0 ✭ ✘ ✁ ✥ ✂ ✚ , ✕ ✑ ✭ ✘ ✁ ✚ , ✕ ✰ ✭ ✘ ✂ ✚ and ✕ ✁ ✭ ❉ . Then ✎ has one a0 -model ✱ ✭ ✢ ✘ ✕ a0 ✥ ✕ ✰ ✚ ✥ ✕ a0 ✫ . Updating ✱ with ✌ ✁ , according to our a0 -model update definition, we have a unique resulting a0 - model ✱ ★ ✭ ✢ ✘ ✕ a0 ✚ ✥ ✕ a0 ✫ . Indeed, this result is also obtained from Proposition 2.

As a contrary case to the gaining knowledge update, we now characterize an agent ignoring a fact from her knowledge set which we call ignorance update, i.e. updating ✎ with ✒ ✌ a0 . From Definition 1, it is easy to see that ✎ ✂ ✒ a0 ✴ ✭ ✒ ✌ a0 . However, it should be noted that updating ✎ ✂ ✒ a0 can not be used to achieve ✎ ✂ ✒ ✌ a0 . Consider a a0 -model ✱ ✭ ✢ ✘ ✘ ✁ ✥ ✂ ✚ ✥ ✘ ✁ ✚ ✚ ✥ ✘ ✁ ✥ ✂ ✚ ✫ . Updating ✱ with ✒ ✌ ✁ we have a possible resulting a0 -model ✱ ★ ✭ ✢ ✘ ✘ ✁ ✥ ✂ ✚ ✥ ✘ ✁ ✚ ✥ ✘ ✂ ✚ ✚ ✥ ✘ ✁ ✥ ✂ ✚ ✫ , while updating ✱ with ✒ ✁ will lead to a possible result ✱ ★ ★ ✭ ✢ ✘ ✘ ✁ ✥ ✂ ✚ ✥ ✘ ✁ ✚ ✥ ✘ ✂ ✚ ✚ ✥ ✘ ✂ ✚ ✫ . Note that both ✱ ★ and ✱ ★ ★ entail ✒ ✌ ✁ , but ✱ ★ ❄ ✴ ✱ ★ ★ according to Definition 2.

Proposition 3 Given ✎ and ✍ ✘ ✒ ✌ a0 where a0 is objective. ✱ ★ ✭ ✢ ✣ ★ ✥ ✕ ★ ✫ is a a0 -model of ✎ ✂ ✒ ✌ a0 if and only if there exists a a0 -model ✱ ✭ ✢ ✣ ✥ ✕ ✫ of ✎ such that

• (i) if ✱ ✴ ✭ ✌ a0 , then ✕ ★ ✭ ✕ and ✣ ★ ✭ ✣ ✸ ✘ ✕ a0 ✚ , where ✕ a0 ✴ ✭ ✒ a0 ;
• (ii) otherwise, ✕ ★ ✭ ✕ and ✣ ★ ✭ ✣ .

Example 3 Suppose ✎ ✘ ✒ ✌ ✁ ✓ ✒ ✌ ✂ ✓ ✌ ✢ ✁ ✎ ✂ ✫ ✓ ✌ ☎ and the agent wants to ignore ☎ . Let ✕ a0 ✭ ✘ ✁ ✥ ✂ ✥ ☎ ✚ , ✕ ✑ ✭ ✘ ✁ ✥ ☎ ✚ , ✕ ✰ ✭ ✘ ✂ ✥ ☎ ✚ , ✕ ✁ ✭ ✘ ☎ ✚ , ✕ ✄ ✭ ✘ ✁ ✥ ✂ ✚ , ✕ ☎ ✭ ✘ ✁ ✚ , ✕ ✝ ✭ ✘ ✂ ✚ , ✕ ✞ ✭ ❉ . Clearly, ✎ has three a0 -models: ✱ a0 ✭ ✢ ✘ ✕ a0 ✥ ✕ ✑ ✥ ✕ ✰ ✚ ✥ ✕ a0 ✫ , ✱ ✑ ✭ ✢ ✘ ✕ a0 ✥ ✕ ✑ ✥ ✕ ✰ ✚ ✥ ✕ ✑ ✫ , and ✱ ✰ ✭ ✢ ✘ ✕ a0 ✥ ✕ ✑ ✥ ✕ ✰ ✚ ✥ ✕ ✰ ✫ . From Proposition 3, ✎ ✂ ✒ ✌ ☎ has the following twelve a0 -models: ✢ ✘ ✕ a0 ✥ ✕ ✑ ✥ ✕ ✰ ✥ ✕ ✁ ✚ ✥ ✕ ✄ ✫ , where ✬ ✭ ✆ ✥ ✞ ✥ ✠ ✥ ✡ and ☛ ✭ ☞ ✥ ✍ ✥ ✏ .

Nowwe consider the case when ✍ is of the form ✌ a0 ✎ ✌ ✒ a0 where a0 is objective. Updating ✎ with this type of ✍ is particularly useful in reasoning about sensing actions [Scherl and Levesque, 1993; Son and Baral, 2000] where ✌ a0 ✎ ✌ ✒ a0 represents the effect of a sensing action after whose execution, the agent will know either a0 or its negation. We refer to such an update as a sensing update. The following proposition characterizes the update of ✎ with a formula of the form ✌ a0 ✎ ✌ ✒ a0 . It is interesting to note that the sufficient and necessary condition for a a0 -model of ✎ ✂ ✢ ✌ a0 ✎ ✌ ✒ a0 ✫ is similar to the one presented in Proposition 2.

Proposition 4 Given ✎ and ✍ ✘ ✌ a0 ✎ ✌ ✒ a0 where a0 is objective. ✱ ★ ✭ ✢ ✣ ★ ✥ ✕ ★ ✫ is a a0 -model of ✎ ✂ ✢ ✌ a0 ✎ ✌ ✒ a0 ✫ if and only if there exists a a0 -model ✱ ✭ ✢ ✣ ✥ ✕ ✫ of ✎ such that ✕ ✭ ✕ ★ and ✣ ★ ✭ ✣ ✣ ✱ ✳ ✵ ✧ or ✕ ✭ ✕ ★ and ✣ ★ ✭ ✣ ✣ ✱ ✳ ✒ ✵ ✧

Proof: Let ✍ ✘ ✌ a0 ✎ ✌ ✒ a0 and ✱ ★ ✭ ✢ ✣ ✣ ✱ ✳ ✵ ✧ ✥ ✕ ✫ . From the definition of ✣ ✣ ✱ ✳ ✵ ✧ , it is easy to see that ✱ ★ ✴ ✭ ✍ .

Consider any ✱ ★ ★ ✭ ✢ ✣ ★ ★ ✥ ✕ ★ ★ ✫ where ✱ ★ ★ ✴ ✭ ✍ and ✕ ★ ★ ✾ ✭ ✕ . According to the condition 1 of Definition 2, ✱ ★ ❄ ✴ ✱ ★ ★ . So ✱ ★ ★ can not be a a0 -model of ✎ ✂ ✍ . In other words, each a0 -model of ✎ ✂ ✍ must have a form of ✱ ★ ★ ✭ ✢ ✣ ★ ★ ✥ ✕ ✫ . Then from Theorem 1, to prove the result, it is sufficient to prove for a0 -model ✱ ★ ★ ✭ ✢ ✣ ★ ★ ✥ ✕ ✫ where ✣ ★ ★ ✾ ✭ ✣ ✣ ✱ ✳ ✵ ✧ or ✣ ★ ★ ✾ ✭ ✣ ✣ ✱ ✳ ✒ ✵ ✧ , ✱ ★ ✳ ✴ ✱ ★ ★ . This can be shown in the same way as in the proof of Proposition 2.

Example 4 Suppose ✎ ✘ ✌ ✂ ✓ ✒ ✌ ✁ ✓ ✒ ✌ ✒ ✁ represents the current knowledge of an agent. Note that ✎ implies that the agent does not have any knowledge about ✁ . Consider the update of ✎ with ✍ ✘ ✌ ✁ ✎ ✌ ✒ ✁ which can be thought of as the agent trying to reason - in the planning or plan verification stage - about a sensing action 2 that will give her the knowledge about ✁ . Let ✕ a0 ✭ ✘ ✁ ✥ ✂ ✚ ✥ ✕ ✑ ✭ ✘ ✂ ✚ ✥ ✕ ✰ ✭ ✘ ✁ ✚ and ✕ ✁ ✭ ❉ . It is easy to see that ✱ a0 ✭ ✢ ✘ ✕ a0 ✥ ✕ ✑ ✚ ✥ ✕ a0 ✫ and ✱ ✑ ✭ ✢ ✘ ✕ a0 ✥ ✕ ✑ ✚ ✥ ✕ ✑ ✫ are two a0 -models of ✎ . Then according to the above proposition, it is obtained that ✱ ★ a0 ✭ ✢ ✘ ✕ a0 ✚ ✥ ✕ a0 ✫ and ✱ ★ ✑ ✭ ✢ ✘ ✕ ✑ ✚ ✥ ✕ ✑ ✫ are the two a0 -models of ✎ ✂ ✍ .

As another important type of knowledge update, we consider the update of ✎ with ✍ ✘ ✒ ✌ a0 ✓ ✒ ✌ ✒ a0 . This update can be thought of as the result of an agent forgetting her knowledge about the fact a0 . We will refer to such an update as a forgetting update. The following proposition shows that in order to forget a0 from ✎ , for each a0 -model of the current knowledge set, the agent only needs to expand the set of possible worlds of this model with exactly one specific world.

Proposition 5 Given ✎ and ✍ ✘ ✒ ✌ a0 ✓ ✒ ✌ ✒ a0 where a0 is objective. ✱ ★ ✭ ✢ ✣ ★ ✥ ✕ ★ ✫ is a a0 -model of ✎ ✂ ✍ if and only if there exists a a0 -model ✱ ✭ ✢ ✣ ✥ ✕ ✫ of ✎ such that

• (i) if ✱ ✴ ✭ ✌ a0 , then ✕ ★ ✭ ✕ and ✣ ★ ✭ ✣ ✸ ✘ ✕ a0 ✚ , where ✕ a0 ✴ ✭ ✒ a0 ;
• (ii) if ✱ ✴ ✭ ✌ ✒ a0 , then ✕ ★ ✭ ✕ and ✣ ★ ✭ ✣ ✸ ✘ ✕ a0 ✚ , where ✕ a0 ✴ ✭ a0 ;
• (iii) otherwise, ✕ ★ ✭ ✕ and ✣ ★ ✭ ✣ .

Proof: Let ✍ ✘ ✒ ✌ a0 ✓ ✒ ✌ ✒ a0 and ✱ ✭ ✢ ✣ ✥ ✕ ✫ be a a0 - model of ✎ . Then it is easy to see that for two a0 -models ✱ ★ ✭ ✢ ✣ ★ ✥ ✕ ★ ✫ and ✱ ★ ★ ✭ ✢ ✣ ★ ★ ✥ ✕ ★ ★ ✫ such that ✱ ★ ✴ ✭ ✍ and ✱ ★ ★ ✴ ✭ ✍ , and ✕ ★ ✭ ✕ and ✕ ★ ★ ✾ ✭ ✕ , ✱ ★ ❄ ✴ ✱ ★ ★ . So ✱ ★ ★ can not be a a0 -model of ✎ ✂ ✍ . In other words, a a0 -model of ✎ ✂ ✍ must have a form ✱ ★ ✭ ✢ ✣ ★ ✥ ✕ ✫ .

From Theorem 1, to prove the result, we only need to show that for any a0 -model ✱ ★ ★ ✭ ✢ ✣ ★ ★ ✥ ✕ ✫ such that ✱ ★ ★ ✴ ✭ ✍ and ✣ ★ ★ ✾ ✭ ✣ ✸ ✘ ✕ a0 ✚ , ✱ ★ ✳ ✴ ✱ ★ ★ .

Let ✱ ✭ ✢ ✣ ✸ ✘ ✕ a0 ✚ ✥ ✕ ✫ , where ✕ a0 ✴ ✭ ✒ a0 if ✱ ✴ ✭ ✌ a0 and ✕ a0 ✴ ✭ a0 if ✱ ✴ ✭ ✌ ✒ a0 . We first prove that for any a0 - model ✱ ★ ★ ✭ ✢ ✣ ★ ★ ✥ ✕ ✫ such that ✱ ★ ★ ✴ ✭ ✍ and ✣ ★ ★ does not have a form of ✣ ✸ ✘ ✕ ✁ ✚ , ✱ ★ ✳ ✴ ✱ ★ ★ .

Suppose ✱ ✴ ✭ ✌ a0 . Clearly ✱ ★ ✴ ✭ ✍ .

Case 1. Consider a a0 -model ✱

✭

✢

✣

✥

✕

✫ where ✣

✭

2 Such reasoning is necessary in creating plans with sensing actions or verifying such plans. On the other hand after the execution of a sensing action the agent exactly knows either ✔ or ✕ ✔ , and can simply use the notion of belief update.

★

★

★

★

★

✣ ✸ ✘ ✕ a0 ✚ ✻ ✣ ★ ★ . Note that ✱ ★ ★ ✴ ✭ ✍ as well. However, from Proposition 1, we have ✌ ✱ ★ ★ ✻ ✌ ✱ ★ ✻ ✌ ✱ ✱ ★ ✳ ✴ ✱ ★ ★ according to Definition 2 (i.e. condition (b)).

. So Case 2. Suppose ✣ ★ ★ ❀ ✣ ★ (proper set inclusion). Without loss of generality, we assume that ✣ ★ ★ ✭ ✣ ✸ ✘ ✕ a0 ✚ ✶ ✘ ✕ ✄ ✚ where ✕ ✄ ✲ ✣ . This follows that ✣ ✾ ❀ ✣ ★ ★ and ✣ ★ ★ ✾ ❀ ✣ . So it is the case that ✌ ✱ ✶ ✌ ✱ ★ ★ ✾ ✭ ❉ and ✌ ✱ ★ ★ ✶ ✌ ✱ ✾ ✭ ❉ . On the other hand, we have ✣ ✻ ✣ ★ , from Definition 2 (i.e. condition (a)), we have ✱ ★ ✳ ✴ ✱ ★ ★ .

Case 3. Now suppose ✣ ★ ★ ✾ ❀ ✣ ★ and ✣ ★ ✾ ❀ ✣ ★ . Without loss of generality, we can assume that ✣ ★ ★ ✭ ✣ ✸ ✘ ✕ a0 ✥ ✕ ✁ ✚ ✶ ✘ ✕ ✄ ✚ , where ✕ ✄ ✲ ✣ and ✕ a0 ✥ ✕ ✄ ✾ ✲ ✣ . Again, this results to the situation that ✣ ✾ ❀ ✣ ★ ★ and ✣ ★ ★ ✾ ❀ ✣ . ¿From the above discussion, it implies that ✱ ★ ✳ ✴ ✱ ★ ★ .

Following the same way as above, we can prove that under the condition that ✱ ✴ ✭ ✌ ✒ a0 and ✱ ★ ✭ ✢ ✣ ✸ ✘ ✕ a0 ✚ ✥ ✕ ✫ where ✕ a0 ✴ ✭ a0 , for any a0 -model ✱ ★ ★ ✭ ✢ ✣ ★ ★ ✥ ✕ ✫ such that ✱ ★ ★ ✴ ✭ ✍ and ✣ ★ ★ does not have a formof ✣ ✸ ✘ ✕ ✄ ✚ ✱ ★ ✳ ✴ ✱ ★ ★ .

Nowwe show that for any a0 -model ✱ ★ ★ that is of the form ✱ ★ ★ ✭ ✢ ✣ ✸ ✘ ✕ ✁ ✚ ✥ ✕ ✫ and ✕ ✁ is any worldsuch that ✕ ✁ ✴ ✭ ✒ a0 if ✱ ✴ ✭ ✌ a0 or ✕ ✁ ✴ ✭ a0 if ✱ ✴ ✭ ✌ ✒ a0 , ✱ ★ ✾ ✳ ✴ ✱ ★ ★ and ✱ ★ ★ ✾ ✳ ✴ ✱ ★ . Suppose ✱ ★ ✳ ✴ ✱ ★ ★ . Since ✣ ✻ ✣ ✸ ✘ ✕ a0 ✚ , then according to Definition 2, condition (a) or (b) should be satisfied. As ✣ ✻ ✣ ✸ ✘ ✕ ✁ ✚ , condition (a) can not be satisfied. So condition (b) must be satisfied. That is, for any ✁ such that ✱ ✴ ✭ ✌ ✁ and ✱ ★ ✾ ✴ ✭ ✌ ✁ , ✱ ★ ★ ✴ ✭ ✌ ✁ . However, this implies that ✌ ✱ ✶ ✌ ✱ ★ ✻ ✌ ✱ ✶ ✌ ✱ ★ ★ , and also ✌ ✱ ✩ ✌ ✱ ★ ★ ✻ ✌ ✱ ✩ ✌ ✱ ★ . From Proposition 1 (Results 2 and 4), it follows that ✣ ✸ ✣ ★ ✻ ✣ ✸ ✣ ★ ★ , that is, ✣ ✸ ✘ ✕ a0 ✚ ✻ ✣ ✸ ✘ ✕ ✁ ✚ . Obviously, this is not true. Similarly, we can show that ✱ ★ ★ ✾ ✳ ✴ ✱ ★ . That means, both ✱ ★ and ✱ ★ ★ are in ✧ ✆ ☎ ✢ ✱ ✥ ✍ ✫ . This completes our proof.

Example 5 Suppose ✎ ✘ ✌ ✂ ✓ ✢ ✌ ✁ ✎ ✌ ✒ ✁ ✫ represents the current knowledge of an agent. After executing a forgetting action the agent now would like to update her knowledge with ✍ ✘ ✒ ✌ ✁ ✓ ✒ ✌ ✒ ✁ . Let ✕ a0 ✭ ✘ ✁ ✥ ✂ ✚ ✥ ✕ ✑ ✭ ✘ ✂ ✚ ✥ ✕ ✰ ✭ ✘ ✁ ✚ ✥ ✕ ✁ ✭ ❉ . It is easy to see that ✱ a0 ✭ ✢ ✘ ✕ a0 ✚ ✥ ✕ a0 ✫ and ✱ ✑ ✭ ✢ ✘ ✕ ✑ ✚ ✥ ✕ ✑ ✫ are the two a0 -models of ✎ . Then using Proposition 5, we conclude that ✱ ★ a0 ✭ ✢ ✘ ✕ a0 ✥ ✕ ✑ ✚ ✥ ✕ a0 ✫ , ✱ ★ ✑ ✭ ✢ ✘ ✕ a0 ✥ ✕ ✁ ✚ ✥ ✕ a0 ✫ , ✱ ★ ✰ ✭ ✢ ✘ ✕ ✑ ✥ ✕ a0 ✚ ✥ ✕ ✑ ✫ , and ✱ ★ ✁ ✭ ✢ ✘ ✕ ✑ ✥ ✕ ✰ ✚ ✥ ✕ ✑ ✫ are the four a0 -models of ✎ ✂ ✍ . Note that ✢ ✘ ✕ a0 ✥ ✕ ✰ ✚ ✥ ✕ a0 ✫ cannot be a a0 -model of ✎ ✂ ✍ according to Proposition 5.

4 Persistence of Knowledge and Ignorance

Like most systems that do dynamic modeling, the knowledge update discussed previously is non-monotonic in the sense that while adding new knowledge into a knowledge set, some previous knowledge in the set might be lost. However, it is important to investigate classes of formulas that are persistent with respect to an update, as this may partially simplify the underlying inference problem [Engelfreit, 1998; Zhang, 1999]. Given ✎ and ✍ , a formula ☛ is said tobe persistent with respect to the update of ✎ with ✍ , if ✎ ✴ ✭ ☛ implies ✎ ✂ ✍ ✴ ✭ ☛ . If ☛ is of the form ✌ a0 , we call this persistence as knowledge persistence, while if ☛ is of the form ✒ ✌ a0 , we call it ignorance persistence. The question that we address now is that under what conditions, a formula ☛ is persistent with respect to the update of ✎ with ✍ .

As the update of ✎ with ✍ is achieved based on the update of every a0 -model of ✎ with ✍ , our task reduces to the studyof persistence with respect to a a0 -model update. This is defined in the following definition.

Definition 5 (Persistencewith respect to a0 -model Update) Let ✍ and ☛ be two formulas and ✱ be a a0 -model. ☛ is persistent with respect to the update of ✱ with ✍ if for any ✱ ★ ✲ ✧ ✆ ☎ ✢ ✱ ✥ ✍ ✫ , ✱ ✴ ✭ ☛ implies ✱ ★ ✴ ✭ ☛ .

Clearly a formula ☛ is persistent with respect to the update of ✎ with ✍ if and only if for each a0 -model ✱ of ✎ , ☛ is persistent with respect to the update of ✱ with ✍ . To characterize the persistence property with respect to a0 -model updates, we first define a preference ordering on a0 -models in terms of a formula.

Definition 6 (Formula Closeness) Let ✍ be a formula and ✱ ✑ and ✱ ✰ be two a0 -models. We say ✱ ✑ is as close to ✍ as ✱ ✰ , denoted as ✱ ✑ ✳ a0 ✱ ✰ , if one of the following conditions holds:

1. ✱ ✑ ✲ ✌ ✱ ✔ ✬ ✢ ✍ ✫ ;
2. if ✱ ✑ ✥ ✱ ✰ ✾ ✲ ✌ ✱ ✔ ✬ ✢ ✍ ✫ , then for any ✱ ✲ ✌ ✱ ✔ ✬ ✢ ✍ ✫ , ✱ ✑ ✳ ✴ ✱ ✰ .

Intuitively, the above definition specifies a partial ordering tomeasure the closeness between two a0 -models to a formula. In particular, if ✱ ✑ is a a0 -model of ✍ , then ✱ ✑ is closer to ✍ than all other a0 -models (i.e. condition 1). If neither ✱ ✑ nor ✱ ✰ is a a0 -model of ✍ , then the comparison between ✱ ✑ and ✱ ✰ with respect to ✍ is defined based on the a0 -model preference ordering ✳ ✴ for each a0 -model ✱ of ✍ (i.e. condition 2). Note that if both ✱ ✑ and ✱ ✰ are a0 -models of ✍ , we have ✱ ✑ ✳ a0 ✱ ✰ and ✱ ✰ ✳ a0 ✱ ✑ , and both of them are equally close to ✍ .

Example 6 Let ✍ ✘ ✌ ✁ ✓ ✌ ✂ , ✕ a0 ✭ ✘ ✁ ✥ ✂ ✚ , ✕ ✑ ✭ ✘ ✂ ✚ , ✕ ✰ ✭ ✘ ✁ ✚ and ✕ ✁ ✭ ❉ . Clearly, ✍ has one a0 -model ✱ ✭ ✢ ✘ ✕ a0 ✚ ✥ ✕ a0 ✫ . Consider two a0 -models ✱ ✑ ✭ ✢ ✘ ✕ a0 ✥ ✕ ✑ ✚ ✥ ✕ a0 ✫ and ✱ ✰ ✭ ✢ ✘ ✕ ✑ ✥ ✕ ✰ ✚ ✥ ✕ ✑ ✫ . Now let us compare which one of them is closer to ✍ . Since neither ✱ ✑ nor ✱ ✰ is a a0 -model of ✍ , we can use condition 2 in Definition 6 to compare ✱ ✑ and ✱ ✰ . According to Definition 2, it is easy to see that ✱ ✑ ✳ ✴ ✱ ✰ as ✕ a0 ✶ ✕ ✑ ✸ ✕ ✑ ✶ ✕ a0 ✭ ✘ ✁ ✚ ✾ ✭ ❉ . Therefore, we conclude ✱ ✑ ✳ a0 ✱ ✰ . Furthermore, we also have ✱ ✑ ❄ a0 ✱ ✰ .

Proposition 6 Let ✍ be a formula. For any two a0 -models ✱ ✑ and ✱ ✰ , if ✱ ✑ ✳ a0 ✱ ✰ , then ✱ ✰ ✴ ✭ ✍ implies ✱ ✑ ✴ ✭ ✍ .

Proof: Suppose ✱ ✰ ✴ ✭ ✍ . Then ✱ ✰ ✲ ✌ ✱ ✔ ✬ ✢ ✍ ✫ . From Definition 6, we know that for any other a0 -model ✱ ★ , ✱ ✰ ✳ a0 ✱ ★ . So ✱ ✰ ✳ a0 ✱ ✑ . But we have ✱ ✑ ✳ a0 ✱ ✰ . This implies that both ✱ ✑ and ✱ ✰ are equally close to ✍ . Hence, ✱ ✑ ✴ ✭ ✍ .

Given a formula ✍ and a sequence of a0 -models ✱ ✑ ✥ ✆ ✆ ✆ ✥ ✱ ✖ , if the relation ✱ ✑ ✳ a0 ✱ ✰ ✳ a0 ✆ ✆ ✆ ✳ a0 ✱ ✖ holds, then it means that ✱ ✁ is closer to ✍ than ✱ ✄ , where

• ✬ ❄ ☛ . Now under this condition, if there is another formula ☛ which satisfies the property that ✱ ✄ ✴ ✭ ☛ implies ✱ ✁ ✴ ✭ ☛ whenever ✬ ❄ ☛ , we say that formula ☛ is persistent with respect to formula ✍ . In other words, when a0 -models move closer to ✍ , ☛ 's truth value is preserved in these a0 -models. The following definition formalizes this idea.

Definition 7 ( ✳ a0 -persistence) Let ☛ , ✍ be two formulas. We say that ☛ is ✳ a0 -persistent if for any two a0 -models ✱ ✑ and ✱ ✰ , ✱ ✰ ✴ ✭ ☛ and ✱ ✑ ✳ a0 ✱ ✰ implies ✱ ✑ ✴ ✭ ☛ .

Now we have the following important relationship between ✳ a0 -persistence and a0 -model update persistence.

Theorem 2 Let ☛ and ✍ be two formulas and ✱ be a a0 - model. ☛ is persistent with respect to the update of ✱ with ✍ if ☛ is ✳ a0 -persistent.

Proof: Let ✱ ★ be a a0 -model in ✧ ✆ ☎ ✢ ✱ ✥ ✍ ✫ . Then we have ✱ ★ ✲ ✌ ✱ ✔ ✬ ✢ ✍ ✫ . So for any a0 -model ✱ ★ ★ , we have ✱ ★ ✳ a0 ✱ ★ ★ . So ✱ ★ ✳ a0 ✱ . Now suppose ☛ is ✍ -persistent. It follows that ✱ ✴ ✭ ☛ implies ✱ ★ ✴ ✭ ☛ . As ✱ ★ is an arbitrary a0 -model in ✧ ✆ ☎ ✢ ✱ ✥ ✍ ✫ , we can conclude that ☛ is persistent with respect to the update of ✱ with ✍ .

From Theorem 2, we have that ✳ a0 -persistence is a sufficient condition to guarantee a formula persistence with respect to a a0 -model update. As will be shown next, we can provide a unique characterization for ✍ -persistence. We first define the notion of ordering preservation as follows.

Definition 8 (Ordering Preservation) Given two formulas ☛ and ☞ . We say that ordering ✳ a0 preserves ordering ✳ ✁ if for any two a0 -models ✱ ✑ and ✱ ✰ , ✱ ✑ ✳ a0 ✱ ✰ implies ✱ ✑ ✳ ✁ ✱ ✰ .

The intuition behind ordering preservation is clear. That is, if ✳ a0 preserves ✳ ✁ , then for any two a0 -models ✱ ✑ and ✱ ✰ , whenever ✱ ✑ is closer to ☛ than ✱ ✰ , ✱ ✑ will be closer to ☞ than ✱ ✰ as well. Finally, we have the following important result to characterize ✍ -persistence.

Theorem 3 Given two formulas ☛ and ✍ , ☛ is ✳ a0 -persistent if and only if ✳ a0 preserves ✳ a0 .

• Proof: (☎ ) Suppose ☛ is ✳ a0 -persistent. That is, for any two a0 -models ✱ ✑ and ✱ ✰ , ✱ ✑ ✳ a0 ✱ ✰ and ✱ ✰ ✴ ✭ ☛ implies ✱ ✑ ✴ ✭ ☛ . So under the constraint that ☛ is ✍ -persistent, whenever ✱ ✑ ✳ a0 ✱ ✰ , we have ✱ ✑ ✳ a0 ✱ ✰ . That means, ✳ a0 preserves ✳ a0 .
• (✆ ) Suppose ✳ a0 preserves ✳ a0 . From Definition 8, we have that for any two a0 -models ✱ ✑ and ✱ ✰ , ✱ ✑ ✳ a0 ✱ ✰ implies ✱ ✑ ✳ a0 ✱ ✰ . Now suppose ✱ ✑ ✳ a0 ✱ ✰ . So we have ✱ ✑ ✳ a0 ✱ ✰ . From Proposition 6, we have that ✱ ✰ ✴ ✭ ☛ implies ✱ ✑ ✴ ✭ ☛ . From this it follows that ☛ is ✳ a0 -persistent.

5 Conclusion and Future Directions

In this paper we developed the notion of knowledge update - an analogous notion to belief update, that is useful in characterizing the knowledge change of an agent in presence of new knowledge. Our notion is particularly relevant in reasoning about actions and plan verifications when there are sensing actions. We presented simpler alternative characterization of knowledge update for particular cases, and showed its equivalence to the original characterization. Finally we discussed when particular knowledge (or ignorance) persists with respect to a knowledge update.

We believe our work here to be a starting point on knowledge update, and as evident from the research in belief update and revision in the past decade. A lot remains to be done in knowledge update. For example, issues such as iterative knowledge update, abductive knowledge update, minimal knowledge in knowledge update, etc. remain to be explored. Similarly, in regards to reasoning about actions, additional specific cases of knowledge update need to be identified and simpler alternative characterization for them will be needed to be developed. Finally, we are currently working on establishing complexity results for knowledge update.

Acknowledgement

The authors thank Norman Foo and Abhaya Nayak for useful discussions on this topic. The research of the firat author was supported by NSF under grants IRI 9501577 and 0070463, and part of this research was performed while he was visiting the University of Western Sydney. The research of the second author was supported in part by Australian Research Council under grant A49803542.