-
Consistent Update Synthesis via Privatized Beliefs
Authors:
Thomas Schlögl,
Roman Kuznets,
Giorgio Cignarale
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…
▽ More
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.
△ Less
Submitted 14 June, 2024;
originally announced June 2024.
-
A Sufficient Epistemic Condition for Solving Stabilizing Agreement
Authors:
Giorgio Cignarale,
Stephan Felber,
Hugo Rincon Galeana
Abstract:
In this paper we provide a first-ever epistemic formulation of stabilizing agreement, defined as the non-terminating variant of the well established consensus problem. In stabilizing agreements, agents are given (possibly different) initial values, with the goal to eventually always decide on the same value. While agents are allowed to change their decisions finitely often, they are required to ag…
▽ More
In this paper we provide a first-ever epistemic formulation of stabilizing agreement, defined as the non-terminating variant of the well established consensus problem. In stabilizing agreements, agents are given (possibly different) initial values, with the goal to eventually always decide on the same value. While agents are allowed to change their decisions finitely often, they are required to agree on the same value eventually. We capture these properties in temporal epistemic logic and we use the Runs and Systems framework to formally reason about stabilizing agreement problems. We then epistemically formalize the conditions for solving stabilizing agreement, and identify the knowledge that the agents acquire during any execution to choose a particular value under our system assumptions. This first formalization of a sufficient condition for solving stabilizing agreement sets the stage for a planned necessary and sufficient epistemic characterization of stabilizing agreement.
△ Less
Submitted 1 March, 2024;
originally announced March 2024.
-
A priori Belief Updates as a Method for Agent Self-Recovery
Authors:
Giorgio Cignarale,
Roman Kuznets
Abstract:
Standard epistemic logic is concerned with describing agents' epistemic attitudes given the current set of alternatives the agents consider possible. While distributed systems can (and often are) discussed without mentioning epistemics, it has been well established that epistemic phenomena lie at the heart of what agents, or processes, can and cannot do. Dynamic epistemic logic (DEL) aims to descr…
▽ More
Standard epistemic logic is concerned with describing agents' epistemic attitudes given the current set of alternatives the agents consider possible. While distributed systems can (and often are) discussed without mentioning epistemics, it has been well established that epistemic phenomena lie at the heart of what agents, or processes, can and cannot do. Dynamic epistemic logic (DEL) aims to describe how epistemic attitudes of the agents/processes change based on the new information they receive, e.g., based on their observations of events and actions in a distributed system. In a broader philosophical view, this appeals to an a posteriori kind of reasoning, where agents update the set of alternatives considered possible based on their "experiences."
Until recently, there was little incentive to formalize a priori reasoning, which plays a role in designing and maintaining distributed systems, e.g., in determining which states must be considered possible by agents in order to solve the distributed task at hand, and consequently in updating these states when unforeseen situations arise during runtime. With systems becoming more and more complex and large, the task of fixing design errors "on the fly" is shifted to individual agents, such as in the increasingly popular self-adaptive and self-organizing (SASO) systems. Rather than updating agents' a posteriori beliefs, this requires modifying their a priori beliefs about the system's global design and parameters.
The goal of this paper is to provide a formalization of such a priori reasoning by using standard epistemic semantic tools, including Kripke models and DEL-style updates, and provide heuristics that would pave the way to streamlining this inherently non-deterministic and ad hoc process for SASO systems.
△ Less
Submitted 11 December, 2023;
originally announced December 2023.
