More Like this

1. The correctness of concurrencies in (reversible) concurrent calculi

   https://doi.org/10.1016/j.jlamp.2023.100924  

   Aubert, Clément (January 2024, Journal of Logical and Algebraic Methods in Programming)

   Claudio Antares Mezzina (Ed.)

   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. 

   more » « less
2. A Formalization of the Reversible Concurrent Calculus CCSKP in Beluga

   https://doi.org/10.4204/EPTCS.425.5  

   Cecilia, Gabriele (August 2025, Electronic Proceedings in Theoretical Computer Science)

   Aubert, Clément; Di_Giusto, Cinzia; Fowler, Simon; Ka_I_Pun, Violet (Ed.)

   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. 

   more » « less
3. Bisimulations and Reversibility

   https://doi.org/10.1007/978-3-031-99717-4_3  

   Aubert, Clément; Phillips, Iain; Ulidowski, Irek (October 2025, Springer Nature Switzerland)

   Mezzina, Claudio Antares; Schmitt, Alan (Ed.)

   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. 

   more » « less
4. Reversible computations are computations

   https://doi.org/10.46298/entics.16677  

   Aubert, Clément; Krivine, Jean (December 2025, Electronic Notes in Theoretical Informatics and Computer Science)

   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. 

   more » « less
5. Dispersion Relations Alone Cannot Guarantee Causality

   https://doi.org/10.1103/PhysRevLett.132.162301  

   Gavassino, L; Disconzi, M; Noronha, J (April 2024, Physical Review Letters)

   We show that linear superpositions of plane waves involving a single-valued, covariantly stable dispersion relation $$\omega(k)$$ always propagate outside the lightcone, unless $$\omega(k) =a+b k$$. This implies that there is no notion of causality for individual dispersion relations, since no mathematical condition on the function $$\omega(k)$$ (such as the front velocity or the asymptotic group velocity conditions) can serve as a sufficient condition for subluminal propagation in dispersive media. Instead, causality can only emerge from a careful cancellation that occurs when one superimposes all the excitation branches of a physical model. This is shown to happen automatically in local theories of matter that are covariantly stable. 

   more » « less