Synthesis in presence of dynamic links
Résumé
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 an arbitrary 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 the network model does not contain the empty link that dismisses both nodes' messages. We then extend the characterization to sequences of communication links that may contain empty links. We show that the synthesis problem is decidable in this case if and only if the number of consecutive empty links in all possible sequences is uniformly bounded from above.
Origine : Fichiers produits par l'(les) auteur(s)