Consistent Update Synthesis via Privatized Beliefs

TL;DR

To represent leak-free agent-to-agent communication, a way to synthesize an action model which stratifies a pointed Kripke model into private agent-clusters, each representing the local knowledge of the processes is introduced.

Abstract

Kripke models are an effective and widely used tool for representing epistemic attitudes of agents in multi-agent systems, including distributed systems. Dynamic Epistemic Logic (DEL) adds communication in the form of model transforming updates. Private communication is key in distributed systems as processes exchanging (potentially corrupted) information about their private local state should not be detectable by any other processes. This focus on privacy clashes with the standard DEL assumption for which updates are applied to the whole Kripke model, which is usually commonly known by all agents, potentially leading to information leakage. In addition, a commonly known model cannot minimize the corruption of agents' local states due to fault information dissemination. The contribution of this paper is twofold: (I) To represent leak-free agent-to-agent communication, we introduce a way to synthesize an action model which stratifies a pointed Kripke model into private agent-clusters, each representing the local knowledge of the processes: Given a goal formula $\varphi$ representing the effect of private communication, we provide a procedure to construct an action model that (a) makes the goal formula true, (b) maintain consistency of agents' beliefs, if possible, without causing "unrelated" beliefs (minimal change) thus minimizing the corruption of local states in case of inconsistent information. (II) We introduce a new operation between pointed Kripke models and pointed action models called pointed updates which, unlike the product update operation of DEL, maintain only the subset of the world-event pairs that are reachable from the point, without unnecessarily blowing up the model size.

Figures (9)

• Figure 1: Left: Initial pointed Kripke model $\mathcal{M}$. Right: Updated model $\mathcal{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$.
• Figure 2: Left: Initial (pointed) Kripke model $\mathcal{M}$ where agent $a$ and $b$ are uncertain about whether $p$ or $\lnot p$ is true. Right: (Pointed) action model $\mathcal{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., $\mathsf{pre}(\beta) = \varphi$.
• Figure 3: Left: First product update $\mathcal{M} \otimes \mathcal{U}$ of Kripke model $\mathcal{M}$ with action model $\mathcal{U}$. Right: Second product update $(\mathcal{M} \otimes \mathcal{U}) \otimes \mathcal{U}$ with the same action model $\mathcal{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((\mathcal{M} \otimes \mathcal{U})\otimes \mathcal{U}\bigr)\otimes \mathcal{U}$ with the same action model $\mathcal{U}$.
• Figure 5: Intermediate stages in constructing action model $\mathcal{U}_\varphi$ for DBI formula \ref{['blt_goal']} from Example \ref{['Ex:BLT']} based on its DBI normal form $\varphi=B_b(B_t p \land B_l(p \land B_t p))$.

Theorems & Definitions (58)

• Example 1: Balder--Loki--Thor example
• Definition 2
• Definition 3: Kripke frame
• Definition 4: Pointed Kripke model
• Definition 5: Pointed action model
• Definition 6: Product update
• Definition 7: Pointed update
• Definition 8: Bisimulation
• Definition 9: Equivalences
• Theorem 10: Bisimilarity implies modal equivalence