19h15 Dinner
9h00 - 12h30 Distributed Universal Constructions: a Guided Tour Michel Raynal
Abstract: The notion of a universal construction is central in computing science: the wheel has not to be reinvented for each new problem. In the context of n-process asynchronous distributed systems, a universal construction is an algorithm that is able to build any object defined by a sequential specification despite the occurrence of up to (n-1) process crash failures. The aim of this tutorial is to present a guided tour of such universal constructions. Its spirit is not to be a catalog of the numerous constructions proposed so far, but a (as simple as possible) presentation of the basic concepts and mechanisms that constitute the basis these constructions rest on.
Document: Distributed Universal Constructions: a Guided Tour, Slides
12h30 Lunch
14h00 - 17h30 Lower Bounds Techniques for Distributed Computing Petr Kuznetsov
Abstract: Models for distributed systems come in many flavors: processes may communicate through shared memory or by message passing, they may be synchronous or asynchronous, susceptible to failures or not, and so on. The different models require different lower bound results. Nevertheless, many of these proof rely on common techniques, having to do with information transfer and the difficulty of dealing with indistinguishable scenarios. This lecture will explore and explain some of these techniques, together with their applications.
19h30 Dinner
9h00 - 12h30 Network Algorithms Boaz Patt-Shamir
Abstract: We shall talk about three types of problems and algorithms for networks of processors communicating by short messages:
12h30 Lunch
14h00 - 17h30 Local Distributed Computing Pierre Fraigniaud
Abstract: The lecture will address locality in distributed network computing. The objective is to study how to solve complex tasks in a network where nodes are bounded to interact locally, that is, where nodes can only exchange information with nodes in the their vicinity, i.e., at constant distance, or at distance bounded by a function negligible compared to the diameter of the network. The lecture will present the main techniques to derive lower bounds, as well as several deterministic or randomized algorithms for solving non trivial symmetry breaking tasks in networks. In addition, the lecture will survey the most recent results in the context of local computing, and the main open problem in this field.
19h30 Dinner
9h00 - 12h30 Distributed Algorithms for Mobile Networks Sébastien Tixeuil
Abstract: Current distributed systems frequently include some kind of mobility (e.g. passively mobile sensors can be embedded on animals or vehicles whose movements must be coped with by the sensors, while actively mobile devices such as autonomous robots can use mobility to solve complex distributed problems). This talk will present key results and models for designing distributed algorithms run by mobile entities. Recent research results and ongoing projets will also be discussed.
12h30 Lunch
Abstract: Participants will be proposed various exercises on the different topics covered so far in the school in order to help them better comprehend the notions and techniques presented in the different lectures.
15h15 Social event
19h30 Dinner
9h00 - 12h30 Compact and Distributed Data Structures Cyril Gavoille
Abstract: A fundamental question in Distributed Computing is to understand how localized and how much information are required to solve a task on a network. Typically, if the distance between any pair x,y of nodes in a network is asked, we would like to know which minimal information about x and y in the network are needed. The goal in labeling schemes is precisely to understand how much information must be attached to the nodes (formalized as labels) to solve a graph problem assuming the answer can be determined solely on the basis of the labels of the nodes invoked in the query. In this lecture, we will present the main tools and techniques to solve such labeling problems, including distance labeling schemes, nearest common ancestor labeling schemes, and label-based compact routing schemes.
12h30 Lunch
14h00 - 15h30 How can a Distributed Algorithmic Perspective Contribute to the Study of Biological Systems? Amos Korman
Abstract: I will speak about different directions that I take in order to study computational aspects that are fundamental to biological systems while employing a distributed algorithmic perspective. I will mostly focus on the study of ensembles such as ants or birds, and elaborate on modeling their computational challenges with respect to basic tasks such as searching (i.e., foraging for food) and stochastic dissemination of information (i.e., recruitment or alarming processes).
16h00 - 17h30 Formal Methods for the Verification of Distributed Algorithms Paul Gastin
Abstract: We introduce an automata-theoretic method for the verification of distributed algorithms running on ring networks. In a distributed algorithm, an arbitrary number of processes cooperate to achieve a common goal (e.g., elect a leader, sort an array). Processes have unique identifiers (pids) from an infinite, totally ordered domain. An algorithm proceeds in synchronous rounds, each round allowing a process to perform a bounded sequence of actions such as send or receive a pid, store it in some register, and compare register contents wrt. the associated total order. An algorithm is supposed to be correct independently of the number of processes. To specify correctness properties, we introduce a logic that can reason about processes and pids. Referring to leader election, it may say that, at the end of an execution, each process stores the maximum pid in some dedicated register.
We show that the verification problem of distributed algorithms can be reduced to satisfiability of a formula from propositional dynamic logic with loop and converse (LCPDL), interpreted over cylinders over a finite alphabet. This translation is independent of any restriction imposed on the algorithm. However, since the verification problem (and satisfiability for LCPDL) is undecidable, we propose an underapproximation technique, which bounds the number of rounds. This is an appealing approach, as the number of rounds needed by a distributed algorithm to conclude is often exponentially smaller than the number of processes. Using our reduction to LCPDL, we provide an automata-theoretic solution, reducing model checking to emptiness for alternating two-way automata on words. Overall, we show that round-bounded verification of distributed algorithms over rings is PSPACE-complete, provided the number of rounds is given in unary.
19h30 Dinner
9h00 - 10h15 Locality Beyond Classical Models Cyril Gavoille
Abstract: The objective of this lecture is to understand the impact of quantum resources on the efficiency of distributed algorithms. We will present the basic concepts of quantum information, and how to use them to extend the LOCAL model and to solve problems such as coloring or its variants.
11h00 - 12h15 Discussion
12h15 Lunch
13h15 Boat to Tour Fondue, to be confirmed
End of the school