arXiv CSopen access

Self-Correcting Gossip Protocols

arXiv:2605.05801v1 [cs.LO] 7 May 2026

Self-Correcting Gossip Protocols Giorgio Cignarale Hans van Ditmarsch∗ Stephan Felber Malvin Gattinger Hugo Rincon Galeana Vaishnavi Sundararajan

Abstract We investigate self-correcting gossip protocols with errors. In distributed computing, protocols with errors have been widely investigated in temporal epistemic logics. Instead, we propose a dynamic epistemic logic. We show how to correct transmission errors due to faulty messages without a central authority coordinating protocol execution, how this affects optimality, and how this compares to bounded memory and full information protocols.

1

Introduction

In gossip protocols [24, 6, 36, 17, 19, 5, 3, 35, 8, 33], given a set of n agents, each agent knows a single secret (we can think of this as the identity of that agent, or as all the agent knows); when agents call each other, they exchange all secrets they know; and the goal is for all agents to become experts, that is, to know all secrets. Here, we assume that all agents can call each other (are all neighbours), so that there are no network constraints, and we also assume that messages are always received. A stronger epistemic goal is that all agents are super experts, that is, all agents know that all agents know all secrets. If only secrets are exchanged, even higher-order epistemic goals are unreachable [29]. The usual assumption in epistemic gossip protocols is that message transmission is correct, and that agents behave correctly. Under these assumptions, and in the absence of network constraints, 2n − 4 calls are optimal to reach the goal that all become experts   n [24], and n − 2 + 2 calls are optimal to reach the goal that all become super experts [29]. What epistemic goals are still reachable and how is optimality affected when transmission errors may occur during a call, and when agents may behave incorrectly? In distributed computing, bounds on transmission errors are investigated in population protocols [4], the epistemic consequences of faulty behaviour is investigated in [20, 13], and self-correction (self-stabilization) is investigated in [9, 11, 10]. Faulty agents in epistemic gossip protocols ∗

Author affiliations of Giorgio, Stephan: TU Wien, Austria; Hans: CNRS, IRIT, University of Toulouse, France; Malvin: ILLC, University of Amsterdam, Netherlands; Hugo: TU Berlin, Germany; Vaishnavi: IIT Delhi, India. Hans van Ditmarsch, [email protected], is corresponding author. We acknowledge substantial contributions from Roman Kuznets and Ulrich Schmid to this work.

1

have been investigated in [25, 26, 14]. In [26] the authors investigate how the presence of unreliable agents affects whether the gossip protocol can terminate successfully (that is, whether all agents get to know all secrets). They investigate this for dynamic gossip [35] wherein agents not only exchange secrets but also numbers (relaxing network constraints), and for various epistemic gossip protocols including the protocol called LNS wherein one can only call a neighbour if one does not know her secret. They not only require that all reliable agents get to know the secrets of all reliable agents, but also that the reliable agents get to know who the unreliable agents are — the latter is an uncommon requirement in distributed computing. Publication [25] is a precursor of [26], and [14] is a follow-up proposing yet other variations of LNS for unreliable agents. In this work we investigate in depth what happens when at most one transmission error may occur during protocol execution. We assume synchronous communication where agents are only aware of the calls involving them but are aware of a global clock. We show how a transmission error may cause false beliefs, how to correct this without a central authority coordinating protocol execution and how then to obtain epistemic protocol goals. We do not investigate optimality except by examples demonstrating that lower bounds must be higher. We show how our approach compares to (weaker) bounded memory protocols [12] and to (stronger) full information protocols [22]. We later wish to pursue how the same or a similar formalization can be used for self-correcting gossip protocols with at most f faulty messages or with at most f faulty (Byzantine) agents, and for an asynchronous setting.

2

Gossip with at most one transmission error

2.1

Structures, syntax and semantics

Secret distributions Let a set of n agents A = {a1 , . . . , an } be given. We typically assume few agents in which case they are named a, b, c, . . . instead. Given the agents A, the set of secrets is the product A × {0, 1}, where for (a, 1) we write a and for (a, 0) we write a. The overloaded use of agent names as secret values is disambiguated by context. If B ⊆ A × {0, 1} is a subset of secrets, we define the swap ±a of the values for the secret of agent a in that set as B ±a := B[a/a, a/a] (if a is in B replace it by a and simultaneously if a is in B replace it by a). Note that (B ±a )±a = B, and if B has no information on a then B ±a = B. Definition 1 (Secret distribution) A secret distribution is a function S : A → P(A × {0, 1}) For S(a) we write Sa (the holding of a). In an initial secret distribution S, for all a ∈ A, Sa = {a} or Sa = {a}. The set of initial secret distributions is I. In the initial secret distribution denoted I, for all a ∈ A, Ia = {a}. ⊣

2

A secret distribution lists for each agent what secrets that agent holds and what their values are. We let Sa∩b denote Sa ∩ {b, b}. This is the set of values that agent a holds for secret b. It is convenient to have an abbreviated notation for secret distributions: a lexicographically ordered list of n holdings of secrets Sa , Sb , . . . that are separated by vertical bars |, where each Sa is also written as an ordered list but without separation symbols (so {a, b, c} becomes abc), and where holding two values b and b for the same secret is represented as a conflicting value b. We can thus view the secrets Sa held by agent a as an annotated subset B of A. An example is secret distribution S = abc|abc|abc|d, wherein Sa = {a, b, c, c}, etcetera. We often assume the initial secret distribution I, for example a|b|c|d. In error-free gossip, at any stage an agent a holds some subset B ⊆ A of all secrets, including its own, and secret distributions are n-tuples B1 | . . . |Bn with B1 , . . . , Bn ⊆ A. By assuming any such secret b ∈ A held by a to be a secret value (b, 1) in our setting with errors, such error-free secret distributions are now special cases, such as a|b|c|d above. Call and call sequence In error-free gossip a call is a pair (a, b) where a ̸= b ∈ A, denoted ab, and which means that a calls b, and wherein the agents exchange all their (values of) secrets. We say that a and b are involved in the call. In gossip with errors, ab is a correct call and we also consider a faulty call ac b where in the call from a to b there is a transmission error made in the secret c held by a, so that b receives the other value for secret c. Similarly we define abc where in the call from a to b there is a transmission error made in the secret c known by b. Both a correct call and a faulty call are now a call. An arbitrary call is denoted κ (for ‘singleton κall sequence’), and an arbitrary call between a and b, in either direction, is denoted abκ . Definition 2 (Call sequence) A call sequence is a finite sequence of calls containing at most one faulty call. Call sequences are denoted σ, τ , and ϵ is the empty call sequence. We let σ ⊑ τ mean that call sequence σ is a prefix of call sequence τ , and σ.τ is concatenation of call sequences. ⊣ Syntax The set of atoms (propositional variables) P is the product (A × {0, 1}) × A where, analogously to the convention for secrets, for ((b, 0), a) we write ba and for ((b, 1), a) we write ba . Definition 3 (Logical language) The logical language consists of formulas φ ::= ba | ba | ¬φ | φ ∧ φ | Ka φ

⊣

Other propositional connectives are defined by notational abbreviation, Ka φ stands for ‘agent a knows that φ’, K̂a φ := ¬Ka ¬φ stands for ‘agent a considers φ possible’, EB φ := V a∈B Ka φ means that everyone in B knows φ (φ is mutual knowledge among the agents in B). In error-free gossip ba means that agent a knows or holds the secret of agent b. In our setting with errors ba means that a holds value b of the secret of b whereas ba means 3

that a holds value b of secret b. We finally define Kv a b := Ka bb ∨ Ka bb , for ‘agent a knows (the value of) the secret of b’ or ‘a knows secret b’. (The notation for knowing value is reminiscent of notation Kw a p for ‘knowing whether p’, defined as Ka p ∨ Ka ¬p.) After introducing the semantics we will show how all these epistemic readings relate. Definitions 4, 5 and 6 of respectively the semantics of a call, the observation relation, and the semantics of formulas, are defined by simultaneous induction. Semantics of a call In a call the agents exchange all the secrets they know. The semantics of a call do not depend on the direction of the call, so the semantics of calls ab and ba are the same. A call from agent a to agent b affects the secret distribution. In standard gossip, if a holds X ⊆ A and b holds Y ⊆ A, then after the call agents a and b both hold X ∪ Y . For gossip with errors the semantics of a call are slightly more complex: given set of values of secrets X and Y we still take their union, except when the agent already knew the correct value of a secret d before the call, and also when the agent knows the correct value of a secret d after the call. In those cases, if the union of X and Y contains conflicting values d and d for d, we then remove the value that is known to be incorrect. Definition 4 (Semantics of call) Given an initial secret distribution S and a call sequence σ, the secret distribution S[σ] is defined by induction on σ. For the basis, S[ϵ] := S. For the induction, given call sequence σ and a, b, c, d ∈ A with a ̸= b and d ̸= a, b: S[σ.ab]a = S[σ.ba]a = S[σ.ac b]a = S[σ.bac ]a = (S[σ]a ∪ S[σ]b \∗)\∗∗ S[σ.abc ]a = S[σ.bc a]a = (S[σ]a ∪ S[σ]±c b \∗)\∗∗ c c S[σ.bd]a = S[σ.b d]a = S[σ.bd ]a = S[σ]a The set ∗ consists of known incorrect values of secrets by agent a after call sequence σ. The set ∗ is defined as: ∗ = {d | S, σ |= Ka dd } ∪ {d | S, σ |= Ka dd }. The set ∗∗ is defined as follows. For abκ = ab, ba, ac b, bac the set ∗∗ consists of all secret values d such that T, τ |= dd for all initial secret distributions T and call sequences τ with (S, σ) ∼a (T, τ ) and S[σ]b = T [τ ]b , and all secret values d such that T, τ |= dd for all T, τ with (S, σ) ∼a (T, τ ) and S[σ]b = T [τ ]b . For abκ = abc , bc a we replace T [τ ]b by T [τ ]±c ⊣ b . In the definition above, |= is the satisfaction relation of Definition 6, below. The set ∗∗ is defined in a roundabout way for technical reasons: as the ∗∗-discarded values define the semantics of a call abκ , we cannot use the more intuitive formulation that set ∗∗ consists of the known incorrect values after sequence σ.abκ , as that would be circular. However, we can still ‘think’ of agent a first receiving the holding of agent b, then concluding she now knows a secret d as a result of that, and finally ∗∗-discarding the value of that secret she now knows to be incorrect. All this is combined in the semantics of a single call. The sets ∗ and ∗∗ can both be considered forms of self-correction. Intuitively, the set ∗ consists of values of secrets contributed by agent b that agent a refuses to incorporate because she already knows the correct values of those secrets (in case she had self-corrected 4

for those secrets, then she already did so in the past). Whereas intuitively the set ∗∗ consists of the values of secrets that agent a got to know during the call involving a and b and for which she had a conflict before that call, and that she then discards. Set ∗ is self-correction in the form of persistence of correct values; ‘refusal’ to accept incorrect values. Whereas ∗∗ is self-correction in the form of ‘discarding’ values held before the call. As there is at most one transmission error, sets ∗ and ∗∗ can only be about the same unique secret d in a given call sequence and cannot both be non-empty. But the semantics is presented in a general form that is also suitable for multiple errors. From here on, S and T always denote initial secret distributions (while still being declared as such) while non-initial secret distributions always take shape S[σ], T [τ ], I[σ], etcetera. Observation model The observation model M(I) is the Kripke model (W, ∼, V ) where domain W consists of gossip states (S, σ) for initial secret distributions S ∈ I and call sequences σ, where for each a ∈ A observation relation ∼a between gossip states is defined below, and where valuation V maps a gossip state to a secret distribution such that V (S, σ) = S[σ]. Definition 5 (Observation relation) The observation relation is the equivalence closure of the following recursive clauses by call sequence length, where S and T are initial secret distributions, and where a, b, c, d, e, f, g ∈ A with a ̸= b and c, d, f, g ̸= a, and the clauses for the other direction of the call between a and b, and for the other direction of the faulty call between c and d, are the same. (S, ϵ) ∼a (T, ϵ) (S, σ.ab) ∼a (T, τ.ab) (S, σ.ab) ∼a (T, τ.ae b) (S, σ.ab) ∼a (T, τ.abe ) (S, σ.cd) ∼a (T, τ.f g) (S, σ.ce d) ∼a (T, τ.f g)

iff iff iff iff iff iff

Sa = Ta (S, σ) ∼a (T, τ ) and S[σ]b = T [τ ]b (S, σ) ∼a (T, τ ) and S[σ]b = T [τ ]b (S, σ) ∼a (T, τ ) and S[σ]b = T [τ ]±e b (S, σ) ∼a (T, τ ) (S, σ) ∼a (T, τ )

⊣

If (S, σ) ∼a (T, τ ), then |σ| = |τ |. We note that ∼a therefore defines a synchronous observation relation [19, 5, 3, 33]: agents are only aware of calls involving them, but are still aware that a call took place if they were not involved in a call; calls are scheduled in ‘rounds’ consisting of single calls thus defining a global clock. In error-free gossip we only need to consider the initial secret distribution I, we therefore omit that parameter, and then define: ϵ ∼a ϵ, σ.ab ∼a τ.ab iff σ ∼a τ and σb = τb , and σ.cd ∼a τ.f g iff σ ∼a τ (I[σ]b is then denoted σb ) [31, 34]. In the definition of the observation relation, the restriction to call sequences containing at most one transmission error is only implicit. Given (S, σ) ∼a (T, τ ), in case τ contains a faulty call, the extension of τ with ae b or abe is not a call sequence. So, turning the matter around, the clauses involving τ.ae b and τ.abe in the definition imply that τ contains no faulty calls. This means that equivalence classes of ∼a indistinguishable gossip states 5

for sequences σ involving more and more calls, involve fewer and fewer initial secret distributions S, thus eventually resulting in knowledge of secrets, namely when only one secret distribution is considered possible by the agent. Semantics of formulas The formulas of the logical language are interpreted in the observation model. Definition 6 (Semantics) Given a gossip state (S, σ), the semantics are defined by induction on formula structure. S, σ |= ba S, σ |= ba S, σ |= ¬φ S, σ |= φ ∧ ψ S, σ |= Ka φ

iff iff iff iff iff

b ∈ S[σ]a b ∈ S[σ]a S, σ ̸|= φ S, σ |= φ and S, σ |= ψ T, τ |= φ for all (T, τ ) ∼a (S, σ)

A formula φ is valid, notation |= φ, if S, σ |= φ for all initial secret distributions S and call sequences σ. ⊣ Given initial secret distribution S and call sequence σ, a holds the correct value of secret b if Sb ⊆ S[σ]∩b a (inclusion, because a may hold conflicting values), and a knows the (correct) value of secret b if S, σ |= Kv a b, which implies that Sb = S[σ]∩b a (Proposition 13 and its consequences, later). Knowing a secret implies the value is correct. A value is faulty if it is not correct. There are a whole lot of epistemic or vaguely epistemic readings by now. Let us list them here all together in order to put it in proper perspective. We also attach an epistemic reading to combinations of certain values, as in our setting errors are rare. • ba means that a holds value b of the secret of b; • ba means that a holds value b of the secret of b. • ba ∧ ¬ba means that a believes that the secret of b is b; • ¬ba ∧ ba means that a believes that the secret of b is b; • bb ∧ ba ∧ ¬ba means that a correctly believes that the secret of b is b; • bb ∧ ¬ba ∧ ba means that a correctly believes that the secret of b is b; • ¬bb ∧ ba ∧ ¬ba means that a incorrectly believes that the secret of b is b; • ¬bb ∧ ¬ba ∧ ba means that a incorrectly believes that the secret of b is b; • ba ∧ ba means that a has conflicting/inconsistent beliefs about the secret of b; • ¬ba ∧ ¬ba means that a has no beliefs about the secret of b; 6

• Kv a b means that a knows the secret of b (that a knows the value of the secret of b). We recall that Kv a b is defined as Ka bb ∨ Ka bb . We will show that Kv a b → (bb ∧ ba ∧ ¬ba ) ∨ (bb ∧ ¬ba ∧ ba ). Knowledge implies correct belief. However, correct belief does not imply knowledge (of which the simplest example is that I, ab |= bb ∧ ba ∧ ¬ba whereas I, ab ̸|= Kv a b, see also Example 15). In our setting, knowledge is justified correct belief. In the final section we summarily discuss the introduction of belief (quasi-)modalities for some of the above. The semantics are well-defined On the one hand, observation relations ∼a for agent a in the observation model are between gossip states (S, σ) that are valued as secret distributions S[σ] and such secret distributions S[σ] depend on what agent b knows and thus on |= (whether S, σ |= Kv b c for secrets c). On the other hand, the satisfaction relation |= defines what agent b knows as a function of the observation relation ∼b , of which the definition depends on the holding T [τ ]b of agent b in secret distributions T [τ ]. We should therefore show that the logical semantics are well-defined. Consider the following order < on pairs of call sequences and formulas: (σ, φ) < (τ, ψ) iff (|σ| = |τ | and φ is a strict subformula of ψ) or |σ| < |τ | Note that this is a well-founded partial order. Satisfaction relation With a clause S, σ |= φ we associate a pair (σ, φ). All definiens of the inductive clauses of the definition of |= satisfy the order <: (σ, φ) < (σ, ¬φ), (σ, φ) < (σ, φ ∧ ψ), and (τ, φ) < (σ, Ka φ), where we observe that |τ | = |σ|. For the basic clauses S, σ |= ba and S, σ |= ba we need to use the inductive definition of S[σ]. Let us deal with ba where ba is handled similarly. If σ = ϵ, then we check whether b = a and {a} = Sa (a pair (ϵ, ba ) is at the bottom of the order). For the cases σ = τ.acκ we use that: (τ, ba ) < (τ.ac, ba ), (τ.ad c, ba ) and (τ, bc ) < (τ.ac, ba ), (τ.ad c, ba ) or even, when the precall is faulty about b, (τ, bc ) < (τ.acb , ba ), whereas if σ = τ.cdκ we more straightforwardly have that (τ, ba ) < (τ.cdκ , ba ). Observation relation With a clause (S, σ) ∼a (T, τ ) we associate pairs (σ, φ) and (τ, φ) for any φ. We thus get that (σ, φ), (τ, φ) < (σ.abκ , φ), (τ.abκ , φ) because |τ | = |σ| < |σ.abκ | = |τ.abκ |. Similarly, (σ, φ), (τ, φ) < (σ.cdκ , φ), (τ.ef κ , φ). This takes care of the ∼a part of the definiens. However, we also need to show that the identification of holdings in the definiens can be carried out. For that we use that (σ, cb ) < (σ.abκ , cb ) and (σ, cb ) < (σ.abκ , cb ) for arbitrary secrets c held by an agent b in S[σ]b , and we proceed similarly for T [τ ]b and T [τ ]±e b . Secret distribution With a clause S[σ]a (for any a) we associate a pair (σ, φ) for any φ. We thus get that (σ, Kv a d) < (σ.abκ , da ), (σ.abκ , da ), because |σ| < |σ.abκ |, so that the test whether S, σ |= Kv a d, required to determine S[σ.abκ ]a , is well-defined. Finally we have that (σ, da ) < (σ.bcκ , da ) and (σ, da ) < (σ.bcκ , da ) for b, c ̸= a. A Lean implementation for this logical semantics is available at https://m4lvin. github.io/Gossip-in-Lean/docs/Gossip/Error/Basic.html and is also summarily described in the Appendix. 7

2.2

Semantic results

As the knowledge modality is interpreted on structures with equivalence relations, we get the usual validities and validity preservations for knowledge [32]: |= Ka φ → φ (T) |= Ka φ → Ka Ka φ (4) |= ¬Ka φ → Ka ¬Ka φ (5)

|= Ka (φ → ψ) → Ka φ → Ka ψ (K) |= φ implies |= Ka φ (Nec)

As a sanity check we show a number of elementary properties of the observation relation and the epistemic semantics. First in line is that when two gossip states are indistinguishable for an agent, then the agent must hold the same values of secrets in both. Lemma 7 (S, σ) ∼a (T, τ ) implies S[σ]a = T [τ ]a .

⊣

Proof The proof is by induction on the length of call sequence σ. If σ = ϵ, then σ = τ = ϵ, and (S, ϵ) ∼a (T, ϵ) implies that Sa = Ta . Let now σ = σ ′ .κ where call κ involves agents a and b. We observe that τ must then have shape τ ′ .κ′ where κ′ also involves a and b (and where the direction of the call is the same in κ and κ′ ). In all such cases, by the definition of the observation relation it then follows from (S, σ ′ .κ) ∼a (T, τ ′ .κ′ ) that (S, σ ′ ) ∼a (T, τ ′ ) so that by inductive assumption we already have S[σ ′ ]a = T [τ ′ ]a . We now distinguish the different cases. If κ = ab and κ′ is ab or ae b, then from (S, σ ′ .κ) ∼a (T, τ ′ .κ′ ) we also obtain that S[σ ′ ]b = T [τ ′ ]b . From that and S[σ ′ ]a = T [τ ′ ]a we then obtain that S[σ ′ ]a ∪ S[σ ′ ]b = T [τ ′ ]a ∪ T [τ ′ ]b and therefore also, as a’s knowledge is the same in (S, σ ′ ) and (T, τ ′ ), that S[σ ′ ]a ∪ S[σ ′ ]b \∗ = T [τ ′ ]a ∪ T [τ ′ ]b \∗. Furthermore, as (S, σ ′ ) ∼a (T, τ ′ ) and S[σ ′ ]b = T [τ ′ ], we also have that (S[σ ′ ]a ∪ S[σ ′ ]b \∗)\∗∗ = (T [τ ′ ]a ∪ T [τ ′ ]b \∗)\∗∗, which means by definition that S[σ ′ .κ]a = T [τ ′ .κ]a . If κ′ is abe we proceed almost as before, except that from (S, σ ′ .κ) ∼a (T, τ ′ .κ′ ) we now ′ e obtain that S[σ ′ ]b = T [τ ′ ]±e b , and then determine a’s novel holding of values in (T, τ .ab ) ′ ′ ±e as (T [τ ]a ∪ T [τ ]b \∗)\∗∗, wherein the value of e is swapped. All other cases for calls κ involving a and b proceed similarly (using symmetric closure of the definition of the observation relation). Let finally σ = σ ′ .bcκ where call bcκ involves agents b and c (in either order) different ′ from a. Then τ must have shape τ = τ ′ .deκ for some d, e ̸= a. From (S, σ ′ .bcκ ) ∼a ′ (T, τ ′ .deκ ) we then obtain that (S, σ ′ ) ∼a (T, τ ′ ) so that by inductive assumption we ′ already have S[σ ′ ]a = T [τ ′ ]a and therefore as well S[σ ′ .bcκ ]a = T [τ ′ .deκ ]a , as required. □ As our structures are distributed systems where all propositional variables are local to agents, the truth value of an atom local to agent a (‘held by a’) is known by that agent. This is also entirely as expected. Lemma 8 (Locality) |= ba → Ka ba , |= ¬ba → Ka ¬ba , |= ba → Ka ba , and |= ¬ba → Ka ¬ba . ⊣ 8

Proof According to the logical semantics variables ba and ba are local to agent a, that is S, σ |= ba iff b ∈ S[σ]a and S, σ |= ba iff b ∈ S[σ]a . The required then follows from that, the semantics of knowledge, and Lemma 7 that (S, σ) ∼a (T, τ ) implies S[σ]a = T [τ ]a . □ The next Lemma 9 says that own secrets (the value of secret a held by agent a) are preserved. This is a consequence of the modelling assumption that all agents initially only hold their own secret. We call this stubbornness as it implies that even when later confronted with another value for their own secret, agents will always refuse to accept that incorrect value. Note that we do not require or stipulate this property in our semantics, but that it can be shown, it is a consequence of the semantics as defined. Lemma 9 (Stubbornness) (i) S, ϵ |= aa implies S, σ |= aa , and (ii) S, ϵ |= aa implies ⊣ S, σ |= aa . Proof We show the first, where the second follows similarly. The proof is by induction on the length of call sequences σ. Assume S, ϵ |= aa . For σ = ϵ it is trivial. Let now σ = τ.κ. By induction we may assume that S, ϵ |= aa implies S, σ |= aa . Therefore S, σ |= aa . We now have to show that for an arbitrary next call κ, S, σ.κ |= aa . Consider Definition 4 of the call semantics. If agent a is not involved in κ, S[σ.κ]a = S[σ]a . Therefore, as a ∈ S[σ]a , also a ∈ S[σ.κ]a . If agent a is involved in κ, we take the union of the holdings of agent a and of the other agent involved in that call, let us say b, with the exception of the values withheld in the ∗ and the ∗∗ sets. So, if we can prove that secret value a is never a member of ∗ or ∗∗, it must be in that union, so that again a ∈ S[σ.κ]a . Concerning ∗, the secret value withheld is the value that is different from the value that is known by agent a. We now observe that from S, σ |= aa and Locality Lemma 8 it follows that S, σ |= Ka aa . Therefore a ∈ / ∗. Concerning ∗∗, the secret value withheld is the value that is different from the value such that for all (T, τ ) such that (T, τ ) ∼a (S, σ) and another requirement on b, gossip state (T, τ ) makes true that value. As S, σ |= Ka aa , therefore T, τ |= aa . So a∈ / ∗∗. As a ∈ / ∗ and a ∈ / ∗∗, again we conclude that a ∈ S[σ.κ]a . □ As the result holds for value a and for value a, and as an agent initially only holds a single value for its own secret, therefore an agent always only holds a single value for its own secret. A different way to describe this result is to say that for all initial secret distributions S and call sequences σ, Sa = S[σ]∩a a . Lemma 10 (Knowledge of secrets is preserved) (i) S, σ |= Ka bb and σ ⊑ τ implies S, τ |= Ka bb , and (ii) S, σ |= Ka bb and σ ⊑ τ implies S, τ |= Ka bb . ⊣ Proof We show the first, where the proof of the second is similar. The proof is by induction on the length of τ \σ. If τ \σ = ϵ then σ = τ and it is trivial. Let us now show this for τ.κ, on the inductive assumption it holds for τ with σ ⊑ τ . Therefore assume arbitrary (S ′ , τ ′′ ) such that (S ′ , τ ′′ ) ∼a (S, τ.κ). If agent a is not involved in κ, from the definition of ∼a it follows that we already had (S ′ , τ ′′ ) ∼a (S, τ ). From that and inductive assumption S, τ |= Ka bb we then get S ′ , τ ′′ |= bb , and therefore S, τ.κ |= Ka bb . If agent a is involved 9

in κ, then τ ′′ must have shape τ ′ .κ′ . We then have (S ′ , τ ′ .κ′ ) ∼a (S, τ.κ), and from the definition of ∼a it then follows that we already must have had that (S ′ , τ ′ ) ∼a (S, τ ). From that and inductive assumption S, τ |= Ka bb it now follows that for all such (S ′ , τ ′ ) we have that S ′ , τ ′ |= bb . From that and Stubbornness Lemma 9 it then follows that S ′ , τ ′ .κ′ |= bb . As (S ′ , τ ′ .κ′ ) was arbitrary, therefore S, τ.κ |= Ka bb . □ As a corrollary of Lemma 10 we obviously have that: Corollary 11 S, σ |= Kv a b and σ ⊑ τ implies S, τ |= Kv a b.

⊣

This seems to describe Lemma 10 more succinctly and intuitively. But it is slightly weaker, as the formulation does not rule out that S, σ |= Ka bb whereas S, σ.κ |= Ka bb . Although knowledge of secrets is preserved, belief of secrets may not be preserved: if Ka bb is true now it remains true forever, whereas if Ka ba is true now it may be false after error correction such that Ka ¬ba is true later (and such that Ka ba is then false, as this is inconsistent with Ka ¬ba ). In the next Proposition 13 we show that knowledge implies correct belief. In the proof of item (i) of this proposition we need a lemma, that we therefore present first. This Lemma 12 requires additional terminology. For arbitrary initial secret distributions S we define S ±b as the initial secret distribution that is like S except that agent b holds the other value of its own secret, that is, using our already defined notation for swapping values in secret holdings, (S ±b )b = Sb±b (= S[ϵ]±b b ), ±b and for all d ̸= b, (S )d = Sd . Furthermore, for arbitrary call sequences σ we define cor b (σ) as the call sequence that is either σ or wherein, if σ contains a faulty call with a transmission error for (the value of) secret b, this faulty call is replaced by a correct call between the same agents: cor b (ϵ) := ϵ, cor b (σ.ac) := cor b (σ).ac, cor b (σ.ad c) := cor b (σ).ad c and cor b (σ.acd ) := cor b (σ).acd (where d ̸= b), cor b (σ.ab c) = cor b (σ.acb ) := cor b (σ).ac.1 Lemma 12 For all initial secret distributions S, call sequences σ, and agents a, b ∈ A: If ±b 2 ∩b ⊣ Sb = {b}, and S[σ]∩b a = ∅ or S[σ]a = {b}, then (S, σ) ∼a (S , cor b (σ)). Proof The proof is by induction on the length of σ and by further case distinction. The lemma’s formulation and stubbornness implies that a ̸= b. Base case ϵ ±b We must have that S[σ]∩b a = ∅. Also, (S, ϵ) ∼a (S , ϵ) follows from the basic clause of ∼a , because Sa = Sa±b = {a} or Sa = Sa±b = {a}: both singletons only contain the secret of a. Therefore, as cor b (ϵ) = ϵ, (S, ϵ) ∼a (S ±b , cor b (ϵ)). Inductive case σ.κ ∩b If κ does not involve agent a, then S[σ.κ]∩b a = S[σ]a , so that either way (∅ or {b}) by For example, cor b (ab.ab c.cd) = ab.ac.cd, wherein the transmission error for secret b is corrected; cor b (ab.acc.cd) = ab.acc.cd, although there was a transmission error, it was for another secret than b; cor b (ab.ac.cd) = ab.ac.cd, as there was no transmission error. 2 ∩b Obviously we also have, with the roles of b and b swapped: If Sb = {b}, and S[σ]∩b a = ∅ or S[σ]a = {b}, ±b then (S, σ) ∼a (S , cor b (σ)). By analogy that is needed in item (ii) of Proposition 13. 1

10

induction we obtain (S, σ) ∼a (S ±b , cor b (σ)), and therefore as well, as κ does not involve agent a, (S, σ.κ) ∼a (S ±b , cor b (σ).cor b (κ)). Now it is easy to see that for arbitrary σ and τ , cor b (σ.τ ) = cor b (σ).cor b (τ ). Therefore (S, σ.κ) ∼a (S ±b , cor b (σ.κ)). Let now κ involve agent a and an arbitrary other agent c. ∩b ∩b ∩b ∩b If S[σ.κ]∩b a = ∅ then already S[σ]a = ∅ or S[σ]a = {b}, and S[σ]c = ∅ or S[σ]c = {b} (we can rule out that either set contains b as correct values are never discarded in the call semantics). By induction for agents a and c we then obtain that (S, σ) ∼a (S ±b , cor b (σ)) respectively (S, σ) ∼c (S ±b , cor b (σ)), and from the latter we obtain S[σ]c = S ±b [cor b (σ)]c . Now if κ is a correct call, from (S, σ) ∼a (S ±b , cor b (σ)) and S[σ]c = S ±b [cor b (σ)]c we obtain (S, σ.κ) ∼a (S ±b , cor b (σ).κ) and therefore as in this case cor b (σ).κ = cor b (σ.κ), (S, σ.κ) ∼a (S ±b , cor b (σ.κ)). Whereas if κ is a faulty call, it must be for another secret d than b (if κ is faulty, σ does not contain a faulty call, so we can rule out that a or c holds b, and therefore neither a nor c has information about b), from (S, σ) ∼a (S ±b , cor b (σ)) and ±b ±d ±b S[σ]±d c = S [cor b (σ)]c we obtain (S, σ.κ) ∼a (S , cor b (σ).κ), and as again (the error is in b ̸= d) cor b (σ).κ = cor b (σ.κ) we again obtain (S, σ.κ) ∼a (S ±b , cor b (σ.κ)). If S[σ.κ]∩b a = {b} there are more subcases to consider. ∩b In case S[σ]∩b a = ∅ and S[σ]c = {b}, by induction for agents a and c we obtain that (S, σ) ∼a (S ±b , cor b (σ)) respectively (S, σ) ∼c (S ±b , cor b (σ)), from the latter we obtain S[σ]c = S ±b [cor b (σ)]c , so that (S, σ.κ) ∼a (S ±b , cor b (σ).κ) and therefore also (call κ must have been correct as agent c already held a faulty value of a secret before the call, so that again cor b (σ).κ = cor b (σ.κ)), (S, σ.κ) ∼a (S ±b , cor b (σ.κ)). ±b ∩b In the other case, S[σ]∩b a = ∅, S[σ]c = {b} and call κ is faulty such that S[σ]c (which contains b) is the set of secrets passed on to agent a, and we proceed differently. First, ±b from S[σ]∩b a = ∅ and induction for a it follows that (S, σ) ∼a (S , cor b (σ)). Second, as κ is faulty, there are no faulty calls in σ, so that cor b (σ) = σ and cor b (σ.κ) = σ.cor b (κ). Furthermore, S[σ]±b = S ±b [σ]c . From (S, σ) ∼a (S ±b , cor b (σ)) and cor b (σ) = σ we get c (S, σ) ∼a (S ±b , σ), from that and S[σ]±b = S ±b [σ]c we get (S, σ.κ) ∼a (S ±b , σ.cor b (κ)), c and with the above cor b (σ.κ) = σ.cor b (κ) therefore also (S, σ.κ) ∼a (S ±b , cor b (σ.κ)) as requested. In case S[σ]∩b a = {b}, call κ must have been a correct call (as the faulty call, of which ∩b there is not more than one, must be in σ) so that either S[σ]∩b c = ∅ or S[σ]c = {b}. We now proceed as in the previous cases to again obtain (S, σ.κ) ∼a (S ±b , cor b (σ.κ)). □ Proposition 13 (Knowledge implies correct belief) (i) |= Ka bb → (bb ∧ba ∧¬ba ) and (ii) |= Ka bb → (bb ∧ ¬ba ∧ ba ). ⊣ Proof We show the first, where the second is shown similarly. We show this by induction on the length of call sequences. For σ = ϵ it follows ex falso for b ̸= a and otherwise when b = a from the trivial observation that bb = ba = aa , the instantiation Ka aa → aa of the T axiom, and the fact that agents initially only hold a unique value of their own secret, so that aa is false. For σ = τ.κ we distinguish the case where κ does not involve agent a from the case where κ involves a. 11

For σ = τ.bcκ where b, c ̸= a, we assume that S, σ.bcκ |= Ka bb . We now have that S, σ.bcκ |= Ka b, iff (semantics of formulas and observation relation) S, σ |= Ka b, which implies (induction) S, σ |= bb ∧ ba ∧ ¬ba , which implies (by stubbornness for bb and by the call semantics for non-involved agents) S, σ.bcκ |= bb ∧ ba ∧ ¬ba . For σ = τ.acκ , assume S, σ.acκ |= Ka bb . We distinguish two subcases: S, σ |= Ka bb and S, σ ̸|= Ka bb . If S, σ |= Ka bb , by induction we can conclude that S, σ |= bb ∧ ba ∧ ¬ba . Again from stubbornness and again from the call semantics, but now for involved agents (value b for a is preserved in the union, whereas value b either remains absent, or in case contributed by agent c is discarded because in the ∗ set), we conclude that S, σ.acκ |= bb ∧ ba ∧ ¬ba . So in this case ∗ removal may be involved. If S, σ |= ¬Ka bb , this is the harder case, and the case of most interest in the proof. We show the three conjuncts separately, where the (hardest) second comes last. • S, σ.acκ |= bb . From S, σ.acκ |= Ka bb and the validity of Ka bb → bb (factivity T) it follows that S, σ.acκ |= bb . • S, σ.acκ |= ¬ba . From S, σ.acκ |= Ka bb it follows that S, σ.acκ |= ¬ba by the ′ following line of reasoning. By definition, S, σ.acκ |= Ka bb means that (where acκ is ′ ′ ‘another call involving a and c’): for all (S, σ.acκ ) ∼a (T, τ.acκ ), T, τ.acκ |= bb . By ′ definition of the observation relation, (S, σ.acκ ) ∼a (T, τ.acκ ) means that (S, σ) ∼a (T, τ ) and S[σ]c = T [τ ]c , where, seemingly to complicate matters, one or both of these secret distributions may involve a swap T [τ ]±b c . However, this is not a real complication, because we now satisfy the condition for b removal from agent a’s holding in the semantics of call. Which shows that, whether actually removed or not, S, σ.acκ |= ¬ba . So in this case ∗∗ removal may be involved.3 • S, σ.acκ |= ba . It remains to show that S, σ.acκ |= Ka bb implies S, σ.acκ |= ba . Now if S, σ |= ba or S, σ |= bc (and the call is correct), by the semantics of calls we immediately have that S, σ.acκ |= ba , because value b is then in the union S[σ]a ∪S[σ]c of the holdings of agents a and c (the ∗ deletion cannot occur because of assumption S, σ |= ¬Ka bb in this case of the proof; if a ∗∗ deletion occurs this involves value b because of proof assumption S, σ.acκ |= Ka bb ; see previous subcase). We therefore only have the following remaining cases to consider: in (S, σ), agent a has no information on b (ba and ba are both false) or agent a holds b (ba is true), and agent c has no information on b or agent c holds (or contributes, in a faulty call) b. In all such cases either S[σ.acκ ]a = ∅ or S[σ.acκ ]a = {b}. Applying Lemma 12 it ′ ′ then follows that (S, σ.acκ ) ∼a (S ±b , cor b (σ.acκ )). As (S ±b , σ.acκ ) ̸|= bb , therefore (S, σ.acκ ) ̸|= Ka bb . Therefore in all these cases it cannot be that S, σ.acκ |= Ka bb , which ends the proof. 3 We recall that ∗∗ implicitly only removes an incorrect value, in this case b, if the correct value, in this case b, is known to be held by b, but that we cannot formalize this as truth of Ka bb as that would make the logical semantics circular. But in fact the knowledge is already there and ‘preserved’ after the ** self-correction, and vice versa; the self-correction only concerns the truth of ba and ba , not of bb .

12

□ Two observations: (i) In all four cases where a and c have no information on b or incorrect information on b we have that S, σ ̸|= Ka bb as well as S, σ.acκ ̸|= Ka bb , so a’s ignorance of secret b then persists. (ii) We can only have that S, σ |= ¬Ka bb ∧ ¬ba ∧ ¬ba ∧ bc and S, σ.acκ |= Ka bb when agent a already self-corrected on a secret d ̸= b in the past (during σ), and therefore knows that any value she receives for a secret about which she is uninformed must be the correct value. This is the case of the proof above where it says “if S, σ |= ba or S, σ |= bc ” (namely when S, σ ̸|= ba ). A succinct way to express Proposition 13 is that S, σ |= Kv a b implies S[σ]∩b a = Sb . As a corollary of Proposition 13 we have that knowledge is justified correct belief: Corollary 14 (Knowledge is justified correct belief) |= Ka bb ↔ Ka (bb ∧ ba ∧ ¬ba ) ⊣ and |= Ka bb ↔ Ka (bb ∧ ¬ba ∧ ba ). Proof Although a corollary indeed, let us give the simple proof, where we consider the first. The direction from right to left is obvious. For the direction from left to right: Given (S, σ), assume S, σ |= Ka bb . Let (S, σ) ∼a (T, τ ). By the properties of knowledge we then not only have that T, τ |= bb but also that T, τ |= Ka bb . For all those τ we can apply Proposition 13 and obtain T, τ |= bb ∧ ba ∧ ¬ba . As (T, τ ) was arbitrary we therefore have S, σ |= Ka (bb ∧ ba ∧ ¬ba ). Now using assumption S, σ |= Ka bb and that (S, σ) was also arbitrary we get the required |= Ka bb → Ka (bb ∧ ba ∧ ¬ba ). □

2.3

Examples

We explain the semantics with some elementary examples. Example 15 Consider two agents a, b and the initial secret distribution I = a|b. • First consider a single call ab, so that (a|b)[ab] = ab|ab. Then agent a holds the correct value of secret b: a|b, ab |= bb ∧ ba . However a considers it possible that she holds the incorrect value of b: a|b, ab |= K̂a (bb ∧ ba ), because (a|b, ab) ∼a (a|b, abb ) and a|b, abb |= bb ∧ ba . This item illustrates that true belief does not imply justified true belief, that is, knowledge: a|b, ab |= bb ∧ ba ∧ ¬bb whereas a|b, ab ̸|= Kv a b (a|b, ab ̸|= Ka (bb ∧ ba ∧ ¬bb ). • Then consider call sequence ab.abb . We now have that (a|b, ab.abb ) ∼a (a|b, abb.ab), and no other gossip states are considered possible. Furthermore (a|b)[ab.abb ] = ab|ab and (a|b)[abb.ab] = ab|ab. Either way, (a|b)[ab.abb ]a = (a|b)[abb.ab]a = ab: agent a has a conflict for the secret of agent b. In order to resolve the conflict, she needs to call b again. • Therefore, now consider call sequence ab.abb.ab. Intuitively, agent a now has three independent sources of information on the secret of b, of which the majority has value 13

b. This is sufficient for her to learn the correct value b of b’s secret. Because formally, the last observation further restricts the set of possible call sequences. From the two call sequences that a considered possible before, only the first can be extended such that the first and third received value for b correspond, we cannot extend the second into abb.ab.abb as this contains more than one faulty call. The only gossip state she therefore considers possible is (a|b, ab.abb.ab). At the third call agent a can therefore restrict the set of initial secret distributions that she considers possible from {a|b, a|b} to the singleton {a|b}, such that she now knows that the correct value of b’s secret is b and not b. (Agent a knows / has justified true belief of secret b.) The incorrect value b held by a in (a|b)[ab.abb ] = (ab|ab) no longer appears in her holding in (a|b)[ab.abb.ab] = (ab, ab) as a consequence of the deletion of that value according to the semantics of calls. In this case we have that, for agent a, ∗∗ = {b} (and ∗ = ∅). Furthermore, also b will not incorporate the incorrect value b of his own secret that he receives from a in the third call. This is because knowledge Kv b b of his own secret is preserved after all calls and therefore in particular after the the first two calls. In this case we have that, for agent b, ∗ = {b} (and ∗∗ = ∅). • As a different extension of the first call ab, consider ab.ab. Even though (a|b, ab) ∼a (a|b, abb ), we have that (a|b, ab.ab) ̸∼a (a|b, abb.ab), because agent a has a conflict in one and not in the other. Also, agent a does not consider (a|b, abb.abb ), because abb.abb has more than one faulty call. We have that a|b, ab.ab |= Ka bb : after a majority of two independent observations of value b, a again knows that this must be the correct value. We can also get knowledge of secrets without first having a conflict to resolve. • Finally, consider call sequence ab.ab.abb extending the previous ab.ab. Receiving an incorrect value b for the secret of b does not cause agent a to have a conflict for the secret of b as she already knows the (correct) value b for that secret. As the value b is known to be incorrect it is not added to the holding of secret values of agent a (the set ∗ = {b}), so that (a|b)[ab.ab] = (a|b)[ab.ab.abb ] = ab|ab. (This is just as for agent b after ab.abb.ab in the first item.) ⊣ Example 16 Let there now be three agents a, b, c. • Consider initial gossip state a|b|c and call sequence ac.ab. Agent a considers the following gossip states possible: (a|b|c, ac.ab), (a|b|c, acc.ab), (a|b|c, ac.abb ), as well as well as other gossip states wherein a transmission error is made by herself. They all result in agent a holding {a, b, c}. Agent a does not know she holds the correct values of all three secrets. From (a|b|c, ac.ab) ∼a (a|b|c, acc.ab) we obtain that ac.ab |= K̂a cc . • Consider the extension ac.ab.abb . We have that (a|b|c)[ac.ab.abb ] = abc|abc|ac. Agent a now still considers possible the gossip states (a|b|c, ac.ab.abb ) and (a|b|c, ac.abb.ab). She no longer considers possible that she holds an incorrect value for c. She knows 14

that at most one transmission error occurs, and knows that the error involved the secret of b, she therefore now knows the secret of c: a|b|c, ac.ab.abb |= Ka cc , implying a|b|c, ac.ab.abb |= Kv a c. ⊣ Example 17 An agent can get to know the secret of another agent without ever calling that agent. Consider the call sequence ab.bc.ad.de.ce and the usual initial secret distribution I (that is, a|b|c|d|e). We show that after this call sequence agent e knows the secret of a, without ever having called a. Let us first show schematically how the secret distribution develops and after that justify some details: a|b|c|d|e

ab.bc.ad

→

de

ce

abd|abc|abc|abd|e → abd|abc|abc|abde|abde → abd|abc|abcde|abde|abcde

After call de agent e holds all secrets except c. At this stage agent e considers it possible that she incorrectly believes a: for example, we have that (a|b|c|d|e, ab.bc.ad.de) ∼e (a|b|c|d|e, ab.bc.ad.da e) (and that (a|b|c|d|e, ab.bc.ad.de) ∼e (a|b|c|d|e, ab.bc.aa d.de); note that an error in the first call aa b will not reach d and therefore not e). After call ce agent e learns that c did not hold a value for secret d but was informed about a. As the values of a received from d and from c do not conflict, agent e can therefore rule out gossip state (a|b|c|d|e, ab.bc.ad.da e). For the same reason that the observed value of a did not conflict in the final two calls de and ce, she can also rule out that the final call ce was an incorrect call ca e, or that the second call bc was an incorrect call ba c. Finally, agent c can rule out that the first call was aa b, as that would have made b pass on this incorrect value a to c in call bc, whereas in call ad agent d would still have received value a from a, so that also in that case e would have observed different values for a in calls de and ce. Agent e now knows the secret of a. A fortiori, an agent can get to know the secret of another agent including self-correcting the value for the secret of that agent without ever calling that agent. A simple variation on the previous would be the call sequence ab.bc.ad.da e.de.ce. After da e, agent e holds an incorrect value a of the secret of agent a. After calling d again she receives correct value a and thus now has a conflict for the secret of a. In call ce agent e learns, as before, that agent c does not hold a value for secret d. The value of a agent e receives in that call is therefore an independent observation, which again creates a majority of a over a. Yet another example, for four agents a, b, c, d, is (a|b|c|d, ab.aa c.ad.cd.cb). We get the following transitions: a|b|c|d

ab.aa c

→

ad

cd

cb

abc|ab|abc|d → abcd|ab|abc|abcd → abcd|ab|abcd|abcd → abcd|abcd|abcd|abcd

After ab.aa c agent c knows that the first call was involving a and b, however she cannot distinguish (a|b|c|d, ab.aa c) from (a|b|c|d, ab.ac). After the subsequent third and fourth calls ad.cd, agent c (after the second call involving her) still cannot distinguish (a|b|c|d, ab.aa c.ad.cd) from (a|b|c|d, ab.ac.ad.cda ). However, the final call cb rules out secret distribution a|b|c|d, as that would otherwise have resulted in agent c learning that a holds a instead of a. So, the alternative evolution of secret distributions would then have been: ...

ab.ac.ad

→

cda

cb

abcd|ab|abc|abcd → abcd|ab|abcd|abcd → abcd|abcd|abcd|abcd 15

Clearly, agent c again knows the secret of a. But of course she can distinguish a call sequence where she knows that its value is a from a call sequence where she knows that its value is a. ⊣

2.4

Gossip protocol

Expert and super expert An agent who holds all secrets without conflict is an expert, an agent who knows that all agents hold all secrets without conflict is a super expert. Similarly, an agent who holds all correct secrets without conflict is a correct expert and an agent who knows that all agents hold all correct secrets without conflict is a correct super expert. Call sequences satisfying that all are (correct) experts or (correct) super experts are called (correct) successful respectively (correct) supersuccessful. In gossip without errors we only consider correct experts and correct super experts, and all success is correct success. Gossip protocol A gossip protocol is an algorithm encoding the intuition: Until the termination condition holds, select a pair ab of agents that satisfy a call condition, and execute call ab. The gossip problem is whether a gossip protocol terminates and for which condition. The termination condition is also known as the epistemic goal. The usual termination condition is that all agents are experts. We also consider the termination condition that all agents are super experts. Apart from that we consider the termination conditions that all are correct experts or all are correct super experts. The call condition for a call from a to b (whether correct or faulty) in general requires a and b to be neighbours (given a possibly restricted network), and for agent a to know that the call condition holds. However, here we only consider that all agents are neighbours and we only consider the gossip protocol ANY with trivial call condition ⊤ (‘true’), which is known by agent a — another triviality, as Ka ⊤ is valid. There are also more distributed, equivalent, ways to describe gossip protocols than above [3, 34, 29]. Instead of termination it is sufficient to require stabilization, such that any permitted call can continue to be executed forever, even when all agents are (super) experts. The effect of this is removing the ‘until’ parts in the description above. Given an infinite call sequence, in order to have success of some kind, stabilization (termination) is only required if the infinite sequence is fair: at any stage all permitted calls will occur again later [31, 3]. Stabilization is more in line with assumptions in distributed computing. Our setting for gossip with errors seems a very simple one, because calls and protocols are not in the logical language, the call condition is the trivial formula ⊤, and the network is complete (all are neighbours). However, the presence of errors comes with novel logical complications, as self-correcting makes true propositional variables ba or ba false again, unlike in error-free gossip.

16

Let us now formally introduce the terminology to accommodate the novel distinction between correct and incorrect termination (note the disjunctions turn out exclusive). Expa ExpA Expcor a Expcor A

:= ((b ∧ ¬ba ) ∨ (¬ba ∧ ba )) Vb∈A a := Expa Va∈A := ((b ∧ b ∧ ¬ba ) ∨ (bb ∧ ¬ba ∧ ba )) Vb∈A b cor a := a∈A Exp a V

a is an expert all agents are experts a is a correct expert all agents are correct experts

Furthermore, Ka ExpA means that agent a is a super expert and Ka Expcor A means that agent a is a correct super expert. Given all that, termination condition EA ExpA requires that all are super experts and EA Expcor A that all are correct super experts. The gossip protocol is now called (where this should hold for arbitrary initial secret distributions S, σ ω informally represents an infinite call sequence, and τ is a call sequence, that is, finite): • successful if all fair σ ω have a prefix τ such that S, τ |= ExpA ; • supersuccessful if all fair σ ω have a prefix τ such that S, τ |= EA ExpA . • correct successful if all fair σ ω have a prefix τ such that S, τ |= Expcor A ; • correct supersuccessful if all fair σ ω have a prefix τ such that S, τ |= EA Expcor A ; • first-correct successful if |= ExpA → Expcor A ; • first-correct supersuccessful if |= EA ExpA → EA Expcor A . The last four are novel categories of termination. Concerning the final two, it not only matters whether all become correct experts but also whether this happens first. Note that ExpA may be true, but then become false again when an agent after a subsequent call has a conflict for the value of some secret; and subsequently may again become true, as well as, eventually, Expcor EA Expcor A . In view of that it may be considered remarkable that A is V the only stable termination goal (Proposition 20), as it is equivalent to a,b Kv a b in our semantics. Preservation of truth is then a direct consequence of Lemma 10. We continue with such results for successful and supersuccessful termination.

2.5

Results for successful and supersuccessful termination

We will show that eventually everybody becomes an expert and a correct expert, but that it cannot be guaranteed that everybody becomes a correct expert before becoming an expert. Proposition 18 (1.) |= Expa ↔ Ka Expa and (2.) |= ¬Expa ↔ Ka ¬Expa but (3.) ̸|= cor Expcor ⊣ a ↔ Ka Exp a . Proof The direction Ka φ → φ of all the above is a property of knowledge. For the other direction: 17

1. This follows almost directly from Lemma 8 that the value of all local atoms is known by the agent holding them. If Expa , then for all b ∈ A, (ba ∧ ¬ba ) ∨ (¬ba ∧ ba ) is true. From that, with Lemma 8, also follows (Ka ba ∧ Ka ¬ba ) ∨ (Ka ¬ba ∧ Ka ba ). With the properties of knowledge we then also have that Ka (ba ∧ ¬ba ) ∨ Ka (¬ba ∧ ba ), and by weakening both known formulas we then obtain Ka ((ba ∧ ¬ba ) ∨ (¬ba ∧ ba )) (in disjunction with itself, so we omitted that). 2. If ¬Expa , there must be a secret that a does not hold or for which she has a conflict, that is, ¬ba ∧ ¬ba or ba ∧ ba . Using Lemma 8 of locality again, we then have Ka ¬ba ∧ Ka ¬ba or Ka ba ∧Ka ba , and therefore Ka (¬ba ∧¬ba ) or Ka (ba ∧ba ). Therefore Ka ¬Expa . cor 3. However, ̸|= Expcor a ↔ Ka Exp a . Given four agents a, b, c, d, a very simple counterexample is that a|b|c|d, ab.cd.ac.bd |= Expcor whereas a|b|c|d, ab.cd.ac.bd ̸|= Ka Expcor a a because (a|b|c|d, ab.cd.ac.bd) ∼a (a|b|c|d, ab.cd.acc.bd), and (a|b|c|d)[ab.cd.acc.bd]a is also abcd ({a, b, c, d}) but in that case that is incorrect, so that a|b|c|d, ab.cd.acc.bd ̸|= Expcor a . It is easy to see that also b, c, d do not know that knowledge of all secrets is correct after ab.cd.ac.bd. A more involved counterexample is Example 21 in the next subsection.

□ Proposition 19 The gossip protocol ANY is: (1.) successful, (2.) supersuccessful, (3.) correct successful, and (4.) correct supersuccessful. However, it is (5.) not first-correct successful and (6.) not first-correct supersuccessful. ⊣ Proof We recall that the notions of successful and supersuccessful are defined with respect to fairly scheduled infinite call sequences, and that in the protocol ANY any call ab remains arbitrarily often permitted (instead of termination we assume stabilization). Without loss of generality, assume initial secret distribution I. For items (1.) to (4.) we show that for any gossip state (I, σ) not satisfying the termination condition, call sequence σ can be extended to a τ such that (I, τ ) satisfies the termination condition. 1. ANY is successful: Given I, σ ̸|= ExpA , there must be a ̸= b with I[σ]∩b a = ∅ or ∩b I[σ]a = {b, b}. In the first case, after σ, call ab is permitted so that I[σ.ab]∩b a = {b} and therefore I, σ.ab |= (ba ∧ ¬ba ) ∨ (¬ba ∧ ba ), as required. In the second case call ab is also permitted and results in error correction so that also I[σ.ab]∩b a = {b}. In case ∩b ∩b there are still such a, b with I[σ]a = ∅ or I[σ]a = {b, b} we repeat the procedure. 2. ANY is supersuccessful: Given I, σ ̸|= EA ExpA , there must be a, b ∈ A with I, σ |= K̂a ¬Expb . Therefore, there is (T, τ ) ∼a (I, σ) with T, τ ̸|= Expb , and a c ∈ A (possibly c = a) with T, τ |= ¬cb ∧ ¬cb or T, τ |= cb ∧ cb . After τ , call bc is permitted, so that, as for the first item, T, τ.bc |= (cb ∧ ¬cb ) ∨ (¬cb ∧ cb ). Call bc is also permitted after σ, as well as a subsequent call ab (note that these calls bc and ab may cause a conflict in agent a for some secret d ̸= c, which would requires a further extension of the call sequence with a single call ad when iterating the procedure). We now 18

have that I, σ.bc.ab |= Ka (cb ∧ ¬cb ) or that I, σ.bc.ab |= Ka (¬cb ∧ cb ), and therefore I, σ.bc.ab |= Ka ((cb ∧ ¬cb ) ∨ (¬cb ∧ cb )) as required. We repeat the procedure until a knows that b is an expert, and until there are no a, b ∈ A with I, σ |= K̂a ¬Expb . 3. ANY is correct successful: without loss of generality, suppose there are a, b such that bb ∧ ba ∧ ¬ba is false. Let us assume that ba ∧ ¬ba are true, as we have already shown ANY to be successful, so that bb must be false. If so, as call ab is permitted, after this call agent a knows secret b so that with Proposition 13 we obtain bb ∧ ba ∧ ¬ba . We repeat the procedure until this holds for all pairs c, d of agents in A. Note that for c ̸= b we may well have that cc ∧ ca ∧ ¬ca is true but Kv a c is false, which does not require any further calls from agent a (unlike in the next item, where knowledge of secrets is required). 4. ANY is correct supersuccessful: We may assume the previous item, so we can obtain bb ∧ ba ∧ ¬ba for all agents a and b. In case agent a does not know this, as call ab is permitted, it is sufficient to have a call b in order to confirm that the value b she holds is correct. Also note that this termination goal is stable: see Proposition 20, below. 5. ANY is not first-correct successful: see Example 21, below. 6. ANY is not first-correct supersuccessful: see Example 22, below. □ Correct super success is the only stable property of a gossip protocol in this setting with errors. cor Proposition 20 If S, σ |= EA Expcor A and σ ⊑ τ , then S, τ |= EA Exp A

⊣

Proof We observe that EA Expcor A is equivalent to the conjunction of Ka ((bb ∧ ba ∧ ¬ba ) ∨ (bb ∧ ¬ba ∧ ba )) for all agents a, b ∈ A. Such a conjunct is equivalent to Ka (bb ∧ ba ∧ ¬ba ) ∨ Ka (bb ∧ ¬ba ∧ ba ) (because agents know their local propositions, Lemma 8), and applying Corollary 14 therefore equivalent to Ka ba ∨ Ka ba in our semantics, in other words, V equivalent to Kv a b. We obtained that EA ExpA is equivalent to a,b∈A Kv a b. Now applying Lemma 10, we immediately obtain that S, σ |= EA ExpA and σ ⊑ τ imply S, τ |= EA ExpA . □

2.6

Examples of successful and supersuccessful termination

We give examples of successful and supersuccessful termination, including the phenomenon of lucky calls where an agent may learn that another agent is an expert without calling them, that comes with novel variations in this setting with errors.

19

Example 21 First, success. Assume I = a|b|c|d. Consider call sequence abb.bc.bd.cd.ab.ab. In the first call, a receives a faulty value b of b’s secret. Then, b, c, d exchange all secrets between them. Then a calls b again and now has a conflict for b, and finally makes another call wherein she self-corrects and now knows the secret of b. A certain road towards resolving a conflict about b is calling b, even when there might be other roads achieving the same goal. Also note that agent b does not get a conflict about his own secret in that final call ab: the value b he obtains from agent a he knows to be incorrect and therefore discards. Schematically the execution is: abb

a|b|c|d → ab|ab|c|d ab abcd|abcd|abcd|abcd →

bc.bd.cd

→ ab|abcd|abcd|abcd abcd|abcd|abcd|abcd

ab

→

We have that a|b|c|d, abb.bc.bd.cd.ab.ab |= Expcor A . b Now consider ab.ac.cd.da.ab.ab wherein agent a disseminates an incorrect value for b to the other agents. Then, as before, a learns in a call with b that the value of b may be faulty and confirms the correct value b in another call ab (again obtaining the required majority of two independently obtained values b over one b). But agents c and d still incorrectly believe that b is the secret of b. Schematically: abb

ac

cd.da

a|b|c|d → ab|ab|c|d → abc|ab|abc|d → ab abcd|abcd|abcd|abcd → abcd|abcd|abcd|abcd

abcd|ab|abcd|abcd

ab

→

We have that a|b|c|d, abb.ac.cd.da.ab.ab |= ExpA ∧ ¬Expcor A . b Finally, consider ab.bc.ad.cd.cb.db.ad.ab. The first conflict now appears in call cd. Both c and d need to verify b’s secret. Calls cb and db may be in either order. In subsequent call ad, agent a learns a conflicting value for b, but not agent d, who already knows the correct value of b after the prior call db. Agent a now calls b to learn the correct value. We end up with a|b|c|d, abb.bc.ad.cd.cb.db.ad.ab |= Expcor A . abb

bc

ad

a|b|c|d → ab|ab|c|d → ab|abc|abc|d → abd|abc|abc|abd cb.db ad abd|abc|abcd|abcd → abd|abcd|abcd|abcd → ab abcd|abcd|abcd|abcd → abcd|abcd|abcd|abcd

cd

→ ⊣

Example 22 Now, super success. First, consider the error-free eight call sequence σ = ab.cd.ac.bd.ab.ad.bc.cd and the initial secret distribution I = a|b|c|d. In error-free gossip this call sequence is supersuccessful and eight calls are optimal [31, 29]. In our semantics for gossip with errors the call sequence is successful and also correct successful as all agents hold the correct value: I, σ |= ExpA ∧ Expcor A But it is not supersuccessful and therefore also not correct supersuccessful: I, σ |= ¬EA ExpA ∧ ¬EA Expcor A 20

For example, consider agent a. Agent a considers it possible that the last call was cdd , after which c has a conflict for secret d and is no longer an expert. From (I, σ) ∼a (I, ab.cd.ac.bd.ab.ad.bc.cdd ) it follows that I, σ |= K̂a ¬Expc and therefore I, σ ̸|= EA ExpA , and a fortiori also I, σ ̸|= EA Expcor A . In our setting the expert goal ExpA has become ‘unstable’, for example, extending σ with the call cdd above also makes c have a conflict, so that I, σ.cdd ̸|= ExpA . It may further be of interest to observe that we still have that I, σ |= Ka Expcor a Agent a is a correct super expert (but not yet b, c, d). First, note that after call sequence ab.cd.ac.bd.ab.ad, agent a only considers that call sequence possible (in call ac she learns that the second call was cd, and in second call ab she learns that the previous call was bd). Agent a is a correct superexpert because she has for each other agent two independent observations of the correct value of their secret: ab and ab for the secret of b (obvious), ac and the subsequent ab for the secret of c,4 and ac and ad for the secret of d.5 Next, consider τ = ab.ac.add.ab.ac.bc.bd.bd.cd.cd After the second call ac, agent a incorrectly believes that the secrets are abcd. After call bc agents b and c still incorrectly believe that the secrets are abcd, in the first call bd agent b obtains a conflicting value for secret d which is corrected in the second call bd, and similarly for c in the subsequent cd.cd. We have that I, τ |= EA ExpA ∧ ¬EA Expcor A Not only does a still hold an incorrect secret of agent d, but a also believes that b and c hold that incorrect secret of d. Finally, a correct supersuccessful call sequence can be obtained by all agents calling each other twice (and therefore   having two independent observations for all secrets, establishing knowledge), thus in 2 n2 calls (12 calls for n = 4) in a schedule not containing errors: let ρ = ab.ac.ad.bc.bd.cd then we have I, ρ.ρ |= EA ExpA ∧ EA Expcor A Any faulty call occurring in such a call sequence seems likely to lead to lengthier sequences, but as long as scheduling of calls is fair, all calls will occur again at some stage and thus any 4 An error for c cannot have been in call ac or call ab, as the observed values would then be different, where it is important that c did not call b after call ac and before call ab; if the error had been in call cd then b would have passed on the incorrect value to a in second call ab and a would have observed a conflict for c in that call; if the error had been in call bd, a would similarly have had a conflict for c in subsequent ab. 5 An error for d cannot have been in calls ac or ad, as the observed values of d were the same. The error cannot have been in call cd, as call bd would then have been correct so that a would have observed conflict in ad. It cannot have been in bd, as the conflict would then already have appeared in the next ab. It cannot have been in ab either, for the same reason.

21

conflict will be resolved. It is unclear if call sequences with faulty calls always take longer to reach correct super success, because agent a correcting a conflict for secret b thus learns that all other values c she holds must be correct, which speeds up the process again. ⊣ We close with another example explaining the phenomenon of lucky calls and how this interacts with incorrect values for secrets. A lucky call is a call wherein an agent learns that another agent is an expert without calling that agent [29]. So it is then not necessary to call that agent in order to find out whether the agent knows all secrets. Example 23 Consider the call sequence ac.ad.ac.bc.bc.ac without transmission errors, and initial secret distribution a|b|c|d. After the first three calls, agent a knows that agents a, c, d know the secrets a, c, d. In the call bc, agents b and c become experts.6 In the call ac, agent a also becomes an expert and, as c already was an expert in that call, it is easy to see that agent a also learns that b must be an expert. Agent a is lucky. However, a does not know if b became an expert by calling c or by calling d: she cannot distinguish the actual call sequence from the call sequence ac.ad.ac.bd.cd.ac. Agent a therefore also does not know whether d is an expert, as d is not one in the actual call sequence, but is an expert in the other call sequence, that a considers possible. Now consider the call sequence ac.ad.ac.bb d.cd.ac with a transmission error made in the call bb d so that d passes on the incorrect value of b to c and after that c tot a. Then after final call ac agents a, c and d all incorrectly believe that b’s secret is b (we have that, respectively, ba ∧ ¬ba , bc ∧ ¬bc and bd ∧ ¬bd hold). Agent a now incorrectly believes that b is an expert holding secrets abcd, in the sense that a considers possible (for example) gossip state (a|b|c|d, ac.ad.ac.bc.bc.ac) and where a|b|c|d, ac.ad.ac.bc.bc.ac |= ab ∧ bb ∧ cb ∧ db , whereas actually b is the only correct expert: a|b|c|d, ac.ad.ac.bb d.cd.ac |= ab ∧ bb ∧ cb ∧ db !⊣

3

Weaker and stronger call semantics

In this section we consider alternative call semantics. First, instead of agents exchanging all the secrets they know, there are more refined message semantics than that, wherein the agents only send or only receive these secrets, or only some but not all of the secrets, or only one secret per message. In gossip, merely sending is known as ‘push’, merely receiving is known as ‘pull’, and the exchange of secrets of our call semantics is known as ‘pushpull’ [17]. These are standard variations. We will not consider those variations but stick to agents exchanging all the secrets they hold. This comes closer to exchanging ‘all you know’ in order to speed up information dissemination as much as possible, as in full information protocols [22] and in resolving distributed knowledge [2]. Still, from the perspective of exchanging all that is known, one could say that we hold somewhat of a middle ground, as we use some but not all the information available from the history of prior calls. We use some information, because the agents reason over call sequences containing at most 6

We added another call bc to keep agent a in the dark about the identity of the callers in bc.bc. Such an extra call is not needed in the asynchronous version on which the example is based.

22

one error: this implicitly means that agents can ‘count’ the number of observations of the value of a secret (namely how often this occurs in a call sequence they consider possible), and can ‘remember’ having corrected a conflicting value for a secret (namely if they only consider call sequences possible wherein they had to self-correct): quotes that are indeed intended to scare, as the logical language does not have such primitives: neither is explicit. We now explore some other options to use the history of calls in the semantics. We first consider an alternative message semantics wherein agents only store, for each other agent, the information exchanged in the last call with that agent. This is a less expressive semantics |=last . Such protocols with bounded memory have been considered in distributed computing in [12, 7]. Second, we consider a message semantics wherein agents store the entire history of calls and secret holdings of all other agents. This is more expressive semantics |=full . Those message semantics are known in distributed computing as full-information protocols [22].

3.1

Call semantics only storing the last call

Consider an alternative semantics for gossip wherein: Each agent a stores for all agents b ̸= a, for the last call involving a and b, the pair (X, Y ) consisting of the set X of values of secrets contributed by a to that call, and the set Y of secret values received by a from b in that call. Note it says received by a and not sent by b, as a transmission error may have occurred. In case no call between a and b took place yet, agent a stores its initial secret value a or a for herself, and ∅ for b: this is the pair ({a}, ∅) or ({a}, ∅). An initial secret distribution S and a call sequence σ thus determine an n-tuple that we denote last(S, σ), with for each agent a a projection last(S, σ)a . From last(S, σ)a we can determine agent a’s holding of values denoted S[σ]last a , where we do not specify how this is exactly determined. It is not entirely trivial: although each agent stores the last call involving any other agent, the agent does not store the order of these n − 1 calls. It is not known which of these was the actual last call, in which case we could have simply taken the union X ∪ Y of the pair (X, Y ) associated with that call. And there is the issue of errors. This setup defines a logical semantics denoted |=last to distinguish it from our |= semantics. We define (S, σ) ∼last (T, τ ) iff Sa = Ta and last(σ)a = last(τ )a . With that, the a semantics for knowledge becomes: • S, σ |=last Ka φ iff T, τ |= φ for all T and τ such that (S, σ) ∼last (T, τ ). a The other inductive clauses of |=last , for negation and conjunction, are then as for the satisfaction relation |=. What atomic propositions should be associated with this storage of last calls is unclear, and a bit up for grabs. It is at least clear that the set of atomic propositions should now be different. We need more atoms to describe the local state of an agent, not merely ba for ‘agent a holds secret value b’ but instead of that, or additional to that, bca for ‘agent a received secret value b from c’ in the last call with c; and with, let us 23

say, an initial atom aaa as well (and all that for b and a as well). Agent a would then have c a conflict for the secret of b if she holds conflicting values b as well as bd for the secret of b. And we would need a mechanism to express self-correction in the language. We will not go into all that, or at least not go into all that even further, but instead: (i) give some results for the error-free case of the last-call semantics, and (ii) give examples demonstrating the different results to be expected for the single-error case of the last-call semantics. Error-free last-call semantics Even for error-free gossip there are differences between the last-call semantics |=last and the standard semantics |=. Assume a |=last semantics that makes atom ba true if agent a received secret b in the last call from some agent c. So, along the line above, ba is true iff there is a c such that bca is true. We recall that the initial secret distribution I is a stand-in for the (unique) initial secret distribution in error-free gossip. The following can be shown. First, success corresponds for the last-call and for the standard semantics. This is not surprising. Second, an agent may be a super expert for the standard semantics but not for the last call semantics: this is because an agent may be lucky and learn that another agent is an expert without calling that agent [29]. This is more remarkable. Third, a last-call super expert is also a standard super expert. Fourth, super success for the last-call semantics implies super success for the standard semantics. Proposition 24 1. I, σ |= ExpA iff I, σ |=last ExpA 2. I, σ |= Ka ExpA does not imply I, σ |=last Ka ExpA 3. I, σ |=last Ka ExpA implies I, σ |= Ka ExpA 4. I, σ |=last EA ExpA implies I, σ |= EA ExpA

⊣

Proof 1. (⇒): If a holds secret b, then (for b ̸= a) a must have received secret b from some agent c, not necessarily for the first time in the last call with c, but then c would still have sent b to a in the last call between a and c. This holds for all a and b. (⇐): If I, σ |=last ExpA then some agent c sent b to a in the last call between a and c. Therefore a holds the secret b. 2. Consider the call sequence ac.ad.ac.bc.bc.ac without transmission errors from Example 23, wherein agent a is lucky about agent b in final call ac. At this stage agent a knows that a, b, c are experts. Now extend this call sequence with call ad. Then a is a super expert: Ka ExpA is now true. But agent a never called b and therefore stores ({a}, ∅) for the last call involving b. Therefore, although I, σ |=last Expb , we still have I, σ ̸|=last Ka Expb and therefore I, σ ̸|=last Ka ExpA .

24

3. Let pair (X, Y ) be associated with the last call between a and c. If X ∪ Y = A, then a knows that that c is an expert after the call, and knows that in either semantics, that is, I, σ |=last Ka Expc and I, σ |= Ka Expc . From assumption I, σ |=last Ka ExpA it follows that I, σ |=last Ka Expc holds for all c ∈ A. Therefore also I, σ |= Ka ExpA . 4. The fourth item is a consequence of the third. □ Concerning the fourth item, we conjecture that also: I, σ |= EA ExpA implies I, σ |=last EA ExpA With an asynchronous call semantics, even when an agent a is lucky about b, in order to become super experts, agent b still has to call a in order to learn that a is an expert. So in the end, all agents have to be involved in a call to each other after which they are both expert to reach the super expert goal [29, Lemma 34]. If it were shown that this requirement also holds for a synchronous semantics, then the implication would be established. Last-call semantics with errors However, let us now consider some scenarios involving the last-call semantics |=last and faulty calls. A modal logical issue with the last-call semantics is what ‘knowing the secret’ now means, as the accessibility relations of the last-call semantics, and thus the notion of knowledge, are completely determined by the local states of the agents. In the |=last semantics ‘a knows secret b’ therefore necessarily corresponds to a local state value of agent a, whereas in our semantics ‘a knows secret b’ corresponds to a knowing a local state value of agent b. Obvious candidates for ‘a knows secret b’ in the last-call semantics are: (i) the value of b received by a in the last call with b, or (ii) the same values of b received by a from all agents c. And all that in their last call with a. Unfortunately, for both interpretations, where we again write Kv a b for ‘a knows secret b’, and where S is an initial secret distribution: Observation 25 S, σ |=last Kv a b does not imply S, σ |= Kv a b.

⊣

For reading (i) it is obvious, as in the single call from b to a there could be a transmission error for secret b. But for reading (ii) the implication also fails. Consider four agents, secret distribution I = a|b|c|d, and call sequence bb a.ac.ad.ca.da. Then a received b from all three other agents in their last call. But b is still the incorrect value. In the last-call semantics we can still imagine a eventually getting to know the correct value of a secret by holding conflicting values b and b and receiving b from another agent (and self-correcting on a majority of two b’s), or even by already holding a value b and receiving b from another agent (a majority of two b’s without need to self-correct). But even after a receives value b from agent b a thousand times, when in the next call with b she after all receives b then she will have a conflict, as she only compares this to the value b received in the final of those one thousand calls. Therefore: 25

Observation 26 S, σ |=last Kv a b and σ ⊑ τ do not imply S, σ |=last Kv a b.

⊣

In the standard semantics, there is a difference between correct belief, that is not knowledge of secrets, and justified correct belief, that counts as knowledge of secrets. But not in the last-call semantics. Now, correct belief is by definition known correct belief, as it is a feature of the local state. Such negative results suggest that it would be very hard to get correct termination. But strangely enough this is not the case. Because (see the contrast with Observation 25): Observation 27 S, σ |=last

V

a,b∈A Kv a b implies S, σ |=

V

a,b∈A Kv a b.

⊣

In other words: cor Observation 28 S, σ |=last EA Expcor A implies S, σ |= EA Exp A .

⊣

This is because when all agents agree on all values, also locally for all values they received from other agents, any conflicts must have been resolved or have never occurred. The last-call semantics is the precisely minimal and adequate one to obtain such correct super success, which is exactly why we wished to present it as an alternative. This is relevant because it may well be that super success is the strongest goal that can be obtained for synchronous gossip (this has only been proved for asynchronous gossip [29]). last The result does not hold in the other direction that S, σ |= EA Expcor A implies S, σ |= cor EA ExpA . Super success is unstable in the last-call semantics, because knowledge Kv a b is unstable (Observation 26). Another plus of the last-call semantics is that it is first-correct supersuccessful, unlike the standard semantics (Proposition 19). Observation 29 |=last EA ExpA → EA Expcor A .

⊣

This is a consequence of our choice of defining knowledge of a secret for the last-call semantics. An agent cannot agree on the values of all secrets for all agents unless they are all correct, otherwise there must have been a conflict. So in a way the last-call semantics is ‘only-correct supersuccessful’. Continuing on that theme, despite being first-correct supersuccessful, the last-call semantics in not first-correct successful: Observation 30 ̸|=last ExpA → Expcor A .

⊣

A counterexample for four agents is ab.ac.bc.add.ab.ac, after which all agents hold values for all secrets and without conflict, but agents a, b, c hold the incorrect value of secret d.

26

3.2

Full information protocol

In an alternative |=full semantics for calls, agents do not merely exchange sets of values of secrets but they exchange full information, that is, they also exchange trees (or dags, see below) of subsequences of calls, namely of their own previous calls, but also of the previous calls of other agents having called them, and so on. Full information protocols are wellknown from distributed computing [22]. We first compare full-information semantics |=full with the standard semantics |= for correct gossip, and then repeat the exercise, more tentatively, for gossip with errors. Error-free full-information semantics In full-information semantics, given a gossip state (I, σ), in a call ab the agents a and b exchange in a call not only their sets of secrets I[σ]a respectively I[σ]b but also their full views va∼ (σ) respectively vb∼ (σ). The inductive definition is as follows for synchrony, where b, c ̸= a. By identifying identical subtrees, it can be said to construct a dag, a directed acyclic graph. The • symbol represents the call not involving a (but a’s awareness of the global clock). We follow the presentation in [27, Chapter 2]. := ϵ va∼ (ϵ) va∼ (σ.bc) := va∼ (σ).• va∼ (σ.ab) := (va∼ (σ), vb∼ (σ)).ab va∼ (σ.ba) := (vb∼ (σ), va∼ (σ)).ba If we now define (synchronous) full view observation relations just as the observation relations from Definition 5, and restricted to the error-free call semantics, the only different clause is the one for agents involved in the call. We put the old and the new one next to each other, to highlight the difference (the clause for ba is similar): (I, τ.ab) (I, σ.ab) ∼full a (I, σ.ab) ∼a (I, τ.ab)

iff iff

(I, τ ) (I, σ) ∼full a (I, σ) ∼a (I, τ )

and and

(I, σ) ∼full (I, τ ) b I[σ]b = I[τ ]b

(I, τ ) One can show [27] that (I, σ) ∼full (I, τ ) implies va∼ (σ) = va∼ (τ ), and that (I, σ) ∼full a a implies I[σ]a = I[τ ]a . The full-information semantics is therefore at least as strong as the standard semantics in the sense that any positive information about facts obtained with the standard semantics, such as ba , Kc ba , Kc bb and Kv c b, is also obtained with full information. For such formulas φ we have that I, σ |= φ implies I, σ |=full φ. But it is also really stronger, as we can reach arbitrary higher-order epistemic termination goals. One can show, first, that the goal of super success is reached by the same call sequence in the full-information semantics; second, that the goal of super success can be reached faster in the full-information semantics; and third, that there are higher order goals of mutual knowledge of all secrets than can be reached in the full-information semantics but not in the standard semantics. (A way to describe the third result that contrasts better with the previous two, is to state that 3. I, σ |=full EA EA EA ExpA does not imply I, σ |= EA EA EA ExpA . However, the right-hand side there does not imply unsatisfiability, which is stronger.) 27

Proposition 31 1. I, σ |= EA ExpA implies I, σ |=full EA ExpA ; 2. I, σ |=full EA ExpA does not imply I, σ |= EA ExpA ; 3. EA EA EA ExpA is |=full satisfiable but is not |= satisfiable.

⊣

Proof 1. Induction on the length of call sequences proves that I, σ |= Ka bc implies I, σ |=full Ka bc . Here we use that exchange of secrets is part of the standard call semantics but also of the full-information protocols, so that I, σ.ab |= ca if I, σ |= ca or I, σ |= cb just as well as I, σ.ab |=full ca if I, σ |=full ca or I, σ |=full cb . We also use that all variables are local: ba ↔ Ka ba is valid in either semantics. Now note that Ka ba is a V conjunct of EA ExpA = a,b Ka ba . 2. With full-information gossip protocols one can get knowledge faster than with standard gossip protocols. An example for four agents a, b, c, d is the eight-call sequence σ = ab.cd.ac.bd.ab.ad.bc.cd that satisfies I, σ |= EA ExpA , where eight calls is the   n optimal n − 2 + 2 for n = 4. We can remove calls ad and bc from this sequence and still obtain that goal in the full semantics but therefore not standardly: I, ab.cd.ac.bd.ab.bc |=full EA ExpA I, ab.cd.ac.bd.ab.bc ̸|= EA ExpA The reason is, that in the full information protocol, in call ab prior to call ad, agent a by also sending b her full view (as also implied by the definition of ∼full a ) effectively informs agent b that she learnt in call ac that agents a and c are experts (‘all she knows’) and that in that same call agent b similarly informs agent a that agents b and d are experts. Then, also in the same way, in call cd agent c informs agent d that c and a are experts and agent d informs agent c that b and d are experts. Therefore call ad has no longer to take place in order for a to learn that d is an expert and for d to learn that a is an expert, and similarly for call bc. (This example and similar examples are found in [18, 8, 27].) 3. The first item showed that EA ExpA is |=full satisfiable. Assume a |=full supersuccessful call sequence σ, that is, I, σ |=full EA ExpA . Then all agents a are super experts so that I, σ |=full Ka ExpA . We first show that I, σ |=full Ka ExpA implies I, σ.ab |=full Kb Ka ExpA . I, σ |=full Ka ExpA ⇔ I, σ |=full Ka Ka ExpA ⇔ 28

I, τ |=full Ka ExpA for all (I, τ ) ∼full (I, σ) a ⇒ (I, σ) and (I, τ ) ∼full I, σ) I, τ |=full Ka ExpA for all (I, τ ) ∼full a b ⇒ preservation of factual knowledge I, τ.ab |=full Ka Expa for all (I, τ ) ∼full (I, σ) and (I, τ ) ∼full (I, σ) a b ⇔ I, τ.ab |=full Ka Expa for all (I, τ.ab) ∼full (I, σ.ab) b ⇔ I, σ.ab |=full Kb Ka ExpA full As we can do thus reach Kb KaExp EA EA ExpA  A for all a, b ∈ A, we have that σ.τ |= n where τ is the sequence of all 2 calls. Not only knowledge of secrets is preserved after call sequence extension, but also higher-order knowledge, so the proof above can be adapted to show that I, σ.ab |=full Kb Ka ExpA implies I, σ.ab.bc |=full Kc Kb Ka ExpA .7 Combining the two we then get that I, σ.τ.τ |=full EA EA EA ExpA . Much faster schedules exist, but we only care about satisfiability and not about optimality here.

It remains to show that EA EA EA ExpA is unsatisfiable with the standard call semantics. Now for asynchrony our life would be been simpler: EA EA ExpA is unsatisfiable in the asynchronous |= semantics [29], so it would already have sufficed to show that EA EA ExpA is satisfiable in the |=full semantics. But it is unknown whether EA EA ExpA is unsatisfiable in the synchronous |= semantics (although it seems likely that it is unsatisfiable). In the asynchronous semantics one can show that, even when two agents become super experts in the same call, they both consider it possible that the other agent did not become a superexpert. We do not know if there is information leakage with synchrony such that agents that become super experts could learn this from one another. But we have another trick up our sleave. First, the synchronous and asynchronous standard semantics of error-free gossip coincide in the fact that once all agents are super experts, any further calls are not informative. Agent a can now predict the information exchange with any other agent b: only the set of all secrets will be exchanged. What you can predict is not informative. Second, given synchrony, for all subsequent calls not involving herself, she knows (because she is a super expert) that in all such cases only agents both already knowing all the secrets will call: not informative. Therefore, even if EA EA ExpA where satisfiable, yet higher-order termination goals are unsatisfiable: EA EA EA ExpA is unsatisfiable in the synchronous |= semantics. □ We conjecture that EA EA ExpA is also unsatisfiable for synchronous gossip, just as for asynchronous gossip, in which case we would also have that I, σ |=full EA EA ExpA does not imply I, σ |= EA EA ExpA . 7 One could imagine a proof for Ka φpos for any φpos in the fragment ba | φ ∨ φ | φ ∧ φ | Ka φ which is almost like the positive fragment corresponding to the universal fragment in first-order logic, except for the absence of basic clause ¬ba .

29

Example 32 Given four agents a, b, c, d and call sequence σ = ab.cd.ac.bd.ab.ad.bd.cd we have that I, σ |= EA ExpA . Then also I, σ |=full EA ExpA . Extend this call sequence with all six calls between two agents τ = ab.ac.ad.bc.bd.cd. Then I, σ.τ |=full EA EA ExpA . Now extend that call sequence once more with all six calls τ between two agents. Then  I, σ.τ |=full EA EA EA ExpA . Note that this is O(n2 ) for n agents (we made n2 calls, three times). Faster schedules to reach this goal, of O(n), are given in [18]. ⊣ Full-information semantics with errors In full-information semantics with errors we need to take arbitrary initial secret distributions into account in the observation relation (T, τ ) iff va∼ (S, σ) = va∼ (T, τ ), and furthermore there may and we thus get that (S, σ) ∼full a be transmission errors in the communicated secret values. Instead of providing a formal definition, let us sketch some issues and consequences. We can no longer compute the current holding of an agent from its full view and the initially held secret values. That agents share their sets of (values of) secrets in each call is now essential, as there may be transmission errors. Assuming that the semantics of a call ab is the same in |= and |=full , and an appropriate adjustment of the observation relation ∼full for faulty calls, we expect a that we still get (where S is an arbitrary initial secret distribution): Conjecture 33 S, σ |= EA ExpA implies S, σ |=full EA ExpA

⊣

A piece of good news is that when a obtains a conflict for a secret b and resolves this by for example calling b, thus obtaining a majority of correct values of b’s secret, in any next call to anyone, including b, she will not only communicate the correct value of b to anyone, but also communicate her knowledge Kv a b of the correct value, and so on, including higher-order knowledge of secrets. It therefore seems that also for gossip with errors: Conjecture 34 S, σ |=full EA EA EA ExpA does not imply S, σ |= EA EA EA ExpA

4

⊣

Discussion and conclusion

There are some clear topics for further research. First, we presented a synchronous semantics of gossip with errors, but we would like to show similar results for an asynchronous semantics of gossip of errors. This poses some additional technical complications. Second, we restricted ourselves to one transmission error because the restriction came with sufficient complications and already results in a modal epistemic setting. But one should obviously think of multiple errors. Third, instead of transmission errors we also wish to investigate faulty or so-called Byzantine agents. In the first subsection below we discuss the issues with asynchrony, the generalization of our results from one transmission error to a bound of f transmission errors, and the formalization of one or f faulty agents. In this work holding a secret and knowing a secret are really different epistemic notions. Other epistemic notions may also come into question. In the second subsection below we succinctly present connections to some other epistemic notions: belief, hope, protocoldependent knowledge, and local state knowledge. The final third subsection contains a short conclusion. 30

4.1

Asynchrony, multiple errors, and faulty agents

We succinctly discuss asynchrony, the generalization to gossip protocol executions with a bound of f transmission errors, and how to address gossip with at most f faulty agents. Asynchrony If we change the clauses of the observation relation for calls not involving the distinguishing agent a, and leave everything else in the semantics the same — in the semantics of calls, the observation relation, and the satisfaction relation — we get an asynchronous semantics of gossip. Let us show the novel clauses for the observation relation; where cdκ is any call involving c and d, faulty or not. (S, σ.cdκ ) ∼a (T, τ.f g κ ) iff (S, σ) ∼a (T, τ ) (S, σ.cdκ ) ∼a (T, τ ) iff (S, σ) ∼a (T, τ )

synchronous asynchronous

In the synchronous semantics a ∼a -equivalence class consists of a finite number of call sequences of the same length. But in the asynchronous semantics a ∼a -equivalence class always consists of an infinite number of call sequences, because agent a cannot distinguish the actual call sequence from a call sequence also containing an arbitrarily large number of subsequent calls not involving it (and also not from many other call sequences having such calls prior to a’s last call). In order to investigate whether these asynchronous semantics of gossip with errors are also well-defined, we therefore cannot use the previous partial order between pairs of call sequences and formulas, that was based on the equal length of indistinguishable call sequences. For example, consider Ka φ. The semantics of knowledge (that is the same for synchrony and asynchrony) gives us that: S, σ |= Ka φ iff T, τ |= φ for all (T, τ ) ∼a (S, σ). However, this time round we do not have that (τ, φ) < (σ, Ka φ), because the required |τ | = |σ| to establish this need not be the case. Call sequence τ may be arbitrarily long, and in particular longer than σ. We intend to attack this problem by defining an alternative partial order based on socalled direct knowledge of secrets [33] (see also [27]). If in a call from a to b either a learns a new secret from b, or b learns a new secret from a we say that the direct knowledge of secrets of a respectively of b increases. As for n agents there are n2 secrets to know there is an upper bound on the direct knowledge of secrets. One can then show that, given the restricted information exchange in gossip where agents only exchange sets of secrets, the maximum length of call sequences in which direct knowledge of secrets changes is 2n3 [33], and this is then used to show that each infinite ∼a -equivalence class is equally informative as a finite ∼a -equivalence class where the maximum length of call sequences is 2n3 . Any other call is then redundant (bisimulation invariant). For a logical language as ours but with also call modalities [ab]φ, this is then sufficient to completely axiomatize asynchronous knowledge. It seems such results are reproducable in an asynchronous logic of gossip with errors, where of course (in case of at most one transmission error) the number of directly knowable secrets is twice that of error-free gossip. This does not seem to affect the order of magnitude of the above 2n3 but only the constant factor. One could then envisage a partial order not based on the length |σ| of call sequences σ but on the number ♯σ of directly 31

known secrets after σ. Surely there are several snakes in the grass lying in wait for the intrepid investigator. Multiple transmission errors We can lift the restriction of one transmission error per protocol execution to f transmission errors per protocol execution. One call may now contain multiple transmission errors, and in both directions of the exchange. We need to choose between having for each agent f different incorrect values, on the assumption that all transmission errors are different, or having f occurrences of one incorrect value. The latter seems more suitable for faulty agents than for transmission errors, as faulty agents can repeatedly and intentionally send the same faulty message, whereas all transmission errors are presumably different. We recall that the two values a and a of the secret of a ‘really’ are, respectively, pairs (a, 1) and (a, 0) of the set of secret values A × {0, 1}. By enlarging this to A×{0, . . . , f } we get our set of at most f incorrect values per agent (f +1 values per agent, as it includes one correct value), denoted as a0 , . . . , af . However, in a different usage, we can also see these a0 , . . . , af are named occurrences of the same error. Already with merely two values but allowing f occurrences of an incorrect value, we can generalize the epistemic semantics with agents reasoning about sets of indistinguishable call sequences: instead of a majority of two in order to decide that a value is correct (that is, one more than the maximum of one error), we now need a majority of f + 1, and the worst case in order to be able to obtain that therefore consists of 2f + 1 calls, a well-known figure in distributed computing [13]. In the presence of multiple errors or multiple names of an error, knowing the secret would now be defined as Kv a b := Ka b0b ∨ . . . ∨ Ka bfb and the semantics of a call ab would need clauses ∗ removing all values bi among i = 0, . . . , f known to be incorrect from a’s holding on condition that Kv a b and therefore exactly one such Ka bjb for j ̸= i holds. The results for one error seem easily reproduced for the case of f errors. Beyond that, one can consider at most f errors per time frame of y calls (which seems a more realistic assumption), or at most f errors per agent (which seems to go easier on the formalization because we have a distributed system). Both directions seem promising to pursue. Instead of upper bounds on faults one could instead have a probability on the occurrence of faults. But that would call for an entirely different approach, because knowledge as complete certainty in a modal logic like ours can then never be obtained, given the nonzero chance of an error [16]. So that does not seem to be a promising direction of research to pursue in a modal logic. Faulty agents For a bound of f faulty (Byzantine) agents the expert goal of the gossip protocol should become: for all correct agents to hold the secrets of the correct agents, and similarly for the super expert goal. We recall that [26] also requires the correct agents to identify the incorrect agents, which is a stronger goal that seems hard to satisfy in a fully distributed setting. This subject is also deferred to future research, where we restrict ourselves here to a typical benchmark example for faulty agents, employing the same language and semantics. 32

Given B ⊆ A, a B expert is an agent who holds all secrets in the set B, and a B super expert is an agent who knows that all agents in B hold all secrets in B. As we use the same semantics, in particular we use the same observation relation, encoding that agents may not know they are faulty. Such faulty agents are therefore rather byzantine, in the sense of being randomly incorrect, than malicious or otherwise intentionally incorrect. However, it does at least not rule out that agents are always incorrect, as in the following example. Example 35 Given four agents a, b, c, d and initial secret distribution I = a|b|c|d, assume d is faulty and that d always sends the incorrect value d of its secret. Then after call sequence ab.cdd.ac.bdd , agents a, b, c correctly know the secrets of a, b, c, that is, those in B = A\{d} = {a, b, c} are correct B experts. Now consider the extended call sequence σ = ab.cdd.ac.bdd.ab.add.bc.cdd . We would like to achieve then that all the (correct) agents in B are B (correct) super experts. But, just as in Example 22, this is not the case. The agents do not even know they are correct, as for example the last call could also have been cd instead of cdd thus giving agent c a conflict for secret d; in other words, non-involved agents can not (and can never) rule out the possibility of a conflict in a call in which they are not involved. So S, σ ̸|= EB ExpB and a fortiori also S, σ ̸|= EB Expcor ⊣ B .

4.2

Epistemic perspectives

Belief We would like to say that values correct and incorrect are believed when not known, as there are so few errors. Such belief carries weight in our formalization, as we distinguish the (super) expert goal wherein we do not resolve such beliefs from the correct (super) expert goal wherein all is known. If ba ∧ ¬ba is true we say that agent a believes that the secret of agent b is b, and if ¬ba ∧ ba is true then agent a believes that the secret of agent b is b. We cannot merely identify the truth of local atoms ba resp. ba with this belief, as they also occur in the context ba ∧ ba wherein a has a conflict for secret b. We can make this belief formal and define Ba b := ba ∧ ¬ba and Ba b := ¬ba ∧ ba . We now have ∩b that that S, σ |= Ba b iff S[σ]∩b a = {b} and that S, σ |= Ba b iff S[σ]a = {b}. Because Kv a b as disjunct Ka bb implies Ba b, and Kv a b as disjunct Ka bb implies Ba b, ‘knowledge implies belief’ as expected. And belief does not imply knowledge, which is also expected. Even correct belief does not imply knowledge which might have been unexpected: we recall (Section 2.1) that correct belief bb ∧ba ∧¬ba does not imply knowledge Kv a b, simply because correct belief bb ∧ ba ∧ ¬ba does not imply known correct belief Ka (bb ∧ ba ∧ ¬ba ). Correct belief has to be justified by the epistemic semantics to become known. Only that amounts to knowing the secret: Kv a b is equivalent to Ka (bb ∧ ba ∧ ¬ba ) ∨ Ka (bb ∧ ¬ba ∧ ba ) (Corollary 14). Such belief Ba b is not a modality but a boolean abbreviation. For exampe, we cannot write ¬φ ∧ Ba φ for arbitrary formulas φ to express that belief is incorrect. Hope Another epistemic notion to consider is the one known in the literature as hope [13, 28]. An agent hopes φ, if φ is known conditionally on the agent being correct, definable 33

as Ha φ := Ka (correct a → φ). Such hope modalities are interpreted in Kripke models for partial equivalence relations (symmetric and transitive relations, with a corresponding modal logic KB4), where in the faulty part of the model the agent’s relation is empty. Now in our setting, agent a holding conflicting values for a secret b is like a having contradictory values for secret b, so it is like a knowing a contradiction (having an empty relation). But without actually being contradictory: to be interpreted as belief instead of conflict we merely require different values of secrets to be mutually exclusive. Known protocols We assumed that call sequences contain at most one faulty call and transmission error. This reduces the set of possible secret distributions when extending call sequences, because extensions that contain more than one faulty call are not allowed and can therefore not be indistinguishable for the agent. Or we assume the same, but with more faulty calls and at most f errors. Alternatively we could allow arbitrary call sequences, but impose restrictions on the observation relation and thus on indistinguishable call sequences, that are explicit in the logical language. A good candidate for such a logicbased restriction is the so-called protocol-dependent knowledge of [30, 15]: instead of the usual knowledge Ka φ we now have knowledge KaP φ which means that agent a knows that φ on the assumption that gossip protocol P is common knowledge, where we can think of protocol P as the combined call conditions Pab for all calls ab, such as ‘a does not know the secret of b’ or ‘a considers it possible that b does not know her secret’. In this particular case of gossip with errors we could therefore have knowledge Ka≤f φ where f becomes false when the call sequences contains more than f errors. (Formulas may also ′ contain epistemic modalities K P and K P for different protocols.) We would thus get the full observation model for the protocol ANY (including valuations for multiple values of secrets) but where the observation relations are partial equivalence relations that are empty when the ‘protocol is violated’, that is: when call sequences are extended so they contain more than f errors. Such Ka≤f knowledge modalities are KB4, not S5. The observation model defined in Section 2.1 is simply the restriction of this full observation model to the part with non-empty relations. Local state In a distributed system it is customary that an agent locally stores all the information it receives in messages from other agents. In contrast, in an (propositional) epistemic semantics some information is stored locally as the value of atomic propositions, in our case local atoms ba (and b) for a holding secret value b (b), and other information is stored indirectly in the Kripke model, in our case: the observation model. As a consequence, what is known as a local state in distributed computing is far more extensive than the valuation of local atoms for a given agent in a gossip state in the observation model (that is, in a world in a Kripke model). However, we can relate the two perspectives in a precise way. First: An agent a gathers the following information during the execution of a call sequence: for each call ab involving a (and for no other calls), agents a contributes a set of secret values X and receives from b a set of secret values Y (which include possibly 34

incorrectly transmitted values). The local state of agent a given an initial secret distribution S and after call sequence σ where a is involved in each call of subsequence τ is therefore: The set of secrets held by a before each call in τ and the set of secrets received by a from b in that call. local state (i) A global state is then an n-tuple of local states. Second: In our Kripke semantics the correspondent for agent a’s local state is: The pair consisting of the observation model and the ∼a equivalence class in that model containing the actual gossip state (S, σ), as well as agent a’s holding S[σ]a of local atoms. local state (ii) In multi-S5 Kripke models (with equivalence relations) the structure of the model is common knowledge and so also known to agent a, whereas agent a’s knowledge is determined by her equivalence class. Again, a global state is the n-tuple of local states of which the intersection . . . is the pair consisting of the observation model and the actual gossip state (S, σ), that is valued with secret distribution S[σ]!

4.3

Conclusion

We determined when epistemic goals can be obtained for a simple gossip protocol given a bound of at most one transmission error. The dynamic epistemic analysis allows to determine and resolve conflicts in novel ways, that also result in more optimal executions wherein agents may learn the correct value of the secret of another agent without calling that agent. We wish to generalize our results to asynchrony, to f transmission errors, and to f faulty agents. Beyond that, we wish to generalize it to other distributed epistemic gossip protocols and to restricted network conditions, and to obtain hard bounds for various optimality questions.

References [1] T. Achim, A. Best, and A. Bietti et al. Aristotle: IMO-level automated theorem proving, 2025. [2] T. Ågotnes and Y.N. Wáng. Resolving distributed knowledge. Artif. Intell., 252:1–21, 2017. [3] K.R. Apt and D. Wojtczak. Verification of distributed epistemic gossip protocols. J. Artif. Intell. Res., 62:101–132, 2018. [4] J. Aspnes and E. Ruppert. An introduction to population protocols. Bull. EATCS, 93:98–117, 2007. [5] M. Attamah, H. van Ditmarsch, D. Grossi, and W. van der Hoek. Knowledge and gossip. In Proc. of 21st ECAI, pages 21–26. IOS Press, 2014. 35

[6] B. Baker and R. Shostak. Gossips and telephones. Discrete Mathematics, 2(3):191 – 193, 1972. [7] A. Castañeda, J. Lefèvre, and A. Trehan. Self-healing routing and other problems in compact memory. CoRR, abs/1803.03042, 2018. [8] M.C. Cooper, A. Herzig, F. Maffre, F. Maris, and P. Régnier. The epistemic gossip problem. Discret. Math., 342(3):654–663, 2019. [9] A. Daliot and D. Dolev. Self-stabilization of byzantine protocols. In T. Herman and S. Tixeuil, editors, Proc. of 7th SSS (Self-Stabilizing Systems), volume 3764 of LNCS, pages 48–67, 2005. [10] D. Dolev. Self-Stabilization. MIT Press, 2000. [11] D. Dolev, M. Függer, M. Posch, U. Schmid, A. Steininger, and C. Lenzen. Rigorously modeling self-stabilizing fault-tolerant circuits: An ultra-robust clocking scheme for systems-on-chip. J. Comput. Syst. Sci., 80(4):860–900, 2014. [12] D. Dolev and E. Hoch. Constant-space localized byzantine consensus. In G. Taubenfeld, editor, Distributed Computing, pages 167–181, 2008. [13] K. Fruzsa, R. Kuznets, and U. Schmid. Fire! In J.Y. Halpern and A. Perea, editors, Proc. of the 18th TARK, volume 335 of EPTCS, pages 139–153, 2021. [14] T. Furer. Unreliability in social networks. Master’s thesis, University of Bern, 2023. [15] M. Gattinger. New Directions in Model Checking Dynamic Epistemic Logic. PhD thesis, University of Amsterdam, 2018. ILLC Dissertation Series DS-2018-11. [16] J.Y. Halpern. Reasoning about Uncertainty. MIT Press, Cambridge MA, 2003. [17] S.M. Hedetniemi, S.T. Hedetniemi, and A.L. Liestman. A survey of gossiping and broadcasting in communication networks. Networks, 18:319–349, 1988. [18] A. Herzig and F. Maffre. How to share knowledge by gossiping. AI Commun., 30(1):1– 17, 2017. [19] A.-M. Kermarrec and M. van Steen. Gossiping in distributed systems. SIGOPS Oper. Syst. Rev., 41(5):2–7, 2007. [20] R. Kuznets, L. Prosperi, U. Schmid, and K. Fruzsa. Epistemic reasoning with Byzantine-faulty agents. In Proc. of 12th FroCoS, pages 259–276, 2019. LNCS 11715. [21] The mathlib Community. The Lean mathematical library. In Proc. of 9th CPP, pages 367–381, 2020.

36

[22] Y. Moses and M.R. Tuttle. Programming simultaneous actions using common knowledge. Algorithmica, 3:121–169, 1988. [23] L. de Moura and S. Ullrich. The Lean 4 Theorem Prover and Programming Language. In Automated Deduction – CADE 28, pages 625–635. Springer, 2021. [24] R. Tijdeman. On a telephone problem. Nieuw Archief voor Wiskunde, 3(19):188–192, 1971. [25] L. van den Berg. Unreliable gossip. Master’s thesis, University of Amsterdam, 2018. MoL-2018-01. [26] L. van den Berg and M. Gattinger. Dealing with unreliable agents in dynamic gossip. In M.A. Martins and I. Sedlár, editors, Proc. of 3rd DaLí, pages 51–67, 2020. LNCS 12569. [27] H. van Ditmarsch. Reasoning about gossip. Manuscript to appear with Cambridge University Press, 2026. [28] H. van Ditmarsch, K. Fruzsa, and R. Kuznets. A new hope. In D. Fernández-Duque and A. Palmigiano, editors, Proc. of the 14th AiML, pages 349–369. College Publications, 2022. [29] H. van Ditmarsch and M. Gattinger. You can only be lucky once: optimal gossip for epistemic goals. Mathematical Structures in Computer Science, page 1–28, 2024. [30] H. van Ditmarsch, M. Gattinger, L.B. Kuijer, and P. Pardo. Strengthening gossip protocols using protocol-dependent knowledge. FLAP, 6(1):157–203, 2019. [31] H. van Ditmarsch, M. Gattinger, and R. Ramezanian. Everyone knows that everyone knows: Gossip protocols for super experts. Stud Logica, 111(3):453–499, 2023. [32] H. van Ditmarsch, J.Y. Halpern, W. van der Hoek, and B. Kooi, editors. Handbook of epistemic logic. College Publications, 2015. [33] H. van Ditmarsch, W. van der Hoek, and L.B. Kuijer. The logic of gossiping. Artificial Intelligence, 286:103306, 2020. [34] H. van Ditmarsch, J. van Eijck, P. Pardo, R. Ramezanian, and F. Schwarzentruber. Epistemic protocols for dynamic gossip. J. Applied Logic, 20:1–31, 2017. [35] H. van Ditmarsch, J. van Eijck, P. Pardo, R. Ramezanian, and F. Schwarzentruber. Dynamic gossip. Bulletin of the Iranian Mathematical Society, 45(3):701–728, 2019. [36] D.B. West. A class of solutions to the gossip problem, part I. Discrete Mathematics, 39(3):307–326, 1982.

37

Appendix: formalizing self-correcting gossip in Lean Lean is a functional programming language and an interactive theorem prover [23]. We formalized the semantics for self-correcting gossip described in this paper using Lean and its mathematical library mathlib [21]. In particular we verify that the semantics is wellfounded, and various properties of the notions of knowledge and belief. Here we highlight some aspects of the formalization. The full documentation of the formalization is available at https://m4lvin.github.io/Gossip-in-Lean/docs/Gossip/Error/Basic.html The whole formalization is (implicitly) parameterized by the number of agents n. To represent the set of all agents we use Fin n, the finite type with n elements. Calls are then defined as follows with three constructors, corresponding to the cases where there is no transmission error (ab), an error from the caller (ac b), or an error from the callee (abc ). inductive Call : Type /-- ⌜a b⌝ -/ | normal : (caller : @Agent n) → (callee : { b : @Agent n // b ̸= caller }) → Call /-- ⌜a^c b⌝ -/ | fstE : (caller : @Agent n) → (err : @Agent n) → (callee : { b : @Agent n // b ̸= caller }) → Call /-- ⌜a b^c⌝ -/ | sndE : (caller : @Agent n) → (callee : { b : @Agent n // b ̸= caller }) → (err : @Agent n) → Call

We make heavy use of the notation command in Lean so that we can denote agents, values and calls in a way that is more similar to our notation here in the paper. For example, instead of Call.sndE a b c we can also write ⌜a b^c⌝ for the call abc . A sequence of calls is then just a List of calls. For convenient pattern matching we let the head of the list denote the most recent call. To also ensure sequences contain at most one error we define a function maxOne and then let OSequence be its Subtype. A key part of the formalization are four functions that correspond to the definitions in section 2.1. Below is the Lean code for eval corresponding to |= from Definition 6. def eval : @Dist n → @OSequence n → @Form n → Prop | _, _, .Top => True | S, σ, .Neg φ => ¬ eval S σ φ | S, σ, .Has a (j,k) => (j,k) ∈ resultSet a S σ | S, σ, .Con φ ψ => eval S σ φ ∧ eval S σ ψ | S, σ, .K a φ => ∀ t, ∀ τ , (he : equiv a (S,⟨σ,rfl⟩) (t,τ )) → eval t τ φ termination_by _ σ φ => (σ.length, φ.length) -- use lexicographic order to show termination decreasing_by -- Sequence length stays the same, but formula becomes shorter. · apply Prod.Lex.right [. . .]

38

(↓, =) (=, ↓) contribSet(|σ|,1)

(↓, =)

(↓, ↑) =)

(↓, ↑)

(↓,

equiv(|σ|,0)

(=, ↓)

resultSet(|σ|,0) (↓, ↑) eval(|σ|,|φ|)

(=, ↓)

Figure 1: Mutual recursion and termination proof. Edge labels say how (|σ|, |φ|) changes. We need to convince Lean that the eval function terminates, corresponding to the question whether our semantics is well-founded, as discussed on page 7. Just like the definitions in Section 2.1 are mutually recursive, also in Lean we need to place the function eval inside a mutual block together with functions that encode the other definitions: resultSet and contribSet formalize Definition 4 for the semantics of calls, and equiv formalizes Definition 5 for the observation relation. Each function then also has a termination_by annotation that labels each recursive call with a value in the lexicographic order of pairs of sequence length and formula length. In the decreasing_by block we then provide proofs that indeed in each recursive call the values are decreasing. We visualize the mutual recursion in Figure 1 where each arrow represents a recursive call from one function to another (or itself) and is labelled by how the lexicographic value changes. Again we define shorter notation, so that we can write S⌈σ⌉ |= φ instead of eval S σ φ and so that we can write S⌈σ⌉a for resultSet a S σ . We also write b @ a for the atom ba saying that a has value b. To denote values b or b we use (b, k) where k is a Bool value. One of the first results we prove in Lean is equiv_Equivalence, saying that ∼a is indeed an equivalence relation. Besides this, we also show the results from Section 2.2, as shown in Figure 2. Parts of our Lean code were written by the Aristotle tool [1], and we refer to the git repository for details.

39

/-- Lemma 7 -/ lemma indistinguishable_then_same_values {n} {a : @Agent n} {S T: @Dist n} {σ τ : OSequence} : (S, σ) ~_a (T, τ ) → S⌈σ⌉a = T⌈τ ⌉a /-- Lemma 8 -/ lemma local_is_known {a b : @Agent n} (k : Bool) : ⊨ (( ⟨b,k⟩ @ a ) =⇒ (K a ( ⟨b,k⟩ @ a) )) ∧ ⊨ ((Neg (⟨b,k⟩ @ a)) =⇒ (K a (Neg (⟨b,k⟩ @ a)))) /-- Lemma 9 -/ lemma stubbornness m σ (h : σ.length = m) : S⌈σ⌉ |= (a, k) @ a

↔

S a = k

/-- Lemma 10 -/ lemma knowledge_of_secrets_is_preserved {a b : @Agent n} (hKv : S⌈σ⌉ |= Kv a b) (hSub : σ ⊑ τ ) : S⌈τ ⌉ |= Kv a b /-- Lemma 12 -/ lemma consider_corrected (a b : @Agent n) {S : @Dist n} {σ : @OSequence n} {k : Bool} (real_b_is_k : S b = k) (a_has_no_b_k : (b, k) ∈ / S⌈σ⌉a) : equiv a (S, ⟨σ, rfl⟩) (S.switch b, ⟨⟨cor b σ, cor_maxOne σ.2⟩, cor_same_length⟩) /-- Proposition 13 -/ lemma knowledge_implies_correct_belief {n} {a b : @Agent n} {k} : V V ⊨ (K a ((b,k) @ b)) =⇒ (((b,k) @ b) ((b,k) @ a) (¬’(b, !k) @ a)) /-- Corollary 14 -/ lemma knowledge_is_justified_true_belief {n} {a b : @Agent n} : V V ⊨ K a ((b,k) @ b) ⇔ K a ( ((b,k) @ b) ((b,k) @ a) (¬’ (b, !k) @ a))

Figure 2: Overview of results proven in Lean (with links to documentation).

40