Nathalie Bertrand
email: nathalie.bertrand@inria.fr

Marijana Lazić
email: lazic@in.tum.de

Josef Widder

A Reduction Theorem for Randomized Distributed Algorithms under Weak Adversaries

Weak adversaries are a way to model the uncertainty due to asynchrony in randomized distributed algorithms. They are a standard notion in correctness proofs for distributed algorithms, and express the property that the adversary (scheduler), which has to decide which messages to deliver to which process, has no means of inferring the outcome of random choices, and the content of the messages. In this paper, we introduce a model for randomized distributed algorithms that allows us to formalize the notion of weak adversaries. It applies to randomized distributed algorithms that proceed in rounds and are tolerant to process failures. For this wide class of algorithms, we prove that for verification purposes, the class of weak adversaries can be restricted to simple ones, so-called round-rigid adversaries, that keep the processes tightly synchronized. As recently a verification method for round-rigid adversaries has been introduced, our new reduction theorem paves the way to the parameterized verification of randomized distributed algorithms under the more realistic weak adversaries.

Introduction

Automated verification of fault-tolerant distributed algorithms faces the combinatorial explosion problem. The asynchronous parallel composition of many processes leads to a huge number of executions. Recently, several verification methods [START_REF] Gleissenthall | Pretend synchrony[END_REF][START_REF] Kragl | Synchronizing the asynchronous[END_REF][START_REF] Bouajjani | On the completeness of verifying message passing programs under bounded asynchrony[END_REF][START_REF] Damian | Communication-closed asynchronous protocols[END_REF][START_REF] Bertrand | Verification of randomized consensus algorithms under round-rigid adversaries[END_REF] are based on the idea that for many distributed algorithms, instead of considering all these asynchronous executions, it is sufficient to consider only fewer (representative) synchronous executions. The central argument is similar to the reductions (also know as, mover analysis) by Lipton [START_REF] Lipton | Reduction: A method of proving properties of parallel programs[END_REF] and Elrad and Francez [START_REF] Elrad | Decomposition of distributed programs into communication-closed layers[END_REF]: given an arbitrary execution, by repeatedly swapping neighboring transitions, one arrives at one of the representative (synchronous) executions. As this argument works on executions (traces), it works for reachability properties, and for specific stuttering-insensitive linear temporal properties.

In this paper, we extend this idea to randomized distributed algorithms and probabilistic properties [START_REF] Ben-Or | Another advantage of free choice: Completely asynchronous agreement protocols (extended abstract)[END_REF][START_REF] Mostéfaoui | Randomized k-set agreement in crash-prone and Byzantine asynchronous systems[END_REF][START_REF] Aspnes | Randomized protocols for asynchronous consensus[END_REF]. Rather than arguing on traces, probabilistic guarantees require us to reason on Markov decision processes (MDPs). In MDPs the non-determinism is resolved by using adversaries, that is, by functions that map an execution prefix to the next action taken. In case the next action is a coin toss, we obtain a branching, where each branch is associated with a probability. As a result, an MDP together with an adversary induce a computation tree with probabilistic branching. As the adversary is a function on the prefix, it is not clear whether in the presence of this branching, it is possible to conduct a swapping argument on the computation tree that maintains probabilistic properties. The technical challenge we face is to characterize a family of adversaries that permits a swapping argument in order to arrive at a computation tree that corresponds to a synchronous execution. Restricting to synchronous executions considerably decreases the verification effort, by reducing the number of executions to check. For the analysis of distributed consensus algorithms, there are two well-researched classes of adversaries, namely strong and weak adversaries. Strong adversaries have full knowledge of the execution prefix, while weak adversaries are based on a projection (abstraction) of the execution prefix, in particular, they do not have access to the content of the exchanged messages and the outcomes of coin tosses. In this paper, we formalize weak adversaries, and make explicit that they inherently impose restrictions on the local code of a distributed algorithm, that is, they can only be defined for a class of distributed algorithms (which was not apparent from their mathematical definition in the literature).

Intuitively, these algorithms expose some form of symmetry regarding the local control flow. Consider a formalization of Ben-Or's consensus algorithm [START_REF] Ben-Or | Another advantage of free choice: Completely asynchronous agreement protocols (extended abstract)[END_REF] in Figure 1. The subscript in the locations (nodes) encode the local estimate of the consensus value, for instance D 0 and D 1 are locations where processes decide 0 and 1, respectively. We observe that the control flows on the 0 side and the 1 side are symmetric: if we ignore the subscripts the paths through the graph are identical. In contrast, consider the (made-up) example in Figure 2. If at location J there would be a branching due to receiving messages with different consensus estimates, the two paths that lead to F differ in length. An adversary may observe whether a process has taken the left path or the right path which allows the adversary to infer knowledge on the consensus value that led to branching at location J. However, typical randomized consensus algorithms from the literature [START_REF] Ben-Or | Another advantage of free choice: Completely asynchronous agreement protocols (extended abstract)[END_REF][START_REF] Bracha | Asynchronous Byzantine agreement protocols[END_REF][START_REF] Mostéfaoui | Randomized k-set agreement in crash-prone and Byzantine asynchronous systems[END_REF][START_REF] Jiun | Bosco: One-step Byzantine asynchronous consensus[END_REF] have a structure similar to Figure 1. Almost sure termination of these algorithms have been automatically verified in [START_REF] Bertrand | Verification of randomized consensus algorithms under round-rigid adversaries[END_REF] under synchronous executions formalized via round-rigid adversaries. In this paper we show that for these distributed algorithms the computation trees that are defined by weak adversaries can be reduced to round-rigid computation trees by a swapping argument. As a result we show that the verification results from [START_REF] Bertrand | Verification of randomized consensus algorithms under round-rigid adversaries[END_REF] apply to a wider class of adversaries than originally claimed.

More formally, our new reduction theorem says that for each weak adversary there exists a round-rigid adversary that maintains the original probabilities of properties. For strong adversaries, we were not able to derive such a reduction argument, which indicates that the verification problem for strong adversaries is harder. This would also explain why the mathematical proofs in the literature for strong adversaries are considerably more involved [START_REF] Aguilera | The correctness proof of Ben-Or's randomized consensus algorithm[END_REF].

Contributions. We present in Section 2 a new formalization of randomized distributed algorithms that allows us to define the weak adversary model from the literature [START_REF] Aspnes | Randomized protocols for asynchronous consensus[END_REF]. Our model is based on threshold automata [START_REF] Konnov | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms[END_REF] and their probabilistic extension [START_REF] Bertrand | Verification of randomized consensus algorithms under round-rigid adversaries[END_REF]. To faithfully express the weak adversaries, we introduce a process-based semantics, i.e., rather than the counter system semantics from [START_REF] Konnov | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms[END_REF][START_REF] Bertrand | Verification of randomized consensus algorithms under round-rigid adversaries[END_REF], we propose semantics based on processes that exchange messages. We then prove our reduction in two steps. First, in Section 3, we reduce adversaries to communication-closed [START_REF] Elrad | Decomposition of distributed programs into communication-closed layers[END_REF] adversaries, that is, adversaries that to a process in round r only deliver messages of round r ≤ r. Then, in Section 4, we reduce weak communication-closed adversaries to round-rigid adversaries.

Modeling Randomized Threshold-based Algorithms

Probabilistic threshold automata with semantics based on counter systems were introduced in [START_REF] Bertrand | Verification of randomized consensus algorithms under round-rigid adversaries[END_REF]. For a discussion on the operation of threshold-based distributed algorithms, and how they are captured by threshold automata we refer to [START_REF] Bertrand | Verification of randomized consensus algorithms under round-rigid adversaries[END_REF].

Here we provide more concrete semantics based on processes and message buffers (modeled as sets). A probabilistic threshold automaton with processes, PTA P , is a tuple (L, Z, R, RC ), where -L is a non-empty finite set of locations that contains the disjoint subsets: initial locations I, final locations F, and border locations B, with |B| = |I|. -Z is a disjoint union of the following five sets:

• Π is a set of parameter variables;

• P = {p 1 , . . . , p n }, for some n ≥ 1, is a finite set of processes; It is the disjoint union of C and F, representing sets of correct and faulty processes, respectively;

• T is a finite set of types of messages • V is a finite set of values of messages, typically V = {0, 1}; • Λ ⊆ {x t,v | t ∈ T , v ∈ V} is a set of local receive variables;
-R is a finite set of rules; and -RC , the resilience condition, is a constraint over parameter variables.

Rule Guard

Update

r1 true ∅ r2 true ∅ r3 true {x0} r4 true {x1} r5 x0+x1 ≥ n-t ∧ x0 ≥ (n+t)/2 {y0} r6 x0+x1 ≥ n-t ∧ x1 ≥ (n+t)/2 {y1} r7 x0+x1 ≥ n-t ∧ x0 < (n+t)/2 ∧ x1 < (n+t)/2 {y?} Rule Guard Update r8 y0+y1+y? ≥ n-t ∧ y0 ≥ t+1 ∅ r9 y0+y1+y? ≥ n-t ∧ y0 > (n+t)/2 ∅ r10 y0+y1+y? ≥ n-t ∧ y0 < t+1 ∧ y1 < t+1 ∅ r11 y0+y1+y? ≥ n-t ∧ y1 > (n+t)/2 ∅ r12 y0+y1+y? ≥ n-t ∧ y1 ≥ t+1 ∅ r13 true ∅ r14 true ∅ Table 1.
The rules of the probabilistic threshold automaton for Ben-Or's algorithm from Figure 1, where zi ∈ {x0, x1, y0, y1, y ? } refers to messages of type z and value i.

{E 0 , E 1 , D 0 , D 1 , CT 0 , CT 1 } are final locations. The set of parameters is Π = {n, t, f }, where n is the total set of processes, f is the number of faulty processes, and t is an upper bound on the number of faults. The 14 rules of the PTA P from Figure 1 are given in Table 1 (and detailed later). There are two message types, T = {x, y}, and three values V = {0, 1, ?}, where x-messages can only have values 0 and 1, and y-messages all three values. The local receive variables from Λ are thus written x 0 , x 1 , y 0 , y 1 , y ? where we write shortly, e.g., type-value pair (x, 0). See [START_REF] Bertrand | Verification of randomized consensus algorithms under round-rigid adversaries[END_REF] for an in-detail exposition of Ben-Or's algorithm and its formalization as threshold automaton. There, one can observe that the pseudo-code of this algorithm consists of a while loop, and one loop iteration is refered to as a round. In the threshold automaton in Figure 1, the solid arrows represent local transitions within a round, while dashed arrows represent local transitions to the next round. In each round, each process starts in I 0 or I 1 . The subscript of the locations show what is the process' current estimate of the consensus value. A process informs its peers about its consensus estimate by firing rule r 3 or r 4 and sending a message of type x 0 or x 1 , respectively. Then it waits in SR until sufficiently many -given by the guards -messages are received to fire r 5 , r 6 , and r 7 , etc. If the thresholds are chosen properly, this shall ensure that if a process enters D 0 in some round, and thus decides 0, no process ever enters D 1 in some round and decided 1 (agreement of consensus). The randomization is introduced in rule r 10 : this is a coin toss where a process chooses its estimate for the next round if there was no clear majority around a value. The dashed arrows then show how a process transitions from a final location of round r to the beginning of round r + 1. Performing an infinite number of rounds, and (if necessary) coin tosses, shall ensure that eventually every process decides.

Resilience condition. Let N 0 denote the set of natural numbers including zero. A resilience condition RC defines the set of admissible parameter values P RC = {p ∈ N |Π| 0 : p |= RC }, for which the algorithm is designed to be correct. For example, Ben-Or's consensus algorithm is correct when n/5 > t ≥ f ≥ 0. We introduce a function N : P RC → N 0 that maps a vector of admissible parameters to a number of modeled processes in the system. For instance, for the automaton in Figure 1, N is the function (n, t, f ) → n-f , as we model only the n-f correct processes explicitly, while the effect of Byzantine faulty processes is captured in non-deterministic choices between different guards. For crash-resilient algorithms, where all processes are initially correct (until they crash), we model them all explicitly, that is, N (n, t, f ) = n. The set of modeled processes is then

C = {p 1 , . . . , p N }.
Messages. The set of all messages is M = (P×T ×V ×N 0 ). A message m is a tuple (sen, type, val , rnd ) where the process sen ∈ P is the sender, the message type is type ∈ T , the value is val ∈ V, and the message is sent in the round rnd ∈ N 0 . Note that we do not make explicit the process receiving the message, because we focus on broadcast communications, and thus messages are sent to every process.

Let M F = F × T × V × N 0 be the subset of all messages where the sender is a faulty process, and M C = C × T × V × N 0 the subset of messages sent by correct processes. In our example from Figure 1 we have |F| = f and |C| = n -f .

In the sequel, we assume M is equipped with a total order < M . This total order can be naturally derived from the order on N 0 , and fixed orders on the processes, on the types, and on the values.

Rules. We introduce rules in detail, and give syntactic restrictions that model the local transitions of a distributed algorithm from/to particular locations. A rule r is a tuple (from, δ to , ϕ, u) where from ∈ L is the source location, δ to ∈ Dist(L) is a probability distribution over the destination locations, u ⊆ T × V is the update set, and ϕ is a guard, i.e., a conjunction of expressions of the form

v∈V (b v • x t,v ) ā • p + a 0 where t ∈ T is a fixed message type; for a message value v ∈ V, b v ∈ N 0 is a non-negative integer and x t,v ∈ Λ is a local receive variable; ∈ {≥, <}, ā ∈ Z |Π|
is a vector of integers, a 0 ∈ Z, and p is the vector of all parameters. If a guard contains only one conjunct, we sometimes call it a simple threshold guard (or just a simple guard ). The set of all simple guards that appear in a probabilistic threshold automaton PTA P is denoted by G(PTA P ).

If r.δ to is a Dirac distribution, i.e., if there exists ∈ L such that r.δ to ( ) = 1, we call r a Dirac rule, and simply denote it (from, , ϕ, u).

Probabilistic threshold automata model algorithms with multiple rounds that follow the same code. They represent the behaviour each correct process follows within a round. Informally, a round happens between border locations and final locations. The round switch rules let processes move from final locations of a given round to border locations of the next round. From each border location there is exactly one Dirac rule to an initial location, and it has a form ( , , true, ∅) where ∈ B and ∈ I. As |B| = |I|, one can think of border locations as copies of initial locations. It remains to model from which final locations to which border location (that is, initial for the next round) processes move. This is done by round switch rules. They can be described as Dirac rules ( , , true, ∅) with ∈ F and ∈ B. The set of round switch rules is denoted by S ⊆ R. A location belongs to B iff all the incoming edges are in S. Similarly, a location is in F iff there is only one outgoing edge and it is in S.

Example 2. Back to our running example, the only rule that is not a Dirac rule is r 10 , and round switch rules are represented by dashed arrows. Also the update sets are either empty sets or singletons, where we again write shortly, e.g., x 0 instead of the type-value pair (x, 0).

Symmetry in PTA P

In the distributed algorithm community, weak adversaries are typically defined by not being able to observe message content and the outcome of coin tosses. In the PTA P model, one can often retrieve information about the outcome of a coin toss by the location a process ends up in, or about the message contents by the rule that is taken. For instance, in our example, depending on the outcome of a coin toss, a process goes either to location CT 0 or CT 1 . Also, firing r 5 or r 6 reveals which messages of type x-with value 0 or 1-are in the majority. This motivates the introduction of two equivalence relations, one on locations and one on guards (and thus rules). In our example on the one hand, the locations CT 0 and CT 1 should be equivalent, and on the other hand the rules r 5 and r 6 should be equivalent. In the following, we formalize weak adversaries using such symmetries in threshold automata.

Equivalence relations on guards and rules. Let us first define a correspondence between threshold guards. Fix two simple threshold guards

ϕ 1 : v∈V (b t1,v • x t1,v ) 1 ā • p + a 0 and ϕ 2 : v∈V (d t2,v • x t2,v ) 2 c • p + c 0 .
We say that ϕ 1 and ϕ 2 correspond to each other, denoted by ϕ 1 ≡ ϕ ϕ 2 , if:

-1 and 2 are the same relation, either ≥ or <, coefficients are the same, that is, ā = c and a 0 = c 0 , message types are the same, that is, t 1 = t 2 , there exists a permutation π on the set of values V, such that b t1,v = d t2,π(v) .

We extend this definition to threshold guards. Let ϕ

A = ϕ A 1 ∧ . . . ∧ ϕ A k and ϕ B = ϕ B 1 ∧ . . . ∧ ϕ B
m be threshold guards, and each ϕ A i and ϕ B j be a simple guard. We say ϕ A and ϕ B correspond to each other, and write ϕ A ≡ ϕ ϕ B , if k = m and there is a permutation ρ on the set {1, . . . , k} such that

ϕ A i ≡ ϕ ϕ B ρ(i)
for every 1 ≤ i ≤ k.

Example 3. In case x, y ∈ T and 0, 1, 2 ∈ V, we have y 0 ≥ n-2t ≡ ϕ y 1 ≥ n-2t and y 0 + 3y 1 < t + 1 ≡ ϕ y 1 + 3y 2 < t + 1. In the example from Table 1 we have r 5 ≡ ϕ r 6 , r 8 ≡ ϕ r 12 , and r 9 ≡ ϕ r 11 .

The equivalence relation over guards, allows us to define an equivalence relation ≡ R ⊆ R × R on rules. Let r 1 and r 2 be two rules from R. We have r 1 ≡ R r 2 if and only if it holds that: r 1 .ϕ ≡ ϕ r 2 .ϕ, and there exists a permutation π on the set of values V, such that (t, v) ∈ r 1 .u if and only if (t, π(v)) ∈ r 2 .u.

Example 4. Consider again our example from Table 1. The rules r 1 , r 2 , r 3 , r 4 have trivial guards, which are therefore all in the same equivalence class of ≡ ϕ . In contrast, not all the rules are equivalent w.r.t. relation ≡ R , as their update sets are different. Thus, we have r 1 ≡ R r 2 and r 3 ≡ R r 4 .

Equivalence relation on locations. We define equivalence relation ≡ L ⊆ L × L on locations inductively as follows:

-The set of border locations B is one equivalence class of ≡ L , that is, for every 1 , 2 ∈ B and every 3 ∈ B it holds that 1 ≡ L 2 , and 1 ≡ L 3 .

-Let 1 and 2 be two locations from L \ B. We have 1 ≡ L 2 if and only if there exist rules r 1 and r 2 and locations s 1 and s 2 such that

• s i is a source location of r i , for i = 1, 2, that is, r i .from = s i , • i is a destination location for r i , formally, r i .δ to ( i ) > 0, for i = 1, 2, • s 1 ≡ L s 2 , and r 1 ≡ R r 2 .
-The set of final locations F is either one equivalence class of ≡ L or a union of finitely many equivalence classes of ≡ L . As a consequence, there are no two locations 1 ∈ F and 2 ∈ F such that 1 ≡ L 2 .

Let PTA P be a probabilistic threshold automaton with processes, equipped with equivalence relations ≡ L and ≡ R . Assume , 0 , 1 ∈ L are locations, and r = (from, δ to , ϕ, u) ∈ R is a non-Dirac rule such that its source location is (r.from = ), and 0 and 1 are its destination locations. Then 0 ≡ L 1 . In words, all destinations of a non-Dirac rule are equivalent locations.

Example 5. In Figure 1 we have 7 equivalence classes w.r.

t. ≡ L , namely {I 0 , I 1 }, {J 0 , J 1 }, {SR}, {SP }, {E 0 , E 1 }, {D 0 , D 1 }, and {CT 0 , CT 1 }.
Such an equivalence relation does not always exist, due to the last requirement on final locations. For instance, on the automaton from Figure 2, where I ∈ B, J ∈ I, F ∈ F, where all rules have guard true and empty update set, it is not possible to define ≡ L . Intuitively, an adversary is able to infer whether the left or the right branch is taken, and consequently in similar asymmetric automata it may infer information about message content or coin tosses. However, typical randomized consensus algorithms from the literature [START_REF] Ben-Or | Another advantage of free choice: Completely asynchronous agreement protocols (extended abstract)[END_REF][START_REF] Bracha | Asynchronous Byzantine agreement protocols[END_REF][START_REF] Mostéfaoui | Randomized k-set agreement in crash-prone and Byzantine asynchronous systems[END_REF][START_REF] Jiun | Bosco: One-step Byzantine asynchronous consensus[END_REF] have a structure similar to the one in Figure 1, and are thus symmetric.

Semantics of a PTA P

The semantics of a probabilistic threshold automaton with processes is an infinitestate Markov decision process (MDP), which we formally define below.

Given a PTA P and a function N (defined earlier), we define the semantics, called probabilistic system with processes Sys(PTA P ), to be infinite-state MDP (Σ, I, Act, ∆), where Σ is the set of configurations for PTA P among which I ⊆ Σ are initial, the set of actions is Act = P(M) × C, and ∆ : Σ × Act → Dist(Σ) is the probabilistic transition function.

Configurations. A configuration σ is a tuple (s, Sent, Rcvd , p), where the components are defined as follows:

σ.s : C → L × N 0 is a function that describes the control states of processes, that is, the location and the round of each correct process, σ.Sent ⊆ M C is a set of messages sent by correct processes, σ.Rcvd : C → P(M) is a function that keeps track of the received messages for every correct process.

-σ.p ∈ N |Π| 0 is a vector of parameter values.
We write σ.Rcvd [p] |t,v,k for the set of messages from σ.Rcvd [p] of type t and value v that are sent in round k. Formally,

σ.Rcvd [p] |t,v,k = {m ∈ σ.Rcvd [p] | m.type = t ∧ m.val = v ∧ m.rnd = k}.
We write σ.s loc : C → L and σ.s rnd : C → N 0 for the projections to the first and the second component of σ.s, respectively.

A configuration σ = (s, Sent, Rcvd , p) is initial if all processes are in border locations of round 0, and there are no sent nor received messages in any round:

σ.Sent = ∅, for every p ∈ C we have σ.Rcvd [p] = ∅, for every p ∈ C there is a location ∈ B such that σ.s[p] = ( , 0).

A threshold guard evaluates to true in a configuration σ for a process p and a round k, written σ, p, k |= ϕ, if for all its conjuncts v∈V (b

v • x t,v ) ≥ ā • p + a 0 we have v∈V (b v • |σ.Rcvd [p] |t,v,k |) ≥ ā • (σ.p ) + a 0 ,
v • x t,v ) < ā • p + a 0 .
Actions. An action α = (M, p) ∈ Act stands for the atomic execution of the following two steps: (i) process p receives the set of messages M ⊆ M, and after that (ii) process p makes progress by executing a rule, if possible.

An action α = (M, p) is applicable to a configuration σ if each message from M has either been sent by a correct process or it comes from a faulty process, i.e., for every m ∈ M we have: m ∈ σ.Sent or m ∈ M F .

A rule r = (from, δ to , ϕ, u) is executable by a process p in a configuration σ with σ.s[p] = ( , k) if: (i) p is in the source location of the rule, that is, from = , and (ii) the guard evaluates to true in σ for p and k, that is, σ, p, k |= ϕ. In every configuration for every process there is at most one executable rule.

It is also important to note the role of the round number k in the definition of an executable rule. Whether a rule r is executable by p in σ depends only on the messages from the round in which this process is in σ. Thus, threshold automata are communication-closed [START_REF] Elrad | Decomposition of distributed programs into communication-closed layers[END_REF][START_REF] Damian | Communication-closed asynchronous protocols[END_REF] by construction and thus provide an effective model for many communication-closed fault-tolerant distributed algorithms in the literature. We consider this notion in more detail in Section 3.

Let σ be a configuration and let action α = (M, p) be applicable to σ. When α is applied to σ, process p receives messages from M , which results in configuration σ aux , and then executes a rule r that is executable by p in σ aux (if there is an executable rule), which finally results in σ . Note that M = ∅ implies that σ = σ aux , and if there is no executable rule in σ aux then we have σ aux = σ .

Let us define a function exec : Σ × Act → R ∪ {⊥} that given a configuration σ and an action α = (M, p) applicable to σ, outputs (i) the unique rule r that is executable by p in configuration σ aux obtained from σ by changing only σ aux .Rcvd [p] = σ.Rcvd [p] ∪ M , if such a rule exists, and (ii) it outputs ⊥ if no such rule exists. We define exec(σ, α) = ⊥ if α is not applicable to σ.

Let α = (M, p) be an action applicable to σ, and let be either a potential destination location of exec(σ, α) = ⊥, or is the location of p in σ if exec(σ, α) = ⊥. We write apply(σ, α, ) for the resulting configuration: parameters are unchanged, all messages from M are added to σ.Rcvd [p], and if exec(σ, α) = r = ⊥, then new messages from M are added to σ.Sent according to the update set r.u, and finally while the location and the round of all processes except p are unchanged, we have that location of p becomes and its round is unchanged (or increased by 1 if r is a round switch rule).

Formally, if α = (M, p), we have that apply(σ, α, ) = σ if and only if apply(σ, α, ) is defined and the following holds:

-The parameter values do not change: σ .p = σ.p.

-Process p receives all messages from M , formally, σ .Rcvd [p] = σ.Rcvd [p]∪M .

-The control states of processes, that is, their locations and rounds given by the function σ .s, are updated as follows:

• After updating σ.Rcvd [p], if there is no executable r for p, that is, if exec(σ, α) = ⊥, then the control states of all processes remain the same: σ .s = σ.s. • Otherwise, if exec(σ, α) = r = ⊥, then the control states for all the processes except for p remain the same. Formally, σ .s[q] = σ.s[q] for every q = p. Process p moves to location and either (i) it stays in the same round if r ∈ S is not a round switch rule, or (ii) it moves to the following round if r ∈ S. Formally, if we denote the round of p in σ by σ.s rnd [p] = k, then we have that σ .s[p] = ( , k) if r is not a round switch, and σ .s[p] = ( , k+1) if r is a round switch rule. -The set of sent messages is updated as follows:

• If exec(σ, α) = ⊥, then no rule is fired and thus no message is sent, that is, σ .Sent = σ.Sent.

• If exec(σ, α) = r = ⊥ then the rule r is fired, and the update set r.u dictates the set of messages (their types and values) that process p sends to all in round k = σ.s rnd

[p], that is, σ .Sent = σ.Sent ∪ {(p, t, v, k) | (t, v) ∈ r.u}.
Let α = (M, p) be applicable to σ, and let process p be in round k in configuration σ, that is, σ.s(p) = ( , k) for some location and round k. Then we define the round of action α in configuration σ to be k, and denote this by rnd σ (α) = k. When it is clear from the context which configuration we refer to, we only write rnd(α) instead of rnd σ (α).

Probabilistic transition function. The probabilistic transition function ∆ is defined such that for every two configurations σ and σ and for every action α applicable to σ, with exec(σ, α) = r ∈ R ∪ {⊥}, we have

∆(σ, α)(σ ) = ® r.δ to ( ) if apply(σ, α, ) = σ for some ∈ L 0 otherwise.
Note that if r = ⊥ we define r.δ to ( ) = 1, and if there exists a location with apply(σ, α, ) = σ , this location is uniquely defined.

Paths. A (finite or infinite) path in Sys(PTA) is an alternating sequence of configurations and actions σ 0 , α 0 , σ 1 , α 1 . . ., such that for i > 0, there exists a location i such that apply(σ i-1 , α i-1 , i ) = σ i . We denote the set of all paths by Paths and the set of all finite paths (ending with a configuration) by Paths fin . The length of a finite path ρ = σ 0 , α 0 , σ 1 , α 1 . . . , σ k is the number of actions taken, that is, |ρ| = k. Wlog if ρ is an infinite path, we let |ρ| = ∞. We sometimes consider prefixes of a (finite or infinite) path ρ, and for s < |ρ| write ρ s for σ 0 , α 0 , . . . , σ s . Also the last configuration σ k of a finite path ρ = σ 0 , α 0 . . . , α k-1 , σ k is written last(ρ). As sent messages cannot be unsent, the set of sent messages can only grow along a path. Thus, the set last(ρ).Sent contains the set σ i .Sent for every 0 ≤ i ≤ k. That is why we often write ρ.Sent instead of last(ρ).Sent.

Message identities

An adversary formalizes which messages will be received next. When formalizing weak adversaries, we have to capture that the adversary can pick a message without being aware of the content of the message. For this we introduce message identities in the model. Note that every action may include sending a finite number of messages. Therefore, in a finite path there are finitely many sent messages, and we can assign them their identities (IDs for short). For a path ρ ∈ Paths fin , we define IDs of messages sent by correct processes along ρ by a function ID[ρ] : ρ.Sent → N defined recursively on the length ρ: Base case. If ρ is a degenerative path ρ = σ 0 , then σ 0 is an initial configuration, and therefore, there are no sent messages in it. Formally, σ 0 .Sent = ∅ and there is nothing to assign.

Recursion. Let ρ = τ ασ ∈ Paths fin be a non-degenerative finite path. We distinguish two cases depending if new messages were sent while executing α.

-If no message is sent when applying α to last(τ ), i.e. if either no rule is executed exec(last(τ ), α) = ⊥, or if there is an executed rule exec(last(τ ), α) = r = ⊥ but r.u = ∅, then the function ID is unchanged: we set

ID[ρ] = ID[τ ].
-Otherwise, let r = exec(last(τ ), α) and let the set of messages sent when executing rule r from last(τ ) be r.u = {m 1 , . . . , m k } for some k ≥ 1, with

m 1 < M m 2 • • • < M m k .
Then the function ID[ρ] is defined as follows:

ID[ρ](m) = ® ID[τ ](m) if m ∈ τ.Sent, |τ.Sent| + i if m = m i ∈ r.u for 1 ≤ i ≤ k
Revealing messages from their IDs. It is important to notice that for every natural number n ≤ |τ.Sent| there is a unique message m ∈ τ.Sent with that identity, that is, with ID(m) = n. We define an inverse of msg when defined. Given a path ρ ∈ Paths fin we define a function rev-msg[ρ] : {1, 2, . . . , |ρ.Sent|} → ρ.Sent, such that for every n with 1 ≤ n ≤ |ρ.Sent| we have rev-msg

[ρ](n) = m if and only if ID[ρ](m) = n.
We extend this definition to a set of IDs, and define rev-msg[ρ] of a set of natural numbers N ⊂ N to be rev-msg

[ρ](N ) = {rev-msg[ρ](n) | n ∈ N }.
Faulty messages. Recall that M F = F × T × V × N 0 is the set of messages m = (p, t, v, k) ∈ M with the sender being a faulty process, that is, p ∈ F. Note that this set has countably infinitely many elements, and therefore there exists a bijection between the set of natural numbers and M F . We choose one such bijection ID f : M F → N to be an enumerating function for the set of the faulty messages.

Similarly, we define a reveal function rev-msg f : N → M F as the inverse of the identity function, that is, rev-msg f = ID -1 f . Moreover, for a set of natural numbers N ⊂ N we define rev-msg f (N ) = {rev-msg f (n) | n ∈ N }.

Adversaries

The non-determinism in Markov decision processes is traditionally resolved by a so-called adversary, see e.g. [START_REF] Baier | Principles of model checking[END_REF]Chap. 10]. An adversary is a function a : Paths fin → 2 N×{c,f } ×C that given a finite path ρ = σ 0 , α 0 , σ 1 , . . . , σ k of Sys(PTA P ) selects a set of message IDs with the nature of their senders (a set of elements from N × {c} or N × {f }) together with a correct process (thus from C) to whom these messages are delivered.

As an adversary only gives message IDs, we need to understand which messages correspond to them. This is why we introduce the function reveal[a] : Paths fin → Act that reveals the next action in a path according to the choice of the adversary a. Let a(ρ) = (N 1 × {c} × {p}) ∪ (N 2 × {f } × {p}), where N 1 and N 2 are finite sets of natural numbers, and p ∈ C is a correct process. Then we define reveal[a](ρ) to be the action (M 1 ∪ M 2 , p), where M 1 = rev-msg[ρ](N 1 ) and M 2 = rev-msg f (N 2 ).

Given a path ρ, we also define a function choice[ρ] : 2 ρ.Sent ×C → 2 N×{c,f } ×C that tells us which choice a(ρ) should the adversary take in order to obtain the expected action. Let (M, p) ∈ 2 ρ.Sent × C, with M = M 1 ∪ M 2 where M 1 are messages sent by correct processes and M 2 are messages sent by faulty processes.

Let N 1 = {ID[ρ](m) | m ∈ M 1 } and let N 2 = {ID f (m) | m ∈ M 2 }. Then we have choice[ρ](M, p) = (N, p), where N = (N 1 × {c}) ∪ (N 2 × {f }).
Given an initial configuration σ 0 , an adversary a generates a set paths(σ 0 , a) of infinite paths σ 0 , α 0 , σ 1 , . . . with the following property: for every i > 0, α i = reveal[a](σ 0 , σ 1 , . . . , σ i-1 ) and there exists a location i such that σ i = apply(σ i-1 , α i , i ). Every infinite path π ∈ paths(σ 0 , a), and every finite path ρ which is a prefix of an infinite path π ∈ paths(σ 0 , a), are said to be induced by a.

The MDP Sys(PTA P ) together with an initial configuration σ 0 and an adversary a induce a Markov chain, denoted by M σ0 a . Precisely, the state space of M σ0 a is Paths fin , its initial state is the initial configuration σ 0 -which is also a path of length 0-and the probabilistic transition function δ a,σ0 : Paths fin → Dist(Paths fin ) is defined for every τ ∈ Paths fin starting in σ 0 and ending in some configuration σ, for every action α, and every σ ∈ Σ by:

δ a (τ ) (τ ασ ) = ∆(σ, reveal[a](τ ))(σ ).
In words, the probability in M σ0 a to move from state τ to state τ ασ is non-zero as soon as there exists an action α such that σ = apply(σ, α , ) and a picks α . This equals the probability that the corresponding process moves to if the adversary a picks action α . Note that the Markov chain M σ0 a is acyclic, and even has the shape of a tree, since its states are the finite paths in Paths fin . We write P σ0 a for the probability measure over infinite paths starting at σ 0 in M σ0 a . Given σ 0 , a and a finite path ρ = σ 0 , α 0 , . . . , σ k ∈ Paths fin , we write M ρ a for the Markov chain which corresponds to the part of M σ0 a with initial state ρ. The probability measure P ρ a in M ρ a is inherited from the one in M σ0 a .

Weak adversaries. In order to define weak adversaries, we introduce an equivalence relation on paths. For two sets of messages M 1 and M 2 we say they are equivalent up to message values if there is a bijection f : M 1 → M 2 such that for every m ∈ M 1 we have that m and f (m) have the same sender, type and round. Formally, we have m.sen = f (m).sen, m.type = f (m).type, m.rnd = f (m).rnd .

The weak observation relation relates two configurations that differ only in message content and symmetric locations of processes. Formally: We extend the relation to finite paths of the same length: if π = σ 1 , σ 2 , . . . , σ k and π = σ 1 , σ 2 , . . . , σ k , then we write π ≡ w π if σ i ≡ w σ i for every

1 ≤ i ≤ k.
An adversary a is weak if for every two finite paths π and π with π ≡ w π we have that a(π) = a(π ). In words, a weak adversary does not distinguish two paths if they are equivalent, and thus makes the same choice for equivalent paths.

Note that for threshold automata on which ≡ L cannot be defined, we can also not define ≡ w . Therefore, weak adversaries are a property of only those distributed algorithms that can be modeled by symmetric automata.

Lemma 1. Let π = σ 0 , . . . , σ k , α k , σ k+1 and π = σ 0 , . . . , σ k , α k , σk+1 be two paths such that exec(σ k , α k ) = r is a non-Dirac rule with two destination locations = ¯ , with apply(σ k , α k , ) = σ k+1 and with apply(σ k , α k , ¯ ) = σk+1 . Then for every weak adversary a we have a(π) = a(π).

Proof. Fix an arbitrary weak adversary a. By definition of weak adversaries, it is enough to show that π ≡ w π, and thus to prove that σ k+1 ≡ w σk+1 .

We check all conditions for two configurations to be weakly-equivalent. Of course, σ k+1 .p = σk+1 .p. Let α k = (M, p).

For every correct process q = p, σ k+1 .s(q) = σk+1 .s(q). Writing σ k+1 .s(p) = ( , k) and σk+1 .s(p) = ( ¯ , k), then the rounds k and k are trivially equal, and ≡ L ¯ holds by definition of the equivalence relation on locations.

Moreover, the update is defined by the rule r, and is independent of the destination location, so that the sent messages coincide: σ k+1 .Sent = σ k .Sent ∪ r.u = σk+1 .Sent.

We now compare receive sets, and again they do not depend on the destination location, but only on r. For each correct process q = p it trivially holds that σ k+1 .Rcvd (q) = σk+1 .Rcvd (q). Also σ k+1 .Rcvd (p) = σ k .Rcvd (p) ∪ M = σk+1 .Rcvd (p).

We define two more notions for adversaries: An adversary a is communicationclosed if for every finite path ρ the action reveal[a](ρ) = α = (M, p) is such that each message m ∈ M is sent before or in the same round in which process p is in last(ρ). Formally, m.rnd ≤ rnd(α). An adversary a is round-rigid if for every finite path ρ the action reveal[a](ρ) = α = (M, p) has the smallest possible round, that is, there is no applicable action α such that rnd(α ) < rnd(α). In the sequel, we show that weak round-rigid adversaries are as expressive as weak adversaries (see Theorem 1 and Theorem 2).

Atomic Propositions and Stutter Equivalence

Properties of threshold-based distributed algorithms are expressed in temporal logic. More precisely, we consider a stutter-insensitive fragment of LTL, namely, LTL -X [START_REF] Baier | Principles of model checking[END_REF]Chapter 7]. The atomic propositions describe the non-emptiness of a location in a given round, i.e., whether there is at least one correct process in location ∈ L \ B in round k [START_REF] Bertrand | Verification of randomized consensus algorithms under round-rigid adversaries[END_REF]. The set of all such propositions for a round k ∈ N 0 is denoted by AP k = {ap( , k) : ∈ L \ B}. For every k we define a labeling function

λ k : Σ → 2 AP k such that ap( , k) ∈ λ k (σ) iff ∃p ∈ C. σ.s(p) = ( , k).
For a path π = σ 0 , α 1 , σ 1 , . . . , α n , σ n , n ∈ N, and a round k, a trace trace k (π) w.r.t. the labeling function λ k is the sequence

λ k (σ 0 )λ k (σ 1 ) . . . λ k (σ n ). Similarly, if a path is infinite π = σ 0 , α 1 , σ 1 , α 2 , σ 2 , . . ., then trace k (π) = λ k (σ 0 )λ k (σ 1 ) . . ..
We say that two finite traces are stutter equivalent w.r.t. AP k , denoted trace k (π 1 ) trace k (π 2 ), if there is a finite sequence A 0 A 1 . . . A n ∈ (2 AP k ) + , n ∈ N 0 , such that both trace k (π 1 ) and trace k (π 2 ) are contained in the language given by the regular expression

A + 0 A + 1 . . . A + n .
If traces of π 1 and π 2 are infinite, then stutter equivalence trace k (π 1 ) trace k (π 2 ) is defined in the standard way [START_REF] Baier | Principles of model checking[END_REF]. To simplify notation, we say that paths π 1 and π 2 are stutter equivalent w.r.t. AP k , and write π 1 k π 2 , instead of referring to specific path traces. Two stutter equivalent paths satisfy the same LTL -X formulas [3, Theorem 7.92].

Remark. We emphasize that atomic propositions cannot check emptiness of border locations from the set B. The specifications cannot observe the moment of transition from one round to another. This allows us to swap transitions of adjacent rounds below.

The following lemma expresses that an action may only change atomic propositions of its own round, as it only affects a process in that round.

Lemma 2. Let π = σ 0 , α 1 , σ 1 , . . . , σ s-1 , α s , σ s be a finite path. Then, for every round k = rnd(α s ), it holds that λ k (σ s-1 ) = λ k (σ s ).

Proof. Let ap( , k) ∈ λ k (σ s-1 ), meaning that for some correct process p ∈ C, σ s-1 .s(p) = ( , k). Since rnd(α s ) = k, we have α s = (M, q) for a set of messages M and some correct process q = p. Thus, application of α s does not affect p, and σ s .s(p) = ( , k). In other words, ap( , k) ∈ λ k (σ s ). This holds for every ap( , k) ∈ λ k (σ s-1 ), concluding the proof.

Using Lemma 2, it is easy to prove that swapping two actions of different rounds in a path yield a stutter equivalent path w.r.t. AP k for every ∈ N 0 : Lemma 3. Let π = σ 0 , . . . , σ s , σ s+1 , σ s+2 and π = σ 0 , . . . , σ s , σ s+1 , σ s+2 be two paths with π s = π s = σ 0 , . . . , σ s , and such that there are two actions α and α with rnd(α) = rnd(α ), and there are locations and with

σ s+1 = apply(σ s , α, ) σ s+2 = apply(σ s+1 , α , ) σ s+1 = apply(σ s , α , ) σ s+2 = apply(σ s+1 , α, )
Then σ s+2 = σ s+2 and for every k ∈ N 0 , π k π .

Proof. Let us first prove that σ s+2 = σ s+2 . Both σ s+2 and σ s+2 are obtained from σ s by applying α with and α with , just in different orders. By standard communication-closure arguments [START_REF] Elrad | Decomposition of distributed programs into communication-closed layers[END_REF][START_REF] Chaouch-Saad | A reduction theorem for the verification of round-based distributed algorithms[END_REF][START_REF] Damian | Communication-closed asynchronous protocols[END_REF], if an action from a smaller round happens in an execution after an action of larger round, it is easy to prove that these two actions do not affect each other. Thus, in any order they will lead to the same configuration.

Let us now fix an arbitrary k ∈ N 0 and prove that π k π . As these two paths have the same prefix of length s, it suffices to prove that σ s , σ s+1 , σ s+2 k σ s , σ s+1 , σ s+2 . We distinguish three cases: (i) k = rnd(α) and k = rnd(α ), (ii) k = rnd(α), and (iii) k = rnd(α ). Cases (ii) and (iii) are symmetrical, so that we only prove (ii).

(i) By Lemma 2 we have

λ k (σ s ) = λ k (σ s+1 ) = λ k (σ s+1 ) = λ k (σ s+2
), which trivially yields the required statement.

(ii) As in this case k = rnd(α ), we can apply Lemma 2 and obtain that

λ k (σ s+1 ) = λ k (σ s+2 ) and λ k (σ s ) = λ k (σ s+1 ). Therefore, trace k (σ s , σ s+1 , σ s+2 ) = λ k (σ s )λ k (σ s+2 )λ k (σ s+2 ), and trace k (σ s , σ s+1 , σ s+2 ) = λ k (σ s )λ k (σ s )λ k (σ s+2 ),
and they are clearly stutter equivalent w.r.t. k.

Reduction to Communication-closed Adversaries

In this section we show that in the threshold automata framework (which models communication-closed algorithms by construction, cf. Section 2.2), for every adversary, there exists an "equivalent" communication-closed adversary. This step is quite intuitive: if the adversary delivers a message m of round r to a process in round r = r, this is "similar" to an adversary that instead does not deliver m now, but delivers m later when the process enters r. However, we need to formalize this, in order to set the stage of our central reduction in Section 4.

For a set of messages M and a round k we denote by M | k the set of messages from M sent in round k, that is,

M | k = {m ∈ M | m.rnd = k}. Similarly, we define M | ≤k = ∪ i≤k M | i the set of messages from M sent in any round i ≤ k.
Communication-closed configurations and Markov chains. The definition of rules executable in σ in Section 2.2 yields that messages received from the "future", i.e., from a round k > σ.s rnd (p), do not play a role for process p in σ. Namely, if two configurations σ and σ differ only in the messages that processes have received from future rounds, then the same rules are executable in σ and σ . That is why for every σ we define σ to be a configuration in which each process only has received messages from "past" and "present", i.e., from a round k ≤ σ.s rnd (p). As border locations can be seen as borders between consecutive rounds, we decide to let processes from border locations in σ receive messages only from the "past", as if they were not yet in the next round. Formally, σ.s = σ.s and σ.Sent = σ.Sent and σ.p = σ.p and for all p ∈ C, if

s loc (p) ∈ B then σ.Rcvd (p) = σ.Rcvd (p)| ≤s rnd (p)-1 otherwise σ.Rcvd (p) = σ.Rcvd (p)| ≤s rnd (p) . A configuration σ is communication-closed if σ = σ.
Recall that a path has the form σ 0 , α 0 , . . . , α s-1 , σ s , but given a sequence of configurations σ 0 , . . . , σ s of a path generated by an adversary a, we can easily recover the missing actions. This allows us to consider the states of Markov chains to be finite sequences of configurations rather than finite paths. Both representations are equivalent, and thus in this section we consider paths as sequences of configurations. We can lift the notion of communication-closed configurations to communication-closed paths, such that given a path ρ = σ 0 , . . . , σ k we define µ(ρ) = σ 0 , . . . , σ k . Finally, we obtain a communication-closed Markov chain M σ0 a by replacing each state ρ in M σ0 a by µ(ρ).

Communication-closed adversaries. Given an arbitrary adversary a, we define its corresponding communication-closed adversary cc(a) as follows. If a process p is scheduled by a it is also scheduled by cc(a), but it receives different messages: if p is not at the beginning of a round, cc(a) should check which messages a would give to p, and among them cc(a) should choose only those messages that do not come from future rounds. Once a process reaches a round (when it is at a border location in B), it receives all the messages from that round and all those that were previously sent to it, but the process could not receive it earlier (because at that time these were messages from the future.) As cc(a) has to know the behavior of a, we show how to recover a path generated by a (if it exists) if we are given a communication-closed path. Formally, given an adversary a and a communication-closed path ρ, we define ν a (ρ) to be a path τ generated by a, such that µ(τ ) = ρ, if such a path exists; otherwise, ν a (ρ) is undefined. Observe that if ρ is a path generated by a, then ρ = ν a (µ(ρ)).

Finally, we define a communication-closed version of an adversary formally. Recall that τ i denotes the prefix of τ of length i. Definition 2. Let a be an adversary. For a given finite path ρ, if ν a (µ(ρ)) is undefined then cc(a)(ρ) is an arbitrary action. Otherwise, if ν a (µ(ρ)) = τ = σ 0 , . . . , σ s , let reveal[a](τ i ) = α i = (M i , p ji ), for each 0 ≤ i ≤ s and some p ji ∈ C. If α s = (M s , p), in order to define cc(a)(ρ) we distinguish two cases:

-If σ s .s[p] = ( , k) with ∈ B, then cc(a)(ρ) = choice[τ ](M s | ≤k , p). -If σ s .s[p] = ( , k) with ∈ B, then for S p = {i | 1 ≤ i < s ∧ α i = (M i , p)}
being the set of indices of the actions involving process p:

cc(a)(ρ) = choice[τ ](M, p), for M = M s | ≤k ∪ i∈Sp M i | k .
Theorem 1. For every adversary a, M σ0 a = M σ0 cc(a) . Moreover, for every LTL -X formula ψ, P σ0 a (ψ) = P σ0 cc(a) (ψ).

4 From Weak to Round-Rigid Adversaries

In this section we reduce a communication-closed weak adversary to a roundrigid adversary. More precisely, we show that we can transform the Markov chain defined by the weak adversary to a round-rigid Markov chain that satisfies specific temporal logic formulas with the same probabilities.

Swapping function for paths and swapped adversaries We first define a swapping function for a path ρ = σ 0 , α 0 , σ

-X formula ψ, ρ |= ψ iff sw[ρ, s](ρ) |= ψ. If ρ = sw[ρ, s](ρ)
, we also write sw[ρ, s] -1 (ρ ) = ρ. Now, given a weak communication-closed adversary a, a path ρ, and a swapping index s for ρ, we define the swapped adversary a = swap[ρ, s](a) that, intuitively, will implement the swapping function sw[ρ, s] over a-induced paths. Formally, for any finite path ρ , the definition distinguishes whether ρ s ≡ ρ s , and depends on the length of ρ :

(i) if |ρ | < s, then a (ρ ) = a(ρ ); (ii) if ρ s ≡ w ρ s and |ρ | ≥ s, then a (ρ ) = a(ρ ); (iii) if ρ s ≡ w ρ s and |ρ | = s, then a (ρ ) = choice[ρ ] reveal[a](ρ s+1 ) ; (iv) if ρ s ≡ w ρ s and |ρ | = s+1, then a (ρ ) = choice[ρ ] reveal[a](ρ s ) ; (v) if ρ s ≡ w ρ s and |ρ | ≥ s+2, then a (ρ ) = choice[ρ ] reveal[a](sw[ρ, s] -1 (ρ )) .
Let us give some intuition on the definition of the swapped adversary swap[ρ, s](a). Cases (i) and (ii) concern paths that are not involved in the swapping: either they are shorter than the position s at which the swap occurs, or their prefix of length s is not weakly-equivalent to the one of ρ. In these easy cases, a = swap[ρ, s](a) is defined as a. Case (iii) applies to all paths of length s that are weakly-equivalent to ρ s , and the goal is to define swap[ρ, s](a) so that it selects action α s+1 . However, under a and swap[ρ, s](a), the identities of messages may be different along paths (and their extensions) that are equivalent to ρ s . We thus need to use the reveal[a] and choice[ ] functions to define that the action prescribed by swap[ρ, s](a) is α s+1 . Case (iv) applies to paths of length s+1, whose prefix of length s is weakly-equivalent to ρ s . For them, the decision swap[ρ, s](a) should results in action α s . Finally, (v) deals with longer paths, for which a and swap[ρ, s](a) take the same decisions, up to the renaming of message identities, and the earlier swapping of α s and α s+1 .

σ 0 a : σ2 σ s σ s+1 σ s+2 σs+2 α 0 , 0 . . . α s+1 , s+1 αs s ¯ s σ 0 a : σ2 σ s σ s+1 σs+1 σ s+2 σs+2
α 0 , 0 Fig. 3. Parts of Markov chains M σ 0 a (above) and M σ 0 a (below) following Proposition 1. We assume here αs is a non-Dirac action with two destination locations s and ¯ s, and αs+1 is a Dirac action with destination location s+1. If some of actions α0, . . . , αs-1 are non-Dirac, we omit drawing branches that are irrelevant for Proposition 1. Note that reveal[a](σ0, . . . , σs+1) and reveal[a](σ0, . . . , σs+1) must be the same action αs+1, as a is a weak adversary. This is the key insight that allows swapping, which would not be possible for a strong adversary with reveal[a](σ0, . . . , σs+1) = reveal[a](σ0, . . . , σs+1).

Excerpts of the Markov chains M σ0

a and M σ0 a in Figure 3 illustrate the transformation to the swapped adversary. Observe that swapping α s and α s+1 relies on the fact that a is weak. Indeed, the same action α s+1 applies after α s even if α s induces a non-Dirac distribution. Observe that swap[ρ, s](a) is still a weak adversary, since it is defined uniformly over weakly-equivalent paths.

Adversaries a and swap[ρ, s](a) are tightly related. First, the successor configurations in two steps after a path ρ ≡ w ρ s are the same, and they have the same probabilities to happen. Second, the Markov chains from these points are identical. Finally the probabilities of LTL -X formulas are preserved.

Proposition 1. Let a be a weak communication-closed adversary, ρ an a-induced path and s a swapping index. Then, the swapped adversary a = swap[ρ, s](a) is again a weak communication-closed adversary, and it satisfies:

1. for every ρ ≡ w ρ s and every σ ∈ Σ, we have

P ρ a (F =2 σ) = P ρ a (F =2 σ) 2.
for every path ρ with |ρ| = s+2, we have

M ρ a = M sw[ρ,s]( ρ) a
3. for every LTL -X formula ψ, we have

P σ0 a (ψ) = P σ0 a (ψ)
Proof. Remark that indeed swap[ρ, s](a) is weak, because it is defined uniformely for weakly-equivalent paths. It is also communication-closed, as a is.

Let us now prove the three statements.

1. Let ρ ≡ w ρ s , and let σ be a configuration with P ρ a (F =2 σ) > 0. Then there exists an a-induced path ρ α s σ s+1 α s+1 σ and locations s , s+1 such that This is (v) in the definition of swap[ρ, s](a), and also applies if ρ ≡ w ρ s , in which case sw[ρ, s] -1 (ρ ) = ρ . In words, swap[ρ, s](a) consists in applying a on the reverse swapped path. Therefore, the subsequent Markov chains are equal, as illustrated on Figure 3. 3. Finally, to prove that the probabilities of LTL -X formulas are preserved, we argue that M σ0 a and M σ0 swap[ρ,s](a) are essentially the same, up to the swapping of some paths at positions s and s+1. Remember that they both are treeshaped. First, they are equal up to depth s. Then item (i) shows that the successors from depth s in two steps are the same, and they happen with same probabilities. Last, item (ii) shows that the subsequent Markov chains are identical. To conclude, we use Lemma 3 to justify that even if actions are swapped at positions s and s+1, they satisfy the same LTL -X formulas.

Theorem 2. For every weak communication-closed adversary a under which every round terminates, there exists a weak round-rigid adversary a such that for every LTL -X formula ψ we have P σ0 a (ψ) = P σ0 a (ψ). Proof (sketch). Theorem 2 is obtained by applying iteratively Proposition 1 to consecutive actions that are in reverse order. Since every round is assumed to terminate under a, one can start by moving towards the beginning all actions of round 1 that happen after actions of later rounds; then one swaps all actions of round 2, and so on, to obtain in the limit a weak adversary which is round-rigid.

Conclusions

Parameterized verification of safety and almost sure termination of a class of distributed consensus algorithms [START_REF] Ben-Or | Another advantage of free choice: Completely asynchronous agreement protocols (extended abstract)[END_REF][START_REF] Bracha | Asynchronous Byzantine agreement protocols[END_REF][START_REF] Mostéfaoui | Randomized k-set agreement in crash-prone and Byzantine asynchronous systems[END_REF][START_REF] Jiun | Bosco: One-step Byzantine asynchronous consensus[END_REF] has been recently considered in [START_REF] Bertrand | Verification of randomized consensus algorithms under round-rigid adversaries[END_REF]. For almost sure termination, the authors limited themselves to so-called "roundrigid" adversaries, which were introduced by the authors for that purpose. Verification under these adversaries was reduced to verification of specifications in a linear temporal logic that can be checked (within a few minutes) with the ByMC model checker [START_REF] Konnov | ByMC: Byzantine model checker[END_REF].

In this paper, we have shown that automated verification under weak adversaries can be reduced to verification of round-rigid adversaries. More precisely, in order to verify randomized distributed algorithms under weak adversaries, one only needs to verify their behavior under round-rigid adversaries, which has been done in [START_REF] Bertrand | Verification of randomized consensus algorithms under round-rigid adversaries[END_REF] for various randomized consensus algorithms. In order to define weak adversaries, we were forced to reason within a system model with semantics that explicitly talks about processes with IDs and messages. In contrast, the standard semantics of threshold automata, namely, counter systems is used in [START_REF] Bertrand | Verification of randomized consensus algorithms under round-rigid adversaries[END_REF] and in ByMC. For a complete chain of proof we would need to connect process-based semantics to counter systems. This is a rather standard technical argument so that we do not give it here. From a theoretical viewpoint we find our reduction from weak adversaries to round-rigid adversaries more interesting: reductions for concurrent distributed systems is typically done for reachability properties [START_REF] Lipton | Reduction: A method of proving properties of parallel programs[END_REF][START_REF] Elrad | Decomposition of distributed programs into communication-closed layers[END_REF][START_REF] Konnov | Para 2 : Parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms[END_REF] or linear temporal properties [START_REF] Chaouch-Saad | A reduction theorem for the verification of round-based distributed algorithms[END_REF][START_REF] Konnov | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms[END_REF][START_REF] Damian | Communication-closed asynchronous protocols[END_REF]. As a result, the reduction argument is conducted on traces generated by the system: one shows that by swapping transitions in a trace we arrive at another, yet "simpler" trace of the system. In this paper, we lifted this reasoning from traces to computation trees and MDPs which shows that reductions are not only efficient in nondeterministic systems but also in probabilistic systems defined by distributed algorithms. This mirrors the recent "synchronizing" trend in the verification of non-deterministic fault-tolerant distributed algorithms [START_REF] Gleissenthall | Pretend synchrony[END_REF][START_REF] Kragl | Synchronizing the asynchronous[END_REF][START_REF] Bouajjani | On the completeness of verifying message passing programs under bounded asynchrony[END_REF][START_REF] Damian | Communication-closed asynchronous protocols[END_REF][START_REF] Bertrand | Verification of randomized consensus algorithms under round-rigid adversaries[END_REF], and opens this domain to automated parameterized verification of randomized distributed algorithms.

Example 1 . 2 Fig. 1 .Fig. 2 .

 1212 Fig.1. Ben-Or's randomized consensus algorithm as a probabilistic threshold automaton with processes.

  and similarly for conjuncts of the other form, i.e., v∈V (b

Definition 1 .

 1 The weak observation relation is the equivalence relation ≡ w ⊆ Σ 2 such that σ ≡ w σ if and only if for every correct process p ∈ C, if σ.s(p) = ( 1 , k 1 ) and σ .s(p) = ( 2 , k 2 ), then k 1 = k 2 and 1 ≡ L 2 . σ.Sent and σ .Sent are equivalent up to message values for all p ∈ C, σ.Rcvd (p) and σ .Rcvd (p) are equivalent up to message values σ.p = σ .p

σ

  s+1 = apply(σ s , α s , s ) σ = apply(σ s+1 , α s+1 , s+1 ) Let ρ = sw[ρ, s](ρ α s σ s+1 α s+1 σ). By definition of swap[ρ, s](a), ρ is a path induced by swap[ρ, s](a), and it ends in σ. More precisely, lettingα s+1 = choice[ρ ] reveal[a](ρ ) σ s+1 = apply(σ s , α s+1 , s+1 ) α s = choice[ρ α s+1 σ s+1 ] reveal[a ](ρ α s σ s+1 ) σ s+2 = apply(σ s+1 , α s , s ) then σ s+2 = σ and ρ = ρ α s+1 σ s+1 α s σ. Thus P ρ swap[ρ,s](a) (F =2 σ) > 0.Moreover, by commutativity of multiplication, the probabilities of reaching σ in two steps in M ρ a and M ρ swap[ρ,s](a) coincide: they are equal to α s .δ to ( s ) × α s+1 .δ to ( s+1 ). 2. To prove that the Markov chains after ρ of length s+2 under a, and the one after sw[ρ, s](ρ) under swap[ρ, s](a) are equal, we observe that, for paths longer than s+2, a (ρ ) = choice[ρ ] reveal[a](sw[ρ, s] -1 (ρ )) .

  1 , . . . , σ s , α s , σ s+1 , α s+1 , σ s+2 . . . and s ∈ N a swapping index for ρ, such that rnd(α s ) > rnd(α s+1 ). It applies to a path ρ = σ0 , . . . , σs , ᾱs , σs+1 , ᾱs+1 , σs+2 , . . . such that ρs ≡ w ρ s , and swaps its actions (and target locations) at steps s and s+1. Formally, if ¯ s , ¯ s+1 are the destination locations at step s and s+1, i.e. apply(σ s , ᾱs , ¯ s ) = σs+1 and apply(σ s+1 , ᾱs+1 , ¯ s+1 ) = σs+2 , then for σ s+1 = apply(σ s , ᾱs+1 , ¯ s+1 ) we definesw[ρ, s](ρ) = ® σ0 , . . . ,σs , ᾱs+1 , σ s+1 , ᾱs , σs+2 , . . . if ρs ≡ w ρ s ρ otherwise. Note that the configurations in ρ and sw[ρ, s](ρ) may only differ at position s+1, and that ρ and sw[ρ, s](ρ) are stutter-equivalent. Hence, for every LTL

This project has received funding from Interchain Foundation (Switzerland), and the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme under grant agreement No 787367 (PaVeS).