Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Sufficient Epistemic Condition for Solving Stabilizing Agreement

Giorgio Cignarale, Stephan Felber, Hugo Rincon Galeana

TL;DR

This paper epistemically formalizes the conditions for solving stabilizing agreement, and identifies the knowledge that the agents acquire during any execution to choose a particular value under the authors' system assumptions.

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 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.

A Sufficient Epistemic Condition for Solving Stabilizing Agreement

TL;DR

This paper epistemically formalizes the conditions for solving stabilizing agreement, and identifies the knowledge that the agents acquire during any execution to choose a particular value under the authors' system assumptions.

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 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.
Paper Structure (5 sections, 1 theorem, 4 equations)

This paper contains 5 sections, 1 theorem, 4 equations.

Table of Contents

  1. Introduction
  2. Epistemic Framework
  3. Epistemic Modeling of Stabilizing Agreement
  4. An Epistemic Solution for Stabilizing Agreement
  5. Conclusion and Further Work

Key Result

theorem thmcountertheorem

Let $\mathcal{I}$ be an interpreted system consistent with choice determinism, local state introspection, perfect input recall, second depth broadcaster and largest mutually-known condition, then $\mathcal{I}$ is consistent with stabilizing agreement.

Theorems & Definitions (12)

  • definition thmcounterdefinition: Primitive value formula
  • definition thmcounterdefinition: Current primitive knowledge
  • definition thmcounterdefinition: Primitive knowledge limit
  • definition thmcounterdefinition: Current mutually-known primitive knowledge
  • definition thmcounterdefinition: Mutually-known primitive knowledge limit
  • definition thmcounterdefinition: Stable choice system
  • definition thmcounterdefinition: Stabilizing agreement
  • definition thmcounterdefinition: The Second Depth Broadcaster Condition
  • definition thmcounterdefinition: Value Selection Strategy
  • definition thmcounterdefinition: The Largest Mutually-Known Choice Condition
  • ...and 2 more