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