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 may be 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 模型来解释。 我们建议对通信模式逻辑进行分解,我们表明,在更新通信模式时保留了集体的双相似性( 其分布式知识的比较模型 ) 。 我们还可以通过更新简单化的复杂内容来解释通信模式, 这是一种广为人知的分布式计算结构框架。 我们显示,不同的语义相对一致, 并提议在简单化的组合中进行集体调整 。</s>