We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.FL

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo

Computer Science > Formal Languages and Automata Theory

Title: Synthesis in Presence of Dynamic Links

Authors: Béatrice Bérard (Sorbonne Université, CNRS, LIP6, Paris, France), Benedikt Bollig (CNRS & LSV, ENS Paris-Saclay, Université Paris-Saclay, France), Patricia Bouyer (CNRS & LSV, ENS Paris-Saclay, Université Paris-Saclay, France), Matthias Függer (CNRS & LSV, ENS Paris-Saclay, Université Paris-Saclay, Inria, France), Nathalie Sznajder (Sorbonne Université, CNRS, LIP6, Paris, France)
Abstract: The problem of distributed synthesis is to automatically generate a distributed algorithm, given a target communication network and a specification of the algorithm's correct behavior.
Previous work has focused on static networks with an a priori fixed message size. This approach has two shortcomings: Recent work in distributed computing is shifting towards dynamically changing communication networks rather than static ones, and an important class of distributed algorithms are so-called full-information protocols, where nodes piggy-pack previously received messages onto current messages.
In this work, we consider the synthesis problem for a system of two nodes communicating in rounds over a dynamic link whose message size is not bounded. Given a network model, i.e., a set of link directions, in each round of the execution, the adversary choses a link from the network model, restricted only by the specification, and delivers messages according to the current link's directions. Motivated by communication buses with direct acknowledge mechanisms, we further assume that nodes are aware of which messages have been delivered.
We show that the synthesis problem is decidable for a network model if and only if it does not contain the empty link that dismisses both nodes' messages.
Comments: In Proceedings GandALF 2020, arXiv:2009.09360
Subjects: Formal Languages and Automata Theory (cs.FL); Distributed, Parallel, and Cluster Computing (cs.DC); Computer Science and Game Theory (cs.GT); Logic in Computer Science (cs.LO)
Journal reference: EPTCS 326, 2020, pp. 33-49
DOI: 10.4204/EPTCS.326.3
Cite as: arXiv:2002.07545 [cs.FL]
  (or arXiv:2002.07545v2 [cs.FL] for this version)

Submission history

From: EPTCS [view email]
[v1] Tue, 18 Feb 2020 13:21:24 GMT (107kb,D)
[v2] Wed, 23 Sep 2020 01:24:22 GMT (35kb)

Link back to: arXiv, form interface, contact.