Search Results

Documents authored by Rajsbaum, Sergio

Document
Brief Announcement
DOI: 10.4230/LIPIcs.DISC.2024.42
Brief Announcement: Solvability of Three-Process General Tasks

Authors: Hagit Attiya, Pierre Fraigniaud, Ami Paz, and Sergio Rajsbaum

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

Abstract
The topological view on distributed computing represents a task T as a relation Δ between the complex ℐ of its inputs and the complex 𝒪 of its outputs. A cornerstone result in the field is an elegant computability characterization of the solvability of colorless tasks in terms of ℐ, 𝒪 and Δ. Essentially, a colorless task is wait-free solvable if and only if there is a continuous map from the geometric realization of ℐ to that of 𝒪 that respects Δ. This paper makes headway towards providing an analogous characterization for general tasks, which are not necessarily colorless, by concentrating on the case of three-process inputless tasks. Our key contribution is identifying local articulation points as an obstacle for the solvability of general tasks, and defining a topological deformation on the output complex of a task T, which eliminates these points by splitting them, to obtain a new task T', with an adjusted relation Δ' between the input complex ℐ and an output complex 𝒪' without articulation points. We obtain a new characterization of wait-free solvability of three-process general tasks: T is wait-free solvable if and only if there is a continuous map from the geometric realization of ℐ to that of 𝒪' that respects Δ'.
Cite as

Hagit Attiya, Pierre Fraigniaud, Ami Paz, and Sergio Rajsbaum. Brief Announcement: Solvability of Three-Process General Tasks. In 38th International Symposium on Distributed Computing (DISC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 319, pp. 42:1-42:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{attiya_et_al:LIPIcs.DISC.2024.42,
  author =	{Attiya, Hagit and Fraigniaud, Pierre and Paz, Ami and Rajsbaum, Sergio},
  title =	{{Brief Announcement: Solvability of Three-Process General Tasks}},
  booktitle =	{38th International Symposium on Distributed Computing (DISC 2024)},
  pages =	{42:1--42:7},
  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.42},
  URN =		{urn:nbn:de:0030-drops-212700},
  doi =		{10.4230/LIPIcs.DISC.2024.42},
  annote =	{Keywords: Wait-free computing, lower bounds, topology}
}
Document
DOI: 10.4230/LIPIcs.DISC.2023.4
One Step Forward, One Step Back: FLP-Style Proofs and the Round-Reduction Technique for Colorless Tasks

Authors: Hagit Attiya, Pierre Fraigniaud, Ami Paz, and Sergio Rajsbaum

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

Abstract
The paper compares two generic techniques for deriving lower bounds and impossibility results in distributed computing. First, we prove a speedup theorem (a-la Brandt, 2019), for wait-free colorless algorithms, aiming at capturing the essence of the seminal round-reduction proof establishing a lower bound on the number of rounds for 3-coloring a cycle (Linial, 1992), and going by backward induction. Second, we consider FLP-style proofs, aiming at capturing the essence of the seminal consensus impossibility proof (Fischer, Lynch, and Paterson, 1985) and using forward induction. We show that despite their very different natures, these two forms of proof are tightly connected. In particular, we show that for every colorless task Π, if there is a round-reduction proof establishing the impossibility of solving Π using wait-free colorless algorithms, then there is an FLP-style proof establishing the same impossibility. For 1-dimensional colorless tasks (for an arbitrarily number n ≥ 2 of processes), we prove that the two proof techniques have exactly the same power, and more importantly, both are complete: if a 1-dimensional colorless task is not wait-free solvable by n ≥ 2 processes, then the impossibility can be proved by both proof techniques. Moreover, a round-reduction proof can be automatically derived, and an FLP-style proof can be automatically generated from it. Finally, we illustrate the use of these two techniques by establishing the impossibility of solving any colorless covering task of arbitrary dimension by wait-free algorithms.
Cite as

Hagit Attiya, Pierre Fraigniaud, Ami Paz, and Sergio Rajsbaum. One Step Forward, One Step Back: FLP-Style Proofs and the Round-Reduction Technique for Colorless Tasks. In 37th International Symposium on Distributed Computing (DISC 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 281, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{attiya_et_al:LIPIcs.DISC.2023.4,
  author =	{Attiya, Hagit and Fraigniaud, Pierre and Paz, Ami and Rajsbaum, Sergio},
  title =	{{One Step Forward, One Step Back: FLP-Style Proofs and the Round-Reduction Technique for Colorless Tasks}},
  booktitle =	{37th International Symposium on Distributed Computing (DISC 2023)},
  pages =	{4:1--4:23},
  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.4},
  URN =		{urn:nbn:de:0030-drops-191304},
  doi =		{10.4230/LIPIcs.DISC.2023.4},
  annote =	{Keywords: Wait-free computing, lower bounds}
}
Document
DOI: 10.4230/DagRep.12.12.27
Formal Methods and Distributed Computing: Stronger Together (Dagstuhl Seminar 22492)

Authors: Hagit Attiya, Constantin Enea, Sergio Rajsbaum, and Ana Sokolova

Published in: Dagstuhl Reports, Volume 12, Issue 12 (2023)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 22492 "Formal Methods and Distributed Computing: Stronger Together", held in December 2022.
Cite as

Hagit Attiya, Constantin Enea, Sergio Rajsbaum, and Ana Sokolova. Formal Methods and Distributed Computing: Stronger Together (Dagstuhl Seminar 22492). In Dagstuhl Reports, Volume 12, Issue 12, pp. 27-53, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{attiya_et_al:DagRep.12.12.27,
  author =	{Attiya, Hagit and Enea, Constantin and Rajsbaum, Sergio and Sokolova, Ana},
  title =	{{Formal Methods and Distributed Computing: Stronger Together (Dagstuhl Seminar 22492)}},
  pages =	{27--53},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2023},
  volume =	{12},
  number =	{12},
  editor =	{Attiya, Hagit and Enea, Constantin and Rajsbaum, Sergio and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.12.12.27},
  URN =		{urn:nbn:de:0030-drops-178452},
  doi =		{10.4230/DagRep.12.12.27},
  annote =	{Keywords: automated verification and reasoning, concurrent data structures and transactions, distributed algorithms, large-scale replication}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CONCUR.2022.3
Distributed Decision Problems: Concurrent Specifications Beyond Binary Relations (Invited Talk)

Authors: Sergio Rajsbaum

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
Much discussion exists about what is computation, but less about is a computational problem. Turing’s definition of computation was based on computing functions. When we move from sequential computing to interactive computing, discussions concentrate on computations that do not terminate, overlooking notions of distributed problems. Many models where concurrency happens have been proposed, ranging from those equivalent to a Turing machine, to those where much heated discussion has taken place, claiming that interactive models are fundamentally different from Turing machines. It is argued here that there is no need to go all the way to non-terminating interaction, to appreciate how different distributed computation is from sequential computation. The discussion concentrates on the various ways that exist of representing a distributed decision problem. Each process of a distributed system starts with an initial private input value, and after communicating with other processes in the system, produces a local output value. An input/output relation is needed, to specify which output values are legal for a particular assignment of input values to the processes. An overview is provided of some results that show how rich the topic of distributed decision problems can be, when asynchronous processes can fail, but mostly independent of particular models of distributed computing and their many intricate details (types of failures and of communication). We are in a world very different from that of the functions of sequential computation; moving away from the world of graphs beyond binary relations, to the world of simplicial complexes.
Cite as

Sergio Rajsbaum. Distributed Decision Problems: Concurrent Specifications Beyond Binary Relations (Invited Talk). In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 3:1-3:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{rajsbaum:LIPIcs.CONCUR.2022.3,
  author =	{Rajsbaum, Sergio},
  title =	{{Distributed Decision Problems: Concurrent Specifications Beyond Binary Relations}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{3:1--3:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.3},
  URN =		{urn:nbn:de:0030-drops-170660},
  doi =		{10.4230/LIPIcs.CONCUR.2022.3},
  annote =	{Keywords: Distributed decision tasks, simplicial complex, linearizability, interval-linearizability, Arrow’s impossibility, Speedup theorems}
}
Document
DOI: 10.4230/LIPIcs.STACS.2022.33
A Simplicial Model for KB4_n: Epistemic Logic with Agents That May Die

Authors: Éric Goubault, Jérémy Ledent, and Sergio Rajsbaum

Published in: LIPIcs, Volume 219, 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022)

Abstract
The standard semantics of multi-agent epistemic logic S5_n is based on Kripke models whose accessibility relations are reflexive, symmetric and transitive. This one dimensional structure contains implicit higher-dimensional information beyond pairwise interactions, that we formalized as pure simplicial models in a previous work in Information and Computation 2021 [Éric Goubault et al., 2021]. Here we extend the theory to encompass simplicial models that are not necessarily pure. The corresponding class of Kripke models are those where the accessibility relation is symmetric and transitive, but might not be reflexive. Such models correspond to the epistemic logic KB4_n. Impure simplicial models arise in situations where two possible worlds may not have the same set of agents. We illustrate it with distributed computing examples of synchronous systems where processes may crash.
Cite as

Éric Goubault, Jérémy Ledent, and Sergio Rajsbaum. A Simplicial Model for KB4_n: Epistemic Logic with Agents That May Die. In 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 219, pp. 33:1-33:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{goubault_et_al:LIPIcs.STACS.2022.33,
  author =	{Goubault, \'{E}ric and Ledent, J\'{e}r\'{e}my and Rajsbaum, Sergio},
  title =	{{A Simplicial Model for KB4\underlinen: Epistemic Logic with Agents That May Die}},
  booktitle =	{39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022)},
  pages =	{33:1--33:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-222-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{219},
  editor =	{Berenbrink, Petra and Monmege, Benjamin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2022.33},
  URN =		{urn:nbn:de:0030-drops-158434},
  doi =		{10.4230/LIPIcs.STACS.2022.33},
  annote =	{Keywords: Epistemic logic, Simplicial complexes, Distributed computing}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2022.73
Continuous Tasks and the Asynchronous Computability Theorem

Authors: Hugo Rincon Galeana, Sergio Rajsbaum, and Ulrich Schmid

Published in: LIPIcs, Volume 215, 13th Innovations in Theoretical Computer Science Conference (ITCS 2022)

Abstract
The celebrated 1999 Asynchronous Computability Theorem (ACT) of Herlihy and Shavit characterized distributed tasks that are wait-free solvable and uncovered deep connections with combinatorial topology. We provide an alternative characterization of those tasks by means of the novel concept of continuous tasks, which have an input/output specification that is a continuous function between the geometric realizations of the input and output complex: We state and prove a precise characterization theorem (CACT) for wait-free solvable tasks in terms of continuous tasks. Its proof utilizes a novel chromatic version of a foundational result in algebraic topology, the simplicial approximation theorem, which is also proved in this paper. Apart from the alternative proof of the ACT implied by our CACT, we also demonstrate that continuous tasks have an expressive power that goes beyond classic task specifications, and hence open up a promising venue for future research: For the well-known approximate agreement task, we show that one can easily encode the desired proportion of the occurrence of specific outputs, namely, exact agreement, in the continuous task specification.
Cite as

Hugo Rincon Galeana, Sergio Rajsbaum, and Ulrich Schmid. Continuous Tasks and the Asynchronous Computability Theorem. In 13th Innovations in Theoretical Computer Science Conference (ITCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 215, pp. 73:1-73:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{galeana_et_al:LIPIcs.ITCS.2022.73,
  author =	{Galeana, Hugo Rincon and Rajsbaum, Sergio and Schmid, Ulrich},
  title =	{{Continuous Tasks and the Asynchronous Computability Theorem}},
  booktitle =	{13th Innovations in Theoretical Computer Science Conference (ITCS 2022)},
  pages =	{73:1--73:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-217-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{215},
  editor =	{Braverman, Mark},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2022.73},
  URN =		{urn:nbn:de:0030-drops-156696},
  doi =		{10.4230/LIPIcs.ITCS.2022.73},
  annote =	{Keywords: Wait-free computability, topology, distributed computing, decision tasks, shared memory}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2020.13
Relaxed Queues and Stacks from Read/Write Operations

Authors: Armando Castañeda, Sergio Rajsbaum, and Michel Raynal

Published in: LIPIcs, Volume 184, 24th International Conference on Principles of Distributed Systems (OPODIS 2020)

Abstract
Considering asynchronous shared memory systems in which any number of processes may crash, this work identifies and formally defines relaxations of queues and stacks that can be non-blocking or wait-free while being implemented using only read/write operations. Set-linearizability and Interval-linearizability are used to specify the relaxations formally, and precisely identify the subset of executions which preserve the original sequential behavior. The relaxations allow for an item to be returned more than once by different operations, but only in case of concurrency; we call such a property multiplicity. The stack implementation is wait-free, while the queue implementation is non-blocking. Interval-linearizability is used to describe a queue with multiplicity, with the additional relaxation that a dequeue operation can return weak-empty, which means that the queue might be empty. We present a read/write wait-free interval-linearizable algorithm of a concurrent queue. As far as we know, this work is the first that provides formalizations of the notions of multiplicity and weak-emptiness, which can be implemented on top of read/write registers only.
Cite as

Armando Castañeda, Sergio Rajsbaum, and Michel Raynal. Relaxed Queues and Stacks from Read/Write Operations. In 24th International Conference on Principles of Distributed Systems (OPODIS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 184, pp. 13:1-13:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{castaneda_et_al:LIPIcs.OPODIS.2020.13,
  author =	{Casta\~{n}eda, Armando and Rajsbaum, Sergio and Raynal, Michel},
  title =	{{Relaxed Queues and Stacks from Read/Write Operations}},
  booktitle =	{24th International Conference on Principles of Distributed Systems (OPODIS 2020)},
  pages =	{13:1--13:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-176-4},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{184},
  editor =	{Bramas, Quentin and Oshman, Rotem and Romano, Paolo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2020.13},
  URN =		{urn:nbn:de:0030-drops-134983},
  doi =		{10.4230/LIPIcs.OPODIS.2020.13},
  annote =	{Keywords: Asynchrony, Correctness condition, Linearizability, Nonblocking, Process crash, Relaxed data type, Set-linearizability, Wait-freedom, Work-stealing}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2020.18
Locally Solvable Tasks and the Limitations of Valency Arguments

Authors: Hagit Attiya, Armando Castañeda, and Sergio Rajsbaum

Published in: LIPIcs, Volume 184, 24th International Conference on Principles of Distributed Systems (OPODIS 2020)

Abstract
An elegant strategy for proving impossibility results in distributed computing was introduced in the celebrated FLP consensus impossibility proof. This strategy is local in nature as at each stage, one configuration of a hypothetical protocol for consensus is considered, together with future valencies of possible extensions. This proof strategy has been used in numerous situations related to consensus, leading one to wonder why it has not been used in impossibility results of two other well-known tasks: set agreement and renaming. This paper provides an explanation of why impossibility proofs of these tasks have been of a global nature. It shows that a protocol can always solve such tasks locally, in the following sense. Given a configuration and all its future valencies, if a single successor configuration is selected, then the protocol can reveal all decisions in this branch of executions, satisfying the task specification. This result is shown for both set agreement and renaming, implying that there are no local impossibility proofs for these tasks.
Cite as

Hagit Attiya, Armando Castañeda, and Sergio Rajsbaum. Locally Solvable Tasks and the Limitations of Valency Arguments. In 24th International Conference on Principles of Distributed Systems (OPODIS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 184, pp. 18:1-18:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{attiya_et_al:LIPIcs.OPODIS.2020.18,
  author =	{Attiya, Hagit and Casta\~{n}eda, Armando and Rajsbaum, Sergio},
  title =	{{Locally Solvable Tasks and the Limitations of Valency Arguments}},
  booktitle =	{24th International Conference on Principles of Distributed Systems (OPODIS 2020)},
  pages =	{18:1--18:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-176-4},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{184},
  editor =	{Bramas, Quentin and Oshman, Rotem and Romano, Paolo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2020.18},
  URN =		{urn:nbn:de:0030-drops-135037},
  doi =		{10.4230/LIPIcs.OPODIS.2020.18},
  annote =	{Keywords: Wait-freedom, Set agreement, Weak symmetry breaking, Impossibility proofs}
}
Document
DOI: 10.4230/LIPIcs.DISC.2019.21
Wait-Free Solvability of Equality Negation Tasks

Authors: Éric Goubault, Marijana Lazić, Jérémy Ledent, and Sergio Rajsbaum

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

Abstract
We introduce a family of tasks for n processes, as a generalization of the two process equality negation task of Lo and Hadzilacos (SICOMP 2000). Each process starts the computation with a private input value taken from a finite set of possible inputs. After communicating with the other processes using immediate snapshots, the process must decide on a binary output value, 0 or 1. The specification of the task is the following: in an execution, if the set of input values is large enough, the processes should agree on the same output; if the set of inputs is small enough, the processes should disagree; and in-between these two cases, any output is allowed. Formally, this specification depends on two threshold parameters k and l, with k<l, indicating when the cardinality of the set of inputs becomes "small" or "large", respectively. We study the solvability of this task depending on those two parameters. First, we show that the task is solvable whenever k+2 <= l. For the remaining cases (l = k+1), we use various combinatorial topology techniques to obtain two impossibility results: the task is unsolvable if either k <= n/2 or n-k is odd. The remaining cases are still open.
Cite as

Éric Goubault, Marijana Lazić, Jérémy Ledent, and Sergio Rajsbaum. Wait-Free Solvability of Equality Negation Tasks. In 33rd International Symposium on Distributed Computing (DISC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 146, pp. 21:1-21:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{goubault_et_al:LIPIcs.DISC.2019.21,
  author =	{Goubault, \'{E}ric and Lazi\'{c}, Marijana and Ledent, J\'{e}r\'{e}my and Rajsbaum, Sergio},
  title =	{{Wait-Free Solvability of Equality Negation Tasks}},
  booktitle =	{33rd International Symposium on Distributed Computing (DISC 2019)},
  pages =	{21:1--21:16},
  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.21},
  URN =		{urn:nbn:de:0030-drops-113288},
  doi =		{10.4230/LIPIcs.DISC.2019.21},
  annote =	{Keywords: Equality negation, distributed computability, combinatorial topology}
}
Document
DOI: 10.4230/DagRep.8.5.60
Formal Methods and Fault-Tolerant Distributed Comp.: Forging an Alliance (Dagstuhl Seminar 18211)

Authors: Javier Esparza, Pierre Fraignaud, Anca Muscholl, and Sergio Rajsbaum

Published in: Dagstuhl Reports, Volume 8, Issue 5 (2019)

Abstract
The Dagstuhl Seminar "Formal Methods and Fault-Tolerant Distributed Computing: Forging an Alliance" took place May 22-25, 2018. Its goal was to strengthen the interaction between researchers from formal methods and from distributed computing, and help the two communities to better identify common research challenges.
Cite as

Javier Esparza, Pierre Fraignaud, Anca Muscholl, and Sergio Rajsbaum. Formal Methods and Fault-Tolerant Distributed Comp.: Forging an Alliance (Dagstuhl Seminar 18211). In Dagstuhl Reports, Volume 8, Issue 5, pp. 60-79, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{esparza_et_al:DagRep.8.5.60,
  author =	{Esparza, Javier and Fraignaud, Pierre and Muscholl, Anca and Rajsbaum, Sergio},
  title =	{{Formal Methods and Fault-Tolerant Distributed Comp.: Forging an Alliance (Dagstuhl Seminar 18211)}},
  pages =	{60--79},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2018},
  volume =	{8},
  number =	{5},
  editor =	{Esparza, Javier and Fraignaud, Pierre and Muscholl, Anca and Rajsbaum, Sergio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.8.5.60},
  URN =		{urn:nbn:de:0030-drops-98933},
  doi =		{10.4230/DagRep.8.5.60},
  annote =	{Keywords: distributed computing, distributed systems, formal verification}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.16
Decentralized Asynchronous Crash-Resilient Runtime Verification

Authors: Borzoo Bonakdarpour, Pierre Fraigniaud, Sergio Rajsbaum, David A. Rosenblueth, and Corentin Travers

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
Runtime Verification (RV) is a lightweight method for monitoring the formal specification of a system during its execution. It has recently been shown that a given state predicate can be monitored consistently by a set of crash-prone asynchronous distributed monitors, only if sufficiently many different verdicts can be emitted by each monitor. We revisit this impossibility result in the context of LTL semantics for RV. We show that employing the four-valued logic Rv-LTL will result in inconsistent distributed monitoring for some formulas. Our first main contribution is a family of logics, called Ltl2k+4, that refines Rv-Ltl incorporating 2k + 4 truth values, for each k >= 0. The truth values of Ltl2k+4 can be effectively used by each monitor to reach a consistent global set of verdicts for each given formula, provided k is sufficiently large. Our second main contribution is an algorithm for monitor construction enabling fault-tolerant distributed monitoring based on the aggregation of the individual verdicts by each monitor.
Cite as

Borzoo Bonakdarpour, Pierre Fraigniaud, Sergio Rajsbaum, David A. Rosenblueth, and Corentin Travers. Decentralized Asynchronous Crash-Resilient Runtime Verification. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 16:1-16:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bonakdarpour_et_al:LIPIcs.CONCUR.2016.16,
  author =	{Bonakdarpour, Borzoo and Fraigniaud, Pierre and Rajsbaum, Sergio and Rosenblueth, David A. and Travers, Corentin},
  title =	{{Decentralized Asynchronous Crash-Resilient Runtime Verification}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{16:1--16:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.16},
  URN =		{urn:nbn:de:0030-drops-61856},
  doi =		{10.4230/LIPIcs.CONCUR.2016.16},
  annote =	{Keywords: Runtime monitoring, Distributed algorithms, Fault-tolerance}
}
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact