On Asynchrony and Reversibility in CCS

Abstract

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.