Consistent update synthesis via privatized beliefs

Epistemic logic (EL)^[1] has been extremely successful in modeling epistemic and doxastic attitudes of agents and groups in multi-agent systems, including distributed systems^[2]. Dynamic epistemic logic (DEL)^[3,4] upgrades EL by introducing model-transforming modalities called updates. Relational structures such as action models in Action Model Logic (AML) and arrow update models in the Generalized Arrow Update Logic (GAUL)^[5] are used to represent the evolution of agents' uncertainty under information change in complex communication scenarios. GAUL and AML have proved to be equally update expressive^[6]. Thus, without loss of generality, we use the term 'update models' to refer to either action models of AML or arrow update models of GAUL. In the update synthesis task, the aim is to (i) find whether there exists an update model that makes a given goal formula $ \varphi $ true and (ii) construct that update model from $ \varphi $^[6]. Because the desiderata for this goal are so strong, there is no general guarantee that such synthesis is always possible. For example, in standard public announcement logic^[4] and in arrow update logic^[7] it is not possible in general. However, Hales^[8] proved that it is possible for AML. While it is possible to construct AML or GAUL update models representing completely private communication^[9] (Fig. 2), there is no standardized update synthesis procedure for it.

Our paper is further motivated by two different yet intertwined issues:

● As argued by Artemov^[10], in multi-agent settings, common knowledge of the model (CKM) is required by agents in order to compute higher-order beliefs of other agents. While his argument focuses on uncertainties about facts, it can also be extended to agents' uncertainty about attitudes of other agents. The underlying problem is that, in multi-agent Kripke models, there is an implicit ontological distinction between two kinds of possible worlds: (a) worlds that are actually possible (AP); and (b) worlds that are only virtually possible (VP). While the former worlds constitute, for a given agent, the arena in which the actual world might lie, the latter kind of worlds are considered only to the extent of computing other agents' beliefs. Artemov argues that without the CKM (comprising both APs and VPs), agents would not be able to compute such higher-order beliefs. Furthermore, avoiding the CKM assumption improves tolerance against local state corruption: upon receiving corrupted information from a faulty agent, a (correct) agent might only deem the local state of the sender as corrupted, instead of being forced to consider a larger part of the accessible Kripke model inconsistent.

● Update models do not naturally represent private agent-to-agent communication, as the product update operation typical of DEL is applied in principle to the full product of all the world-event pairs whose preconditions are matched^[4]. In this sense, these updates are applied globally to the whole model, potentially leading to information leakage. The problem is also identified by Herzig, as 'it is not easy to come up with a meaningful notion of a speaker'^[11], highlighting the fact that local communication might have (undesired) effects on a global model.

Our solution to both issues is to change the structure of the Kripke models under consideration. While Artemov proposes to avoid the CKM by changing the definition of truth for knowledge^[10], we instead suggest a stratified Kripke model structure (more precisely, the kind of structures that will be introduced for privatization are directed acyclic graphs.), without changing any basic definitions: by stratifying a Kripke model into a pointed privatized Kripke model we detach each agent's view of the model from any other agent's view of it. In our stratified models, not only do we clearly distinguish between APs and VPs for any agent, but we also avoid the CKM assumption by letting each agent access only a limited and private part of it (a formal definition of privatization is provided in Section 4), without losing the ability to reason about higher-order beliefs of other agents of arbitrary depths. At the same time, while we do not solve the broader issue of agency identified by Herzig, we propose an alternative update operation called pointed updates, which does not apply to the full product of the Kripke model and the action model. In particular, we exploit the novel stratification method (and the distinction between APs and VPs) to discern when to form a world-event tuple and when not. In this sense, our updates are not applied to the whole model, as they are progressively applied only to those worlds that match a certain structure (other than a certain precondition). The proposed stratified structure complies with the crucial notion of a local view of an agent, typical of distributed systems, which is only a limited portion of the global view of the system, usually inaccessible to agents. The stratification not only represents the idea of each agent having a partial view of a Kripke model, but also distinguishes the actual world from any other worlds, by making it inaccessible. In other words, we endorse a fallibilistic assumption, that is, no agent can be sure that the global state of the system is captured in their limited view of it. Naturally, agents might have an accurate view of the system during execution, represented in our model by worlds propositionally equivalent to the actual world that are, however, accessible only in agents' (respective) private clusters.

The aim of this paper is to provide a novel action model synthesis mechanism for AML designed for enforcing private beliefs specified by a quantifier-free goal formula while preserving the consistency of agents' beliefs whenever possible. Our solution to the leak-free, consistent update synthesis task accounts for a limited range of goal formulas, restricted to deterministic belief increase only, i.e., to conjunctions of (positive) modal operators. This limitation is due to the fact that preserving minimality and consistency becomes highly problematic for unrestricted goal formulas: on the one hand, negations of belief operators might introduce ignorance, potentially contradicting previously held beliefs. On the other hand, disjunctions of modal operators have multiple realizations, making the update non-deterministic. Addressing the remaining cases (and their interactions) is left for future work.

Finally, the proposed update mechanism is generally more efficient with respect to AML and GAUL updates as it deletes all states not reachable from the actual world, making the growth in size of the model at worst linear in the size of the goal formula after one update and decreasing starting from the second update based on the same modal syntactic tree. By contrast, it is well known that repeated applications of AML and GAUL updates lead to the exponential growth of the model. It is also known that the model checking problem is PSPACE-complete^[12].

A prominent approach for dealing dynamically with beliefs in Kripke terms is the Dynamic Belief Revision^[13,14], where agents' conditional beliefs are expressed via a plausibility relation ranging over virtual states. This account, however, cannot represent truly private updates, as its models encode both plausibility and epistemic relations that would be revealed by the CKM assumption. In recent years, different answers to the limitations of the CKM assumption in the standard semantics for EL and DEL have been proposed, for example by changing accessibility relations^[10] or by using belief bases as primitives^[15,16]. Our approach, on the other hand, performs private, leakage-free consistent synthesis by structuring standard Kripke models into exclusively accessible parts that are not known to other agents, let alone commonly known.

Existing synthesis methods typically work in a language extended with quantifiers over updates, such as the Arbitrary Action Modal Logic^[8] and Arbitrary Arrow Update Modal Logic^[6]. While quantification over updates allows us to express the synthesis operation within the logical language, a major shortcoming, however, in particular with respect to the applications for distributed systems is that these update operations do not focus on issues of privatization and of minimal change. In addition, most existing synthesis methods do not address belief consistency preservation^[6].

We start by giving a motivating example in Section 2, as well as introducing the basic definitions of DEL and the crucial new definition of pointed update. In Section 3 we propose a solution to the leak-free consistent update synthesis for a limited range of goal formulas and we show its fruitfulness by applying it to our motivating example. In Section 4, we illustrate the properties of the synthesized action models, in particular with respect to privatization properties, crucial for avoiding information leakage while preserving consistency. Finally, conclusions are provided in Section 5.

We use the standard doxastic multimodal language $ \mathfrak{L} $:

where $ i \in {\cal{A}}=\{1,\dots,n\} $ (for $ n>1 $) and $ p \in {Prop} $, where $ {Prop} $ is the set of propositional atoms. Formula $ B_i \varphi $ means agent $ i $ believes $ \varphi $ (to be true). The other Boolean connectives are defined as usual and $ \hat{B}_i := \lnot B_i \lnot $ representing the dual modality considers possible.

Definition 1 (Kripke frame) A Kripke frame for the set of agents $ {\cal{A}} $ is a pair $ \langle W, R\rangle $ where $ W \ne \varnothing $ is a non-empty set, called domain and $ R = (R_1, \ldots, R_n) $ consists of binary accessibility relations $ R_i \subseteq W \times W $.

Unless specified otherwise, we assume $ {\cal{KD}}45 $, which is the class of frames that satisfy:

● transitivity: if $ uR_i v $ and $ vR_i w $ then $ uR_i w $.

● euclideanity: if $ uR_i v $ and $ uR_i w $ then $ vR_i w $.

● seriality: every state has an outgoing arrow for every $ i \in {\cal{A}} $.

These three frame properties correspond to the following axioms^[17]:

● transitivity $ \Leftrightarrow $ $ B_i \varphi \rightarrow B_iB_i \varphi $.

● euclideanity $ \Leftrightarrow $ $ \neg B_i \varphi \rightarrow B_i \neg B_i \varphi $.

● seriality $ \Leftrightarrow $ $ B_i \varphi \rightarrow \hat{B}_i \varphi $.

Note that we generally do not assume the factivity of beliefs ($ B_i \varphi \rightarrow \varphi $), which in terms of frame properties corresponds to reflexivity ($ u R_i u $).

We introduce the standard definitions of DEL^[4]:

Definition 2 (Pointed Kripke model) For a set of agents $ {\cal{A}} $, a Kripke model is a triple $ {\cal{M}} = \langle S, R, V\rangle $ where $ \langle S, R\rangle $ is a Kripke frame with domain $ S $ consisting of possible worlds or states, and the valuation function $ V \colon {Prop} \to 2^S $ determines the set $ V(p)\subseteq S $ of possible worlds where an atom $ p \in {Prop} $ is true. A pointed Kripke model is a pair $ ({\cal{M}},w) $ where $ w \in S $ represents the actual world/state.

Truth at world $ w $ of model $ {\cal{M}} $ is determined by $ {\cal{M}}, w \vDash p $ iff $ w \in V(p) $. Boolean connectives are defined as usual. $ {\cal{M}}, w \vDash B_i \varphi $ iff $ {\cal{M}}, w' \vDash \varphi $ for all $ w'\in S $ such that $ w R_i w' $. A formula $ \varphi $ is false at world $ w $, $ {\cal{M}},w \nvDash \varphi $, iff it is not true at $ w $.

Definition 3 (Pointed action model) For a set of agents $ {\cal{A}} $, an action model is a triple $ {\cal{U}} = \langle E, Q, \text{pre} \rangle $ where $ \langle E, Q\rangle $ is a Kripke frame with domain $ E $ consisting of actions or events, and the precondition function $ \text{pre}: E \rightarrow {\cal{L}} $ assigns the precondition $ \text{pre}(\beta)\in {\cal{L}} $ that is necessary for an event $ \beta \in E $ to happen. A pointed action model is a pair $ ({\cal{U}},\alpha) $ where $ \alpha \in E $ represents the actual event/action.

Definition 4 (Product update) The (restricted modal) product update of a Kripke model $ {\cal{M}} = \langle S,R,V \rangle $ with an action model $ {\cal{U}} = \langle E, Q, \text{pre} \rangle $ is a Kripke model $ {\cal{M}} \otimes {\cal{U}} := \langle S',R',V' \rangle $ where

● $ S' := \{(v, \beta) \in S \times E \mid {\cal{M}}, v \vDash \text{pre}(\beta) \} $,

● $ R'_i := \left\{\bigl((v, \beta),(u, \gamma)\bigr)\in S'\times S' \mid (v, u) \in R_i \text{ and } (\beta, \gamma) \in Q_i\right\} $,

● $ V'(p) := \{(v, \beta) \in S' \mid v \in V(p)\} $.

If $ S' = \varnothing $, the product update is undefined.

A product update provides the semantics for a communication scenario represented by a pointed action model $ ({\cal{U}},\alpha) $: formula $ \varphi $ is true after the communication $ {\cal{U}} $, i.e., $ {\cal{M}}, w \vDash [{\cal{U}},\alpha] \varphi $, iff $ {\cal{M}} \otimes {\cal{U}}, (w,\alpha) \vDash \varphi $ or $ (w,\alpha) \notin S' $.

Definition 5 (Bisimulation [Kripke frames and Kripke models]) A bisimulation between Kripke frames $ \langle W, R\rangle $ and $ \langle W', R'\rangle $ is a nonempty binary relation ${ \cal{B}} \subseteq W \times W' $, such that for every $ v {\cal{B}} v' $ and $ i \in {\cal{A}} $:

● Forth: if $ v R_i u $, then there is $ u'\in S' $ such that $ v' R_i'u' $ and $ u {\cal{B}} u' $;

● Back: if $ v' R_i' u' $, then there is $ u \in S $ such that $ v R_i u $ and $ u {\cal{B}} u' $.

A bisimulation between Kripke models $ {\cal{M}}=\langle S, R,V\rangle $ and $ {\cal{M}}'=\langle S', R',V'\rangle $ is a bisimulation $ {\cal{B}}\subseteq S \times S' $ between their frames $ \langle S, R\rangle $ and $ \langle S', R'\rangle $ that additionally satisfies for every $ v {\cal{B}} v' $ and $ p \in {Prop} $:

● Atoms: $ v \in V(p) $ iff $ v' \in V'(p) $.

Similarly a bisimulation between action models $ {\cal{U}}=\langle E, Q, \text{pre}\rangle $ and $ {\cal{U}}'=\langle E', Q', \text{pre}'\rangle $ is a bisimulation $ {\cal{B}}\subseteq E \times E' $ between their frames $ \langle E, Q\rangle $ and $ \langle E',Q'\rangle $ that additionally satisfies for every $ \alpha {\cal{B}} \alpha' $:

● Pre: $ \text{pre}(\alpha) = \text{pre}'(\alpha') $.

Two pointed Kripke models $ ({\cal{M}}, v) $ and $ ({\cal{M}}', v') $ (respectively pointed action models $ ({\cal{U}}, \alpha) $ and $ ({\cal{U}}', \alpha') $) are bisimilar denoted $ {\cal{M}}, v\underline{\leftrightarrow} {\cal{M}}', v' $ (resp. $ {\cal{U}}, \alpha\underline{\leftrightarrow} {\cal{U}}', \alpha' $), iff there exists a bisimulation $ {\cal{B}} $ between $ {\cal{M}} $ and $ {\cal{M}}' $ (resp. $ {\cal{U}} $ and $ {\cal{U}}' $) s.t. $ v {\cal{B}} v' $ (resp. $ \alpha {\cal{B}} \alpha' $).

Definition 6 (Modal Equivalence) Pointed Kripke models $ ({\cal{M}}, v) $ and $ ({\cal{M}}', v') $ are called modally equivalent, notation $ {\cal{M}}, v \equiv {\cal{M}}', v' $, whenever $ {\cal{M}}, v \vDash \varphi $ iff $ {\cal{M}}', v' \vDash \varphi $ for all formulas $ \varphi $.

Theorem 7: (Bisimilarity implies modal equivalence^[18]) If $ {\cal{M}}, v\underline{\leftrightarrow} {\cal{M}}', v' $, then $ {\cal{M}}, v\equiv {\cal{M}}', v' $.

2.1.   Motivational example

We illustrate our objective by means of the following example:

Example 8 (Balder–Loki–Thor example) Teenage brothers Balder, Loki, and Thor prepare for an exam that, as is commonly known among them, contains one question asking to decide whether $ p $ or $ \neg p $ is the case. Suppose the correct answer is $ \neg p $. The initial model $ {\cal{M}} $ is the left model of Fig. 1. While the three are studying, Loki, unbeknownst to Thor, tries to trick Balder: Loki lies to Balder that he has overheard Thor boasting to know the correct answer to be $ p $. Balder seems to dismiss Loki's claim as a ruse, leaving Loki thinking his trick had no effect. In truth, however, Balder does believe Loki and is now under the impression that Loki agrees with Thor that the answer is $ p $. Balder himself, on the other hand, is not going to take Thor's word on it, given Thor's propensity to boast and act rashly. Thus, using $ b $, $ l $, and $ t $ for the brothers, Loki's trick should change Balder's beliefs to achieve the goal formula:

without either affecting Loki's or Thor's beliefs or making $ B_b p $ true.

Since ignorance of the correct answer is common belief in the initial model $ {\cal{M}} $, the public announcement of $ \varphi $ would cause everybody's beliefs to become inconsistent, whereas a private message $ B_t p \land B_l B_t p \land B_l p $ would cause the same inconsistency, but for Balder's beliefs only. This happens whether one uses the world-removing or arrow-removing updates.

Instead, we propose an update method that stratifies the initial model $ {\cal{M}} $ into several clusters representing individual beliefs and updating only some of these clusters, depending on the modal structure of the goal formula, resulting in model $ {\cal{M}}^U $ in Fig. 1, where updated clusters are represented by light-gray rectangles. Cluster 0 contains only the actual world $ v $, which no agent considers possible. Cluster $ -1 $ (the sink) is the copy of the initial model representing (higher-order) beliefs of agents unaffected by the message, including Loki's and Thor's beliefs. In particular, the ignorance of the correct answer is still common belief between Loki and Thor. Balder is also ignorant of the correct answer: his beliefs are represented by cluster $ 1 $, so $ {\cal{M}}^U, v \nvDash B_b p \lor B_b \neg p $. But his ignorance is not anymore common with Loki and Thor. Indeed, according to cluster $ 2 $, which represents Balder's beliefs about Thor's beliefs, $ {\cal{M}}^U, v \vDash B_b B_t p $. Cluster $ 3 $ plays the same role for Balder's beliefs about Loki's beliefs, making $ {\cal{M}}^U, v \vDash B_b B_l p $. Thus, while himself being ignorant of the answer, Balder thinks that Loki and Thor have chosen for themselves. Finally, cluster $ 4 $ is Balder's beliefs about Loki's beliefs about Thor's beliefs so that $ {\cal{M}}^U, v \vDash B_bB_lB_t p $. Overall, $ {\cal{M}}^U, v \vDash \varphi $. The $ b $-labeled double arrow from cluster $ 3 $ to the sink $ -1 $ represents two $ b $-labeled arrows from the only world of cluster $ 3 $ to each of the two worlds of the sink and ensures that Balder believes that Loki believes that Balder has not changed his beliefs, $ {\cal{M}}^U, v \vDash B_b B_l (\neg B_b p \land \neg B_b \neg p) $. Similarly, the $ b,l $-labeled double arrows from clusters $ 2 $ and $ 4 $ to the sink signify that in no scenario where Thor has chosen an answer for himself, does he expect others to follow his example (or even be aware of his choice). It is easy to see that no agent has inconsistent beliefs, $ {\cal{M}}^U \vDash \neg B_b \bot \land \neg B_l \bot \land \neg B_t \bot $, and that Loki's and Thor's beliefs are the same as in the initial model, $ M, v \vDash B_a \psi $ iff $ {\cal{M}}^U, v \vDash B_a \psi $ for $ a \in \{l,t\} $.

Figure 1. 

Left: Initial pointed Kripke model $ {\cal{M}} $. Right: Updated model $ {\cal{M}}^U $ (the actual world $ v $ is dark gray). A formula $ \varphi $ within a circle representing a world means that $ \varphi $ is true in this world. A light-gray rectangle with $ n $ in the top left corner is the cluster that is numbered $ n $. A double arrow from such cluster $ n $ to cluster $ m $ represents a set of accessibility arrows with the same agent's label from every world of cluster $ n $ to every world of cluster $ m $.

In the following sections we will demonstrate how to synthesize an action model so that after the initial model $ {\cal{M}} $ is updated with it, we arrive at the desired updated model $ {\cal{M}}^U $.

2.2.   Pointed updates

It is well known that repeatedly applying product updates for multi-round communication can cause an exponential blow up of the domain of the model, even for simple models and action models, see Figs 2–4. Indeed, every updated model has exactly one world where $ p $ is false. Hence, a further update of a model of $ N $ worlds with $ {\cal{U}} $ creates a model with $ 2N-1 $ worlds.

Figure 2. 

Left: Initial (pointed) Kripke model $ {\cal{M}} $ where agent $ a $ and $ b $ are uncertain about whether $ p $ or $ \lnot p $ is true. Right: (Pointed) action model $ {\cal{U}} $ for a private message $ p $ to $ a $: agent $ a $ learns $ p $, while $ b $ believes that nothing happened. A formula $ \varphi $ within a square representing an event $ \beta $ is the precondition for this event, i.e., $ \text{pre}(\beta) = \varphi $.

Figure 3. 

Left: First product update $ {\cal{M}} \otimes {\cal{U}} $ of Kripke model $ {\cal{M}} $ with action model $ {\cal{U}} $. Right: Second product update $ ({\cal{M}} \otimes {\cal{U}}) \otimes {\cal{U}} $ with the same action model $ {\cal{U}} $. $ p $ is true in all worlds that start from $ p $ and false in all worlds that start from $ \lnot p $.

Figure 4. 

Third product update $ \bigl(({\cal{M}} \otimes {\cal{U}})\otimes {\cal{U}}\bigr)\otimes {\cal{U}} $ with the same action model $ {\cal{U}} $.

The standard (often implicit) solution is to reduce the size of the resulting model by using bisimulation contraction^[19], making the model smaller again. For example, bisimulation contraction deletes all worlds that are unreachable from the resulting actual world, resulting in a bisimilar and hence, modally equivalent^[18], model.

To avoid this two-step procedure, we introduce the notion of pointed updates, which incorporates this world-removing operation formally and explicitly:

Definition 9 (Pointed update) Let $ ({\cal{M}},w)=(\langle S, R, V\rangle, w) $ be a pointed Kripke model and $ ({\cal{U}},\alpha) = (\langle E, Q, \text{pre}\rangle, \alpha) $ be a pointed action model. If $ {\cal{M}}, w \vDash \text{pre}(\alpha) $, then we define the updated pointed Kripke model $ \bigl({\cal{M}}\odot {\cal{U}}, (w,\alpha)\bigr) $ where $ {\cal{M}}\odot {\cal{U}} := \langle S^ {\cal{U}}, R^ {\cal{U}}, V^ {\cal{U}}\rangle $ as follows. Let $ T^ {\cal{U}} := \bigl\{(v,\beta) \in S \times E \mid {\cal{M}}, v \vDash \text{pre}(\beta)\bigr\} $. Note that $ (w,\alpha) \in T^ {\cal{U}} $.

● The domain $ S^ {\cal{U}} $ is the smallest subset of $ T^ {\cal{U}} $ containing $ (w,\alpha) $ such that:

if $ (v,\beta) \in S^ {\cal{U}} $, $ (u,\gamma) \in T^ {\cal{U}} $, and both $ v R_i u $ and $ \beta Q_i \gamma $ for some agent $ i $, then $ (u,\gamma) \in S^ {\cal{U}} $;

● $ R^ {\cal{U}}_i := \left\{\bigl((v, \beta),(u, \gamma)\bigr)\in S^ {\cal{U}}\times S^ {\cal{U}} \mid (v, u) \in R_i \text{ and } (\beta, \gamma) \in Q_i\right\} $;

● $ V^ {\cal{U}}(p) := \left\{(v, \beta)\in S^ {\cal{U}} \mid v \in V(p)\right\} $.

To show that pointed updates produce the same result as product updates but with smaller models, we use the notion of bisimulation.

Definition 10 ($ G $-bisimulation) Pointed Kripke models $ ({\cal{M}}, v) $ and $ ({\cal{M}}', v') $ are $ G $-bisimilar for a group $ G \subseteq {\cal{A}} $ of agents, notation $ {\cal{M}}, v \underline{\leftrightarrow}_G {\cal{M}}', v' $, iff for any $ a \in G $

● $ G $-Forth: if $ v R_a u $, then there is $ u'\in S' $ such that $ v' R_a'u' $ and $ {\cal{M}},u\underline{\leftrightarrow} {\cal{M}},u' $;

● $ G $-Back: if $ v' R_a' u' $, then there is $ u \in S $ such that $ v R_a u $ and $ {\cal{M}},u\underline{\leftrightarrow} {\cal{M}},u' $.

The definition of $ G $-bisimilarity for pointed action models is analogous.

Definition 11 ($ G $-indistinguishability) Pointed Kripke models $ ({\cal{M}}, v) $ and $ ({\cal{M}}', v') $ are called $ G $-indistinguishable for group $ G \subseteq {\cal{A}} $, notation $ {\cal{M}}, v \equiv_G {\cal{M}}', v' $, whenever $ {\cal{M}}, v \vDash B_a \varphi $ iff $ {\cal{M}}', v' \vDash B_a \varphi $ for all formulas $ \varphi $ and agents $ a\in G $.

Theorem 12: ($ G $-bisimilarity implies $ G $-indistinguishability) If $ {\cal{M}}, v\underline{\leftrightarrow}_G {\cal{M}}', v' $, then $ {\cal{M}}, v\equiv_G {\cal{M}}', v' $.

Proof Because $ G $-Forth and $ G $-Back (Definition 10) hold, the statement follows from Theorem 7 and Definition 11 as $ {\cal{M}}, u \equiv {\cal{M}}', u' $ in both cases. □

Theorem 13: (Product and pointed updates are bisimilar) Given a pointed Kripke model $ ({\cal{M}},w) $ and pointed action model $ ({\cal{U}},\alpha) $ such that $ {\cal{M}},w \vDash \text{pre}(\alpha) $, we have $ {\cal{M}}\odot {\cal{U}}, (w,\alpha) \underline{\leftrightarrow} {\cal{M}}\otimes {\cal{U}}, (w,\alpha) $.

Proof: Let $ {\cal{M}}= \langle S, R, V\rangle $, $ {\cal{U}} = \langle E, Q, \text{pre}\rangle $, $ {\cal{M}}\odot {\cal{U}} = \langle S^ {\cal{U}}, R^ {\cal{U}}, V^ {\cal{U}}\rangle $ and $ {\cal{M}} \otimes {\cal{U}} = \langle S',R',V' \rangle $. By construction, $ (w,\alpha) \in S^ {\cal{U}} \subseteq S' $, and $ R^ {\cal{U}} = R'_{\upharpoonright (S^ {\cal{U}} \times S^ {\cal{U}})} $, and $ V^ {\cal{U}} = V'_{\upharpoonright S^ {\cal{U}}} $. Hence, it is easy to see that $ {\cal{B}} := \left\{\bigl((v,\beta),(v,\beta)\bigr) \mid (v,\beta) \in S^ {\cal{U}}\right\} $ is the required bisimulation. □

Theorem 14: (Updates preserve bisimilarity) Given bisimilar pointed Kripke models $ {\cal{M}},w\underline{\leftrightarrow} {\cal{M}}',w' $ and bisimilar pointed action models $ {\cal{U}},\alpha\underline{\leftrightarrow} {\cal{U}}',\alpha' $ such that $ {\cal{M}},w \vDash \text{pre}(\alpha) $, we have $ {\cal{M}}\otimes {\cal{U}}, (w,\alpha) \underline{\leftrightarrow} {\cal{M}}'\otimes {\cal{U}}', (w',\alpha') $ and $ {\cal{M}}\odot {\cal{U}}, (w,\alpha) \underline{\leftrightarrow} {\cal{M}}'\odot {\cal{U}}',$ $ (w',\alpha') $. The same holds for $ G $-bisimilarity.

Proof: For product updates, the proof can be found in van Ditmarsch et al.^[4]. For pointed updates, it then follows from Theorem 13. The statements for $ G $-bisimilarity easily follow. □

The advantage of pointed updates can be illustrated by the fact that, while repeated product updates of $ {\cal{M}} $ with $ {\cal{U}} $ from Fig. 2 lead to the exponential growth of the domain, pointed updates yield the three-world pointed Kripke model depicted left in Fig. 3, no matter how many times the pointed update is performed:

While bisimulation contraction^[19] can shrink the model obtained by the product update operation, it needs to be invoked on the resulting model in a second step. In other words, first the model needs to be computed (with a potential exponential blowup) and then the bisimulation contraction runs on that model, making the operation computationally costly. On the other hand, the pointed update operation that we introduce runs only once and it produces a model which is no bigger than the one that would be obtained by the product update operation.

In the following section, we use this mechanism to solve the consistent update synthesis problem.

In this section, we propose a solution to the consistent update synthesis task for goal formulas $ \varphi $ representing deterministic belief increase (DBI) by generating a pointed action model $ {\cal{U}}_ \varphi $ such that the result of a pointed update of any given pointed Kripke model with $ {\cal{U}}_ \varphi $ satisfies $ \varphi $ and inconsistent beliefs (including higher-order beliefs) are not introduced whenever they are possible to avoid. By deterministic belief increase we mean situations when several agents are prescribed additional beliefs (including higher-order beliefs) without creating alternative ways of fulfilling the prescription. Before giving the formal definition, it should be mentioned that there is always a trivial way of creating new beliefs by making the agents' beliefs inconsistent, i.e., making them believe all statements including the desired ones. However, making agents' reasoning inconsistent does not comport with the ideology of minimal change, nor is productive in terms of correcting agents' incidental false beliefs. The main novelty in our method of update synthesis is the aim to preserve consistency whenever possible. Now we give a formal definition of goal formulas representing deterministic belief increase:

Definition 15 The set of target agents of a modal formula $ \varphi $ is defined as follows: $ \text{ta}(p) := \varnothing $; $ \text{ta}(\lnot \varphi) := \text{ta}(\varphi) $; $ \text{ta} (\varphi \land \psi) := \text{ta}(\varphi) \cup \text{ta}(\psi) $; finally $ \text{ta} (B_i \varphi) := \{i\} $.

E.g., $ \text{ta}\bigl(B_b (B_t p \land B_l B_t p \land B_l p)\bigr) = \{b\} $ even though $ \text{ta}(B_t p \land B_l B_t p \land B_l p) = \{t,l\} $.

Definition 16 (DBI goal formulas, DBI normal form) DBI goal formulas $ \varphi $, or DBI formulas for short, are defined by the following BNF:

where $ \xi $ is any purely propositional formula and $ i \in {\cal{A}} $. Thus, each DBI goal formula is a non-empty conjunction of belief operators. Formulas in DBI normal form are DBI formulas $ \varphi $ obtained by restricting the construction as follows: $ B_i \xi $ is always DBI normal; $ B_i\varphi $ and $ B_i(\xi \wedge \varphi) $ are DBI normal iff $ \varphi $ is DBI normal and $ i \notin \text{ta}(\varphi) $; $ \varphi \wedge \psi $ is DBI normal iff $ \varphi $ and $ \psi $ are DBI normal and $ \text{ta}(\varphi) \cap \text{ta}(\psi) = \varnothing $.

Lemma 17 For any DBI goal formula $ \varphi $, there exists a DBI normal formula $ \varphi' $ such that $ {\cal{K}}45 \vDash \varphi \equiv \varphi' $.

Proof We conduct the proof by structural induction over DBI goal formula $ \varphi $.

Base case: As $ \varphi = B_i \xi $ for propositional formula $ \xi $, $ \varphi $ is already DBI normal.

Induction hypothesis: Given goal formula $ \varphi $, for its proper sub formula $ \psi $ there exists a formula $ \psi' $ that is both DBI normal and equivalent to $ \psi $.

Induction step:

● If $ \varphi = B_i \psi $ or $ \varphi = B_i (\xi \wedge \psi) $ for propositional formula $ \xi $, it follows from the induction hypothesis that there exists a formula $ \psi' $ that is DBI normal and equivalent to $ \psi $. Suppose by contradiction that $ B_i \psi' $ (respectively $ B_i (\xi \wedge \psi') $) is not DBI normal, thus $ i \in \text{ta}(\psi') $. Hence by Definition 16 $ \psi' = (B_i \psi") \wedge \tau $, where $ i \not\in \text{ta}(\psi") $, $ i \not\in \text{ta}(\tau) $ and both $ \psi" $ and $ \tau $ are DBI normal. Using the $ {\cal{K}}45 $ logical equivalences $ B_iB_i \theta \equiv B_i \theta $, $ B_i(\xi \land B_i \theta) \equiv B_i(\xi \land \theta) $ and $ B_i\theta \land B_i \eta \equiv B_i(\theta \land \eta) $ we get the following equivalence chains:

$ B_i \psi \equiv B_i \psi' \equiv B_i (B_i \psi" \wedge \tau) \equiv B_iB_i \psi" \wedge B_i \tau \equiv B_i \psi" \wedge B_i \tau \equiv B_i (\psi" \wedge \tau) $

$ B_i (\xi \wedge \psi) \equiv B_i (\xi \wedge \psi') \equiv B_i (\xi \wedge B_i \psi" \wedge \tau) \equiv B_i (\xi \wedge B_i \psi") \wedge B_i \tau$ $\equiv B_i (\xi \wedge \psi") \wedge B_i \tau \equiv B_i (\xi \wedge \psi" \wedge \tau) $.$ B_i (\psi" \wedge \tau) $ respectively $ B_i (\xi \wedge \psi" \wedge \tau) $ are DBI normal.

● Else, if $ \varphi = \varphi_1 \wedge \varphi_2 $, using the induction hypothesis there exist the two DBI normal formulas $ \varphi_1' $ and $ \varphi_2' $, where $ \varphi_1' $ is equivalent to $ \varphi_1 $ and $ \varphi_2' $ is equivalent to $ \varphi_2 $. Suppose by contradiction that $ \text{ta}(\varphi_1') \cap \text{ta}(\varphi_2') = G \ne \varnothing $, as otherwise $ \varphi_1' \wedge \varphi_2' $ would already be DBI normal (and equivalent to $ \varphi $). Hence it must be that $ \varphi_1' = \bigwedge\limits_{i \in G} B_i \psi_1^i \wedge \varphi_1" $ and $ \varphi_2' = \bigwedge\limits_{i \in G} B_i \psi_2^i \wedge \varphi_2" $, where $ \text{ta}(\varphi_1") \cap \text{ta}(\varphi_2") = \varnothing $ and $ \varphi_1" $, $ \varphi_2" $ as well as all $ \psi_1^i $ and $ \psi_2^i $ are DBI normal. Thus using the equivalence $ B_i\theta \land B_i \eta \equiv B_i(\theta \land \eta) $ and associativity and commutativity of $ \wedge $ we get $ \varphi_1' \wedge \varphi_2' \equiv \bigwedge\limits_{i \in G} (B_i \psi_1^i \wedge \varphi_1") \wedge \bigwedge\limits_{i \in G} (B_i \psi_2^i \wedge \varphi_2")$ $\equiv \bigwedge\limits_{i \in G} B_i (\psi_1^i \wedge \psi_2^i) \ \wedge \ \varphi_1" \wedge \varphi_2" $.

In addition, $ \bigwedge\limits_{i \in G} B_i (\psi_1^i \wedge \psi_2^i) \wedge \varphi_1" \wedge \varphi_2" $ is DBI normal. □

Lemma 18 ($ G $-bisimilarity and goal formula preservation) If $ {\cal{M}}, v\underline{\leftrightarrow}_G {\cal{M}}', v' $ and $ \varphi $ is a DBI formula with $ \text{ta}(\varphi) \subseteq G $, then $ {\cal{M}}, v \vDash \varphi $ iff $ {\cal{M}}', v' \vDash \varphi $.

Proof It follows from Theorem 12 and the fact that $ \varphi $ is a conjunction of $ B_i \psi_i $ for $ i \in \text{ta}(\varphi) \subseteq G $. □

Without loss of generality, from now on, we only consider formulas in DBI normal form. For instance, formula (1) is a DBI formula but not DBI normal. Its normal form would be $ B_b\bigl(B_tp \land B_l(p \land B_t p)\bigr) $. Given such a DBI normal formula $ \varphi $, we now construct a pointed action model $ ({\cal{U}}_ \varphi,0) $ such that for any pointed Kripke model $ ({\cal{M}}, w) $, the pointed update $ {\cal{M}}\odot {\cal{U}}_ \varphi $ is defined, $ {\cal{M}}\odot {\cal{U}}_ \varphi, (w,0) \vDash \varphi $, while other epistemic differences between $ ({\cal{M}}, w) $ and $ \left({\cal{M}}\odot {\cal{U}}_ \varphi, (w,0)\right) $ are minimized. Informally, this means that an update should not influence any beliefs except for those explicitly stated in $ \varphi $ and logically following from $ \varphi $ based on the agents' pre-update beliefs (we adopt the minimality principle in the same spirit of the standard AGM approach^[20] for which an update should lead to the loss of as few previous beliefs as possible^[21]). In particular, if $ j \notin \text{ta}(\varphi) $, then $ j $'s beliefs should not be affected even if $ B_j $ occurs in $ \varphi $: updating somebody else's beliefs about $ j $'s beliefs should not affect actual $ j $'s beliefs.

Algorithms 1, 2, 3, and 4 show the construction of an action model for a consistent DBI update.

We illustrate this update synthesis method by applying it to Example 8:

Example 19 For the DBI normal form $ \varphi=B_b(B_t p \land B_l(p \land B_t p)) $ of formula (1) from Example 8, pointed action model $ ({\cal{U}}_{\varphi}, 0) $ constructed according to Algorithm 1 can be found in the left part of Fig. 5. The result of the pointed update of $ ({\cal{M}},v) $ from the left part of Fig. 1 with this $ ({\cal{U}}_{\varphi}, 0) $ can be seen on the right of Fig. 5 (and is isomorphic to the right part of Fig. 1). It is easy to see that $ {\cal{M}}\odot {\cal{U}}_\varphi, (v,0) \vDash \varphi $. Since all accessibility relations in this updated model $ {\cal{M}}\odot {\cal{U}}_\varphi $ are serial, it follows that it is common belief that all agents have consistent beliefs.

In addition, we claim that this update synthesis has been achieved with minimal change to agents' beliefs. Indeed, it is easy to prove using $ G $-bisimilarities for appropriate groups of agents that

where $ v $ is the actual world and $ u $ is the other world of $ {\cal{M}} $ (we omit set braces in the subscript of $ \equiv ).$ The statements in the first column mean that the update is imperceptible for agents $ l $ and $ t $ and that agent $ b $ thinks that agent $ l $ does not think $ b $'s beliefs have changed. Similarly, the second column testifies that $ b $ thinks that neither $ t $'s beliefs about $ b $ and $ l $ nor $ l $'s beliefs about what $ t $ thinks regarding $ b $ or $ l $ changed. In other words, the only higher-order beliefs that are affected by the update are those explicitly dictated by $ \varphi $.

Figure 5. 

Successful update synthesis $ {\cal{M}}\odot {\cal{U}}_\varphi, (v,0) \vDash \varphi $ by applying pointed update with pointed action model $ ({\cal{U}}_ \varphi,0) $ for DBI formula (1) from Example 8 to $ ({\cal{M}},v) $ from Fig. 1 (left).

We illustrate the advantage of using pointed updates over the product update operation using Example 8:

Example 20 Consider the same example but using the product update of standard DEL: The result of updating the initial model with the action model obtained from $ \varphi $ is shown in Fig. 6. In particular, the result of the product update has only one additional world with respect to the model obtained via pointed update $ {\cal{M}}\odot {\cal{U}}_\varphi $ visible in Fig. 5 (left), which is not reachable from the actual world, namely the $ p $ world in the $ v $ cluster at the top. However, the difference between the two operations is striking in case of iterated updates: applying to the resulting model the product update operation again with the same action model leads to the Kripke model sketched in Fig. 7, which contains a number of worlds that are not reachable from the actual world but copied in every sub-model nonetheless. Compare this to the pointed update operation, whose result is the same for any number of iterations for the same action model (Theorem 33).

Figure 6. 

Balder-Loki-Thor updated model using product updates $ {\cal{M}} \otimes {\cal{U}}_\varphi $.

Figure 7. 

Sketch of the result of the iterated product update operation $ ({\cal{M}} \otimes {\cal{U}}_\varphi) \otimes {\cal{U}}_\varphi $. Grey rectangles are a compact way to represent sub-models originating from worlds in the previous model. Dotted arrows are meant to capture the direction of the arrows and the agents involved. Unlike double arrows, they do not represent arrows from and to all worlds in the rectangle, but only from and to some of these worlds. We leave to the reader their identification. Finally, note that the sink is a copy of the previous model.

Let us now prove that $ {\cal{U}}_ \varphi $ performs update synthesis for any DBI normal $ \varphi $, minimizes belief change of other agents, and preserves consistency whenever possible.

We will use the auxiliary fact that updates do not affect propositional formulas:

Lemma 21 (Propositional invariance) Let $ (w,\alpha) $ belong to the domain of $ {\cal{M}}\odot {\cal{U}} $ for some Kripke model $ {\cal{M}} $ and action model $ {\cal{U}} $. Then for any propositional formula $ \xi $,

Proof For product updates $ \otimes $, this is well known (according to van Ditmarsch et al.^[4]). For pointed updates, it follows from Theorem 13. □

Definition 22 ($ \varphi $-enforcing) We call a pointed action model $ {\cal{U}} = \langle E, Q, \text{pre}\rangle $ with point $ \alpha \in E $ and formula $ \varphi $ in DBI normal form, $ \varphi $-enforcing iff

● if $ \varphi = B_i \xi $, for propositional formula $ \xi $, then for all states $ \beta \in E $ s.t. $ \alpha Q_i \beta $, $ \models \text{pre}(\beta) \rightarrow \xi $.

● else if $ \varphi = B_i \psi $, then there exists at least one state $ \beta' \in E $ s.t. $ \alpha Q_i \beta $ and for all states $ \beta \in E $ s.t. $ \alpha Q_i \beta $, $ ({\cal{U}}, \beta) $ is $ \psi $-enforcing.

● else if $ \varphi = B_i (\xi \wedge \psi) $, for propositional formula $ \xi $, then there exists at least one state $ \beta' \in E $ s.t. $ \alpha Q_i \beta $ and for all states $ \beta \in E $ s.t. $ \alpha Q_i \beta $, $ ({\cal{U}}, \beta) $ is $ \psi $-enforcing and $ \models \text{pre}(\beta) \rightarrow \xi $.

● else if $ \varphi = \psi_1 \wedge \psi_2 $, then $ ({\cal{U}}, \alpha) $ is $ \psi_1 $- and $ \psi_2 $-enforcing.

Lemma 23 (Update with $ \varphi $-enforcing action model) For pointed Kripke model $ ({\cal{M}}, v) $, DBI normal formula $ \varphi $, and $ \varphi $-enforcing pointed action model $ ({\cal{U}}, \alpha) $, if the update $ {\cal{M}} \odot {\cal{U}} = \langle S', R', V' \rangle $ is defined (if $ M,v \models \text{pre}(\alpha) $), then

Proof We conduct the proof by induction over the recursive structure of $ \varphi $.

● In the base case, when $ \varphi = B_i \xi $, since $ ({\cal{U}}, \alpha) $ is $ \varphi $-enforcing, for all states $ (w, \beta) $ s.t. $ (v, \alpha) R'_i (w, \beta) $, $ {\cal{U}} \odot {\cal{M}}, (w, \beta) \models \xi $. Hence $ {\cal{U}} \odot {\cal{M}}, (v, \alpha) \models B_i \xi $ by semantics of $ B_i $.

● If $ \varphi = B_i \psi $, since for all $ i $-accessible states $ \beta $ from $ \alpha $, $ ({\cal{U}}, \beta) $ is $ \psi $-enforcing using the IH we get that for all $ i $-accessible states $ (w, \beta) $ from $ (v, \alpha) $, $ {\cal{M}} \odot {\cal{U}}, (w, \beta) \models \psi $. Hence $ {\cal{U}} \odot {\cal{M}}, (v, \alpha) \models B_i \psi $ by semantics of $ B_i $.

● If $ \varphi = B_i (\xi \wedge \varphi) $ the reasoning is simply a combination of the previous two cases.

● If $ \varphi = \psi_1 \wedge \psi_2 $, as $ ({\cal{U}}, \alpha) $ is $ \psi_1 $- and $ \psi_2 $-enforcing using the IH we get that $ {\cal{U}} \odot {\cal{M}}, (v, \alpha) \models \psi_1 $ and $ {\cal{U}} \odot {\cal{M}}, (v, \alpha) \models \psi_2 $ from which $ {\cal{U}} \odot {\cal{M}}, (v, \alpha) \models \psi_1 \wedge \psi_2 $ follows.□

Lemma 24 ($ {\cal{U}}_\varphi $ is $ \varphi $-enforcing) For DBI normal formula $ \varphi $, the pointed action model $ ({\cal{U}}_\varphi, 0) $ synthesized by Algorithm 1 is $ \varphi $-enforcing and $ \text{pre}^\varphi(0) = \top $.

Proof We start the proof by induction over the structure of $ \varphi $ and the action model $ {\cal{U}}'_\varphi $ recursively constructed by Algorithm 2. We prove the statement for the resulting model $ {\cal{U}}'_\varphi $ after the function call $ { \text{CreateActionModel}}(\varphi, {\cal{U}}, u) $, where $ {\cal{U}} = \langle \{0\}, \varnothing, {\text{pre}} \rangle $, where $ \text{pre}(0) = \top $ following from code lines 1.–4. of Algorithm 1.

● In the base case where $ \varphi = B_i \xi $, it trivially follows from Algorithm 2 code lines 1.–3. that $ {\cal{U}}'_\varphi $ is $ \varphi $-enforcing, as a single new $ i $-accessible state $ u' $ from $ u $ is constructed with $ \text{pre}^\varphi(u') = \xi $.

● If $ \varphi = B_i \varphi' $ from Algorithm 2 code lines 4.–6. in particular using the IH for line 6. it follows that $ ({\cal{U}}'_\varphi, u') $ is $ \varphi' $-enforcing. Since $ \varphi $ is DBI normal and therefore $ i \not\in \text{ta}(\varphi') $ and the fact that recursive calls in Algorithm 2 only ever occur for newly created states, $ u' $ is the only state $ i $-accessible from $ u $. Hence $ {\cal{U}}'_\varphi $ is $ \varphi $-enforcing.

● If $ \varphi = B_i (\xi \wedge \varphi') $ by Algorithm 2 code lines 7.–10. the reasoning is a combination of the previous two cases.

● If $ \varphi = \varphi_1 \wedge \varphi_2 $ by Algorithm 2 code lines 11.–13. in particular using the IH, for the recursive call on line 12. we get that the intermediate model $ {\cal{U}}"_\varphi $ after the exeuction of code line 12. is $ \varphi_1 $-enforcing. Since $ \text{ta}(\varphi_1) \cap \text{ta}(\varphi_2) = \varnothing $ by DBI normality of $ \varphi $ and the fact that recursive function calls are only made for newly created states, we can be certain that the recursive call in line 13. operates on a separate branch in the model than the call in line 12 did. Thus we conclude that $ {\cal{U}}'_\varphi $ is not only $ \varphi_2 $-, but continues to be $ \varphi_1 $-enforcing as well.

By the simple observation that no recursive calls of Algorithm 2 are made for existing states, therefore also not for state $ 0 $, it remains by Algorithm 1 code line 4 that $ \text{pre}^\varphi(0) = \top $, as Algorithm 4 does not modify the precondition of prior existing states. □

Theorem 25: (Update synthesis success) For any DBI normal formula $ \varphi $ and any pointed Kripke model $ ({\cal{M}},v) $, the pointed update of $ ({\cal{M}},v) $ with $ ({\cal{U}}_ \varphi,0) $ is defined and

Proof Follows from Lemma 23 and Lemma 24. □

The sequence of modal operators that one encounters, when traversing the syntax tree of formula $ \varphi $ (including the empty list $ \varepsilon $) starting from its root, we call modal operator sequence or simply modality sequence. For example, given $ \varphi = B_i(B_j p \wedge B_r q) $, the set of modal operator sequences of $ \varphi $, would be $ \{ \varepsilon, B_i, B_i B_j, B_i B_r\} $.

To formulate statements about minimal change, we introduce the notion of independent formulas.

Definition 26 (Independent formulas) Let $ \varphi $ be a DBI normal formula and its corresponding action model $ {\cal{U}}_ \varphi=\langle E^ \varphi, Q^ \varphi, \text{pre}^ \varphi\rangle $ be constructed according to Algorithm 1. A modal formula $ \theta $ is in $ \top $-shape with respect to event $ \alpha_0 \in E^ \varphi $ iff for each sequence of modal operators $ B_{i_1}\dots B_{i_k} $ used in the construction of $ \theta $, including the empty sequence $ \varepsilon $ with $ k=0 $, and for the unique corresponding sequence $ \alpha_0 Q^ \varphi_{i_1}\alpha_1Q^ \varphi_{i_2}\alpha_2\dots\alpha_{k-1}Q^ \varphi_{i_k}\alpha_k $ of events $ \alpha_j \in E^ \varphi $ all $ \text{pre}^ \varphi(\alpha_j)=\top $ for $ 0\leq j\leq k $ (note that the uniqueness of such a sequence formally follows from Lemma 48 and Theorem 49). Formula $ \theta $ is called independent of $ \varphi $ iff it is in $ \top $-shape w.r.t. $ 0\in E^ \varphi $. If $ \theta $ is not independent of $ \varphi $, it is dependent on $ \varphi $.

Example 27 For formula $ \varphi=B_b\bigl(B_t p \land B_l(p \land B_tp)\bigr) $ from Example 8, we have that $ \theta = \lnot B_b B_b p \lor B_t B_l p $ is independent from $ \varphi $ because the modal operator sequences $ \varepsilon $, $ B_b $, $ B_bB_b $, $ B_t $, and $ B_tB_l $ correspond to event sequences $ 0 $, $ 0Q^ \varphi_b4 $, $ 0Q^ \varphi_b4Q^ \varphi_b4 $, $ 0Q^ \varphi_t { }\mathop{-} 1 $, and $ 0Q^ \varphi_t { }\mathop{-} 1 Q^ \varphi_l { }\mathop{-} 1 $ and preconditions for events $ 0 $, $ 4 $, and $ { }\mathop{-} 1 $ are all $ \top $. On the other hand, $ \eta = \lnot B_b B_t p $ is dependent on $ \varphi $ because modality sequence $ B_bB_t $ corresponds to event sequence $ 0Q^ \varphi_b4Q^ \varphi_t3 $, and $ \text{pre}^ \varphi(3) =p\ne \top $. Both $ \theta $ and $ \eta $ were true in $ {\cal{M}},v $ from Fig. 1, left. While the pointed update with $ ({\cal{U}}_ \varphi,0) $ keeps $ \theta $ true, formula $ \eta $ becomes false in $ {\cal{M}} \odot {\cal{U}}_ \varphi, (v,0) $ (see Fig. 5, right).

In other words, given a formula $ \varphi $ in DBI normal form, a formula $ \theta $ is independent of $ \varphi $ if the sequences of modal operators in the formula $ \theta $ have a corresponding sequence of events in $ U_\varphi $ and the precondition of those events is always $ \top $. A formula is then dependent in case at least one of the preconditions for those events is different from $ \top $. The main idea is that the pointed update $ U_\varphi $ will keep the formulas that are independent of $ \varphi $ true after the update.

Theorem 28 (Update synthesis minimality) If formula $ \theta $ is independent of a DBI normal formula $ \varphi $, then for any pointed Kripke model $ ({\cal{M}},v) $,

Proof Let $ {\cal{M}}=\langle S, R, V\rangle $. We prove by induction on the construction of $ \theta $ that, for any $ \alpha \in E^ \varphi $ and any $ u \in S $, if $ \theta $ is in $ \top $-shape with respect to $ \alpha $, then $ {\cal{M}}, u \vDash \theta $ iff $ {\cal{M}}\odot {\cal{U}}_ \varphi, (u,\alpha) \vDash \theta $. (6) is an instance of this induction statement for $ \alpha=0 $ and $ u=v $. Note that if $ \theta $ is in $ \top $-shape with respect to $ \alpha $, then $ \text{pre}^ \varphi(\alpha) = \top $ because of the empty sequence $ \varepsilon $, hence, the pointed update of $ ({\cal{M}},u) $ with $ ({\cal{U}}_ \varphi,\alpha) $ is defined for all $ u \in S $. For propositional atoms, the statement follows from the definition of pointed updates. The cases for Boolean connectives are straightforward. It remains to show the induction statement for $ \theta = B_i \eta $. Let $ \beta \in E^ \varphi $ be the unique event such that $ \alpha Q_i^ \varphi\beta $. Then $ \text{pre}^ \varphi(\beta) = \top $ because of sequence $ B_i $ of $ \theta $ and, additionally, $ \eta $ is in $ \top $-shape with respect to $ \beta $. By IH, for any $ u \in S $, we have $ {\cal{M}},u\vDash \eta $ iff $ {\cal{M}}\odot {\cal{U}}_ \varphi, (u,\beta) \vDash \eta $. We have $ {\cal{M}}, u \nvDash B_i \eta $ iff $ {\cal{M}}, w \nvDash\eta $ for some $ uR_iw $. By IH, this is equivalent to $ {\cal{M}}\odot {\cal{U}}_ \varphi, (w,\beta) \nvDash\eta $, which is equivalent to $ {\cal{M}}\odot {\cal{U}}_ \varphi, (u,\alpha) \nvDash B_i\eta $ because $ (u,\alpha)R^ \varphi_i(w,\gamma) $ iff $ u R_i w $ and $ \gamma=\beta $. □

Corollary 29 Let $ \varphi = \bigwedge_{j\in G}B_j\omega_j $ be a DBI normal formula, where $ \varnothing \ne G \subseteq {\cal{A}} $.

1. If $ i \notin \text{ta}(\varphi) $, i.e., if $ i\notin G $, then $ i $'s beliefs are unaffected by pointed update $ {\cal{U}}_ \varphi $, i.e., $ {\cal{M}},v \vDash B_i \sigma $ iff $ {\cal{M}}\odot {\cal{U}}_ \varphi, (v,0) \vDash B_i \sigma $ for any formula $ \sigma $ and any pointed Kripke model $ ({\cal{M}},v) $.

2. If $ i\in \text{ta}(\varphi) $, but $ \omega_i = \bigwedge_{j\in H}B_j\pi_j $ has no propositional component, then $ i $'s propositional beliefs are unaffected by $ {\cal{U}}_ \varphi $, i.e., $ {\cal{M}},v \vDash B_i \chi $ iff $ {\cal{M}}\odot {\cal{U}}_ \varphi, (v,0) \vDash B_i \chi $ for any propositional formula $ \chi $ and any pointed Kripke model $ ({\cal{M}},v) $.

Theorem 30 (Update synthesis consistency preservation) Let $ \varphi $ be a DBI normal formula. Pointed update with $ {\cal{U}}_ \varphi $ can only cause (higher-order) inconsistent beliefs iff the respective (higher-order) beliefs originally excluded the respective propositional preconditions: for any modality sequence $ B_{i_1}\dots B_{i_k} $ with $ i_j\ne i_{j+1} $ for any $ j $ and any pointed Kripke model $ ({\cal{M}},v) $,

for the unique sequence $ 0 Q^ \varphi_{i_1}\alpha_1Q^ \varphi_{i_2}\alpha_2\dots Q^ \varphi_{i_k}\alpha_k $ of events $ \alpha_j \in E^ \varphi $.

Proof Let $ {\cal{M}}= \langle S, R, V\rangle $ and $ {\cal{M}} \odot {\cal{U}}_ \varphi = \langle S^ \varphi, R^ \varphi, V^ \varphi\rangle $ for the pointed update of $ ({\cal{M}},v) $ with $ ({\cal{U}}_ \varphi,0) $. The left statement holds iff there is a sequence $ vR_{i_1}s_1R_{i_2}s_2\dots R_{i_k}s_k $ of states from $ S $ such that $ {\cal{M}}, s_j \vDash \text{pre}^ \varphi(\alpha_j) $ for $ j=1,\dots,k $. It is easy to observe (by induction on $ k $) that this is equivalent to $ (s_j,\alpha_j) \in S^ \varphi $ for $ j=1,\dots,k $ and $ (v,0)R^ \varphi_{i_1}(s_1,\alpha_1)R^ \varphi_{i_2}(s_2,\alpha_2)\dots R^ \varphi_{i_k}(s_k,\alpha_k) $. The equivalence to the right statement now follows from the fact that $ {\cal{M}}\odot {\cal{U}}_ \varphi, (s_k,\alpha_k) \nvDash \bot $ and the uniqueness of the sequence of $ \alpha_j $'s such that $ 0 Q^ \varphi_{i_1}\alpha_1Q^ \varphi_{i_2}\alpha_2\dots Q^ \varphi_{i_k}\alpha_k $. □

Corollary 31 Let $ \varphi $ be a DBI normal formula.

1. If $ \varphi $ fits either of the clauses of Cor. 29 for agent $ i $, then $ {\cal{U}}_ \varphi $ preserves $ i $'s consistency, i.e., $ {\cal{M}},v \nvDash B_i \bot $ iff $ {\cal{M}}\odot {\cal{U}}_ \varphi, (v,0) \nvDash B_{i} \bot $ for any $ ({\cal{M}},v) $.

2. If $ \varphi = B_i\left(\xi \land \bigwedge_{k\in H} B_k \pi_k\right) \land \bigwedge_{j\in G} B_j \omega_j $ where $ i \notin G $ and $ \xi $ is propositional, then $ {\cal{U}}_ \varphi $ makes $ i $'s beliefs inconsistent if and only if $ i $ originally does not consider $ \xi $ to be possible, i.e., $ {\cal{M}},v \vDash \hat{B}_i \xi $ iff $ {\cal{M}}\odot {\cal{U}}_ \varphi, (v,0) \nvDash B_{i} \bot $ for any $ ({\cal{M}},v) $.

Definition 32 (Idempotence) We call an action model $ ({\cal{U}}, \alpha) $ idempotent iff pointed updates $ \bigl({\cal{M}} \odot {\cal{U}},\,\, (w,\alpha)\bigr) $ and $ \Bigl(({\cal{M}} \odot {\cal{U}}) \odot {\cal{U}},\,\, \bigr((w,\alpha),\alpha\bigr)\Bigr) $ are defined and isomorphic for any pointed Kripke model $ ({\cal{M}}, w) $.

Theorem 33 For any DBI normal formula $ \varphi $ and any pointed Kripke model $ ({\cal{M}}, v) $, $ {\cal{M}} \odot {\cal{U}}_\varphi, (v, 0) $ is idempotent.

Proof The updates $ {\cal{M}} \odot {\cal{U}}_\varphi, (v, 0) $ and $ ({\cal{M}} \odot {\cal{U}}_\varphi) \odot {\cal{U}}_\varphi, ((v, 0), 0) $ are always defined by Theorem 25.

Since $ {\cal{U}}_\varphi $ has an out-tree structure, meaning every state is reachable by a directed walk from the point, we conduct the proof by forward induction over this structure beginning from the root $ 0 $.

Ind. statement.: Given state $ ((w, \alpha), \beta) $ in the model $ ({\cal{M}} \odot {\cal{U}}_\varphi) \odot {\cal{U}}_\varphi $, $ \beta = \alpha $.

Ind. hyp.: Given state $ ((w, \alpha), \beta) $ for all its parent states $ ((w', \alpha'), \beta') $ the inductive statement holds.

Base case: Point $ (v, 0) $ is the only state that can be combined with $ 0 $, since by Algorithm 1 $ 0 $ has no incoming edges in $ {\cal{U}}_\varphi $.

Ind. step: Suppose by IH the inductive statement holds for state $ ((w, \alpha), \alpha) $, but not for its $ i $-accessible state $ ((x, \beta), \gamma) $, meaning $ \gamma \ne \beta $. Note that this $ i $-accessible state must exist, since $ ({\cal{M}} \odot {\cal{U}}_\varphi) \odot {\cal{U}}_\varphi, ((v, 0), 0) $ could not be smaller than $ {\cal{M}} \odot {\cal{U}}_\varphi, (v, 0) $, as all preconditions in $ {\cal{U}}_\varphi $ are propositional by Algorithm 2. Since $ ((w, \alpha), \alpha) {R_i^{ {\cal{U}}_\varphi}}^{ {\cal{U}}_\varphi} ((x, \beta), \gamma) $ it must be the case that also $ (w, \alpha) R_i^{ {\cal{U}}_\varphi} (x, \beta) $ by Definition 9. Since $ \varphi $ is DBI normal, every state in $ {\cal{U}}_\varphi $ has no more than one $ j $-accessible state, hence $ \beta $ is the only $ i $-accessible state from $ \alpha $. Therefore if $ ((w, \alpha), \alpha) {R_i^{ {\cal{U}}_\varphi}}^{ {\cal{U}}_\varphi} ((x, \beta), \gamma) $ it must be that $ \gamma = \beta $. □

The minimality of the update synthesis method we have described relies on a particular structure of the action model used for the update. We call this structure privatized. In this section, we give an explicit definition and show why it serves the purpose of preserving beliefs whenever possible. We begin with the notion of modal syntactic tree, which represents the nesting of modalities within a formula as a tree and provides the basis of the formal definition of privatization. Note that the structure of the action model returned by Algorithm 1 (almost) exactly follows this tree structure already, so there was no need to introduce it explicitly.

Definition 34 (Modal syntactic tree) The modal syntactic tree $ {\cal{T}}_{\varphi} $ of a goal formula $ \varphi $ is an out-tree with a single unlabeled root, while all non-root nodes are labeled with modal operators representing the nesting of modalities in $ \varphi $. Hence it is essentially $ \varphi $'s syntax tree, where however all non-modal operators are left out.

Some examples of modal syntactic trees are provided in Fig. 8: In $ {\cal{T}}_{B_i \xi} $, the root has one child-leaf labeled $ B_i $. Both $ {\cal{T}}_{B_i \varphi} $ and $ {\cal{T}}_{B_i (\xi \wedge \varphi)} $ are obtained by labeling the root of $ {\cal{T}}_{\varphi} $ with $ B_i $ and making it the only child of the new root. Finally, $ {\cal{T}}_{\varphi \wedge \psi} $ is obtained by taking the disjoint union of $ {\cal{T}}_{\varphi} $ and $ {\cal{T}}_{\psi} $ and identifying their roots.

Figure 8. 

Modal syntactic trees.

Definition 35 (Modal-syntactic-tree root paths) For formula $ \varphi $ we define $ RootP(\varphi) $ as the set of paths $ \big((root, \alpha_1, i_1), \ldots, (\alpha_{l-1}, \alpha_l, i_l)\big) $ of length $ l\geq0 $ in $ {\cal{T}}_{\varphi} $ starting from the root, where $ i_k $ is the label of $ \alpha_k $ for $ k=1,\dots,l $.

Definition 36 (Kripke-frame root walks) For a pointed Kripke frame $ (\langle S, R \rangle, w) $ we similarly define the set of root walks $ RootW(\langle S, R \rangle, w) $ as the set of all walks starting from the root (point) $ w $. We further define the restriction $ RootW_{{\rm{nsr}}}(\langle S, R \rangle, w) $ as the subset of $ RootW(\langle S, R \rangle, w) $, where we exclude walks that contain at least two successive edges for the same agent.

Definition 37 (Agent sequence) For a walk $ \sigma = \bigl((\alpha_1, \alpha_2, i_1), \ldots, (\alpha_l, \alpha_{l+1}, i_l)\bigr) $ from Defs. 35 or 36 we define $ {AgSeq}({\sigma}) := (i_1, \dots, i_l) $. In particular, $ {AgSeq}(\varepsilon) := \varepsilon $. We extend this definition to sets, where for a set of walks $ \Sigma $, $ {AgSeq}(\Sigma) $ is the set of corresponding agent sequences.

The set of all agent sequences of length $ l $ we denote by $ {\cal{A}}^l $. The set of all agent sequences of length $ l $ without any successively repeating agents we denote by $ {\cal{A}}^l_{ {\rm{nsr}}} $.

We now define clusters and walk accessible parts of the model.

Definition 38 (Clusters and reachable states) For a Kripke frame $ {\cal{F}} = \langle W, R \rangle $, world $ w\in W $, and sequence $ (i_1, \ldots, i_l)\in {\cal{A}}^l $ of agents, we introduce the cluster of path-accessible worlds

In particular, for the empty sequence, $ C_{ {\cal{F}},w}^{\varepsilon}= \{w\} $. We also define the reachability operator

For a set $ W' \subseteq W $, we define $ {R}({\cal{F}}, W') := \bigcup_{w' \in W'} {R}({\cal{F}}, w') $.

Definition 39 For action model $ {\cal{U}} = \langle E, Q, pre\rangle $ and state $ u \in E $, we define the $ u $-sub model $ {\cal{U}}^u = \langle E^u, Q^u, pre^u\rangle $ as the sub model of $ \langle E, Q, pre\rangle $ that is reachable from $ u $, where $ E^u = {R}({\cal{U}}, u) $, $ Q^u = Q_{\upharpoonright (E^u \times E^u)} $ and $ V^u = V_{\upharpoonright E^u} $.

Lemma 40 For DBI goal formula $ \varphi $, action model $ \langle E, Q, pre\rangle $, for which $ u \in E $ is a leaf node (potentially with a reflexive loop), let $ \langle E^\varphi, Q^\varphi, pre^\varphi\rangle $ be the action model synthesized by a call of Algorithm 2 $ \text{CreateActionModel}(\varphi, \langle E, Q, pre\rangle, u) $, then the size of its $ u $-sub model $ \langle E^{\varphi^u}, Q^{\varphi^u}, pre^{\varphi^u}\rangle $ is at worst linear in the size of the modal syntactic tree of $ \varphi $.

Proof We conduct the proof by structural induction over the DBI goal formula $ \varphi $.

Base case: $ \varphi = B_i \xi $ for purely propositional formula $ \xi $. The resulting $ u $-sub action model consists only of the root $ u $ and a newly created node $ u' $, with an at least an $ i $-arrow going from $ u $ to $ u' $ and a reflexive loop for $ u' $:

$ E^\varphi = \{u, u'\} $, $ Q_i^\varphi \supseteq \{(u, u'), (u', u')\} $.

Induction hypothesis: Given goal formula $ \varphi $, for its proper sub formula $ \varphi' $ and state $ u' \in E $, let $ \langle E^\varphi, Q^\varphi, pre^\varphi\rangle $ be the action model synthesized by a call of Algorithm 2 $ { \text{CreateActionModel}}(\varphi, \langle E, Q, pre\rangle, u') $, then the size of the $ u' $-sub model $ \langle E^{\varphi^{u'}}, Q^{\varphi^{u'}}, pre^{\varphi^{u'}}\rangle $ is at worst linear in the size of the modal syntactic tree of $ \varphi' $.

Induction step:

● If $ \varphi = B_i \varphi' $ or $ \varphi = B_i (\xi \wedge \varphi') $ for purely propositional formula $ \xi $. By Algorithm 2 it follows that only a single $ i $-accessible new state $ u' $ is added, after which the algorithm is called recursively (on code line 6. respectively 9.) for $ u' $ and $ \varphi' $. Since after the recursive call, the $ u' $-sub model $ \langle E^{u'}, Q^{u'}, pre^{u'}\rangle $ is linear in the size of the modal syntactic tree of $ \varphi' $, by assumption of the IH $ \langle E^{u}, Q^{u}, pre^{u}\rangle $ is linear in the size of the modal syntactic tree of $ \varphi $ as well, as the difference between $ \langle E^{u}, Q^{u}, pre^{u}\rangle $ and $ \langle E^{u'}, Q^{u'}, pre^{u'}\rangle $ is only a single state.

● Else if $ \varphi = \varphi_1 \wedge \varphi_2 $. Using the IH for both recursive calls (on code lines 12. and 13.), it directly follows that $ \langle E^{u}, Q^{u}, pre^{u}\rangle $ is linear in the size of both $ \varphi_1 $'s and $ \varphi_2 $'s, thus also $ \varphi $'s modal syntactic tree.□

Theorem 41 The action model $ \langle E^\varphi, Q^\varphi, pre^\varphi\rangle $ synthesized by a call $ { \text{SynthesizeActionModel}}(\varphi) $ of Algorithm 1 for DBI goal formula $ \varphi $ is at worst linear in the size of the modal syntactic tree of $ \varphi $.

Proof Follows from Algorithm 1, Algorithm 4, and Lemma 40. □

Definition 42 We define $ \mathfrak{L}_{ {\rm{nsr}}{}} $ as the largest subset of $ \mathfrak{L} $ s.t. in any $ \varphi \in \mathfrak{L}_{ {\rm{nsr}}{}} $ no two subsequent nestings of modalities with the same agent occur, meaning formulas like $ B_jB_i(p \wedge \hat{B}_i q)) $ are disallowed.

Note that this restriction of the language does not affect any of the results in Section 3 because of the following obvious proposition.

Proposition 43 Every DBI formula is in $ \mathfrak{L}_{ {\rm{nsr}}{}} $.

Before we provide a formal definition of privatization we want to first give an informal definition and also clarify why we introduce two notions.

Given a formula $ \varphi \in \mathfrak{L}_{ {\rm{nsr}}{}} $ a pointed Kripke frame is weakly privatized with respect to $ \varphi $ iff for every agent sequence of any root path of $ \varphi $'s modal syntactic tree, all states are accessible via such an agent sequence from the point are not accessible via another agent sequence (without successively repeating agents). A Kripke frame is strongly privatized iff it is weakly privatized and for every agent sequence for any root path of $ \varphi $'s modal syntactic tree there exists at least one state accessible via this agent sequence.

The reason why we make a distinction between weak and strong privatization is that when applying a strongly privatized action model the resulting epistemic model need not necessarily be strongly but only weakly privatized, since whole clusters could get removed as a result of the update.

Definition 44 (Privatized) We call a pointed Kripke frame $ ({\cal{F}}, w) = (\langle S, R \rangle, w) $ (strongly) privatized with respect to formula $ \varphi \in \mathfrak{L}_{ {\rm{nsr}}{}} $ iff for any root path $ \sigma \in RootP(\varphi) $

Definition 45 (Weakly Privatized) Similarly we call a pointed Kripke frame $ ({\cal{F}}, w) = (\langle S, R \rangle, w) $ weakly privatized w.r.t. formula $ \varphi \in \mathfrak{L}_{ {\rm{nsr}}{}} $ iff for any root path $ \sigma \in RootP(\varphi) $

Definition 46 (Walk accessibility) For a pointed Kripke frame $ ({\cal{F}}, w) = (\langle W, R \rangle, w) $ we define walk accessibility operator

to be the set of agent-alternating walks starting from $ w $ and ending in $ u $. By $ \pi_k $ we denote the $ k $th projection function.

Walk accessibility yields an alternative equivalent definition of privatized frames:

Lemma 47 (Privatized alt.) A pointed Kripke frame $ ({\cal{F}}, w) $ is (strongly) privatized w.r.t. $ \varphi \in \mathfrak{L}_{ {\rm{nsr}}{}} $ iff for any root path $ \sigma \in RootP(\varphi) $

Proof: Follows from Defs. 37, 44, and 46. □

Lemma 48 (Weakly privatized alt.) A pointed Kripke frame $ ({\cal{F}}, w) $ is weakly privatized w.r.t. $ \varphi \in \mathfrak{L}_{ {\rm{nsr}}{}} $ iff for any root path $ \sigma \in RootP(\varphi) $

Proof: Follows from Defs. 37, 45 and 46. □

Theorem 49 For DBI formula $ \varphi $, the pointed action model $ ({\cal{U}}_\varphi, 0) $ as constructed by Algorithm 1 is privatized w.r.t. $ \varphi $.

Proof by induction on the recursive construction of $ \widetilde{ {\cal{U}}}_\varphi $ by Algorithm 2.

Ind. hyp.: Given DBI goal formula $ \varphi $, its proper subformula $ \varphi' $, and action model $ {\cal{U}} $ that does not contain any out-neighbors for agents in $ \text{ta}(\varphi') $, the $ u' $-sub model $ (\widetilde{ {\cal{U}}}_\varphi', u') $ after a recursive call $ { \text{CreateActionModel}}(\varphi', {\cal{U}}, u') $ is privatized w.r.t. $ \varphi' $, when not considering any loops at its point $ u' $.

Base case: For formula $ B_i \xi $, where $ \xi $ is propositional, since $ {AgSeq}(RootP(B_i \xi)) = \{\varepsilon, (i)\} $, we only need to check all states walk-accessible via these two sequences. Since in $ \widetilde{ {\cal{U}}}_{B_i \xi} $ the state $ m \notin \{0, -1\} $ is the only state accessible via an $ i $-edge from the root $ 0 $, as the $ 0 $ itself has no incoming arrows, $ {AgSeq}({WAcc}_{{\rm{nsr}}}(m, \widetilde{ {\cal{U}}}_{B_i \xi}, 0)) = \{i\} $. Furthermore the root $ 0 $ is only walk-accessible via the empty sequence $ \varepsilon $, therefore $ {AgSeq}({WAcc}_{{\rm{nsr}}}(0, \widetilde{ {\cal{U}}}_{B_i \xi}, 0)) = \{\varepsilon\} $. Lastly as the sink $ -1 $ is not walk-accessible via any of the two sequences $ \varepsilon $ and $ (i) $ in $ {AgSeq}(RootP(B_i \xi)) $ we conclude that $ (\widetilde{ {\cal{U}}}_{B_i \xi}, 0) $ is indeed privatized w.r.t. $ B_i \xi $.

Ind. step: If $ \varphi = B_i \psi $ for DBI normal formula $ \psi $, then $ (\widetilde{ {\cal{U}}}_\psi, u') $ the $ u' $-sub model returned by the recursive call of Algorithm 2 on line 6 is privatized w.r.t. $ \psi $, when considered without the reflexive $ i $ loop of $ u' $ by the IH. Since this recursive call on line 6. was the last line to execute, it follows that $ \widetilde{ {\cal{U}}}_\varphi = \widetilde{ {\cal{U}}}_\psi $. As $ i \notin \text{ta}(\psi) $ and the $ i $-edge from $ u $ to $ u' $ is the only outgoing edge connecting $ u $ with the $ u' $-sub model $ (\widetilde{ {\cal{U}}}_\varphi, u') $, we conclude that $ (\widetilde{ {\cal{U}}}_\varphi, u) $ is privatized with respect to $ \varphi $.

If $ \varphi = B_i(\xi \wedge \psi) $ for propositional formula $ \xi $ and DBI normal formula $ \psi $, the reasoning is analogous to the previous case, as privatization is a frame property and thus independent of the additional precondition added.

If $ \varphi = \varphi_1 \wedge \varphi_2 $, for DBI normal formulas $ \varphi_1 $ and $ \varphi_2 $, by the IH for the recursive function call on line 12. $ (\widetilde{ {\cal{U}}}_{\varphi_1}, u) $ is privatized w.r.t. $ \varphi_1 $. Since $ \text{ta}(\varphi_1) \cap \text{ta}(\varphi_2) = \varnothing $ it follows that $ RootP(\varphi) = RootP(\varphi_1) \sqcup RootP(\varphi_2) $, hence by the IH for the recursive call on line 13. the resulting model $ (\widetilde{ {\cal{U}}}_\varphi, u) $ is not only privatized w.r.t. $ \varphi_2 $, but remains privatized w.r.t. $ \varphi_1 $ as well, thus is privatized w.r.t. $ \varphi $.

Since by the initial call of Algorithm 2 on line 5 in Algorithm 1 $ {\cal{U}} $ consists only of the state $ 0 $ without any in- or outgoing edges and since the point of the resulting model $ \widetilde{ {\cal{U}}}_\varphi $ doesn't contain any incoming edges (in particular no loops), $ \widetilde{ {\cal{U}}}_\varphi $ is privatized w.r.t. $ \varphi $. It remains to investigate the execution of the call of Algorithm 4 on line 6, which however merely adds $ j $-arrows from states to the new $ -1 $ state if they don't already have outgoing $ j $-edges for every agent $ j $, therefore $ {\cal{U}}_\varphi $ is indeed privatized w.r.t. $ \varphi $. □

Lemma 50 Let the pointed update $ \bigl({\cal{M}}\odot {\cal{U}},(w,\alpha)\bigr) $ of a pointed Kripke model $ ({\cal{M}},w) $ with a pointed action model $ ({\cal{U}},\alpha) $ be defined. For any $ \rho \in \bigcup\limits_{l=0}^{\infty} {\cal{A}}^l $,

Proof Let $ {\cal{M}} = \langle S, R, V \rangle $, $ {\cal{U}} = \langle E, Q, pre \rangle $, and $ {\cal{M}}\odot {\cal{U}} = \langle S', R', V'\rangle $. We use induction on $ l = |\rho| $.

Base case $ l = 0 $: Since $ {\cal{A}}^0 = \{ \varepsilon\} $ the statement follows trivially from Defs 38 and 9.

Ind. step: Consider any agent sequence $ \overline{\rho} = \rho \circ i $ of length $ l+1 $ and state $ (x, \beta) \in C^{\overline{\rho}}_{ {\cal{M}} \odot {\cal{U}}, (w, \alpha)} $. By Definition 38, there must exist a state $ (v, \gamma) \in C^{\rho}_{ {\cal{M}} \odot {\cal{U}}, (w, \alpha)} $ such that $ (v, \gamma) R'_i (x, \beta) $, in particular, $ v R_i x $ and $ \gamma Q_i \beta $ by Definition 9. By IH for $ \rho $ of length $ l $, we have $ v \in C^{\rho}_{ {\cal{M}}, w} $ and $ \gamma \in C^{\rho}_{ {\cal{U}}, \alpha} $. Thus, by Definition 38 both $ x \in C^{\overline{\rho}}_{ {\cal{M}}, w} $ and $ \beta \in C^{\overline{\rho}}_{ {\cal{U}},\alpha} $. □

Theorem 51 For a pointed action model $ ({\cal{U}}, \alpha) $ privatized w.r.t. DBI formula $ \varphi $ and a pointed epistemic Kripke model $ ({\cal{M}}, w) $, if their pointed update exists, then $ ({\cal{M}} \odot {\cal{U}}, (w, \alpha)) $ is weakly privatized with respect to $ \varphi $.

Proof Suppose by contradiction that the pointed action model $ ({\cal{U}}, \alpha) $ is privatized w.r.t. $ \varphi $, but for some pointed Kripke model $ ({\cal{M}}, v) $, the update $ ({\cal{M}} \odot {\cal{U}}, (w, \alpha)) $ exists, however is not weakly privatized w.r.t. $ \varphi $. This means that there exists a root path $ \sigma \in RootP(\varphi) $, agent sequence $ \rho \in \bigcup\limits^{\infty}_{l=0} {\cal{A}}^l_{nsr} \setminus {AgSeq}(\sigma) $ and state $ (x, \beta) \in C^{\rho}_{ {\cal{M}} \odot {\cal{U}}, (w, \alpha)} $ and $ (x, \beta) \in C^{{AgSeq}(\sigma)}_{ {\cal{M}} \odot {\cal{U}}, (w, \alpha)} $. By Lemma 50 this implies that $ \beta \in C^{{AgSeq}(\sigma)}_{ {\cal{U}}, \alpha} $ and $ \beta \in C^{\rho}_{ {\cal{U}}, \alpha} $. However this contradicts the assumption that $ ({\cal{U}}, \alpha) $ is privatized w.r.t. $ \varphi $, as $ C^{{AgSeq}(\sigma)}_{ {\cal{U}}, \alpha} \cap C^{\rho}_{ {\cal{U}}, \alpha} = \varnothing $ by Definition 44. □

Theorem 52 For DBI formula $ \varphi $ and any pointed Kripke model $ ({\cal{M}}, v) $, the pointed update between $ ({\cal{U}}_\varphi, 0) $ (as synthesized by Algorithm 1) and $ ({\cal{M}}, v) $ is defined and $ ({\cal{M}} \odot {\cal{U}}, (w, \alpha)) $ is weakly privatized.

Proof Follows immediately from Theorems 25, 49, and 51. □

We presented a way to synthesize a pointed action model for a limited range of goal formulas that: (i) makes the goal formula true in the resulting model; (ii) privatizes any Kripke model to which it is applied to, thus breaking the common knowledge of the model assumption and simulating totally private communication; (iii) preserves consistency whenever possible, marking a difference from, e.g., van Ditmarsch et al.^[6]; and (iv) has minimal side effects, in the sense that it changes as few beliefs unspecified in the goal formula as possible. In addition, the synthesized pointed action models are combined with pointed Kripke models via the new pointed update operation, which does not apply to the whole model globally, but rather it respects the structure of the privatization introduced in the synthesis. Since the pointed update is a subset of the full product update operation, the proposed update mechanism is quite efficient: only the initial update increases the size of the model at worst linearly in the size of the goal formula, while all subsequent updates via goal formulas with the same belief structure (or substructure thereof) only decrease the model size. Compare this with the exponential blow up after iterated updates using the standard product updates.

Compared with existing synthesis methods our work presents the following advantages: the synthesis methods proposed in the literatures^[6,8] do not focus on issues of privatization and of minimal change, which is a strong shortcoming when considering applications to distributed systems. Recall that the goal of the synthesis tasks is, given a goal formula $ \varphi $, to output an update model that, applied to any initial model, outputs a model where $ \varphi $ holds. For some models however, $ \varphi $ could hold vacuously, in case e.g., there are no relations in the resulting model for a given agent involved in the formula. In our case, this is not possible: because of the proposed stratification of the model, an agent does not result in believing inconsistencies unless precisely instructed so by a sequence of updates. In other words, our synthesis method addresses belief consistency preservation, while other existing methods do not. While it is possible to construct AML or GAUL update models representing completely private communication^[9] and thus it is possible to synthesize them, there is no standardized update synthesis procedure for it. Finally, AAUL was proved to be undecidable^[22]. On the other hand, our language is a restriction of the standard doxastic language, and is hence decidable. Consequently, while not as powerful, it is computationally more appealing for the synthesis task.

We aim at extending the update mechanism so as to allow a wider range of goal formulas, introducing negations of modal operators, which might introduce ignorance, and disjunctions of modal operators, which have multiple possible realizations, while preserving the properties of privatization, minimality and consistency. Furthermore, we plan to introduce group updates, such as public announcements, providing full granularity in the update design.