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.
翻译:我们提出通信模式逻辑。通信模式描述了进程或智能体之间相互告知信息的方式,独立于信息内容本身。分布式计算中的全信息协议是其中所有智能体相互告知信息的特例。我们在分布式计算模型中研究该协议,这些模型中的通信可能发生失败:智能体对自己接收到的消息是确定的,但可能不确定其他智能体接收到的消息。在一种包含分布式知识和通信模式模态词的动态认知逻辑中,后者通过更新克里普克模型进行解释。我们提出了通信模式逻辑的公理化系统,并证明在利用通信模式更新模型时,集体互模拟(基于分布式知识比较模型)得以保持。我们还可以通过更新单纯复形(分布式计算中一种著名的拓扑框架)来解释通信模式。我们证明了不同语义之间的对应关系,并提出了单纯复形之间的集体互模拟。