On the Progression of Knowledge and Belief for Nondeterministic Actions in the Situation Calculus

1 Introduction

In the area of reasoning about actions, a fundamental problem is projection, which is to determine whether a query holds after a sequence of actions have occurred. A powerful solution to the projection problem is progression, which updates the initial knowledge base (KB) according to the effects of actions, and then checks whether the query holds in the resulting KB. Progression is widely used in planning and high-level program execution. Lin and Reiter [1997] pointed out STRIPS technology was a simple form of progression. To tackle the problem of conformant planning, Cimatti et al. [2004] used BDDs [Bryant, 1992] to represent KBs, and implemented progression via forgetting in propositional logic. Later, Bertoli et al. [2006] applied a similar idea in contingent planning. Recently, Fan et al. [2012] proposed an interpreter for first-order knowledge-based Golog with sensing via progression. The above works focus on world change. However, we also need to handle knowledge and belief change resulting from possibly nondeterministic actions in some scenarios.

For example, Alice is in a dark room with a computer, a heater and their switches. Alice knows that both the computer and the heater are on. Now, Alice wants to turn off the heater, knowing that she might but improbably press the wrong switch. Alice ends up pressing the wrong switch. As a result, the computer rather than the heater is off, Alice knows one of them is off and believes that the heater is off. After observing the heater is on, Alice revises her beliefs, and believes that the heater is on.

The above example illustrates that it is necessary to consider knowledge and belief change in some applications. There are some representative frameworks that accommodate knowledge and belief change. Scherl and Levesque [2003] proposed an epistemic extension to the situation calculus. Shapiro et al. [2011] integrated belief revision wrt accurate sensing into the situation calculus. Delgrande and Levesque [2012; 2013] furthered this work by considering nondeterminstic actions. Schwering and Lakemeyer [2014] extended the framework of [Shapiro et al., 2011] to the case of onlybelieving. In addition, Baltag and Smets [2008] proposed a general framework for integrating belief revision into dynamic epistemic logics (DELs) [van Ditmarsch et al., 2007]. They proposed the action priority update operation: when updating a plausibility model by an action plausibility model, give priority to the action plausibility order. By incorporating action priority update into the situation calculus, Fang and Liu [2013] developed a general framework for reasoning about actions and change in multi-agent scenarios.

The above works focus on how to represent knowledge and belief change. There also have been works on progression of knowledge and/or belief in DELs or the situation calculus. Herzig et al. [2003] studied the progression of positive knowledge wrt deterministic actions in the single-agent case. Laverny and Lang [2005a; 2005b] showed how to update graded beliefs wrt noisy observation actions and nondeterministic physical actions. However, their work is with the epistemic closed-world assumption (ECWA) [Herzig et al., 2003], i.e., if I cannot prove that I know φ, then I do not know φ. Aucher [2011] gave a syntactic representation of progression of multi-agent belief wrt epistemic actions in DELs. Nevertheless, the approach is essentially model-based: he made use of the so-called Kit-Fine formulas defined in [Moss, 2007]. A Kit-Fine formula of depth n provides a complete syntactic representation of the structure up to depth n of a pointed Kripke model. Moreover, his approach allows false beliefs. While these approaches are propositional, there are also some first-order treatments. By appealing to the logic of only-knowing [Levesque, 1990], which is an extension of the ECWA, Lakemeyer and Levesque [2009] studied progression of only-knowing in the single-agent case. Belle and Lakemeyer [2014] extended this work to the multi-agent case. Liu and Wen [2011] explored progression of knowledge (but not belief) under certain restrictions. However, they focused on deterministic actions.

In this paper, based on Fang and Liu's framework, we study progression of both knowledge and belief wrt nondeterministic actions in the single-agent propositional case without making the ECWA. We first present a model-theoretic definition of progression of knowledge and belief. We show that for propositional actions, i.e., actions whose precondition axioms and successor state axioms are propositional formulas, progression of knowledge and belief reduces to forgetting in the logic of knowledge and belief, which we show is closed under forgetting. Thus we are able to show that for propositional actions, progression of knowledge and belief is always definable in the logic of knowledge and belief. Since Fang and Liu's framework handles belief change including belief revision and update, our belief progression subsumes both belief revision and update.

This paper is organized as follows. Formal preliminaries are given in Section 2. In Section 3, we study forgetting in the logic of knowledge and belief. In Section 4, we investigate the progression of knowledge and belief. Section 5 considers progression for some special cases including epistemic actions and deterministic actions. Finally, Section 6 concludes this paper.

2 Preliminaries

In this section, we present Baltag and Smets' logic of knowledge and belief. Then we introduce Fang and Liu's extension of the situation calculus, specify the components of a single-agent basic action theory, and give the definition of knowledge and belief in the extended situation calculus. Finally, we introduce the assumptions we make in this paper.

2.1 The logic of knowledge and belief

Baltag and Smets gave the logic of knowledge and belief LKB based on plausibility models. The logic is obtained from the propositional language by adding a syntactic rule: if φ is a formula, then both Kφ and Bφ are formulas, where K and B are modal operators. Kφ (resp. Bφ) is read as "the agent knows (resp. believes) φ".

The semantic models are plausibility models, which are based on the concept of locally well-preordered relations.

Definition 2.1 A preorder ≤ is a reflexive and transitive binary relation. We use ∼ for the associated comparability relation, i.e., s ∼ t iff s ≤ t or t ≤ s. The comparability class for an element s, written [s], is the set {t | s ∼ t}. We say that ≤ is locally well-founded if every non-empty subset of every comparability class has a least element. A locally well-preordered relation is a locally well-founded preorder.

As usual, s ≤ t is read as "s is at least as plausible as t", and s ∼ t is read as "s and t are comparable" or "s and t are alternatives". We use s → t to denote that t is a least element of [s], and read it as "t is a most plausible alternative to s".

We fix a finite set of propositions P = {p1, · · · , pn}.

Definition 2.2 A plausibility model is a tuple (S,≤, V ), where S is a non-empty set of possible worlds, ≤ is a locally well-founded relation on S, and V : P → 2S assigns a subset of S to each proposition. A plausibility state is a pair (W, s), where W is a plausibility model and s is a world of S, called the actual world.

Definition 2.3 Let (W, s) be a plausibility state where W = (S, ≤, V ). We interpret formulas in LKB by induction:

• W, s |= p iff s ∈ V (p);
• W, s |= ¬φ iff W, s ̸|= φ;
• W, s |= φ ∧ ψ iff W, s |= φ and W, s |= ψ;
• W, s |= Kφ iff for every t s.t. s ∼ t, W, t |= φ;
• W, s |= Bφ iff for every t s.t. s → t, W, t |= φ.

Thus, the agent knows φ in s if φ holds in all alternatives to s, and she believes φ in s if φ holds in all the most plausible alternatives to s. We use ⊤ and ⊥ for true and false respectively. We write ˆKφ .= ¬K¬φ and ˆBφ .= ¬B¬φ. We say that a formula in LKB is objective if it does not contain any K or B operators.

The notion of knowledge is S5 knowledge (i.e., knowledge is truthful and both positively and negatively introspective), the notion of belief is KD45 belief (i.e., belief is consistent and introspective), and knowledge entails belief. That is, the following formulas are valid:

Finally, we introduce a normal form for formulas in LKB, and prove two fundamental properties.

Definition 2.4 An extended term is a formula of the form θ∧ Kψ ∧ ∧i ˆKηi ∧Bϕ∧ ∧i ˆBξi, where θ, ψ, ϕ, ηi and ξi are all objective, and the number of ηi's or ξi's is not zero.

Theorem 2.1 Every formula φ in LKB can be equivalently reduced to a formula without nested modalities, whose size is no more than that of φ.

Proof: We apply the following transformation rules, none of which increases the size of the formula. Here Oi are K or B.

1. O(φ ∧ψ) ≡ Oφ ∧Oψ, ˆO(φ ∨ψ) ≡ ˆOφ ∨ ˆOψ;
2. O1(φ∨O2ψ) ≡ O1φ∨O2ψ, O(φ∨ ˆOψ) ≡ Oφ∨ ˆOψ;
3. ˆO(φ∧Oψ) ≡ ˆOφ∧Oψ, ˆO1(φ∧ ˆO2ψ) ≡ ˆO1φ∧ ˆO2ψ;
4. ¬Oφ ≡ ˆO¬φ, OˆOφ = ˆOφ, ˆOOφ = Oφ;

Theorem 2.2 Every formula φ in LKB can be equivalently transformed to a disjunction of extended terms, whose size is at most 2l+4 , where l is the size of φ.

Proof: By Theorem 2.1, φ can be converted to a formula without nested modalities. We then apply the distributive law of ∨ over ∧ until we get a disjunction of conjunction of objective and modal formulas. We make each disjunct an extended term by adding ⊤, K⊤, ˆK⊤, B⊤, and/or ˆB⊤ conjuncts when necessary.

2.2 The situation calculus with plausibility orders

The situation calculus [Reiter, 2001] is a many-sorted firstorder language suitable for describing dynamic worlds. There are three disjoint sorts: action for actions, situation for situations, and object for everything else. A situation calculus language has the following components: a constant S0 denoting the initial situation; a binary function do(a, s) denoting the successor situation to s resulting from performing action a; a binary predicate s ⊏ s′ meaning that situation s is a proper subhistory of s′ ; a binary predicate Poss(a, s) meaning that action a is possible in situation s; a finite number of action functions; a finite number of relational and functional fluents, i.e., predicates and functions taking a situation term as their last argument, which denote relations and functions whose values vary from situation to situation; and a finite number of situation-independent predicates and functions.

The situation calculus has been extended to accommodate knowledge, belief and nondeterministic actions by Fang and Liu. They incorporated plausibility order and action priority update into the situation calculus. For an agent, there are plausibility orders on the set of situations and that of actions. To model plausibility order, they introduced a special fluent B(s′ , s) 1 , which means that the agent considers situation s′ at least as plausible as s. Similarly, they introduced a special predicate A(a′ , a, s), meaning that the agent considers that a′ is executed at least as plausible as that a is executed in situation s, to represent action plausibility orders.

We introduce the following abbreviations:

1. Init(s) .= ¬(∃a, s′ ).s = do(a, s′ );
2. Exec(s) .= (∀a, s∗ ).do(a, s∗ ) ⊑ s ⊃ Poss(a, s∗ );
3. K(s′ , s) .= B(s′ , s) ∨B(s, s′ ).

Intuitively, Init(s) says s is an initial situation, and Exec(s) means s is an executable situation, i.e., an action history in which it is possible to perform the actions one after the other. K(s′ , s) states that the agent considers s′ comparable to s.

Using a second-order formula, we define an abbreviation Lwf(s) saying that B(s′ , s) is locally well-founded:

Similarly, we can define an abbreviation Alwf(a, s) which says that A(a′ , a, s) is locally well-founded.

Based on Fang and Liu's approach, a single-agent domain is specified by a basic action theory (BAT) of the form:

1. Σ are the foundational axioms:
2. do(a, s) = do(a′ , s′ ) ⊃ a = a′ ∧ s = s′2 ;
3. (¬s ⊏ S0) ∧ (s ⊏ do(a, s′ ) ≡ s ⊑ s′ );
4. ∀P.∀s[Init(s)⊃P(s)] ∧ ∀a, s[P(s)⊃P(do(a, s))] ⊃ (∀s)P (s);

1 The B fluent taking two situation arguments is enough for the single-agent case although the original B fluent takes three situation arguments. The following A predicate is similar.

2 Throughout this paper, free variables are assumed to be universally quantified from outside.

• B(s′ , s) ⊃ [Init(s) ≡ Init(s′ )].

A model of these axioms consists of a forest of isomorphic trees rooted at the initial situations, which can be B-related to only initial situations.

1. Dap is a set of action precondition axioms (APAs), one for each action α, of the form Poss(α(⃗x), s) ≡ Πα(⃗x, s).
2. Dss is a set of successor state axioms (SSAs), one for each fluent F (including the B fluent), of the form F(⃗x, do(a, s)) ≡ ΦF (⃗x, a, s). These embody a solution to the frame problem [Reiter, 1991]. It includes the SSA for the B fluent as follows:

Intuitively, after action a is performed in situation s, the agent considers situation s′′ at least as plausible as do(a, s) iff s′′ is the result of doing some action a′ in some situation s′ , a is possible in s, a′ is possible in s′ , and either the agent considers a′ more plausible than a and s′ comparable to s, or she thinks that a′ and a are equally plausible and s′ is at least as plausible as s.

Thus the A predicate acts on the B-fluent via the SSA for the B-fluent. This is a dynamic generalization of AGM revision, giving priority to the new information (i.e., to actions) over previous beliefs.

1. Daa is a set of action plausibility axioms, one for each action function α, of the formA(a,α(⃗x),s)≡Ψα(a,⃗x,s).
2. Duna is the set of unique names axioms for actions.
3. DS0 , called the initial KB, is a set of sentences uniform in S0. We will make this more precise in Section 2.3.
4. BInit consists of axioms stating that B is locally wellpreordered in initial situations.
5. Reflexivity: Init(s) ⊃ B(s, s);
6. Transitivity: Init(s)∧B(s′,s)∧B(s′′, s′ )⊃B(s′′, s);
7. Locally well-founded: Init(s) ⊃ Lwf(s).
8. D |= AExec, which consists of axioms stating that A is locally well-preordered in executable situations.
9. Exec(s) ⊃ A(a, a, s);
10. Exec(s) ∧ A(a′ , a, s) ∧ A(a′′ , a′ , s) ⊃ A(a′′ , a, s);
11. Exec(s) ⊃ Alwf(a, s).

Throughout the paper, we use D for a BAT of this form. Then we can show that B is locally well-preordered in all executable situations.

We give the definition of mental attitudes knowledge and belief in the situation calculus. We begin with the MPB relation derived from the B fluent:

Intuitively, MPB(s′ , s) means that according to the agent, s′ is a most plausible situation in the comparability class of s.

Definition 2.6 (Knowledge and belief) Let φ(s) be a formula with a single free variable s.

1. The agent knows φ in situation s: K(φ, s) .= ∀s′ .K(s′ , s) ⊃ φ(s′ );
2. The agent believes φ in situation s: B(φ, s) .= ∀s′ .MPB(s′ , s) ⊃ φ(s′ ).

The desired properties of knowledge and belief also hold in executable situations, e.g., the truth axiom:

Example 1 We now formalize the example from the introduction. Assume that the observation action might be inaccurate. Let c(s) (resp. h(s)) denote that the computer (resp. heater) is on in situation s, αc (resp. αh) denote the action of flipping the switch for the computer (resp. heater), and oh (resp. o¬h) denote the action of observing h (resp. ¬h) holds. The axioms are:

• Poss(αh, s) ≡ Poss(αc, s) ≡ ⊤;
• Poss(oh, s) ≡ h(s); Poss(o¬h, s) ≡ ¬h(s);
• A(a′ , a, s) ≡ a = a′ ∨ a′ = αh ∧ a = αc ∨ a′ = oh ∧ a = o¬h;
• h(do(a, s)) ≡ h(s) ∧ a ̸= αh ∨ ¬h(s) ∧ a = αh;
• c(do(a, s)) ≡ c(s) ∧ a ̸= αc ∨ ¬c(s) ∧ a = αc.
• K(c ∧ h, S0).

After executing action αc and αh in S0, Sαc and Sαh are two new situations, and the latter is more plausible than the former since Alice believes she ends up pressing the right button. At the next level, Soh and S′o¬h are two new situations, and the order relation changes. This is because Alice considers truth of h more plausible than falsity of h. The above is illustrated with Figure 1.

2.3 Assumptions, terminology and notations

In this paper, we study the progression in the propositional case. So we shall assume:

1. All ordinary fluents are propositional fluents, i.e., unary predicates whose only argument is of sort situation.
2. All action functions take no arguments.
3. For each APA whose form is Poss(α, s) ≡ Πα(s), Πα(s) is uniform in s and does not use the B fluent. Each SSA is similar. Thus all the actions are propositional actions.
4. Except for the equality predicate, the language has no situation-independent predicates and functions.

Let Lsc be a situation calculus language. We use L to denote the situation-suppressed language to Lsc, i.e., the language obtained from Lsc by removing the sort situation and the B fluent, and removing the situation argument from every ordinary fluent. We use L′ to denote the primed version of L, i.e., for each ordinary fluent F(s), there is a proposition F ′ in L′ . We let L∗ denote the union of L and L′ . Intuitively, we can use L to talk about a situation σ, and use L′ to talk about a successor situation of σ. For a language L, say L, L′ , or L∗ , we use LKB to denote the language with K and B operators based on L.

Often, we need to restrict our attention to formulas that refer to a particular situation. For this purpose, we give the definition of uniform formulas as follows:

Definition 2.7 (Uniform formulas) Let σ be a fixed situation term and F a fluent. Then the formulas uniform in σ are the smallest set of formulas in Lsc satisfying:

We use φ[σ] to denote that φ is uniform in σ.

Let φ be a formula, µ and µ′ two expressions. We denote by φ[µ/µ′ ] the result of replacing every occurrence of µ in φ with µ′ . We use sitM to denote the domain of an Lscstructure M for sort situation. Let α be an action. We denote by Sα the situation term do(α, S0).

3 Forgetting in knowledge and belief

Zhang and Zhou [2009] studied forgetting in single-agent S5 modal logic. In this section, we extend the definition of forgetting to LKB, and show that it is always definable in LKB and computable.

Let X range over subsets of P. We start by introducing forgetting in propositional logic.

Definition 3.1 Let φ be a formula in L. forget(φ,X) is defined by induction on X as follows:

• forget(φ, ∅) .= φ;
• forget(φ, {p}) .= φ[p/⊤] ∨ φ[p/⊥];
• forget(φ,X ∪ {p}) .= forget(forget(φ, {p}),X).

To define forgetting in LKB, we extend the concept of Xbisimulation from [Zhang and Zhou, 2009].

Definition 3.2 Let (W, s) and (W ′ , s′ ) be two plausibility states where W=(S,≤, V ) and W ′ =(S′ ,≤′ , V ′ ). An Xbisimulation between (W, s) and (W ′, s′ ) is a relation R ⊆ S×S′ s.t. R(s, s′ ), and whenever R(t, t′ ), we have:

atoms t ∈ V (p) iff t′ ∈ V ′ (p) for all p ̸∈ X;

forth∼ For all u s.t. t ∼ u, there is u′ s.t. t′ ∼′ u′ and R(u, u′ );

forth→ For all u s.t. t → u, there is u′ s.t. t′ →′ u′ and R(u, u′ );

back∼ For all u′ s.t. t′ ∼′ u′ , there is u s.t. t ∼ u and R(u, u′ );

back→ For all u′ s.t. t′ →′ u′ , there is u s.t. t → u and R(u, u′ ).

We say that (W, s) and (W ′ , s′ ) are X-bisimilar, written (W, s)↔X (W ′ , s′ ), if there is an X-bisimulation between (W, s) and (W ′ , s′ ). For simplicity, we write ↔ for ↔∅ .

Below we define forgetting in LKB.

Definition 3.3 Let φ be a formula in LKB. A formula ψ is a result of forgetting X from φ, written kbforget(φ,X) ≡ ψ, if for any plausibility state (W, s), (W, s) is a model of φ iff there exists a model (W ′ , s′ ) of ψ s.t. (W, s)↔X (W ′ , s′ ).

Next, we analyze basic properties of forgetting. We say a formula φ irrelevant to an atom p, if it is equivalent to a formula which does not contain any occurrence of p.

Proposition 3.1 Let φ be a formula in LKB and kbforget(φ,X) ≡ ψ. Then, φ |= ψ and for any η irrelevant to every p ∈ X, φ |= η iff ψ |= η.

Proposition 3.2 · If φ is an objective formula in LKB, then kbforget(φ, X) ≡ forget(φ, X);

• If kbforget(φi,X) ≡ ψi (i = 1, 2), then kbforget(φ1 ∨ φ2, X) ≡ ψ1 ∨ ψ2.

The following proposition shows that extended terms are closed under forgetting.

Proposition 3.3 Let φ be an extended term θ∧Kψ∧∧i ˆKηi∧ Bϕ∧ ∧i ˆBξi. Let forget(θ ∧ψ,X) ≡ θ′ , forget(ψ,X) ≡ ψ′ , forget(ηi ∧ ψ, X) ≡ η′i , forget(ϕ ∧ ψ, X) ≡ ϕ′ , forget(ξi ∧ψ∧ϕ, X) ≡ ξ ′i . Then kbforget(φ, X) ≡ θ′ ∧Kψ′ ∧

Since every formula in LKB can be equivalently transformed to a disjunction of extended terms, by Propositions 3.2 and 3.3, we have:

Theorem 3.1 Forgetting in LKB is always definable in LKB and computable.

4 Progression of knowledge and belief

In this section, we begin with the definition of progression of knowledge and belief. Then we introduce the construction of the combination formula of an extended term wrt a propositional action, which contains information about the past and the present. Next, we show that progression of knowledge and belief reduces to forgetting in the combination formula. The forgetting operation eliminates all past information and preserves information about the present. Thus we are able to give a complete syntactic representation of progression of knowledge and belief for propositional actions in LKB.

4.1 Definition of progression

Intuitively, a progression of DS0 wrt an action α should be a set of sentences DSα with the following properties: 1. just as DS0 is uniform in S0, DSα should be uniform in Sα; 2. for all queries uniform in Sα, the old theory D is equivalent to the new theory (D - DS0 ) ∪ DSα .

To define progression, we first adapt the concept of bisimulation from the logic of knowledge and belief, and define a similarity relation between Lsc-structures. Roughly, a bisimulation is a relation between situations of two Lsc-structures where related situations agree on all ordinary fluents and have matching accessibility possibilities.

Definition 4.1 Let M and M ′ be Lsc-structures with the same domains for actions. Let γ ∈ sitM and γ ′ ∈ sitM′ . We write M, γ ∼ M ′ , γ ′ if there is a bisimulation R ⊆ sitM × sitM′ s.t. γRγ ′ , and whenever δRδ′ , we have:

1. M, δ ≡ M ′ , δ′ , denoting that M, δ and M ′ , δ′ agree on all ordinary fluents, that is, for every ordinary fluent F, M |= F(δ) iff M ′ |= F(δ′ ).
2. For all ρ s.t. KM(δ, ρ), there is ρ′ s.t. KM′(δ′ , ρ′ ) and ρRρ′ , (the forth condition for the K relation), here KM is the denotation of the K relation in M.
3. For all ρ s.t. MPBM(δ, ρ), there is ρ′ s.t. MPBM′(δ′ , ρ′ ) and ρRρ′ , (the forth condition for the MPB relation).
4. For all ρ′ s.t. KM′(δ′ , ρ′ ), there is ρ s.t. KM(δ, ρ) and ρRρ′ , (the back condition for the K relation).
5. For all ρ′ s.t. MPBM′(δ′ , ρ′ ), there is ρ s.t. MPBM(δ, ρ) and ρRρ′ , (the back condition for the MPB relation).

We write M ∼Sα M ′ if M, SM α ∼ M ′ , SM′

α . Following the definition of progression in [Liu and Wen, 2011], we have:

Definition 4.2 (Progression) Let DSα be a set of sentences uniform in Sα. DSα is a progression of DS0 wrt α if D |= DSα , and for every model M of (D-DS0 ) ∪DSα , there is a model M ′ of D s.t. M ∼Sα M ′ .

Then it is straightforward to prove:

Theorem 4.1 Let DSα be a progression of DS0 wrt α. Then for every φ uniform in Sα, D |= φ iff (D-DS0 ) ∪DSα |= φ. So for any query about Sα, the old theory D and the new

theory (D - DS0 ) ∪ DSα are equivalent.

We now introduce some notations used in the rest of this section. The APA for any action a is in the form of Poss(a, s) ≡ Πa[s], and the SSA for any ordinary fluent F is in the form of F(do(a, s)) ≡ ΦF (a)[s]. Let α be an action. We let Poss∗ (α) denote Πα, i.e., the situation-supressed formula of Πα[s]. We let Dss(α) denote the instantiation of Dss wrt α, i.e., the set of sentences F(do(α, s)) ≡ ΦF (α)[s]. We use D∗ ss (α) to denote the set of sentences F ′ ≡ ΦF (α), and PSS(α) to denote Poss∗ (α) ∧ D∗ ss (α). For a set A of actions, we write Poss∗ (A) .= ∨a∈A Poss∗ (a), and PSS(A) .= ∨a∈A PSS(a).

Definition 4.3 The comparability class of α in S0, denoted by [α], is the set {a | D |= A(a, α, S0) ∨ A(α, a, S0)}. We divide [α] into layers as follows:

Intuitively, [α]k is the k-th layer of [α], i.e., the set of actions of [α] with plausibility degree k, [α]<k is the set of actions of [α] with plausibility degree less than k, and pd(α) is the maximum plausibility degree of actions of [α]. For situations, we can define similar concepts.

Definition 4.4 Let M |= D and α an action possible in S0. We define [α]M as [α]k if M |= ˆK(Poss∗ ([α]k ), S0) ∧ K(¬Poss∗ ([α]<k ), S0).

Intuitively, [α]M is the innermost layer of [α] which contains an action the agent knows possibly executable. Since S0 is comparable to itself, M |= ˆK(Poss∗ ([α]), S0). So [α]M = [α]k for some k no more than the plausibility degree of α.

Finally, the world state of any situation can be represented by a minterm of ⃗ F, i.e., a conjunction of literals of ⃗ F where each proposition appears exactly once. We use mt( ⃗ F) to denote the set of minterms of ⃗ F. Let A be a set of actions. We use psK(A) and psB(A) to denote the following formulas, respectively:

Intuitively, psK(A) says that for any action a ∈ A, if the agent knows it is possible that the precondition of a holds, then she knows it is possible that the effect of a takes place in the same world state. The meaning of psB(A) is similar except that "knows" is replaced by "believes".

4.2 Combination formula

We now define the extended plausibility model for a model M of BAT wrt an action α.

Definition 4.5 Let M |= D - DS0 , and α an action possible in S0. The extended plausibility model of M wrt α, denoted by Wα = (S, ≤, V ), is as follows:

• S: the set of situations of M comparable to SM α ;
• ≤: the restriction of BM to S;
• V : the valuation on S. For each ordinary fluent F , action a, initial situation s, do(a, s) ∈ V (F) iff M |= F(s), and do(a, s) ∈ V (F ′ ) iff M |= F (do(a, s)).

We now analyze the formulas satisfied by the extended plausibility models of models of extended terms.

Lemma 4.1 Let φ = θ ∧ Kψ ∧ ∧i ˆKηi ∧ Bϕ ∧ ∧i ˆBξi be an extended term and α an action. Let M |= (D - DS0 ) ∪ {φ(S0), Poss(α, S0)}, and [α]k = [α]M. Then (Wα, SM α ) satisfies the following formulas:

Intuitively, the first formula says that the actual situation satisfies θ together with the precondition and effect of the actual action α. The second formula states the following. Firstly, the agent knows ψ and the disjunction of the preconditions and effects of alternatives to α. Secondly, for any alternative a to α, if the agent knows it is possible that the precondition of a holds, then she knows it is possible that the effect of a takes place in the same world state. Thirdly, for each initial possibility ηi, it remains a possibility if ψ ∧ ηi entails the disjunction of the preconditions of alternatives to α.

The third formula states the following. Firstly, the agent believes the disjunction of the preconditions and effects of actions in [α]k , and knows that no action with plausibility degree less than k is possible. Secondly, for any action a in [α]k , if the agent believes it possible that the precondition of a holds, then she believes it possible that the effect of a takes place in the same world state. Thirdly, for each initial belief possibility ξi such that ψ ∧ ϕ ∧ ξi entails the disjunction of preconditions of alternatives to α, if the agent does not believe ϕ or believes ¬ξi, then the agent knows it is possible that ϕ and ξi hold but no action in [α]k is possible. The reason is this. Since ψ ∧ ϕ ∧ ξi entails Poss∗([α]), there exists an alternative situation do(α′ , s′ ) to the situation do(α, s) such that s′ is a most plausible alternative to s and satisfies ψ ∧ ϕ ∧ ξi. If the agent does not believe ϕ or believes ¬ξi, then do(α′ , s′ ) cannot be a most plausible alternative to do(α, s), thus no action in [α]k is possible in s′ .

Based on the above formulas, we now define the combination formula of an extended term and an action.

Definition 4.6 Let φ = θ∧Kψ∧ ∧i ˆKηi∧Bϕ∧ ∧i ˆBξi be an extended term, and α an action. We call φ′ = φobj ∧ φK ∧ φB the combination formula of φ wrt α, where φB = ∨pd([α]) k=0 φkB .

Combination formulas have two important properties below:

Lemma 4.2 Let M |= D - DS0 . Then for any ψ ∈ L, M |= ψ[Sα] iff Wα, SM α |= ψ′ .

Lemma 4.3 Let DS0 be φ[S0] where φ is an extended term, α an action, and φ′ the combination formula of φ wrt α. Then for any model M ′ of D -DS0 such that its extended plausibility state W ′α, SM′ α |= φ′ , there exists a model M of D s.t. M ∼Sα M ′ .

Proof sketch: Suppose that M |= Poss(α, S0). Let W ′α = (S′ ,≤′ , V ′ ). We construct M as follows. M and M ′ have the same domains for actions. Firstly, all initial situations of M are S′ , and let S0 is S′M′ α . For situations of M, we use tM to denote the correspond world t′ of S′ . Similarly, for those of M ′ , we use tM′ to denote t′ . For any ordinary fluent, M |= F(tM ) iff t′ ∈ V (F). And BM (tM , uM ) iff t′ ≤′ u′ . Secondly, for every ηi, if ψ ∧ ηi ∧ ¬Poss∗ ([α]) is consistent, we add a ψ ∧ ηi ∧ ¬Poss∗ ([α])-situation into M, and let it be equally plausible to elements of [S0]1 . Thirdly, there are two cases. (1) W ′α, SM′ α |= ¬Bϕ. Then for all ξi, either ψ ∧ ϕ ∧ ξi ∧¬Poss∗ [α] is consistent, or there exists a world satisfying ψ∧ϕ∧ξi ∧¬Poss∗ ([α]k ). For the first case, we add a ψ∧ϕ∧ ξi∧¬Poss∗ ([α])-situation into M, and let it be more plausible than all situations in [S0]. For the second case, we let any ψ∧ϕ∧ξi ∧¬Poss∗ ([α]k )-situation be more plausible than all situations in [S0]. (2) W ′α, SM′ α |= Bϕ. Then for all ξi, either ψ∧ϕ∧ξi∧¬Poss∗ ([α]) is consistent, or if W ′α, SM′ α |= B¬ξi, then there exists a ψ ∧ ϕ ∧ ξi ∧ ¬Poss∗ ([α]k )-world. For the first case, we add a ψ∧ϕ∧ξi∧¬Poss∗ ([α]k )-situation into M, and let it be equally plausible to [S0]0 . For the second case, we let any ψ ∧ ϕ ∧ ξi ∧ ¬Poss∗ ([α]k )-situation be equally plausible to [S0]0 . Then we can show that M |= φ[S0].

We now construct a relation between the situations of M and those of M ′ as follows: R = {(do(a, tM ), do(a′ , uM′ )) | M |= K(do(a, tM ), SM α ),M ′ |=K(do(a′ , uM′ ), SM′ α ) and M, tM ≡ M ′ , uM′ }. Obviously (SM α , SM′ α ) ∈ R. We now prove R is a bisimulation between M and M ′ . Here we only prove the back condition for the K relation. Suppose that R(do(a, tM ), do(a′ , uM′)) and KM′((a′′ , vM′), do(a′ , uM′)). Since W ′α, SM′ α |= psK([α]), W ′α, do(a′′ , vM′ ) |= Poss∗ (a′′ ) and do(a′′ , vM′ ) ∼′ SM′ α , there exists a state w ∼′ SM′ α s.t. W ′α,w |= Poss∗ (a′′ ), and w and do(a′′ , vM′ ) agree on all propositions in ⃗ F . We can show that KM (do(a′′ , wM ), do(a, tM )) and R(do(a′′ , wM ), do(a′′ , vM′ )).

4.3 Representing progression

By Lemmas 4.1, 4.2 and 4.3, we have the following theorem which shows that for an extended term and an action, progression of knowledge and belief reduces to forgetting in the combination formula.

Theorem 4.2 Let DS0 be φ[S0] where φ is an extended term, α an action, and φ′ the combination formula of φ wrt α. Let kbforget(φ′ , ⃗ F) ≡ ψ. Then ψ[ ⃗ F ′/ ⃗ F][Sα] is a progression of DS0 wrt α.

Example 2 Continuing with Example 1, initially we have K(c ∧ h, S0), which we expand into an extended term φ = ⊤ ∧ K(c ∧ h) ∧ ˆK⊤ ∧ B⊤ ∧ ˆB⊤. We compute the combination formula of φ wrt αc as follows:

• PSS(αc) ≡ (c′ ↔ ¬c) ∧ (h′ ↔ h);
• PSS(αh) ≡ (c′ ↔ c) ∧ (h′ ↔ ¬h);
• φobj ≡ (c′ ↔ ¬c) ∧ (h′ ↔ h);
• φK ≡ K(c ∧ h ∧ (PSS(αc) ∨ PSS(αh))∧ [ ˆK(c ∧ h) ⊃ ˆK(c ∧ h ∧ PSS(αc))]∧ [ ˆK(c ∧ h) ⊃ ˆK(c ∧ h ∧ PSS(αh))] ∧ ˆK⊤ ≡ K(c∧h∧(¬c′∧h′ ∨c′∧¬h′ ))∧ ˆK(¬c′∧h′ )∧ ˆK(c′∧¬h′ );
• Since Poss∗ (αc) ≡ ⊤, φ1B ≡ ⊥ and φ0B
• ≡ B(PSS(αh))∧K⊤∧[ˆB(c∧h) ⊃ ˆB(c∧h∧PSS(αh))]∧ [¬B⊤ ∨ B⊥ ⊃ ˆK(⊤ ∧ ⊤ ∧ ⊥)]

≡B[(c′ ↔c)∧(h′ ↔¬h)]∧[ ˆB(c∧h) ⊃ ˆB(c∧h∧c′ ∧¬h′ )].

So the combination formula φ′ = φobj ∧ φK ∧ φ0B ≡ ¬c′ ∧ h′ ∧ K(c ∧ h ∧ (c′ ∧ ¬h′ ∨ ¬c′ ∧ h′ )) ∧ B(c′ ∧ ¬h′ ). Forgetting c and h from the above formula, we get: ¬c′ ∧ h′ ∧K(c′ ∧¬h′ ∨¬c′ ∧ h′ ) ∧B(c′ ∧¬h′ ), since

• forget(c ∧ h ∧ ¬c′ ∧ h′ , {c, h}) ≡ ¬c′ ∧ h′ ;
• forget(c ∧ h ∧ (c′ ∧¬h′ ∨¬c′ ∧ h′ ), {c, h}) ≡ c′ ∧ ¬h′ ∨ ¬c′ ∧ h′ ;
• forget(c ∧ h ∧ c′ ∧¬h′ , {c, h}) ≡ c′ ∧¬h′ .

Thus (¬c ∧h∧K(c ∧¬h∨¬c ∧h) ∧B(c ∧¬h))[Sαc ] is a progression of DS0 wrt αc. It says: the computer is off but the heater is on, Alice knows that only one of them is on, and she believes that the computer is on but the heater is off.

Since every formula in LKB can be equivalently transformed to a disjunction of extended terms, by Theorem 4.2, we get the main result of this paper:

Corollary 4.1 In the single-agent propositional case, progression of knowledge and belief for propositional actions is always definable in LKB and computable.

We remark that, in the single-agent propositional case, this result is more general than the one obtained by Liu and Wen [2011] . Firstly, they considered knowledge but did not consider belief. Secondly, they only handled deterministic actions. Thirdly, for sensing actions, they required that the initial KB should not contain negative knowledge.

Finally, we analyze the size of progression. By the size of an action α, we mean the size of the formula PSS([α]).

Theorem 4.3 Let α be an action. Then there exists a progression wrt α with size at most 223n+3 4l+4m2 , where l is the size of DS0 , m is the size of α, and n is the number of fluents.

Proof: Firstly, let φ be an extended term of size p, we estimate the size of the progression of φ. Let φ′ be the combination formula. The size of φ′ is ≤ 2n+16nm + 2n+2m+ 2p2m+ 6pm+m2 ≤ 23np2m2 . Converting φ′ into a disjunction of extended terms, we get a formula of size ≤ 223n p2m2+4 . Then forget all propositions from ⃗ F; the result has size ≤ 223n+2 p2m2 . We can convert DS0 into a disjunction of extended terms, whose size is ≤ 2l+4 . So there exists a progression of DS0 whose size is ≤ 223n+3 4l+4m2 .

Thus the size of progression is double exponential in the size of the initial formula and the number of fluents but single exponential in the size of the action.

5 Some special cases

In general, the combination formula is too complicated. In this section, we consider computing progression for some simple cases including epistemic actions and deterministic actions. For these cases, we can implement progression via some techniques of knowledge compilation, e.g., BDDs, to maintain the size of progressed KBs to a reasonable level.

5.1 Epistemic actions

Definition 5.1 An action α is an epistemic action possible in S0, if for every ordinary fluent F and action a ∈ [α], we have Dss(a) |= F(do(a, s)) ≡ F(s) .

Intuitively, α is an epistemic action if all alternatives to α in S0 do not affect the world. The form of progression for epistemic actions is simpler than in the general case.

Theorem 5.1 Let DS0 be φ[S0] where φ = θ∧Kψ∧∧i ˆKηi∧ Bϕ ∧ ∧i ˆBξi is an extended term, and α an epistemic action possible in S0. Let φ′ = φobj ∧ φK ∧ φB , where φB = ∨pd([α]) k=0 φkB , and

1. φobj =θ ∧ Poss∗ (α);

Then φ′ [Sα] is a progression of DS0 wrt α.

Epistemic actions do not change the world state. So two formulas psK(A) and psB(A) and the instantiations of Dss for epistemic actions are superfluous. Hence, we have: for epistemic actions, the size of progression is one exponential lower than in the general case:

Theorem 5.2 Let α be an epistemic action. Then there exists a progression wrt α with size at most 4l+4m2 , where l is the size of DS0 and m is the size of α.

Example 3 Continuing with Example 2, we have DSαc ≡ φ[Sαc ] where φ = ¬c ∧ h ∧K(c ∧ ¬h ∨ ¬c ∧ h) ∧ ˆK⊤∧ B(c ∧ ¬h) ∧ ˆB⊤. The progression of φ wrt oh is as follows:

• φobj ≡ ¬c ∧ h ∧ h ≡ ¬c ∧ h;

Thus DSoh = (¬c∧h∧K(c∧¬h∨¬c∧h)∧Bh∧ ˆK¬h)[Soh ] is a progression of DSαc wrt oh. It says: neither the objective world nor Alice's knowledge changes, but Alice changes her beliefs, and believes that the heater is on. Moreover, Alice knows it is possible that the heater is off.

5.2 Deterministic actions

Definition 5.2 An action α is deterministic in S0 if [α] = {α}.

It says α is a deterministic action, if the comparability class of α is a singleton.

Theorem 5.3 Let DS0 be φ[S0] where φ = θ∧Kψ∧∧i ˆKηi∧ Bϕ∧∧i ˆBξi is an extended term, and α a deterministic action possible in S0. Let φ′ = kbforget(φobj,K ∧ φB, ⃗ F), where

• φobj,K = θ ∧ K(ψ ∧ PSS(α)) ∧ ∧ψ∧ηi|=Poss∗ (α) ˆKηi;

Then φ′ [ ⃗ F ′/ ⃗ F][Sα] is a progression of DS0 wrt α.

The above formula φ′ states the following. Firstly, θ still holds, and the agent remains her knowledge of ψ and gets to know the precondition and effect of α. Secondly, the agent keeps considering ηi possible if ψ ∧ ηi |= Poss∗ (α). Thirdly, when φ entails that the agent believes the precondition of α possible, the agent keeps believing ϕ and keeps believing ξi possible if ψ∧ϕ∧ ξi |= Poss∗ (α). The third part is because: under the restriction, the most plausible alternatives to Sα are do(α, s′ ) where s′ is a most plausible alternative to S0 such that s′ satisfies the precondition of α.

This theorem shows that extended terms are closed under progression wrt deterministic actions. As a corollary of this theorem, we have: for deterministic actions, the size of progression is one exponential lower than in the general case:

Theorem 5.4 Let α be a deterministic action. Then there exists a progression wrt α with size at most 4l+42nm2 , where l is the size of DS0 , m is the size of α, and n is the number of fluents.

An action which accurately observes that γ holds, written oγ, is a deterministic epistemic action where Poss(oγ, s) ≡ γ(s). Since epistemic actions do not change the world state, as an immediate corollary of Theorem 5.3, we have:

Corollary 5.1 Let DS0 be φ[S0] where φ = θ∧Kψ∧∧i ˆKηi∧ Bϕ ∧ ∧i ˆBξi is an extended term, and oγ be an accurate observation action possible in S0. Let φ′ = φobj,K ∧ φB, where

• φobj,K = θ ∧ K(ψ ∧ γ) ∧ ∧ψ∧ηi|=γ ˆKηi;

Then φ′ [Soγ ] is a progression of DS0 wrt oγ.

Example 4 Reconsider the example from the introduction. Assume that the observation action is accurate. The axioms are the same as those in Example 1, except for the A axiom:

As depicted in Figure 2, now the situations Soh and S′o¬h are not comparable since oh and o¬h are not comparable. From Example 2, we have DSαc ≡ φ[Sαc ] where φ = ¬c ∧ h ∧ K(c ∧ ¬h ∨ ¬c ∧ h) ∧ ˆK⊤ ∧ B(c ∧ ¬h) ∧ ˆB⊤. By Corollary 5.1, since φ ̸|= ˆBh, the following is a progression of DSαc wrt oh:

which is equivalent to K(¬c∧h, Soh ). Compared to Example 3, Alice not only believes that the heater is on, but also gets to know the truth.

6 Conclusions

In this paper, we have studied progression of knowledge and belief wrt nondeterministic actions in the single-agent propositional case. We gave a model-theoretic definition of progression of knowledge and belief. We studied forgetting in the logic of knowledge and belief, and showed that it is closed under forgetting. We constructed the combination formula which combines the information of an extended term and an action. We showed that for propositional actions, both physical and epistemic, progression of knowledge and belief reduces to forgetting in the combination formula, and hence is always definable in the logic of knowledge and belief. In general, progression might cause a double exponential blowup in the size of the formula. We showed that for the special cases of epistemic actions and deterministic actions, the blowup is only single exponential. For these cases, we can acquire practical solutions to progression via techniques of knowledge compilation, e.g., BDDs, SDDs [Darwiche, 2011], and minimal-DNFs [To et al., 2009]. We have used the results of progression for deterministic actions in implementing an epistemic planner [Wan et al., 2015]. All results in this paper can carry over to the single-agent propositional fragments of several extensions to the situation calculus, e.g., [Shapiro et al., 2011] and [Liu and Wen, 2011].

For the future, we would like to identify fragments and explore sound but incomplete progression to prevent the double exponential blowup. Then, we will apply practical forms of progression in doxastic planning and high-level program execution for belief-based programs. We would also like to investigate progression for non-propositional actions and the multi-agent case.

Acknowledgments

Yongmei Liu is also affiliated to the Guangdong Key Laboratory of Information Security Technology, Sun Yat-sen University, China. We thank the anonymous reviewers for helpful comments. This work received support from the Natural Science Foundation of China under Grant Nos. 61073053 and 61463044.