A Modular Formalization of Reversibility for Concurrent Models and Languages

TL;DR

This paper presents a modular framework for extending concurrent models and languages with causal-consistent reversibility, enabling reuse across different formal systems like CCS and X-machines.

Contribution

It introduces a general, modular approach to formalize reversible extensions of various concurrent models, promoting theory reuse and consistency.

Findings

Framework successfully applied to CCS and X-machines

Enables modular and causal-consistent reversibility in concurrency models

Facilitates reuse of theories across different formal systems

Abstract

Causal-consistent reversibility is the reference notion of reversibility for concurrency. We introduce a modular framework for defining causal-consistent reversible extensions of concurrent models and languages. We show how our framework can be used to define reversible extensions of formalisms as different as CCS and concurrent X-machines. The generality of the approach allows for the reuse of theories and techniques in different settings.