Ivan Lanese
email: ivan.lanese@gmail.com

Iain Phillips
email: i.phillips@imperial.ac.uk

Irek Ulidowski
email: i.ulidowski@leicester.ac.uk

An Axiomatic Approach to Reversible Computation

Keywords: Reversible Computation, Labelled Transition System with Independence, Causal Safety, Causal Liveness

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, 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 these properties. In particular, we show how they 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 notions related to causal consistent reversibility, namely causal safety and causal liveness, and show that they are derivable from our axioms.

Introduction

Reversible computing studies computations which can proceed both in the standard, forward direction, and backward, going back to past states. Reversible computation has attracted interest due to its applications in areas as different as low-power computing [START_REF] Landauer | Irreversibility and heat generated in the computing process[END_REF], simulation [4], robotics [START_REF] Laursen | Automatic error recovery in robot assembly operations using reverse execution[END_REF], biological modelling [START_REF] Phillips | A reversible process calculus and the modelling of the ERK signalling pathway[END_REF] and debugging [23].

There is widespread agreement in the literature about what properties characterise reversible computation in the sequential setting. Thus in reversible finite state automata [START_REF] Pin | On the language accepted by finite reversible automata[END_REF], reversible cellular automata [START_REF] Kari | Reversible cellular automata: From fundamental classical results to recent developments[END_REF], reversible Turing machines [START_REF] Bennett | Logical reversibility of computation[END_REF] and reversible programming languages such as Janus [START_REF] Yokoyama | A reversible programming language and its invertible self-interpreter[END_REF] the main point is that the mapping from inputs to outputs is injective, and the reverse computation is deterministic.

Matters are less clear when it comes to reversible computation in the concurrent setting. Indeed, various reversible concurrent models have been studied, most notably in the areas of process calculi [START_REF] Danos | Reversible communicating systems[END_REF][START_REF] Phillips | Reversing algebraic process calculi[END_REF][START_REF] Lanese | Reversibility in the higher-order π-calculus[END_REF], event structures [START_REF] Ulidowski | Reversing event structures[END_REF], Petri nets [START_REF] Barylska | Reversible computation vs. 9. de Frutos Escrig[END_REF][START_REF] Melgratti | Reversing P/T nets[END_REF] and programming languages such as Erlang [START_REF] Lanese | A theory of reversibility for Erlang[END_REF].

A main result of this line of research is that the notion of reversibility most suited for concurrent systems is causal-consistent reversibility (other notions are also used, e.g., to model biological systems [START_REF] Phillips | A reversible process calculus and the modelling of the ERK signalling pathway[END_REF]). According to an informal account of causal-consistent reversibility, any action can be undone provided that its consequences, if any, are undone beforehand. Following [START_REF] Danos | Reversible communicating systems[END_REF] this account is formalised using the notion of causal equivalent traces: two traces are causal equivalent if and only if they only differ for swapping independent actions, and inserting or removing pairs of an action and its reverse. According to [START_REF] Danos | Reversible communicating systems[END_REF]Section 3] Backtracking an event is possible when and only when a causally equivalent trace would have brought this event as the last one which is then formalised as the so called causal consistency (CC) [6, Theorem 1], stating that coinitial computations are causal equivalent if and only if they are cofinal. Our new proof of CC (Proposition 3.6) shows that it holds in essentially any reversible formalism satisfying the Loop Lemma and the Parabolic Lemma, and we believe that CC is insufficient on its own to capture the informal notion.

A formalisation closer to the informal statement above is provided in [20, Corollary 22], stating that a forward transition t can be undone after a derivation iff all its consequences, if any, are undone beforehand. We are not aware of other discussions trying to formalise such a notion, except for [START_REF] Phillips | Reversibility and asymmetric conflict in event structures[END_REF], in the setting of reversible event structures. In [START_REF] Phillips | Reversibility and asymmetric conflict in event structures[END_REF], a reversible event structure is cause-respecting if an event cannot be reversed until all events it has caused have also been reversed; it is causal if it is cause-respecting and a reversible event can be reversed if all events it has caused have been reversed [START_REF] Phillips | Reversibility and asymmetric conflict in event structures[END_REF]Definition 3.34].

We provide (Section 4) a novel definition of the idea above, composed by: Causal Safety (CS): an action cannot be reversed until any actions caused by it have been reversed; Causal Liveness (CL): we should allow actions to reverse in any order compatible with CS, not necessarily the exact inverse of the forward order.

We shall see that CC does not capture the same property as CS+CL (Examples 4.15, 4.37), and that there are slightly different versions of CS and CL, which can all be proved under a small set of reasonable assumptions.

The main aim of this paper is to take an abstract model, namely labelled transition systems with independence equipped with reverse transitions (Section 2), and to show that the properties above (as well as others) can be derived from a small set of simple axioms (Sections 3, 4, 5). This is in sharp contrast with the large part of works in the literature, which consider specific frameworks such as CCS [START_REF] Danos | Reversible communicating systems[END_REF], CCS with broadcast [START_REF] Mezzina | On reversibility and broadcast[END_REF], CCB [START_REF] Kuhn | Local reversibility in a Calculus of Covalent Bonding[END_REF], π-calculus [START_REF] Cristescu | A compositional semantics for the reversible pi-calculus[END_REF], higher-order π [START_REF] Lanese | Reversibility in the higher-order π-calculus[END_REF], Klaim [START_REF] Giachino | Causal-consistent rollback in a tuple-based language[END_REF], Petri nets [START_REF] Melgratti | Reversing P/T nets[END_REF], μOz [START_REF] Lienhardt | A reversible abstract machine and its space overhead[END_REF] and Erlang [START_REF] Lanese | A theory of reversibility for Erlang[END_REF], and all give similar but formally unrelated proofs of the same main results. Such proofs will become instances of our general results. More precisely, our axioms will:

exclude behaviours which are not compatible with causal-consistent reversibility (as we will discuss shortly); -allow us to derive the main properties of reversible calculi which have been studied in the literature, such as CC (Proposition 3.6); -hold for a number of reversible calculi which have been proposed, such as RCCS [START_REF] Danos | Reversible communicating systems[END_REF] and reversible Erlang [START_REF] Lanese | A theory of reversibility for Erlang[END_REF] (Section 6).

Thus, when defining a new reversible formalism, one just has to check whether the axioms hold, and get for free the proofs of the most relevant properties. Notably, the axioms are normally easier to prove than the properties, hence the assessment of a reversible calculus gets much simpler. As a reference, Table 1 lists the axioms and properties used in this paper.

In order to understand which kinds of behaviours are incompatible with a causal-consistent reversible setting, consider the following LTSs in CCS: → 0: as above, but starting from the same process, hence showing that it is not enough to remember the initial configuration; P a → P where P = a.P : one can go back forever, against the idea that a state models a process reachable after a finite computation.

We remark that all such behaviours are perfectly reasonable in CCS, and they are dealt with in the reversible setting by adding history information about past actions. For example, in the first case one could remember the initial state, in the second case both the initial state and the action taken, and in the last case the number of iterations that have been performed. Due to space constraints, some proofs and additional results can only be found in the companion technical report [START_REF] Lanese | An axiomatic approach to reversible computation (TR)[END_REF].

Labelled Transition Systems with Independence

We want to study reversibility in a setting as general as possible. Thus, we base on the core of the notion of labelled transition system with independence (LTSI) [START_REF] Sassone | Models of concurrency: Towards a classification[END_REF]Definition 3.7]. However, while [START_REF] Sassone | Models of concurrency: Towards a classification[END_REF] requires a number of axioms on LTSI, we take the basic definition and explore what can be done by adding or not adding various axioms. Also, we extend LTSI with reverse transitions, since we study reversible systems. We define first labelled transition systems (LTSs).

We consider the LTS of the entire set of processes in a calculus, rather than the transition graph of a particular process and its derivatives, hence we do not fix an initial state. Definition 2.1. A labelled transition system (LTS) is a structure (Proc, Lab, ), where Proc is the set of states (or processes), Lab is the set of action labels and ⊆ Proc × Lab × Proc is a transition relation.

We let P, Q, . . . range over processes, a, b, c, . . . range over labels, and t, u, v, . . . range over transitions. We can write t : P a → Q to denote that t = (P, a, Q). We call a-transition a transition with label a.

Definition 2.2 (LTS with independence).

We say that (Proc, Lab, →, ι) is an LTS with independence (LTSI) if (Proc, Lab, →) is an LTS and ι is an irreflexive symmetric binary relation on transitions.

In many cases (see Section 6), the notion of independence coincides with the notion of concurrency. However, this is not always the case. Indeed, concurrency implies that transitions are independent since they happen in different processses, but transitions taken by the same process can be independent as well. Think, for instance, of a reactive process that may react in any order to two events arriving at the same time, and the final result does not depend on the order of reactions.

We shall assume that all transitions are reversible, so that the Loop Lemma [6, Lemma 6] holds. This does not hold in models of reversibility with control mechanisms such as irreversible actions [START_REF] Danos | Reversible communicating systems[END_REF][START_REF] Danos | Transactions in RCCS[END_REF] or a rollback operator [START_REF] Lanese | Controlling reversibility in higher-order pi[END_REF]. Nevertheless, when showing properties of models with controlled reversibility it has proved sensible to first consider the underlying models where all transitions are reversible, and then study how control mechanisms change the picture [START_REF] Giachino | Causal-consistent rollback in a tuple-based language[END_REF][START_REF] Lanese | A theory of reversibility for Erlang[END_REF]. The present work helps with the first step. Definition 2.3. Given (Proc, Lab, ), let the reverse LTS be (Proc, Lab, ), where P a Q iff Q a P . It is convenient to combine the two LTSs (forward and reverse): let the reverse labels be Lab = {a : a ∈ Lab}, and define the combined LTS to be → ⊆ Proc × (Lab ∪ Lab) × Proc by

P a → Q iff P a Q and P a → Q iff P a Q.
We stipulate that the union Lab∪Lab is disjoint. We let α, . . . range over Lab∪Lab.

For α ∈ Lab ∪ Lab, the underlying action label und(α) is defined as und(a) = a and und(a) = a. Let a = a for a ∈ Lab. Given t :

P α → Q, let t : Q α → P be the transition which reverses t.
We let ρ, σ, . . . range over finite sequences α 1 . . . α n , with ε P representing the empty sequence starting and ending at P . We shall write ε when P is understood. Given an LTS, a path is a sequence of forward or reverse transitions of the form

P 0 α1 → P 1 • • • αn → P n .
We let r, s, . . . range over paths. We may write r : P ρ → * Q where the intermediate states are understood. On occasion we may refer to a path simply by its sequence of labels ρ. Given a path r : P

ρ → * Q and R σ → * S are coinitial if P = R and cofinal if Q = S.
We say that a path is forward-only if it contains no reverse transitions.

Let (Proc, Lab, →) be an LTS. The irreversible processes in (Proc, Lab, →) are Irr = {P ∈ Proc : P }. A rooted path is a path r :

P ρ → * Q such that P ∈ Irr.
In the following we will consider LTSIs obtained by adding a notion of independence to combined LTSs as above. We will call the result a combined LTSI.

Basic Properties

In this section we show that most of the properties in the reversibility literature (see, e.g., [START_REF] Danos | Reversible communicating systems[END_REF][START_REF] Phillips | Reversing algebraic process calculi[END_REF][START_REF] Lanese | Reversibility in the higher-order π-calculus[END_REF][START_REF] Lanese | A theory of reversibility for Erlang[END_REF]), in particular the parabolic lemma and causal consistency, can be proved under minimal assumptions on the combined LTSI under analysis.

We formalise the minimal assumptions using three axioms, described below.

Definition 3.1 (Basic axioms).

Let L = (Proc, Lab, →, ι) be a combined LTSI. We say L satisfies:

Square Property (SP) if whenever t :

P α → Q, u : P β → R
→ P i for all i = 0, 1, . . ..
WF can alternatively be formulated using backward transitions, but the current formulation makes sense also in non-reversible calculi (e.g., CCS), which can be used as a comparison. Let us discuss the intuition behind these axioms. SP takes its name from the Square Lemma, where it is proved for concrete calculi and languages in [START_REF] Danos | Reversible communicating systems[END_REF][START_REF] Lanese | Reversibility in the higher-order π-calculus[END_REF][START_REF] Lanese | A theory of reversibility for Erlang[END_REF], and captures the idea that independent transitions can be executed in any order, that is they form commuting diamonds. SP can be seen as a sanity check on the chosen notion of independence. BTI generalises the key notion of backward determinism used in sequential reversibility (see, e.g., [START_REF] Pin | On the language accepted by finite reversible automata[END_REF] for finite state automata and [START_REF] Yokoyama | A reversible programming language and its invertible self-interpreter[END_REF] for the imperative language Janus) to a concurrent setting. Backward determinism can be spelled as "two coinitial backward transitions do coincide". This can be generalised to "two coinitial backward transitions are independent". Finally, WF means that we consider systems which have a finite past. That is, we consider systems starting from some initial state and then moving forward and back.

Axioms SP and BTI are related to properties which are part of the definition of (occurrence) transition systems with independence in [START_REF] Sassone | Models of concurrency: Towards a classification[END_REF]Definitions 3.7,4.1]. WF was used as an axiom in [START_REF] Phillips | Reversibility and models for concurrency[END_REF].

Using the minimal assumptions above we can prove relevant results from the literature. We first define causal equivalence, equating computations differing only for swaps of independent transitions and simplification of a transition with its reverse.

Definition 3.2 (cf. [6]

). Let (Proc, Lab, →, ι) be an LTSI satisfying SP. Let ≈ be the smallest equivalence relation on paths closed under composition and satisfying:

1. if t : P α → Q, u : P β → R are independent, and u : Q β → S, t : R α → S (which exist by SP) then tu ≈ ut ; 2. tt ≈ ε and tt ≈ ε.
We first consider the Parabolic Lemma ([6, Lemma 10]), which states that each path is causal equivalent to a backward path followed by a forward path. The proof of Proposition 3.4 (available in [START_REF] Lanese | An axiomatic approach to reversible computation (TR)[END_REF]) is very similar to that of [6, Lemma 10] except that in the latter BTI is shown directly as part of the proof.

A corollary of PL is that if a process is reachable from an irreversible process, then it is also forwards reachable from it. In other words, making a system reversible does not introduce new reachable states but only allows one to explore differently forwards reachable states. This is relevant in reversible debugging of concurrent systems [START_REF] Giachino | Causal-consistent reversible debugging[END_REF][START_REF] Lanese | A theory of reversibility for Erlang[END_REF], where one wants to find bugs that actually occur in forward-only computations. See the companion technical report [START_REF] Lanese | An axiomatic approach to reversible computation (TR)[END_REF]Corollary A.1]. We now move to causal consistency [6, Theorem 1]. Definition 3.5. Causal Consistency (CC): if r and s are coinitial and cofinal then r ≈ s.

Essentially, causal consistency states that history information allows one to distinguish computations which are not causal equivalent, indeed, if two computations are cofinal, that is they reach the same final state (which includes the stored history information) then they need to be causal equivalent.

Causal consistency frequently includes the other direction, namely that coinitial causal equivalent computations are cofinal, meaning that there is no way to distinguish causal equivalent computations. This second direction follows easily from the definition of causal equivalence.

Notably, our proof of CC below is very much shorter than existing proofs. UT was shown in the forward-only setting of occurrence TSIs in [START_REF] Sassone | Models of concurrency: Towards a classification[END_REF]Corollary 4.4]; it was taken as an axiom in [START_REF] Phillips | Reversibility and models for concurrency[END_REF].

Example 3.9 (PL alone does not imply WF or CC). Consider the LTSI with states P i for i = 0, 1, . . . and transitions t i : P i+1 a → P i , u i : P i+1 b → P i with a = b and t i ι u i . BTI and SP hold. Hence PL holds by Proposition 3.4. However clearly WF fails. Also t i and u i are coinitial and cofinal, and a = b, so that UT fails, and hence CC fails using Corollary 3.8. Note that the ab diamonds here have the same side states so are degenerate (cf. Lemma 4.4).

Causal Safety and Causal Liveness

In the literature, causal consistent reversibility is frequently informally described by saying that "a transition can be undone if and only if each of its consequences, if any, has been undone". In this section we study this property, where the two implications will be referred to as causal safety and causal liveness. We provide three different versions of such properties, based on independence of transitions (Section 4.2), ordering of events (Section 4.3), and independence of events (Section 4.4), and study their relationships. In order to define such properties we need the concept of event.

([P, α, Q]) = α.
Events are introduced as a derived notion in an LTS with independence in [START_REF] Sassone | Models of concurrency: Towards a classification[END_REF], in the context of forward-only computation. We have changed their definition by using coinitial independence at all corners of the diamond, yielding rotational symmetry. This reflects our view that forward and backward transitions have equal status.

Our definition can be simplified if the LTSI, and independence in particular, are well-behaved. Thus, we now add a further axiom related to independence. CPI states that independence is a property of commuting diamonds more than of their specific pairs of edges. Indeed, it allows independence to propagate around a commuting diamond.

Definition 4.3. If a combined LTSI satisfies axioms SP, BTI, WF and CPI,

we say that it is pre-reversible.

The name 'pre-reversible' indicates that we expect to require further axioms, but the present four are enough to ensure that LTSIs are well-behaved, with events compatible with causal equivalence. Pre-reversible axioms are separated from further axioms by a dashed line in Table 1.

The following non-degeneracy property was shown for occurrence transition systems with independence in [33, page 312], which have forward transitions only. We have to cope with backwards as well as forward transitions. We are now able to show independence of diamonds (ID), which can be seen as dual of SP. We now consider the interaction between events and causal equivalence. We need some notation first. Definition 4.8. Let r be a path in an LTSI L and let e be an event of L. Let (r, e) be the number of occurrences of transitions t in r such that t ∈ e, minus the number of occurrences of transitions t in r such that t ∈ e.

We now show that (r, e) is invariant under causal equivalent traces.

CS and CL via Independence of Transitions

We first define causal safety and liveness using the independence relation. 1. We say that L is causally safe (CS) if whenever

P a → Q, r : Q ρ → * R, (r, [P, a, Q]) = 0 and S a → R with (P, a, Q) ∼ (S,
a, R), then (P, a, Q) ι t for all t in r such that (r, [t]) > 0.

We say that L is causally live (CL) if whenever

P a → Q, r : Q ρ → * R
and (r, [P, a, Q]) = 0 and (P, a, Q) ι t, for all t in r such that (r, [t]) > 0, then we have S a → R with (P, a, Q) ∼ (S, a, R). We may wish to close the independence relation over this axiom: 1. Independence is mostly coinitial and given by closing under BTI and CPI. Additionally we make the leftmost atransition independent with all b-transitions. Note that all a-transitions belong to the same event, and all b-transitions belong to the same event. Also SP and WF hold, so that the LTSI is pre-reversible, and CC holds. However IRE does not hold. Furthermore CS fails using Definition 4.11. Indeed, consider any path bab → * from the start. CS would imply that the first b is independent with the a but this is not the case (we do have b ι a). Also CL fails using Definition 4.11. Indeed, consider any path abb → * from the start. Since the leftmost a-transition is independent with all b-transitions, we should be able to reverse a at the end of the path, but this is not possible.

The next axiom states that independence is fully determined by its restriction to coinitial transitions. This is related to axiom (E) of [33, page 325], but here we allow reverse as well as forward transitions.

then there are t 1 ∼ t 1 , t 2 ∼ t 2 such that t 1 and t 2 are coinitial and t 1 ι t 2 .

Thanks to previous axioms, independence behaves well w.r.t. reversing.

Proposition 4.18. If an LTSI satisfies SP, CPI, IRE, IEC then it also satisfies RPI.

All the axioms that we have introduced are independent, i.e. none is derivable from the remaining axioms. Proposition 4.19. SP, BTI, WF, CPI, IRE, IEC are independent of each other.

CS and CL via Ordering of Events

To define CS and CL via ordering of events, we define the causality relation ≤ on events. Previously, orderings on events have been defined using forward-only rooted paths; in fact, the definitions coincide for pre-reversible LTSIs. Proof. Straightforward using PL and Lemma 4.9.

We now give definitions of causal safety and causal liveness using ordering on events. Definition 4.24. Let L = (Proc, Lab, →, ι) be an LTSI.

1. We say that L is ordered causally safe (CS < ) if whenever

P a → Q, r : Q ρ → * R, (r, [P, a, Q]) = 0 and S a → R with (P, a, Q) ∼ (S, a, R), then [P, a, Q] < e
for all e such that (r, e ) > 0. 2. We say that L is ordered causally live (CL < ) if whenever and(r, [P, a, Q]) = 0 and [P, a, Q] < e for all e such that (r, e ) > 0 then we have S a → R with (P, a, Q) ∼ (S, a, R).

P a → Q, r : Q ρ → * R
We postpone giving proofs of CS < and CL < until we have introduced a further definition of causal safety and liveness using independence of events.

CS and CL via Independent Events

We now introduce a third version of causal safety and liveness, which uses independence like CS and CL, but on events rather than on transitions. First we lift independence from transitions to events. Definition 4.25 (Coinitially independent events). Let events e, e be (coinitially) independent, written e ci e , iff there are coinitial transitions t, t such that [t] = e, [t ] = e and t ι t . Thus in pre-reversible LTSIs, ci is fully determined just considering forward events. By Lemma 4.26, if we know e ci e then we know und(e) ci und(e ).

We can give a third formulation of causal safety and liveness using ci: Definition 4.27. Let L = (Proc, Lab, →, ι) be a pre-reversible LTSI.

1. We say that L is coinitially causally

(CS ci ) if whenever P a → Q, r : Q ρ → * R, (r, [P, a, Q]) = 0 and S a → R with (P, a, Q) ∼ (S, a, R), then [P, a, Q] ci
e for all forward events e such that (r, e) > 0.

We say that L is coinitially causally live

(CL ci ) if whenever P a → Q, r : Q ρ → * R and (r, [P, a, Q]) = 0 and [P, a, Q] ci e,
for all forward events e such that (r, e) > 0, then we have S a → R with (P, a, Q) ∼ (S, a, R).

Note that in Definition 4.27 we operate at the level of events, rather than at the level of transitions as in Definition 4.11.

Theorem 4.28. If an LTSI is pre-reversible then it satisfies CS ci .

We now introduce a weaker version of axiom IRE (Definition 4.12).

Definition 4.29 (Coinitial IRE (CIRE)). If [t] ci [u] and t, u are coinitial then t ι u.

Theorem 4.30. If a pre-reversible LTSI satisfies CIRE then it satisfies CL ci . We next give an example where CC holds but not CS ci (and not CPI).

Example 4.31. Consider the cube with transitions a, b, c on the left in Figure 2, where the forward direction is from left to right. We add independence as given by BTI. So SP, BTI, WF hold, but not CPI. From the start we have an atransition followed by a path r = bc followed by a. For CS ci to hold, we want a to be the reverse of the same event as the first a. They are connected by a ladder with sides cb. We add independence for all corners on the two faces of the ladder (ab and ac). Then we get bc ≈ cb (independence at a single corner is enough). However the bs are not the same event since the bc face does not have independence at each corner. Therefore we do not get [a] ci [b], and CS ci fails. We next give an example where CS ci and CL ci hold but not CC.

→ P i , P i+1 c → P i , Q i+1 c → Q i , P i+1 a → Q i for i = 0, 1, .
. .. This is shown on the right in Figure 2. Clearly WF does not hold. We add coinitial independence to make BTI and CPI hold. Then also SP and CIRE hold. However, CC fails since, for example P 1 a → Q 0 b → P 0 and P 1 c → P 0 are coinitial and cofinal but not causally equivalent. Note that there are just three events a, b, c with a ci c, b ci c but not a ci b. CS ci and CL ci hold. Indeed, c is independent from every other action, and it can always be undone, while a and b are independent from c only and they can be undone after any path composed by c and no others.

Polychotomy

In this section we relate our three versions of causal safety and liveness, with the help of what we call polychotomy, which states that if events do not cause each other and are not in conflict, then they must be independent. We start by defining a conflict relation on events. Definition 4.33. Two forward events e, e are in conflict, written e # e , if there is no rooted path r such that (r, e) > 0 and (r, e ) > 0.

Much as for orderings, conflict on events has been defined previously using forward-only rooted paths [START_REF] Van Glabbeek | The difference between splitting in n and n + 1[END_REF][START_REF] Phillips | Reversibility and models for concurrency[END_REF]; in fact, the definitions coincide for pre-reversible LTSIs. We omit the details.

Definition 4.34 (Polychotomy).

Let L be a pre-reversible LTSI. We say that L satisfies polychotomy if whenever e, e are forward events, then exactly one of the following holds: 1. e = e ; 2. e < e ; 3. e < e; 4. e # e ; or 5. e ci e .

Property NRE below is related to polychotomy.

any forward event e we have (r, e) ≤ 1.

Lemma 4.36 (Polychotomy).

Suppose that a pre-reversible LTSI satisfies NRE. Then polychotomy holds. Example 4.37. Consider the LTSI in Figure 3. We add independence to make BTI and CPI hold. Both SP and WF hold. Hence, CC holds as well. There are three events, labelled with a, b, c. Clearly NRE fails for both a and b. We see that a < c but also a ci c, so that polychotomy fails. CS ci holds by Theorem 4.28. However CS < fails: consider the transition P a → Q together with the path r : Example 4.43. Consider the LTSI in Figure 4. Independence is given by closing under BTI and CPI. There are three events, labelled a, b, c, which are all independent of each other. We see that NRE holds but not CIRE. Also CL ci and CL < fail: consider

Q bc → * R
P a → Q b → R, where a cannot be reversed at R.

Coinitial Independence

In this section we consider coinitial LTSIs, defined as follows, and their relationship with LTSIs in general.

Definition 5.1. Let L = (Proc, Lab, →, ι) be a combined LTSI. Then ι is coinitial if for all transitions t, u, if t ι u then t and u are coinitial. We say that L is coinitial if ι is coinitial.

We define a mapping c restricting general independence to coinitial transitions and a mapping g extending independence along events. Definition 5.2. Given an LTSI (Proc, Lab, →, ι), define t g(ι) u iff t ∼ t ι u ∼ u for some t , u . Furthermore, define t c(ι) u iff t ι u and t, u are coinitial. Proposition 5.3. Let L = (Proc, Lab, →, ι) be a pre-reversible LTSI. In some reversible calculi (such as RCCS) independence of coinitial transitions is defined purely by reference to the labels. If this is the case it is a simple matter to verify the axioms CPI and CIRE. Proof. Straightforward, noting that labels on opposite sides of a diamond of transitions must be equal.

Note that I must be irreflexive, since ι is irreflexive.

If we have a coinitial pre-reversible LTSI satisfying CIRE then CS < and CL < hold (using Proposition 4.42 and Proposition 4.39). Applying mapping g we get a general pre-reversible LTSI satisfying IRE and IEC by Proposition 5.3. This will satisfy CS and CL as a result of applying Theorem 4.13 and Theorem 4.14 respectively. It will also satisfy CS < and CL < . Conversely, if we have a general pre-reversible LTSI satisfying IRE then CS and CL hold by Theorem 4.13 and Theorem 4.14 respectively. Applying mapping c we get a coinitial pre-reversible LTSI satisfying CIRE. This will satisfy CS < and CL < .

Case Studies

We look at whether our axioms hold in various reversible formalisms. Remarkably, all the works below provide proofs of the Loop Lemma.

RCCS

We consider here the semantics of RCCS in [START_REF] Danos | Reversible communicating systems[END_REF], and restrict the attention to coherent processes [6, Definition 2]. In RCCS, transitions Definition 7]. This allows us to define coinitial independence as t ι u iff t and u are concurrent. We now argue that the resulting coinitial LTSI is pre-reversible and also satisfies CIRE. SP was shown in [6, Lemma 8]. BTI was shown in the proof of [START_REF] Danos | Reversible communicating systems[END_REF]Lemma 10]. WF is straightforward, noting that backward transitions decrease memory size. Hence, we obtain a very much simplified proof of CC. For CPI and CIRE we note that independence is defined on the underlying labels and thus Proposition 5.4 applies. Therefore CS < and CL < hold. Using Proposition 5.3, we can get an LTSI with general independence satisfying IRE and IEC, and therefore CS and CL. This is the first time these causal properties have been proved for RCCS.

P μ:ζ → Q and P μ :ζ → Q are concurrent if μ ∩ μ = ∅ [6,

HOπ

We consider here the uncontrolled reversible semantics for HOπ [START_REF] Lanese | Reversibility in the higher-order π-calculus[END_REF]. We restrict our attention to reachable processes, called there consistent. The semantics is a reduction semantics; hence there are no labels (or, equivalently, all the labels coincide). To have more informative labels we can consider the transitions defined in [18, Section 3.1], where labels are composed of memory information and a flag denoting whether the transition is forward or backward. The notion of independence would be given by the concurrency relation on coinitial transitions [START_REF] Lanese | Reversibility in the higher-order π-calculus[END_REF]Definition 9]. All pre-reversible LTSI axioms hold, as well as CIRE which is needed for causal safety and liveness. Specifically, SP is proved in [START_REF] Lanese | Reversibility in the higher-order π-calculus[END_REF]Lemma 9]. BTI holds since distinct memories have disjoint sets of keys [18, Definition 3 and Lemma 3] and by the definition of concurrency [START_REF] Lanese | Reversibility in the higher-order π-calculus[END_REF]Definition 9]. WF holds as each backward step consumes a memory, which is finite to start with. Finally, CPI and CIRE are valid since the notion of concurrency is defined on the annotated labels and using our Proposition 5.4.

As a result we obtain a very much simplified proof of CC. Moreover, using CPI and CIRE, we get the CS < and CL < safety and liveness properties and, applying mapping g from Section 5, we get a general pre-reversible LTSI satisfying IRE and IEC, hence CS and CL are satisfied. This is the first time that causal properties have been shown for HOπ.

Rπ

We consider the (uncontrolled) reversible semantics for π-calculus defined in [START_REF] Cristescu | A compositional semantics for the reversible pi-calculus[END_REF]. We restrict the attention to reachable processes. The semantics is an LTS semantics. Independence is given as concurrency which is defined for consecutive transitions [START_REF] Cristescu | A compositional semantics for the reversible pi-calculus[END_REF]Definition 4.1]. CC holds [START_REF] Cristescu | A compositional semantics for the reversible pi-calculus[END_REF]Theorem 4.5].

Our results are not directly applicable to Rπ, since SP holds up to label equivalence of transitions on opposite sides of the diamond, rather than equality of labels as in our approach. We would need to extend axiom SP and the definition of causal equivalence to allow for label equivalence in order to handle Rπ using our axiomatic method.

Erlang We consider the uncontrolled reversible (reduction) semantics for Erlang in [START_REF] Lanese | A theory of reversibility for Erlang[END_REF]. We restrict our attention to reachable processes. In order to have more informative labels we can consider the annotations defined in [20, Section 4.1]. We then can define coinitial transitions to be independent if they are concurrent [START_REF] Lanese | A theory of reversibility for Erlang[END_REF]Definition 12].

We next discuss the validity of our axioms in reversible Erlang. SP is proved in [20, Lemma 13] and BTI is trivial from the definition of concurrency [START_REF] Lanese | A theory of reversibility for Erlang[END_REF]Definition 12]. WF holds since the pairs of integers (total number of elements in memories, total number of messages queued) ordered under lexicographic order are always positive and decrease at each backward step. Intuitively, each step but the ones derived using the rule for reverse sched (see [START_REF] Lanese | A theory of reversibility for Erlang[END_REF]Figure 11]) consumes an item of memory, and each step derived using rule reverse sched removes a message from a process queue. Finally, CPI and CIRE hold since the notion of concurrency is defined on the annotated labels, and by Proposition 5.4.

Since this the setting is very similar to the one of HOπ (both calculi have a reduction semantics and a coinitial notion of independence defined on enriched labels), we get the same results as for HOπ, including CC, and CS and CL.

Reversible occurrence nets Reversible occurrence nets [START_REF] Melgratti | Reversing P/T nets[END_REF][START_REF] Melgratti | Reversing Place Transition nets[END_REF] are traditional occurrence nets (safe and with no backward conflicts) extended with a reverse transition for each forward transition. They give rise to an LTS where states are pairis (N, m) with N a net and m a marking. A computation that represents firing a transition t in (N, m) and resulting in (N, m ) is given by a firing relation (N, m) t → (N, m ). The notion of independence is the concurrency relation [START_REF] Melgratti | Reversing P/T nets[END_REF]Section 3] which is defined between arbitrary firings (transitions). Hence, we get a general LTSI. The CC property is shown by following the traditional approach in [START_REF] Danos | Reversible communicating systems[END_REF]. SP and PL are shown as well. PL and CC require several pages of proofs [START_REF] Melgratti | Reversing Place Transition nets[END_REF]. The causal safety and causal liveness properties are not considered in [START_REF] Melgratti | Reversing P/T nets[END_REF][START_REF] Melgratti | Reversing Place Transition nets[END_REF].

We can obtain CC, and additionally CS and CL, as follows. SP and BTI are proved for reversible occurrence nets in [START_REF] Melgratti | Reversing Place Transition nets[END_REF] as Lemma 4.3 and Lemma 3.3 respectively. WF holds because there are no forward cycles of firings in occurrence nets, hence no infinite reverse paths. In order to have CS and CL, we need to show CPI and IRE. Lemma 3.4 in [START_REF] Melgratti | Reversing Place Transition nets[END_REF] gives CPI. Events can be defined on firings as in our Definition 4.5, and then IRE holds as the concurrency relation preserves such events.

Conclusion, Related and Future Work

The literature on causal-consistent reversibility (see, for example the early survey [START_REF] Lanese | Causal-consistent reversibility[END_REF]) has a number of proofs of results such as the parabolic lemma (PL) and the causal consistency property (CC), all of which are instantiated to a specific calculus, language or formalism. We have taken here a complementary approach, analysing the properties of interest in an abstract and language-independent setting. In particular, we have shown how to prove the most relevant of these properties from a small number of axioms.

Our approach builds upon [START_REF] Phillips | Reversibility and models for concurrency[END_REF], where a set of axioms for reverse LTSs was given and several interesting properties were shown. While the idea is similar, the development is rather different since we consider more basic axioms (we only share WF, while many of the axioms in [START_REF] Phillips | Reversibility and models for concurrency[END_REF], such as UT, follow from ours), and since the two papers focus on different properties. We focus on CC and various forms of CS and CL, while [START_REF] Phillips | Reversibility and models for concurrency[END_REF] considers correspondence with prime event structures and reversible bisimulations. Moreover, LTSs in [START_REF] Phillips | Reversibility and models for concurrency[END_REF] do not have a notion of independence.

In other related work, we may particularly mention [START_REF] Danos | General reversibility[END_REF], which like ours takes an abstract view, though based on category theory. However, its results concern irreversible actions, and do not provide insights in our setting, where all actions are reversible. The only other work which takes a general perspective is [START_REF] Bernadet | A modular formalization of reversibility for concurrent models and languages[END_REF], which concentrates on how to derive a reversible extension of a given formalism. However, proofs concern a limited number of properties (essentially our CC), and hold only for extensions built using the technique proposed there. Also [START_REF] Phillips | Reversing algebraic process calculi[END_REF][START_REF] Phillips | Reversing algebraic process calculi[END_REF] are general, since they propose how to reverse a calculus that can be defined in a general format of SOS rules. However, the format has its syntactic constraints while our approach abstracts from them. Finally, [9] presents a number of properties such as, for example, backward confluence, which arise in the context of reversing of steps of executed transitions in Place/Transition nets.

The approach proposed in this paper opens a number of new possibilities. Firstly, when devising a new reversible formalism, our results provide a rich toolbox to prove (or disprove) relevant properties in a simple way. This is particularly relevant since causal-consistent reversibility is getting applied to more and more complex languages, such as Erlang [START_REF] Lanese | A theory of reversibility for Erlang[END_REF], where direct proofs become cumbersome and error-prone. Secondly, our abstract proofs are relatively easy to formalise in a proof-assistant, which is even more relevant given that this will certify the correctness of the results for many possible instances. Another possible extension of our work concerns integrating into our framework irreversible actions [START_REF] Danos | Transactions in RCCS[END_REF]. In order to do that we could take inspiration from the above-mentioned [START_REF] Danos | General reversibility[END_REF].

→ 0 :

 0 from state 0 one does not know whether to go back to a.0 or to b.0; a.0 + b.0 a → 0, a.0 + b.0 b

ρ→

  * Q, the inverse path is r : Q ρ → * P where ε = ε and αρ = ρ α. The length of a path r (notated |r|) is the number of transitions in the path. Paths r : P

Definition 3 . 3 .Proposition 3 . 4 .

 3334 Parabolic Lemma (PL): for any path r there are forwardonly paths s, s such that r ≈ ss and |s| + |s | ≤ |r|. Suppose an LTSI satisfies BTI and SP. Then PL holds.

Proposition 3 . 6 .Corollary 3 . 8 .

 3638 Suppose an LTSI satisfies WF and PL. Then CC holds. Proof. Let r : P ρ → * Q and r : P ρ → * Q. Using WF, let I, s be such that s : I σ → * P , I ∈ Irr. Now srsr is a path from I to I, and so by PL there are r 1 , r 2 forward-only such that r 1 r 2 ≈ srsr . But I ∈ Irr and so r 1 = ε and r 2 = ε. Thus ε ≈ srsr , so that sr ≈ sr and r ≈ r as required. Causal consistency implies the unique transition property. Definition 3.7. An LTSI (Proc, Lab, →, ι) satisfies Unique Transition (UT) if P a → Q and P b → Q imply a = b. If an LTSI satisfies CC then it satisfies UT.

Definition 4 . 2 (

 42 Coinitial Propagation of Independence (CPI)). If t : Pα → Q, u : P β → R, u : Q β → Sand t : R α → S with t ι u, then u ι t .

Lemma 4 . 4 .

 44 Suppose that an LTSI is pre-reversible. If we have a diamond t : P α → Q, u : P β → R with t ι u together with cofinal transitions u : Q β → S and t : R α → S, then the diamond is non-degenerate, meaning that P, Q, R, S are distinct states. If an LTSI is pre-reversible then by Lemma 4.4 and the use of CPI we can simplify the statement of Definition 4.1 to: Definition 4.5 (Event, simplified definition). Let (Proc, Lab, →, ι) be a prereversible LTSI. Let ∼ be the smallest equivalence relation satisfying: if t : P α → Q, u : P β → R, u : Q β → S, t : R α → S, and t ι u, then t ∼ t .

Definition 4 . 6 (Proposition 4 . 7 .

 4647 Independence of Diamonds (ID)). An LTSI satisfies the Independence of Diamonds property (ID) if whenever we have a diamond t :P α → Q, u : P β → R, u : Q β → Sand t : R α → S, with -Q = R if α and β are both forwards or both backwards; -P = S otherwise; then t ι u. If an LTSI satisfies BTI and CPI then it satisfies ID.

Lemma 4 . 9 .Proposition 4 . 10 .

 49410 Let L be a pre-reversible LTSI. Let r ≈ s. Then for each event e we have that (r, e) = (s, e). Lemma 4.9 generalises what was shown for the forward-only setting in[START_REF] Sassone | Models of concurrency: Towards a classification[END_REF] Corollary 4.3]. If an LTSI is pre-reversible, then for any rooted path r and any forward event e we have (r, e) ≥ 0.

Definition 4 . 11 .

 411 Let L = (Proc, Lab, →, ι) be a pre-reversible LTSI.

  Fig. 1.

Definition 4 . 20 .

 420 Let L = (Proc, Lab, →, ι) be an LTSI. Let e, e be events of L. Let e ≤ e iff for all rooted paths r, if (r, e ) > 0 then (r, e) > 0. As usual e < e means e ≤ e and e = e . If e < e we say that e is a cause of e . Lemma 4.21. If an LTSI satisfies SP, BTI, WF and CPI then ≤ is a partial ordering on events.

Definition 4 .

 4 22 ([12,28]). Let L = (Proc, Lab, →, ι) be an LTSI. Let e, e be events of L. Let e ≤ f e iff for all rooted forward-only paths r, if r contains a representative of e then r also contains a representative of e. Lemma 4.23. For any LTSI, e ≤ e implies e ≤ f e . If an LTSI satisfies SP, BTI, WF and CPI then e ≤ f e implies e ≤ e .

Lemma 4 . 26 .

 426 If an LTSI is pre-reversible, then if e ci e we have also e ci e .

Fig. 2 .

 2 Fig. 2.

Definition 4 . 35 (

 435 Fig. 3.

  and S a → R, and note that a < c. The next lemma allows us to connect ordered safety and liveness with coinitial safety and liveness. Lemma 4.38. Suppose that a pre-reversible LTSI satisfies NRE. Suppose P a → Q, e = [P, a, Q], r : Q ρ → * R and (r, e ) > 0 where e is a forward event. Then exactly one of e ci e and e < e holds. Proposition 4.39. Suppose that a pre-reversible LTSI L satisfies NRE. Then 1. L satisfies CS < . 2. L satisfies CL ci iff L satisfies CL < . Property RED below is also related to NRE and polychotomy. Definition 4.40. An LTSI satisfies Reverse Event Determinism (RED) if whenever t, t are backward coinitial transitions and t ∼ t then t = t . Proposition 4.41. If a LTSI L is pre-reversible then the following are equivalent: 1. L satisfies NRE; 2. L satisfies RED; 3. independence ci is irreflexive on events; and 4. polychotomy holds. Proposition 4.42. Suppose that a pre-reversible LTSI satisfies CIRE. Then it also satisfies NRE. NRE was shown in the forward-only setting of occurrence transition systems with independence in [33, Corollary 4.6]. It was also shown in the reversible setting without independence in [28, Proposition 2.10].

Fig. 4 .

 4 Fig. 4.

Proposition 5 . 4 .

 54 Let L = (Proc, Lab, →, ι) be a coinitial combined LTSI. Suppose that I is a binary relation on Lab such that for any coinitial transitions t : P α → Q and u : P β → R we have t ι u iff I(a, b), where a and b are the underlying labels a = und(α), b = und(β). Then L satisfies CPI and CIRE.

Table 1 .

 1 Axioms and properties for causal reversibility.

4.1 Events Definition 4.1 (Event, general definition).

  Let (Proc, Lab, →, ι) be an LTSI.Let ∼ be the smallest equivalence relation satisfying: if t : P S, and t ι u, u ι t , t ι u , u ι t, and-Q = R if αand β are both forwards or both backwards; -P = S otherwise; then t ∼ t . The equivalence classes of forward transitions, written [P, a, Q], are the events. The equivalence classes of reverse transitions, written [P, a, Q], are the reverse events. Define a labelling function from → / ∼ to Lab by setting

α → Q, u : P β → R, u : Q β → S, t : R α →

1 .

 1 If L is coinitial and satisfies CIRE then L = (Proc, Lab, →, g(ι)) is a prereversible LTSI and satisfies IRE and IEC. 2. if L satisfies IRE then L = (Proc, Lab, →, c(ι)) is a pre-reversible coinitial LTSI and satisfies CIRE.

	Thanks to Proposition 5.3, we can extend a coinitial pre-reversible LTSI sat-
	isfying CIRE in a canonical way to a pre-reversible LTSI satisfying IRE and
	IEC.

Extending Horizons of Computing. The first author has also been partially supported by French ANR project DCore ANR-18-CE25-0007 and by INdAM as a member of GNCS (Gruppo Nazionale per il Calcolo Scientifico).