论通信模型对可实现性的影响
形式语言与自动机理论
2025-12-08 v1 计算机科学中的逻辑
摘要
多方会话类型 (MPST) 为分布式系统中通信协议的指定和验证提供了类型理论基础。MPST 依赖于全局类型的概念，该类型指定全局行为，以及局部类型，即全局行为到每个局部参与者的投影。MPST 中的一个核心概念是可实现性——即从全局规范导出的局部实现是否在给定的通信模型下正确实现了预期的协议。虽然可实现性在点对点语义下已被广泛研究，但在其他替代通信模型（如基于包、因果有序或同步通信）中，它仍然知之甚少。在本文中，我们开发了一个统一框架，用于在一系列通信模型中推理可实现性和子类型化。我们表明，通信模型不影响子类型化的概念，但会影响可实现性的概念。我们引入了几个用于子类型检查和可实现性检查的决策程序，其复杂度从 NLOGSPACE 到 EXPSPACE 不等，具体取决于对全局类型所做的假设，特别是取决于它们的可补全性和给定补集的大小。
引用
@article{arxiv.2512.05609,
title = {On the Impact of the Communication Model on Realisability},
author = {Cinzia Di Giusto and Etienne Lozes and Pascal Urso},
journal= {arXiv preprint arXiv:2512.05609},
year = {2025}
}