Revising Beliefs and Intentions in Stochastic Environments

1 Introduction

Autonomous agents operating in dynamic environments need a method for keeping track of their beliefs, updating these as new information is received. But an agent also carries intentions they are committed to bring about, and these also need to be updated on the basis of new information or deliberation. While there is an enormous amount of literature on the former topic of belief revision, the topic of intention revision received, in comparison, less attention [Cohen and Levesque, 1990; Wooldridge, 2000; van der Hoek et al., 2007; Castelfranchi and Paglieri, 2007; Lorini and Herzig, 2008; Shoham, 2009; Grant et al., 2010; Icard et al., 2010; van Ditmarsch et al., 2011; Shapiro et al., 2012; van Zee and Doder, 2016; van Zee et al., 2020].

As observed by many of the aforementioned authors, intention and beliefs are deeply intertwined, and their revisions need to be studied together. For instance, for an agent to be able to intend something, it does not suffice if it is merely the case that their beliefs and the intention are separately consistent on their own: they need to cohere together, in the sense that the agent's beliefs should be consistent with the achievement of the intention [van Zee et al., 2020].

In prior work on intention revision, such interactions between belief and intention have only been studied for agents acting in deterministic environments. But for many practical applications, agents act in stochastic environments, where their actions have uncertain outcomes.

In this paper, we present the first framework for the joint revision of beliefs and intentions in stochastic environments.

We define beliefs and intentions in a decidable probabilistic temporal logic interpreted on Markov Decision Processes (MDPs), giving the ability to express beliefs about the uncertainty in actions' outcomes, as well as complex temporal intentions. We propose a set of rationality postulates for revision operators in this logic. Using these rationality postulates, we also obtain semantic understanding of revision through Katsuno & Mendelzon-style representation theorems [Katsuno and Mendelzon, 1991].

Working with stochastic environments and highly expressive beliefs and intentions about probability and time brings new challenges compared to prior work in the field, both technical and conceptual. In terms of technical challenges, giving a representation theorem is complicated by the fact that in general, there are infinitely many MDPs satisfying certain beliefs, due to the presence of probability, and that we have no general guarantees on the expressibility of sets of MDPs. These features are vital to the original theorems of [Katsuno and Mendelzon, 1991]. To overcome this challenge, we employ results and methods from [Falakh et al., 2023] to still obtain representation theorems. But to make our work more practically applicable, we go further by defining two novel postulates which additionally provide representation theorems for a specific class of operators that are conceptually simple and generally computable, properties which are not guaranteed by the results of [Falakh et al., 2023].

In terms of conceptual challenges, stochastic environments also require more nuanced approaches to the interplay between beliefs and intentions than is considered in prior work. Let us illustrate this with the following example (which we will frequently revisit throughout this paper).

Consider an agent named Theo, who intends to attend an obscure, underground concert tomorrow. He only has $5, and admission costs precisely $5. He believes that if he goes to the ticket office today, he can almost certainly buy a ticket since no one knows the band and they are therefore unlikely to be sold out. Theo is also aware that the concert venue sometimes sends out free tickets for concerts in the mail, as a promotion. So Theo also believes that if he stays at home, he may receive tickets, albeit with a small probability.

Now, for simplicity assume that Theo's favorite brand of beer costs $5, both at shops and at the concert venue. How would Theo revise his intentions with the new intention to also buy a drink tomorrow? His beliefs do in one sense support the possibility of achieving both intentions, since he could luck out and get free tickets, attend the concert, and buy the drink there. So perhaps the revision should just be adding the new intention on top of his original one. But should rational agents make decisions based on unlikely outcomes? It would be more reasonable to say that an agent's intentions are coherent only if they can achieve them with reasonably high probability, with the definition of being 'reasonably high' as a choice to be made. So it may be more reasonable that when revising with this new intention, Theo drops his old intention of attending the concert.

To see how the nuance of probabilities also influences the interplay between beliefs and intentions, note that accepting intentions should revise the agent's beliefs: if he intends to attend the concert, Theo should also believe he no longer has $5 after the concert, as the only way to be reasonably sure about his attendance is to spend it on tickets.

Similarly, revising beliefs should also be able to trigger intention revision. Say Theo gets a call from his friend Stan, who tells him that the band, which Theo thought to be obscure, has suddenly become an international sensation overnight. Theo revises his beliefs about him being able to buy tickets at the ticket office, as they are now highly likely to be sold out. And since it so unlikely to get tickets, no matter what he does, it may be reasonable to drop his intention of attending the concert.

2 PLBP+

An agent's beliefs and intentions naturally concern themselves with probability ("I believe speeding is likely to be dangerous") and time ("I intend to apply for jobs until I succeed"). Therefore we choose to express beliefs and intentions in an appropriate probabilistic temporal logic. We choose to work with an extended version of the Probabilistic Logic of Bounded Policies (PLBP), introduced by [Motamed et al., 2023]. We refer to this extension as PLBP+. We now explain the syntax and semantics of the logic.

We fix a countably infinite set Prop of propositional variables and a finite set A of actions throughout the paper. To each action a ∈ A we associate a precondition prea, which is a conjunction of literals over Prop, and a finite nonempty list Posta of possible postconditions, which are also conjunctions of literals. Intuitively, the precondition of an action is precisely what must be satisfied so that the action can be executed, and a postcondition of an action is one of its possible outcomes, i.e. that which is made true after executing the action. We refer to the ith postcondition of a as posta,i.

Before we can define the stochastic environments that serve as models of the logic, some notation is required. We write f : X ⇀ Y to denote that f is a partial function fromX to Y , and write f(x)↓ to denote that f is defined on input x ∈ X. Given a set X, some x ∈ X and n ⩾ 0, we write Xn x for the set of all sequences in X of length n starting with x (i.e. with X0 x = ∅ and X1 x = {x}), and we write X⩽n x = ⋃nk=0 Xk x . Finally, we write ∆(X) for the set of all finitely supported (discrete) probability distributions on X, i.e. those probability distributions D : X → [0, 1] such that D(x) > 0 for only finitely many x.

Definition 1 (MDP). A Markov decision process (MDP) over A is a tuple M = (S, P, V ), where S is the set of states, P : S×A ⇀∆(S) is the partial probabilistic transition function, and V : S → 2Prop is the valuation. We often abbreviate P(s, a) by Ps,a. These are required to satisfy the following conditions. First, for all s ∈ S, there is some a ∈ A such that s ⊩ prea, where ⊩ here is the standard propositional satisfaction relation. Second, Ps,a↓ iff s ⊩ prea. And third, given Ps,a↓, we have that (i) for all t ∈ S such that Ps,a(t) > 0, there is a unique posta,i in Posta such that t ⊩ posta,i, and (ii) for all posta,i in Posta there is at most one t such that Ps,a(t) > 0 and t ⊩ posta,i.

A pointed MDP (pMDP) is a pair P = (M, s) where M is an MDP, and s is a state in M. We denote the set of all pMDPs P by pMDP.

A key feature of PLBP+ is the ability to reason about n-step policies, which specify how the agent will act for n time steps.

Definition 2 (n-step policies). Given a pMDP P = (M, s) and n ⩾ 0, an n-step P-policy is a function π: S⩽n s → A such that sk ⊩ preπ(s1···sk) for all s1 · · · sk ∈ S⩽n s .

Given n-step π with n ⩾ 1 and t ∈ S, define the pushforward of π to t to be the (n-1)-step (M, t)-policy πt given by putting πt(t) = π(st).

We will drop P when the pMDP is clear from context, speaking just of n-step policies. Or conversely, when the n is not relevant within some context, we just speak of P-policies.

Definition 3 (Paths and path distributions). For an n-step policy π, we define Paths(π) as the set of all paths s0 · · · sn ∈ Sn+1 such that s0 = s, and P(sk, π(s0 · · · sk))(sk+1) > 0 for all 0 ⩽ k < n.

Given an n-step policy π, its path distribution is the probability distribution µπ ∈ ∆(Paths(π)) defined as µπ(s0 · · · sn) = ∏0⩽k<n P(sk, π(s0 · · · sk))(sk+1). This extends to sets of paths in the standard way, i.e. µπ(X) = ∑w∈X µπ(w).

Definition 4 (Syntax). The syntax of PLBP+ is inductively defined by the following grammar:

where p ∈ Prop, n ⩾ 0, a ∈ A , r ∈ Q ∩ [0, 1], and ▷◁ ∈ {⩾ , ⩽}. Formulas φ are referred to as state formulas, formulas α are referred to as policy formulas, and formulas Φ are referred to as path formulas.

State formulas are interpreted over states, policy formulas over policies, and path formulas over policies and paths. The state formula ♢nα should be read as "there exists an n-step policy for which α holds". The policy formula doa is read as "the current policy chooses action a now", and Pr▷◁rΦ as "under the current policy, Φ holds with probability ▷◁ r". The path formula XΦ is read as "at the next time on this path and policy, Φ holds". Note that [Motamed et al., 2023] introduce syntactic restrictions in formulas so that the amount of nested X-operators never exceeds the length of a path on which it is interpreted. We allow arbitrary path formulas to be interpreted over arbitrary paths, closer to how logics such as LTLf approach temporal logic over finite traces [De Giacomo and Vardi, 2013].

Definition 5 (Semantics). Given an MDP M, the semantics of PLBP+ is defined via simultaneous induction over state, policy and path formulas. We omit the semantics of Boolean operators as it is standard. For state formulas, it is defined for states s as

• M, s ⊩ p iff p ∈ V (s),
• M, s ⊩ ♢nα iff there exists an n-step (M, s)-policy π such that M, π ⊩ α.

For policy formulas, it is defined for an (M, s)-policy π as

• M, π ⊩ doa iff π(s) = a,
• M, π ⊩ Pr▷◁rΦ iff µπ({w ∈ Paths(π) | M, π,w ⊩ Φ}) ▷◁ r.

For path formulas, it is defined for policies π and paths w = s0 · · · sn ∈ Paths(π) as

• M, π, w ⊩ φ iff M, s0 ⊩ φ,
• M, π, w ⊩ α iff M, π ⊩ α,

· M, π, w ⊩ XΦ iff n ⩾ 1 and M, πs1 , s1 · · · sn ⊩ Φ. For a state formula φ, we write �φ� := {P ∈ pMDP | P ⊩ φ}. We say φ ⊩ ψ if �φ� ⊆ �ψ�, and φ ≡ ψ if �φ� = �ψ�. For a path formula Φ, we write [Φ] for the set of all triples (M, π, w) consisting of an MDP M, a (M, s)-policy for some state s, and a path w ∈ Paths(π) such that M, π, w ⊩ Φ. Given a (M, s)- policy π, we write [Φ]π := {w ∈ Paths(π) | M, π, w ⊩ Φ}. We say Φ ⊨ Ψ if [Φ] ⊆ [Ψ], and Φ ∼= Ψ if [Φ] = [Ψ].

As is usual, we define the other Boolean connectives ∨ and → as abbreviations, as well as the propositional constants ⊤ and ⊥ for verity and falsity. Similarly, we can also define a universally quantified version of the ♢n -modality by putting □n := ¬♢n¬. And we define Pr▷◁rΦ for symbols ▷◁ ∈ {=, ̸= , >, <} by appropriate abbreviations, e.g. Pr>rΦ := ¬Pr⩽rΦ. Note that we can also define more complicated (bounded) temporal operators, such as the bounded until Φ Un Ψ := ∨0⩽k⩽n (XkΨ ∧ ∧0⩽ℓ<k XℓΦ), where Xk is an abbreviation for X k-many times. And finally, observe that we may also define a general ♢-modality with the semantics of there being an n-step policy for some n. This is done by observing that for each α there is a number td(α) (the temporal depth of α) such that if there is an n-step policy for which α holds, then there is an n-step policy with n ⩽ td(α) for which α holds. This td(α) is intuitively the amount of nested X-operators and doa-propositions appearing in α. We can then define ♢α := ∨0⩽n⩽td(α) ♢nα.

Satisfiability and therefore entailment for PLBP+ state formulas is decidable, placing the problem in the class 2EXPSPACE of problems decidable with a deterministic algorithm using space double exponential w.r.t. the input.

Theorem 1 (Satisfiability of PLBP+). The satisfiability problem for PLBP+ state formulas (i.e. given a state formula φ, decide whether �φ� ̸= ∅) lies in 2EXPSPACE.

Proof sketch. The proof is an easy adaptation of the proof for PLBP. Using the unravelling method of modal logic, we observe that PLBP+ possesses the finite model property, with satisfiable formulas having models of of size up to a bound calculatable from the formula. We iterate over sets S of size up to this bound. We then define a first-order logic formula α over the signature of real-closed field (RCF; see [Chang and Keisler, 2012] for a definition), such that α is valid in RCF iff there exists a valuation and probabilistic transition function over S such that the resulting pMDP satisfies φ. Since α is of double exponential size w.r.t. φ, and is in existential prenex form, it follows from existential RCF being decidable in polynomial space [Canny, 1988] that the overall procedure runs in double exponential space.

Having discussed the logic we base our work on, we can now introduce how we define beliefs and intentions. We identify beliefs with state formulas: the agent's beliefs are about what the environment (pMDP) looks like, independent of how the agent chooses to act. As an example, the formula □1 (doa → Pr=.5Xposta,i) expresses the belief that after executing a now, we get the ith postcondition of a afterwards with probability 50%. Similarly, we identify intentions with path formulas: the agent intends to bring about certain outcomes (paths) throughout time, as in e.g.[Rao and Georgeff, 1991; Khan and Lesp´erance, 2012; Leask, 2021]. As an example, the formula doa Un Pr>rΦ expresses the intention to keep executing a until a point from which Φ will hold with probability > r, for a maximum of n steps. Note that this gives us a very rich notion of intention, going far beyond the atomic action intentions ("I intend to perform a at time t") of [Shoham, 2009; van Zee et al., 2020].

Example 1 (Running example). Coming back to our example from Section 1 about Theo and the concert, we can rewrite the beliefs and intentions therein as PLBP+ formulas (fixing some probabilities for the terms 'likely' and 'unlikely'). The relevant propositional variables are Prop = {five, conc}, with the former denoting Theo having $5, and the latter denoting Theo being at the concert. The example concerns the actions stay of staying at home, goTick of going to the ticket office to buy a ticket, and buyDr of buying his favorite drink. The relevant preconditions are pregoTick = five (it costs $5 to buy tickets), and prebuyDr = five (Theo needs to have $5 to buy drinks). The relevant postconditions are PostgoTick = {conc ∧ ¬five, ¬conc ∧ five} (Theo either gets to attend and spends $5, or he doesn't and keeps it), Poststay = {conc ∧ five, ¬conc ∧ five} (whether he gets a ticket or not, he keeps his money), and PostbuyDr = {¬five} (buying a drink is deterministic: Theo pays $5). His original beliefs are modelled by the state formula φ1 = five∧□((dogoTick ∨dostay)∧dogoTick → Pr⩾.9Xconc∧ dostay → Pr⩽.01Xconc), i.e. Theo has $5, can try to buy a ticket or stay at home, and with probability at least 90% the former gets him to the concert, while at most 1% the latter does. The intentions of attending the concert and buying drinks are respectively Φ1 = Xconc and Φ2 = XdobuyDr. The statement that the band has become popular (i.e. tickets are likely to be sold out) is φ2 = □(dogoTick → Pr⩽0.01Xconc) (there's only a 1% chance Theo gets to buy tickets).

3 Coherence and Beliefs

In this section, we introduce our proposal for defining the 'coherence' of beliefs and intentions, as well as what it means to believe something on the basis of certain intentions.

As mentioned in Section 1, it is not sufficient that an agent's beliefs and intentions are separately consistent: we need joint consistency. This joint consistency between beliefs and intentions is what has been referred to as coherence by [van Zee et al., 2020]. What we want, is a requirement on beliefs and intentions, stating that the agent's beliefs should somehow be consistent with the possible achievement of their intentions. Note that this is effectively the Strong Consistency Principle proposed by [Bratman, 1987] in his influential theory of intentions.

Coherence is defined in prior work as stating that there exists some model of the agent's beliefs, in which the agent has a policy which achieves the intention. Translating this definition to our setting, we are asking given a belief φ and an intention Φ, whether there exists some P ∈ �φ�, and a P-policy π, such that π 'achieves' Φ. What does it mean that π 'achieves' Φ? Contrary to the prior work, in our setting actions have uncertain outcomes: some of the paths produced by π may satisfy Φ, while others do not. It is sensible to define the notion of achievement with regards to the probability with which these paths satisfy Φ, i.e. µπ([Φ]π).

We therefore propose to take a parametric, applicationdependent approach to coherence, in which we take some value 0 ⩽ θ < 1 with the intuition being that the agent only considers policies that achieve intentions with probability greater than θ. The value of θ will depend on the specific problem domain or type of agent we are considering at the time.

Definition 6 (θ-coherence). Let 0 ⩽ θ < 1 be a rational number. A state formula φ and path formula Φ are θ-coherent if there exists a pMDP P ∈ �φ� and a P-policy π such that µπ([Φ]π) > θ.

Note that this definition is equivalent to stating that the formula φ ∧ ♢Pr>θΦ is satisfiable. Therefore, by Theorem 1 we get that it is actually decidable whether beliefs and intentions are θ-coherent.

Example 2 (Running example, continued). Our discussion in Section 1 effectively observed that Theo's strong beliefs φ1 and intentions Φ1 ∧ Φ2 are 0-coherent (where Φ1 = Xconc and Φ2 = XdobuyDr), due the possibility of choosing the action stay. But note that this combined intention is not e.g. 0.05coherent with φ1, since in any model of φ1, any policy will assign at most probability 0.01 to Φ1 ∧ Φ2. We do have that Φ1 alone is 0.05-coherent with φ1 - the same holds for Φ2.

While beliefs as we have discussed them so far have been about what the environment looks like, independent of how the agent actually chooses to act, an essential part of a theory of belief and intention is that since an agent is committed to performing intentions, they actually in some sense 'believe' that the outcomes of those intentions will hold. To model this, [van der Hoek et al., 2007] propose to separate so-called strong beliefs from weak beliefs. The former are what we have considered so far: independent of how the agent actually acts. The latter are believed on the assumption the agent performs their intentions. The separation prevents scenarios like the Little Nell Problem [McDermott, 1982].

Since weak beliefs are contingent on the performance of intentions, we propose to consider these to be path formulas as well: we weakly believe certain properties (like outcomes of intended actions) will hold throughout time. This is similar to the approach to weak beliefs of [van Zee et al., 2020]. Trying to use their approach naively, we could choose to define the weak beliefs obtained from our beliefs φ and intentions Φ to be those path formulas Ψ such that for all P ∈ �φ� and Ppolicies π, we have for all w ∈ Paths(π) that if M, π, w ⊩ Φ, then also M, π, w ⊩ Ψ.

But this approach is problematic, as our running example of Theo and the concert shows. By our naive definition of weak beliefs, Theo will not weakly believe that he will have $0 tomorrow, because of the existence of the policy in which he stays at home today. One could certainly argue that it is more practical and rational that Theo should in fact believe that, assuming he manages to attend the concert, he will be out of money. The problem here, as with coherence, is that the policy of staying at home achieves the intention with too low a probability. Therefore, we also parameterize the definition of weak beliefs by the same θ stating when a policy should be considered as 'achieving' an intention, removing from consideration policies which only achieve the intention by sheer luck.

Definition 7 (θ-weak beliefs). Let 0 ⩽ θ < 1 be a rational number. Given a state formula φ and path formula Φ, the set WBθ(φ, Φ) of θ-weak beliefs of φ and Φ is defined as the set of all path formulas Ψ such that for all P ∈ �φ� and P-policies π such that µπ([Φ]π) > θ, it holds for all w ∈ Paths(π) that if M, π,w ⊩ Φ, thenM, π,w ⊩ Ψ.

Note that Ψ ∈ WBθ(φ, Φ) if and only if φ∧Pr>θΦ∧Φ ⊨ Ψ, which is again if and only if φ ⊩ □(Pr>θΦ → Pr=1(Φ → Ψ)). By Theorem 1, we can therefore decide whether a given formula Ψ is in WBθ(φ, Φ).

Example 3 (Running example, continued). We have that indeed X¬five ̸∈ WB0(φ1,Φ1), while X¬five ∈ WB0.05(φ1, Φ1) and XX¬five ∈ WB0.05(φ1, Φ2): Theo 0.05weakly believes he will not have his money tomorrow if he intends to attend the concert tomorrow. And he also 0.05weakly believes he will not have his money the day after tomorrow if he intends to buy a drink tomorrow.

We see directly from the definitions that the satisfiability of weak beliefs is equivalent to the coherence of the corresponding strong beliefs and intentions.

4 Representation for Revision Operators

We now move our attention to the revision of beliefs and intentions. Similar to prior work [van Zee et al., 2020], we follow the approach of revising an agent's strong beliefs φ and intentions Φ with new strong beliefs ψ and intentions Ψ, by first revising the strong beliefs independently of the intentions, and afterwards revising the intentions in a way that takes the revised strong beliefs into account. We explore this joint revision in Section 4.3.

We will start by discussing belief revision operators, and providing a representation theorem for them. By virtue of our setup, we will afterwards see that almost all of the machinery we develop here will also apply to intention revision operators. We conclude this section by discussing what our setup tells us about the interplay between belief and intention.

Throughout this section, we write Bel for the set of state formulas, and Int for the set of path formulas.

4.1 Belief Revision

Definition 8 (Belief revision operator). A belief revision operator is a function ◦ : Bel × Bel → Bel, with φ ◦ ψ being read as the result of revising φ by ψ.

Conceptually, we wish for belief revision operators to satisfy the intuition that they are revising φ by ψ by 'minimally' changing φ until ψ can be added without problems. But the original approach of [Katsuno and Mendelzon, 1991] with finite-signature propositional logic does not apply to our setting: there are infinitely many pMDPs due to e.g. the presence of probability in our models, and generally speaking, there exists no formula φ that expresses even a single pMDP P (i.e. such that �φ� = {P}), since we could always consider pMDPs which differ from P only at times which are 'outside the scope' of φ. Luckily, the approach of [Falakh et al., 2023] still allows us to obtain a representation theorem by adding some requirements on the semantic side, which they refer to a min-completeness and min-expressibility.

First some preliminaries on orders are required. A relation ⪯ ⊆X ×X is a total preorder if it is reflexive, transitive and connected (i.e. x ⪯ y or y ⪯ x for all x, y ∈ X). We write x ≺ y iff x ⪯ y and y ⪯̸ x. We say x ∈ U ⊆ X is ⪯-minimal in U if x ⪯ y for all y ∈ U, and write min(U, ⪯) for the set of all such ⪯-minimal elements in U.

Definition 9 (pMDP assignments). A pMDP assignment is a function ⪯(-) : Bel → 2pMDP×pMDP such that ⪯φ is a total preorder for all φ. The assignment is faithful if the following three conditions hold: (i) If P ⊩ φ and P′ ⊩ φ, then P ⪯φ P′ and P′ ⪯φ P. (ii) If P ⊩ φ and P′ ⊮ φ, then P ≺φ P′ . (iii) If φ ≡ ψ, then ⪯φ = ⪯ψ. The assignment is min-complete if min(�ψ�,⪯φ) ̸= ∅ for all φ and ψ with �ψ� ̸= ∅. It is min-expressible if for all φ and ψ there exists ψ⪯,φ ∈ Bel such that �ψ⪯,φ� = min(�ψ�, ⪯φ).

The rationality postulates used by [Falakh et al., 2023] are precisely those of [Katsuno and Mendelzon, 1991], and are equivalent to the original presentation of the AGM postulates by [Alchourr´on et al., 1985]. Though Katsuno & Mendelzon's work was concerned with finite-signature propositional logic, we emphasize that the rationality postulates are applicable in much more general settings: citing [Segerberg, 1999], "AGM is not really logic; it is a theory about theories".

The postulates are as follows.

• (B1) φ ◦ ψ ⊩ ψ.
• (B2) If φ∧ψ is satisfiable, then φ ◦ ψ ≡ φ∧ψ.
• (B3) If ψ is satisfiable, then φ ◦ ψ is satisfiable.
• (B4) If φ1 ≡ φ2 and ψ1 ≡ ψ2, then φ1 ◦ ψ1 ≡ φ2 ◦ ψ2.
• (B5) (φ ◦ ψ) ∧χ ⊩ φ ◦ (ψ ∧χ).
• (B6) If (φ◦ψ)∧χ is satisfiable, then it holds that φ◦(ψ∧χ) ⊩ (φ ◦ ψ) ∧ χ.

The postulate (B1) expresses the success of revision: the new information must be incorporated by the revision. The postulate (B2) expresses that when the new information is consistent with our beliefs, revision should be the same as just adding the new information. The postulate (B3) expresses that we maintain consistency whenever we add consistent information to our beliefs, and the postulate (B4) expresses that revision should not care about syntax. Finally, the postulates (B5) and (B6) ensure that revision can be thought of as based on a notion of minimal change, with the outcome of revision φ ◦ ψ giving those models of ψ that are 'closest' to models of φ. Given such a interpretation, we would naturally have that a model of ψ which is closest to φ and satisfies χ is automatically also the model of ψ ∧ χ closest to φ, which is exactly what (B5) states. And similarly, we would never have that there exist models M,N ∈ �ψ ∧ χ� such that M is closest to φ amongst �ψ ∧ χ� but N is strictly closer to φ than M amongst �ψ�, which is exactly what (B6) rules out.

Example 4 (Running example, continued). Consider Theo's original strong beliefs φ1 and the new piece of information φ2 = □(dogoTick → Pr⩽0.01Xconc) (which he gains by learning the band is actually popular). Then the postulates tell us already several things about how the revision φ1 ◦φ2 will look, for any belief revision operator ◦ satisfying them. For example, (B3) tells us that φ1 ◦ φ2 must be satisfiable, since φ2 clearly is. We get that φ1 ◦φ2 cannot be equivalent to φ1 ∧φ2, as that formula is not satisfiable: Theo has to drop some beliefs. But whatever he drops, (B1) tells us that φ1 ◦ φ2 ⊩ φ2: he comes to believe that if he goes to the ticket office, the probability that tickets are available is at most 1%.

The following general representation result, Theorem 2, expresses that belief revision minimally changes beliefs to accommodate new information.

Theorem 2 (General representation for PLBP+). The following statements hold:

• For every min-complete, min-expressible and faithful pMDP assignment ⪯(-) there exists a belief revision operator ◦ satisfying (B1)-(B6) such that �φ ◦ ψ� = min(�ψ�, ⪯φ).

Proof. This follows from the results of [Falakh et al., 2023], as we now explain. Consider PLBP+ state formulas as what they refer to as a base logic: PLBP+ state formulas are the sentences, pMDPs are the worlds, the satisfaction relation ⊩ is used, the bases are the singletons {φ} of state formulas, and the abstract union of {φ} and {ψ} is {φ ∧ ψ}. Then what they refer to as base change operators, are precisely what we refer to as belief revision operators.

• For every belief revision operator ◦ satisfying (B1)- (B6) there exists a min-complete, min-expressible and faithful pMDP assignment ⪯(-) such that �φ ◦ ψ� = min(�ψ�, ⪯φ).

[Delgrande et al., 2018] introduce a postulate (Acyc), which (applied to PLBP+ state formulas as a base logic) states the following:

• For any φ and ψ0, . . . , ψn with �ψi ∧ (φ ◦ ψ(i+1) mod (n+1))� ̸= ∅ for all i, it holds that �ψ0 ∧ (φ ◦ ψn)� ̸= ∅.

By Theorem 10.13 of [Falakh et al., 2023], we get that the following statements hold:

• For every min-complete, min-expressible and faithful pMDP assignment ⪯(-), there exists a belief revision operator ◦ satisfying (B1)-(B6) and (Acyc) such that �φ ◦ ψ� = min(�ψ�, ⪯φ).

We see that in fact, PLBP+ state formulas formwhat they call a disjunctive base logic, since PLBP+ state formulas contain disjunctions. Therefore, their Corollary 10.17 applies and tells us that any belief revision operator ◦ satisfying (B1)- (B6) also automatically satisfies (Acyc), which completes our proof.

• For every belief revision operator ◦ satisfying (B1)-(B6) and (Acyc), there exists a min-complete, min-expressible and faithful pMDP assignment ⪯(-) such that �φ ◦ ψ� = min(�ψ�, ⪯φ).

While Theorem 2 gives us a representation theorem for belief revision operators, it does not give us much in the way of practical belief revision. It is not clear from the start howwe can come up with min-complete and min-expressible pMDP assignments. And even if we find such assignments, we have no guarantee in general that the resulting belief revision operator ◦ is actually computable. Therefore we propose finitely expressible pMDP assignments, which are a more specific class of pMDP assignments that are both easily understood from an intuitive, conceptual point of view, as well as computable under very mild assumptions. We start with some technical preliminaries.

Definition 10 (Finitariness). A total preorder ⪯ on a (possibly infinite) set X is finitary if the set {[x]⪯ | x ∈ X} is finite, where [x]⪯ = {y ∈ X | x ⪯ y and y ⪯ x}. Given a finitary total preorder ⪯ and x ∈ X, we write level⪯(x) := |{[y]⪯ | y ∈ X and y ⪯ x}|. Writing height(⪯) := |{[x]⪯ | x ∈ X}|, we define the level sets X⪯,1, . . . ,X⪯,height(⪯) by putting X⪯,k := {x ∈ X | level⪯(x) = k}.

The idea is that a finitary total preorder may be defined on an infinite set, but it divides the set into finitely many 'levels' of equivalent elements.

Definition 11 (FEF pMDP assignments). A pMDP assignment ⪯(-) is finitely expressible if ⪯φ is finitary for all φ ∈ Bel, and for all φ there exist φ1 , . . . , φheight(⪯φ) ∈ Bel such that �φk � = pMDP⪯φ,k, i.e. the k-th level set of pMDP according to ⪯φ. We refer to finitely expressible and faithful pMDP assignments as FEF pMDP assignments for short.

Finitely expressible pMDP assignments divide the space of pMDPs into finitely many levels for every φ, with every level expressible by formulas of PLBP+. And indeed, finite expressibility implies both min-completeness and min-expressibility.

FEF pMDP assignments are conceptually simple, because they are in fact the same as specifying for every φ a finite sequence of weakenings of φ, which corresponds intuitively to the idea that in revision we keep removing information step-by-step from our beliefs until they can accommodate the new information. We make this correspondence precise in Proposition 1.

Definition 12 (Belief weakening maps). A belief weakening map is a function ⟨-⟩ : Bel → Bel+ (where we write Bel+ to denote the set of all non-empty finite sequences of φ ∈ Bel) assigning to all φ ∈ Bel a finite sequence ⟨φ⟩1 ⊩ · · · ⊩ ⟨φ⟩n, such that ⟨φ⟩1 ≡ φ.

Proposition 1. The following statements hold:

• For every FEF pMDP assignment ⪯(-) there exists a belief weakening map ⟨-⟩ such that |⟨φ⟩| = height(⪯φ ) + 1 and �⟨φ⟩k� = ⋃1⩽ℓ⩽k pMDP⪯φ,ℓ for all φ and k.
• For every belief weakening map ⟨-⟩, there exists an FEF pMDP assignment ⪯(-) such that height(⪯φ) ⩽ |⟨φ⟩| + 1 and �⟨φ⟩k� = ⋃1⩽ℓ⩽k pMDP⪯φ,ℓ for all φ and k.

Proof. Take an FEF pMDP assignment ⪯(-). Since it is finitely expressible, we have that for all φ there exist φ1 , . . . , φheight(⪯φ) such that �φk � = pMDP⪯φ,k. Defining the belief weakening map by putting ⟨φ⟩1 := φ and ⟨φ⟩k+1 := ∨1⩽ℓ⩽k φℓ for 1 ⩽ k ⩽ height(⪯φ), we indeed get the required property.

Now take a belief weakening map ⟨-⟩. Given φ and P, write

i.e. the number of the first weakening of φ that P satisfies if possible, and otherwise ∞. We define the pMDP assignment by putting P ⪯φ P′ iff ⟨φ, P⟩ ⩽ ⟨φ, P′ ⟩. It is immediate that this assignment produces total preorders, since it is defined by comparing numbers. Faithfulness follows from the observations that (i) ⟨φ, P⟩ = 1 if P ⊩ φ, (ii) ⟨φ, P⟩ > 1 if P ⊮ φ, and (iii) the definition being completely syntax-invariant.

Finitariness follows from ⟨φ, P⟩ taking at most |⟨φ⟩| + 1 values. If we do not have ⟨φ⟩k ≡ ⟨φ⟩ℓ for any k ̸= ℓ (i.e. the weakenings are semantically distinct), if ∨⟨φ⟩ is not a tautology (i.e. the value ⟨φ, P⟩ = ∞ can appear), and if φ is satisfiable, then height(⪯φ) = |⟨φ⟩| + 1. If any of those assumptions do not hold (e.g. if ∨⟨φ⟩ is a tautology), then the height may be lower, though never higher.

To see that the assignment is finitely expressible, we recursively define for 1 ⩽ k ⩽ height(⪯φ) the formulas φk by putting

where the maximum is taken to be 0 if it would not be defined.

The idea of this construction is that it takes care of the possibilities that (i) φ ≡ ⊥, and that (ii) ⟨φ⟩k ≡ ⟨φ⟩ℓ for some k ̸= ℓ.

We now argue that the belief revision operators resulting from FEF pMDP assignments (in the sense of Theorem 2) are computable if the underlying belief weakening map is computable. To compute φ ◦ ψ, first check if ψ is satisfiable (which is decidable by Theorem 1): if it is not, we safely output ⊥. Then compute ⟨φ⟩1, . . . , ⟨φ⟩n, and iterate over all 1 ⩽ k ⩽ n, checking whether ψ ∧ ⟨φ⟩k is satisfiable. For the first such k, output the formula ψ ∧ ⟨φ⟩k. If no such k exists, output ψ.

We now show that we can actually give a representation theorem for FEF pMDP assignments. For this we introduce a novel postulate (Bω), expressing the finitariness of the revision operator. In the postulate, we define a belief partition to be a sequence φ1 , . . . , φn ∈ Bel of some length n, such that (i) φ1 ∨ · · · ∨φn is a tautology, (ii) φk is satisfiable for all k, and (iii) φk ∧ φℓ is unsatisfiable for all k ̸= ℓ.

• (Bω) For all φ there exists a belief partition φ1 , . . . , φn , such that for all ψ, there exists k with φ ◦ ψ ≡ ψ ∧ φk .

Theorem3 (Representation for FEF pMDP assignments). The following statements hold:

• For every FEF pMDP assignment ⪯(-) there exists a belief revision operator ◦ satisfying (B1)-(B6) and (Bω), such that �φ ◦ ψ� = min(�ψ�, ⪯φ).
• For every belief revision operator ◦ satisfying (B1)-(B6) and (Bω) there exists an FEF pMDP assignment ⪯(-) such that �φ ◦ ψ� = min(�ψ�, ⪯φ).

Proof. Take an FEF pMDP assignment ⪯(-). Since finite expressibility entails min-expressibility, we apply the construction used by [Falakh et al., 2023] in their Definition 6.3: we let φ ◦ ψ := ψ⪯,φ (which we defined in our Definition 9). As observed by [Falakh et al., 2023] in the proof of their Theorem 6.4, it follows from the min-completeness (and min-retractiveness, which is entailed by our assignment producing total preorders) of ⪯ (which we get again from it being finitely expressible) that ◦ satisfies (B1)-(B6). And by definition of min-expressibility, we get that �φ ◦ ψ� = min(�ψ�,⪯φ). It remains to show that ◦ also satisfies (Bω). It actually suffices to see that the formulas φ1 , . . . , φk we get from ⪯ being finitely expressible, form a belief partition. Since �φ ◦ ψ� = min(�ψ�,⪯φ), it follows from finitariness that for all φ and ψ there is some k such that �φ ◦ ψ� = �ψ� ∩ pMDP⪯,k = �ψ ∧ φk �.

Take a belief revision operator ◦ satisfying (B1)-(B6) and (Bω). By Corollary 10.17 of [Falakh et al., 2023], we know that ◦ satisfies their postulate (Acyc) as well. Therefore, by their Theorem 10.13, there exists a faithful pMDP assignment ⪯ such that �φ ◦ ψ� = min(�ψ�, ⪯φ). Fix φ. Since ◦ satisfies (Bω), there exists a belief partition φ1 , . . . , φn such that for all ψ, there is some k with φ ◦ ψ ≡ ψ ∧ φk .

In the following, we introduce the notation pMDP/⪯φ = {[P]⪯φ | P ∈ pMDP}.

For the finite expressibility of ⪯, we will show that {�φ1 �, . . . , �φk �} = pMDP/⪯φ, which is precisely what finite expressibility means. We note that it suffices to show that (i) for all 1 ⩽ k ⩽ n, there is some X ∈ pMDP/⪯φ such that �φk � ⊆ X, and (ii) the previous correspondence is injective, i.e. for all X ∈ pMDP/⪯φ there is at most one 1 ⩽ k ⩽ n with �φk � ⊆ X. The reason this would suffice is as follows. By definition of belief partitions, the sets �φ1 �, . . . , �φk � form a partition of pMDP. And clearly, pMDP/⪯φ is also a partition. So (i) states that {�φ1 �, . . . , �φk �} is a refinement of pMDP/⪯φ. But in fact, we can see that pMDP/⪯φ is also a refinement of {�φ1 �, . . . , �φk �}, and thus, since refinement is an antisymmetric relation, we are able to conclude that {�φ1 �, . . . , �φk �} = pMDP/⪯φ. To see that pMDP/⪯φ is also a refinement of {�φ1 �, . . . , �φk �}, take any X ∈ pMDP/⪯φ, and suppose for the sake of contradiction that there is no k such that X ⊆ �φk �. Since {�φ1 �, . . . , �φk �} is a partition and it must be that X ̸= ∅, this means that there exist distinct ℓ ̸= m such that X ∩ �φℓ � ̸= ∅ ̸= X ∩ �φm�. But by (i), we have that �φℓ � ⊆ Xℓ and �φm� ⊆ Xm for some Xℓ , Xm ∈ pMDP/⪯φ, and by (ii), we must have that Xℓ ̸=Xm. Therefore, we have that X∩Xℓ ̸= ∅ ̸=X∩Xm, which contradicts pMDP/⪯φ being a partition, since a cell cannot intersect two distinct cells (it only intersects itself).

To see that (i) holds, take any φk . By definition of belief partitions, φk is satisfiable. Therefore, by postulate (B3), we get that φ ◦ φk is satisfiable as well. By (Bω), it must be that φ ◦ φk ≡ φk ∧ φl for some ℓ. But ℓ must be equal to k, since φk and φℓ for distinct k ̸= ℓ are mutually unsatisfiable, which would contradict φ ◦ φk being satisfiable. Therefore, φ ◦ φk ≡ φk . Since �φ ◦ ψ� = min(�ψ�, ⪯φ) for all ψ, we get in particular that �φk � = min(�φk �,⪯φ). But that means that for all P, P′ ∈ �φk �, we have that P ⪯φ P′ and vice-versa. So by definition of pMDP/⪯φ, we get that φk ⊆ X for some X ∈ pMDP/⪯φ.

To see that (ii) holds, take any X ∈ pMDP/⪯φ, and suppose for the sake of contradiction that there exist k ̸= ℓ such that �φk � ⊆ X and �φℓ � ⊆ X. By definition of pMDP/⪯φ, we get that for all P ∈ �φk � and P′ ∈ �φℓ �, it holds that P ⪯φ P′ and vice-versa. Consider the formula φk ∨φℓ . As this is satisfiable, we have that φ◦(φk ∨φℓ ) is as well, by (B3). By (Bω), we know that φ◦ (φk ∨φℓ ) ≡ (φk ∨φℓ )∧φm for some m. It must be that m ∈ {k, ℓ}, as otherwise (φk ∨ φℓ ) ∧ φm would be unsatisfiable by definition of belief partitions. So either φ◦(φk ∨φℓ ) ≡ φk or φ◦(φk ∨φℓ ) ≡ φℓ - assume w.l.o.g. that it is the former. Since �φ ◦ ψ� = min(�ψ�,⪯φ) for all ψ, we thus get in particular that �φk � = min(�φk ∨ φℓ �, ⪯φ) = min(�φk � ∪ �φℓ �,⪯φ). As we know by definition of belief partitions that �φk � ̸= �φℓ �, this contradicts our earlier finding that for all P ∈ �φk � and P′ ∈ �φℓ �, it holds that P ⪯φ P′ and vice-versa.

4.2 Intention Revision

Unlike belief revision operators, intention revision operators do not act solely on intentions, but actually perform revision in the context of strong beliefs.

Definition 13 (Intention revision operator). An intention revision operator is a function ·: Int × Bel × Int → Int, with Φ ·φ Ψ being read as the result of revising Φ by Ψ under the strong beliefs φ.

There are a couple of desiderata for an intention revision operator ·. First, since we are revising Φ with a new intention Ψ, the outcome of revision Φ·φΨ should in some sense 'entail' Ψ. Or at least, we should believe (given our strong beliefs φ) that Ψ is achievedwhenever Φ·φΨ is achieved. In other words, Ψ should be weakly believed to hold given φ and Φ ·φ Ψ. As we may want to be able to neglect outcomes produced by policies that achieve Φ ·φ Ψ with negligible probability, we again speak of θ-weak beliefs per our discussion in Section 3. We follow the traditional AGM approach of revision, which always accepts the new datum we are revising by.

Fixing a θ throughout this section, our desideratum becomes the following postulate:

Second, if Φ ∧ Ψ and φ are θ-coherent, then revising Φ by Ψ w.r.t. φ should produce something whose achievement is 'equivalent' to that of Φ ∧ Ψ: we only drop intentions when necessary. Similar considerations apply as with the first desideratum: the equivalence need only be up to the agent's weak beliefs. We formalize this as stating that Φ ∧ Ψ ∈ WBθ(φ, Φ ·φ Ψ) and Φ ·φ Ψ ∈ WBθ(φ, Φ ∧ Ψ) - or equivalently, the following postulate:

• (I2) If φ and Φ∧Ψ are θ-coherent, thenWBθ(φ,Φ·φΨ) = WBθ (φ, Φ ∧ Ψ).

Third, intention revision should produce actionable intentions when possible. If φ and Ψ are θ-coherent, then φ and Φ ·φ Ψ should also be. Our postulate becomes:

• (I3) If φ and Ψ are θ-coherent, then φ and Φ ·φ Ψ are θcoherent.

At this point it is first important to note that our desiderata so far are conceptually highly similar to the postulates (B1)-(B3) of belief revision. This similarity can in fact be made precise: we define a new 'entailment' relation on path formulas, ⊨θφ, given by putting Φ ⊨θφ Ψ iff Ψ ∈ WBθ(φ, Φ), and Φ ∼=θφ Ψ iff WBθ(φ, Φ) = WBθ(φ, Ψ). The desiderata are then precisely the postulates (B1)-(B3), with ⊨θφ replacing ⊩, ∼=θφ replacing ≡, and θ-coherence w.r.t. φ replacing satisfiability. The next three postulates are similarly analogues of (B4-B6).

• (I4) If WBθ(φ,Φ1) = WBθ(φ,Φ2) and WBθ(φ,Ψ1) = WBθ(φ,Ψ2), then WBθ(φ,Φ1 ·φ Ψ1) = WBθ(φ,Φ2 ·φ Ψ2).
• (I5) Φ ·φ (Ψ∧Ω) ∈WBθ((Φ ·φ Ψ) ∧Ω).
• (I6) If φ and (Φ·φΨ)∧Ωare θ-coherent, then (Φ·φΨ)∧Ω ∈ WBθ(Φ ·φ (Ψ ∧ Ω)).

The postulate (I4) is stating that intention revision is syntaxinvariant, though again up to the agent's weak beliefs. Postulates (I5) and (I6), similar to (B5) and (B6) play a role in ensuring the representation of Theorem 4 goes through.

Example 5. We consider Theo's original intention Φ1 of attending the concert tomorrow, and revise with the intention Φ2 of buying a drink tomorrow. The postulates again tell us some things about the revision Φ1 ·φ1 Φ2. By (I3), we have that since Φ2 is 0.05-coherent w.r.t. φ1, it must be that Φ1 ·φ1 Φ2 is also 0.05-coherent w.r.t. φ1. Therefore Φ1 ·φ1 Φ2 ̸∼=0.05 φ1 Φ1∧Φ2 (as we knowΦ1∧Φ2 not to be 0.05-coherent w.r.t. φ1), and since ∼= ⊆ ∼=0.05 φ1 , we get that Φ1 ·φ1 Φ2 ̸∼= Φ1 ∧ Φ2, i.e. the revision must drop some of his intentions. But whatever it drops, (I1) tells us that we still have Φ2 ∈ WB0.05(φ1, Φ1 ·φ1 Φ2) - Theo 0.05-weakly believes he will buy drinks tomorrow. And Φ1 ̸∈ WB0.05(φ1, Φ1 ·φ1 Φ2), as we saw that Φ1 ·φ1 Φ2 ̸∼=0.05 φ1 Φ1 ∧Φ2: the revised intention does not contain the intention of attending the concert.

Now, we start on a representation theorem for intention revision. Instead of intention revision using orderings on paths, like one might think, we need to take the strong beliefs φ and the threshold θ into account in order to produce θ-coherent intentions. The orderings are on what we call θ-bundles, which are to be thought of as sufficiently (according to θ) likely outcomes of a policy.

Definition 14 (θ-bundles). A θ-bundle in a pMDP P = (M, s) is a triple B = (M, π,W) consisting of a P-policy π and a set W ⊆ Paths(π) such that µπ(W) > θ. The set of θbundles in P is denoted Bunθ(P). For φ ∈ Bel, we write Bunθ(φ) = ⋃P∈�φ� Bunθ (P).

Now, for a θ-bundle B = (M, π,W) and Φ ∈ Int, we define B ⊨ Φ iff M, π,w ⊩ Φ for all w ∈ W. The seemingly odd notation is justified by the following observation: Ψ ∈ WBθ(φ, Φ) iff for all B ∈ Bunθ(φ) it holds that B ⊨ Φ implies B ⊨ Ψ. In other words, we can think of our earlier 'entailment relation' ⊨θφ of path formulas (defined as Φ ⊨θφ Ψ iff Ψ ∈ WBθ(φ, Φ)) as actually being derived in the standard way from the satisfaction relation ⊨ ⊆ Bunθ(φ) × Int.

This means that, fixing φ ∈ Bel, PLBP+ path formulas Ψ ∈ Int and θ-bundles B ∈ Bunθ(φ) form an instance of base logics in the sense of [Falakh et al., 2023], in which θ-coherence w.r.t. φ is the notion of satisfiability. We can utilize this powerful fact to give definitions and a representation theorem that fully mirror those we gave for belief revision: the definitions and theorems here are the same as in Section 4.1, in which occurences of ⊩ are replaced by ⊨θφ and pMDPs are replaced by θ-bundles B ∈ Bunθ(φ).

In the following, we write [Φ]θφ for the set of all B ∈ Bunθ(φ) such that B ⊩ Φ.

Definition 15 (θ-bundle assignments). A θ-bundle assignment is a Bel-indexed family ⪯(-,-) of functions ⪯φ,(-) : Int → 2Bunθ(φ)×Bunθ(φ) such that ⪯φ,Φ is a total preorder for all Φ. The assignment is faithful if: (i) If B ⊨ Φ and B′ ⊨ Φ, then B ⪯φ,Φ B′ and B′ ⪯φ,Φ B. (ii) If B ⊨ Φ and B′ ⊭ Φ, then B ≺φ,Φ B′ . (iii) If Φ ∼=θφ Ψ, then ⪯φ,Φ = ⪯φ,Ψ.

The assignment is finitely expressible if ⪯φ,Φ is finitary for all φ and Φ, and for all φ and Φ there exist Φφ,1 , . . . ,Φφ,height(⪯φ,Ψ) ∈ Int such that [Φφ,k ]θφ = (Bunθ(φ))⪯φ,Φ,k, i.e. the k-th level set of Bunθ(φ) according to ⪯φ,Φ. We refer to finitely expressible and faithful θ-bundle assignments as FEF θ-bundle assignments for short.

We have an analogue of Proposition 1, showing how FEF θ-bundle assignments are precisely θ-intention weakening maps, assigning to every φ and Φ a sequence of path formulas ⟨Φ⟩φ1 ⊨θφ · · · ⊨θφ ⟨Φ⟩φn such that ⟨Φ⟩φ1 ∼=θφ Φ. And using a new postulate (Iω), we can give a representation theorem for FEF θ-bundle assignments. In the following, a θ-intention partition for φ is a sequence Φ1 , . . . ,Φn ∈ Int such that (i) Φ1 ∨ · · · ∨ Φn is a tautology w.r.t. ⊨θφ, (ii) φ and Φk are θcoherent for all k, and (iii) φ and Φk ∧ Φℓ are not θ-coherent for all k ̸= ℓ.

• (Iω) For all φ and Φ there exists a θ-intention partition Φ1 , . . . ,Φn w.r.t. φ, such that for all Ψ, there exists k with Φ ·φ Ψ ∼=θφ Ψ ∧ Φk .

Theorem 4 (Representation for intention revision). The following statements hold:

• For every FEF θ-bundle assignment ⪯(-,-) there exists an intention revision operator · satisfying (I1)-(I6) and (Iω), such that [Φ ·φ Ψ]θφ = min([Ψ]θφ, ⪯φ,Φ).
• For every intention revision operator · satisfying (I1)- (I6) and (Iω) there exists an FEF θ-bundle assignment ⪯(-,-) such that [Φ ·φ Ψ]θφ = min([Ψ]θφ, ⪯φ,Φ).

Proof sketch. The proof is identical to that of Theorem 3: for every φ, we now consider path formulas with the entailment relation ⊨θφ to form a base logic in the sense of [Falakh et al., 2023], interpreted over θ-bundles in Bunθ(φ).

We conclude this section by stating that intention revision operators satisfying (I1)-(I6) and (Iω) are computable if the underlying θ-intention weakening maps are computable, by a conceptually identical algorithm as for belief operators. To compute Φ ·φ Ψ, first check if φ and Ψ are θ-coherent: if not, output ⊥. Then compute ⟨Φ⟩φ1 , . . . , ⟨Φ⟩φn , and iterate over 1 ⩽ k ⩽ n, checking whether φ and Ψ ∧ ⟨Φ⟩φk are θ-coherent. For the first such k, output Ψ ∧ ⟨Φ⟩φk . If no such k exists, output Ψ.

4.3 Joint Revision of Beliefs and Intentions

In this section, we present the fundamental interaction between beliefs and intentions that motivates the current work: revision of beliefs may trigger revision of intentions, and vice-versa. We capture this interaction through the following definition in which joint revision proceeds by first revising strong beliefs, and then revising intentions w.r.t. the revised strong beliefs.

Definition 16 (Belief-intention revision operator). Given a belief revision operator ◦ and an intention revision operator ·, their belief-intention revision operator is the function ∗: (Bel × Int)2 → Bel × Int defined as (φ,Φ) ∗ (ψ,Ψ) := (φ ◦ ψ, Φ ·φ◦ψ Ψ).

Note that we define the joint revision operator through independent belief and intention revision operators. We could have taken joint revision operators as primitive and provided postulates for them capturing the desired interplay, but the definition above simplifies presentation and follows earlier lines of work [van Zee et al., 2020].

In joint revision, belief revision may trigger intention revision, since the intention revision's notion of coherence depends on the new strong belief φ◦ψ. And vice-versa, intention revision triggers belief revision, though key is the separation between strong and weak beliefs: only the latter depend on intentions, as seen in Definition 7. As argued earlier, intention revision should not change strong beliefs.

The postulates for belief and intention revision tell us certain properties of these joint belief-intention revision operators, which we illustrate through our running example.

Example 6 (Running example, continued). First, note that intention revision changes weak beliefs. We saw in Example 3 that X¬five ∈ WB0.05(φ1, Φ1): when intending to attend the concert, Theo 0.05-weakly believes he will be out of money tomorrow. Now consider the revision (φ1,Φ1) ∗ (⊤,Φ2) = (φ1,Φ3) (i.e. we just wish to revise with the intention to buy a drink). By the postulates for intention revision, we get that Xfive ∈ WB0.05(φ1, Φ3), since Φ3 ⊨0.05 φ Φ2 ⊨0.05 φ Xfive.

So after revision, we weakly believe that Theo does have $5 tomorrow: otherwise, he could not buy a drink tomorrow.

Now, note that belief revision actually changes intentions. Consider the revision (φ1, Φ1)∗(φ2, ⊤) = (φ1◦φ2, Φ1·φ1◦φ2 ⊤). We know that since φ2 is satisfiable, φ1 ◦ φ2 must also be by our belief revision postulates. So we have that ⊤ is 0.05-coherent w.r.t. φ1 ◦ φ2 (⊤ always is as long as the strong beliefs are satisfiable). We can derive by our intention revision postulates that Φ1 ·φ1◦φ2 ⊤ must also be 0.05-coherent w.r.t. φ1 ◦ φ2. But we know that φ2 and Φ1 are not 0.05-coherent. Therefore, it cannot be that Φ1 ·φ1◦φ2 ⊤ ⊨0.05 φ1 Φ1. This means that by revising with the belief that the band is popular, Theo is forced to abandon his intention to attend the concert.

5 Conclusion

We have initiated the study of belief and intention revision in stochastic environments, expressed in an appropriate probabilistic temporal logic. We give rationality postulates for revision, and prove representation theorems both for revision operators in general, as well for operators that are generally computable using the novel postulates (Bω) and (Iω).

In future work, we plan to extend our framework to allow for iterated revision, `a la [Darwiche and Pearl, 1997]. We also wish to develop a representation theorem with a modified version of (I1), which would allow success of revision only given coherent new intentions, as is also the case in the work of [van Zee et al., 2020]. Such revision could follow the approach as taken in the consistent AGM revision of [Hansson, 2023a; Hansson, 2023b], where revision with inconsistent statements maintains the original beliefs, or the more nuanced approach of [Konieczny et al., 2010], in which revision by a formula does not need to immediately entail it, but instead only increase its plausibility every time it is revised with.