65 Search Results for "Widder, Josef"


Volume

LIPIcs, Volume 121

32nd International Symposium on Distributed Computing (DISC 2018)

DISC 2018, October 15-19, 2018, New Orleans, USA

Editors: Ulrich Schmid and Josef Widder

Document
Holistic Verification of Blockchain Consensus

Authors: Nathalie Bertrand, Vincent Gramoli, Igor Konnov, Marijana Lazić, Pierre Tholoniat, and Josef Widder

Published in: LIPIcs, Volume 246, 36th International Symposium on Distributed Computing (DISC 2022)


Abstract
Blockchain has recently attracted the attention of the industry due, in part, to its ability to automate asset transfers. It requires distributed participants to reach a consensus on a block despite the presence of malicious (a.k.a. Byzantine) participants. Malicious participants exploit regularly weaknesses of these blockchain consensus algorithms, with sometimes devastating consequences. In fact, these weaknesses are quite common and are well illustrated by the flaws in various blockchain consensus algorithms [Pierre Tholoniat and Vincent Gramoli, 2019]. Paradoxically, until now, no blockchain consensus has been holistically verified. In this paper, we remedy this paradox by model checking for the first time a blockchain consensus used in industry. We propose a holistic approach to verify the consensus algorithm of the Red Belly Blockchain [Tyler Crain et al., 2021], for any number n of processes and any number f < n/3 of Byzantine processes. We decompose directly the algorithm pseudocode in two parts - an inner broadcast algorithm and an outer decision algorithm - each modelled as a threshold automaton [Igor Konnov et al., 2017], and we formalize their expected properties in linear-time temporal logic. We then automatically check the inner broadcasting algorithm, under a carefully identified fairness assumption. For the verification of the outer algorithm, we simplify the model of the inner algorithm by relying on its proven properties. Doing so, we formally verify, for any parameter, not only the safety properties of the Red Belly Blockchain consensus but also its liveness in less than 70 seconds.

Cite as

Nathalie Bertrand, Vincent Gramoli, Igor Konnov, Marijana Lazić, Pierre Tholoniat, and Josef Widder. Holistic Verification of Blockchain Consensus. In 36th International Symposium on Distributed Computing (DISC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 246, pp. 10:1-10:24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.DISC.2022.10,
  author =	{Bertrand, Nathalie and Gramoli, Vincent and Konnov, Igor and Lazi\'{c}, Marijana and Tholoniat, Pierre and Widder, Josef},
  title =	{{Holistic Verification of Blockchain Consensus}},
  booktitle =	{36th International Symposium on Distributed Computing (DISC 2022)},
  pages =	{10:1--10:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-255-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{246},
  editor =	{Scheideler, Christian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2022.10},
  URN =		{urn:nbn:de:0030-drops-172019},
  doi =		{10.4230/LIPIcs.DISC.2022.10},
  annote =	{Keywords: Model checking, automata, logic, byzantine failure}
}
Document
Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms

Authors: Nathalie Bertrand, Bastien Thomas, and Josef Widder

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)


Abstract
Distributed algorithms typically run over arbitrary many processes and may involve unboundedly many rounds, making the automated verification of their correctness challenging. Building on domain theory, we introduce a framework that abstracts infinite-state distributed systems that represent distributed algorithms into finite-state guard automata. The soundness of the approach corresponds to the Scott-continuity of the abstraction, which relies on the assumption that the distributed algorithms are layered. Guard automata thus enable the verification of safety and liveness properties of distributed algorithms.

Cite as

Nathalie Bertrand, Bastien Thomas, and Josef Widder. Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 15:1-15:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.CONCUR.2021.15,
  author =	{Bertrand, Nathalie and Thomas, Bastien and Widder, Josef},
  title =	{{Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{15:1--15:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.15},
  URN =		{urn:nbn:de:0030-drops-143926},
  doi =		{10.4230/LIPIcs.CONCUR.2021.15},
  annote =	{Keywords: Verification, Distributed algorithms, Domain theory}
}
Document
Short Paper
Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper)

Authors: Sean Braithwaite, Ethan Buchman, Igor Konnov, Zarko Milosevic, Ilina Stoilkovska, Josef Widder, and Anca Zamfir

Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)


Abstract
Blockchain synchronization is one of the core protocols of Tendermint blockchains. In this short paper, we discuss our recent efforts in formal specification of the protocol and its implementation, as well as some initial model checking results. We demonstrate that the protocol quality and understanding can be improved by writing specifications and model checking them.

Cite as

Sean Braithwaite, Ethan Buchman, Igor Konnov, Zarko Milosevic, Ilina Stoilkovska, Josef Widder, and Anca Zamfir. Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper). In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 10:1-10:8, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{braithwaite_et_al:OASIcs.FMBC.2020.10,
  author =	{Braithwaite, Sean and Buchman, Ethan and Konnov, Igor and Milosevic, Zarko and Stoilkovska, Ilina and Widder, Josef and Zamfir, Anca},
  title =	{{Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol}},
  booktitle =	{2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
  pages =	{10:1--10:8},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-169-6},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{84},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.10},
  URN =		{urn:nbn:de:0030-drops-134238},
  doi =		{10.4230/OASIcs.FMBC.2020.10},
  annote =	{Keywords: Blockchain, Fault Tolerance, Byzantine Faults, Model Checking}
}
Document
Long-Run Average Behavior of Vector Addition Systems with States

Authors: Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)


Abstract
A vector addition system with states (VASS) consists of a finite set of states and counters. A configuration is a state and a value for each counter; a transition changes the state and each counter is incremented, decremented, or left unchanged. While qualitative properties such as state and configuration reachability have been studied for VASS, we consider the long-run average cost of infinite computations of VASS. The cost of a configuration is for each state, a linear combination of the counter values. In the special case of uniform cost functions, the linear combination is the same for all states. The (regular) long-run emptiness problem is, given a VASS, a cost function, and a threshold value, if there is a (lasso-shaped) computation such that the long-run average value of the cost function does not exceed the threshold. For uniform cost functions, we show that the regular long-run emptiness problem is (a) decidable in polynomial time for integer-valued VASS, and (b) decidable but nonelementarily hard for natural-valued VASS (i.e., nonnegative counters). For general cost functions, we show that the problem is (c) NP-complete for integer-valued VASS, and (d) undecidable for natural-valued VASS. Our most interesting result is for (c) integer-valued VASS with general cost functions, where we establish a connection between the regular long-run emptiness problem and quadratic Diophantine inequalities. The general (nonregular) long-run emptiness problem is equally hard as the regular problem in all cases except (c), where it remains open.

Cite as

Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Long-Run Average Behavior of Vector Addition Systems with States. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 27:1-27:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{chatterjee_et_al:LIPIcs.CONCUR.2019.27,
  author =	{Chatterjee, Krishnendu and Henzinger, Thomas A. and Otop, Jan},
  title =	{{Long-Run Average Behavior of Vector Addition Systems with States}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{27:1--27:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.27},
  URN =		{urn:nbn:de:0030-drops-109293},
  doi =		{10.4230/LIPIcs.CONCUR.2019.27},
  annote =	{Keywords: vector addition systems, mean-payoff, Diophantine inequalities}
}
Document
Reconfiguration and Message Losses in Parameterized Broadcast Networks

Authors: Nathalie Bertrand, Patricia Bouyer, and Anirban Majumdar

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)


Abstract
Broadcast networks allow one to model networks of identical nodes communicating through message broadcasts. Their parameterized verification aims at proving a property holds for any number of nodes, under any communication topology, and on all possible executions. We focus on the coverability problem which dually asks whether there exists an execution that visits a configuration exhibiting some given state of the broadcast protocol. Coverability is known to be undecidable for static networks, i.e. when the number of nodes and communication topology is fixed along executions. In contrast, it is decidable in PTIME when the communication topology may change arbitrarily along executions, that is for reconfigurable networks. Surprisingly, no lower nor upper bounds on the minimal number of nodes, or the minimal length of covering execution in reconfigurable networks, appear in the literature. In this paper we show tight bounds for cutoff and length, which happen to be linear and quadratic, respectively, in the number of states of the protocol. We also introduce an intermediary model with static communication topology and non-deterministic message losses upon sending. We show that the same tight bounds apply to lossy networks, although, reconfigurable executions may be linearly more succinct than lossy executions. Finally, we show NP-completeness for the natural optimisation problem associated with the cutoff.

Cite as

Nathalie Bertrand, Patricia Bouyer, and Anirban Majumdar. Reconfiguration and Message Losses in Parameterized Broadcast Networks. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 32:1-32:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.CONCUR.2019.32,
  author =	{Bertrand, Nathalie and Bouyer, Patricia and Majumdar, Anirban},
  title =	{{Reconfiguration and Message Losses in Parameterized Broadcast Networks}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{32:1--32:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.32},
  URN =		{urn:nbn:de:0030-drops-109345},
  doi =		{10.4230/LIPIcs.CONCUR.2019.32},
  annote =	{Keywords: model checking, parameterized verification, broadcast networks}
}
Document
Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries

Authors: Nathalie Bertrand, Igor Konnov, Marijana Lazić, and Josef Widder

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)


Abstract
Randomized fault-tolerant distributed algorithms pose a number of challenges for automated verification: (i) parameterization in the number of processes and faults, (ii) randomized choices and probabilistic properties, and (iii) an unbounded number of asynchronous rounds. This combination makes verification hard. Challenge (i) was recently addressed in the framework of threshold automata. We extend threshold automata to model randomized consensus algorithms that perform an unbounded number of asynchronous rounds. For non-probabilistic properties, we show that it is necessary and sufficient to verify these properties under round-rigid schedules, that is, schedules where processes enter round r only after all processes finished round r-1. For almost-sure termination, we analyze these algorithms under round-rigid adversaries, that is, fair adversaries that only generate round-rigid schedules. This allows us to do compositional and inductive reasoning that reduces verification of the asynchronous multi-round algorithms to model checking of a one-round threshold automaton. We apply this framework and automatically verify the following classic algorithms: Ben-Or’s and Bracha’s seminal consensus algorithms for crashes and Byzantine faults, 2-set agreement for crash faults, and RS-Bosco for the Byzantine case.

Cite as

Nathalie Bertrand, Igor Konnov, Marijana Lazić, and Josef Widder. Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 33:1-33:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.CONCUR.2019.33,
  author =	{Bertrand, Nathalie and Konnov, Igor and Lazi\'{c}, Marijana and Widder, Josef},
  title =	{{Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{33:1--33:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.33},
  URN =		{urn:nbn:de:0030-drops-109358},
  doi =		{10.4230/LIPIcs.CONCUR.2019.33},
  annote =	{Keywords: threshold automata, counter systems, parameterized verification, randomized distributed algorithms, Byzantine faults}
}
Document
Complete Volume
LIPIcs, Volume 121, DISC'18, Complete Volume

Authors: Ulrich Schmid and Josef Widder

Published in: LIPIcs, Volume 121, 32nd International Symposium on Distributed Computing (DISC 2018)


Abstract
LIPIcs, Volume 121, DISC'18, Complete Volume

Cite as

Ulrich Schmid and Josef Widder. LIPIcs, Volume 121, DISC'18, Complete Volume. In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@Proceedings{schmid_et_al:LIPIcs.DISC.2018,
  title =	{{LIPIcs, Volume 121, DISC'18, Complete Volume}},
  booktitle =	{32nd International Symposium on Distributed Computing (DISC 2018)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-092-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{121},
  editor =	{Schmid, Ulrich and Widder, Josef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2018},
  URN =		{urn:nbn:de:0030-drops-98456},
  doi =		{10.4230/LIPIcs.DISC.2018},
  annote =	{Keywords: Software and its engineering, Distributed systems organizing principles, Computing methodologies, Distributed computing methodologies}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization, Awards

Authors: Ulrich Schmid and Josef Widder

Published in: LIPIcs, Volume 121, 32nd International Symposium on Distributed Computing (DISC 2018)


Abstract
Front Matter, Table of Contents, Preface, Conference Organization, Awards

Cite as

Ulrich Schmid and Josef Widder. Front Matter, Table of Contents, Preface, Conference Organization, Awards. In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, pp. 0:i-0:xx, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{schmid_et_al:LIPIcs.DISC.2018.0,
  author =	{Schmid, Ulrich and Widder, Josef},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization, Awards}},
  booktitle =	{32nd International Symposium on Distributed Computing (DISC 2018)},
  pages =	{0:i--0:xx},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-092-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{121},
  editor =	{Schmid, Ulrich and Widder, Josef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2018.0},
  URN =		{urn:nbn:de:0030-drops-97899},
  doi =		{10.4230/LIPIcs.DISC.2018.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization, Awards}
}
Document
Invited Talk
Autonomous Vehicles: From Individual Navigation to Challenges of Distributed Swarms (Invited Talk)

Authors: Sándor P. Fekete

Published in: LIPIcs, Volume 121, 32nd International Symposium on Distributed Computing (DISC 2018)


Abstract
Recent years have seen impressive advancements in the development of robots on four wheels: autonomous cars. While much of this progress is owed to a combination of breakthroughs in artificial intelligence and improved sensors, dealing with complex, non-ideal scenarios, where errors or failures can turn out to be catastrophic is still largely unsolved; this will require combining "fast", heuristic approaches of machine learning with "slow", more deliberate methods of discrete algorithms and mathematical optimization. However, many of the real challenges go beyond performance guarantees for individual vehicles and aim at the behavior of swarms: How can we control the complex interaction of a distributed swarm of vehicles, such that the overall behavior can measure up to and go beyond the capabilities of humans? Even though many of our engineering colleagues do not fully realize this yet, there is no doubt that this will have to be based to no small part on expertise in distributed algorithms. I will present a multi-level overview of results and challenges, ranging from information exchanges of small groups all the way to game-theoretic mechanisms for large-scale control. Application scenarios do not just arise from road traffic (where short response times, large numbers of vehicles and individual interests give rise to many difficulties), but also from swarms of autonomous space vehicles (where huge distances, times and energies make distributed methods indispensable).

Cite as

Sándor P. Fekete. Autonomous Vehicles: From Individual Navigation to Challenges of Distributed Swarms (Invited Talk). In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, p. 1:1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{fekete:LIPIcs.DISC.2018.1,
  author =	{Fekete, S\'{a}ndor P.},
  title =	{{Autonomous Vehicles: From Individual Navigation to Challenges of Distributed Swarms}},
  booktitle =	{32nd International Symposium on Distributed Computing (DISC 2018)},
  pages =	{1:1--1:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-092-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{121},
  editor =	{Schmid, Ulrich and Widder, Josef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2018.1},
  URN =		{urn:nbn:de:0030-drops-97904},
  doi =		{10.4230/LIPIcs.DISC.2018.1},
  annote =	{Keywords: Autonomous vehicles, interaction, robot swarms, game theory}
}
Document
Invited Talk
Challenges for Machine Learning on Distributed Platforms (Invited Talk)

Authors: Tom Goldstein

Published in: LIPIcs, Volume 121, 32nd International Symposium on Distributed Computing (DISC 2018)


Abstract
Deep neural networks are trained by solving huge optimization problems with large datasets and millions of variables. On the surface, it seems that the size of these problems makes them a natural target for distributed computing. Despite this, most deep learning research still takes place on a single compute node with a small number of GPUs, and only recently have researchers succeeded in unlocking the power of HPC. In this talk, we'll give a brief overview of how deep networks are trained, and use HPC tools to explore and explain deep network behaviors. Then, we'll explain the problems and challenges that arise when scaling deep nets over large system, and highlight reasons why naive distributed training methods fail. Finally, we'll discuss recent algorithmic innovations that have overcome these limitations, including "big batch" training for tightly coupled clusters and supercomputers, and "variance reduction" strategies to reduce communication in high latency settings.

Cite as

Tom Goldstein. Challenges for Machine Learning on Distributed Platforms (Invited Talk). In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, pp. 2:1-2:3, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{goldstein:LIPIcs.DISC.2018.2,
  author =	{Goldstein, Tom},
  title =	{{Challenges for Machine Learning on Distributed Platforms}},
  booktitle =	{32nd International Symposium on Distributed Computing (DISC 2018)},
  pages =	{2:1--2:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-092-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{121},
  editor =	{Schmid, Ulrich and Widder, Josef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2018.2},
  URN =		{urn:nbn:de:0030-drops-97910},
  doi =		{10.4230/LIPIcs.DISC.2018.2},
  annote =	{Keywords: Machine learning, distributed optimization}
}
Document
Invited Talk
Logical Analysis of Distributed Systems: The Importance of Being Constructive (Invited Talk)

Authors: Michael Mendler

Published in: LIPIcs, Volume 121, 32nd International Symposium on Distributed Computing (DISC 2018)


Abstract
The design and analysis of complex distributed systems proceeds along numerous levels of abstractions. One key abstraction step for reducing complexity is the passage from analog transistor electronics to synchronously clocked digital circuits. This significantly simplifies the modelling from continuous differential equations over the real numbers to discrete Mealy automata over two-valued Boolean algebra. Although typically taken for granted, this step is magic. How do we obtain clock synchronization from asynchronous communication of continuous values? How do we decide on the discrete meaning of continuous signals without a synchronization clock? From a logical perspective, the possibility of synchronization is paradoxical and appears "out of thin air." The chicken-or-egg paradox persists at higher levels abstraction for distributed software. We cannot achieve globally consistent state from local communications without synchronization. At the same time we cannot synchronize without access to globally consistent state. From this perspective, distributed algorithms such as for leader election, consensus or mutual exclusion do not strictly solve their task but merely reduce one synchronization problem to another. This talk revisits the logical justification of the synchronous abstraction claiming that correctness arguments, in so far as they are not merely reductions, must intrinsically depend on reasoning in classical logic. This is studied at the circuit level, where all software reductions must end. The well-known result that some synchronization elements cannot be implemented in delay-insensitive circuits is related to Berry's Thesis according to which digital circuits are delay-insensitive if and only if they are provably correct in constructive logic. More technically, the talk will show how non-inertial delays give rise to a constructive modal logic while inertial delays are inherently non-constructive. This gives a logical explanation for why inertial delays can be used to build arbiters, memory-cells and other synchronization elements, while non-inertial delays are not powerful enough. Though these results are tentative, they indicate the importance of logical constructiveness for metastable-free discrete abstractions of physical behavior. This also indicates that metastability is an unavoidable artifact of the digital abstraction in classical logic.

Cite as

Michael Mendler. Logical Analysis of Distributed Systems: The Importance of Being Constructive (Invited Talk). In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, p. 3:1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{mendler:LIPIcs.DISC.2018.3,
  author =	{Mendler, Michael},
  title =	{{Logical Analysis of Distributed Systems: The Importance of Being Constructive}},
  booktitle =	{32nd International Symposium on Distributed Computing (DISC 2018)},
  pages =	{3:1--3:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-092-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{121},
  editor =	{Schmid, Ulrich and Widder, Josef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2018.3},
  URN =		{urn:nbn:de:0030-drops-97925},
  doi =		{10.4230/LIPIcs.DISC.2018.3},
  annote =	{Keywords: Hardware synchronisation, inertial delays, delay-insensitive circuits, constructive circuits, metastability, constructive modal logic}
}
Document
Selecting a Leader in a Network of Finite State Machines

Authors: Yehuda Afek, Yuval Emek, and Noa Kolikant

Published in: LIPIcs, Volume 121, 32nd International Symposium on Distributed Computing (DISC 2018)


Abstract
This paper studies a variant of the leader election problem under the stone age model (Emek and Wattenhofer, PODC 2013) that considers a network of n randomized finite automata with very weak communication capabilities (a multi-frequency asynchronous generalization of the beeping model's communication scheme). Since solving the classic leader election problem is impossible even in more powerful models, we consider a relaxed variant, referred to as k-leader selection, in which a leader should be selected out of at most k initial candidates. Our main contribution is an algorithm that solves k-leader selection for bounded k in the aforementioned stone age model. On (general topology) graphs of diameter D, this algorithm runs in O~(D) time and succeeds with high probability. The assumption that k is bounded turns out to be unavoidable: we prove that if k = omega (1), then no algorithm in this model can solve k-leader selection with a (positive) constant probability.

Cite as

Yehuda Afek, Yuval Emek, and Noa Kolikant. Selecting a Leader in a Network of Finite State Machines. In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, pp. 4:1-4:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{afek_et_al:LIPIcs.DISC.2018.4,
  author =	{Afek, Yehuda and Emek, Yuval and Kolikant, Noa},
  title =	{{Selecting a Leader in a Network of Finite State Machines}},
  booktitle =	{32nd International Symposium on Distributed Computing (DISC 2018)},
  pages =	{4:1--4:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-092-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{121},
  editor =	{Schmid, Ulrich and Widder, Josef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2018.4},
  URN =		{urn:nbn:de:0030-drops-97933},
  doi =		{10.4230/LIPIcs.DISC.2018.4},
  annote =	{Keywords: stone age model, beeping communication scheme, leader election, k-leader selection, randomized finite state machines, asynchronous scheduler}
}
Document
The Role of A-priori Information in Networks of Rational Agents

Authors: Yehuda Afek, Shaked Rafaeli, and Moshe Sulamy

Published in: LIPIcs, Volume 121, 32nd International Symposium on Distributed Computing (DISC 2018)


Abstract
Until now, distributed algorithms for rational agents have assumed a-priori knowledge of n, the size of the network. This assumption is challenged here by proving how much a-priori knowledge is necessary for equilibrium in different distributed computing problems. Duplication - pretending to be more than one agent - is the main tool used by agents to deviate and increase their utility when not enough knowledge about n is given. We begin by proving that when no information on n is given, equilibrium is impossible for both Coloring and Knowledge Sharing. We then provide new algorithms for both problems when n is a-priori known to all agents. However, what if agents have partial knowledge about n? We provide tight upper and lower bounds that must be a-priori known on n for equilibrium to be possible in Leader Election, Knowledge Sharing, Coloring, Partition and Orientation.

Cite as

Yehuda Afek, Shaked Rafaeli, and Moshe Sulamy. The Role of A-priori Information in Networks of Rational Agents. In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, pp. 5:1-5:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{afek_et_al:LIPIcs.DISC.2018.5,
  author =	{Afek, Yehuda and Rafaeli, Shaked and Sulamy, Moshe},
  title =	{{The Role of A-priori Information in Networks of Rational Agents}},
  booktitle =	{32nd International Symposium on Distributed Computing (DISC 2018)},
  pages =	{5:1--5:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-092-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{121},
  editor =	{Schmid, Ulrich and Widder, Josef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2018.5},
  URN =		{urn:nbn:de:0030-drops-97945},
  doi =		{10.4230/LIPIcs.DISC.2018.5},
  annote =	{Keywords: rational agents, distributed game theory, coloring, knowledge sharing}
}
Document
Distributed Approximate Maximum Matching in the CONGEST Model

Authors: Mohamad Ahmadi, Fabian Kuhn, and Rotem Oshman

Published in: LIPIcs, Volume 121, 32nd International Symposium on Distributed Computing (DISC 2018)


Abstract
We study distributed algorithms for the maximum matching problem in the CONGEST model, where each message must be bounded in size. We give new deterministic upper bounds, and a new lower bound on the problem. We begin by giving a distributed algorithm that computes an exact maximum (unweighted) matching in bipartite graphs, in O(n log n) rounds. Next, we give a distributed algorithm that approximates the fractional weighted maximum matching problem in general graphs. In a graph with maximum degree at most Delta, the algorithm computes a (1-epsilon)-approximation for the problem in time O(log(Delta W)/epsilon^2), where W is a bound on the ratio between the largest and the smallest edge weight. Next, we show a slightly improved and generalized version of the deterministic rounding algorithm of Fischer [DISC '17]. Given a fractional weighted maximum matching solution of value f for a given graph G, we show that in time O((log^2(Delta)+log^*n)/epsilon), the fractional solution can be turned into an integer solution of value at least (1-epsilon)f for bipartite graphs and (1-epsilon) * (g-1)/g * f for general graphs, where g is the length of the shortest odd cycle of G. Together with the above fractional maximum matching algorithm, this implies a deterministic algorithm that computes a (1-epsilon)* (g-1)/g-approximation for the weighted maximum matching problem in time O(log(Delta W)/epsilon^2 + (log^2(Delta)+log^* n)/epsilon). On the lower-bound front, we show that even for unweighted fractional maximum matching in bipartite graphs, computing an (1 - O(1/sqrt{n}))-approximate solution requires at least Omega~(D+sqrt{n}) rounds in CONGEST. This lower bound requires the introduction of a new 2-party communication problem, for which we prove a tight lower bound.

Cite as

Mohamad Ahmadi, Fabian Kuhn, and Rotem Oshman. Distributed Approximate Maximum Matching in the CONGEST Model. In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, pp. 6:1-6:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{ahmadi_et_al:LIPIcs.DISC.2018.6,
  author =	{Ahmadi, Mohamad and Kuhn, Fabian and Oshman, Rotem},
  title =	{{Distributed Approximate Maximum Matching in the CONGEST Model}},
  booktitle =	{32nd International Symposium on Distributed Computing (DISC 2018)},
  pages =	{6:1--6:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-092-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{121},
  editor =	{Schmid, Ulrich and Widder, Josef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2018.6},
  URN =		{urn:nbn:de:0030-drops-97950},
  doi =		{10.4230/LIPIcs.DISC.2018.6},
  annote =	{Keywords: distributed graph algorithms, maximum matching, deterministic rounding, communication complexity}
}
  • Refine by Author
  • 9 Widder, Josef
  • 5 Ghaffari, Mohsen
  • 5 Konnov, Igor
  • 4 Bertrand, Nathalie
  • 4 Kuhn, Fabian
  • Show More...

  • Refine by Classification
  • 24 Theory of computation → Distributed algorithms
  • 12 Theory of computation → Distributed computing models
  • 4 Computing methodologies → Distributed algorithms
  • 4 Networks → Network algorithms
  • 4 Theory of computation → Logic and verification
  • Show More...

  • Refine by Keyword
  • 5 Distributed Graph Algorithms
  • 3 Distributed Algorithms
  • 3 leader election
  • 3 parameterized verification
  • 2 Approximation Algorithms
  • Show More...

  • Refine by Type
  • 64 document
  • 1 volume

  • Refine by Publication Year
  • 57 2018
  • 3 2019
  • 1 2013
  • 1 2015
  • 1 2020
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail