Armando Castañeda
email: armando.castanedar@inria.com

Damien Imbs
email: damien.imbs@irisa.fr

Sergio Rajsbaum
email: rajsbaum@math.unam.mx

Michel Raynal
email: raynal@irisa.fr

Enriching the reduction map of sub-consensus tasks

Keywords: Decision task, Distributed computability, Problem hierarchy, Renaming problem, k-Set agreement, Symmetry Breaking, Wait-freedom. Enrichir la Tâche de décision, Calculabilité distribuée, Hiérarchie de problèmes, Renommage, k-Accord ensembliste, Cassage de symétrie, Sans-attente

Understanding the relative computability power of tasks, in the presence of asynchrony and failures, is a central concern of distributed computing theory. In the wait-free case, where the system consists of n processes and any of them can fail by crashing, substantial attention has been devoted to understanding the relative power of the subconsensus family of tasks, which are too weak to solve consensus for two processes. The first major results showed that set agreement and renaming (except for some particular values of n) cannot be solved wait-free in read/write memory. Then it was proved that renaming is strictly weaker than set agreement (when n is odd).

This paper considers a natural family of subconsensus tasks that includes set agreement, renaming and other generalized symmetry breaking (GSB) tasks. It extends previous results, and proves various new results about when there is a reduction and when not, among these tasks. Among other results, the paper shows that there are incomparable subconsensus tasks.

Introduction

A task is the distributed computing equivalent of the notion of a function encountered is sequential computing. In a task, each input is a vector, whose entries are distributed to the processes, and after communicating with each other, processes decide on local outputs, that together form a legal output vector respecting the task specification. In an asynchronous system, a protocol solves a task wait-free if any process that continues to run will halt with an output value in a fixed number of steps, regardless of delays or crashes of other processes.

Understanding the relative computability power of tasks, in presence of asynchrony and failures, is a central concern of distributed computing theory. Given two tasks, can one be used to implement the other, or are they incomparable? To this end, an important line of research consists in defining relevant families of tasks, designing reductions from tasks to other tasks, proving when such reductions are impossible, and looking for tasks that are universal for the family.

The consensus hierarchy Measuring the relative power of tasks using consensus numbers [START_REF] Herlihy | Wait-Free Synchronization[END_REF] has been very fruitful. A task has consensus number x if it is powerful enough to wait-free implement consensus [START_REF] Fischer | Impossibility of Distributed Consensus with One Faulty Process[END_REF] in a system of x processes but too weak to implement it in a system of x + 1 processes. If it can implement consensus for any number of processes, its consensus number is +∞. If a task can solve consensus for n processes, it is universal in a n-process system [START_REF] Herlihy | Wait-Free Synchronization[END_REF], in the sense that it can be used to solve any other task in such a system. The consensus hierarchy implied by this result describes the relative power of a large family of tasks. As shown in [START_REF] Herlihy | Wait-Free Synchronization[END_REF], read/write registers have consensus number 1, test&set, queues, stacks have consensus number 2, etc., until tasks such as compare&swap or LL/SC whose consensus number is +∞. The consensus hierarchy provides us with a simple way to know if a given task is computationally stronger than another in the presence of asynchrony and any number of process crashes.

Sub-consensus tasks Substantial attention has been devoted to understanding the relative power of the subconsensus family of tasks, which are too weak to solve consensus for two processes, and yet, very little is known. Subconsensus tasks have a fine structure, inaccessible by consensus-based analysis. In summary, the only hierarchy results known are the following set agreement and renaming results. First, while both tasks have consensus number 1 (as read/write registers), they cannot be implemented from read/write registers, except for some particular values of n, for which renaming can be implemented from read/write registers. Second, it was proved that renaming is strictly weaker than set agreement, when n is odd. We now describe in more detail these results.

In the (n, k)-set agreement task [START_REF] Chaudhuri | More Choices Allow More Faults: Set Consensus Problems in Totally Asynchronous Systems[END_REF], n processes have to agree on at most k different values. It is a weakening of consensus, and when k = 1, it is equal to consensus. The first major result about subconsensus tasks was that (n, k)-set agreement cannot be implemented from read/write registers, even when k = n-1 [START_REF] Borowsky | Generalized FLP Impossibility Result for t-Resilient Asynchronous Computations[END_REF][START_REF] Herlihy | The Topological Structure of Asynchronous Computability[END_REF][START_REF] Saks | Wait-Free k-Set Agreement Is Impossible: The Topology of Public Knowledge[END_REF], and lead to the discovery of a deep connection between distributed computing and topology. Later on, the structure of the set agreement family of tasks was identified to be a partial order, and it was shown that (n, k)-set agreement cannot be used to solve consensus among two processes, even when k = 2, e.g. [START_REF] Chaudhuri | Understanding the Set Consensus Partial Order Using the Borowsky-Gafni Simulation (Extended Abstract)[END_REF][START_REF] Herlihy | Set Consensus Using Arbitrary Objects (Preliminary Version)[END_REF].

When solving M -renaming [START_REF] Attiya | Renaming in Asynchronous Environment[END_REF] the processes have to decide distinct names from a name space whose size M is as small as possible. Initially it was proved that (n + 1)-renaming, cannot be wait-free solved in a read/write system [START_REF] Attiya | Renaming in Asynchronous Environment[END_REF]. It took a substantial use of topology to show that (except for some specific values of n [START_REF] Castañeda | New Combinatorial Topology Upper and Lower Bounds for Renaming[END_REF]), M -renaming can be implemented out of read/write registers if and only if M ≥ 2n -1 [START_REF] Herlihy | The Topological Structure of Asynchronous Computability[END_REF].

Set agreement and renaming appear to be quite dissimilar tasks, one being about agreement while the other is about symmetry breaking. Thus it was surprising to know [START_REF] Gafni | Distributed Programming with Tasks[END_REF][START_REF] Gafni | Subconsensus Tasks: Renaming is Weaker Than Set Agreement[END_REF] that (n, n -1)-set agreement can be used to implement (2n -2)-renaming, while the opposite is impossible, when n is odd. The result was first proved in [START_REF] Gafni | Subconsensus Tasks: Renaming is Weaker Than Set Agreement[END_REF] in a natural round-by-round iterated computational model (IM) (e.g. see [START_REF] Rajsbaum | Iterated Shared Memory Models[END_REF]), and then extended to the usual read/write model in [START_REF] Gafni | Distributed Programming with Tasks[END_REF] using a simulation.

The family of generalized symmetry breaking tasks Until recently, the main hierarchy results for subconsensus tasks where about (n, k)-set agreement and M -renaming, and only for the particular case of k = n -1, M = 2n -2, and n odd. In an effort to expand these results, a conceptual framework has recently been introduced in [START_REF] Imbs | The Universe of Symmetry Breaking Tasks[END_REF], to investigate the family of generalized symmetry breaking (GSB) tasks. The notation n, m, ℓ, u -GSB is used to denote the tasks on n processes for m possible decision values, [1..m], where each value has to be decided by at least ℓ and at most u processes 1 Some examples of GSB tasks are the following. M -renaming is nothing else than the n, M, 0, 1 -GSB task. Weak symmetry breaking [START_REF] Gafni | Subconsensus Tasks: Renaming is Weaker Than Set Agreement[END_REF] is the n, 2, 1, n -1 -GSB task. A new task is k-slot [START_REF] Imbs | The Universe of Symmetry Breaking Tasks[END_REF], the n, k, 1, n -GSB task.

Among other results, it is shown in [START_REF] Imbs | The Universe of Symmetry Breaking Tasks[END_REF] that perfect renaming, i.e., n, n, 1, 1 -GSB, is universal for the whole family of GSB tasks, in the sense that any of these tasks can be solved from an algorithm solving the n, n, 1, 1 -GSB task.

Contents of the paper

The aim of this paper is to expand our knowledge about the fine structure of subconsensus tasks, enriching the map of reductions among set agreement, renaming and other GSB tasks. The map of Figure 1 summarizes our new results, as well as previous results. An arrow with a black dot represents a new reduction; if it has a cross it is an impossibility result. As any GSB task on n processes is solvable from n, n, 1, 1 -GSB, the corresponding arrows are not depicted.

(n, 1)-SA (n, 2)-SA (n, k)-SA (n, n -2)-SA (n, n -1)-SA n, n, 1, 1 -GSB + × n = 2 ∀n ≥ 3 ∀n ≥ 4 ∀n ∀n, k ≥ ⌈ n 2 ⌉ + 1 gcd( k 1 , ..., k k-1 ) = 1 ∀n, k . . . . . . + n, ⌈ n k ⌉, 1, n -GSB n, 2n -⌈ n k ⌉, 0, 1 -GSB n, n + k -1, 0, 1 -GSB ∀n, k ∀n, k ∀n ∀n, k ∀n, k [12]
[15]

× ∀n odd, k = n -1 [START_REF] Gafni | Distributed Programming with Tasks[END_REF][START_REF] Gafni | Subconsensus Tasks: Renaming is Weaker Than Set Agreement[END_REF] (n, n -1)-T&S (n ′ , n -1)-T&S ∀n [START_REF] Gafni | Adaptive Renaming and Set Agreement: a Guided Visit to Asynchronous Computability[END_REF] ∀n, n ′ [START_REF] Gafni | Adaptive Renaming and Set Agreement: a Guided Visit to Asynchronous Computability[END_REF] gcd( n 1 , ..., n n-1 ) = 1

∀n, k = n -1 [7] ∀n, k = n -1 [17] + + ∀n, in IM n, n + 1, 0, 1 -GSB ∀n, in IM + [23] A B C n = 2 D ∀n = 2 x , x > 1, k = n -1 E × ∀n, k = n -1
Figure 1: A map relating (n, k)-set agreement tasks and GSB tasks.

Perhaps our main result is showing that two apparently very different kinds of subconsensus tasks, perfect renaming and (n, n -2)set agreement, an agreement and a symmetric breaking, are incomparable. We single out from the map of Figure 1 the following results, arrows labeled A,B,C, D and E.

• Arrow A : Perfect renaming cannot implement (n, n -2)-set agreement in the IM (Theorem 7).

• Arrow B: (n + 1)-renaming (i.e., the most powerful non-perfect renaming problem) cannot implement (n, n -1)-set agreement in the IM (Theorem 6).

• Arrow C: A characterization of values of k for which (n, k)-set agreement cannot implement perfect renaming (Theorem 9).

• Arrow D: A partial answer to the question left open in [START_REF] Gafni | Subconsensus Tasks: Renaming is Weaker Than Set Agreement[END_REF] where it was shown that (2n -2)-renaming cannot implement (n, n -1)-set agreement when n is odd. This result is extended to all n = 2 x , x > 1 (Theorem 4), i.e., it is extended for infinitely many values of n. However, let us observe that for n ≥ 3, arrow B closes the open question in [START_REF] Gafni | Subconsensus Tasks: Renaming is Weaker Than Set Agreement[END_REF], in the IM, since obviously (n + 1)-renaming can implement (2n -2)-renaming, for n ≥ 3. In fact, note that arrow B strengthens significantly this result showing that, in the IM, even (n + 1)-renaming cannot implement (n, n -1)-set agreement.

• Arrow E: (2n -2)-renaming cannot implement (n, n -2)-set agreement, for any n (Theorem 5). Of course all cases n = 2 x , x > 1, are implied by arrow D, however, the proof of this result is simple and does not use any topological argument.

When considering the map of Figure 1 let us notice that the right part of the bottom line is due to [START_REF] Gafni | Adaptive Renaming and Set Agreement: a Guided Visit to Asynchronous Computability[END_REF] where it is shown that (a) (n, n -1)-set agreement and (n, n -1)-test&set are equivalent and (b) (n, n -1)-test&set and (n ′ , n -1)-test&set are also equivalent for any n ′ ≥ n.

Related work A hierarchy of subconsensus tasks has been defined in [START_REF] Gafni | N-Consensus is the Second Strongest Object for N+1 Processes[END_REF] where a problem P belongs to class k if k is the smallest integer such that P can be wait-free solved in an n-process asynchronous read/write system enriched with (n, k)-set agreement objects. Also, [START_REF] Herlihy | A Classification of Wait-free Loop Agreement Tasks[END_REF] studies the hierarchy of loop agreement subconsensus tasks, under a restricted implementation notion, and identify an infinite hierarchy, where some loop agreement tasks are incomparable.

The M -renaming problem considered in this paper is different from the adaptive renaming version, where the size of the output name space depends on the actual number of processes that participate in a given execution, and not on the total number of processes of the system, n. While the consensus number of perfect adaptive renaming is known to be 2 [START_REF] Castañeda | The Renaming Problem in Shared Memory Systems: an Introduction[END_REF], in this paper we consider the relative power of non-adaptive renaming. Let us recall that in a system with n processes, adaptive (2p -⌈ p n-1 ⌉)-renaming is equivalent to (n, n -1)-set agreement [START_REF] Gafni | Adaptive Renaming and Set Agreement: a Guided Visit to Asynchronous Computability[END_REF] where p, 1 ≤ p ≤ n, denotes the number of participating processes. It is shown in [START_REF] Gafni | From Adaptive Renaming to Set Agreement[END_REF] that (n, k)-set agreement can be solved from adaptive (p + k -1)-renaming. Combined with this paper, this emphasizes an important difference between adaptive and non-adaptive renaming. Let us also notice that test&set and its variants are adaptive while GSB tasks are not.

Roadmap

The paper is composed of 5 sections. Section 2 presents formally the model, the notion of a task and the notations used in the paper. Then, Section 3 focuses on the new arrows from GSB tasks to (n, k)-set Agreement, while Section 4 focuses on the new arrows in the other direction. Finally, Section 5 concludes the paper.

2 Model, tasks and notation 2.1 Base read/write wait-free computation model Due to space limitations and the fact that this model is widely used in the literature, we do not explain it in detail here. A detailed description of this model is given in [START_REF] Imbs | The Universe of Symmetry Breaking Tasks[END_REF]. Nevertheless, we restate carefully some aspects of this model because we are interested in a comparison-based and an index-independent solvability notion that are not as common.

Read/write wait-free system model This paper considers the usual asynchronous, wait-free shared memory system where at most n -1 out of n processes p 1 , ..., p n can fail by crashing. The participating processes in a run are processes that take at least one step in that run. Those that take a finite number of steps are faulty (sometimes called crashed), the others are correct (or non-faulty). That is, the correct processes of a run are those that take an infinite number of steps. Moreover, a non-participating process is a faulty process. A participating process can be correct or faulty.

The memory is made up of single-writer/multi-reader registers. The subscript i (used in p i ) is called the index of p i . Indexes are used only for addressing purposes (this is formalized below).

The algorithms designed for this computation model have to work despite up to n -1 process crashes. In some sections, in addition to registers, processes are allowed to cooperate through certain objects that implement some task T .

Identities Each process p i has an identity denoted id i that is kept in input i . An identity is an integer value in [1..N ], where N > n.

(two identities can be compared with <, = and >). We assume that in every initial configuration of the system, the identities are distinct: i = j ⇒ input i = input j .

A process does not know the identity of the other processes. More precisely, every input configuration where identities are distinct and in [1..N ] is possible. Thus, processes "know" n, N and the fact that no two processes have the same identity.

Index-independent algorithm

We say that an algorithm A is index-independent if the following holds for every run r and every permutation π() of the process indexes. Let r π be the run obtained from r by permuting the input values according to π() and, for each step, the index i of the process that executes the step is replaced by π(i). Then r π is a run of A.

Let a permutation π() such that π(i) = j. The index-independence ensures that p j behaves in r π exactly as p i behaves in r: it decides the same thing in the same step. Let us observe that in an index-independent algorithm, output i = v in run r, then output π(i) = v in run r π . This formalizes the fact that indexes are only an addressing mechanism: the output of a process does not depend on indexes, it depends only on the inputs (ids) and on the interleaving.

Comparison-based algorithm Intuitively, an algorithm A is comparison-based if processes use only comparisons (<, =, >) on their inputs. More formally, let us consider the ordered inputs i 1 < i 2 < • • • < i n of a run r of A and any other ordered inputs j 1 < j 2 < • • • < j n . The algorithm A is comparison-based if the run r ′ obtained by replacing in r each i ℓ by j ℓ , 1 ≤ ℓ ≤ n (in the corresponding process), is a run of A. Notice that each process decides the same output in both runs, and at the same step.

Tasks

Task A one-shot decision problem is specified by a task (I, O, ∆), that consists of a finite set of input vectors I, a set of output vectors O, and a relation ∆ that associates with each I ∈ I at least one O ∈ O (e.g. see Section 2.1 of [START_REF] Herlihy | The Topological Structure of Asynchronous Computability[END_REF]). All vectors are n-dimensional.

Solving a task An algorithm A solves a task T if the following holds: each process p i starts with an input value (stored in a local variable input i ) and each non-faulty process eventually decides on an output value by writing it to a local write-once register output i . The input vector I ∈ I is such that I[i] = input i and we say "p i proposes I[i]" in the considered run. Moreover, the decided vector J is such that (1) J ∈ ∆(I), and (2) for each process p i that decides we have J

[i] = output i .
The (n, k)-set agreement (SA) task Each process p i is assumed to propose a value and each correct process has to decide a value such that the following properties are satisfied.

• Termination. Each process decides a value.

• Validity. A decided value is a proposed value.

• Agreement. At most k different values are decided.

The (n, k)-test and set (T&S) task Each process p i is required to decide a value such that the following properties are satisfied. (The instance k = 1 does correspond to the usual Test&set object.)

• Termination. Each process decides a value.

• Validity. Each process decides 0 (winer) or 1 (looser).

• Agreement. At least one and at most k processes decide the value 0.

The n, m, ℓ, u -GSB tasks Each process starts with a distinct identity from a set [1..N ]. Each correct process has to decide a value such that the following properties are satisfied.

• Termination. Each correct process decides a value.

• Validity. A decided value belongs to [1..m]. • Symmetric agreement. Each value v ∈ [1.
.m] is decided by at least ℓ and at most u processes, in executions where all decide.

We consider only feasible tasks, i.e., tasks for with ∆(I) = ∅. It is easy to see that m × ℓ ≤ n ≤ m × u is a necessary and sufficient condition for the n, m, ℓ, u -GSB task to be feasible. The structure, complexity and computability issues of the universe of n, m, ℓ, u -GSB tasks is investigated in [START_REF] Imbs | The Universe of Symmetry Breaking Tasks[END_REF].

As already indicated, the n, m, 0, 1 -GSB task is the (non-adaptive) m-renaming problem while the new n, k, 1, nk + 1 -GSB task (which we call k-slot task) is a generalization of the WSB (weak symmetry breaking) task (which is the n, 2, 1, n -1 -GSB task). Other new GSB tasks are described in [START_REF] Imbs | The Universe of Symmetry Breaking Tasks[END_REF].

Notation 1 Let T and T ′ be two tasks. T → T ′ means that there is an algorithm that solves task T ′ in the read/write wait-free model enriched with objects that solve task T . T ↔ T ′ is a shortcut for T → T ′ ∧ T ′ → T (T and T ′ are equivalent). T T ′ means that there is no algorithm that solves task T ′ in the read/write wait-free model enriched (only) with objects that solve task T .

An iterated model

Attempts at unifying different read/write distributed computing models have restricted their attention to a subset of round-based executions. The approach introduced in [START_REF] Borowsky | A Simple Algorithmically Reasoned Characterization of Wait-Free Computations (Extended Abstract)[END_REF] generalizes these attempts by proposing an iterated model in which processes execute an infinite sequence of rounds, and in each round communicate through a specific object that provides processes with a single operation denoted write snapshot().

One-shot write-snapshot object When invoked by a process p i , the semantics of the write snapshot() operation consists of executing a write, and immediately a snapshot operation. More precisely, it is defined by the following properties, where v i is the value written by p i and sm i , the value (or view) it gets back from the operation. A view sm i is a set of pairs (id k , v k ), where v k is the value written by p k in the object. (Let sm i = ∅ if the process p i never invokes write snapshot().) These properties are:

• Self-inclusion. ∀i : (id i , v i ) ∈ sm i . • Containment. ∀i, j : sm i ⊆ sm j ∨ sm j ⊆ sm i . • Immediacy. ∀i, j : [(id i , v i ) ∈ sm j ∧ (id j , v j ) ∈ sm i ] ⇒ (sm i = sm j ).
• Termination. Any invocation of WS .write snapshot() by a correct process terminates. The iterated model In the iterated model (IM) the shared memory is made up of an infinite number of one-shot write-snapshot objects WS [START_REF] Attiya | Renaming in Asynchronous Environment[END_REF], WS [START_REF] Attiya | The Combinatorial Structure of Wait-Free Solvable Tasks[END_REF], . . . These objects are accessed sequentially and asynchronously by each process, according to the classical round-based pattern described in Figure 2, where r i denotes the current round number of process p i . Although the IM restricts the order in which processes can access the shared objects, there is no limitation in terms of task solvability [START_REF] Borowsky | A Simple Algorithmically Reasoned Characterization of Wait-Free Computations (Extended Abstract)[END_REF], even when the IM is enriched with certain objects more powerful than read/write registers [START_REF] Gafni | Distributed Programming with Tasks[END_REF].

r i ← 0; loop forever r i ← r i + 1; local computations; compute v i ; sm i ← WS [r i ].write snapshot(v i ); local computations end loop.
When the IM is enriched with objects of type X, the system additionally has an infinite number of objects of type X, X [1], X [2], . . ., which are accessed sequentially but asynchronously. Therefore, in round r, each process access WR[r] and X [r]. Section 3.4 considers the IM enriched with GSB objects, more specifically perfect renaming and (n + 1)-renaming objects.

3 From GSB tasks to (n, k)-set agreement

Two preliminary results

This section presents two results that will be used in Sections 3.2 and 3.4 for proving impossibility results from perfect renaming to set agreement.

Lemma 1 uses an idea that is recurrent in the rest of the paper: given an algorithm A for n processes that solves a task from a certain class of objects, one can slightly modify A to achieve an algorithm B, possibly for less than n processes, that solves the same task from a distinct class of objects.

Lemma 1 For 1 ≤ k ≤ n : n + 1, n + 1, 1, 1 -GSB → (n + 1, k)-SA ⇒ n, n + 1, 0, 1 -GSB → (n, k)-SA .
Proof Let A be an algorithm that solves (n + 1, k)-SA from n + 1, n + 1, 1, 1 -GSB. Consider the set of executions S of A in which only p 1 , . . . , p n participate. Observe that for any execution E of S, the collection of outputs that p 1 , . . . , p n receive in any invocation to an n + 1, n + 1, 1, 1 -GSB object, are valid outputs for n, n + 1, 0, 1 -GSB. We get a new algorithm B by modifying p i 's code, 1 ≤ i ≤ n, as follows (p n+1 does not change). Each n + 1, n + 1, 1, 1 -GSB object of A is replaced by an n, n + 1, 0, 1 -GSB object. Observe that for any execution E of B with participating set p 1 , . . . , p n , there is an execution in S that is the same as E. Moreover, notice that p 1 , . . . , p n decide at most k distinct values in E. Therefore, suppressing p n+1 from B, we obtain an algorithm B ′ for n processes that solves (n, k)-SA from n, n + 1, 0, 1 -GSB.

✷ Lemma 1

The following lemma is in some sense the opposite of Lemma 1. Roughly speaking, it says that given an impossibility result for (n -1)-slot, i.e., n, n -1, 1, n -GSB, one can obtain an impossibility result for perfect renaming on n ′ ≥ n processes.

Lemma 2 For 1 ≤ k ≤ n -1 : n, n -1, 1, n -GSB (n, k)-SA ⇒ ∀n ′ ≥ n + 1 : n ′ , n ′ , 1, 1 -GSB (n ′ , k)-SA .
Proof First, it is proved in [START_REF] Imbs | The Universe of Symmetry Breaking Tasks[END_REF] that (n -1)-slot on n processes can implement (n + 1)-renaming on n-processes, that is

n, n -1, 1, n -GSB → n, n + 1, 0, 1 -GSB. (1)
By [START_REF] Attiya | Renaming in Asynchronous Environment[END_REF] and since by hypothesis n, n -1, 1, n -GSB (n, k)-SA, we get

n, n + 1, 0, 1 -GSB (n, k)-SA. (2)
Also Lemma 1 and (2) imply

n + 1, n + 1, 1, 1 -GSB (n + 1, k)-SA. (3)
Now, in [START_REF] Imbs | The Universe of Symmetry Breaking Tasks[END_REF] it is proved that perfect renaming on n + 1 processes can implement any GSB task on n + 1 processes, thus n + 1, n + 1, 1, 1 -GSB → n + 1, n + 2, 0, 1 -GSB, and hence by ( 3)

n + 1, n + 2, 0, 1 -GSB (n + 1, k)-SA. ( 4
)
Collection des Publications Internes de l'Irisa c IRISA Therefore, by ( 4) and Lemma 1 on n + 2 processes we get

n + 2, n + 2, 1, 1 -GSB (n + 2, k)-SA. (5)
Let us repeat the same reasoning for n + 2. Let us observe that n + 2, n + 2, 1, 1 -GSB → n + 2, n + 3, 0, 1 -GSB (proved in [START_REF] Imbs | The Universe of Symmetry Breaking Tasks[END_REF]). Hence, from this observation and (5) we have

n + 2, n + 3, 0, 1 -GSB (n + 2, k)-SA. (6)
Thus, by [START_REF] Castañeda | An Equivariance Theorem with Applications to Renaming[END_REF] and Lemma 1 on n + 3 processes

n + 2, n + 2, 1, 1 -GSB (n + 2, k)-SA. (7)
Repeating the same for n + 3, n + 4, etc., the lemma follows.

✷ Lemma 2

From perfect renaming to set agreement

This section shows a possibility and two impossibility results from perfect renaming to set agreement. The possibility result, Theorem 1, relies on the following lemma.

Lemma 3 For n = 2 : n, n, 1, 1 -GSB → (n, 1)-T&S.

Proof Consider an object O that solves 2, 2, 1, 1 -GSB. By Theorem 2 of [START_REF] Imbs | The Universe of Symmetry Breaking Tasks[END_REF], we can assume that O is comparison-based. Consider an i ∈ {1, 2} and let E be an execution of O in which only p i participates (solo execution). It follows from the fact that O is comparisonbased that p i cannot use its input name in E. Consequently, the output name of p i in this execution is not a function of its input name. Therefore in every solo execution, no matter its input name, p i always decides the same output name, say v. Now, as p i decides v in a solo execution and O is index-independent, we can conclude that in any solo execution in which p j participates (j ∈ {1, 2} and j = i), whatever its input name, p j decides also v. Hence, the output name decided in a solo execution of O is predetermined. Let v be this output name.

We claim that we can solve (2, 1)-T&S from O: each process calls O with its input name as input and decides 0 (winner) if it receives v (the value that O always outputs in a solo execution), otherwise it decides 1 (loser). The correctness proof of this implementation is the following. In a solo execution the participating processes obtains v from O, and hence decides 0 (winner). In an execution in which the two processes of the system participate, exactly one of them obtain v from O, by the specification of 2, 2, 1, 1 -GSB, and thus exactly one process decides 0 (winner) and exactly one process decides 1 (looser). The lemma follows.

✷ Lemma 3

Theorem 1 For n = 2 : n, n, 1, 1 -GSB → (n, 1)-SA.

Proof By Lemma 3, 2, 2, 1, 1 -GSB → (2, 1)-T&S. Also it is known that (2, 1)-T&S → (2, 1)-SA [START_REF] Herlihy | Wait-Free Synchronization[END_REF], and hence 2, 2, 1, 1 -GSB → (2, 1)-SA. ✷ Theorem 1

Roughly speaking, the proofs of following two theorems consist on showing that n, n -1, 1, n -GSB (n, k)-SA for a small value of n, and then apply Lemma 2.

Theorem 2 ∀n ≥ 3 : n, n, 1, 1 -GSB (n, 1)-SA.
Proof Consider the task 2, 1, 1, 2 -GSB. Obviously 2, 1, 1, 2 -GSB is read/write wait-free solvable and hence 2, 1, 1, 2 -GSB (2, 1)-SA, as (2, 1)-SA is not read/write solvable [START_REF] Fischer | Impossibility of Distributed Consensus with One Faulty Process[END_REF]. Therefore, by Lemma 2, ∀n ≥ 3, n, n, 1, 1 -GSB (n, 1)-SA. ✷ Theorem 2

Theorem 3 ∀n ≥ 4 : n, n, 1, 1 -GSB (n, 2)-SA.

Proof Observe that 3, 2, 1, 3 -GSB is WSB on 3 processes, hence equal to (2n -2)-renaming on 3 processes, by Corollary 2 of [START_REF] Gafni | Subconsensus Tasks: Renaming is Weaker Than Set Agreement[END_REF]. Also in [START_REF] Gafni | Subconsensus Tasks: Renaming is Weaker Than Set Agreement[END_REF] it is proved that (n, n -1)-SA is strictly stronger than (2n -2)-renaming for odd n, hence 3, 2, 1, 3 -GSB (3, 2)-SA. Therefore, by Lemma 2, ∀n ≥ 4, n, n, 1, 1 -GSB (n, 2)-SA. ✷ Theorem 3

From (2n -2)-renaming to set agreement

As mentioned in the Introduction, it is proved in [START_REF] Gafni | Subconsensus Tasks: Renaming is Weaker Than Set Agreement[END_REF] that n, 2n -2, 0, 1 -GSB (n, n-1)-SA, for odd n (recall that n, 2n -2, 0, 1 -GSB is (2n -2)-renaming on n processes). Note that for k = n -1, n, 2n -2, 0, 1 -GSB is n, 2n -⌈ n k ⌉, 0, 1 -GSB. Now, it is proved in [START_REF] Castañeda | New Combinatorial Topology Upper and Lower Bounds for Renaming[END_REF] that if gcd( n 1 , . . . , n n-1 ) = 1 (and only in this case), then n, 2n -2, 0, 1 -GSB is read/write wait-free solvable. Thus, for these values of n, n, 2n -2, 0, 1 -GSB (n, n -1)-SA, since it has been proved [START_REF] Borowsky | Generalized FLP Impossibility Result for t-Resilient Asynchronous Computations[END_REF][START_REF] Herlihy | The Topological Structure of Asynchronous Computability[END_REF][START_REF] Saks | Wait-Free k-Set Agreement Is Impossible: The Topology of Public Knowledge[END_REF] that (n, n -1)-SA is not read/write wait-free solvable. There are odd and even values of n holding this property. What does it happen when n is even and gcd( n 1 , . . . , n n-1 ) = 1? It is observed in [START_REF] Castañeda | An Equivariance Theorem with Applications to Renaming[END_REF] that if gcd( n 1 , . . . , n n-1 ) = 1 then n is a prime power. The only case in which n is prime power and even is n = 2 x , x ≥ 1. However, for the case n = 2, n, 2n -2, 0, 1 -GSB is equivalent to perfect renaming, and hence cannot implement (n, n -1)-SA, by Theorem 2. All these results partially answer the question left open in [START_REF] Gafni | Subconsensus Tasks: Renaming is Weaker Than Set Agreement[END_REF]. Observe that the result in [START_REF] Gafni | Subconsensus Tasks: Renaming is Weaker Than Set Agreement[END_REF] is extended for infinitely many values of n.

Theorem 4 For n = 2, n, 2n -2, 0, 1 -GSB ↔ (n, n -1)-SA, ∀n, (n, n -1)-SA → n, 2n -2, 0, 1 -GSB, and ∀n = 2 x , x > 1, n, 2n -2, 0, 1 -GSB (n, n -1)-SA.

Theorem 5 below shows that for any n, n, 2n -2, 0, 1 -GSB is not strong enough for solving (n, n -2)-SA. Of course all cases n = 2 x , x > 1, are implied by Theorem 4, however, the proof of Theorem 5 is simple (uses the same idea as the one used in the proof of Lemma 1) and self-contained.

Lemma 4 ∀n: n, 2n -2, 0, 1 -GSB → (n, n -2)-SA ⇒ n -1, 2n -2, 0, 1 -GSB → (n -1, n -2)-SA .
Proof Let A be an algorithm that solves (n, n -2)-SA from n, 2n -2, 0, 1 -GSB. Consider the set of executions S of A in which only p 1 , . . . , p n-1 participate. Observe that for any execution E of S, the collection of outputs that p 1 , . . . , p n-1 receive in any invocation to an n, 2n -2, 0, 1 -GSB object, are valid outputs for n -1, 2n -2, 0, 1 -GSB. We get a new algorithm B by modifying p i 's code, 1 ≤ i ≤ n -1, as follows. Each n, 2n -2, 0, 1 -GSB object of A is replaced by an n -1, 2n -2, 0, 1 -GSB object. Observe that for any execution E of B with participating set p 1 , . . . , p n-1 , there is an execution in S that is the same as E. Moreover, at most n -2 distinct values are decided in E. Therefore, suppressing p n from B, we obtain an algorithm B ′ for n -1 processes that solves

(n -1, n -2)-SA from n -1, 2n -2, 0, 1 -GSB. ✷ Lemma 4
Theorem 5 ∀n, n, 2n -2, 0, 1 -GSB (n, n -2)-SA.

Proof Suppose, for the sake of contradiction, that n, 2n -2, 0, 1 -GSB → (n, n -2)-SA. Hence, n -1, 2n -2, 0, 1 -GSB → (n -1, n -2)-SA, by Lemma 4. In [START_REF] Attiya | Renaming in Asynchronous Environment[END_REF] it is proved that M -renaming on n -1 processes, i.e., n -1, M, 0, 1 -GSB, is read/write wait-free solvable if M ≥ 2(n -1) -1 = 2n -3. Therefore, n -1, 2n -2, 0, 1 -GSB is read/write wait-free solvable, from which follows that (n -1, n -2)-SA is read/write wait-free solvable, since n -1, 2n -2, 0, 1 -GSB → (n -1, n -2)-SA. However, it has been proved that (n -1, n -2)-SA is not read/write wait-free solvable [START_REF] Borowsky | Generalized FLP Impossibility Result for t-Resilient Asynchronous Computations[END_REF][START_REF] Herlihy | The Topological Structure of Asynchronous Computability[END_REF][START_REF] Saks | Wait-Free k-Set Agreement Is Impossible: The Topology of Public Knowledge[END_REF]. A contradiction. ✷ Theorem 5

From perfect renaming to set agreement in the iterated model

This section proves Theorem 7 below, which states that in IM, n, n, 1, 1 -GSB (n, n -2)-SA. For the rest of the section we only consider IM. The strategy of the proof is the following.

1. Given the task n, n + 1, 0, 1 -GSB, we define a new n-process task T such that if n, n + 1, 0, 1 -GSB → (n, n -1)-SA, then T → (n, n -1)-SA.

2. Using a result in [START_REF] Gafni | Subconsensus Tasks: Renaming is Weaker Than Set Agreement[END_REF], we will prove that T (n, n -1)-SA, hence n, n + 1, 0, 1 -GSB (n, n -1)-SA, by the previous item.

3. Finally, the fact that n, n + 1, 0, 1 -GSB (n, n -1)-SA and a simple observation that Lemma 1 holds in IM, implies that n + 1, n + 1, 1, 1 -GSB (n + 1, n -1)-SA, from which follows the desired result.

For proving Theorem 7, we model tasks using notions from combinatorial topology as in many papers (see for example [START_REF] Attiya | The Combinatorial Structure of Wait-Free Solvable Tasks[END_REF][START_REF] Borowsky | Generalized FLP Impossibility Result for t-Resilient Asynchronous Computations[END_REF][START_REF] Gafni | Subconsensus Tasks: Renaming is Weaker Than Set Agreement[END_REF][START_REF] Herlihy | The Topological Structure of Asynchronous Computability[END_REF][START_REF] Saks | Wait-Free k-Set Agreement Is Impossible: The Topology of Public Knowledge[END_REF]). We review some basic concepts.

A simplex σ is a finite set. The elements of a simplex are its vertexes. The dimension of a simplex σ is the number of its vertexes minus 1. If σ has n + 1 vertexes then it is called an n-simplex. A simplex τ is a face of σ if τ is a subset of σ. If τ is not equal to σ then τ is a proper face of σ. A complex K is a set of simplexes, closed under containment. The dimension of a complex K is the maximum dimension of its simplexes. A complex K of dimension n is an n-complex. For a simplex σ, we often denote as σ the complex containing all faces of σ (including σ itself). A complex L is a subcomplex of the complex K if L ⊆ K.

An n-complex is connected if any two n-simplexes can be joined by a sequence of n-simplexes in which each pair of neighboring simplexes share an (n -1)-face. An n-complex K is an n-manifold (sometimes called pseudo-manifold) if it is connected and each of its (n -1)-simplexes is contained in one or two n-simplexes. We say that an (n -1)-simplex of K is internal if it is contained in two n-simplexes, otherwise it is external. The boundary of an n-manifold K, denoted ∂K, is the subcomplex induced by its external (n -1)-simplexes. For example, the complex induced by an n-simplex σ and all its faces is a n-manifold with boundary; its boundary ∂σ contains all (n -1)-faces of σ.

For a domain of inputs I, the input complex I is an (n -1)-complex that contains (n -1)-simplexes (subsets with n elements) of {1, . . . , n} × I, and all their faces, such that no pair of vertexes have the same index, the first entry of each pair. An output complex, O, over a domain of outputs O, is defined similarly. The meaning of a vertex (i, v) of I (resp. O) is that process with index i has input (resp. output) v.

A task is defined as a triple I, O, △ , where I is an input complex, O is an output complex and △ is a recursive map carrying each m-simplex σ of I, 0 ≤ m ≤ n -1, to a non-empty m-subcomplex of O. This definition has the following operational interpretation: △(σ) is the set of legal final states in executions where only the m + 1 processes in σ participate (the rest fail without taking any steps).

The concept of manifold task is introduced in [START_REF] Gafni | Subconsensus Tasks: Renaming is Weaker Than Set Agreement[END_REF]. It is proved there that manifold tasks are too weak to solve (n, n -1)-SA. Manifold tasks are used in [START_REF] Gafni | Subconsensus Tasks: Renaming is Weaker Than Set Agreement[END_REF] for proving that in IM, for odd n, n, 2n -2, 0, 1 is strictly weaker than (n, n -1)-SA (the result is extended for the general model in [START_REF] Gafni | Distributed Programming with Tasks[END_REF]).

Definition 1 ([17])

A task I, O, △ is a manifold task if for every m-simplex σ ∈ I, 0 ≤ m ≤ n -1, △(σ) is a m-manifold and ∂△(σ) = △(∂σ).
Lemma 5 ([17]) No manifold task can solve (n, n -1)-SA.

We are interested in the task n, n + 1, 0, 1 -GSB. This task is modeled as I R , O R , △ R , where:

• The domain of inputs is {1, . . . , N } and no pair of vertexes of a simplex in I R have the same input value.

• The outputs are {1, . . . , n + 1} and no pair of vertices of a simplex in O R have the same output value.

• For each m-simplex σ ∈ I R , △ R (σ) is the m-subcomplex of O R containing every m-simplex that has the same indexes at its vertexes as σ. Therefore, for each

(n -1)-simplex σ ∈ I R , △ R (σ) = O R .
Using I R , O R , △ R we define a task T , whose main properties are that (1) it solves (n, k)-SA, provided that I R , O R , △ R solves (n, k)-SA, and (2) it is a manifold task. The task T is defined as I T , O T , △ T , with I T = I R , O T = O R , and △ T is defined as follows:

• For 0 ≤ m ≤ n -2, for each m-simplex σ of I, △ T (σ) is the complex induced by the m-face of τ that has the same indexes at its vertexes as σ.

• For m = n -1, for or each (n -1)-simplex σ of I, △ T (σ) = O T \ τ , where τ is the (n -1)-simplex {(1, 1), . . . , (n, n)} of O I . Figure 3 depicts an example of complex O T \ τ of dimension 2. The proof of Lemma 6 uses a similar idea than the one used in the proof of Lemma 1.

P 1 R 3 Q 1 P 3 R 1 Q 3 P 1 R 4 P 2 Q 4 R 2 P 4 Q 2 R 4 P 2 Q 4 R 3 P 1 Q 1 P 3 R 1 Q 3 P 1 λ λ ′
Lemma 6 For 1 ≤ k ≤ n -1 : I R , O R , △ R → (n, k)-SA ⇒ I T , O T , △ T → (n, k)-SA . Proof First, recall that I R = I T and O R = O T . It is not hard to see that by the definition of I R , O R , △ R and I T , O T , △ T , for every m-simplex σ ∈ I R , △ T (σ) ⊂ △ R (σ), (8)
for each 0 ≤ m ≤ n -1. Therefore, any valid collection of outputs for

I T , O T , △ T is a valid collection of outputs for I R , O R , △ R .
Collection des Publications Internes de l'Irisa c IRISA Now, let A be an algorithm that solves (n, k)-SA from I R , O R , △ R . We get a new algorithm B by modifying p i 's code, 1 ≤ i ≤ n, as follows. Each I R , O R , △ R object in A is replaced by an I T , O T , △ T object. As explained above, [START_REF] Castañeda | The Renaming Problem in Shared Memory Systems: an Introduction[END_REF] says that any valid collection of outputs for I T , O T , △ T is a valid collection of outputs for I R , O R , △ R . Therefore, for each execution E of B, there is an execution of A that is the same as E, thus the participating processes of E decide at most k distinct values, i.e., I T , O T , △ T → (n, k)-SA.

✷ Lemma 6

Lemma 7 The task I T , O T , △ T is a manifold task.

Proof Let τ denote the (n -1)-simplex {(1, 1), . . . , (n, n)} of O T . First, for each 0 ≤ m ≤ n -2, for every m-simplex σ ∈ I T , △ T (σ) = τ ′ , where τ ′ is the m-face of τ that has the same indexes at its vertexes as σ. Clearly △ T (σ) is an m-manifold with ∂△ T (σ) = ∂τ ′ = △(∂σ). Now consider an (n -1)-simplex σ ∈ I T . We have that △ T (σ) = O T \ τ . We will first prove that O T is an (n -1)-manifold without boundary, and then show that this implies that O T \ τ is a (n -1)-manifold (with boundary) and ∂△ T (σ) = △(∂σ).

For proving that O T is an (n -1)-manifold without boundary, we prove the two following claims: (C1) Each (n -2)-simplex of O T is contained in exactly two (n -1)-simplexes, and (C2) O T is connected. Let us first prove claim C1. Consider an (n -2)-simplex λ of O T . By definition of O T , λ has the form {(i 1 , nm 1 ), . . . , (i n-1 , nm n-1 )}, where for all 1 ≤ j 1 = j 2 , k 1 = k 2 ≤ n -1, we have i j1 = i j2 and nm k1 = nm k2 . Note that there is exactly one index process in {1, . . . , n} that does not appear in λ, and similarly there are exactly two output names in {1, . . . , n + 1} that do not appear in λ. Let j be such index and k 1 and k 2 be such output names. By definition of O T , (n -1)-simplexes γ 1 = λ ∪ {(j, k 1 )} and γ 2 = λ ∪ {(j, k 2 )} belong to O T . Moreover, clearly λ is contained in γ 1 and γ 1 , and also there is no other (n -1)-simplex of O T containing λ because O T is defined over the output space {1, . . . , n + 1}.

Let us now prove claim C2, namely, O T is connected. Given two (n -1)-simplexes λ, λ ′ ∈ O T , the sequential algorithm findSequence() in Figure 4 outputs a sequence S of (n -1)-simplexes of O T such that each pair of neighboring simplexes share an (n -2)-face, and the first and last simplexes are λ and λ ′ . Without loss of generality, the algorithm assumes that λ and λ ′ have the form {(i 1 , nm i ), . . . , (i n , nm n )} and {(i 1 , nm ′ i ), . . . , (i n , nm ′ n )}, respectively. Algorithm findSequence() uses the following notation. Let γ be an (n -1) simplex of O T . Consider an index i ∈ {1, . . . , n} and let (j, x) be the vertex of γ such that i = j. The (n -2)face γ -{(j, x)} of γ is denoted as γ|i. This notation is used in lines 05 and 10 of findSequence(). Consider and an output name y ∈ {1, . . . , n + 1} such that there is no (j, x) ∈ γ such that y = x. The (n -2)-face γ -{(j, x)} of γ is denoted as γ|x. This notation is used in line 09 of findSequence(). The dot (•) operator in lines 06, 11 and 14 means concatenation. Figure 3 contains an example of a path produced by findSequence().

For the j-th iteration of the loop in line 02, 1 ≤ j ≤ n, let γ j be the last simplex of the sequence S at the beginning of the iteration. An invariant (I) of findSequence() is that at the beginning of the j-th iteration, S is a sequence of (n -1)-simplexes of O T such that each pair of neighboring simplexes share an (n -2)-face, and also for every vertex

(i, x) ∈ γ j , if i = i k for some 1 ≤ k ≤ j -1, then x = nm ′ k (recall that λ = {(i 1 , nm i ), . . . , (i n , nm n )} and λ ′ = {(i 1 , nm ′ i ), . . . , (i n , nm ′ n )}).
Observe that invariant (I) implies that, at line 14, the last simplex γ of S shares an (n -2)-face with λ ′ . In particular, γ and λ ′ share γ|i n ; in fact it can be that γ = λ ′ . Therefore, S • λ ′ in line 14 is the desired sequence of simplexes. Figure 3 contains an example of a path produced by findSequence().

By induction we prove invariant (I). For j = 1, it clearly holds, since S = λ. Suppose that (I) holds for 1 ≤ j ≤ n -1; we will prove it holds for j + 1. Consider the simplex γ in line 03 in the j-th iteration of findSequence(). By assumption, for every vertex

(i, x) ∈ γ, if i = i k for some 1 ≤ k ≤ j -1, then x = nm ′ k .
We have two cases. If nm ′ j does not appear in γ, i.e., line 04 is false, then γ ′ in line 05 and γ share the (n -2)-face γ|i j , since γ ′ = γ|i j ∪ (i j , nm ′ j ) . Moreover, observe that for every vertex

(i, x) ∈ γ ′ , if i = i k for some 1 ≤ k ≤ j, then x = nm ′ k .
In addition, γ ′ ∈ O T because, by induction hypothesis, γ|i j ∈ O T and nm ′ ∈ {1, . . . , n + 1}. Therefore, invariant (I) holds for j + 1.

In the second case we have that nm ′ j indeed appears in γ, that is line 04 is true. Thus γ ′ in line 09 and γ share the (n -2)-face γ|nm ′ j , because γ ′ = γ|nm ′ j ∪{(i, x)}. Also, γ ′ ∈ O T , by the definition of i and x, and because γ|nm ′ j ∈ O T , by induction hypothesis. Moreover, since for all

1 ≤ k 1 = k 2 ≤ n, nm ′ k1 = nm ′ k2 , it cannot be that i = i k , for some 1 ≤ k ≤ j -1, which implies that for every vertex (ℓ, x) ∈ γ ′ , if ℓ = i k for some 1 ≤ k ≤ j -1, then x = nm ′ k .
Observe that we now have the same situation as in the previous case, considering the sequence S • γ ′ , thus the same argument used for proving that case shows that γ ′ and γ ′′ in line 10 share an (n -2)-face, and for every vertex (ℓ, x) ∈ γ ′′ , if ℓ = i k for some 1 ≤ k ≤ j, then x = nm ′ k . Invariant (I) holds for j + 1. Until here we have proved that O T is a manifold without boundary. We now prove that O T \τ is a manifold with boundary, where τ is the (n -1)-simplex {(1, 1), . . . , (n, n)} of O T . Moreover, we prove that ∂(O T \ τ ) = ∂τ . The fact that O T \ τ is connected comes from the observation that the correctness of algorithm findSequence() does not depend at all on the order i 1 , . . . , i n of the index processes (recall that, for findSequence(), λ = {(i 1 , nm i ), . . . , (i n , nm n )} and λ ′ = {(i 1 , nm ′ i ), . . . , (i n , nm ′ n )}). Thus, if during the execution of findSequence(), appears τ in the sequence S in some iteration, say in the j-th iteration, it is enough to restart the execution with λ = {(i 1 , nm i ), . . . , (i j+1 , nm j+1 ), (i j , nm j ), . . . , (i n , nm n )} and λ = (i 1 , nm ′ i ), . . . , (i j+1 , nm ′ j+1 ), (i j , nm ′ j ), . . . , (i n , nm ′ n ) , i.e., swapping i j with i j+1 . This "evades" the simplex τ . Now, because O T is a manifold without boundary, each (n -2)-simplex of O T \ τ is contained in one or two (n -1)-simplexes. Moreover, it is not hard to see that an (n -2)-simplex of O T \ τ is contained in exactly one (n -1)-simplex if and only if it is face of τ , namely, it belongs to ∂τ . Thus, O T \ τ is a manifold with ∂(O T \ τ ) = ∂τ . We now are ready to prove the main results of this section.

Theorem 6 In IM, ∀n : n, n + 1, 0, 1 -GSB (n, n -1)-SA.

Proof By Lemmas 5 and 7, we get I T , O T , △ T (n, n -1)-SA, and by Lemma 6,

I R , O R , △ R (n, n -1)-SA. Thus n, n + 1, 0, 1 -GSB (n, n -1)-SA, since n, n + 1, 0, 1 -GSB is I R , O R , △ R . ✷ Theorem 6
Theorem 7 In IM, ∀n : n, n, 1, 1 -GSB (n, n -2)-SA.

Proof It is straightforward to see that Lemma 1 holds in IM; the proof is essentially the same. Now, by Theorem 6 we have that ∀n : n, n + 1, 0, 1 -GSB (n, n -1)-SA, and from Lemma 1 with k = n -2, it follows that ∀n : n + 1, n + 1, 0, 1 -GSB (n + 1, n -1)-SA. Therefore, in the end we get ∀n : n, n, 1, 1 -GSB (n, n -2)-SA. ✷ Theorem 7

4 From (n, k)-set agreement to GSB 4.1 From set agreement to perfect renaming Lemma 8 uses the same idea as the one used in Lemma 1 in Section 3.1. Theorems 8 and 9 below are proved using Lemma 8.

Lemma 8 For 1 ≤ k ≤ n -1 : (n, k)-SA → n, n, 1, 1 -GSB ⇒ k, n, 0, 1 -GSB is read/write wait-free solvable .
Proof Let A be an algorithm that implements n, n, 1, 1 -GSB from (n, k)-SA. Consider the set of executions S of A in which only p 1 , . . . , p k participate. Observe that for any execution E of S, the outputs of p 1 , . . . , p k in E are valid outputs for k, n, 0, 1 -GSB. Note that S contains a set S ′ of executions in which each invocation by p i , 1 ≤ i ≤ k, to any (n, k)-SA object outputs the value p i uses as input.

Let B be the algorithm obtained by modifying p i 's code in A, 1 ≤ i ≤ k, as follows (the codes of p k+1 until p n are not modified). Each invocation to an (n, k)-SA object is replaced by a function that just outputs the input it receives. For any execution E of B with participating set p 1 , . . . , p k , there is an execution in S ′ that is the same as E. Then, suppressing the processes p k+1 , . . . , p n from B, we obtain an algorithm B ′ for k processes that read/write solves k, n, 0, 1 -GSB.

✷ Lemma 8

Theorem 8 ∀n > 2: (n, n -1)-SA n, n, 1, 1 -GSB.

Proof Suppose, for the sake of contradiction, that (n, n -1)-SA → n, n, 1, 1 -GSB. It then follows from Lemma 8 with k = n -1 that n -1, n, 0, 1 -GSB is read/write wait-free solvable. However, it is proved in [START_REF] Attiya | Renaming in Asynchronous Environment[END_REF] that n -1, n, 0, 1 -GSB (n-renaming on n -1 processes) is not read/write wait-free solvable for any value of n. A contradiction.

✷ Theorem 8 Theorem 9 For n, k : k ≥ ⌈ n 2 ⌉ + 1 ∧ gcd( k 1 , . . . , k k-1 ) = 1 ⇒ (n, k)-SA n, n, 1, 1 -GSB .
Proof Suppose, for the sake of contradiction, that (n, k)-SA → n, n, 1, 1 -GSB. It follows from Lemma 8 that k, n, 0, 1 -GSB is read/write wait-free solvable. Let us now observe that, as 2k-2 ≥ n+(n mod 2), it follows that k, n, 0, 1 -GSB → k, 2k -2, 0, 1 -GSB. Moreover, it is proved in [START_REF] Castañeda | New Combinatorial Topology Upper and Lower Bounds for Renaming[END_REF] that k, 2k -2, 0, 1 -GSB is not read/write solvable if gcd( k 1 , . . . , k k-1 ) = 1, from which the lemma follows.

✷ Theorem 9

This section ends with the following simple result.

Theorem 10 ∀n : (n, 1)-SA → n, n, 1, 1 -GSB.

Proof The algorithm is very simple. The processes have an n-array A of (n, 1)-SA objects. It is proved in [START_REF] Gafni | Renaming with k-set Consensus: an Optimal Algorithm in n + k -1 Slots[END_REF] that (n + k -1)-renaming can be solved from (n, k)-set agreement, thus:

Theorem 11 ∀n, k : (n, k)-SA → n, n + k -1, 0, 1 -GSB.
An algorithm is presented in [START_REF] Mostéfaoui | Exploring Gafni's Reduction Land: from Ω k to Wait-free adaptive (2p -⌈ p k ⌉)-renaming via k-set Agreement[END_REF] that solves n-process adaptive (2p -⌈ p k ⌉)-renaming from (n, k)-SA. This algorithm implies the following.

Theorem 12 ∀n, k : (n, k)-SA → n, 2n -⌈ n k ⌉, 0, 1 -GSB.
In what follows we prove that (n, k)-SA → n, ⌈ n k ⌉, 1, n -GSB. Since (n, k)-SA solves (n, k)-participating set [START_REF] Mostéfaoui | Exploring Gafni's Reduction Land: from Ω k to Wait-free adaptive (2p -⌈ p k ⌉)-renaming via k-set Agreement[END_REF], it is enough to prove that (n, k)-participating set solves n, ⌈ n k ⌉, 1, n -GSB. The (n, k)-participating set (PS) task is the one-shot write snapshot task (defined by self-inclusion, containment, immediacy and termination properties stated in Section 2.3) plus the following property (at most k processes output the same set):

• Bounded simultaneity. ∀ℓ, 1 ≤ ℓ ≤ n : |{j : |sm j | = ℓ}| ≤ k.
Using an (n, k)-PS object we can solve n, ⌈ n k ⌉, 1, n -GSB, as Lemma 9 shows.

Lemma 9 ∀n, k : (n, k)-PS → n, ⌈ n k ⌉, 1, n -GSB.
Proof It is easy to solve n, ⌈ n k ⌉, 1, n -GSB from (n, k)-PS: every process p i invokes the same (n, k)-PS object and decides ⌈ |smi| k ⌉, where sm i is the set it receives from the (n, k)-PS object.

To prove the correctness of the algorithm we have to show that in every execution each one of the ⌈ n k ⌉ slots is decided by at least one process. Suppose, for the sake of contradiction, that there is an execution E in which no process decides some slot x, 1 ≤ x ≤ ⌈ n k ⌉. The (n, k)-PS object outputs sets ordered by containment: S 1 ⊂ . . . ⊂ S m . Moreover, the processes p i that get sm i = S j are the processes p i such that (id i , -) ∈ S j \ S j-1 [START_REF] Borowsky | Immediate Atomic Snapshots and Fast Renaming[END_REF] (for j = 0, S -1 = ∅). Since no process decides x in E, it must be that for some j, 1 ≤ j ≤ m -1, |S j | ≤ (x -1)k and |S j+1 | ≥ xk + 1 (otherwise the processes that get S j or S j+1 would decide x). Observe that |S j+1 \ S j | ≥ k + 1, hence at least k + 1 processes received S j+1 from the (n, k)-PS object. A contradiction with the bounded simultaneity property.

✷ Lemma 9

As mentioned above, it is proved in [START_REF] Mostéfaoui | Exploring Gafni's Reduction Land: from Ω k to Wait-free adaptive (2p -⌈ p k ⌉)-renaming via k-set Agreement[END_REF] that (n, k)-SA → (n, k)-PS, thus the previous lemma implies the following result.

Theorem 13 ∀n, k : (n, k)-SA → n, ⌈ n k ⌉, 1, n -GSB.
Theorems 14 and 15 shows the relation between ⌈ n k ⌉-slot, (n + k -1)-renaming and (2n -⌈ n k ⌉)-renaming.

Theorem 14 ∀n, k : n, n + k -1, 0, 1 -GSB → n, 2n -⌈ n k ⌉, 0, 1 -GSB. Proof Let us observe that n + k -1 ≤ 2n -⌈ n k ⌉, for 1 ≤ k ≤ n -1.
Therefore, an algorithm that solves n, ⌈ n k ⌉, 1, n -GSB, also solves n, 2n -⌈ n k ⌉, 0, 1 -GSB. Consequently, n, n + k -1, 0, 1 -GSB → n, 2n -⌈ n k ⌉, 0, 1 -GSB. ✷ Theorem 14

Theorem 15 ∀n, k : n, n + k -1, 0, 1 -GSB → n, ⌈ n k ⌉, 1, n -GSB.

Collection des Publications Internes de l'Irisa c IRISA Proof Consider the following algorithm A. Each process first calls an n, n + k -1, 0, 1 -GSB object X and then decides (y mod ⌈ n k ⌉) + 1, where y is the value it receives from X. In what follows we prove that A solves n, ⌈ n k ⌉, 1, n -GSB, i.e., in every execution, each element of 1, . . . , ⌈ n k ⌉ is decided by at least one process. For the rest of the proof let α be ⌈ n k ⌉. First observe that mod operator splits the integers 1, . . . , n + k -1 into α equivalence classes, [0], . . . , [α -1]. Let #[j] denotes the number of elements of the equivalence class [j]. Each one of these equivalence classes contains roughly the same amount of elements, i.e., ∀i, j : |#[i] -#[j]| ≤ 1. We will prove the following inequality, which, as explained in detail below, implies the correctness of A. For every i ∈ {0, . . . , α -1}, We now prove that β ≥ k. We identify two cases: (a) n is multiple of k, i.e., n = xk, for some x ≥ 1, and (b) n is not multiple of k, i.e., n = xk + y, for some x ≥ 0 and 1 ≤ y ≤ k -1. For case (a) we have that α = x, and thus β = ⌊ n+k-1 α ⌋ = ⌊k + k-1

x ⌋ ≥ k. For case (b) we have that α = x + 1, and hence

β = ⌊ n+k-1 α ⌋ = ⌊ xk+y+k-1 x+1 ⌋ = ⌊ k(x+1)+y-1 x+1 ⌋ = ⌊k + y-1
x+1 ⌋ ≥ k. Inequality (9) follows. Using inequality [START_REF] Chaudhuri | More Choices Allow More Faults: Set Consensus Problems in Totally Asynchronous Systems[END_REF], the correctness proof of A is simple. Suppose, by contradiction, that there is an execution in which an element x of 1, . . . , ⌈ n k ⌉ is not decided by at least one process. Therefore, it must be that the n processes of the system got values from the n, n + k -1, 0, 1 -GSB object, that do not belong to the equivalence class [x -1]. Thus, α-1 j=0,j =i #[j] ≥ n, which contradicts inequality [START_REF] Chaudhuri | More Choices Allow More Faults: Set Consensus Problems in Totally Asynchronous Systems[END_REF]. The theorem follows.

✷ Theorem 14

Conclusion

Significant efforts have been devoted in the past to the elusive question of understanding the relative computability power of subconsensus tasks in a wait-free setting. These efforts have lead to the discovery of new algorithmic ideas and sophisticated algebraic topology techniques for impossibility results. Yet, essentially only one relation was known for specific values of n: (2n -2)-renaming is strictly weaker than (n, n -1)-SA for odd n. In this paper we have significantly developed the map of computability relations among renaming, set agreement and other GSB tasks. The map with our results and previous results, is in Figure 1. Among other results, we have showed that even the most powerful non-perfect symmetry breaking problem, namely non-adaptive (n + 1)-renaming is not powerful enough to solve the easiest agreement problem, namely (n, n -1)-SA. Hence the question: can non-adaptive perfect renaming, i.e. n-renaming, be used to solve (n, n -1)-SA? If so, which is the value of k < n -1 such that (n, k)-SA can be solved from perfect renaming? Some of the previous impossibility results have been proved in the iterated model IM, hence the question: can we extend the simulation of [START_REF] Gafni | Distributed Programming with Tasks[END_REF] to generalize the results to the non-iterated model? More precisely, [START_REF] Gafni | Distributed Programming with Tasks[END_REF] proves that IM with 01-tasks [START_REF] Gafni | The 01-Exclusion Families of Tasks[END_REF] is equivalent to the snapshot model with 01-tasks, which is sufficient to extend the result in [START_REF] Gafni | Subconsensus Tasks: Renaming is Weaker Than Set Agreement[END_REF] to a non-iterated model. An open issue is then to extend the result in [START_REF] Gafni | Distributed Programming with Tasks[END_REF] to include GSB tasks, and hence generalize our results to a non-iterated model.

Figure 2 :

 2 Figure 2: Generic algorithm for the iterated write-snapshot model (code for p i )

Figure 3 :

 3 Figure 3: Complex O T \ τ of dimension 2 and a sequence produced by findSequence()

Figure 4 :

 4 Figure 4: Finding a sequence of simplexes that joins two (n -1)-simplexes λ, λ ′ ∈ O T

1 α⌋.

 1 We prove inequality[START_REF] Chaudhuri | More Choices Allow More Faults: Set Consensus Problems in Totally Asynchronous Systems[END_REF]. Let β be ⌊ n+k-As explained above, equivalence classes [0], . . . , [α -1] have roughly the same amount of elements of 1, . . . , n + k -1. To be precise, for every i ∈ {0, . . . , α -1} ,#[i] ∈ {β, β + 1}. (In particular, if n + k -1 is multiple of α, then for all i ∈ {0, . . . , α -1} , #[i] = β; otherwise there is at least one i ∈ {0, . . . , α -1} such that #[i] = β + 1.) Clearly we have α-1 j=0 #[j] = n + k -1, thus, for any i ∈ {0, . . . , α -1}, ] -#[i] ≤ n + k -1β, because #[i] ∈ {β, β + 1}.Therefore, if we prove that β ≥ k, then inequality (9) holds.

  Starting from i = 1, each process invokes A[i] with its input name as input; if it receives its input name from A[i], it decides output name i, otherwise increases i by one and repeats.

	✷ Theorem 10
	4.2 From (n, k)-set agreement to ⌈ n k ⌉-slot, (n + k -1)-renaming and (2n -⌈ n k ⌉)-renaming

Collection des Publications Internes de l'Irisa c IRISA


Axel Legay

Benoît Delahaye

Saddek Bensalem

Statistical Model Checking: An Overview

published or not. The documents may come   L'archive ouverte pluridisciplinaire

Introduction and Context

Quantitative properties of stochastic systems are usually specified in logics that allow one to compare the measure of executions satisfying certain temporal properties with thresholds. The model checking problem for stochastic systems with respect to such logics is typically solved by a numerical approach that iteratively computes (or approximates) the exact measure of paths satisfying relevant subformulas. The algorithm for computing such measures depends on the class of stochastic systems being considered as well as the logics used for specifying the correctness properties. Model checking algorithms for a variety of contexts have been discovered [START_REF] Baier | Model-checking algorithms for continuous-time markov chains[END_REF][START_REF] Courcoubetis | The complexity of probabilistic verification[END_REF][START_REF] Ciesinski | On probabilistic computation tree logic[END_REF] and there are mature tools (see e.g. [START_REF] Kwiatkowska | Prism 2.0: A tool for probabilistic model checking[END_REF][START_REF] Ciesinski | Liquor: A tool for qualitative and quantitative linear time analysis of reactive systems[END_REF]) that have been used to analyze a variety of systems in practice.

Despite the great strides made by numerical model checking algorithms, there are many challenges. Numerical algorithms work only for special systems that have certain structural properties. Further the algorithms require a lot of time and space, and thus scaling to large systems is a challenge. Finally, the logics for which model checking algorithms exist are extensions of classical temporal logics, which are often not the most popular among engineers.

Another way to verify quantitative properties is to use a simulation-based approach. The key idea is to deduce whether or not the system satisfies the property by observing some of its executions with a monitoring procedure [START_REF] Bauer | Monitoring of real-time properties[END_REF][START_REF] Havelund | Synthesizing monitors for safety properties[END_REF], and use hypothesis testing to infer whether the samples provide a statistical evidence for the satisfaction or violation of the specification [START_REF] Younes | Probabilistic verification of discrete event systems using acceptance sampling[END_REF]. Of course, in contrast to a numerical approach, a simulation-based solution does not guarantee a correct result. However, it is possible to bound the probability of making an error. Simulation-based methods are known to be far less memory and time intensive than numerical ones, and are sometimes the only option [START_REF] Younes | Numerical vs. statistical probabilistic model checking[END_REF].

The crux of the statistical model checking approach is that since sample executions of a stochastic system are drawn according to the distribution defined by the system, they can be used to get estimates of the probability measure on executions. Starting from time-bounded Probabilistic Computational Tree Logic properties [START_REF] Younes | Probabilistic verification of discrete event systems using acceptance sampling[END_REF], the technique has been extended to handle properties with unbounded until operators [START_REF] Sen | On statistical model checking of stochastic systems[END_REF], as well as to black-box systems [START_REF] Sen | Statistical model checking of black-box probabilistic systems[END_REF][START_REF] Younes | Probabilistic verification for "black-box" systems[END_REF]. Tools based on this idea have been built [START_REF] Sen | Vesta: A statistical model-checker and analyzer for probabilistic systems[END_REF][START_REF] Younes | Ymer: A statistical model checker[END_REF], and they have been used to analyze many systems.

This approach enjoys many advantages. First, these algorithms only require that the system be executable (or rather, sample executions be drawn according to the measure space defined by the system). Thus, it can be applied to larger class of systems than numerical model checking algorithms including black-box systems and infinite state systems. Second the approach can be generalized to a larger class of properties, including Fourier transform based logics. Finally, the algorithm is easily parallelizable, which can help scale to large systems. However, the statistical approach also has some disadvantages when compared with the numerical approach. First, it only provides probabilistic guarantees about the correctness of the algorithms answer. Next, the sample size grows very large if the model checker's answer is required to be highly accurate. Finally, the statistical approach only works for purely probabilistic systems, i.e., those that do not have any nondeterminism. Furthermore, since statistical tests are used to determine the correctness of a system, the approach only works for systems that "robustly" satisfy a given property, i.e., the actual measure of paths satisfying a given subformula, is bounded away from the thresholds to which it is compared in the specification.

In this tutorial, we will overview existing statistical model checking algorithms and discuss their efficiency. We will also overview existing tools and case studies and discuss future work.

Our Objective

We consider a stochastic system S and a property φ. An execution of S is a possibly infinite sequence of states of S. Our objective is to solve the probabilistic model checking problem, i.e., to decide whether S satisfies φ with a probability greater or equal to a certain threshold θ. The latter is denoted S |= P ≥θ (φ), where P is called a probabilistic operator. This paper will overview solutions to this problem. These solutions depend on the nature of S and φ. We consider three cases.

1. We first assume that S is a white-box system, i.e., that one can generate as much executions of the system as we want. We also assume that φ does not contain probabilistic operators. In Section 3, we recall basic statistical algorithms that can be used to verify bounded properties (i.e., properties that can be monitored on fixed-length execution) of white-box systems. 2. In Section 4, we discuss extensions to the full probabilistic computation tree logic [START_REF] Ciesinski | On probabilistic computation tree logic[END_REF]. There, we consider the case where φ can also contain probabilistic operators and the case where it has to be verified on infinite executions. 3. In Section 5, we briefly discuss the verification of black-box systems, i.e.

systems for which a part of the probability distribution is unknown.

In Section 6, we will present various experiments that show that (1) statistical model checking algorithms can be more efficient than numerical ones, and (2) statistical model checking algorithms can be applied to solve problems that are beyond the scope of numerical methods. Finally, Section 7 discusses our vision of the future of statistical model checking.

Remark 1. The objective of the tutorial is not to feed the reader with technical details, but rather to introduce statistical model checking, and outline its main advantages in terms of efficiency, uniformity, and simplicity.

Remark 2. There are other techniques that allow to estimate the probability for S to satisfy φ. These approaches (that are based on Monte-Carlo techniques) will not be covered in this paper. The interested reader is redirected to [START_REF] Grosu | Monte carlo model checking[END_REF][START_REF] Hérault | Approximate probabilistic model checking[END_REF][START_REF] Laplante | Probabilistic abstraction for model checking: An approach based on property testing[END_REF] for more details.

Remark 3. Statistical Model Checking also applies to non stochastic systems [START_REF] Grosu | Monte carlo model checking[END_REF]. This topic will not be covered in this tutorial.

Statistical Model Checking : The Beginning

In this section, we overview several statistical model checking techniques. We assume that S is a white-box system and that φ is a bounded property. By bounded properties, we mean properties that can be defined on finite executions of the system. In general, the length of such executions has to be precomputed. Let B i be a discrete random variable with a Bernoulli distribution of parameter p. Such a variable can only take two values 0 and 1 with P r[B i = 1] = p and P r[B i = 0] = 1p. In our context, each variable B i is associated with one simulation of the system. The outcome for B i , denoted b i , is 1 if the simulation satisfies φ and 0 otherwise. To make sure that the above approach works, one has to make sure that one can get the result of any experiment in a finite amount of time. In general, this means that we are considering bounded properties, i.e., properties that can be decided on finite executions. Remark 4. All the results presented in this section are well-known mathematical results coming from the area of statistics. As we shall see, these results are sufficient to verify bounded properties of a large class of systems. As those properties are enough in many practical applications, one could wonder whether the contribution of the computer scientist should not be at the practical level rather than at the theoretical one.

Before going further one should answer one last question: "What is the class of models that can be considered?" In fact, statistical model checking can be applied to any stochastic system and logic on which one can define a probability space for the property under consideration. Hence, the approach provides a uniform way for the verification of a wide range of temporal logic properties over various stochastic models, including Markov Chains or Continuous Timed Markov Chains [START_REF] Vardi | Automatic verification of probabilistic concurrent finite-state programs[END_REF][START_REF] Baier | Principles of Model Checking[END_REF][START_REF] Baier | Model-checking algorithms for continuous-time markov chains[END_REF]. In general, it is not necessary to make the hypothesis that the system has the Markovian property1 , except when working with nested formulas (see Section 4). It is worth mentioning that the technique cannot be applied to systems that combine both nondeterministic and stochastic aspects (such as Markov Decision Processes). Indeed, the simulation-based approach could not distinguish between the probability distributions that are sampled.

Qualitative Answer Using Statistical Model Checking

The main approaches [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF][START_REF] Sen | Statistical model checking of black-box probabilistic systems[END_REF] proposed to answer the qualitative question are based on hypothesis testing. Let p = P r(φ), to determine whether p ≥ θ, we can test H : p ≥ θ against K : p < θ. A test-based solution does not guarantee a correct result but it is possible to bound the probability of making an error. The strength (α, β) of a test is determined by two parameters, α and β, such that the probability of accepting K (respectively, H) when H (respectively, K) holds, called a Type-I error (respectively, a Type-II error ) is less or equal to α (respectively, β).

A test has ideal performance if the probability of the Type-I error (respectively, Type-II error) is exactly α (respectively, β). However, these requirements make it impossible to ensure a low probability for both types of errors simultaneously (see [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF] for details). A solution to this problem is to relax the test by working with an indifference region (p 1 , p 0 ) with p 0 ≥p 1 (p 0p 1 is the size of the region). In this context, we test the hypothesis H 0 : p ≥ p 0 against H 1 : p ≤ p 1 instead of H against K. If the value of p is between p 1 and p 0 (the indifference region), then we say that the probability is sufficiently close to θ so that we are indifferent with respect to which of the two hypotheses K or H is accepted. The thresholds p 0 and p 1 are generally defined in term of the single threshold θ, e.g., p 1 = θδ and p 0 = θ + δ. We now need to provide a test procedure that satisfies the requirements above. In the next two subsections, we recall two solutions proposed by Younes in [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF][START_REF] Younes | Statistical probabilistic model checking with a focus on time-bounded properties[END_REF].

Single Sampling Plan. To test H 0 against H 1 , we specify a constant c. If n i=1 b i is larger than c, then H 0 is accepted, else H 1 is accepted. The difficult
part in this approach is to find values for the pair (n, c), called a single sampling plan (SSP in short), such that the two error bounds α and β are respected. In practice, one tries to work with the smallest value of n possible so as to minimize the number of simulations performed. Clearly, this number has to be greater if α and β are smaller but also if the size of the indifference region is smaller. This results in an optimization problem, which generally does not have a closed-form solution except for a few special cases [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF]. In his thesis [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF], Younes proposes a binary search based algorithm that, given p 0 , p 1 , α, β, computes an approximation of the minimal value for c and n.

Remark 5. There are many variants of this algorithm. As an example, in [START_REF] Sen | On statistical model checking of stochastic systems[END_REF], Sen et al. proposes to accept H 0 if

( n i=1 bi) n ≥p.
Here, the difficulty is to find a value for n such that the error bounds are valid.

Sequential probability ratio test. The sample size for a single sampling plan is fixed in advance and independent of the observations that are made. However, taking those observations into account can increase the performance of the test. As an example, if we use a single plan (n, c) and the m > c first simulations satisfy the property, then we could (depending on the error bounds) accept H 0 without observing the nm other simulations. To overcome this problem, one can use the sequential probability ratio test (SPRT in short) proposed by Wald [START_REF] Wald | Sequential tests of statistical hypotheses[END_REF]. The approach is briefly described below.

In SPRT, one has to choose two values A and B (A > B) that ensure that the strength of the test is respected. Let m be the number of observations that have been made so far. The test is based on the following quotient:

p 1m p 0m = m i=1 P r(B i = b i | p = p 1 ) P r(B i = b i | p = p 0 ) = p dm 1 (1 -p 1 ) m-dm p dm 0 (1 -p 0 ) m-dm , ( 1
)
where

d m = m i=1 b i . The idea behind the test is to accept H 0 if p1m p0m ≥ A, and H 1 if p1m p0m ≤ B.
The SPRT algorithm computes p1m p0m for successive values of m until either H 0 or H 1 is satisfied; the algorithm terminates with probability 1 [START_REF] Wald | Sequential tests of statistical hypotheses[END_REF]. This has the advantage of minimizing the number of simulations. In his thesis [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF], Younes proposed a logarithmic based algorithm SPRT that given p 0 , p 1 , α and β implements the sequential ratio testing procedure.

Discussion. Computing ideal values A id and B id for A and B in order to make sure that we are working with a test of strength (α, β) is a laborious procedure (see Section 3.4 of [START_REF] Wald | Sequential tests of statistical hypotheses[END_REF]). In his seminal paper [START_REF] Wald | Sequential tests of statistical hypotheses[END_REF], Wald showed that if one defines

A id ≥A = (1-β) α and B id ≤ B = β
(1-α) , then we obtain a new test whose strength is (α , β ), but such that α + β ≤ α + β, meaning that either α ≤α or β ≤ β. In practice, we often find that both inequalities hold. This is illustrated with the following example taken from [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF].

Example 1. Let p 0 = 0.5, p 1 = 0.3, α = 0.2 and β = 0.1. If we use A id ≥A = (1-β) α and B id ≤ B = β (1-α)
, then we are guaranteed that α ≤0.222 and β ≤0.125. Through computer simulation (reproducing the same experiments 10000 of time), we observe that α ≤0.175 and β ≤0.082. So the strength of the test is in reality better than the theoretical assumption.

Some Generalities Regarding Efficiency

The efficiency of the above algorithms is characterized by the number of simulations needed to obtain an answer as well as the time it costs to compute a simulation. The latter often depends on the property under verification. Both numbers are expected numbers as they change from executions to executions and can only be estimated (see [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF] for an explanation). However, some generalities are known. For example, it is known that, except for some situations, SPRT is always faster than SSP. When θ = 1 (resp. θ = 0) SPRT degenerates to SSP; it is not a problem since SSP is known to be optimal for such values. Observe that the time complexity of statistical model checking is independent from the state-space and that the space complexity is of the order of the state space. Also, the expected number of simulations for SSP is logarithmic with respect to α and β and linear with respect to the indifference region; for SPRT, the number depends on the probability distribution p. Remark 6. A very relevant discussion on complexity of statistical model checking can be found in Section 5.4 of [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF].

Statistical Model Checking: Next Step

In the previous section, we have proposed statistical model checking algorithms for verifying bounded properties of white-box systems. In this section, we go one step further and consider three nontrivial extensions that are:

1. The nested case, i.e., the case where φ can also contain probabilistic operators. As an example, we can write the following property P ≥θ1 (q ⇒ P ≥θ2 (φ 2 )) 2. The unbounded case, i.e., the case where φ cannot be decide on a finite execution. Here we will restrict ourselves to the until property. Given two formulas φ 1 and φ 2 , the until operator ensures that φ 1 is true until φ 2 has been seen. 3. Boolean combinations of formulae, i.e., formulae of the form: P ≥θ1 (φ 1 ) ∧ P ≥θ2 (φ 2 ).

We will only survey existing results and give pointers to the relevant papers.

The Unbounded Case: Until

We are now concerned with the verification of the until property. This property requires that a property φ 1 remains valid until a property φ 2 has been seen. The problem is that we do not know a priori the moment when φ 2 will be satisfied. Hence, one has to reason on infinite execution. There are two works on this topics, one by Sen et al. [START_REF] Sen | On statistical model checking of stochastic systems[END_REF] and one more recent work by Pekergin et al. [START_REF] Rabih | Statistical model checking using perfect simulation[END_REF]. We will not give details on these works, but the reader should know that Sen works by extending the model with extra probabilities, which makes the solution extremely slow. Pekergin uses a new technique that is based on perfect simulation. According to [START_REF] Rabih | Statistical model checking using perfect simulation[END_REF], this technique is not only faster than Sen's one, but also more general as it allows to study the steady-state operator for continuous timed Markov Chains.

Remark 7. Contrary to the numerical results [START_REF] Vardi | Automatic verification of probabilistic concurrent finite-state programs[END_REF][START_REF] Bustan | Verifying omega-regular properties of markov chains[END_REF] the above results are not sufficient to verify properties of the form P ≥θ (φ), where φ is a property expressed in Linear Temporal Logic [START_REF] Pnueli | The temporal logic of programs[END_REF]. Incomplete results regarding the verification of these properties with simulation-based techniques can be found in [START_REF] Hérault | Approximate probabilistic model checking[END_REF][START_REF] Grosu | Monte carlo model checking[END_REF].

Nested Probability Operators

We consider the problem of checking whether S satisfies φ with a probability greater or equal to θ. However, contrary to what we have been doing so far, we will now assume that φ cannot be decided on a single execution, i.e., we will assume that φ is of the form P ≥θ1 φ 1 . So, where is the difficulty? The difficulty is that φ cannot be model checked on a single execution, but rather depends on another test. Hence, we have to provide a way to nest tests. In his thesis, Younes proposed the following theorem.

Theorem 1. Let ψ = P ≥θ (φ) be a property and assume that φ can be verified with Type-I error α and Type-II error β , then ψ can be verified with Type-I error α and Type-II error β, assuming that the indifference region is of size at least

((θ + δ)(1 -α ), (1 -(1 -(θ -δ)))(1 -β ).
Hence one has to find a compromise between the size of the indifference region of the inner test and the outer one. There are two interesting facts to know about nested operators:

1. Even for bounded properties, the above result (and in fact, any result in the literature [START_REF] Sen | On statistical model checking of stochastic systems[END_REF][START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF][START_REF] Younes | Probabilistic verification for "black-box" systems[END_REF][START_REF] Younes | Ymer: A statistical model checker[END_REF]) only works for systems that have the Markovian property. 2. In practice, the complexity (in term of number of sampling) becomes exponential in the number of tests.

Remark 8. An interesting research direction would be to study the link with probabilistic testing [START_REF] Larsen | Bisimulation through probabilistic testing[END_REF].

Boolean Combinations

We have to consider two operations, namely conjunction and negation (as it is known that any Boolean combination reduces to combinations of these two operators). We recall some results provided by Younes. We start with conjunction.

Theorem 2. Let ψ be the conjunction of n properties φ 1 , . . . , φ 2 . Assume that each φ i can be decided with Type-I error α i and Type-II error β I . Then φ can be decided with Type-I error min i (α i ) and Type-II error max i (β i ).

The idea behind the proof of the theorem is that 1. If we claim that the conjunction is not satisfied, this means that we have deduced that one of the operands is not.

2. If we claim that the conjunction is satisfied, this means that we have concluded that all the operands are satisfied. As we may have made mistakes in each individual verification, we get max i (β i ).

For negation, the result is provided by the following theorem.

Theorem 3. To verify a formula ¬ψ with Type-I error α and Type-II error β, it is sufficient to verify ψ with Type-I error β and Type-II error α.

Black-box Systems: A Note

Black-box Systems is an interesting class of stochastic systems whose treatment is beyond the scope of numerical techniques. Roughly speaking, a black-box systems is simply a system whose probability distribution (i.e., set of behaviors) is not totally known and cannot be observed. Hence, one can view a black-box system as a finite set of executions pre-computed and for which no information is available.

In the context of such systems, Type errors and indifference region cannot play a role. Indeed, those parameters influence the number of simulations that can be computed, but here the simulations are given and you cannot compute more! A solution to this problem is to conduct a SSP test assuming that the parameter n is fixed to the number of simulations that are given in advance. The difficulty is to chose the constant c in such a way that it becomes roughly equal to accept H 0 or H 1 if θ = p. In his thesis [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF] and in [START_REF] Younes | Error control for probabilistic model checking[END_REF], Younes proposed a solution to the problem. He also shown that a previous solution proposed by Sen [32] is not correct.

There are techniques to verify nested formulas over black-box systems. However, a technique for the verification of unbounded properties is still needed.

Tools and Experiments

Any statistical model checking toolset is build by combining 1) a monitoring procedure to decide whether a finite execution satisfies the property under consideration, 2) a statistical model checking algorithm, and 3) a tool that allows to describe a system and generate sets of executions.

The two firsts tools that implemented statistical model checking algorithms are Ymer [START_REF] Younes | Ymer: A statistical model checker[END_REF] and Vesta [START_REF] Sen | Vesta: A statistical model-checker and analyzer for probabilistic systems[END_REF]. Vesta implements a variation of the single sampling plan algorithm. The choice of implementing the SSP algorithm is motivated by the fact that it is easier to parallelize as the number of simulations to perform is known in advance. However, in his thesis, Younes showed that sequential algorithms are also easily parallelizable. Ymer is limited to bounded properties while Vesta also incorporate the unbounded until. In [START_REF] Jansen | How fast and fat is your probabilistic model checker? an experimental performance comparison[END_REF], the authors conducted several experiments that tend to show that (1) Ymer is faster than Vesta and (2) Vesta makes more false positive (selecting the bad hypothesis) than Ymer.

Regarding the unbounded case, it seems that Vesta is not very efficient and can make a lot of false positive. Both Vesta and Ymer have been applied to huge case studies. A comparison of Ymer and Vesta to established tools such as PRISM [START_REF] Kwiatkowska | Prism 2.0: A tool for probabilistic model checking[END_REF] can be found in [START_REF] Jansen | How fast and fat is your probabilistic model checker? an experimental performance comparison[END_REF].

Both Ymer and Vesta as well as their successors [START_REF] Katoen | Simulation-based ctmc model checking: An empirical evaluation[END_REF][START_REF] Katoen | The ins and outs of the probabilistic model checker mrmc[END_REF] focus on the verification of classical stochastic extension of temporal logics. In a series of recent work, we have shown that statistical model checking can also be used in other contexts that are clearly beyond the scope of existing tools. This topic is the subject of the next subsections.

Verifying Circuits

In [START_REF] Clarke | Statistical model checking of mixed-analog circuits with an application to a third order delta-sigma modulator[END_REF][START_REF] Clarke | On simulation-based probabilistic model checking of mixed-analog circuits[END_REF], we applied SPRT to verifying properties of mixed-signal circuits, i.e., circuits for which there is an interaction between analog (continuous) and digital (discrete) values. Our first contribution was to propose a version of stochastic discrete-time event systems that fits into the framework introduced by Younes with the additional advantage that it explicitly handles analog and digital signals. We also introduced probabilistic signal linear temporal logic, a logic adapted to the specification of properties for mixed-signal circuits in the temporal domain and in the frequency domain. Our second contribution was the analysis of a Δ-Σ modulator. A Δ-Σ modulator is an efficient Analog-to-Digital Converter circuit, i.e., a device that converts analog signals into digital signals. A common critical issue in this domain is the analysis of the stability of the internal state variables of the circuit. The concern is that the values that are stored by these variables can grow out of control until reaching a maximum value, at which point we say that the circuit saturates. Saturation is commonly assumed to compromise the quality of the analog-to-digital conversion. In [START_REF] Dang | Verification of analog and mixed-signal circuits using hybrid systems techniques[END_REF] and [START_REF] Gupta | Towards formal verification of analog designs[END_REF] reachability techniques developed in the area of hybrid systems are used to analyze the stability of a third-order modulator. Their idea is to use such techniques to guarantee that for every input signal in a given range, the states of the system remain stable. While this reachability-based approach is sound, it has important drawbacks such as (1) signals with long duration cannot be practically analyzed, and (2) properties that are commonly specified in the frequency domain rather than in the time domain cannot be checked. Our results show that a simulation-based approach makes it possible to handle properties and signals that are beyond the scope of the reachability-based approach. As an example, in our experiments, we analyze discrete-time signals with 24000 sampling points in seconds, while the approach in [START_REF] Dang | Verification of analog and mixed-signal circuits using hybrid systems techniques[END_REF] takes hours to analyze signals with up to 31 sampling points. We are also able to provide insight into a question left open in [START_REF] Dang | Verification of analog and mixed-signal circuits using hybrid systems techniques[END_REF] by observing that saturation does not always imply an improper signal conversion. This can be done by comparing the Fourier transform of each of the input analog signals with the Fourier transform of its corresponding digital signal. Such a property can easily be expressed in our logic and Model Checked with our simulation-based approach. We are unaware of other formal verification techniques that can solve this problem. Indeed, numerical techniques cannot reason on an execution at a time.

Systems Biology

In [START_REF] Clarke | Statistical model checking in biolab: Applications to the automated analysis of t-cell receptor signaling pathway[END_REF], we considered the verification of complex biological systems. we introduced a new tool, called BioLab, for formally reasoning about the behavior of stochastic dynamic models by integrating SPRT into the BioNetGen [START_REF] Faeder | Graphical rule-based representation of signal-transduction networks[END_REF][START_REF] Faeder | Rule-based modeling of biochemical systems with BioNetGen[END_REF] framework for rule-based modeling. We then used BioLab to verify the stochastic bistability of T-cell signalling. Our results have recently been extended to take prior knowledge on the model into account [START_REF]A Bayesian Approach to Model Checking Biological Systems[END_REF].

Remark 9. Statistical model checking techniques recently received a lot of attention in the area of systems biology. As an example, Carnegie Mellon University was awarded a $10.000.000 grant for applying such techniques in the medical area [START_REF] Cmacs | [END_REF].

Heterogeneous Applications

In [START_REF] Basu | Statistical abstraction and model-checking of large heterogeneous systems[END_REF], we have proposed to apply statistical model checking techniques to the verification of heterogeneous applications. Systems integrating multiple heterogeneous distributed applications communicating over a shared network are typical in various sensitive domains such as aeronautic or automotive embedded systems. Verifying the correctness of a particular application inside such a system is known to be a challenging task, which is often beyond the scope of existing exhaustive validation techniques.

In our paper, we proposed to exploit the structure of the system in order to increase the efficiency of the verification process. The idea is conceptually simple: instead of performing an analysis of the entire system, we proposed to analyze each application separately, but under some particular context/execution environment. This context is a stochastic abstraction that represents the interactions with other applications running within the system and sharing the computation and communication resources. The idea is to build such a context automatically by simulating the system and learning the probability distributions of key characteristics impacting the functionality of the given application. The abstraction can easily be analyzed with statistical model checking techniques.

The overall contribution of our study is an application of the above method on an industrial case study, the heterogeneous communication system (HCS for short) deployed for cabin communication in a civil airplane. HCS is an heterogeneous system providing entertainment services (ex : audio/video on passengers demand) as well as administrative services (ex: cabin illumination, control, audio announcements), which are implemented as distributed applications running in parallel, across various devices within the plane and communicating through a common Ethernet-based network. The HCS system has to guarantee stringent requirements, such as reliable data transmission, fault tolerance, timing and synchronization constraints. An important requirement is the accuracy of clock synchronization between different devices. This latter property states that the difference between the clocks of any two devices should be bounded by a small constant, which is provided by the user and depends on his needs (for example, to guarantee the fiability of another service). Hence, one must be capable to compute the smallest bound for which synchronization occurs and compare it with the bound expected by the user. Unfortunately, due to the large number of heterogeneous components that constitute the system, deriving such a bound manually from the textual specification is an unfeasible task. In this paper, we propose a formal approach that consists in building a formal model of the HCS, then we apply simulation-based algorithms to this model in order to deduce the smallest value of the bound for which synchronization occurs. We start with a fixed value of the bound and check whether synchronization occurs. If yes, then we make sure that this is the best one. If no, we restart the experiment with a new value.

We have been able to derive precise bounds that guarantee proper synchronization for all the devices of the system. We also computed the probability to satisfy the property for smaller values of the bound, i.e., bounds that do not satisfy the synchronization property with probability 1. Being able to provide such an information is of clear importance, especially when the best bound is too high with respect to user's requirements. We have observed that the values we obtained strongly depend on the position of the device in the network. We also estimated the average and worst proportion of failures per simulation for bounds that are smaller than the one that guarantees synchronization. Checking this latter property has been made easy because statistical model checking allows us to reason on one execution at a time. Finally, we have also considered the influence of clock drift on the synchronisation results. The experiments highlight the generality of our technique, which could be applied to other versions of the HCS as well as to other heterogeneous applications.

The Future of Statistical Model Checking

There are various directions for future research in the statistical model checking area. Here is a list of possible topics.

-Using efficient techniques for performing simulation is crucial to guarantee good performances for any statistical model checking algorithm. Unfortunately, the existing algorithms do not exploit efficient simulation techniques. It would thus be worth combining statistical model checking algorithms with such techniques (example : rare-event simulations, , ...). This is a huge implementation effort which also requires to define a methodology to select the good simulation technique to be applied. -Statistical model checking algorithms have not yet been applied to the verification of multi-core systems, this area should be investigated. -Statistical model checking algorithms do not apply to systems that combine both stochastic and non deterministic aspects. Extending the results to such systems is however crucial to perform verification of security protocols, networking protocols, and performance protocols. -Statistical model checking algorithms reduce to decide between two hypothesis. In many areas, especially systems biology, we may have a prior knowledge on the probability to satisfy each hypothesis. Incorporating this prior knowledge in the verification process may considerably reduce the number of simulations needed for the algorithm to terminate. -Statistical model checking algorithms suppose that the property φ can be checked on finite executions of the system. There are however many situations where φ cannot be checked in a finite amount of time. This is for example the case when φ is a long-run average or a steady state property.

In systems biology, we are clearly interested in the study of such properties. -Verifying applications running within a huge heterogeneous system without is a challenging problem. In a recent work [START_REF] Basu | Statistical abstraction and model-checking of large heterogeneous systems[END_REF], the authors have proposed a new simulation-based technique for solving such problem. The technique starts by performing simulations of the system in order to learn the context in where the application is used. Then, it creates a stochastic abstraction for the application, which takes the context information into account. Up to know, there is no automatic way to learn the context and derive the stochastic context. However, what we have observed so far is that it often takes the form of properties that cannot be expressed in classical temporal logic. Hence, statistical model checking may be our last resort to analyze the resulting abstraction. -Statistical model checking may help testers. In [START_REF] Merayo | A statistical approach to test stochastic and probabilistic systems[END_REF], Cavalli et al. proposed to use statistical techniques for conformance testing of timed stochastic systems. The technique should be automated. This could lead to new algorithms for verifying the so-called black-box systems.

G

  . Roşu et al. (Eds.): RV 2010, LNCS 6418, pp. 122-135, 2010. c Springer-Verlag Berlin Heidelberg 2010

The Markovian property ensures that the probability to go from a state s to a next state only depends on s, not on the states that have been visited before reaching s.

Acknowledgments

We would like to thanks our collaborators on the statistical model checking project: Sumit Jha, and Marius Bozga.