Search Results

Documents authored by Gilbert, G. Nigel



Gilbert, G. Nigel

Document
Social Science Microsimulation: Tools for Modeling, Parameter Optimization, and Sensitivity Analysis (Dagstuhl Seminar 9719)

Authors: G. Nigel Gilbert, Ulrich Mueller, Klaus G. Troitzsch, and Ramzi Suleiman

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)


Abstract

Cite as

G. Nigel Gilbert, Ulrich Mueller, Klaus G. Troitzsch, and Ramzi Suleiman. Social Science Microsimulation: Tools for Modeling, Parameter Optimization, and Sensitivity Analysis (Dagstuhl Seminar 9719). Dagstuhl Seminar Report 177, pp. 1-30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1997)


Copy BibTex To Clipboard

@TechReport{gilbert_et_al:DagSemRep.177,
  author =	{Gilbert, G. Nigel and Mueller, Ulrich and Troitzsch, Klaus G. and Suleiman, Ramzi},
  title =	{{Social Science Microsimulation: Tools for Modeling, Parameter Optimization, and Sensitivity Analysis (Dagstuhl Seminar 9719)}},
  pages =	{1--30},
  ISSN =	{1619-0203},
  year =	{1997},
  type = 	{Dagstuhl Seminar Report},
  number =	{177},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.177},
  URN =		{urn:nbn:de:0030-drops-150647},
  doi =		{10.4230/DagSemRep.177},
}
Document
Social Science Microsimulation: A Challenge for Computer Science (Dagstuhl Seminar 9518)

Authors: Jim Doran, G. Nigel Gilbert, Ulrich Mueller, and Klaus G. Troitzsch

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)


Abstract

Cite as

Jim Doran, G. Nigel Gilbert, Ulrich Mueller, and Klaus G. Troitzsch. Social Science Microsimulation: A Challenge for Computer Science (Dagstuhl Seminar 9518). Dagstuhl Seminar Report 112, pp. 1-27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1995)


Copy BibTex To Clipboard

@TechReport{doran_et_al:DagSemRep.112,
  author =	{Doran, Jim and Gilbert, G. Nigel and Mueller, Ulrich and Troitzsch, Klaus G.},
  title =	{{Social Science Microsimulation: A Challenge for Computer Science (Dagstuhl Seminar 9518)}},
  pages =	{1--27},
  ISSN =	{1619-0203},
  year =	{1995},
  type = 	{Dagstuhl Seminar Report},
  number =	{112},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.112},
  URN =		{urn:nbn:de:0030-drops-150003},
  doi =		{10.4230/DagSemRep.112},
}

Gilbert, David

Document
Multiscale Spatial Computational Systems Biology (Dagstuhl Seminar 14481)

Authors: David Gilbert, Monika Heiner, Koichi Takahashi, and Adelinde M. Uhrmacher

Published in: Dagstuhl Reports, Volume 4, Issue 11 (2015)


Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 14481 "Multiscale Spatial Computational Systems Biology". This seminar explored challenges arising from the need to model and analyse complex biological systems at multiple scales (spatial and temporal), which falls within the general remit of Computational Systems Biology. A distinguishing factor of the seminar was the modelling exercise -- where teams explored different modelling paradigms, in order to better understand the details of the approaches, their challenges, potential applications, and their pros and cons. This activity was carried out in a collaborative and self-directed manner using the Open Space Technology approach as evidenced by a high degree of communication both within and between the teams. Eight teams were formed, and reports from five of them are included in this document.

Cite as

David Gilbert, Monika Heiner, Koichi Takahashi, and Adelinde M. Uhrmacher. Multiscale Spatial Computational Systems Biology (Dagstuhl Seminar 14481). In Dagstuhl Reports, Volume 4, Issue 11, pp. 138-226, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@Article{gilbert_et_al:DagRep.4.11.138,
  author =	{Gilbert, David and Heiner, Monika and Takahashi, Koichi and Uhrmacher, Adelinde M.},
  title =	{{Multiscale Spatial Computational Systems Biology (Dagstuhl Seminar 14481)}},
  pages =	{138--226},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{4},
  number =	{11},
  editor =	{Gilbert, David and Heiner, Monika and Takahashi, Koichi and Uhrmacher, Adelinde M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.4.11.138},
  URN =		{urn:nbn:de:0030-drops-49723},
  doi =		{10.4230/DagRep.4.11.138},
  annote =	{Keywords: Multiscale, multidimensional, computational modelling, space, time, systems biology, synthetic biology}
}
Document
Computational Biology (Dagstuhl Seminar 02471)

Authors: Ross B. Altman, David Gilbert, and Thomas Lengauer

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)


Abstract

Cite as

Ross B. Altman, David Gilbert, and Thomas Lengauer. Computational Biology (Dagstuhl Seminar 02471). Dagstuhl Seminar Report 360, pp. 1-30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2003)


Copy BibTex To Clipboard

@TechReport{altman_et_al:DagSemRep.360,
  author =	{Altman, Ross B. and Gilbert, David and Lengauer, Thomas},
  title =	{{Computational Biology (Dagstuhl Seminar 02471)}},
  pages =	{1--30},
  ISSN =	{1619-0203},
  year =	{2003},
  type = 	{Dagstuhl Seminar Report},
  number =	{360},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.360},
  URN =		{urn:nbn:de:0030-drops-152405},
  doi =		{10.4230/DagSemRep.360},
}

Gilbert, Henri

Document
QUAD: Overview and Recent Developments

Authors: David Arditti, Côme Berbain, Olivier Billet, Henri Gilbert, and Jacques Patarin

Published in: Dagstuhl Seminar Proceedings, Volume 7021, Symmetric Cryptography (2007)


Abstract
We give an outline of the specification and provable security features of the QUAD stream cipher proposed at Eurocrypt 2006. The cipher relies on the iteration of a multivariate system of quadratic equations over a finite field, typically GF(2) or a small extension. In the binary case, the security of the keystream generation can be related, in the concrete security model, to the conjectured intractability of the MQ problem of solving a random system of m equations in n unknowns. We show that this security reduction can be extended to incorporate the key and IV setup and provide a security argument related to the whole stream cipher.We also briefly address software and hardware performance issues and show that if one is willing to pseudorandomly generate the systems of quadratic polynomials underlying the cipher, this leads to suprisingly inexpensive hardware implementations of QUAD.

Cite as

David Arditti, Côme Berbain, Olivier Billet, Henri Gilbert, and Jacques Patarin. QUAD: Overview and Recent Developments. In Symmetric Cryptography. Dagstuhl Seminar Proceedings, Volume 7021, pp. 1-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)


Copy BibTex To Clipboard

@InProceedings{arditti_et_al:DagSemProc.07021.9,
  author =	{Arditti, David and Berbain, C\^{o}me and Billet, Olivier and Gilbert, Henri and Patarin, Jacques},
  title =	{{QUAD: Overview and Recent Developments}},
  booktitle =	{Symmetric Cryptography},
  pages =	{1--20},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{7021},
  editor =	{Eli Biham and Helena Handschuh and Stefan Lucks and Vincent Rijmen},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07021.9},
  URN =		{urn:nbn:de:0030-drops-10155},
  doi =		{10.4230/DagSemProc.07021.9},
  annote =	{Keywords: MQ problem, stream cipher, provable security, Gr\~{A}ƒ\^{A}¶bner basis}
}

Gilbert, David Roger

Document
09091 Abstracts Collection – Formal Methods in Molecular Biology

Authors: Rainer Breitling, David Roger Gilbert, Monika Heiner, and Corrado Priami

Published in: Dagstuhl Seminar Proceedings, Volume 9091, Formal Methods in Molecular Biology (2009)


Abstract
From 23. February to 27. February 2009, the Dagstuhl Seminar 09091 ``Formal Methods in Molecular Biology '' was held in Schloss Dagstuhl~--~Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.

Cite as

Rainer Breitling, David Roger Gilbert, Monika Heiner, and Corrado Priami. 09091 Abstracts Collection – Formal Methods in Molecular Biology. In Formal Methods in Molecular Biology. Dagstuhl Seminar Proceedings, Volume 9091, pp. 1-24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)


Copy BibTex To Clipboard

@InProceedings{breitling_et_al:DagSemProc.09091.1,
  author =	{Breitling, Rainer and Gilbert, David Roger and Heiner, Monika and Priami, Corrado},
  title =	{{09091 Abstracts Collection – Formal Methods in Molecular Biology }},
  booktitle =	{Formal Methods in Molecular Biology},
  pages =	{1--24},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{9091},
  editor =	{Rainer Breitling and David Roger Gilbert and Monika Heiner and Corrado Priami},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09091.1},
  URN =		{urn:nbn:de:0030-drops-19972},
  doi =		{10.4230/DagSemProc.09091.1},
  annote =	{Keywords: Formal models, systems biology, biological processes}
}
Document
09091 Executive Summary – Formal Methods in Molecular Biology

Authors: Rainer Breitling, David Roger Gilbert, Monika Heiner, and Corrado Priami

Published in: Dagstuhl Seminar Proceedings, Volume 9091, Formal Methods in Molecular Biology (2009)


Abstract
Formal logical models play an increasing role in the newly emerging field of Systems Biology. Compared to the classical, well-established approach of modeling biological processes using continuous and stochastic differential equations, formal logical models offer a number of important advantages. Many different formal modeling paradigms have been applied to molecular biology, each with its own community, formalisms and tools. In this seminar we brought together modelers from various backgrounds to stimulate closer interaction within the field and to create a common platform for discussion. A central feature of the seminar was a modeling competition (with a highly collaborative flavor) of various modeling paradigms.

Cite as

Rainer Breitling, David Roger Gilbert, Monika Heiner, and Corrado Priami. 09091 Executive Summary – Formal Methods in Molecular Biology. In Formal Methods in Molecular Biology. Dagstuhl Seminar Proceedings, Volume 9091, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)


Copy BibTex To Clipboard

@InProceedings{breitling_et_al:DagSemProc.09091.2,
  author =	{Breitling, Rainer and Gilbert, David Roger and Heiner, Monika and Priami, Corrado},
  title =	{{09091 Executive Summary – Formal Methods in Molecular Biology}},
  booktitle =	{Formal Methods in Molecular Biology},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{9091},
  editor =	{Rainer Breitling and David Roger Gilbert and Monika Heiner and Corrado Priami},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09091.2},
  URN =		{urn:nbn:de:0030-drops-19964},
  doi =		{10.4230/DagSemProc.09091.2},
  annote =	{Keywords: Formal models, systems biology, biological processes.}
}
Document
BioModel Engineering: Its role in Systems Biology and Synthetic Biology

Authors: David Roger Gilbert, Rainer Breitling, and Monika Heiner

Published in: Dagstuhl Seminar Proceedings, Volume 9091, Formal Methods in Molecular Biology (2009)


Abstract
BioModel Engineering takes place at the interface of computing science, mathematics, engineering and biology, and provides a systematic approach for designing, constructing and analyzing computational models of biological systems. Some of its central concepts are inspired by efficient software engineering strategies. BioModel Engineering does not aim at engineering biological systems per se, but rather aims at describing their structure and behavior, in particular at the level of intracellular molecular processes, using computational tools and techniques in a principled way. The two major application areas of BioModel Engineering are systems biology and synthetic biology. In the former, the aim is the design and construction of models of existing biological systems, which explain observed properties and predict the response to experimental interventions; in the latter, BioModel Engineering is used as part of a general strategy for designing and constructing synthetic biological systems with novel functionalities. The overall steps in building computational models in a BioModel Engineering framework are: Problem Identification, Model Construction, Static and Dynamic Analysis, Simulation, and Model management and development. A major theme in BioModel Engineering is that of constructing a (qualitative) model means (1) finding the structure, (2) obtaining an initial state and (3) parameter fitting. In an approach that we have taken, the structure is obtained by piecewise construction of models from modular parts, the initial state which describes concentrations of species or numbers of molecules is obtained by analysis of the structure, and parameter fitting comprises determining the rate parameters of the kinetic equations by reference to trusted data. Model checking can play a key role in BioModel Engineering – for example in recent work we have shown how parameter estimation can be achieved by characterising the desired behaviour of a model with a temporal logic property and altering the model to make it conform to the property as determined through model checking.

Cite as

David Roger Gilbert, Rainer Breitling, and Monika Heiner. BioModel Engineering: Its role in Systems Biology and Synthetic Biology. In Formal Methods in Molecular Biology. Dagstuhl Seminar Proceedings, Volume 9091, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)


Copy BibTex To Clipboard

@InProceedings{gilbert_et_al:DagSemProc.09091.4,
  author =	{Gilbert, David Roger and Breitling, Rainer and Heiner, Monika},
  title =	{{BioModel Engineering: Its role in Systems Biology and Synthetic Biology}},
  booktitle =	{Formal Methods in Molecular Biology},
  pages =	{1--2},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{9091},
  editor =	{Rainer Breitling and David Roger Gilbert and Monika Heiner and Corrado Priami},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09091.4},
  URN =		{urn:nbn:de:0030-drops-19929},
  doi =		{10.4230/DagSemProc.09091.4},
  annote =	{Keywords: Biochemical systems, models, design, construction, systems biology, synthetic biology, model checking.}
}

Gilbert, Seth

Document
Efficient Signature-Free Validated Agreement

Authors: Pierre Civit, Muhammad Ayaz Dzulfikar, Seth Gilbert, Rachid Guerraoui, Jovan Komatovic, Manuel Vidigueira, and Igor Zablotchi

Published in: LIPIcs, Volume 319, 38th International Symposium on Distributed Computing (DISC 2024)


Abstract
Byzantine agreement enables n processes to agree on a common L-bit value, despite up to t > 0 arbitrary failures. A long line of work has been dedicated to improving the bit complexity of Byzantine agreement in synchrony. This has culminated in COOL, an error-free (deterministically secure against a computationally unbounded adversary) solution that achieves O(nL + n² log n) worst-case bit complexity (which is optimal for L ≥ n log n according to the Dolev-Reischuk lower bound). COOL satisfies strong unanimity: if all correct processes propose the same value, only that value can be decided. Whenever correct processes do not agree a priori (there is no unanimity), they may decide a default value ⊥ from COOL. Strong unanimity is, however, not sufficient for today’s state machine replication (SMR) and blockchain protocols. These systems value progress and require a decided value to always be valid (according to a predetermined predicate), excluding default decisions (such as ⊥) even in cases where there is no unanimity a priori. Validated Byzantine agreement satisfies this property (called external validity). Yet, the best error-free (or even signature-free) validated agreement solutions achieve only O(n²L) bit complexity, a far cry from the Ω(nL+n²) Dolev-Reischuk lower bound. Is it possible to bridge this complexity gap? We answer the question affirmatively. Namely, we present two new synchronous algorithms for validated Byzantine agreement, HashExt and ErrorFreeExt, with different trade-offs. Both algorithms are (1) signature-free, (2) optimally resilient (tolerate up to t < n / 3 failures), and (3) early-stopping (terminate in O(f+1) rounds, where f ≤ t denotes the actual number of failures). On the one hand, HashExt uses only hashes and achieves O(nL + n³κ) bit complexity, which is optimal for L ≥ n²κ (where κ is the size of a hash). On the other hand, ErrorFreeExt is error-free, using no cryptography whatsoever, and achieves O((nL + n²)log n) bit complexity, which is near-optimal for any L.

Cite as

Pierre Civit, Muhammad Ayaz Dzulfikar, Seth Gilbert, Rachid Guerraoui, Jovan Komatovic, Manuel Vidigueira, and Igor Zablotchi. Efficient Signature-Free Validated Agreement. In 38th International Symposium on Distributed Computing (DISC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 319, pp. 14:1-14:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{civit_et_al:LIPIcs.DISC.2024.14,
  author =	{Civit, Pierre and Dzulfikar, Muhammad Ayaz and Gilbert, Seth and Guerraoui, Rachid and Komatovic, Jovan and Vidigueira, Manuel and Zablotchi, Igor},
  title =	{{Efficient Signature-Free Validated Agreement}},
  booktitle =	{38th International Symposium on Distributed Computing (DISC 2024)},
  pages =	{14:1--14:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-352-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{319},
  editor =	{Alistarh, Dan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2024.14},
  URN =		{urn:nbn:de:0030-drops-212408},
  doi =		{10.4230/LIPIcs.DISC.2024.14},
  annote =	{Keywords: Validated Byzantine agreement, Bit complexity, Round complexity}
}
Document
Every Bit Counts in Consensus

Authors: Pierre Civit, Seth Gilbert, Rachid Guerraoui, Jovan Komatovic, Matteo Monti, and Manuel Vidigueira

Published in: LIPIcs, Volume 281, 37th International Symposium on Distributed Computing (DISC 2023)


Abstract
Consensus enables n processes to agree on a common valid L-bit value, despite t < n/3 processes being faulty and acting arbitrarily. A long line of work has been dedicated to improving the worst-case communication complexity of consensus in partial synchrony. This has recently culminated in the worst-case word complexity of O(n²). However, the worst-case bit complexity of the best solution is still O(n²L + n²κ) (where κ is the security parameter), far from the Ω(nL + n²) lower bound. The gap is significant given the practical use of consensus primitives, where values typically consist of batches of large size (L > n). This paper shows how to narrow the aforementioned gap. Namely, we present a new algorithm, DARE (Disperse, Agree, REtrieve), that improves upon the O(n²L) term via a novel dispersal primitive. DARE achieves O(n^{1.5}L + n^{2.5}κ) bit complexity, an effective √n-factor improvement over the state-of-the-art (when L > nκ). Moreover, we show that employing heavier cryptographic primitives, namely STARK proofs, allows us to devise DARE-Stark, a version of DARE which achieves the near-optimal bit complexity of O(nL + n²poly(κ)). Both DARE and DARE-Stark achieve optimal O(n) worst-case latency.

Cite as

Pierre Civit, Seth Gilbert, Rachid Guerraoui, Jovan Komatovic, Matteo Monti, and Manuel Vidigueira. Every Bit Counts in Consensus. In 37th International Symposium on Distributed Computing (DISC 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 281, pp. 13:1-13:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{civit_et_al:LIPIcs.DISC.2023.13,
  author =	{Civit, Pierre and Gilbert, Seth and Guerraoui, Rachid and Komatovic, Jovan and Monti, Matteo and Vidigueira, Manuel},
  title =	{{Every Bit Counts in Consensus}},
  booktitle =	{37th International Symposium on Distributed Computing (DISC 2023)},
  pages =	{13:1--13:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-301-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{281},
  editor =	{Oshman, Rotem},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2023.13},
  URN =		{urn:nbn:de:0030-drops-191399},
  doi =		{10.4230/LIPIcs.DISC.2023.13},
  annote =	{Keywords: Byzantine consensus, Bit complexity, Latency}
}
Document
Byzantine Consensus Is Θ(n²): The Dolev-Reischuk Bound Is Tight Even in Partial Synchrony!

Authors: Pierre Civit, Muhammad Ayaz Dzulfikar, Seth Gilbert, Vincent Gramoli, Rachid Guerraoui, Jovan Komatovic, and Manuel Vidigueira

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


Abstract
The Dolev-Reischuk bound says that any deterministic Byzantine consensus protocol has (at least) quadratic communication complexity in the worst case. While it has been shown that the bound is tight in synchronous environments, it is still unknown whether a consensus protocol with quadratic communication complexity can be obtained in partial synchrony. Until now, the most efficient known solutions for Byzantine consensus in partially synchronous settings had cubic communication complexity (e.g., HotStuff, binary DBFT). This paper closes the existing gap by introducing SQuad, a partially synchronous Byzantine consensus protocol with quadratic worst-case communication complexity. In addition, SQuad is optimally-resilient and achieves linear worst-case latency complexity. The key technical contribution underlying SQuad lies in the way we solve view synchronization, the problem of bringing all correct processes to the same view with a correct leader for sufficiently long. Concretely, we present RareSync, a view synchronization protocol with quadratic communication complexity and linear latency complexity, which we utilize in order to obtain SQuad.

Cite as

Pierre Civit, Muhammad Ayaz Dzulfikar, Seth Gilbert, Vincent Gramoli, Rachid Guerraoui, Jovan Komatovic, and Manuel Vidigueira. Byzantine Consensus Is Θ(n²): The Dolev-Reischuk Bound Is Tight Even in Partial Synchrony!. In 36th International Symposium on Distributed Computing (DISC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 246, pp. 14:1-14:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{civit_et_al:LIPIcs.DISC.2022.14,
  author =	{Civit, Pierre and Dzulfikar, Muhammad Ayaz and Gilbert, Seth and Gramoli, Vincent and Guerraoui, Rachid and Komatovic, Jovan and Vidigueira, Manuel},
  title =	{{Byzantine Consensus Is \Theta(n²): The Dolev-Reischuk Bound Is Tight Even in Partial Synchrony!}},
  booktitle =	{36th International Symposium on Distributed Computing (DISC 2022)},
  pages =	{14:1--14:21},
  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.14},
  URN =		{urn:nbn:de:0030-drops-172059},
  doi =		{10.4230/LIPIcs.DISC.2022.14},
  annote =	{Keywords: Optimal Byzantine consensus, Communication complexity, Latency complexity}
}
Document
Smoothed Analysis of Information Spreading in Dynamic Networks

Authors: Michael Dinitz, Jeremy Fineman, Seth Gilbert, and Calvin Newport

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


Abstract
The best known solutions for k-message broadcast in dynamic networks of size n require Ω(nk) rounds. In this paper, we see if these bounds can be improved by smoothed analysis. To do so, we study perhaps the most natural randomized algorithm for disseminating tokens in this setting: at every time step, choose a token to broadcast randomly from the set of tokens you know. We show that with even a small amount of smoothing (i.e., one random edge added per round), this natural strategy solves k-message broadcast in Õ(n+k³) rounds, with high probability, beating the best known bounds for k = o(√n) and matching the Ω(n+k) lower bound for static networks for k = O(n^{1/3}) (ignoring logarithmic factors). In fact, the main result we show is even stronger and more general: given 𝓁-smoothing (i.e., 𝓁 random edges added per round), this simple strategy terminates in O(kn^{2/3}log^{1/3}(n)𝓁^{-1/3}) rounds. We then prove this analysis close to tight with an almost-matching lower bound. To better understand the impact of smoothing on information spreading, we next turn our attention to static networks, proving a tight bound of Õ(k√n) rounds to solve k-message broadcast, which is better than what our strategy can achieve in the dynamic setting. This confirms the intuition that although smoothed analysis reduces the difficulties induced by changing graph structures, it does not eliminate them altogether. Finally, we apply tools developed to support our smoothed analysis to prove an optimal result for k-message broadcast in so-called well-mixed networks in the absence of smoothing. By comparing this result to an existing lower bound for well-mixed networks, we establish a formal separation between oblivious and strongly adaptive adversaries with respect to well-mixed token spreading, partially resolving an open question on the impact of adversary strength on the k-message broadcast problem.

Cite as

Michael Dinitz, Jeremy Fineman, Seth Gilbert, and Calvin Newport. Smoothed Analysis of Information Spreading in Dynamic Networks. In 36th International Symposium on Distributed Computing (DISC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 246, pp. 18:1-18:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{dinitz_et_al:LIPIcs.DISC.2022.18,
  author =	{Dinitz, Michael and Fineman, Jeremy and Gilbert, Seth and Newport, Calvin},
  title =	{{Smoothed Analysis of Information Spreading in Dynamic Networks}},
  booktitle =	{36th International Symposium on Distributed Computing (DISC 2022)},
  pages =	{18:1--18:22},
  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.18},
  URN =		{urn:nbn:de:0030-drops-172094},
  doi =		{10.4230/LIPIcs.DISC.2022.18},
  annote =	{Keywords: Smoothed Analysis, Dynamic networks, Gossip}
}
Document
Complete Volume
LIPIcs, Volume 209, DISC 2021, Complete Volume

Authors: Seth Gilbert

Published in: LIPIcs, Volume 209, 35th International Symposium on Distributed Computing (DISC 2021)


Abstract
LIPIcs, Volume 209, DISC 2021, Complete Volume

Cite as

35th International Symposium on Distributed Computing (DISC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 209, pp. 1-860, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@Proceedings{gilbert:LIPIcs.DISC.2021,
  title =	{{LIPIcs, Volume 209, DISC 2021, Complete Volume}},
  booktitle =	{35th International Symposium on Distributed Computing (DISC 2021)},
  pages =	{1--860},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-210-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{209},
  editor =	{Gilbert, Seth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2021},
  URN =		{urn:nbn:de:0030-drops-148015},
  doi =		{10.4230/LIPIcs.DISC.2021},
  annote =	{Keywords: LIPIcs, Volume 209, DISC 2021, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Seth Gilbert

Published in: LIPIcs, Volume 209, 35th International Symposium on Distributed Computing (DISC 2021)


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

Cite as

35th International Symposium on Distributed Computing (DISC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 209, pp. 0:i-0:xxii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{gilbert:LIPIcs.DISC.2021.0,
  author =	{Gilbert, Seth},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{35th International Symposium on Distributed Computing (DISC 2021)},
  pages =	{0:i--0:xxii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-210-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{209},
  editor =	{Gilbert, Seth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2021.0},
  URN =		{urn:nbn:de:0030-drops-148028},
  doi =		{10.4230/LIPIcs.DISC.2021.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Brief Announcement
Brief Announcement: Polygraph: Accountable Byzantine Agreement

Authors: Pierre Civit, Seth Gilbert, and Vincent Gramoli

Published in: LIPIcs, Volume 179, 34th International Symposium on Distributed Computing (DISC 2020)


Abstract
In this paper, we introduce Polygraph, the first accountable Byzantine consensus algorithm. If among n users f < n/3 are malicious then it ensures consensus, otherwise it eventually detects malicious users that cause disagreement. Polygraph is appealing for blockchains as it allows to totally order blocks in a chain whenever possible, hence avoiding double spending and, otherwise, to punish at least n/3 malicious users when a fork occurs. This problem is more difficult than it first appears. Blockchains typically run in open networks whose delays are hard to predict, hence one cannot build upon synchronous techniques [Andreas Haeberlen et al., 2007; Vitalik Buterin and Virgil Griffith, 2019]. One may exploit cryptographic evidence of PBFT-like consensus [Miguel Castro and Barbara Liskov, 2002], however detecting equivocation would be insufficient. We show that it is impossible without extra logs of at least Ω(n) rounds [Pierre Civit et al., 2019]. Each round of Polygraph exchanges O(n²) messages.

Cite as

Pierre Civit, Seth Gilbert, and Vincent Gramoli. Brief Announcement: Polygraph: Accountable Byzantine Agreement. In 34th International Symposium on Distributed Computing (DISC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 179, pp. 45:1-45:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{civit_et_al:LIPIcs.DISC.2020.45,
  author =	{Civit, Pierre and Gilbert, Seth and Gramoli, Vincent},
  title =	{{Brief Announcement: Polygraph: Accountable Byzantine Agreement}},
  booktitle =	{34th International Symposium on Distributed Computing (DISC 2020)},
  pages =	{45:1--45:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-168-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{179},
  editor =	{Attiya, Hagit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2020.45},
  URN =		{urn:nbn:de:0030-drops-131236},
  doi =		{10.4230/LIPIcs.DISC.2020.45},
  annote =	{Keywords: Fault detection, cryptography, equivocation, consensus}
}
Document
Complete Volume
LIPIcs, Vol. 153, OPODIS 2019, Complete Volume

Authors: Pascal Felber, Roy Friedman, Seth Gilbert, and Avery Miller

Published in: LIPIcs, Volume 153, 23rd International Conference on Principles of Distributed Systems (OPODIS 2019)


Abstract
LIPIcs, Vol. 153, OPODIS 2019, Complete Volume

Cite as

23rd International Conference on Principles of Distributed Systems (OPODIS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 153, pp. 1-564, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@Proceedings{felber_et_al:LIPIcs.OPODIS.2019,
  title =	{{LIPIcs, Vol. 153, OPODIS 2019, Complete Volume}},
  booktitle =	{23rd International Conference on Principles of Distributed Systems (OPODIS 2019)},
  pages =	{1--564},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-133-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{153},
  editor =	{Felber, Pascal and Friedman, Roy and Gilbert, Seth and Miller, Avery},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2019},
  URN =		{urn:nbn:de:0030-drops-119510},
  doi =		{10.4230/LIPIcs.OPODIS.2019},
  annote =	{Keywords: LIPIcs, Vol. 153, OPODIS 2019, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Pascal Felber, Roy Friedman, Seth Gilbert, and Avery Miller

Published in: LIPIcs, Volume 153, 23rd International Conference on Principles of Distributed Systems (OPODIS 2019)


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

Cite as

23rd International Conference on Principles of Distributed Systems (OPODIS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 153, pp. 0:i-0:xxii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{felber_et_al:LIPIcs.OPODIS.2019.0,
  author =	{Felber, Pascal and Friedman, Roy and Gilbert, Seth and Miller, Avery},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{23rd International Conference on Principles of Distributed Systems (OPODIS 2019)},
  pages =	{0:i--0:xxii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-133-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{153},
  editor =	{Felber, Pascal and Friedman, Roy and Gilbert, Seth and Miller, Avery},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2019.0},
  URN =		{urn:nbn:de:0030-drops-117869},
  doi =		{10.4230/LIPIcs.OPODIS.2019.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
On Bioelectric Algorithms

Authors: Seth Gilbert, James Maguire, and Calvin Newport

Published in: LIPIcs, Volume 146, 33rd International Symposium on Distributed Computing (DISC 2019)


Abstract
Cellular bioelectricity describes the biological phenomenon in which cells in living tissue generate and maintain patterns of voltage gradients across their membranes induced by differing concentrations of charged ions. A growing body of research suggests that bioelectric patterns represent an ancient system that plays a key role in guiding many important developmental processes including tissue regeneration, tumor suppression, and embryogenesis. This paper applies techniques from distributed algorithm theory to help better understand how cells work together to form these patterns. To do so, we present the cellular bioelectric model (CBM), a new computational model that captures the primary capabilities and constraints of bioelectric interactions between cells and their environment. We use this model to investigate several important topics from the relevant biology research literature. We begin with symmetry breaking, analyzing a simple cell definition that when combined in single hop or multihop topologies, efficiently solves leader election and the maximal independent set problem, respectively - indicating that these classical symmetry breaking tasks are well-matched to bioelectric mechanisms. We then turn our attention to the information processing ability of bioelectric cells, exploring upper and lower bounds for approximate solutions to threshold and majority detection, and then proving that these systems are in fact Turing complete - resolving an open question about the computational power of bioelectric interactions.

Cite as

Seth Gilbert, James Maguire, and Calvin Newport. On Bioelectric Algorithms. In 33rd International Symposium on Distributed Computing (DISC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 146, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{gilbert_et_al:LIPIcs.DISC.2019.19,
  author =	{Gilbert, Seth and Maguire, James and Newport, Calvin},
  title =	{{On Bioelectric Algorithms}},
  booktitle =	{33rd International Symposium on Distributed Computing (DISC 2019)},
  pages =	{19:1--19:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-126-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{146},
  editor =	{Suomela, Jukka},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2019.19},
  URN =		{urn:nbn:de:0030-drops-113267},
  doi =		{10.4230/LIPIcs.DISC.2019.19},
  annote =	{Keywords: biological distributed algorithms, bioelectric networks, natural algorithms}
}
Document
Parallel Finger Search Structures

Authors: Seth Gilbert and Wei Quan Lim

Published in: LIPIcs, Volume 146, 33rd International Symposium on Distributed Computing (DISC 2019)


Abstract
In this paper we present two versions of a parallel finger structure FS on p processors that supports searches, insertions and deletions, and has a finger at each end. This is to our knowledge the first implementation of a parallel search structure that is work-optimal with respect to the finger bound and yet has very good parallelism (within a factor of O(log p)^2) of optimal). We utilize an extended implicit batching framework that transparently facilitates the use of FS by any parallel program P that is modelled by a dynamically generated DAG D where each node is either a unit-time instruction or a call to FS. The work done by FS is bounded by the finger bound F_L (for some linearization L of D), i.e. each operation on an item with distance r from a finger takes O(log r+1) amortized work. Running P using the simpler version takes O((T_1+F_L)/p + T_infty + d * ((log p)^2 + log n)) time on a greedy scheduler, where T_1, T_infty are the size and span of D respectively, and n is the maximum number of items in FS, and d is the maximum number of calls to FS along any path in D. Using the faster version, this is reduced to O((T_1+F_L)/p + T_infty + d *(log p)^2 + s_L) time, where s_L is the weighted span of D where each call to FS is weighted by its cost according to F_L. FS can be extended to a fixed number of movable fingers. The data structures in our paper fit into the dynamic multithreading paradigm, and their performance bounds are directly composable with other data structures given in the same paradigm. Also, the results can be translated to practical implementations using work-stealing schedulers.

Cite as

Seth Gilbert and Wei Quan Lim. Parallel Finger Search Structures. In 33rd International Symposium on Distributed Computing (DISC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 146, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{gilbert_et_al:LIPIcs.DISC.2019.20,
  author =	{Gilbert, Seth and Lim, Wei Quan},
  title =	{{Parallel Finger Search Structures}},
  booktitle =	{33rd International Symposium on Distributed Computing (DISC 2019)},
  pages =	{20:1--20:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-126-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{146},
  editor =	{Suomela, Jukka},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2019.20},
  URN =		{urn:nbn:de:0030-drops-113275},
  doi =		{10.4230/LIPIcs.DISC.2019.20},
  annote =	{Keywords: Parallel data structures, Multithreading, Dictionaries, Comparison-based Search, Distribution-sensitive algorithms}
}
Document
Track C: Foundations of Networks and Multi-Agent Systems: Models, Algorithms and Information Management
Periodic Bandits and Wireless Network Selection

Authors: Shunhao Oh, Anuja Meetoo Appavoo, and Seth Gilbert

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)


Abstract
Bandit-style algorithms have been studied extensively in stochastic and adversarial settings. Such algorithms have been shown to be useful in multiplayer settings, e.g. to solve the wireless network selection problem, which can be formulated as an adversarial bandit problem. A leading bandit algorithm for the adversarial setting is EXP3. However, network behavior is often repetitive, where user density and network behavior follow regular patterns. Bandit algorithms, like EXP3, fail to provide good guarantees for periodic behaviors. A major reason is that these algorithms compete against fixed-action policies, which is ineffective in a periodic setting. In this paper, we define a periodic bandit setting, and periodic regret as a better performance measure for this type of setting. Instead of comparing an algorithm’s performance to fixed-action policies, we aim to be competitive with policies that play arms under some set of possible periodic patterns F (for example, all possible periodic functions with periods 1,2,*s,P). We propose Periodic EXP4, a computationally efficient variant of the EXP4 algorithm for periodic settings. With K arms, T time steps, and where each periodic pattern in F is of length at most P, we show that the periodic regret obtained by Periodic EXP4 is at most O(sqrt{PKT log K + KT log |F|}). We also prove a lower bound of Omega (sqrt{PKT + KT {log |F|}/{log K}}) for the periodic setting, showing that this is optimal within log-factors. As an example, we focus on the wireless network selection problem. Through simulation, we show that Periodic EXP4 learns the periodic pattern over time, adapts to changes in a dynamic environment, and far outperforms EXP3.

Cite as

Shunhao Oh, Anuja Meetoo Appavoo, and Seth Gilbert. Periodic Bandits and Wireless Network Selection. In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 149:1-149:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{oh_et_al:LIPIcs.ICALP.2019.149,
  author =	{Oh, Shunhao and Appavoo, Anuja Meetoo and Gilbert, Seth},
  title =	{{Periodic Bandits and Wireless Network Selection}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{149:1--149:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.149},
  URN =		{urn:nbn:de:0030-drops-107251},
  doi =		{10.4230/LIPIcs.ICALP.2019.149},
  annote =	{Keywords: multi-armed bandits, wireless network selection, periodicity in environment}
}
Document
On Simple Back-Off in Unreliable Radio Networks

Authors: Seth Gilbert, Nancy Lynch, Calvin Newport, and Dominik Pajak

Published in: LIPIcs, Volume 125, 22nd International Conference on Principles of Distributed Systems (OPODIS 2018)


Abstract
In this paper, we study local and global broadcast in the dual graph model, which describes communication in a radio network with both reliable and unreliable links. Existing work proved that efficient solutions to these problems are impossible in the dual graph model under standard assumptions. In real networks, however, simple back-off strategies tend to perform well for solving these basic communication tasks. We address this apparent paradox by introducing a new set of constraints to the dual graph model that better generalize the slow/fast fading behavior common in real networks. We prove that in the context of these new constraints, simple back-off strategies now provide efficient solutions to local and global broadcast in the dual graph model. We also precisely characterize how this efficiency degrades as the new constraints are reduced down to non-existent, and prove new lower bounds that establish this degradation as near optimal for a large class of natural algorithms. We conclude with an analysis of a more general model where we propose an enhanced back-off algorithm. These results provide theoretical foundations for the practical observation that simple back-off algorithms tend to work well even amid the complicated link dynamics of real radio networks.

Cite as

Seth Gilbert, Nancy Lynch, Calvin Newport, and Dominik Pajak. On Simple Back-Off in Unreliable Radio Networks. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{gilbert_et_al:LIPIcs.OPODIS.2018.27,
  author =	{Gilbert, Seth and Lynch, Nancy and Newport, Calvin and Pajak, Dominik},
  title =	{{On Simple Back-Off in Unreliable Radio Networks}},
  booktitle =	{22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
  pages =	{27:1--27:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-098-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{125},
  editor =	{Cao, Jiannong and Ellen, Faith and Rodrigues, Luis and Ferreira, Bernardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2018.27},
  URN =		{urn:nbn:de:0030-drops-100877},
  doi =		{10.4230/LIPIcs.OPODIS.2018.27},
  annote =	{Keywords: radio networks, broadcast, unreliable links, distributed algorithm, robustness}
}
Document
Brief Announcement
Brief Announcement: On Simple Back-Off in Unreliable Radio Networks

Authors: Seth Gilbert, Nancy Lynch, Calvin Newport, and Dominik Pajak

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


Abstract
In this paper, we study local broadcast in the dual graph model, which describes communication in a radio network with both reliable and unreliable links. Existing work proved that efficient solutions to these problems are impossible in the dual graph model under standard assumptions. In real networks, however, simple back-off strategies tend to perform well for solving these basic communication tasks. We address this apparent paradox by introducing a new set of constraints to the dual graph model that better generalize the slow/fast fading behavior common in real networks. We prove that in the context of these new constraints, simple back-off strategies now provide efficient solutions to local broadcast in the dual graph model. These results provide theoretical foundations for the practical observation that simple back-off algorithms tend to work well even amid the complicated link dynamics of real radio networks.

Cite as

Seth Gilbert, Nancy Lynch, Calvin Newport, and Dominik Pajak. Brief Announcement: On Simple Back-Off in Unreliable Radio Networks. In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, pp. 48:1-48:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{gilbert_et_al:LIPIcs.DISC.2018.48,
  author =	{Gilbert, Seth and Lynch, Nancy and Newport, Calvin and Pajak, Dominik},
  title =	{{Brief Announcement: On Simple Back-Off in Unreliable Radio Networks}},
  booktitle =	{32nd International Symposium on Distributed Computing (DISC 2018)},
  pages =	{48:1--48: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.48},
  URN =		{urn:nbn:de:0030-drops-98373},
  doi =		{10.4230/LIPIcs.DISC.2018.48},
  annote =	{Keywords: radio networks, broadcast, unreliable links, distributed algorithm, robustness}
}
Document
Bounds for Blind Rate Adaptation

Authors: Seth Gilbert, Calvin Newport, and Tonghe Wang

Published in: LIPIcs, Volume 46, 19th International Conference on Principles of Distributed Systems (OPODIS 2015)


Abstract
A core challenge in wireless communication is choosing appropriate transmission rates for packets. This rate selection problem is well understood in the context of unicast communication from a sender to a known receiver that can reply with acknowledgments. The problem is more difficult, however, in the multicast scenario where a sender must communicate with a potentially large and changing group of receivers with varied link qualities. In such settings, it is inefficient to gather feedback, and achieving good performance for every receiver is complicated by the potential diversity of their link conditions. This paper tackles this problem from an algorithmic perspective: identifying near optimal strategies for selecting rates that guarantee every receiver achieves throughput within reasonable factors of the optimal capacity of its link to the sender. Our algorithms have the added benefit that they are blind: they assume the sender has no information about the network and receives no feedback on its transmissions. We then prove new lower bounds on the fundamental difficulty of achieving good performance in the presence of fast fading (rapid and frequent changes to link quality), and conclude by studying strategies for achieving good throughput over multiple hops. We argue that the implementation of our algorithms should be easy because of the feature of being blind (it is independent to the network structure and the quality of links, so it's robust to changes). Our theoretical framework yields many new open problems within this important general topic of distributed transmission rate selection.

Cite as

Seth Gilbert, Calvin Newport, and Tonghe Wang. Bounds for Blind Rate Adaptation. In 19th International Conference on Principles of Distributed Systems (OPODIS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 46, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{gilbert_et_al:LIPIcs.OPODIS.2015.8,
  author =	{Gilbert, Seth and Newport, Calvin and Wang, Tonghe},
  title =	{{Bounds for Blind Rate Adaptation}},
  booktitle =	{19th International Conference on Principles of Distributed Systems (OPODIS 2015)},
  pages =	{8:1--8:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-98-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{46},
  editor =	{Anceaume, Emmanuelle and Cachin, Christian and Potop-Butucaru, Maria},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2015.8},
  URN =		{urn:nbn:de:0030-drops-65998},
  doi =		{10.4230/LIPIcs.OPODIS.2015.8},
  annote =	{Keywords: bitrate, multicast, packet transmission, latency, competitive ratio, lower bound, fading}
}

Gilbert, Gaëtan

Document
The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant

Authors: Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, and Théo Winterhalter

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)


Abstract
In dependently typed proof assistants, users can declare axioms to extend the ambient logic locally with new principles and propositional equalities governing them. Additionally, rewrite rules have recently been proposed to allow users to extend the logic with new definitional equalities, enabling them to handle new principles with a computational behaviour. While axioms can only break consistency, the addition of arbitrary rewrite rules can break other important metatheoretical properties such as type preservation. In this paper, we present an implementation of rewrite rules on top of the Coq proof assistant, together with a modular criterion to ensure that the added rewrite rules preserve typing. This criterion, based on bidirectional type checking, is formally expressed in PCUIC - the type theory of Coq recently developed in the MetaCoq project.

Cite as

Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, and Théo Winterhalter. The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{leray_et_al:LIPIcs.ITP.2024.26,
  author =	{Leray, Yann and Gilbert, Ga\"{e}tan and Tabareau, Nicolas and Winterhalter, Th\'{e}o},
  title =	{{The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{26:1--26:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.26},
  URN =		{urn:nbn:de:0030-drops-207545},
  doi =		{10.4230/LIPIcs.ITP.2024.26},
  annote =	{Keywords: type theory, dependent types, rewrite rules, type preservation, Coq}
}
Document
Design and Implementation of the Andromeda Proof Assistant

Authors: Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, and Christopher A. Stone

Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)


Abstract
Andromeda is an LCF-style proof assistant where the user builds derivable judgments by writing code in a meta-level programming language AML. The only trusted component of Andromeda is a minimalist nucleus (an implementation of the inference rules of an object-level type theory), which controls construction and decomposition of type-theoretic judgments. Since the nucleus does not perform complex tasks like equality checking beyond syntactic equality, this responsibility is delegated to the user, who implements one or more equality checking procedures in the meta-language. The AML interpreter requests witnesses of equality from user code using the mechanism of algebraic operations and handlers. Dynamic checks in the nucleus guarantee that no invalid object-level derivations can be constructed. To demonstrate the flexibility of this system structure, we implemented a nucleus consisting of dependent type theory with equality reflection. Equality reflection provides a very high level of expressiveness, as it allows the user to add new judgmental equalities, but it also destroys desirable meta-theoretic properties of type theory (such as decidability and strong normalization). The power of effects and handlers in AML is demonstrated by a standard library that provides default algorithms for equality checking, computation of normal forms, and implicit argument filling. Users can extend these new algorithms by providing local "hints" or by completely replacing these algorithms for particular developments. We demonstrate the resulting system by showing how to axiomatize and compute with natural numbers, by axiomatizing the untyped lambda-calculus, and by implementing a simple automated system for managing a universe of types.

Cite as

Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, and Christopher A. Stone. Design and Implementation of the Andromeda Proof Assistant. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 5:1-5:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{bauer_et_al:LIPIcs.TYPES.2016.5,
  author =	{Bauer, Andrej and Gilbert, Ga\"{e}tan and Haselwarter, Philipp G. and Pretnar, Matija and Stone, Christopher A.},
  title =	{{Design and Implementation of the Andromeda Proof Assistant}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{5:1--5:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.5},
  URN =		{urn:nbn:de:0030-drops-98574},
  doi =		{10.4230/LIPIcs.TYPES.2016.5},
  annote =	{Keywords: type theory, proof assistant, equality reflection, computational effects}
}

Gilbert, Anna C.

Document
Generalized Metric Repair on Graphs

Authors: Chenglin Fan, Anna C. Gilbert, Benjamin Raichel, Rishi Sonthalia, and Gregory Van Buskirk

Published in: LIPIcs, Volume 162, 17th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2020)


Abstract
Many modern data analysis algorithms either assume or are considerably more efficient if the distances between the data points satisfy a metric. However, as real data sets are noisy, they often do not possess this fundamental property. For this reason, Gilbert and Jain [A. Gilbert and L. Jain, 2017] and Fan et al. [C. Fan et al., 2018] introduced the closely related sparse metric repair and metric violation distance problems. Given a matrix, representing all distances, the goal is to repair as few entries as possible to ensure they satisfy a metric. This problem was shown to be APX-hard, and an O(OPT^{1/3})-approximation was given, where OPT is the optimal solution size. In this paper, we generalize the problem, by describing distances by a possibly incomplete positively weighted graph, where again our goal is to find the smallest number of weight modifications so that they satisfy a metric. This natural generalization is more flexible as it takes into account different relationships among the data points. We demonstrate the inherent combinatorial structure of the problem, and give an approximation-preserving reduction from MULTICUT, which is hard to approximate within any constant factor assuming UGC. Conversely, we show that for any fixed constant ς, for the large class of ς-chordal graphs, the problem is fixed parameter tractable, answering an open question from previous work. Call a cycle broken if it contains an edge whose weight is larger than the sum of all its other edges, and call the amount of this difference its deficit. We present approximation algorithms, one depending on the maximum number of edges in a broken cycle, and one depending on the number of distinct deficit values, both quantities which may naturally be small. Finally, we give improved analysis of previous algorithms for complete graphs.

Cite as

Chenglin Fan, Anna C. Gilbert, Benjamin Raichel, Rishi Sonthalia, and Gregory Van Buskirk. Generalized Metric Repair on Graphs. In 17th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 162, pp. 25:1-25:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{fan_et_al:LIPIcs.SWAT.2020.25,
  author =	{Fan, Chenglin and Gilbert, Anna C. and Raichel, Benjamin and Sonthalia, Rishi and Van Buskirk, Gregory},
  title =	{{Generalized Metric Repair on Graphs}},
  booktitle =	{17th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2020)},
  pages =	{25:1--25:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-150-4},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{162},
  editor =	{Albers, Susanne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SWAT.2020.25},
  URN =		{urn:nbn:de:0030-drops-122727},
  doi =		{10.4230/LIPIcs.SWAT.2020.25},
  annote =	{Keywords: Approximation, FPT, Hardness, Metric Spaces}
}

Gilbert, Anna

Document
Track A: Algorithms, Complexity and Games
Sparse Recovery for Orthogonal Polynomial Transforms

Authors: Anna Gilbert, Albert Gu, Christopher Ré, Atri Rudra, and Mary Wootters

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)


Abstract
In this paper we consider the following sparse recovery problem. We have query access to a vector 𝐱 ∈ ℝ^N such that x̂ = 𝐅 𝐱 is k-sparse (or nearly k-sparse) for some orthogonal transform 𝐅. The goal is to output an approximation (in an 𝓁₂ sense) to x̂ in sublinear time. This problem has been well-studied in the special case that 𝐅 is the Discrete Fourier Transform (DFT), and a long line of work has resulted in sparse Fast Fourier Transforms that run in time O(k ⋅ polylog N). However, for transforms 𝐅 other than the DFT (or closely related transforms like the Discrete Cosine Transform), the question is much less settled. In this paper we give sublinear-time algorithms - running in time poly(k log(N)) - for solving the sparse recovery problem for orthogonal transforms 𝐅 that arise from orthogonal polynomials. More precisely, our algorithm works for any 𝐅 that is an orthogonal polynomial transform derived from Jacobi polynomials. The Jacobi polynomials are a large class of classical orthogonal polynomials (and include Chebyshev and Legendre polynomials as special cases), and show up extensively in applications like numerical analysis and signal processing. One caveat of our work is that we require an assumption on the sparsity structure of the sparse vector, although we note that vectors with random support have this property with high probability. Our approach is to give a very general reduction from the k-sparse sparse recovery problem to the 1-sparse sparse recovery problem that holds for any flat orthogonal polynomial transform; then we solve this one-sparse recovery problem for transforms derived from Jacobi polynomials. Frequently, sparse FFT algorithms are described as implementing such a reduction; however, the technical details of such works are quite specific to the Fourier transform and moreover the actual implementations of these algorithms do not use the 1-sparse algorithm as a black box. In this work we give a reduction that works for a broad class of orthogonal polynomial families, and which uses any 1-sparse recovery algorithm as a black box.

Cite as

Anna Gilbert, Albert Gu, Christopher Ré, Atri Rudra, and Mary Wootters. Sparse Recovery for Orthogonal Polynomial Transforms. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 58:1-58:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{gilbert_et_al:LIPIcs.ICALP.2020.58,
  author =	{Gilbert, Anna and Gu, Albert and R\'{e}, Christopher and Rudra, Atri and Wootters, Mary},
  title =	{{Sparse Recovery for Orthogonal Polynomial Transforms}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{58:1--58:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.58},
  URN =		{urn:nbn:de:0030-drops-124653},
  doi =		{10.4230/LIPIcs.ICALP.2020.58},
  annote =	{Keywords: Orthogonal polynomials, Jacobi polynomials, sublinear algorithms, sparse recovery}
}
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