We propose communication pattern logic. A communication pattern describes how processes or agents inform each other, independently of the information content. The full information protocol in distributed computing is the special case wherein all agents inform each other. We study this protocol in distributed computing models where communication might fail: an agent is certain about the messages it receives, but it is uncertain about the messages other agents have received. In a dynamic epistemic logic with distributed knowledge and with modalities for communication patterns, the latter are interpreted by updating Kripke models. We propose an axiomatization of communication pattern logic, and we show that collective bisimilarity (comparing models on their distributed knowledge) is preserved when updating models with communication patterns. We can also interpret communication patterns by updating simplicial complexes, a well-known topological framework for distributed computing. We show that the different semantics correspond, and propose collective bisimulation between simplicial complexes.
翻译:我们提出通信模式逻辑。 通信模式描述流程或代理商如何相互沟通,而不考虑信息内容。 分布式计算中的全部信息协议是所有代理商相互沟通的特例。 我们在通信可能失败的分布式计算模型中研究这一协议: 代理商对它收到的信息是肯定的, 但对于其他代理商收到的信息是不确定的。 在具有分布式知识和通信模式的动态缩略语逻辑中, 后者通过更新 Kripke 模式来解释。 我们提出通信模式逻辑的不一致性, 并表明在更新通信模式时保留了集体的两样性( 其分布式知识的比较模型 ) 。 我们还可以通过更新简化式的复合体来解释通信模式, 这是一种广为人知的分布式计算表理学框架。 我们展示了不同的语义对应, 并提议在简单化的组合间进行集体平衡。