Synthesis in Presence of Dynamic Links

Béatrice Bérard
(Sorbonne Université, CNRS, LIP6, F-75005 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, F-75005 Paris, France)

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.

In Jean-Francois Raskin and Davide Bresolin: Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2020), Brussels, Belgium, September 21-22, 2020, Electronic Proceedings in Theoretical Computer Science 326, pp. 33–49.
Published: 20th September 2020.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: