arXiv CSopen access

An Epistemic Analysis of Random Coordinated Attack

An Epistemic Analysis of Random Coordinated Attack Sophia Knight # University of Minnesota Duluth, Duluth, Minnesota

David Lehnherr # Independent researcher

Sergio Rajsbaum # Instituto de Matemáticas, UNAM, Mexico City, Mexico and IRIF Université Paris Cité, Paris, France

arXiv:2606.17860v1 [cs.DC] 16 Jun 2026

Abstract The coordinated attack problem models the challenges of coordinating a joint action that needs to be performed in a bounded amount of time, by communicating over unreliable links. It is the first distributed computing problem to be proven to be unsolvable. Analysis of coordinated attack also revealed the importance of common knowledge, a central concept of epistemic logic. However, the randomized version of coordinated attack, which is solvable, has not, to the best of our knowledge, been studied through the lens of probabilistic epistemic logic, where processes can generate randomness by flipping coins. In this work, we present a general epistemic logic framework to study randomized algorithms with a bounded number of rounds. It can be used to study tasks such as coordinated attack, approximate agreement, and consensus. The framework can be used to study general dynamic graph models: synchronous systems where reliable processes execute a bounded number of rounds, and messages can be lost, as determined by an adversary. We combine techniques from the logical characterization of dynamic networks and the notion of task solvability in distributed computing with ideas from probabilistic dynamic epistemic logic. The framework is inspired by the operational model of Varghese and Lynch that introduced randomized coordinated attack. More broadly, the resulting notion of probabilistic epistemic task solvability provides a foundation for the epistemic study of randomized distributed computation. Using this framework, we analyze the algorithm of Varghese and Lynch from a knowledgetheoretic perspective, providing a more formal treatment of both the algorithm and its corresponding lower bound. As a byproduct, we improve the lower bound to make it tight. Our lower bound proof relies on indistinguishability arguments, demonstrating that reasoning about knowledge remains important in the probabilistic setting. In addition to the tight lower bound, we give a formal semantics of the crucial notion of ‘information level’ introduced by Varghese and Lynch by showing that it corresponds to a specific epistemic formula. 2012 ACM Subject Classification Theory of computation → Modal and temporal logics; Computing methodologies → Distributed algorithms; Theory of computation → Probabilistic computation Keywords and phrases Distributed computing, Random coordinated attack, Probabilistic epistemic logic, Task solvability Digital Object Identifier 10.4230/LIPIcs...0

1

Introduction

The coordinated attack problem [1] was formalized by Jim Gray in 1978 [2], to identify the challenges of coordinating an action that must be performed in a bounded amount of time, communicating over an unreliable channel. Such coordination is needed often in databases, networking, and other distributed systems. Thus, it was historically significant as the first distributed problem proven to be unsolvable. Moreover, it initiated the study of distributed © CC-BY 4.0; licensed under Creative Commons License CC-BY 4.0 Leibniz International Proceedings in Informatics Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

0:2

An Epistemic Analysis of Random Coordinated Attack

computability and underscored the role of common knowledge, a central concept in epistemic logic [3]. The model used for this classic impossibility result comprises a set of reliable processes that communicate through message exchange in synchronous rounds. It is a very weak model, allowing failure of all links, in every round. The coordinated attack problem is stated in terms of three requirements, for processes starting with initial values that are binary inputs, and outputting binary decision values after some bounded number of rounds, R: Validity: 1. If any process starts with an initial value of 0, then 0 is the only possible decision value for every process. 2. If all processes start with an initial value of 1, and all messages are delivered, then 1 is the only possible decision value for every process. Agreement: All processes choose the same decision value. Termination: Each process eventually outputs a decision value. Since this problem is unsolvable by a deterministic algorithm [4], Varghese and Lynch [5] studied randomized coordinated attack with slightly different correctness conditions: Validity: 1. If any process starts with an initial value of 0, then 0 is the only possible decision value for all processes. 2. If all processes start with an initial value of 1 and all messages are delivered, then 1 is the only possible decision value for all processes. Randomized Agreement: The probability that all processes do not output the same decision value is smaller than ϵ. Termination: All processes eventually output a decision value. Under a deterministic, non-adaptive adversary that cannot read message bits, Varghese and Lynch present an R-round algorithm, and show that it is essentially optimal in terms of ϵ. 1 The algorithm has ϵ = 1/R and they show that the general lower bound is R+1 . The impossibility of coordinated attack is frequently taught in networking, database and distributed computing courses. However, randomized coordinated attack deserves more attention. The ideas for both the algorithm and the lower bound are elegant and simple, described subsequently by Lynch [6, Chapter 5] and Aspnes [7, Chapter 8]. However, little subsequent work has focused on either the algorithm or the lower bound. Despite their simplicity, these results merit closer examination. To begin with, the (small) gap between R1 1 and R+1 is intriguing, and there seems to be an underlying epistemic interpretation: from Lynch’s book Section 5.2.2. (P. 88): “The algorithm is based on what processes know about each other’s initial values and on what they know about each other’s knowledge of the initial values, and so on.” We formalize this claim and elucidate its significance by characterizing both the knowledge gained by processes in the algorithm and the knowledge that remains unattainable in the lower-bound argument. The benefit obtained is first of all, a new exposition of the results, which formalizes the intuitive arguments, and reveals their generality. Once a precise epistemic understanding is reached, it becomes clear how to close the gap between the lower and upper bounds. The core contributions of the present paper are: 1. A probabilistic epistemic framework for randomized bounded synchronous distributed computation. 2. An epistemic characterization of information levels.

Knight, Lehnherr, Rajsbaum

3. A tight lower bound for randomized coordinated attack. 4. A framework that is applicable to general models of communication. The developed framework combines approaches from distributed computing and logical methods for reasoning about uncertainty. We demonstrate the generality of our framework by analyzing randomized coordinated attack in the iterated immediate snapshot model of communication (IIS). A central contribution of this paper is a probabilistic epistemic framework for reasoning about randomized distributed computation. The framework makes it possible to analyze randomized coordinated attack through the lens of knowledge and reveals a common structure underlying both the algorithm of Varghese and Lynch and its lower bound. In this view, information levels correspond to finite levels of iterated knowledge, while the lower bound follows from fundamental constraints on the acquisition of knowledge. This unification not only provides a conceptual explanation of the original results, but also closes the gap between the known upper and lower bounds. The paper is organized as follows. Section 2 defines the operational and logical models of interest, and provides preliminary notions for epistemic logic. In Section 3, the introduced machinery is used to state probabilistic task solvability for epistemic models formally. Section 4 showcases applications of the developed framework, by proving the aforementioned one-to-one correspondence and tightening the lower bound for randomized coordinated attack. Finally, Section 5 concludes our paper and discusses possible future work.

Additional Related Work Over the last decades, several mathematical frameworks for reasoning about distributed task solvability have been developed. Approaches based on combinatorial topology [8], point-set topology [9], and epistemic logic [10] have all led to important insights into the limits of distributed computation. More recently, the seminal work of Goubault et al. [11] bridges topological models and epistemic logic, by relating task solvability to dynamic epistemic logic [12]. In their work, dynamic epistemic logic is used to model how the knowledge of processes evolves through communication. Inspiration for this approach was earlier work by Castañeda et al. [13], which looks at communication patterns epistemically. These works focus on deterministic algorithms for distributed tasks. In contrast, randomized distributed computation introduces an additional probabilistic dimension, both through randomized process behavior and through uncertainty induced by communication failures. In this work, we focus on randomized process behavior, whereas stochastic communication failures have recently been studied by Fraignaud et al. [14]. We stress that we consider the case of bounded computation, which is different from the well developed research line on randomized algorithms for consensus with no agreement error, but requiring termination only with high probability e.g. [15] and [7, Chapter 24]. Knowledge based on probabilistic actions has been studied using probabilistic dynamic logic [16], as well as in the famous interpreted systems model (see [3]), by Halpern [17, 18]. Building on the approach of Goubault et al. [11], communication patterns [13], probabilistic epistemic semantics [16, 17, 18], and the operational model of Varghese and Lynch [5], we develop a novel probabilistic epistemic framework for randomized distributed computation. The framework allows us to analyze problems such as randomized coordinated attack through notions of indistinguishability, iterated knowledge, and probabilistic uncertainty.

0:3

0:4

An Epistemic Analysis of Random Coordinated Attack

2

Operational and logical models

We begin by introducing the model from Lynch [6, Chapter 5], which we call the operational model, generalizing to arbitrary message delivery patterns, following recent research on dynamic networks, but extended with probabilities. Then we introduce a corresponding epistemic model, inspired by the frameworks [11, 13], extending it with probabilities, following [16]. We also present an epistemic notion of probabilistic task solvability. A main goal of this section is to show that the operational model and the epistemic model are in a sense equivalent.

2.1

Operational model

For a positive integer k ∈ N, we define [k] := {1, . . . , k}, and if a = (ai )i∈[k] is a sequence then ai denotes its i-th element. Throughout this work, the set N is a set of n processes, denoted p1 , . . . , pn , or simply p, q, and r if no ambiguity arises. We use vpi for the component of a vector v associated with process pi . Before starting a protocol, processes are assigned a private input value from a domain D by an input configuration I : N → D. In this paper, we consider binary inputs, i.e., D = {0, 1}. The set of all input configurations is denoted by I. Communication and protocol. A communication protocol consists of R synchronous rounds, where at the beginning of each round every process sends a message to all other processes. Messages sent in a given round are simultaneously received at the end of that round, or are lost otherwise. Throughout this work, we only consider full information protocols with perfect recall. That is, processes send their local state in each round, and remember everything they have received. We denote p’s message in round r by mp,r . A communication graph is a directed graph whose vertex set corresponds to the set of processes N . An edge (p, q) in a communication graph indicates that the message sent by process p is delivered to process q. The message mp,r is always received by process p. Consequently, every vertex has a loop. Given a communication graph G := (N, E), we define inp (G) := {q ∈ N | (q, p) ∈ E} as the set of processes from which p receives messages. A set of communication graphs is called a communication pattern. Adversary. The adversary A chooses inputs and determines which messages are delivered in each round by selecting a communication graph for every round, from a fixed set of graphs. This corresponds to an oblivious adversary, as the set of possible graphs in each round is the same, and the adversary can select any graph from this set, e.g. [19]. In the usual setting of the coordinated attack problem, the adversary can select any directed graph, including the one where no messages are delivered to other processes. Executions. An execution models the evolution of the local states of processes over R rounds, in a full information protocol. These do not include decision values, which we model later on. We distinguish between deterministic and probabilistic executions. In a deterministic execution, processes start in an input configuration I ∈ I, and the adversary A drops messages according to a sequence of communication graphs G := (Gr )r∈[R] , where Gr := (N, Er ), denoting the set of successful channels at each round. Deterministic executions can thus be parametrized by a tuple α = (I, G). The set of messages received by process p at the end of round r is recp (G, r) := {mq,l | (q, p) ∈ El for some l ≤ r}.

Knight, Lehnherr, Rajsbaum

Since processes have perfect recall, the local state of a process p in execution α at the end of round r is sp (α, r) := (I(p), recp (G, r)). Moreover, because we only consider full information protocols, processes send their local state in each round, i.e., mp,r = sp (α, r − 1). In a probabilistic execution, processes generate randomness by tossing coins. Since we assume full information protocols, the only randomization in their behavior is to include the outcome of random coins in messages, and at the end, the decision of a process may depend on the random coin values that the process has seen in the past (the number of rounds executed is fixed a priori, and cannot be affected by the randomness). We define the set of all probabilistic executions to be Ω. We stress that we assume the random coin values are not observable by the adversary. Thus, there is a probability distribution over executions, once the adversary fixes inputs and communication graphs. The local randomness of a process p is a random vector X̄p = (Xp,1 , . . . , Xp,R ), where each Xp,r is an independent random variable with finite support sampled by process p in round r. Assuming finite support reflects the standard computational interpretation of randomized distributed algorithms, where processes generate randomness using finite random bit strings (e.g., coin flips). We define X̄p|r := (Xp,1 , . . . , Xp,r ), and write x̄p and x̄p|r for realizations of X̄p and X̄p|r respectively. We use X for the joint variable (X̄p1 , . . . , X̄pn ). Intuitively, X captures the randomness underlying an execution. We define a probability space O = (X, 2X , µ), where µ : 2X → [0, 1] is a probability measure. A probabilistic execution with respect to O is a triple α = (I, G, x), where (I, G) is a deterministic execution and x is an element of X. If the adversary A chooses I and G, the probability that the execution is (I, G, x) equals µ({x}). Moreover, conditioned on I and G, probabilities sum up to 1, i.e., X X Pr[(I, G, x)] = µ({x}) = 1. ∀x∈X.(I,G,x)

x∈X

For a probabilistic execution α = (I, G, x), the local state of process p at the end of round r additionally contains the sampled randomness over rounds: sp (α, r) := (I(p), x̄p|r , recp (G, r)). Decisions. At the end of an execution, processes output a decision value. Let Ω be the set of all executions. For each p ∈ N , we define Sp := {sp (α, R) | p ∈ N and α ∈ Ω}, as the set of all possible local states at the end of executions in Ω. We model decisions of processes as a function δp : Sp → {0, 1} and define δ to represent the decision of all processes. For fixed I and G, this induces a probability distribution on decisions for each process p. For example, conditioned on I and G, the probability that process p decides the value 1 is Pr[{α ∈ Ω | α = (I, G, ·) and δp (sp (α, R)) = 1}]. To simplify notation, we write PrI,G [p decides 1] for the above expression. Lemma 1 is a standard result and states that the probability of a process deciding 1 (or 0) is the same in executions it cannot distinguish (the proof can be found in [6]).

0:5

0:6

An Epistemic Analysis of Random Coordinated Attack

▶ Lemma 1. Let I, I ′ ∈ I, G, G′ be sequences of communication patterns, p ∈ N , and x, x′ ∈ X with x̄p = x̄′p such that sp ((I, G, x), R) = sp ((I ′ , G′ , x′ ), R). We find that PrI,G [p decides 1] = PrI ′ ,G′ [p decides 1]. Example 2 shows how our operational model depicts probabilities. The mentioned algorithm (here only outlined) will be explained in Section 4.1. ▶ Example 2. Varghese and Lynch [5] propose a simple algorithm to solve the randomized coordinated attack problem in n rounds. Before sending its first message, a designated process p rolls a fair n-sided die (the so-called key k) and appends the value to its message. Throughout the protocol, processes compute their information level (formalized later), which is an integer and depends only on the adversarial choice of I and G. It can be shown that processes disagree only if k is equal to a specific level among processes. Consequently, since the adversary fixes I and G, it holds that PrI,G [ processes disagree ] =

2.2

1 . n

Logical model

This section will introduce logical concepts to later reason about the operational model introduced in Section 2.1. We first introduce the logical language used throughout the paper, and then build toward the introduction of probabilistic epistemic models. Language. The set of propositional variables is Prop. For p ∈ Prop and i ∈ N , the language L is inductively defined by the following grammar: ϕ ::= p | ¬ϕ | (ϕ ∧ ϕ) | Kp ϕ. The formula Kp ϕ means that process p knows ϕ. We also define the everybody knows modality ^ Eϕ := Kp ϕ. p∈N

We set E 0 ϕ := ϕ and E n ϕ := E(E n−1 ϕ). In addition to knowledge, we also define a probabilistic modality P≤s ϕ that denotes that the probability of ϕ being true is a most s. We stress that P≤s is a global operator, meaning that probabilities are not assigned by processes, but by the adversary (or the environment) instead. This is in line with the operational probability space O, which induces probabilities over executions from the global perspective of the adversary. Thus, P≤s ϕ means that the adversary believes that ϕ is true with at most probability s. For convenience, we abbreviate P>s ϕ, P<s ϕ, P≥s , and P=s ϕ, which can all be defined in terms of P≤s ϕ. The extension of L with the modality P≤s is denoted by LP . Kripke frames. To model what processes and the adversary can distinguish during an execution, we use Kripke frames. Formally, let W be a set of worlds (global states) and A be a set of agents (e.g., processes or the adversary). A Kripke frame is a pair (W, (∼a )a∈A ) where each ∼a is an equivalence relation on W , also called an indistinguishability relation. We write [w]a for the equivalence class of w under ∼a . For a set of worlds W , we differentiate between two frames: 1. the process-frame FN = (W, (∼p )p∈N ); and 2. the adversarial frame FA = (W, ∼A ).

Knight, Lehnherr, Rajsbaum

0:7

The frames are interpreted as follows; if w ∼p v, then process p cannot distinguish between the worlds w and v; if w ∼A v, then the adversary A cannot tell the two worlds apart. A Kripke model is a triple M = (FN , FA , V ), where FN and FA contain the same set of worlds and V : W → 2Prop is a valuation. Adding a valuation V to a frame enables us to reason about what agents actually know. Probabilistic models. Consider an arbitrary Kripke model M = (FN , FA , V ). We equip each world of the adversarial Kripke Frame FA with a probability space Ow := ([w]A , 2[w]A , µw ) such that Ow = Ov , if w ∼A v. We call the frame FA = (W, ∼A , (Ow )w∈W ) a probabilistic adversarial frame. Furthermore, notice that this choice of modeling implies that X µw (v) = 1. v∈[w]A

An A-probabilistic model is a triple M = (FN , FA , V ), where V : W → 2Prop is a valuation. Definition 3 illustrates the notion of truth in A-probabilistic models. Notice that probabilities are always evaluated relative to an adversarial equivalence class. Hence, probabilistic formulas express probabilities relative to the adversary’s uncertainty. ▶ Definition 3 (|=). Let M := (FN , FA , V ) be an A-probabilistic model. For every world w ∈ W we define the relation M, w |= ϕ by induction on ϕ: M, w |= p

iff

p ∈ V (w)

M, w |= ¬ϕ

iff

M, w ̸|= ϕ

M, w |= ϕ ∧ ψ

iff

M, w |= ϕ and M, w |= ψ

M, w |= Kp ϕ

iff

∀v ∈ [w]p .M, v |= ϕ.

M, w |= P≤s ϕ

iff

µw ({v ∈ [w]A | M, v |= ϕ}) ≤ s.

Let M = (FN , FA , V ) be an A-probabilistic model. A formula ϕ ∈ LP is valid in M, denoted M |= ϕ, if it is true in all worlds.

2.3

Translation

This section introduces the necessary machinery to picture the operational model logically. Besides standard communication updates we also define updates that model the generation of local randomness. Readers familiar with the literature on dynamic epistemic logic will observe that we do not define the updates based on action models. This is purposely done as to not overload the presentation with additional notation. Details on communication updates can be found in [13]. Action models for the generation of randomness are straightforward (as we will demonstrate), because computing probabilities is not part of the update itself. Communication update. Let FN = (W, ∼p )p∈N be a process frame and consider a communication pattern G = {G1 , . . . , GR }. We define the communication update: FN ⊗ G := (W ⊗ , ∼⊗ p )p∈N , ′ where W ⊗ := {(w, Gi ) | w ∈ W and Gi ∈ G}, where (w, Gi ) ∼⊗ p (w , Gj ) if and only if ′ w ∼p w and inp (Gi ) = inp (Gj ). In other words, a process p cannot distinguish two worlds (w, Gi ) and (w, Gj ) if and only if it cannot distinguish w from w′ and receives messages from the same set of processes in Gi and Gj .

0:8

An Epistemic Analysis of Random Coordinated Attack

▶ Example 4. In the immediate snapshot model IS processes communicate by using snapshots and at least one message gets received. Figure 1 depicts the update for two processes p and q, and one global state w. In the frame on the right ⊤⊥ means that p received q’s message but p’s message to q was lost. This scenario corresponds to the communication graph Gp := {(q, p), (p, p), (q, q)}. Moreover, p cannot distinguish ⊤⊥ from ⊤⊤, which corresponds to the communication graph Gpq := {(p, q), (q, p), (p, p), (q, q)}. Formally, p cannot distinguish the worlds induced by Gp and Gpq because inp (Gp ) = inp (Gpq ) = {p, q}. update

w

⊤⊥

p

⊤⊤

q

⊥⊤

Figure 1 A simple message update for IS.

Configuration update. A process frame FN = (W, ∼p )p∈N can be updated with a set V of vectors each containing n values. We define the configuration update of FN with V as: FN ◦ V := (W ◦ , ∼◦p )p∈N , where W ◦ := {(w, v) | w ∈ W and v ∈ V} and (w, v) ∼◦pi (w′ , v ′ ) if and only if w ∼pi w′ and vpi = vp′ i . Example 5 shows an update involving two processes, each privately tossing a coin. ▶ Example 5. Consider two processes p and q and an initial global state w. Each process privately tosses a coin. Without any communication between the processes, this results in four possible global states. Since each process observes the outcome of its own coin toss, it only considers global states possible in which its local outcome is the same. For example, in Figure 2 in the global state T T , both processes observe tails. Process p knows that its own outcome is tails, but does not know the outcome observed by q. Hence, from the perspective of p, both T T and T H are possible. N -execution Frame. We now build a frame that corresponds to the execution from the perspective of a process. The constructions starts from an input frame for private inputs I = (I, ∼p )p∈N , where I1 ∼p I2 if and only if I1 (p) = I2 (p), and iteratively applies configuration and message updates. Let (Gr )r∈[R] be a sequence with the communication patterns for each round. Further for r ∈ [R], let Xr be the set containing all possible realizations of the joint variable (Xp1 ,r , . . . Xpn ,r ). The N -execution frame FNA is iteratively constructed as follows: F1 := (I ◦ X1 ) ⊗ G1 , F2 := (F1 ◦ X2 ) ⊗ G2 , . . . , FNA := (FR−1 ◦ XR ) ⊗ GR . We use the superscript A to be consistent with literature on task solvability and dynamic epistemic logic. Historically, A is used to emphasize the action model, which we do not model explicitly for compactness. q TT w

update

p TH

HT

p q HH

Figure 2 A simple configuration update for two private local coin tosses.

Knight, Lehnherr, Rajsbaum

0:9

We write (I, G, x) for the worlds of FNA where I is the initial input configuration, G is the sequence of communication graphs applied to I, and x is the sampled randomness. Lemma 6 states the relation between FNA and the set of all possible probabilistic executions Ω. ▶ Lemma 6. There is a one-to-one correspondence between the set of all probabilistic executions Ω and the N -execution frame FNA . Furthermore, a process p cannot distinguish ′ two worlds w = (I, G, x) and w′ = (I ′ , G′ , x′ ), denoted w ∼A p w if and only if it has the same ′ local state in both executions, i.e., sp (w, R) = sp (w , R). Proof. The proof is standard (see for example [3, 13]).

◀

A-execution frame. We can build a probabilistic adversarial execution frame FAA from the worlds of FNA . The adversarial indistinguishability relation is given by: ′ ′ ′ (I, G, x) ∼A A (I , G , x )

iff.

I = I ′ and G = G′ .

The probability space O = (X, 2X , µ) of the operational model, naturally induces a probability space Oα for every probabilistic execution α = (I, G, x) ∈ Ω, which defines a probabilistic adversarial frame. Here, the probability measure must be conditioned on being in worlds of [α]A . The measure normalizes correctly, if the operational measure normalizes. Formally, we set Oα := ([α]A , 2[α]A , µ|[α]A ), where µ|[α]A is the operational measure µ conditioned on the adversarial choice of I and G. Constructing FAA after the configuration update is possible because the operational model already encodes randomness via realizations of the joint random variable X. In more general dynamic epistemic settings, probabilistic updates modify probability distributions during the update process itself. This requires genuinely dynamic probabilistic update mechanisms as developed in [16, 20]. Execution model. The set Prop contains all propositional variables. The variables describe either inputs or realizations of a random variable Xp,r . The propositional variable ip represents process p’s binary input, and xsp,r encodes the randomness of process p in round r. Notice, that s depends on the support of the random variable Xp,r , denoted by supp(Xp,r ). Formally, the set propositional variables is: Prop := {ip | p ∈ N } ∪ {xsp,r | r ∈ [R], p ∈ N and s ∈ supp(Xp,r )}. The execution model is a triple I[A] = (FNA , FAA , V A ), where V A is a valuation such that: 1. ip ∈ V A ((I, G, x))) if and only if I(p) = 1; 2. xsp,r ∈ V A ((I, G, x)) if and only if xp,r = s. Again, we use I[A] to adhere to previous literature. The notation emphasizes that the execution is built from the set of possible inputs by applying updates.

3

Task solvability

We now provide a novel notion of probabilistic task solvability for epistemic models. This definition does not depend on the operational model for randomized coordinated attack, and characterizes the solvability of various randomized tasks. We follow the standard approach of relating task solvability to the existence of a map from inputs to admissible outputs. Task model. Let T be a task. The task model I[T ] = (FNT , FAT , V T ) is built over a set of output worlds W T , where each world is of the form (I, G, o). Here, o is an output vector

0:10

An Epistemic Analysis of Random Coordinated Attack

I[A] := (FNA , FAA , V A )

δ induces (FNO , FO A)

communication and configuration updates

O MO := (FNO , FO A,V )

implies V O

I

task specification yields I[T ]

I[T ] := (FNT , FAT , V T )

Figure 3 Illustration of probabilistic epistemic task solvability. The execution model I[A] and the task model I[T ] can be constructed based on the input frame I. The task model together with a decision function δ induce the output model MO . A task is solvable if and only if there exists a decision function δ such that MO satisfies the logical representation of the task specification.

compatible with the input configuration I ∈ I. Two worlds are indistinguishable for a process if and only if they have the same outputs and inputs, i.e., op = o′p and I(p) = I ′ (p). The valuation V T assigns propositional variables denoting the inputs and outputs as in Section 2.3. Encoding the delivered messages is necessary for modeling the adversary. The adversarial indistinguishability relation is as before. We stress that the model I[T ] is deterministic. Similar to the operational model, probabilities are induced by a decision function. Decisions. Given an execution model I[A], we model the decision of processes as a function δ : W A → {0, 1}n from the worlds of the execution model to a binary output vector. The only condition is that processes decide the same values in indistinguishable global states, i.e., ′ ′ for all processes p ∈ N , we have w ∼A p w implies that δ(w)p = δ(w )p . Given a decision function δ, we transform the adversarial task model FAT into an AO probabilistic output frame FO A . The set of worlds for FA is W O := {(I, G, o) ∈ W T | ∃(I, G, x) ∈ W A .δ((I, G, x)) = o}. T In words, the frame FO A is formed over the worlds of FA that are actually produced by δ. This is needed in order to properly define a probability measure for each world. Notice, that this deviates from the deterministic notion of task solvability in [11]. ∗ O We define a probability measure µO and event w∗ for each world w := (I, G, ·) ∈ W ∗ E ⊆ [w ]A , in terms of the operational measure conditioned on the choice of I and G:

µO w∗ (E) = µ({x ∈ X | (I, G, δ(I, G, x)) ∈ E}). The probability space for each world w∗ ∈ W O is then defined as before. The measure µO normalizes correctly because the preimages induced by δ partition the worlds of MA , and the operational measure µ sums to 1 on every adversarial equivalence class. The output O T O model MO := (FNO , FO as well, and defining an A , V ) is obtained by restricting FN to W output valuation V O such that MO , (I, G, ō) |= op

iff.

ōp = 1,

where the propositional variable op represents p’s binary decision. Intuitively, the output model abstracts only the final decisions relevant for task specifications.

Knight, Lehnherr, Rajsbaum

0:11

Characteristic formulas. Given a world w := (I, G, x) of the execution model I[A], it is a standard result that there exists a non probabilistic formula ψw ∈ L that is exactly true in w and nowhere else [3, 21]. This formula is called the characteristic formula of w. Such formulas exist because the sets W A and Prop are finite1 , and every two worlds can be distinguished by at least one process2 . Given a decision function δ, we can use characteristic formulas to describe the sets of p worlds, where a process decides 1. The formula ψI,G describes this set conditioned on the p adversarial choice of I and G. If ¬ψI,G is true in a world (I, G, x), then process p decides 0. Dis We use the characteristic formula ψI,G to encode the worlds where the adversary’s choice of p q I and G was successful, i.e., there exist processes p and q such that ψI,G ∧ ¬ψI,G is true. Since all our logical models are i) based on a measurable operational model, and ii) only condition the operational measure based on equivalence classes, we can relate the probability of a process deciding 1 in the output model MO to the probability of deciding 1 in the operational model: MO , (I, G, o) |= P≤s op

iff.

p I[A] |= P≤s ψI,G

iff.

PrI,G [p decides 1] ≤ s

The middle statement is true in all worlds because if a world w′ belongs to a different p adversarial equivalence class, e.g. w′ ∈ / [(I, G, ·)]A , then ψI,G is false in every world of [w′ ]A , and therefore has probability 0. Task solvability. For deterministic tasks, there is one input model and one output model. However, for randomized tasks, there exists one set of feasible output worlds, but infinitely many output models that satisfy probabilistic properties. Since characteristic formulas exist, the properties of a task T can be expressed as logical formulas, called T -formulas. Given an execution model I[A], we say that the decision function δ solves a task T if and only if every world of the model MO induced by δ satisfies the T -formulas. More formally, for any T -formula τ , it holds that MO |= τ . Figure 3 illustrates task solvability. ▶ Remark 7. For deterministic tasks, the presented notion of task solvability is closely related to the one introduced in [11]. While the underlying logical frameworks differ, we conjecture the notions are equivalent, because I[T ] fully characterizes MO in the deterministic setting.

4

Applications

Section 2 introduced a probabilistic epistemic framework for randomized distributed computation by relating executions, knowledge, and probabilistic outputs. We now apply this framework to randomized coordinated attack. First, we show that the information levels introduced by Varghese and Lynch correspond exactly to finite levels of iterated knowledge. We then use the same epistemic structure to explain the lower bound: decision probabilities can only change gradually between indistinguishable executions, and executions with no communication and full communication are connected by such indistinguishability chains.

4.1

Information levels

Given a probabilistic execution α := (I, G, x), we informally define the information level of a process p inductively: 1 2

Recall that inputs are binary, random variables have finite support, and the number of rounds is fixed. This is because any two communication graphs can be distinguished by at least one process. The literature refers to this property also as proper [22, 23]

0:12

An Epistemic Analysis of Random Coordinated Attack

Base case: At the beginning of round 1 all processes have level 0; Induction: If p receives messages indicating that the minimum level among all processes is k, then p sets its level to k + 1. The formal definition of information levels, given in [6], can be found in the Appendix. We denote the level of process p in execution α in round r with ℓ(p, α, r). Theorem 8 relates the information level of a process at the end of the last round of a probabilistic execution α := (I, G, x) with its knowledge in the world (I, G, x) of the execution model. The expression ¬Kp E n ϕα ensures that processes have exactly level n. ▶ Theorem 8. Let I[A] be the execution model. For every α := (I, G, x) ∈ Ω, we find that ℓ(p, α, R) = n

iff.

I[A], α |= Kp E n−1 ϕα ∧ ¬Kp E n ϕα ,

where ϕα encodes the inputs in α. Proof. See Appendix.

◀

We can relate levels to the validity condition of randomized coordinated attack. Recall that validity ensures that if all messages are delivered and all processes have input 1, then they output 1. Moreover, let ψDis be the formula encoding worlds where processes decide differently. For any world w = (I, G, o), the T -formulas of randomized coordinated attack are   ^ ^ ψval :=  ip ∧ E R ϕ w  → op and ψrandA := P≤ϵ ψDis . p∈N

p∈N

By unfolding the logical operators, we get ^ E R ϕw ≡ Kp E R−1 ϕw , p∈N

and by Theorem 8, this means that all processes have at least level R − 1 at the end of the execution. Notice that this can only be true if all messages were delivered. We do not need to formulate Termination as it is guaranteed for finite rounds. Example 9 shows how we can use the previously developed machinery to fully characterize randomized coordinated attack in the communication model of Section 2. ▶ Example 9. This example shows why the T -formulas ψval and ψrandA characterize randomized coordinated attack. Let δ be a decision function solving the probabilistic coordinated attack problem. By Lemma 6, the execution model I[A] captures every execution in Ω. As explained in Section 3, the decision function δ together with the task specification produce an output model MO . Since δ solves the problem, it holds that for any choice of I and G, the probability of the adversary’s success can be at most some ϵ, which is logically captured by: MO , (I, G, o) |= P≤ϵ ψDis

iff.

Dis I[A] |= P≤ϵ ψI,G

iff.

µ({x ∈ X | (I, G, x) violates Agreement}) ≤ ϵ.

Moreover, if I is the input configuration where all processes have input 1 and G is the sequence of communication graphs where all messages are delivered, then any correct decision function must output only 1’s, because the premise of ψval is met. Therefore, for any random V value x, we find for the output model MO , (I, G, δ((I, G, x)) |= P=1 p∈N op .

Knight, Lehnherr, Rajsbaum

We now explain the intuition behind Theorem 8. Let ϕ be the formula representing the actual input configuration. We now analyze process p’s knowledge at levels 1 to 3. Level 1. Process p has level 1 if and only if it has heard of every other process. Process p has heard of process q (or r) if and only if: 1. p receives a message from the corresponding process; or 2. p receives a message from process q (or r) which has heard of r (or q) in an earlier round. Since a message contains all the inputs the sender knows about, having level 1 is equivalent to knowing all the inputs, i.e., Kp ϕ. Level 2. Process p has level 2 if and only if it knows that every other process has level 1. Epistemically, process p has level 2 if and only if it knows that q and r know all the inputs: Kp (Kq ϕ ∧ Kr ϕ) ≡ Kp E−p ϕ, where E−p means everybody except p knows. By construction of our logical model from the operational one, we have that inputs are unique and process p knows its own input. Together with Kp E−p ϕ, this implies that process p knows that all processes know ϕ, i.e., Kp Eϕ. Level 3. Process p has level 3 if and only if it knows that every other process has level 2. This is expressed as an epistemic formula below, which reduces to Kp E 2 ϕ. Kp (Kq Eϕ ∧ Kr Eϕ) ≡ Kp (Kq (Kp ϕ ∧ Kq ϕ ∧ Kr ϕ) ∧ Kr (Kq ϕ ∧ Kp ϕ ∧ Kr ϕ)). In the reduction, we use logical reasoning from S5 and use results from [6]. The details of the logical derivation can be found in the Appendix where we prove Theorem 8. Theorem 8 allows us to express the algorithm of [5] succinctly and elegantly as a knowledgebased program (see [3]), shown in Algorithm 1 . Formulated as a knowledge-based program, the algorithm becomes surprisingly simple. At the end of round R a process p decides 1 only if it knows that all processes have input 1, e.g. Kp ϕ1 , and its iterated knowledge of this fact is at least k − 1 levels deep. It can be shown that the algorithm’s correctness is restricted to the probability R−1 . Indeed, from Lynch and Varghese [5], processes decide differently if and only if one process, say p, has level exactly k, and another one, say q, has level exactly k − 1. This happens with probability R1 . Translated to our model, the following is true:   _ (Kp E k−1 ϕ1 ∧ ¬Kq E k−1 ϕ1 ) I[A] |= P= R1 xk1,1 ∧ p,q∈N

4.2

Lower bound

We now show that for any randomized coordinated attack protocol, the probability of disagreeing is at least R−1 . This bound improves the prior one of (R + 1)−1 and is tight. The key idea is that indistinguishability in the execution model I[A] limits how quickly decision probabilities can change in the output model MO . Before stating the result, we briefly recall task solvability from Section 3. Consider Figure 3 again, and assume a protocol that solves randomized coordinated attack in the operational model with decision function δ. As demonstrated in Section 2.3, the operational model induces an equivalent execution model I[A], while the task specification induces the task model I[T ], which has no probabilities. The decision function δ connects

0:13

0:14

An Epistemic Analysis of Random Coordinated Attack

Algorithm 1 A knowledge based program for the algorithm in [5] for process pi . The formula ϕ1 denotes that the inputs of all processes are 1. 1: if pi = p1 ∧ round = 1 then

k ← coinflip(k) ▷ Generation of the key k. k 3: x1,1 ← true 4: end if l l+1 5: if Kpi xk ϕ1 for some l ≥ k − 1 then 1,1 ∧ Kpi E ϕ1 ∧ ¬Kpi E 6: decide 1 7: else 8: decide 0 9: end if 2:

these two structures by assigning outputs to executions, thereby inducing the A-probabilistic output model MO . Intuitively, the output probabilities are inherited from executions. Notice, that if the protocol in the operational model did not solve the task, the induced model MO would not satisfy the task formulas. We can now state our result and sketch its proof. The main argument is based on a pq-chain, which is a sequence of executions α1 , . . . αn ∈ W A , such that A A α1 ∼A p α2 ∼q α3 . . . ∼p αn .

Intuitively, output probabilities cannot change abruptly between executions along pq-chains, which allows us to restrict them from above. As standard in indistinguishability arguments, we start with an execution α1 in which no messages are delivered, and end in an execution αn , where all messages are received. By the properties of randomized coordinated agreement, process p must decide 0 in α1 and 1 in αn , if all inputs are 1. Theorem 12 states the lower bound of R−1 for the probability of disagreement for randomized coordinated attack. It was proven in [5] that Algorithm 1 has a probability of disagreeing of at least R−1 , which makes our lower bound tight. The proof can be found in the Appendix and we will outline it subsequently. The first step towards proving Theorem 12 is to establish the standard result stated Lemma 10 for the operational model. Informally, it states that the probability of two processes deciding the value 1 can differ by at most ϵ. Intuitively, if the difference exceeds ϵ, then the processes become more likely to disagree, which violates Randomized agreement. This result is a crucial tool when reasoning about output probabilities along a pq-chain. As illustrated in Section 2.3, this result from the operational model directly translates to the epistemic output model. Corollary 11 states the result formally in the epistemic setting. ▶ Lemma 10. In the operational model, for any protocol that solves randomized coordinated attack, it holds that |PrI,G [i decides] − PrI,G [j decides 1]| ≤ ϵ. Proof. See Appendix.

◀

▶ Corollary 11. Let MO be an output model based on a decision function δ that solves randomized coordinated attack. For every process p, if MO , (I, G, o) |= P=s op , then for all q ̸= p, it holds that MO , (I, G, o) |= P≤s+ϵ oq ∧ P≥s−ϵ oq . We now motivate how probabilities can be bound from above along a pq-chain by applying Corollary 11 to bind probabilities of deciding the value 1. Let α1 := (I1 , G1 , x1 ) ∈ W A and

Knight, Lehnherr, Rajsbaum

0:15

α2 := (I2 , G2 , x2 ) ∈ W A with α1 ∼A p α2 be two probabilistic executions. By Lemma 1, equal local states preserve output probabilities, and thus it holds that: PrI1 ,G1 [p decides 1] = PrI2 ,G2 [p decides 1]. This directly translates to the output model MO . Indeed, by construction, we can relate the operational model to the output model MO , via the execution model I[A], because: MO , w |= P=s op

iff.

I[A] |= P=s ψp1

iff.

PrI,G [p decides 1] = s.

Therefore, it holds that: MO , (I, G, δ(α1 )) |= P=s op

and

MO , (I, G, δ(α2 )) |= P=s op .

Consider now the four worlds below, and assume that the probability of p and q deciding the value 1 in w0 is 0: q

w1

p

w0

w3

p

w2

q

By applying Corollary 11 we immediately obtain that process p decides the value 1 with at most ϵ in w1 . By the same reasoning, this is also true for process q in w2 . By Lemma 1, indistinguishability preserves probabilities and we get that p and q need to decide the value 1 with the same probability as in w1 and w2 respectively. Therefore, the individual probabilities of deciding the value 1 are both bound by ϵ. This is extremely helpful, because we found a pq-chain (w0 , w1 , w3 ) along which p’s probability of deciding 1 increases by at most ϵ. Using epistemic reasoning, we can construct a pq-chain with R-many such segments. In particular, the chain will end in an execution in which p decides 1 with probability 1. In the proof, we use the execution where every process has input 1 and p receives all messages. Thus, p’s probability to decide 1 needs to go from 0 to 1 in R many steps of size at most ϵ, yielding ϵ ≥ R−1 . Interestingly, this proof only considers two out of N processes, and mostly relies on epistemic indistinguishability arguments. Details are provided in the Appendix. ▶ Theorem 12. Any decision function δ solving randomized coordinated attack induces an output model MO such that for all worlds w: MO , w |= P≥ R1 ψDis . Proof. See Appendix.

◀

Our model also allows us to study randomized coordinated attack for more structured communication patterns. The iterated immediate snapshot model (IIS) is the iterated version of the communication pattern presented in Example 4. As it turns out, the proof techniques employed for Theorem 12 can also be applied here, and we obtain Theorem 13, which says that in the more restricted IIS, a lower bound on ϵ is c3−R for some constant c. The intuition is that the number of worlds in the updated model grows exponentially with a factor of 3, and the updated model for two processes forms a pq-chain (see Example 4). Algorithm 1 is still applicable in IIS, although it may no longer be optimal because the processes have access to additional information. In particular, they know that in each round at least one message is received by some process, which may reduce the number of rounds required for a decision or, by Theorem 8, relax the required knowledge.

0:16

An Epistemic Analysis of Random Coordinated Attack

▶ Theorem 13. Any decision function δ solving randomized coordinated attack in IIS induces an output model MO such that for all worlds w: MO , w |= P≥c3−R ψDis , where c ∈ R is a constant. Proof. See Appendix.

5

◀

Conclusion

In this work we developed a probabilistic epistemic framework for bounded time task solvability. Processes may flip coins to solve a task with probability of error as small as possible in a given number of rounds. We illustrated the use of the framework focusing on the randomized coordinated attack problem. Some of the benefits obtained are closing previous upper and lower bounds, as well as formalizing nested knowledge, a notion that plays an important role in agreement tasks, such as consensus and approximate agreement. We emphasize that the presented framework is general and can be used to study randomized algorithms under arbitrary communication patterns, as well as problems other than coordinated attack. We illustrated the generality with a lower bound in an immediate snapshots model of main interest in shared memory, showing that the same type of argument can be used the coordinated attack setting, as well as in other communication models. Two main research directions seem particularly interesting. First, to study (bounded) randomized solvability of other tasks. Our techniques apply directly to approximate agreement e.g. [24], which we will include in the full version. It would be interesting to study other tasks, such as set agreement [25]. It would be interesting to study also equality negation, which has been analyzed both topologically [26] and epistemically [27]. The second research direction is on the epistemic side, where many interesting problems remain open. In particular, about a sound and complete axiomatization, and the expressivity of the language. This paper is primarily focused on the formal study of randomized algorithms, however, it would be interesting to consider more general updates beyond messages and coin flips. In particular, extending the framework to probabilistic actions appears to be an important direction for future work. References 1

2 3

4

5

E. A. Akkoyunlu, K. Ekanadham, R. V. Huber, Some constraints and tradeoffs in the design of network communications, in: Proceedings of the Fifth ACM Symposium on Operating Systems Principles, SOSP ’75, Association for Computing Machinery, New York, NY, USA, 1975, pp. 67–74. doi:10.1145/800213.806523. URL https://doi.org/10.1145/800213.806523 J. Gray, Notes on data base operating systems, in: Operating Systems, An Advanced Course, Springer-Verlag, Berlin, Heidelberg, 1978, pp. 393–481. R. Fagin, J. Y. Halpern, Y. Moses, M. Y. Vardi, Reasoning About Knowledge, MIT Press, 1995. doi:10.7551/MITPRESS/5803.001.0001. URL https://doi.org/10.7551/mitpress/5803.001.0001 M. J. Fischer, N. A. Lynch, M. Paterson, Impossibility of distributed consensus with one faulty process, J. ACM 32 (2) (1985) 374–382. doi:10.1145/3149.214121. URL https://doi.org/10.1145/3149.214121 G. Varghese, N. A. Lynch, A tradeoff between safety and liveness for randomized coordinated attack, Inf. Comput. 128 (1) (1996) 57–71. doi:10.1006/INCO.1996.0063. URL https://doi.org/10.1006/inco.1996.0063

Knight, Lehnherr, Rajsbaum

6 7 8

9

10

11

12 13

14

15 16

17

18 19

20

21 22

N. A. Lynch, Distributed Algorithms, Morgan Kaufmann, 1996. J. Aspnes, Notes on theory of distributed systems, arXiv 2001.04235 (2025). arXiv:2001.04235. URL https://arxiv.org/abs/2001.04235 M. Herlihy, N. Shavit, The asynchronous computability theorem for t-resilient tasks, in: S. R. Kosaraju, D. S. Johnson, A. Aggarwal (Eds.), Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, May 16-18, 1993, San Diego, CA, USA, ACM, 1993, pp. 111–120. doi:10.1145/167088.167125. URL https://doi.org/10.1145/167088.167125 B. Alpern, F. B. Schneider, Defining liveness, Inf. Process. Lett. 21 (4) (1985) 181–185. doi:10.1016/0020-0190(85)90056-0. URL https://doi.org/10.1016/0020-0190(85)90056-0 R. Fagin, J. Y. Halpern, M. Y. Vardi, What can machines know? on the properties of knowledge in distributed systems, J. ACM 39 (2) (1992) 328–376. doi:10.1145/128749.150945. URL https://doi.org/10.1145/128749.150945 É. Goubault, J. Ledent, S. Rajsbaum, A simplicial complex model for dynamic epistemic logic to study distributed task computability, Inf. Comput. 278 (2021) 104597. doi:10.1016/J.IC. 2020.104597. URL https://doi.org/10.1016/j.ic.2020.104597 H. van Ditmarsch, W. van der Hoek, B. Kooi, Dynamic Epistemic Logic, Springer, Dordrecht, Netherland, 2007. A. Castañeda, H. van Ditmarsch, D. A. Rosenblueth, D. A. Velázquez, Pattern models: A dynamic epistemic logic for distributed systems, Comput. J. 67 (7) (2024) 2421–2440. doi:10.1093/COMJNL/BXAE016. URL https://doi.org/10.1093/comjnl/bxae016 P. Fraigniaud, B. Patt-Shamir, S. Rajsbaum, Coordination through stochastic channels, in: D. R. Kowalski (Ed.), 39th International Symposium on Distributed Computing, DISC 2025, Berlin, Germany, October 27-31, 2025, LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, pp. 32:1–32:19. doi:10.4230/LIPICS.DISC.2025.32. URL https://doi.org/10.4230/LIPIcs.DISC.2025.32 H. Attiya, J. Welch, Distributed Computing: Fundamentals, Simulations and Advanced Topics, John Wiley & Sons, Hoboken, NJ, USA, 2004. B. P. Kooi, Probabilistic dynamic epistemic logic, Journal of Logic, Language and Information 12 (4) (2003) 381–408. doi:10.1023/A:1025050800836. URL https://doi.org/10.1023/A:1025050800836 R. Fagin, J. Y. Halpern, Reasoning about knowledge and probability, J. ACM 41 (2) (1994) 340–367. doi:10.1145/174652.174658. URL https://doi.org/10.1145/174652.174658 J. Y. Halpern, Reasoning About Uncertainty, MIT Press, 2003. K. Winkler, A. Paz, H. R. Galeana, S. Schmid, U. Schmid, The time complexity of consensus under oblivious message adversaries, Algorithmica 86 (6) (2024) 1830–1861. doi:10.1007/ S00453-024-01209-4. URL https://doi.org/10.1007/s00453-024-01209-4 J. van Benthem, J. Gerbrandy, B. Kooi, Dynamic update with probabilities, Studia Logica 93 (1) (2009) 67–96. doi:10.1007/s11225-009-9209-y. URL https://doi.org/10.1007/s11225-009-9209-y K. J. J. Hintikka, Knowledge and Belief: An Introduction to the Logic of the Two Notions, Cornell University Press, Ithaca, NY, USA, 1962. É. Goubault, J. Ledent, S. Rajsbaum, A simplicial model for kb4_n: Epistemic logic with agents that may die, in: P. Berenbrink, B. Monmege (Eds.), 39th International Symposium on Theoretical Aspects of Computer Science, STACS 2022, Marseille, France (Virtual Conference), March 15-18, 2022, LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, pp.

0:17

0:18

An Epistemic Analysis of Random Coordinated Attack

33:1–33:20. doi:10.4230/LIPICS.STACS.2022.33. URL https://doi.org/10.4230/LIPIcs.STACS.2022.33 H. van Ditmarsch, E. Goubault, J. Ledent, S. Rajsbaum, Knowledge and simplicial complexes, CoRR abs/2002.08863 (2020). arXiv:2002.08863. URL https://arxiv.org/abs/2002.08863 M. Függer, T. Nowak, M. Schwarz, Tight bounds for asymptotic and approximate consensus, J. ACM 68 (6) (2021) 46:1–46:35. doi:10.1145/3485242. URL https://doi.org/10.1145/3485242 S. Chaudhuri, Agreement is harder than consensus: Set consensus problems in totally asynchronous systems, in: C. Dwork (Ed.), Proceedings of the Ninth Annual ACM Symposium on Principles of Distributed Computing, Quebec City, Quebec, Canada, August 22-24, 1990, ACM, 1990, pp. 311–324. doi:10.1145/93385.93431. URL https://doi.org/10.1145/93385.93431 É. Goubault, M. Lazic, J. Ledent, S. Rajsbaum, Wait-free solvability of equality negation tasks, in: J. Suomela (Ed.), 33rd International Symposium on Distributed Computing, DISC 2019, Budapest, Hungary, October 14-18, 2019, LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019, pp. 21:1–21:16. doi:10.4230/LIPICS.DISC.2019.21. URL https://doi.org/10.4230/LIPIcs.DISC.2019.21 H. van Ditmarsch, É. Goubault, M. Lazic, J. Ledent, S. Rajsbaum, A dynamic epistemic logic analysis of equality negation and other epistemic covering tasks, J. Log. Algebraic Methods Program. 121 (2021) 100662. doi:10.1016/J.JLAMP.2021.100662. URL https://doi.org/10.1016/j.jlamp.2021.100662 L. Lamport, Time, clocks, and the ordering of events in a distributed system, Commun. ACM 21 (7) (1978) 558–565. doi:10.1145/359545.359563. URL https://doi.org/10.1145/359545.359563

23

24

25

26

27

28

A

The system S5

The system S5 consists of the axioms all propositional tautologies

(Taut)

Kp (ϕ → ψ) → (Kp ϕ → Kp ψ)

(K)

Kp ϕ → ϕ

(T)

Kp ϕ → Kp Kp ϕ

(4)

⟨Kp ⟩ϕ → Kp ⟨Kp ⟩ϕ

(5)

as well as the inference rules modus ponens MP and Kp -necessitation Kp -Nec: A

B

A→B B

(MP)

A Kp A

(Kp -Nec)

Information levels

We repeat the definition of the information level from [6]. At the end of round r in execution α, process p is in state sp (α, r) and first computes its “local” happens-before relation [28] after receiving the messages of that round. Intuitively, the relation describes which information the process has at the end of round r.

Knight, Lehnherr, Rajsbaum

▶ Definition 14 (Local happens-before relation). Let α = (I, G, x) be an execution. At the end of round r, process p is in state (ip , x̄p|r , recp (G, r)), and computes the local happens-before relation ≤p on the domain N × [r]. We define ≤p as the smallest relation satisfying: 1. Local progression: if r < r′ , then (p, r) ≤p (p, r′ ); 2. Message causality: if p receives mq,r , then (q, r − 1) ≤p (p, r); 3. Transitivity: if (q, r) ≤p (s, r′ ) and (s, r′ ) ≤p (l, r′′ ), then (q, r) ≤p (l, r′′ ). ▶ Remark 15. In contrast to the Definition of ≤p in [6], we have shifted round indices by 1. After computing the local happens-before relation, process p performs the level algorithm (Definition 16). Intuitively, the level algorithm captures a process’s knowledge about what other processes know, and iteratively, what they know about others’ knowledge. Notice that in a full-information protocol, process p can recompute process q’s level at the end of round r − 1 locally if it received a message from process q at the end of round r. ▶ Definition 16 (Level algorithm [6]). Using the happens-before relation ≤p computed in the current round r (Definition 14), process p locally computes its level ℓ(p, α, r): 1. Initialization: the level of every process is initialized to 0; 2. Base case: if there is some q ̸= p such that (q, 1) ̸≤p (p, r), then ℓ(p, α, r) = 0; 3. Induction: if (q, 1) ≤p (p, r) for all q ̸= p, then define for each q: fq := max{ℓ(q, α, r′ ) | (q, r′ ) ≤p (p, r)}, which is non-empty due to (q, 1) ≤p (p, r) for all q ̸= p. Next, set: ℓ(p, α, r) = min{fq | q ̸= p} + 1. ▶ Remark 17. Since G can be arbitrary, the level algorithm applies to any full-information protocol with perfect recall, regardless of the underlying network topology. Intuitively, if a process has level n, it knows that all other processes have at least level n − 1, and that there exists at least one process with exactly level n − 1. In particular, if a process has level 1, it knows the inputs of all other processes.

C

Proofs for Section 4

This section presents the proofs of Theorem 8, Lemma 10, and Theorem 12.

Theorem 8 Proof. We show both directions separately via induction on n, starting from left to right. That is, we show that ℓ(p, α, R) = n implies I[A], α |= Kp E n−1 ϕα ∧ ¬Kp E n ϕα . In words, if p has level n at the end of execution α, then its nested knowledge of the inputs (represented by ϕα ) is n − 1 deep. In what follows we assume that α := (I, G, x).

0:19

0:20

An Epistemic Analysis of Random Coordinated Attack

Base case. Let ℓ(p, α, R) = 1, we need to show that I[A], (I, G, x) |= Kp ϕα ∧ ¬Kp Eϕα . We show both sides of the conjunction separately, starting with Kp ϕα . By assumption, process p has received information that every other process’s level is 0. By the definition of the operational model in Section 2.1, process p’s local state s(p, α, R) contains all inputs. Since there is a one-to-one correspondence between the operational model and the worlds of the execution model I[A] (see Lemma 6), the valuation V A assigns the same propositional input variables to each world (I ′ , G′ , x′ ) that is indistinguishable ′ ′ ′ ′ ′ ′ from, i.e., (I, G, x) ∼A p (I , G , x ). Therefore, it holds that I[A], (I , G , x ) |= ϕα , and by the definition of truth (see Definition 3), we obtain I[A], (I, G, x) |= Kp ϕα . The argument, that this is process p’s maximal nested knowledge about the inputs, i.e. I[A], α |= ¬Kp Eϕα relies on the same arguments. If process p has exactly level 1, then there exits a process, say q, for which p considers it possible that it only has level 0. In the execution model I[A], this corresponds to p not being able to distinguish α from an execution α′ with I[A], α′ |= ¬Kq ϕα . By Definition 3, it holds that I[A], (I, G, x) |= ¬Kp Eϕα . Inductive step. Let ℓ(p, α, R) = n + 1. We need to show that I[A], (I, G, x) |= Kp E n ϕα ∧ ¬Kp E n+1 ϕα . Again, we show both sides of the conjunction separately, starting with Kp E n ϕα . By assumption process p has received information that every other process’s level is n. By applying the induction hypothesis, we find that I[A], (I, G, x) |= Kp E−p E n−1 ϕα ,

(1)

where E−p is short for everybody except p. A standard formula valid in S5 for arbitrary ψ ∈ L and k ∈ N is3 Kp Kq E k ψ → Kp E k ψ. By setting ψ = ϕα , we obtain that I[A], (I, G, x) |= Kp E n−1 ϕα . Indeed, since for the non-trivial cases of the problem it holds that n > 1, and thus N \ {p} ̸= ∅, we have that ^ E−p ϕα ≡ K q ϕα a∈N \{p}

implies that there exists another process q with I[A], (I, G, x) |= Kp Kq E n−1 ϕα . By axiom 4 (transitivity), we obtain that I[A], (I, G, x) |= Kp Kp E n−1 ϕα . Combined with Equation (1), this implies I[A], (I, G, x) |= Kp Kp E n−1 ϕα ∧ Kp E−p E n−1 ϕα ⇐⇒ I[A], (I, G, x) |= Kp (Kp E

n−1

ϕα ∧ E−p E

n−1

ϕα ) ⇐⇒

I[A], (I, G, x) |= Kp (Kp E n−1 ϕα ∧

^

Kq E n−1 ϕα )

q∈N \{p}

⇐⇒ n

I[A], (I, G, x) |= Kp E ϕα , 3

This formula can be derived in the same way for ψ ∈ LP .

Knight, Lehnherr, Rajsbaum

as desired. The argument for showing that this is the maximal nested knowledge is the same as for the base case. We proceed by showing the claim from right to left. That is, we show that I[A], α |= Kp E n−1 ϕα ∧ ¬Kp E n ϕα implies ℓ(p, α, R) = n. Base case. Assume I[A], (I, G, x) |= Kp ϕα ∧ ¬Kp Eϕα , we need to show that ℓ(p, α, R) = 1. ′ ′ ′ ′ ′ ′ By Definition 3, it holds that (I, G, x) ∼A p (I , G , x ) implies I[A], (I , G , x ) |= ϕα . By the one-to-one correspondence in Lemma 6, it must hold that that for all executions α′ such that s(p, α′ , R) = s(p, α, R), we have I ′ = I. However, this can only occur in the relational model if and only if process p has heard that all other process have at least level 0. By similar reasoning as before, ¬Kp E n ϕα ensures that p’s level is exactly 1. Inductive step. For the inductive step, we prove the contraposition, i.e., ℓ(p, α, R) ̸= 1 implies I[A], (I, G, x) |= ¬Kp E n−1 ϕα ∨ Kp E n ϕα . Assume that ℓ(p, α, R) < n. The other case follows immediately because E k+1 ψ → E k ψ is a standard consequence of axiom T (Kp ψ → ψ). In particular, we will show that I[A], (I, G, x) |= ¬Kp E n−1 ϕα . Since ℓ(p, α, R) < n , there exists a process q from which p has heard of at most level n − 2. Let t be the round in which p has heard of q last, i.e., t is the maximal round for which (q, t) ≤p (p, R). Since there are finitely many rounds, the round t exists. Let G′ be the sequence of communication graphs in which all messages to q after t are dropped. Let α′ = (I, G′ , x). By construction, it holds that inp (G) = inp (G′ ), and thus (I, G, x) ∼p (I, G′ , x). Moreover, since ℓ(q, α′ , R) < n − 1 is true by assumption, the inductive hypothesis applies, by which it must hold that I[A], (I, G′ , x) |= ¬Kq E n−2 ϕ, from which we conclude that p must consider it possible in (I, G, x) that q’s level is n − 2, i.e., I[A], (I, G, x) |= ¬Kp E n−1 ϕα . ◀

Lemma 10 Proof. We define the events A := {(I, G, ·) ∈ Ω | δ(si ((I, G, ·), R)) = 1)}; B := {(I, G, ·) ∈ Ω | δ(sj ((I, G, ·), R)) = 1)}; D := {(I, G, ·) ∈ Ω | δ(si ((I, G, ·), R)) ̸= δ(sj ((I, G, ·), R))}. Then PrI,G [i decides 1] = PrI,G [A]; PrI,G [j decides 1] = PrI,G [B]; PrI,G [i and j disagree ] = PrI,G [D]. Observe that A∆B ⊆ D, where A∆B is the symmetric difference (A \ B) ∪ (B \ A). A standard property of probability measures is: |PrI,G [A] − PrI,G [B]| ≤ PrI,G [A∆B]. By monotonicity (A∆B ⊆ D) and our assumption, we obtain that PrI,G [A∆B] ≤ PrI,G [D] and PrI,G [D] ≤ ϵ, which yields the claim. ◀

0:21

0:22

An Epistemic Analysis of Random Coordinated Attack

Theorem 12 Proof. We construct an explicit pq-chain. The worlds of our interest are associated to three different types of strategies (sequences of communication graphs) that the adversary can choose: 1. Bi with 0 ≤ i ≤ R represents the strategy in which all messages up to round i are received by everyone, and all later messages are dropped. 2. Ai with 0 ≤ i ≤ R − 1 represents the strategy in which only process p does not receive any messages from round i on. Before round i process p received all messages. 3. Ci with 0 ≤ i ≤ R − 1 represents the strategy in which only process q does not receive any messages from round i on. Before round i process q received all messages. Since inputs are fixed to be 1 throughout our construction, we identify worlds of I[A] by those sets only. Consider now the below excerpt of the execution model I[A]. Reflexive and transitive arrows are omitted for simplicity. It holds that A Bi ∼A p Ai and Bi ∼q Ci , for all 0 ≤ i ≤ R,

(2)

as well as A Bj ∼A q Aj−1 and Bj ∼p Cj−1 , for all 1 ≤ j ≤ R. A0

A1

p

...

p

B0

...

q

...

p q

C1

Ct−1

BR

p

p

q

...

AR−1

q

Bt

p q

... p

q

B2

p

C0

At p

q

B1 q

At−1

p

q

(3)

q

Ct

...

CR−1

A pq-chain from A0 , a global state in which process p decides the value 1 with probability 0, to AR−1 , a global state in which process p decides the value 1 with probability 1, is given by: A A A A A0 ∼ A q B1 ∼p A1 ∼q B2 ∼p · · · ∼p AR−1 .

Since p (q) decides 1 in A0 (B0 ) with probability 0, the probability of both individually deciding 1 is at most ϵ in B1 . This naturally generalizes to Ai , Ci , and Bi+1 . That is, for A each segment Ai ∼A q Bi+1 ∼p Ai+1 , the probability of p deciding 1 is at most (i + 1)ϵ. Thus, when in AR−1 , the probability is at most Rϵ. By the task specification, the probability of p deciding 1 in AR−1 is 1, and therefore, it must hold that Rϵ ≥ 1. Rearranging the terms yields ϵ ≥ R−1 . Therefore MO , w |= P≥R−1 ψDis for all worlds of the output model. ◀

Theorem 13 Proof. Throughout this proof, all processes have input 1. We employ the same technique as in the proof of Theorem 12. Our goal is to find a pq-chain from a world in which a process p decides the value 1 with probability 0 to another world in which it decides 1 with probability 1. The probability of a process p deciding 1 along the chain can be bounded by using similar arguments as in Theorem 12, which yields a lower bound ϵ ≥ L1 , where L is the length of the pq-chain of interest. It is a standard result that the worlds in IIS increase exponentially by a factor of 3 in each round [13]. Hence, when fixing two processes p and q, the updated model for round R naturally contains a pq-chain with 3R many worlds. By fixing the inputs of the other processes and assuming that they receive all messages, we can concentrate on this line (see Example 4).

Knight, Lehnherr, Rajsbaum

0:23

The worlds at the endpoints of that line (see Figure 1) are the worlds where process p, respectively q, received no messages throughout all rounds. The world in the middle w∗ (i.e. at position n+1 2 ) is the world where both processes receive every message in all rounds. As in the proof of Theorem 12, we are interested in the first world in which a process decides 1 with probability 1. In Theorem 12, that world was AR−1 . Here, it is the world where the process p (or q) received all messages and process q (or p) received all except the last message. Since the updated model for R rounds is a line, the path from the leftmost world to that world is of length Θ(3R ). Notice that it is difficult to determine the exact length, as it changes with the parity of R. Along each transition, the probability of process p deciding 1 can increase by at most 2ϵ by Lemma 10. Indeed, if we have the segment w1 ∼A q w2 , then: 1. p’s probability of deciding 1 in w2 can be at most ϵ larger than q’s probability in w1 ; and 2. p’s probability of deciding 1 in w1 can be at most ϵ less than q’s probability in w1 . Thus, p’s probability can increase by at most 2ϵ along q transitions, and stays the same along p-transitions by Lemma 1. Because there are also Θ(3R ) many q-transitions, the lower bound is therefore given, for some constant c ∈ R: ϵ ≥ c3−R , by the same reasoning as in Theorem 12. ◀