发表机构
Universidad de Buenos Aires; Conicet; Università di Bari Aldo Moro; Università di Cagliari（布宜诺斯艾利斯大学; 阿根廷国家科学研究委员会; 巴里阿尔多·莫罗大学; 卡利亚里大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文研究CCS框架下异步性与可逆性的相互作用，提出异步变体CCSa及其可逆扩展rCCSa，证明其语义满足因果一致性，填补了异步通信与可逆计算结合的研究空白。
AI 中文摘要
异步通信是现代分布式系统的一项基本特征，其中消息的发送无需与接收方立即同步。在进程演算中，这种行为通常通过将消息发送与消息消费分离来建模。与此同时，可逆计算已成为分析并发系统的重要范式，它支持在保留动作间因果依赖关系的前提下撤销计算。虽然针对CCS等同步进程演算的可逆语义已得到广泛研究，但它们与异步通信的结合在很大程度上仍未被探索。\n 本文在CCS的框架下研究了异步性与可逆性之间的相互作用。我们首先引入了CCSa——一种CCS的异步变体，其中输出动作会生成显式的消息实体，这些实体随后可被匹配的输入动作消费。接着我们定义了rCCSa，它是通过调整Phillips和Ulidowski的框架得到的CCSa的可逆扩展。在rCCSa中，前缀和消息都标注有唯一密钥，用于记录消息的发送和消费事件，使得计算可以在保留因果依赖的情况下被撤销。我们证明了所得的可逆语义满足因果一致性，确保计算可以精确撤销至因果等价的程度。该证明依赖于Lanese等人提出的可逆计算公理框架。
英文摘要
Asynchronous communication is a fundamental feature of modern distributed systems, where messages are emitted without requiring immediate synchronization with receivers. In process calculi, this behaviour is typically modelled by separating message emission from message consumption. At the same time, reversible computation has emerged as an important paradigm for analysing concurrent systems, enabling computations to be undone while preserving causal dependencies between actions. While reversible semantics have been extensively studied for synchronous process calculi such as CCS, their integration with asynchronous communication remains largely unexplored. In this paper we investigate the interaction between asynchrony and reversibility in the setting of CCS. We first introduce CCSa, an asynchronous variant of CCS in which output actions generate explicit message entities that can later be consumed by matching input actions. We then define rCCSa, a reversible extension of CCSa obtained by adapting the framework of Phillips and Ulidowski. In rCCSa, prefixes and messages are annotated with unique keys that record message emission and consumption events, allowing computations to be reversed while preserving causal dependencies. We show that the resulting reversible semantics satisfies causal consistency, ensuring that computations can be reversed exactly up to causal equivalence. The proof relies on the axiomatic framework for reversible computation proposed by Lanese et al.
CommentsIn Proceedings ICE 2026, arXiv:2609.30353
Journal refEPTCS 453, 2026, pp. 23-39
