Consistent update synthesis via privatized beliefs

Abstract

Dynamic Epistemic Logic (DEL) formalizes communication in the form of model-transforming updates. Private communication is key in distributed systems, as processes exchanging information about their private local state should not be detectable by others. This focus on privacy clashes with the standard DEL assumption that updates are applied to the whole Kripke model, which is commonly known by all agents, potentially leading to information leakage. 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 that stratifies a pointed Kripke model into private agent-clusters, each representing the local knowledge of the processes: Given a goal formula representing private communication, we provide a procedure to construct an action model that: (a) makes the goal formula true; (b) maintains consistency of agents' beliefs, if possible; and (c) ensures minimal change of 'unrelated' beliefs. (II) We introduce a new operation between pointed Kripke models and pointed action models called pointed updates that, unlike the product update operation of DEL, maintains only the subset of the world-event pairs that are reachable from the point, without unnecessarily blowing up the model size.