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.
翻译:我们提出通信模式逻辑。通信模式描述了进程或智能体如何相互告知信息,而与信息内容无关。分布式计算中的全信息协议是其中的一个特例,即所有智能体彼此互相告知。我们在可能发生通信故障的分布式计算模型中研究该协议:智能体对其接收的消息是确定的,但可能对其他智能体所接收的消息不确定。在一种具有分布式知识和通信模式模态词的动态认知逻辑中,通信模式通过更新克里普克模型进行解释。我们提出了通信模式逻辑的公理化系统,并证明当使用通信模式更新模型时,集体互模拟(通过分布式知识比较模型)得以保持。我们还可以通过更新单纯复形(一种著名的分布式计算拓扑框架)来解释通信模式。我们证明了不同语义之间的对应关系,并提出了单纯复形之间的集体互模拟。