论文标题
在存在动态链接的情况下合成
Synthesis in Presence of Dynamic Links
论文作者
论文摘要
分布式合成的问题是，给定目标通信网络和算法正确行为的规范，自动生成分布式算法。 先前的工作集中在具有先验固定消息大小的静态网络上。这种方法有两个缺点：分布式计算中的最新工作正在转向动态变化的通信网络，而不是静态网络，而一类重要的分布式算法是所谓的全信息协议，其中Nodes Piggy先前接收到的消息先前接收到了当前消息。 在这项工作中，我们考虑了两个节点的系统的综合问题，这些节点是在一个动态链路上通过其消息大小没有界限的动态链接进行通信的。给定一个网络模型，即在执行的每一轮中，一组链接方向，对手选择网络模型的链接，仅受规范限制，并根据当前链接的方向传递消息。由具有直接确认机制的通信巴士的激励，我们进一步假设节点知道已经传递了哪些消息。 我们表明，当且仅当它不包含否定两个节点的消息的空链接时，对于网络模型而言，综合问题是可以决定的。
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.
