Multi-Agent Belief Base Revision

1 Introduction

Since the seminal work of Alchourr´on, G¨ardenfors and Makinson (AGM) [Alchourr´on et al., 1985], belief revision has been one of the central concepts in knowledge representation (KR). An important distinction in KR is between belief set (or theory) change and belief base change. While belief sets are deductively closed, belief bases may not be. This implies that belief sets are necessarily infinite since they contain all tautologies, whereas belief bases can be finite. Finiteness of belief bases offers an advantage for AI applications whereby autonomous agents (i.e., robots, embodied conversational agents) are conveniently described by the finite body of information in their databases. Existing formal theories of belief base change [Hansson, 1993; 1999; Benferhat et al., 2002] are mainly focused on the single-agent case and describe beliefs by propositional logic formulas.

In more recent times, there has been a growing interest in understanding and modelling belief change in the context of multi-agent systems. Epistemic logic (EL) [Fagin et al., 1995] and dynamic epistemic logic (DEL) [van Ditmarsch et al., 2007] have become the main tools for formalizing epistemic states (e.g., knowledge, belief) and their dynamics in a multi-agent setting. Some extensions of DEL by the notion of belief revision were proposed [van Benthem, 2007; Aucher, 2005; van Ditmarsch, 2005; Baltag and Smets, 2008]. DEL-based approaches to belief revision are based on Kripke semantics which assign to each agent a plausibility ordering (also called epistemic entrenchment ordering) on possible worlds, or a qualitative plausibility measure in the style of rank-based theory [Spohn, 1988] and possibility theory [Dubois and Prade, 1988]. The latter allow to capture minimal change in an agent's belief revision process. The problem of such semantics is that they are not compact thereby making model checking not exploitable in practice. Indeed, the epistemic model - with its possible worlds and agents' plausibility orderings - with respect to which a given property has to be checked is often huge and its correspondence with the informal description of the initial situation is not always immediate.

To overcome these limitations of DEL, we present a generalization of belief base revision to the multi-agent case. Unlike existing single-agent belief base revision approaches in which agents' beliefs are propositional, in our approach agents can have both propositional beliefs and higher-order beliefs about their own beliefs and other agents' beliefs. The idea of using belief bases as a semantics for multi-agent epistemic logic was put forth in [Lorini, 2018; 2020]. In this paper we enrich and expand this idea by the notion of belief revision. Our approach to multi-agent belief revision is more parsimonious than standard DEL-based approaches. Indeed, it only uses belief bases and no plausibility ordering or plausibility measure is needed. This provides an advantage for formal verification since the formulation of model checking in our approach is more compact than in existing DEL-based approaches using Kripke semantics. Compactness also has an impact on the representation of epistemic planning, namely, the generalization of classical planning in which the goal to be achieved is not necessarily a state of the world but some belief states of one or more agents. The initial proposal for epistemic planning was to use a standard logic of knowledge or belief together with a representation of actions in terms of event models of DEL [Bolander and Andersen, 2011; L¨owe et al., 2011]. Given the high expressivity of DEL, it turned out that checking existence of a solution plan becomes quickly undecidable [Bolander and Andersen, 2011; Aucher and Bolander, 2013; Lˆe Cong et al., 2018]. Epistemic planning with simple event models leading to a decidable fragment was studied by [Kominis and Geffner, 2015]. Moreover, decidable epistemic planning in a fragment of standard epistemic logic in which states are only described by conjunctions of epistemic literals (i.e., formulas that do not contain any conjunction or disjunction) and in a variant of epistemic logic based on the notion of observability was studied, respectively, by [Muise et al., 2015] and [Cooper et al., 2016]. The standard formulation of epistemic planning in DEL is based on model checking [Bolander et al., 2015]. This requires a full description of the initial epistemic model that, as emphasized above, is not well-suited for implementation and practical applications. On the contrary, our approach only requires to describe the agents' initial belief bases leading to a compact representation of epistemic planning in which epistemic actions are private belief revision operations.

Outline. Section 2 presents a modal language for modeling both explicit and implicit beliefs of multiple agents. While an agent's explicit belief is a piece of information in the agent's belief base, we call implicit belief a statement that can be inferred from the agent's explicit beliefs. The language has special operators for representing the consequences of an agent's private belief base revision operation. Section 3 presents the semantics exploiting belief bases with respect to which our language is interpreted. Taking inspiration from the notion of screened revision [Makinson, 1997] and, more generally from non-prioritized belief base revision [Hansson et al., 2001], we assume that an agent's belief base is split in two parts: the mutable part, whose elements may change under belief revision, and the core part, whose elements do not change. Sections 4 and 5 are devoted, respectively, to the formulation of model checking and epistemic planning in our setting and to the study and their complexities. In Section 6, we illustrate epistemic planning with the help of a concrete example.

2 Language

This section presents a language for representing agents' individual beliefs of both explicit and implicit type as well as the consequences of a private belief base revision operation on an agent's beliefs. An agent's explicit beliefs are of two types: core beliefs and mutable beliefs. Core beliefs are stable pieces of information in an agent's belief base that do not change under belief revision. On the contrary, mutable beliefs are volatile, they may change over time if they turn out to be inconsistent with what the agent perceives.

Assume a countably infinite set of atomic propositions Atm = {p, q, . . .} and a finite set of agents Agt = {1, . . . , n}. We define the language in two steps. First define the language L0 by:

where p ranges over Atm and i ranges over Agt. L0 is the language for representing explicit beliefs. The formula △ci α is read "agent i has the core belief that α", whereas △mi α is read "agent i has the mutable (or volatile) belief that α".We define the explicit belief operator △iα, read "agent i explicitly believes that α", as follows: △iα def = △ci α∨△mi α.

The language L extends L0 and is defined by:

where α ranges over L0 and i ranges over Agt. The other Boolean constructions ⊤, ⊥, ∨, → and ↔ are defined from α, ¬ and ∧ in the standard way.

The formula ✷ ci ϕ is read "ϕ is derivable from agent i's core beliefs", while ✷iϕ is read "ϕ is derivable from agent i's explicit beliefs". For simplicity, ✷iϕ is also read "agent i implicitly believes that ϕ".

We define the dual operators ✸ ci and ✸i as follows: ✸ ci ϕ def = ¬✷ ci ¬ϕ, and ✸iϕ def = ¬✷i¬ϕ. Formula ✸ ci ϕ has to be read "ϕ is compatible (or consistent) with agent i's core beliefs", whereas ✸iϕ has to be read "ϕ is compatible (or consistent) with agent i's explicit beliefs". The construction [∗iα]ϕ is read "ϕ holds after agent i has privately revised her belief base with α".

3 Semantics

In this section, we present a formal semantics for the language L exploiting belief bases. It refines the belief base semantics from [Lorini, 2020] by splitting an agent's belief base in two parts, the core and the mutable belief base. Unlike the standard Kripke semantics in which possible worlds and epistemic alternatives are primitive, they are here defined from the primitive concept of belief base.

Definition 1 (State). A state is a tuple B = ((Ci)i∈Agt , (Mi)i∈Agt ,V ) where Ci ⊆ L0 is agent i's core belief base, Mi ⊆ L0 is agent i's mutable belief base and V ⊆ Atm is the actual environment. The set of all states is denoted by S.

The following definition specifies truth conditions for formulas in the sublanguage L0.

Definition 2 (Satisfaction relation). Let B = ((Ci)i∈Agt , (Mi)i∈Agt , V ) ∈ S. Then,

Observe in particular the set-theoretic interpretation of the explicit belief operators in the previous definition: agent i has the core (resp. mutable) belief that α if and only if α is included in her core (resp. mutable) belief base.

Given β ∈ L0, we define S(β) = {B ∈ S : B |= β}. S(β) is the set of states induced by the integrity constraint β. This constraint limits the set of states with respect to which formulas are evaluated. Conceptually, it captures the information in the agents common ground, that is, the body of information that the agents commonly believe to be the case [Stalnaker, 2002].

We are interested in a specific subclass of states in which agents' belief bases are consistent.

Definition 3 (Belief consistent state). Let B = ((Ci)i∈Agt , (Mi)i∈Agt ,V ) ∈ S and β ∈ L0. The state B is said to be β-belief consistent (BCβ) if and only if ||Bi||S(β) ̸= ∅ for every i ∈ Agt, where ||X||S(β) = {B′ ∈ S(β) : ∀α ∈ X,B′ |= α} for each X ⊆ L0 and Bi = Ci ∪ Mi. The set of all β-belief consistent states is denoted by SBCβ .

The set ||X||S(β) in the previous definition is called X's truth set under the integrity constraint β.

Note that Definition 3 can be formulated in terms of propositional consistency. To see this, let LPROP be the propositional language built from the set of atomic formulas Atm+ = Atm ∪ {pci,α, pmi,α : i ∈ Agt and α ∈ L0} and let tr be the following translation fromL0 to LPROP:

For each X ⊆ L0, we define tr(X) = {tr(α) : α ∈ X}. Moreover, we say that X is propositionally consistent if and only if ⊥ ̸∈ Cn (tr(X)), where Cn is the classical deductive closure operator over the propositional language LPROP. The following holds.

Proposition 1. Let X ⊆ L0 and β ∈ L0. Then, ||X||S(β) ̸= ∅ if and only if tr(X ∪ {β}) is propositionally consistent.

Proof. Let W be the set of all valuations for the propositional language LPROP. There exists a bijection f : W -→ S such that f(w) |= α iff w |= tr(α), for all w ∈ W and α ∈ L0. Propositional consistency of tr(X ∪ {β}) means that we can find a valuation w ∈ W where all formulas in tr (X ∪ {β}) hold. Thus, there exists B′ ∈ S(β) such that f(w) = B′ and B′ |= β′ for all β′ ∈ X. The left-to-right direction can be proved in an analogous way.

By the previous proposition, the notion of belief consistent state can be defined in an equivalent way by replacing ||Bi||S(β) ̸= ∅ with ⊥ ̸∈ Cn (tr (Bi ∪ {β})) in Definition 3.

We denote by MCS(α,X,Y ,β) the set of maximally Y - consistent subsets of the set X of L0-formulas including α under the integrity constraint β. The definition will be used at a later stage to precisely define the interpretation of the belief revision operator.

Definition 4. Let X, Y ⊆ L0 and α ∈ L0. Then, X′ ∈ MCS(α,X,Y ,β) if and only if:

• X′ ⊆ X ∪ {α},
• α ∈ X′ ,
• ||X′ ∪ Y ||S(β) ̸= ∅, and
• there is noX′′ withX′⊂X′′⊆X and ||X′′ ∪Y ||S(β)̸=∅.

By Proposition 1, the set MCS(α,X,Y ,β) can be defined in an equivalent way by replacing ||X′ ∪ Y ||S(β) ̸= ∅ by ⊥ ̸∈ Cn (tr(X′ ∪ Y ∪ {β})) in the third item and ||X′′ ∪ Y ||S(β) ̸= ∅ by ⊥ ̸∈ Cn (tr(X′′ ∪ Y ∪ {β})) in the fourth item of Definition 4.

The following definition introduces the concept of epistemic alternative.

Definition 5 (Epistemic alternatives). Let i ∈ Agt. Then, Ri and Rci are the binary relations on the set of states S such that, for all B = ((Ci)i∈Agt , (Mi)i∈Agt ,V ),B′ = ((C ′ i )i∈Agt , (M ′ i )i∈Agt , V ′ ) ∈ S:

BRiB′ if and only if ∀α ∈ Bi : B′ |= α, where we recall that Bi = Ci ∪Mi is agent i's belief base.

BRci B′ means that B′ is an epistemic alternative relative to agent i's core beliefs at B, while BRiB′ means that B′ is an epistemic alternative relative to agent i's whole belief base at B. The idea of the previous definitions is that an agent's epistemic alternative is computed from the information in her belief base. Clearly, we have Ri ⊆ Rci since the core belief base is contained in the whole belief base.

The following definition specifies the interpretation of formulas in L. They are interpreted with respect to pairs (B, β) with B ∈ S the actual state and β ∈ L0 the integrity constraint. (We omit Boolean cases, defined in the usual way.)

Definition 6 (Satisfaction relation). Let B = ((Ci)i∈Agt , (Mi)i∈Agt , V ) ∈ S and β ∈ L0. Then:

where B |= α is defined as in Definition 1 and

As the previous definition highlights, agent i implicitly believes that ϕ if and only if ϕ holds in all agent i's epistemic alternatives that are compatible with the integrity constraint β. Since the latter are computed from agent i's belief base, the implicit belief operator ✷i captures the information that is deducible from the information in agent i's belief base under the integrity constraint β. Similarly, the operator ✷ ci captures the information that is derivable from agent i's core beliefs under the integrity constraint β.

The interpretation of the belief revision operator [∗iα] is based on state update. Specifically, the result of the private belief revision operation ∗iα occurring in the state B under the integrity constraint β is the updated state rev(B,i,α,β) in which (i) core belief bases or mutable belief bases of the agents different from i are not modified, and (ii) the input α is added to agent i's mutable belief base only if it is consistent with agent i's core beliefs and the integrity constraint. If the latter is the case, then agent i's updated mutable belief base is equal to the intersection of the subsets of agent i's mutable belief base which are maximally consistent with respect to agent i's core belief base under the integrity constraint and which include the input α. This belief revision operation can be conceived as a generalization of the notion of screened revision [Makinson, 1997] to the multi-agent case. Note that instead of taking the intersection of all maximally consistent subsets (MCSs) of the initial belief base, we could have taken a selection of them, e.g., only MCSs whose cardinality is maximal. This parallels the distinction between full meet and partial meet revision in the belief revision literature [Alchourr´on et al., 1985]. This would have had no impact on the complexity results presented below in Sections 4 and 5.

As the following proposition indicates, the belief revision operation ∗iα is well-defined as it preserves belief consistency.

Proposition 2. Let i ∈ Agt, α, β ∈ L0 and B ∈ SBCβ . Then, rev(B,i,α,β) ∈ SBCβ .

We conclude this section by defining the notions of βvalidity (viz. validity under the integrity constraint β).

Definition 7 (β-Validity). Let ϕ ∈ L and β ∈ L0. We say that ϕ is β-valid, noted |=β ϕ, if and only if, for every B ∈ SBCβ we have (B, β) |= ϕ. We say that ϕ is β-satisfiable if and only if ¬ϕ is not β-valid.

Some interesting validities are listed in the following two propositions.

Proposition 3. Let i, j ∈ Agt and β ∈ L0. Then,

As item (1) indicates, the implicit belief and belief revision operators are closed under necessitation. According to validity (2), if a formula is derivable from an agent's core beliefs, then it is also derivable from the agent's whole belief base. According to validity (3), an agent's belief base must be consistent. This is guaranteed by the fact that the notion of validity of Definition 7 is defined relative to β-belief consistent states. Validity (4) is a consequence of Proposition 2: an agent's belief base remains consistent after the occurrence of a private belief revision operation.

Proposition 4. Let i, j ∈ Agt, x ∈ {c,m} and β ∈ L0. Then,

Validity (5) expresses a form of success postulate: α is consistent with an agent's core belief base if and only if, after revising her beliefs with α, α is included in the agent's mutable belief base. Validities (6) and (7) just mean that core beliefs do not change as a consequence of belief revision. Moreover, since a belief revision operation is private, it only modifies the mutable beliefs of the agent who performs it. Finally, according to validity (8), if the input of belief revision is already consistent with an agent's belief base, then no mutable belief is removed from the agent's belief base. This means that the agent merely expands her belief base without contracting it.

4 Model Checking

The following is a compact formulation of the model checking problem for the language L. In the formulation of model

procedure mc(B, ϕ) match ϕ do case p: return B |= p case △ci α: return α ∈ Ci case △mi α: return α ∈ Mi case ¬ψ: return not mc(B, ψ) case ψ1 ∧ψ2: return mc(B, ψ1) and mc(B, ψ2) case ✷ cGψ: for all B′ ∈ S(β) such that BRci B′ do if not mc(B′ , ψ) return false case ✷Gψ: for all B′ ∈ S(β) such that BRiB′ do if not mc(B′ , ψ) return false return true case [∗iα]ψ: returnmc(rev(B,i,α,β), ψ)

checking we have to suppose B ∈ SBCβ . This guarantees that agents' beliefs are consistent in the actual state.

where the state B = ((Ci)i∈Agt , (Mi)i∈Agt , V ) is said to be finite if V , every Ci and every Mi are finite.

Following [Lorini, 2019], we can prove the following lower bound for our model checking problem.

Theorem 1. Model checking with integrity constraint is PSPACE-hard.

In the rest of this section, we explain that the model checking problem is in PSPACE.

Algorithm 1 sums up the algorithm for the model checking of a formula ϕ in a given finite state B ∈ SBCβ (we check that B ∈ SBCβ with propositional consistency checking; if B ̸∈ SBCβ then the input is not correct). The first three cases are base cases. The next two cases are for Boolean connectives. For the ✷ ci ψ and ✷iψ cases, we enumerate all possible states B′ containing correct subformulas of formulas in the initial B and in the initial formula ϕ. Remark that the current B′ only takes a polynomial amount of space. Checking BRci B′ or BRiB′ can be performed in polynomial time. Finally, the last case is the revision case. It remains to show that ⋂X∈MCS(α,Mi,Ci,β) X can be computed in polynomial space. To this end, we will consider all formulas and, for each of them, we check that it is in all subsets in MCS(α,Mi,Ci,β). To this aim, we explain how MCS(α,Mi,Ci,β) can be enumerated in polynomial space. To do that, we enumerate all X′ ⊆ X ∪ {α} containing α. Then, we check that X′ ∪ Y ∪ {β} is propositionally consistent. We also check that any superset X′′ of X′ containing just one extra formula is such that X′′ ∪ Y ∪ {β} is inconsistent. As propositional consistency is in NP, the overall computation is in polynomial space.

As the depth of nested calls in mc(B, ϕ) is bounded by the size of ϕ, we obtain the PSPACE membership.

Theorem 2. Model checking with integrity constraint is in PSPACE.

5 Epistemic Planning

In this section, we first consider one of the simplest epistemic planning problem, where actions are revision operators equipped with preconditions: (ϕ, [∗iα]) where ϕ ∈ L is a precondition, i is an agent and α ∈ L0. The reader may easily imagine natural extensions in which actions could have ontic effects. For conveying the main idea of our approach, we keep the presentation as simple as possible, we stick to the following refined version of epistemic planning.

A plan is a linear sequence of elements (ψ, [∗iα]) with ψ ∈ L, i ∈ AGT and α ∈ L0. We define the formula 〈π〉ϕ by induction: 〈ϵ〉ϕ = ϕ, and 〈(ψ, [∗iα])π〉ϕ = ψ ∧ [∗iα]〈π〉ϕ.

Epistemic planning

Given: ϕ ∈ L, β ∈ L0, a finite B ∈ SBCβ , and a finite subset A of elements (ψ, [∗iα]) with ψ ∈ L, i ∈ AGT and α ∈ L0.

Question: Does there exist a finite sequence π of elements in A such that (B, β) |= 〈π〉ϕ?

Given how our framework is settled, the epistemic planning is not more difficult than classical planning (STRIPS for instance).

Theorem 3. Epistemic planning is in PSPACE.

Proof. Consider the following graph. Nodes are states. Edges are transitions from a state B′ to rev(B′ ,i,α,β) for some action (ψ, [∗iα]) in A and ψ holds in B′ . That graph is of exponential size since we restrict formulas in bases to be subformulas of ϕ, β, subformulas of formulas appearing in B and formulas occurring in the repertoire A. Solving an epistemic planning instance reduces to reachability in that graph from the initial state B to a final state satisfying ϕ. We solve that reachability problem as follows. We store the current state starting from B. At each step, we non-deterministically choose the next action (ψ, [∗iα]) to execute. We check that ψ holds in the current state and compute the next state. The algorithm accepts when the goal ϕ holds in the current base. As the model checking is in PSPACE, our algorithm is nondeterministic in polynomial space. We conclude by Savitch's theorem [Savitch, 1970].

Our actions modify the current state and then modify possible worlds implicitly (because possible worlds are computed from the current state). On the contrary, in the epistemic planning based on Dynamic Epistemic Logic (DEL) [Bolander et al., 2020], actions explicitly modify possible worlds. DEL allows for very complex actions and the DEL planning problem is undecidable. Our framework has the advantage of being very close to classical planning.

We conclude this section by considering the following variant of epistemic planning, called uniform epistemic planning, in which we enforce an agent i to know that the plan is successful. In particular, uniform epistemic planning consists in checking whether agent i knows how to achieve a certain goal ϕ through the execution of a plan.

Uniform epistemic planning

Given: ϕ ∈ L, β ∈ L0, a finite B ∈ SBCβ , an agent i ∈ AGT, and a finite subset A of elements (ψ, [∗iα]) with ψ ∈ L, i ∈ AGT and α ∈ L0

Question: Does there exist a finite sequence π of elements in A such that (B, β) |= ✷i〈π〉ϕ?

Theorem 4. Uniform epistemic planning is in EXPSPACE.

Proof. We now consider the graph whose nodes are information sets (sets of states) for agent i. There is an edge from I to I ′ if there is an action (ψ, [∗iα]) in A such ψ holds in all states in I and I ′ is the set of states rev(B′ ,i,α,β) where B′ in I. Now, we ask for a path in that graph from the set of possible states for agent i in B to a set of states all satisfying ϕ. As the graph is doubly-exponential, uniform epistemic planning is in NEXPSPACE = EXPSPACE.

6 Example

We illustrate the planning problem defined in the previous section with the help of a concrete example. Let Agt = {iA, iB, iC, iM}. The four agents Ann (iA), Bob (iB), Charles (iC) and Mary (iM) are mobile robots meeting at a roundabout. Each robot has to decide at which moment it will pass. In order to avoid a collision, the robots have to pass sequentially one after the other. We assume an external planning agent is connected to each robot in the system. Its aim is to assign to each robot a priority level from the set of priority levels Lev = {1, . . . , 4} in such a way that a collision is avoided. Each priority level specifies a time in the sequence at which a robot has to pass. We assume that the set Atm includes three types of atomic formulas pri,k, pai,k and oughti,k for every i ∈ Agt and k ∈ Lev. They have to be read, respectively, "priority level k is assigned to robot i", "robot i will pass at time k" and "robot i ought to pass at time k". Following reductionist theories of intention [Sellars, 1968] according to which an intention is reducible to a firstperson normative judgment about what one shall/ought to do, we introduce the following abbreviation:

where intendi,k is read "agent i intends to pass at time k".

We assume the following three pieces of information are part of the robots' common ground, that is, they constitute the integrity constraint of the planning problem under consideration:

According to α1, a robot will pass at a certain time k only if it explicitly believes that it has priority level k. According to α2, two different priority levels cannot be assigned to the same robot. According to α3, a robot cannot believe that two different priority levels were assigned to it. Constraints α2

and α3 presuppose that the external planning agent can assign at most one priority level to one robot.

We suppose each robot i has the following piece of information αi in its core belief base:

Formula αi specifies what a robot should do depending on its priority level and the other robots' priority levels. Specifically, if k is the only priority level which was assigned to robot i and no other robot has the same priority level, then robot i ought to pass at time k. To conclude, we suppose that each robot egocentrically believes that it has priority level 1, thereby being authorized to pass before the others. Specifically, for every robot i we assume pri,1 is the only piece of information in its mutable belief base. Moreover, the priority levels have been assigned in the following way but have not been communicated yet to the robots: Mary should pass first,followed by Bob, then Ann, and Charles as last.

To sum up, we define the actual state B = ((Ci)i∈Agt , (Mi)i∈Agt ,V ) as follows: (i) for every i ∈ Agt, Ci = {αi} and Mi = {pri,1}, and (ii) V = {pr iM,1, pr iB,2, pr iA,3, pr iC,4, ought iM,1, ought iB,2, ought iA,3, oughtiC,4}. The definition of V presupposes that in the initial situation the robots have not decided yet at which time to pass since the priority levels have not been communicated to them. The goal ϕG is to ensure that (i) each robot forms an intention to pass at certain time, and (ii) there are no two different robots with the same intention (i.e., the intention to pass at the same time). The latter condition is necessary to prevent the robots from colliding. Formally,

In order to achieve this goal, the external planning agent can (i) inform a robot that a certain priority level is assigned to it, and (ii) inform a robot that another robot has been informed that a certain priority level is assigned to it. We assume that informative actions of the planning agent are truthful, i.e., a robot can be informed that a certain fact is true only if the fact is indeed true. Thus, the repertoire of actions of the planning agent is defined as follows:

It is routine exercise to verify that the following plan

is a solution of our epistemic planning problem. Indeed, we have (B, α1 ∧ α2 ∧ α3) |= 〈π〉ϕG. The plan just consists in sequentially informing the robots about their priority levels and then sequentially informing the robots that the others have been informed about their priority levels.

7 Conclusion

We proposed a multi-agent framework that encompasses explicit/implicit beliefs and private belief revision. Our syntactic approach has strong advantages compared to the traditional semantic approaches based on Kripke structures. First, whereas Kripke structures are typically exponential in the number of atomic propositions, our syntactic representation with belief bases scales up in general. Secondly, the syntactic approach enables to elegantly define revision operators, compared to existing approaches which use cumbersome plausibility orderings or plausibility measures on possible worlds [van Benthem, 2007; Aucher, 2005; van Ditmarsch, 2005; Baltag and Smets, 2008]. Thirdly, the distinction between explicit/implicit beliefs comes for free in our approach. Fourthly, our model checking problem is in PSPACE, and that gives a hope of having reasonably efficient implementations of both the model checking and the epistemic planning problem, whereas epistemic planning in DEL is undecidable.

Perspectives of future work are manifold. Our framework can easily be adapted to capture introspective agents who have perfect knowledge of their own core and mutable belief base. To this aim, Definition 5 of epistemic alternative should be tuned as follows:

The binary relations Rci and Ri so defined are transitive and Euclidean. Interestingly, unlike DEL in which introspection over beliefs could be lost due to private belief change, in our approach it is necessarily preserved. Indeed, the agents' epistemic accessibility relations are recomputed from belief bases after the occurrence of a private belief revision operation. For this introspective variant, the model checking and epistemic planning remain in PSPACE. Future work will be devoted to an in-depth analysis of the logical properties of belief base revision in the case of introspective agents. Another direction of future work is to move beyond private belief base revision and to explore semi-private forms (e.g., an agent i sees that α while another agent j sees that i sees that α, but i is not aware of this). Last but not least, we plan to compare the expressivity of existing DEL-based approaches to belief revision and the expressivity of our belief base approach.

Acknowledgments

This work is partially supported by the EU ICT-48 2020 project TAILOR (No. 952215) and the ANR project CoPains ("Cognitive Planning in Persuasive Multimodal Communication"). Support from the ANR-3IA Artificial and Natural Intelligence Toulouse Institute is also acknowledged.