存在动态链接时的综合
Synthesis in Presence of Dynamic Links
摘要：
分布式综合的问题是自动生成分布式算法，给定目标通信网络和算法正确行为的规范。以前的工作集中在静态网络与先验固定的消息大小。这种方法有两个缺点：分布式计算最近的工作正在转向动态变化的通信网络，而不是静态的，和一类重要的分布式算法是所谓的全信息协议，其中节点捎带以前收到的消息到当前的消息。在这项工作中，我们考虑了系统的两个节点在一个动态的链接，其消息大小是没有限制的轮通信的综合问题。给定网络模型，即，一组链路方向，在每一轮执行中，对手从网络模型中选择一条链路，仅受规范的限制，并根据当前链路的方向发送消息。出于直接确认机制的通信总线，我们进一步假设节点知道哪些消息已被发送。我们证明了一个网络模型的合成问题是可判定的，当且仅当它不包含空链接，解散两个节点的消息。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
