From knowledge-based programs to graded belief-based programs, part II: off-line reasoning

1 Introduction

Knowledge-based programs, or KBPs [Fagin et al., 1995] are a powerful notion for expressing action policies in which branching conditions refer to knowledge (an agent acts according to what he knows), such as, typically, if Kϕ then π else π′

where K is an epistemic (usually S5) modality, and π, π′ are subprograms. However, branching conditions in KBPs cannot refer to possibly erroneous beliefs or to graded belief, such as in "repeat ask to someone about the way to the railway station until my belief about the direction to take is strong enough". Recently, [Laverny and Lang, 2004] made a first step towards reasoning with belief-based programs (BBPs), where knowledge modalities of KBPs are replaced by graded belief modalities, whose semantics relies on belief states defined as ranking functions, which can be revised by observations and progressed by physical actions, which enables the agent to maintain his current belief state about the world while executing a BBP. Note that BBPs extend a restricted class of KBPs, in which (a) there is a single agent, (b) the agent has perfect recall and (c) branching conditions concern the agent's knowledge about the present state of the world.

However, [Laverny and Lang, 2004] cannot deal with offline reasoning about the effects of a belief-based program. Assume for instance that agent A is looking for the way to the railway station in a foreign town; her initial belief state is void, and she follows a plan consisting in sequentially asking to several pedestrians about the direction to follow, until she has acquired a sufficient level of certainty. Assume moreover

Jérôme Lang

IRIT Université Paul Sabatier 31062 Toulouse Cedex, France lang@irit.fr

that answers, although not fully reliable, are normally correct. Each time A gets a direction confirming (resp. contradicting) her current belief, this belief becomes stronger (resp. weaker). Now, the assumption that answers are normally correct implies, for instance, that if A has already got 3 "right" and no "left" then the next answer is more likely to be "right" again than "left": the plausibility of getting an observation depends on the current state.

Coping with this issue results in a natural way in secondorder uncertainty when projecting a belief state by a BBP: in our example, the agent is able to predict beforehand something like "after asking 5 pedestrians, normally I'll have a very firm belief about the direction to the station, although I cannot totally exclude the possibility that I'll have only a weak, or even a totally void belief". Such a complex belief state is a belief state about (future) belief states, that is, a second-order belief state. Thus, the main concern of this paper is how to do a priori reasoning about the possible states of belief produced by executing the program: uncertainty about which of these states of belief will result is itself represented as a ranking over states of belief.

After recalling some background in Section 2, belief-based programs are introduced in Section 3. Section 4 deals with complex belief states and their progression by actions and programs. In Section 5 we show how to compute progression syntactically. Related work is discussed in Section 6.

2 Background

In this Section we briefly recall some notions from [Laverny and Lang, 2004]. Let PS be a finite set of propositional symbols. LPS is the (non-modal) propositional language generated from PS, the usual connectives and the Boolean constants ⊤ and ⊥. S = 2PS is the set of states associated with PS. Formulas of LPS are said objective. If ϕ ∈ LPS then Mod(ϕ) = {s ∈ S|s |= ϕ}. For A ⊆ S, Form(A) is the objective formula (unique up to logical equivalence) such that Mod(F orm(A)) = A.

Belief states are identified with ordinal conditional functions (OCF) [Spohn, 1988]: a belief state is a function κ : S ↦-→ N, where N = N∪{+∞}, such that mins∈S κ(s) = 0. κ is lifted from S to LPS by κ(ϕ) = min{κ(s) | s |= ϕ}, with the convention min(∅) = +∞ (we will use this convention throughout the paper without recalling it). κ(s) can be seen as the exceptionality degree of s. In particular, κ(s) = 0

means that s is a normal state and κ(s) = +∞ that s is totally impossible. For any ϕ ∈ LPS, the belief state κϕ is defined by κϕ(s) = { 0 if s |= ϕ +∞ if s |= ¬ϕ . In particular, κ⊤ is the void belief state: ∀s, κ⊤(s) = 0.

Beliefs are expressed syntactically in a graded extension KD45G of KD45, whose language LPS is defined as follows:

• (a) if ϕ ∈ LPS then B1ϕ, B2ϕ, . . . , B∞ϕ are in LPS;

(b) if Φ and Ψ in LPS then ¬Φ, Φ ∨ Ψ, Φ ∧ Ψ in LPS.

Note that LPS considers only subjective and flat formulas 1 . Formulas of LPS are denoted by capital Greek letters Φ,Ψ etc. while objective formulas are denoted by small Greek letters ϕ, ψ etc. Biϕ intuitively means that the agent believes ϕ with strength i. The larger i, the stronger the belief expressed by Bi, and B∞ is a knowledge (true belief) modality.

The truth of a formula of LPS in an belief state κ is defined by:

• (a) for ϕ objective and i ∈ N, κ |= Biϕ iff κ(¬ϕ) ⩾ i;
• (b) κ |= Φ∨Ψ iff κ |= Φ or κ |= Ψ;
• (b) κ |= Φ ∧ Ψ iff κ |= Φ and κ |= Ψ;
• (c) κ |= ¬Φ iff κ ̸|= Φ.

Thus, κ |= Biϕ holds as soon as any countermodel of ϕ is exceptional at least to the degree i, or, equivalently, that all states such that κ(s) < i are models of ϕ. In particular, B1ϕ is satisfied when all normal states satisfy ϕ, and B∞ϕ is satisfied when all possible states (to any degree) are models of ϕ.

An observation is a belief state κobs, representing all we observe when getting the observation. Observations can be incomplete and partially unreliable (see [Laverny and Lang, 2004] for examples). The agent revises her current belief state by an observation by combining both: the revision of κ by κobs is undefined when minS(κ + κobs) = ∞, and otherwise is the belief state defined by

In particular, κ⊤ ⊕ κobs = κobs and (κ ⊕ κϕ) = κ(.|ϕ), where κ(.|ϕ) is Spohn's conditioning [Spohn, 1988].

A physical action α is a feedback-free action (that is, it possibly changes the state of the world but does not give any feedback), defined by a transition model consisting of a collection of belief states {κα(.|s), s ∈ S}. κα(s′ |s) is the exceptionality degree of the outcome s′ when performing α in state s. The progression of a belief state κ0 by α is the belief state κ ⋄ α = κ(.|κ0, α) defined (cf. [Boutilier, 1998]) by

A positive formula of LPS is a formula where no Bi appears in the scope of negation. A positive conjunctive (PC) formula of LPS is a formula of the form B∞ϕ∞ ∧

1 This restriction is made for the sake of simplicity; it would be possible to consider nested modalities, and then prove, as it is the case in KD45, that each formula is equivalent to a flat formula, but this issue has no relevance to the issues dealt with in this paper. Likewise, combinations of objective and subjective formulas do not play any role either for expressing belief-based programs.

Bnϕn ∧ . . . ∧ B1ϕ1; without loss of generality we can assume ϕi |= ϕi+1, since B∞ϕ∞ ∧ Bnϕn ∧ . . . ∧ B1ϕ1 is equivalent to B∞ϕ∞ ∧ Bn(ϕ∞ ∧ ϕn) ∧ . . . ∧ B1(ϕ∞ ∧ ϕn ∧ . . . ∧ ϕ1). There is a one-to-one correspondance between belief states and satisfiable PC formulas (modulo logical equivalence): for each κ, the PC formula G(κ) = Φκ is defined as B∞ϕ∞ ∧ Bnϕn ∧ . . . ∧ B1ϕ1, where n = max{k < ∞, ∃s such that κ(s) = k}, and for every i ∈ N∗ , ϕi = Form({s, κ(s) < i}). (Note that n is finite, because S is finite and minκ = 0.) For instance, let κ([a, b]) = 0, κ([a, ¬b]) = 1, κ([¬a, b]) = 3 and κ([¬a, ¬b]) = ∞, then Φκ = B∞(a∨b)∧B3a∧B2a∧B1(a∧b) - which is equivalent to B∞(a ∨ b) ∧ B3a ∧ B1b. Conversely, for each satisfiable PC formula Ψ there is a belief state κΨ = H(Ψ) such that G(H(Ψ)) ≡ Ψ. G(κ) represents all the agent believes in κ2 . We will sometimes make the following slight abuse of notation: when a PC formula Ψ is equivalent to a shorter (but not PC) formula Ψ′ , we write κΨ′ instead of κΨ. For instance, the PC formula Ψ = B∞ϕ∞⊤∧B3⊤∧B2r ∧B1r is equivalent to B2r, therefore we write κB2r instead of κΨ.

3 Belief-based programs

Belief-based programs (BBP) are built up from a set of actions ACT and program constructors:

• the empty plan λ is a BBP;
• for any α ∈ ACT , α is a BBP;
• if π and π′ are BBPs then (π; π′ ) is a BBP;
• if π and π′ are BBP and Φ ∈ LPS, then (if Φ then π else π′ ) and (while Φ do π) are BBPs.

Thus, a BBP is a program whose branching conditions are doxastically interpretable: the agent can decide whether she believes to a given degree that a formula is true (whereas she is generally unable to decide whether a given objective formula is true in the actual world). For instance, the agent performing the BPP

performs the sensing action ask until she has a belief firm enough (namely of degree 2) about the way to follow (whether π is guaranteed to stop is a good question!).

Progression and revision in [Laverny and Lang, 2004] are used for maintaining the agent's current belief state while the program is being executed. However, predicting the future possible states resulting from the execution of a BBP before it has started to be executed (off-line evaluation) cannot be done in a satisfactory way. Consider π = ask; ask; ask; ask, consisting in asking in sequence to 4 pedestrians about the way to the station. Assume that each occurrence of ask can send back obs1 = κB1r or obs2 = κB1¬r, corresponding respectively to a pedestrian telling that the station is on the right (resp. left), taken with some limited reliability (for the sake of simplicity we exclude "don't know" answers). Then all we can predict is that after doing π the agent will be in one of the 5 belief states κB4r, κB4¬r, κB2r, κB2¬r, κ⊤3 . The point now is that obs1 and obs2 cannot always be considered as likely as each other: for instance, we may wish to express that accurate observations are more frequent than inaccurate ones. Therefore, observations should be ranked by their plausibility of occurrence given the current state and the sensing action performed. Then, the projection of an initial belief state by a program results in a second-order (or complex) belief state: in our example, one would expect to obtain that after asking to two persons, then normally the agent is the belief state κB2r or in the belief state κB2¬r, and exceptionally in the void belief state κ⊤. This issue is developed in next Section.

2 This could be formalized by extending our language with graded doxastic versions O1, . . . , O∞ of the only knowing modality (e.g. [Levesque and Lakemeyer, 2000]), Oiϕ meaning that all the agent believes to the degree i is ϕ. Due to space limitations we must omit the details.

4 Complex belief states and progression

4.1 Complex belief states

Definition 1 Let BS be the set of all belief states on S. A complex belief state (CBS) is an ordinal conditional function µ on BS, i.e., a function µ : BS → N such that minκ∈BS µ(κ) = 0

µ is a second-order belief state expressing the beliefs, before executing some given program π, about the (future) possible belief states resulting from its execution.

Example 1 Let S = {r, ¬r}.

is a CBS (by convention, for any belief state κ not mentioned we have µ(κ) = +∞); it intuitively represents a situation where the agent expects the resulting belief state to be either κ0, κ3 or κ4, these last two being normal results and κ0 being exceptional. Note that κ0 = κ⊤, κ3 = κB2r and κ4 = κB2¬r.

We define µκ as the (degenerated) CBS defined by µκ(κ) = 0 and µκ(κ′ ) = ∞ for all κ′ ̸= κ.

Note that since, unlike S, BS is not finite, some CBSs cannot be finitely represented. We say that µ has a finite support iff only a finite number of belief states have a finite plausibility, i.e., {κ ∈ BS|µ(κ) < ∞} is finite; in this case we define nµ (or simply n where there is no ambiguity) as max{i < ∞ | ∃κ such that µ(κ) = i}.

4.2 Progression by sensing actions

Consider a finite set ACTS of sensing actions, that send feedback to the agent, under the form of observations. Each sensing action is defined by a state-dependent plausibility assignment on possible observations.

3 The notation κΦ has been introduced at the end of Section 2.

Definition 2 Let OBS ⊆ BS be a finite set of possible observations (recall that observations are belief states). An observation model is a collection of functions

for every α ∈ ACTS and every s ∈ S, such that:

κOBS(obs|s, α) is the exceptionality degree of getting observation obs as feedback when executing the sensing action α in state s. This definition first appears in [Boutilier et al., 1998], and is similar in spirit to correlation probabilities between states and observations in partially observable Markov decision processes. Condition 1 expresses that there is always at least one normal observation; Condition 2 is a weak consistency condition between states and observations (an observation totally excluding a state cannot occur in that state).

Example 2

(all other observations being impossible, i.e., for obs ̸= obs1, obs2, κ(obs|s, α) = ∞; by convention we omit these when specifying κ(.|s, α)). This means that accurate observations are the normal ones, whereas incorrect obervations are 1-exceptional.

Definition 3 Let κ0 be a belief state and α ∈ ACTS. Given obs ∈ OBS, the plausibility of obtaining obs after α in belief state κ0 is defined by

The progression of κ0 by α is the complex belief state prog(κ0, α) = µ(.|κ0, α) defined by: for all κ ∈ BS,

Thus, κ is all the more normal in the projected CBS µ(.|κ0, α) as there exists a normal state s and a normal observation obs (given s) such that κ is the revision of κ0 by obs. Condition 2 in Definition 2 guarantees that κ0 ⊕ obs is defined whenever κOBS(obs|κ0, α) < ∞, which ensures that µ(.|κ0, α) is a CBS.

Example 3 The figure on the left (resp. right) shows the progression of κ0 (resp. κ1) by ask.

4.3 Progression by physical actions

In addition to sensing actions we consider a finite set ACTP of physical, feedback-free actions 4 . In Section 2, the progression of a belief state by a physical action was defined as a belief state. For the sake of homogeneity, we have now to define it as a CBS: the progression µ(.|κ0, α) of a belief state κ0 by α ∈ ACTP is defined by µ(.|κ0, α) = µκ0⋄α, i.e.,

4.4 Progression by belief-based programs

The progression of a belief state κ by a BBP π is the complex belief state µ(.|κ, π) defined inductively by

• if π = λ then µ(.|κ, π) = µκ;
• if π = α then µ(.|κ, π) is defined in Section 4.3 if α ∈ ACTP and in Section 4.2 if α ∈ ACTS;
• if π = (π1; π2) then µ(κ′ |κ, π) = minκ′′∈BS(µ(κ′′ |κ, π1) + µ(κ′ |κ′′ , π2))
• if π = if Φ then π1 else π2 then µ(κ′ |κ, π) = { µ(κ′ |κ, π1) if κ |= Φ µ(κ′ |κ, π2) otherwise
• if π = while Φ do π′ then µ(κ′ |κ, π) = { µ(κ′ |κ, (π′ ; π)) if κ |= Φ µκ(κ′ ) otherwise

If π contains no while construct then this definition is well-founded (it can be proved that it results a SBS which moreover does not depend on the order in which the above rules are applied). This is not so with while constructs, since the (recursive) definition leads to a fixpoint equation whose solution, when defined, is taken to be its least fixpoint when the latter is a CBS, which is not necessarily the case: consider κ0 = κ⊤ and π = while ⊤ do ask; applying the above definition leads to µ(κ|κ0, π) = ∞ for all κ, which is not a CBS. Moreover, when µ(.|κ0, π) is defined, it does not necessarily have a finite support.

Example 4

• µ(.|κ⊤, (ask; ask)) = [κ3 : 0 ; κ4 : 0 ; κ0 : 1];
• µ(.|κ⊤, (ask; ask; ask; ask)) = [κB4r : 0 ; κB4¬r : 0 ; κ3 : 1 ; κ4 : 1 ; κ0 : 2];
• π1 = (ask; ask; if B2r ∨B2¬r then λ else ask). Then µ(.|κ⊤, π1) = [κ3 : 0 ; κ4 : 0; κ1 : 1 ; κ2 : 1];
• π2 = while ¬(B2r ∨ B2¬r) do ask. Applying the definition gives a fixpoint equation whose solution is µ(.|κ0, π2) = [κ3 : 0 ; κ4 : 0]. 5

4 Such a partition between purely sensing and purely physical actions is usual and does not induce a loss of generality.

5 The question whether this program can run forever is similar to that of whether it is possible that a fair coin tossed repeatedly always turns up heads, and this is thus related to an OCF version of the law of large numbers.

4.5 Two particular cases

An unobservable environment consists of a set of physical actions only (ACTS = ∅).

A fully observable environment is somewhat harder to define formally because of the separation between physical and sensing actions, which prevents us to say that all actions send a full feedback. To cope with this, we assume that ACTS contains one action sense(x) for each propositional variable, which returns the truth value of x with full certainty, and we require that in a program, any physical action α should be followed by all actions sense(x) - which means that after α and this sequence of sensing actions, the state is known with full certainty. Any program of this kind is said to be admissible. The initial state is also required to be known with certainty.

Proposition 1

1. in an unobservable environment, for any κ0 and any program π for which µ(.|κ0, π) is defined, there exists a belief state κ such that µ(.|κ0, π) = µκ;
2. in a fully observable environment, for any belief state κ0 and any admissible program π such that µ(.|κ0, π) is defined, µ(κ|κ0, π) < ∞ implies that κ is a precise belief state, i.e., κ = κs for some s ∈ S.

5 Progression: syntactical computation

Applying progression as it is defined above has a prohibitive complexity, since it amounts at iterating over all belief states, states, and observations. In this Section we give a more friendly, syntactical way of computing progression, based on a compact representation of complex belief states.

So as to be able to reason about the resulting belief states, we now introduce a new family of modalities P1, P2, . . . , P∞ in addition to B1, . . . , B∞. While the Bi modalities deal with uncertainty (about the current state), P1 , P2, . . . , P∞ deal with second-order uncertainty, i.e., uncertainty about the projected belief state (with respect to some program).

L2PS is the language defined by:

• if Φ is a formula of LPS then for all i, PiΦ is a formula of L2PS ;
• if Θ and Θ′ are formulas of L2PS then Θ ∧ Θ′ , Θ ∨ Θ′ and ¬Θ are formulas of L2PS .

Like for Bi modalities, we need not consider nested Pi modalities, neither heterogeneous combinations of Pi and Bi modalities (resp. objective formulas). Satisfaction of a L2PS formula by a CBS is defined by

• µ |= PiΦ iff for all κ ∈ BS, κ |= ¬Φ implies µ(κ) ⩾ i;
• µ |= Θ∧Θ′ iff µ |= Θ and µ |= Θ′ (and similarly for the other connectives).

Validity, satisfiability and logical consequence are defined in the usual way. Intuitively, P1Φ means that all belief states that do not satisfy Φ are exceptional at least to the degree i.

When reasoning about CBS, we are mainly concerned with inferring positive formulas - inferring negative formulas such as ¬PiΦ is somewhat derivative. We define a positive L2PS formula as follows:

• if Φ is a positive LPS formula and i ∈ N then PiΦ is a positive L2PS formula;
• if Θ1 and Θ2 are positive L2PS formulas then Θ1 ∧ Θ2 and Θ1 ∨Θ2 is a positive L2PS formula.

Moreover, a canonical L2PS formula is a L2PS formula of the form Θ = P1Φ1 ∧ P2Φ2 ∧ . . . ∧ PnΦn ∧ P∞Φ∞, where Φ1, . . . , Φn, Φ∞ are positive LPS formulas 6 .

Given a CBS µ with finite support, the canonical L2PS formula G+(µ) = Θµ associated with µ is defined by

where n = nµ and G(κ) is the canonical LPS formula corresponding to κ (cf. Section 2).

Proposition 2 For any CBS µ with finite support and any positive conjunctive L2PS formula Θ, µ |= Θ if and only if Θµ |= Θ, that is, Θµ is the strongest positive conjunctive L2PS formula satisfied by µ.

Example 1 (continued)

We are now in position to give a syntactical characterization of progression.

Definition 4 Let Φ be a positive conjunctive LPS formula and α be any action. The progression of Φ by α is the canonical L2PS formula Prog(Φ, α) corresponding to the CBS µ(.|κΦ, α), i.e.,

We now show how the formula Prog(Φ, α) can be computed without first generating the corresponding µ.

Proposition 3

Let α be a sensing action and Φ = B1ϕ1 ∧. . .∧Bpϕp ∧B∞ϕ a positive conjunctive LPS formula. We define:

• for any obs ∈ OBS and i ∈ N, ψi,obs,α = Form{s ∈ S | µOBS(obs|s, α) < i};
• Xi,Φ,α = {obs ∈ OBS | (ϕ1 ∧ ψi,obs,α) ∨ . . . ∨ (ϕi ∧ ψ1,obs,α) ̸≡ ⊥};
• X∞,Φ,α = {obs ∈ OBS | ϕ ∧ ψ∞,obs,α ̸≡ ⊥};
• n is the largest integer i such that Xi,Φ,α ⊊X∞,Φ,α. Then

where ⊗ is the syntactical revision operator (Proposition 1 of [Laverny and Lang, 2004]), which satisfies Φ ⊗ Φobs = G(H(Φ) ⊕ obs).

6 Notice that canonical L2PS formulas are positive L2PS formulas in which there is no disjunction at the level of the Pi modalities (but disjunctions may appear in the scope of a Pi modality, and of course in the scope of a Bi modality too).

Example 2 (continued) Let Φ = B1r. We get X1,Φ,ask = {obs1}, X2,Φ,ask = {obs1, obs2} and for all n ⩾ 2, Xn,Φ,ask = {obs1, obs2}. Proposition 3 gives Prog(Φ, ask) = P1(B1r ⊗ B1r) ∧ P∞((B1r ⊗ B1r) ∨ (B1r ⊗ B1¬r)) ≡ P1B2r ∧ P∞(B2r ∨ B∞⊤) ≡ P1B2r.

The characterization for physical actions is much easier.

Proposition 4 For any physical action α and any PC LPS formula Φ, P rog(Φ, α) ≡ P∞G(κΦ ⋄ α).

Moreover, G(κΦ ⋄ α) can be computed efficiently using Proposition 2 of [Laverny and Lang, 2004].

Lastly, the progression of a positive conjunctive LPS formula Φ by a BBP π is the canonical L2PS formula P rog(Φ, π) defined inductively as follows:

• Prog(Φ, λ) = P∞Φ;
• Prog(Φ, α) is defined at Definition 4 if α is an action;
• Prog(Φ, if Ψ then π1 else π2) = { Prog(Φ, π1) if Φ |= Ψ Prog(Φ, π2) otherwise
• Prog(Φ, π1; π2) =

where

1. for any canonical L2PS formula Θ, [Θ]i is the strongest positive LPS formula Ψ (unique up to logical equivalence) such that Θ |= PiΨ .
2. for any positive conjunctive LPS formulas Φ1 and Φ2: [Prog(Φ1 ∨ Φ2, π)]i = [Prog(Φ1, π)]i ∨ [P rog(Φ2, π)]i .

Proposition 5 Prog(Φκ, π) = Θµ(.|κ,π)

Example 5

Let π = (ask; ask; if B2r ∨B2¬r then λ else ask) and π′ = (while ¬(B2r ∨B2¬r) do ask).

• Prog(B∞⊤, ask) ≡ P∞(B1r ∨ B1¬r)
• P rog(B∞⊤, ask; ask) ≡ P1(B2r ∨ B2¬r).
• Prog(B∞⊤, π) ≡ P1(B2r∨B2¬r)∧P∞(B1r∨B1¬r)
• Prog(B∞⊤, π′ ) ≡ P∞(B2r ∨ B2¬r)

6 Related work

Partially observable Markov decision processes

POMDPs are the dominant approach for acting under partial observability (including nondeterministic actions and unreliable observations). The relative plausibility of observations given states, as well as the notion of progressing a belief state by an action, has its natural counterparts in POMDPs. Now, there are two important differences between POMDPs and our work.

First, in POMDPs policies, branching is conditioned by the observation sequence that has lead to the current belief state; the policy is therefore directly implementable, without the need for an on-line reasoning phase. In our framework, branching conditions are expressed logically, which may allow for much more compact policies than branching on observations. In this view, BBPs can be seen as high-level, compact specifications of POMDP policies (the policy being the implementation of the program). Our work can thus be seen as a first step towards bridging knowledge-based programs and POMDPs.

Second, we allow for second-order uncertainty whereas POMDPs get rid of it: if pproj(p|p0, π) is the probability of obtaining the probabilistic belief state p after executing π in p0, this second-order belief state is systematically reduced into the first-order one ˆ p, following the lottery reduction principle: ˆ p(s) = ∑p∈PBS pproj(p).p(s) (where PBS is the set of probability distributions on S). This is a loss of expressivity, as seen on the following example: consider the action α of tossing a coin and the action β of sensing it. The agent knows that after performing α only, she will be for sure in a belief state where p(heads) = p(tails) = 0.5. This differs from projecting the effects of α; β: then she knows that he will reach either a belief state where she knows heads or a belief state where she knows tails, with equal probability. After reduction, these two plans and their projections can no longer be distinguished - whereas our CBS do distinguish them 7 .

Cognitive robotics

Another fairly close area is that of cognitive robotics, especially the work around Golog and the situation calculus (e.g., [Reiter, 2001]), which is concerned with logical specifications of actions and programs, including probabilistic extensions and partial observability. [Bacchus et al., 1999] gives an account for the dynamics of probabilistic belief states when perceiving noisy observations and performing physical actions with noisy effectors. [Grosskreutz and Lakemeyer, 2000] considers probabilistic Golog programs with partial observability, with the aim of turning off-line nondeterministic plans into programs that are guaranteed to reach the goal with some given probability. In both works, branching conditions involve objective formulas and there is no account for secondorder uncertainty. Bridging belief-based programs and the situation calculus (and Golog) is a promising issue.

Belief revision with unreliable observations

[Boutilier et al., 1998] might be the closest work to ours, as far as the dynamics of belief states in the presence of noisy observations is concerned. Our notion of an observation model (Definition 3) owes a lot to theirs (which also makes use of ranking functions). Now, their objectives depart from ours, as they focus on a general ontology for belief revision and do not consider physical actions nor programs, nor do they give a syntactical way of computing their revision functions.

7 Incidentally, we can reduce a CBS in a similar way: the reduction of the CBS µ of the is the belief state ˆκµ ∈ BS defined by ˆκµ(s) = minκ∈BS µ(κ)+κ(s). It is readily checked that ˆκ is a belief state. Reducing µ into ˆκµ results in a much simpler (and shorter) structure, which, on the other hand, is much less informative than µ.

Counterfactual belief-based programs

[Halpern and Moses, 2004] consider belief-based programs with counterfactuals whose semantics, like ours, is based on ranking functions. They do not allow for graded belief in branching conditions, nor unreliable observations (ranking functions are used for evaluating counterfactuals), but they allow for counterfactual branching conditions, possibly referring to future belief states, such as "if I believe that if I were not sending this message now then my partner might not get this important information, then I should send it". Adding counterfactuals and beliefs about future states to our framework is worth considering for further research.

Acknowledgements

Thanks to the anonymous referees for many relevant and helpful suggestions.