Search for: All records

Causality serves as an abstract notion of time for concurrent systems. A computation is causal, or simply valid, if each observation of a computation event is preceded by the observation of its causes. The present work establishes that this simple requirement is equally relevant when the occurrence of an event is invertible. We propose a conservative extension of causal models for concurrency that accommodates reversible computations. We first model reversible computations using a symmetric residuation operation in the general model of configuration structures. We show that stable configuration structures, which correspond to prime algebraic domains, remain stable under the action of this residuation. We then derive a semantics of reversible computations for prime event structures, which is shown to coincide with a switch operation that dualizes conflict and causality. 

Concurrency and causality can be expressed within a labelled transition system by exploiting reversibility of transitions. It is natural to ask what behavioural equivalences can be captured by bisimulations in the reversible setting. In this paper we work with keyed configuration structures and CCSK, establish an operational correspondence between the two models, and give definitions of hereditary history-preserving bisimulation and history-preserving bisimulation in both models. We then present several characterisation results for the two bisimulations in terms of previously proposed, as well as new, “reverse” bisimulations. 

Reversible concurrent calculi are abstract models for concurrent systems in which any action can potentially be undone. Over the last few decades, different formalisms have been developed and their mathematical properties have been explored; however, none have been machine-checked within a proof assistant. This paper presents the first Beluga formalization of the Calculus of Communicating Systems with Keys and Proof labels (CCSKP), a reversible extension of CCS. Beyond the syntax and semantics of the calculus, the encoding covers state-of-the-art results regarding three relations over proof labels – namely, dependence, independence and connectivity – which offer new insights into the notions of causality and concurrency of events. As is often the case with formalizations, our encoding introduces adjustments to the informal proof and makes explicit details which were previously only sketched, some of which reveal to be less straightforward than initially assumed. We believe this work lays the foundations for future reversible concurrent calculi formalizations. 

Among the formalisms that can be used to reason about concurrent systems, process calculi stand out both for their simple syntax and close connection to reversibility. They also offer approaches to study relations such as dependence, concurrency or causality between transitions, useful in exploring e.g., causes of bugs or how to multi-thread executions. This paper offers two main contributions: first, we provide separate definitions of a dependence relation and an independence relation, and prove their complementarity on connected transitions instead of postulating it, as is usually done. We also prove that those relations, as well as the notions of event, concurrency, causality and conflict, are unique for any reversible system respecting basic sanity axioms. Second, we prove that the operational definitions of core independence and causality coincide with their characterisations using a pre-existing syntactic mechanism in reversible process calculi, namely communication keys. 

This artifact contains the source code for the paper "A Formalization of the Reversible Concurrent Calculus CCSK^P in Beluga" (ICE 2025). 

This article designs a general principle to check the correctness of the definition of concurrency (a.k.a. independence) of events for concurrent calculi. Concurrency relations are central in process algebras, but also two-sided: they are often defined independently on composable and on coinitial transitions, and no criteria exist to assess whether they “interact correctly”. This article starts by examining how reversibility can provide such a correctness of concurrencies criterion, and its implications. It then defines, for the first time, a syntactical definition of concurrency for CCSK, a reversible declension of the calculus of communicating systems. To do so, according to our criterion, requires to define concurrency relations for all types of transitions along two axes: direction (forward or backward) and concomitance (coinitial or composable). Our definition is uniform thanks to proved transition systems and satisfies our sanity checks: square properties, sideways diamonds, but also the reversible checks (reverse diamonds and causal consistency). We also prove that our formalism is either equivalent to or a refinement of pre-existing definitions of concurrency for reversible systems. We conclude by discussing additional criteria and possible future works.