An Axiomatic Theory for Reversible Computation

TL;DR

The paper presents a general, axiomatic framework for reversible computation based on labelled transition systems with independence (LTSIs). By grounding reversibility in a small set of core axioms, it derives principal properties such as causal consistency, along with novel causal safety and liveness notions, across a wide range of formalisms. It also develops a structured theory of independence and independent events, plus three flavors of CS/CL (transitions, events, ordering) and three structured notions (coinitial, label-generated), with comprehensive case studies showing applicability to RCCS, CCSK, HOπ, Rπ, πIH, Erlang, occurrence nets, and sequential systems. The approach enables modular proofs, supports reasoning about new reversible calculi, and connects labeling/structural choices to the attainment of CC, CS, and CL properties. This framework thus unifies and simplifies the verification of reversibility properties across diverse concurrent models, offering a pathway to formal tooling and future extensions such as rollback controls and irreversible actions.

Abstract

Undoing computations of a concurrent system is beneficial in many situations, e.g., in reversible debugging of multi-threaded programs and in recovery from errors due to optimistic execution in parallel discrete event simulation. A number of approaches have been proposed for how to reverse formal models of concurrent computation including process calculi such as CCS, languages like Erlang, and abstract models such as prime event structures and occurrence nets. However it has not been settled what properties a reversible system should enjoy, nor how the various properties that have been suggested, such as the parabolic lemma and the causal-consistency property, are related. We contribute to a solution to these issues by using a generic labelled transition system equipped with a relation capturing whether transitions are independent to explore the implications between various reversibility properties. In particular, we show how all properties we consider are derivable from a set of axioms. Our intention is that when establishing properties of some formalism it will be easier to verify the axioms rather than proving properties such as the parabolic lemma directly. We also introduce two new properties related to causal consistent reversibility, namely causal liveness and causal safety, stating, respectively, that an action can be undone if (causal liveness) and only if (causal safety) it is independent from all the following actions. These properties come in three flavours: defined in terms of independent transitions, independent events, or via an ordering on events. Both causal liveness and causal safety are derivable from our axioms.

Figures (13)

• Figure 1: Irreversible transition systems in CCS.
• Figure 2: Proof of Proposition \ref{['prop:PL']}, case $t \neq u$.
• Figure 3: Implications between the main properties discussed in Section \ref{['sec:basic']}. We assume SP throughout.
• Figure 4: Rotations within a diamond (Example \ref{['ex:WFnotCC']}).
• Figure 5: The ladder of diamonds in the proof of Lemma .

Theorems & Definitions (168)

• Definition 2.1
• Definition 2.2: LTS with independence
• Definition 2.3: Reverse and combined LTS
• Remark 2.4
• Definition 3.1: Basic axioms
• Definition 3.2: Causal equivalence, cf. DK04
• Definition 3.3
• Proposition 3.4
• proof
• Corollary 3.5