LEMMA 6.6. Given an LTSI $\mathcal{L}$, $t \sim u$ implies $t g(\sim) u$.

PROOF. By definition of $\sim$, noticing that $\iota \subseteq g(\iota)$.

☐

LEMMA 6.7. Given a pre-reversible LTSI $\mathcal{L}$, $t g(\sim) u$ implies $t \sim u$.

PROOF. By definition of $\sim$, we have $t g(\sim) u$ if there is a chain of commuting squares connecting $t$ and $u$. Thanks to ID (which holds in pre-reversible LTSIs) all such squares are commuting squares in $\mathcal{L}$, hence $t \sim u$ as desired. ☐

We can now study the impact of $c$ and $g$ on the axioms satisfied by the LTSI to which they are applied.

PROPOSITION 6.8. Let $\mathcal{L} = (\text{Proc}, \text{Lab}, \to, \iota)$ be a pre-reversible LTSI.

(1) if $\mathcal{L}$ is coinomial and satisfies CIRE then $c(g(\iota)) = \iota$;

(2) if $\mathcal{L}$ satisfies IRE and IEC then $g(c(\iota)) = \iota$;

(3) If $\mathcal{L}$ is coinomial and satisfies CIRE then $g(\mathcal{L})$ is a pre-reversible LTSI and satisfies IRE and IEC.

(4) if $\mathcal{L}$ satisfies IRE then $c(\mathcal{L})$ is a pre-reversible coinomial LTSI and satisfies CIRE.

PROOF. (1) Clearly $\iota \subseteq c(g(\iota))$. For the converse, suppose $t \sim t' \iota u' \sim u$ and $t', u'$ are coinomial and $t, u$ are coinomial. Then $t \iota u$ by CIRE.

(2) Suppose $t \iota u$. By IEC we have $t \sim t' \iota u' \sim u$ with $t', u'$ coinomial. Hence $t g(c(\iota)) u$. Conversely, suppose $t g(c(\iota)) u$. Then $t \iota u$ by IRE.

(3) Suppose $t g(\iota) u$ and $t, u$ are coinomial. Then by CIRE $t \iota u$. So we can use SP for $\iota$ to complete the diamond. Hence SP holds for $\mathcal{L}$'.

Clearly PCI holds for $g(\mathcal{L})$ since $g(\iota)$ and $\iota$ agree on coinomial transitions by CIRE.

For IRE, suppose $t' \sim t g(\iota) u \sim u'$. Then clearly $t' g(\iota) u'$.

Finally, for IEC suppose $t g(\iota) u$. Then $t \sim t' \iota u' \sim u$ with $t', u'$ coinomial, which is exactly what is needed for IEC.

(4) Immediate. ☐

Thanks to Proposition 6.8, we can extend a coinomial pre-reversible LTSI satisfying CIRE in a canonical way to a pre-reversible LTSI satisfying IRE and IEC.

Note that $g(\mathcal{L})$ satisfies IRE (and hence ECH) by construction, since $t g(\iota) u \sim t'$ implies $t g(\iota) t'$. Conditions in Proposition 6.8, item (3) are only needed for the other properties.

## 6.2 Label-generated independence

In some reversible calculi (such as RCCS) independence of coinomial transitions is defined purely by reference to the labels.

**Definition 6.9.** Coinomial label-generated (CLG): if there is an irreflexive binary relation $I$ on Lab, called a *generator relation*, such that for any transitions $t: P \xrightarrow{\alpha} Q$ and $u: P \xrightarrow{\beta} R$ we have $t \iota u$ iff $t$ and $u$ are coinomial and $I(a, b)$, where $a$ and $b$ are the underlying labels $a = \text{und}(\alpha)$, $b = \text{und}(\beta)$.

If this is the case then the axioms IC, PCI and CIRE hold by construction.

PROPOSITION 6.10. If an LTSI is CLG then it satisfies IC, PCI and CIRE.

PROOF. Straightforward, noting for PCI and CIRE that labels on opposite sides of a diamond of transitions must be equal. ☐

Note that $I$ must be irreflexive, since $\iota$ is irreflexive by definition. Even more, we already have seen that for a pre-reversible LTSI there cannot be independent coinomial transitions $t, u$ with the same underlying label (as a consequence of Lemma 4.4 and BLD).
**Definition 6.11.** Label-generated (LG): if there is an irreflexive binary relation *I* on Lab, called a *generator relation*, such that for any transitions *t*: *P* $\xrightarrow{\alpha}$ *Q* and *u*: *R* $\xrightarrow{\beta}$ *S* we have *t* ⊢ *u* iff *I*(*a*, *b*), where *a* and *b* are the underlying labels *a* = und(*α*), *b* = und(*β*).

**PROPOSITION 6.12.** If an LTSI is LG then it satisfies PCI, IRE and RPI.

**PROOF.** Straightforward. □

Note that LG does not imply IEC, in view of the following example.

*Example 6.13.* Consider the LTSI with two transitions $t: P \xrightarrow{a} Q$ and $u: R \xrightarrow{b} S$, where all states are distinct (as in Example 5.16) and $a \neq b$. Let independence be generated by the relation $I = \{(a, b)\}$. Then LG holds, but not IEC, since $t \nvDash u$ but not $[t] \text{ ci } [u]$. ◇

However, LG is compatible with IEC, in view of the following example.

*Example 6.14.* Let $t: P \xrightarrow{a} Q$, $u: P \xrightarrow{b} R$, $u': Q \xrightarrow{b} S$, $t': R \xrightarrow{a} S$, where all states are distinct and $a \neq b$. Let independence be generated by the relation $I = \{(a, b)\}$. Then both LG and IEC hold. However IC fails. ◇

All the axioms and properties we have considered in the previous sections are closed under disjoint unions of LTSIs, defined as follows.

**Definition 6.15 (Disjoint union of LTSIs).** Let (Proc₁, Lab₁, →₁, t₁) and (Proc₂, Lab₂, →₂, t₂) be LT-SIs. Their disjoint union is (Proc₁ ∪ Proc₂, Lab₁ ∪ Lab₂, →₁ ∪ →₂, t₁ ∪ t₂) provided that Proc₁ ∩ Proc₂ = ∅, and undefined otherwise.

However LG and CLG are not necessarily closed under disjoint unions of LTSIs, in view of the following examples.

*Example 6.16.* Take the disjoint union of the LTSI of Example 6.14 together with a further transition $T \xrightarrow{a} U$ with an empty generator relation (this component satisfies LG). Then LG fails; however IEC and IRE still hold. ◇

*Example 6.17.* Take the disjoint union of the LTSI of Example 5.7 (which satisfies CLG) together with further transitions $T \xrightarrow{a} U$ and $T \xrightarrow{b} V$ with an empty generator relation (this component satisfies CLG). Then CLG fails; however IC and CIRE still hold. ◇

The mapping *g* converts an LTSI satisfying CLG into one satisfying LG+IEC. The mapping *c* converts an LTSI satisfying LG into one satisfying CLG. Note that there is an alternative way to convert an LTSI satisfying CLG into one satisfying LG: simply use the relation *I* applied to any pair of transitions. This will in general create more independent transitions than using *g*, and so the result may not satisfy IEC.

## 6.3 Relating different forms of CS/CL

We now discuss the relationships between different forms of CS/CL and consider which ones to work with in particular reversible settings. The starting point is how independence is or can be defined in such settings, and whether it is general or coinitial. We explain how structural axioms and results of this section, together with our axioms, can be used to arrive at the most appropriate causal safety and liveness properties for such reversible settings.

We can sometimes move between LTSIs satisfying CS<sub>ci</sub> and CL<sub>ci</sub> (or equivalently CS< and CL<), all defined in terms of coinitial independence, and LTSIs satisfying CS<sub>t</sub> and CL<sub>t</sub>, which are based
**Definition 6.11.** Label-generated (LG): if there is an irreflexive binary relation *I* on Lab, called a *generator relation*, such that for any transitions *t*: *P* $\xrightarrow{\alpha}$ *Q* and *u*: *R* $\xrightarrow{\beta}$ *S* we have *t* ⊢ *u* iff *I(a, b)*, where *a* and *b* are the underlying labels *a* = und(*α*), *b* = und(*β*).

**PROPOSITION 6.12.** If an LTSI is LG then it satisfies PCI, IRE and RPI.

**PROOF.** Straightforward. □

Note that LG does not imply IEC, in view of the following example.

*Example 6.13.* Consider the LTSI with two transitions $t: P \xrightarrow{a} Q$ and $u: R \xrightarrow{b} S$, where all states are distinct (as in Example 5.16) and $a \neq b$. Let independence be generated by the relation $I = \{(a, b)\}$. Then LG holds, but not IEC, since $t \nvDash u$ but not $[t] \text{ ci } [u]$. ◇

However, LG is compatible with IEC, in view of the following example.

*Example 6.14.* Let $t: P \xrightarrow{a} Q$, $u: P \xrightarrow{b} R$, $u': Q \xrightarrow{b} S$, $t': R \xrightarrow{a} S$, where all states are distinct and $a \neq b$. Let independence be generated by the relation $I = \{(a, b)\}$. Then both LG and IEC hold. However IC fails. ◇

All the axioms and properties we have considered in the previous sections are closed under disjoint unions of LTSIs, defined as follows.

**Definition 6.15 (Disjoint union of LTSIs).** Let (Proc₁, Lab₁, →₁, t₁) and (Proc₂, Lab₂, →₂, t₂) be LT-SIs. Their disjoint union is (Proc₁ ∪ Proc₂, Lab₁ ∪ Lab₂, →₁ ∪ →₂, t₁ ∪ t₂) provided that Proc₁ ∩ Proc₂ = ∅, and undefined otherwise.

However LG and CLG are not necessarily closed under disjoint unions of LTSIs, in view of the following examples.

*Example 6.16.* Take the disjoint union of the LTSI of Example 6.14 together with a further transition $T \xrightarrow{a} U$ with an empty generator relation (this component satisfies LG). Then LG fails; however IEC and IRE still hold. ◇

*Example 6.17.* Take the disjoint union of the LTSI of Example 5.7 (which satisfies CLG) together with further transitions $T \xrightarrow{a} U$ and $T \xrightarrow{b} V$ with an empty generator relation (this component satisfies CLG). Then CLG fails; however IC and CIRE still hold. ◇

The mapping *g* converts an LTSI satisfying CLG into one satisfying LG+IEC. The mapping *c* converts an LTSI satisfying LG into one satisfying CLG. Note that there is an alternative way to convert an LTSI satisfying CLG into one satisfying LG: simply use the relation *I* applied to any pair of transitions. This will in general create more independent transitions than using *g*, and so the result may not satisfy IEC.

## 6.3 Relating different forms of CS/CL

We now discuss the relationships between different forms of CS/CL and consider which ones to work with in particular reversible settings. The starting point is how independence is or can be defined in such settings, and whether it is general or coinitial. We explain how structural axioms and results of this section, together with our axioms, can be used to arrive at the most appropriate causal safety and liveness properties for such reversible settings.

We can sometimes move between LTSIs satisfying CS<sub>ci</sub> and CL<sub>ci</sub> (or equivalently CS< and CL<), all defined in terms of coinitial independence, and LTSIs satisfying CS<sub>t</sub> and CL<sub>t</sub>, which are based
on general independence, using mappings *c* and *g*. Thus, if we have a coin initial pre-reversible LTSI
*L* satisfying CIRE then CS<sub>ci</sub> and CL<sub>ci</sub> hold (using Theorems 5.20 and 5.29, respectively). The LTSI
g(*L*) is pre-reversible and satisfies IRE and IEC by Proposition 6.8. This will satisfy CS<sub>t</sub> and CL<sub>t</sub> as
a result of applying Theorems 5.5 and 5.6, respectively. It will also satisfy CS<sub>ci</sub> and CL<sub>ci</sub>. Conversely,
if we have a general pre-reversible LTSI *L'* satisfying IRE then CS<sub>t</sub> and CL<sub>t</sub> hold by Theorems 5.5
and 5.6, respectively. The LTSI *c*(*L'* ) is a coin initial pre-reversible LTSI satisfying CIRE. This will
satisfy CS<sub>ci</sub> and CL<sub>ci</sub>.

Intuitively, one can think of coin initial independence as a compact way of representing general
independence (provided that this is well-behaved, in that it satisfies IRE and IEC), and *c* and *g*
as ways of moving between the two representations (Proposition 6.8). CS<sub>t</sub> and CL<sub>t</sub> work on the
general representation only, since they check independence between transitions that may be far
apart. The other two forms of CS/CL can instead work with both the representations, and they
are equivalent (Figure 12). Moreover, once we have LTSI with general independence we can work
immediately with CS<sub>t</sub> and CL<sub>t</sub>. On the other hand, when independence is coin initial, we need to
instantiate the notion of event, and understand whether events are causally dependent or coin initial
independent, before we can use the other two notions of CS/CL. The choice between CS<sub>&lt;</sub>/CL<sub>&lt;</sub>
and CS<sub>ci</sub>/CL<sub>ci</sub> depends on whether independence or ordering is more easily or naturally defined
on events.

In some process calculi and programming languages, as can be seen in the next section, inde-
pendence can be defined in terms of transition labels, which gives us structural axioms CLG and
LG. So, to show CS/CL we tend to show CLG (RCCS, CCSK, HOπ, Erlang) or we prove CIRE (Rπ,
reversible occurrence nets) and then use g. Alternatively, we show LG (πIH).

Note that whether or not CLG/LG can be applied to a reversible formalism may depend on the
level of abstraction adopted in the transition labels.

7 CASE STUDIES

We look at whether our axioms hold in various reversible formalisms. Given that we consider a
high number of formalisms, we do not provide full background on them, but refer for it to the
original papers. Also, we sometimes repeat similar observations for different formalisms, so to
make it possible to browse them out of order, to find information on a specific formalism of interest.
Remarkably, all the works below provide proofs of the Loop Lemma.

## 7.1 Reversible CCS (RCCS)

We consider here the semantics of RCCS in [13], and restrict the attention to coherent processes [13, Definition 2]. In RCCS, transitions $P \xrightarrow{\mu;\zeta} Q$ and $P \xrightarrow{\mu';\zeta'} Q'$ are concurrent if $\mu \cap \mu' = \emptyset$ [13, Definition 7]. This allows us to define coin initial independence as $t \prec u$ iff $t$ and $u$ are concurrent. We now argue that the resulting coin initial LTSI is pre-reversible and also satisfies CIRE. SP was shown in [13, Lemma 8]. BTI was shown in the proof of [13, Lemma 10]. WF is straightforward, noting that backward transitions decrease memory size. Hence, we obtain a very much simplified proof of CC. For PCI and CIRE we note that CLG holds and thus Proposition 6.10 applies. Therefore CS<sub>ci</sub> and CL<sub>ci</sub> hold. Using Proposition 6.8, we can get an LTSI with general independence satisfying IRE and IEC, and therefore CS<sub>t</sub> and CL<sub>t</sub>. This is the first time these causal properties have been proved for RCCS.

## 7.2 CCS with Communication Keys (CCSK)

The first notion of independence for CCSK [42] was given in [1]. It is based on the proved transition
system approach where transition labels contain information about derivation of transitions. This
on general independence, using mappings *c* and *g*. Thus, if we have a coin initial pre-reversible LTSI
*L* satisfying CIRE then CS<sub>ci</sub> and CL<sub>ci</sub> hold (using Theorems 5.20 and 5.29, respectively). The LTSI
g(*L*) is pre-reversible and satisfies IRE and IEC by Proposition 6.8. This will satisfy CS<sub>t</sub> and CL<sub>t</sub> as
a result of applying Theorems 5.5 and 5.6, respectively. It will also satisfy CS<sub>ci</sub> and CL<sub>ci</sub>. Conversely,
if we have a general pre-reversible LTSI *L'* satisfying IRE then CS<sub>t</sub> and CL<sub>t</sub> hold by Theorems 5.5
and 5.6, respectively. The LTSI c(*L'* ) is a coin initial pre-reversible LTSI satisfying CIRE. This will
satisfy CS<sub>ci</sub> and CL<sub>ci</sub>.

Intuitively, one can think of coin initial independence as a compact way of representing general
independence (provided that this is well-behaved, in that it satisfies IRE and IEC), and *c* and *g*
as ways of moving between the two representations (Proposition 6.8). CS<sub>t</sub> and CL<sub>t</sub> work on the
general representation only, since they check independence between transitions that may be far
apart. The other two forms of CS/CL can instead work with both the representations, and they
are equivalent (Figure 12). Moreover, once we have LTSI with general independence we can work
immediately with CS<sub>t</sub> and CL<sub>t</sub>. On the other hand, when independence is coin initial, we need to
instantiate the notion of event, and understand whether events are causally dependent or coin initial
independent, before we can use the other two notions of CS/CL. The choice between CS<sub>&lt;</sub>/CL<sub>&lt;</sub>
and CS<sub>ci</sub>/CL<sub>ci</sub> depends on whether independence or ordering is more easily or naturally defined
on events.

In some process calculi and programming languages, as can be seen in the next section, inde-
pendence can be defined in terms of transition labels, which gives us structural axioms CLG and
LG. So, to show CS/CL we tend to show CLG (RCCS, CCSK, HOπ, Erlang) or we prove CIRE (Rπ,
reversible occurrence nets) and then use g. Alternatively, we show LG (πIH).

Note that whether or not CLG/LG can be applied to a reversible formalism may depend on the
level of abstraction adopted in the transition labels.

7 CASE STUDIES

We look at whether our axioms hold in various reversible formalisms. Given that we consider a
high number of formalisms, we do not provide full background on them, but refer for it to the
original papers. Also, we sometimes repeat similar observations for different formalisms, so to
make it possible to browse them out of order, to find information on a specific formalism of interest.
Remarkably, all the works below provide proofs of the Loop Lemma.

## 7.1 Reversible CCS (RCCS)

We consider here the semantics of RCCS in [13], and restrict the attention to coherent processes [13, Definition 2]. In RCCS, transitions $P \xrightarrow{\mu;\zeta} Q$ and $P \xrightarrow{\mu';\zeta'} Q'$ are concurrent if $\mu \cap \mu' = \emptyset$ [13, Definition 7]. This allows us to define coin initial independence as $t \prec u$ iff $t$ and $u$ are concurrent. We now argue that the resulting coin initial LTSI is pre-reversible and also satisfies CIRE. SP was shown in [13, Lemma 8]. BTI was shown in the proof of [13, Lemma 10]. WF is straightforward, noting that backward transitions decrease memory size. Hence, we obtain a very much simplified proof of CC. For PCI and CIRE we note that CLG holds and thus Proposition 6.10 applies. Therefore CS<sub>ci</sub> and CL<sub>ci</sub> hold. Using Proposition 6.8, we can get an LTSI with general independence satisfying IRE and IEC, and therefore CS<sub>t</sub> and CL<sub>t</sub>. This is the first time these causal properties have been proved for RCCS.

## 7.2 CCS with Communication Keys (CCSK)

The first notion of independence for CCSK [42] was given in [1]. It is based on the proved transition
system approach where transition labels contain information about derivation of transitions. This
information can be used to work out whether transitions are in conflict, causally dependent, or con-
current. Two forms of independence are defined in [1]: general independence (called composable
concurrency) and coinitial independence (called coinitial concurrency). CC is then obtained using
our axiomatic approach (following [31], the conference version of the present paper) by showing
SP [1, Theorem 3], BTI [1, Lemma 6] and WF [1, Lemma 7].

Since coinitial independence is defined on labels, we can deduce that the LTSI is CLG. Hence, by Proposition 6.10, PCI and CIRE hold. This allows us to obtain $CS_{ci}$ and $CL_{ci}$. Using Proposition 6.8, we can get an LTSI with general independence which satisfies IRE and IEC, which gives us $CS_t$ and $CL_t$ as well. As for RCCS, this is the first time such causal properties have been proved for CCSK.

7.3 Higher-Order π-calculus (HOπ)

We consider here the uncontrolled reversible semantics for HOπ [27]. 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 [27, Section 3.1], where labels contain the memory created or consumed by the transition (they also contain a flag distinguishing backward from forward transitions, but this plays no role in the definition of the concurrency relation discussed below, hence we can safely drop it). The notion of independence would be given by the concurrency relation on coinitial transitions [27, Definition 9]. All pre-reversible LTSI axioms hold, as well as CIRE. Specifically, SP is proved in [27, Lemma 9]. BTI holds since distinct memories have disjoint sets of keys [27, Definition 3 and Lemma 3] and by the definition of concurrency [27, Definition 9]. WF holds as each backward step consumes a memory, which are a finite number to start with. Finally, PCI and CIRE hold since CLG holds for the LTSI with annotated labels and using our Proposition 6.10.

As a result we obtain a very much simplified proof of CC. Moreover, using PCI and CIRE, we get the $CS_{ci}$ and $CL_{ci}$ safety and liveness properties and, applying mapping $g$ from Section 6, we get a general pre-reversible LTSI satisfying IRE and IEC, so that $CS_t$ and $CL_t$ are satisfied. This is the first time that causal properties have been shown for HOπ.

7.4 Reversible π-calculus (Rπ)

We consider the (uncontrolled) reversible semantics for π-calculus defined in [12]. We restrict the attention to reachable processes. The semantics is an LTS semantics. Independence is given as concurrency which is defined for consecutive transitions [12, Definition 4.1]. CC holds [12, 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 directly handle Rπ using our axiomatic method.

We can however apply our theory to an LTSI obtained by considering labels up-to the equiva-
lence relation =λ [12, just before Lemma 4.3], which intuitively avoids to observe when a name is
being extruded. Notice that the Loop Lemma holds in this new LTSI as well. However, the concur-
rency relation is given on consecutive transitions, and the same for their SP. Nevertheless, we can
define independence as follows: t ιπ u iff t and u are coinital and t and u are concurrent. Notice
that since t and u are coinital then t and u are consecutive.

LEMMA 7.1. ι_π is symmetric.

PROOF. We have to show that *t* and *u* are concurrent iff *t* and *u* are concurrent. Since concurrency is defined as the complement of structural causality and contextual causality [12, Definition 4.1],
information can be used to work out whether transitions are in conflict, causally dependent, or con-
current. Two forms of independence are defined in [1]: general independence (called composable
concurrency) and coinitial independence (called coinitial concurrency). CC is then obtained using
our axiomatic approach (following [31], the conference version of the present paper) by showing
SP [1, Theorem 3], BTI [1, Lemma 6] and WF [1, Lemma 7].

Since coinitial independence is defined on labels, we can deduce that the LTSI is CLG. Hence, by Proposition 6.10, PCI and CIRE hold. This allows us to obtain $CS_{ci}$ and $CL_{ci}$. Using Proposition 6.8, we can get an LTSI with general independence which satisfies IRE and IEC, which gives us $CS_t$ and $CL_t$ as well. As for RCCS, this is the first time such causal properties have been proved for CCSK.

7.3 Higher-Order π-calculus (HOπ)

We consider here the uncontrolled reversible semantics for HOπ [27]. 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 [27, Section 3.1], where labels contain the memory created or consumed by the transition (they also contain a flag distinguishing backward from forward transitions, but this plays no role in the definition of the concurrency relation discussed below, hence we can safely drop it). The notion of independence would be given by the concurrency relation on coinitial transitions [27, Definition 9]. All pre-reversible LTSI axioms hold, as well as CIRE. Specifically, SP is proved in [27, Lemma 9]. BTI holds since distinct memories have disjoint sets of keys [27, Definition 3 and Lemma 3] and by the definition of concurrency [27, Definition 9]. WF holds as each backward step consumes a memory, which are a finite number to start with. Finally, PCI and CIRE hold since CLG holds for the LTSI with annotated labels and using our Proposition 6.10.

As a result we obtain a very much simplified proof of CC. Moreover, using PCI and CIRE, we get the $CS_{ci}$ and $CL_{ci}$ safety and liveness properties and, applying mapping $g$ from Section 6, we get a general pre-reversible LTSI satisfying IRE and IEC, so that $CS_t$ and $CL_t$ are satisfied. This is the first time that causal properties have been shown for HOπ.

7.4 Reversible π-calculus (Rπ)

We consider the (uncontrolled) reversible semantics for π-calculus defined in [12]. We restrict the attention to reachable processes. The semantics is an LTS semantics. Independence is given as concurrency which is defined for consecutive transitions [12, Definition 4.1]. CC holds [12, 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 directly handle Rπ using our axiomatic method.

We can however apply our theory to an LTSI obtained by considering labels up-to the equiva-
lence relation =λ [12, just before Lemma 4.3], which intuitively avoids to observe when a name is
being extruded. Notice that the Loop Lemma holds in this new LTSI as well. However, the concur-
rency relation is given on consecutive transitions, and the same for their SP. Nevertheless, we can
define independence as follows: t ιπ u iff t and u are coinital and t and u are concurrent. Notice
that since t and u are coinital then t and u are consecutive.

LEMMA 7.1. ι_π is symmetric.

PROOF. We have to show that *t* and *u* are concurrent iff *t* and *u* are concurrent. Since concurrency is defined as the complement of structural causality and contextual causality [12, Definition 4.1],
it is enough to prove that *t* and *u* are structural or contextual causal iff *t* and *u* are. For structural
causality, it follows from the definition [12, Definition 4.1]. For contextual causality, it follows
from [12, Proposition 4.2].
□

With this definition of independence SP holds [12, Lemma 4.3]. WF holds as well since each backward step consumes at least a memory. BTI has been proved as part of the proof of PL in [11, Lemma 14]. As a result we obtain a proof of CC much simpler than the one in [11, Theorem 11] (note that causal equivalence in [12, Definition 4.4] is formalised up-to =_λ as well).

Independence is coinitial by construction. We have to prove PCI and CIRE. Unfortunately, we
cannot exploit CLG, since it does not hold, as is clear from the definition of structural cause [12,
Definition 4.1], one of the ingredients of the concurrency relation. Thus we need to go for a direct
proof.

LEMMA 7.2. CIRE holds in the LTSI for Rπ.

PROOF. Concurrency is defined as the complement of structural causality and contextual causal-
ity [12, Definition 4.1]. Contextual causality is defined on labels [12, Proposition 4.2]. Structural
causality depends on whether the *i* components of the two labels occur in the same memory in a
specific relation [12, Definition 2.2]. However, one can notice that *i* can only occur in the memory
of one of the threads participating to the action (see [12, Table 1]), which are the same in transitions
in the same event. The thesis follows.
□

LEMMA 7.3. PCI holds in the LTSI for Rπ.

PROOF. Similar to the one above.

Using PCI and CIRE, we get the CS<sub>ci</sub> and CL<sub>ci</sub> safety and liveness properties. Applying mapping *g* from Section 6, we get a general pre-reversible LTSI satisfying IRE and IEC, so that CS<sub>i</sub> and CL<sub>i</sub> are satisfied. Notice that the notion of independence is not influenced by the abstraction on labels; hence the results can be reflected on the original LTSI of Rπ.

7.5 Reversible Internal π-calculus with Extrusion Histories (πIH)

The calculus πIH [19] is based on the work of Hildebrandt *et al.* [20], which uses extrusion histo-
ries and locations to define a stable non-interleaving early operational semantics for the π-calculus.
Locations and extrusion histories are used to define independence of actions. This notion of inde-
pendence differs from the ones considered in the other case studies in that it allows actions with
conflicting causes to be independent. Despite this major difference, it is shown in [19] that nearly
all our (non-structural) axioms are satisfied (SP, BTI, WF, PCI and IRE); the only exception is that
IEC fails, because a process can have independent transitions with conflicting causes without hav-
ing a single state where equivalent transitions can both be performed. We use IEC to show RPI
(Proposition 5.12). However RPI is shown in [19] for πIH without the need for IEC, using the fact
that independence is defined on transition labels. In fact, LG holds for πIH, from which we can
deduce PCI, IRE and RPI by Proposition 6.12. It follows that all the properties listed in Table 1 hold
for πIH, with the exception of IEC, IC and CLG.

7.6 Reversible Erlang

We consider the uncontrolled reversible (reduction) semantics for Erlang in [30]. We restrict our attention to reachable processes. In order to have more informative labels we can consider the annotations defined in [30, Section 4.1]. We can then define coinitial transitions to be independent iff they are concurrent [30, Definition 12].
it is enough to prove that *t* and *u* are structural or contextual causal iff *t* and *u* are. For structural
causality, it follows from the definition [12, Definition 4.1]. For contextual causality, it follows
from [12, Proposition 4.2].
□

With this definition of independence SP holds [12, Lemma 4.3]. WF holds as well since each backward step consumes at least a memory. BTI has been proved as part of the proof of PL in [11, Lemma 14]. As a result we obtain a proof of CC much simpler than the one in [11, Theorem 11] (note that causal equivalence in [12, Definition 4.4] is formalised up-to =_λ as well).

Independence is coinital by construction. We have to prove PCI and CIRE. Unfortunately, we
cannot exploit CLG, since it does not hold, as is clear from the definition of structural cause [12,
Definition 4.1], one of the ingredients of the concurrency relation. Thus we need to go for a direct
proof.

LEMMA 7.2. CIRE holds in the LTSI for Rπ.

PROOF. Concurrency is defined as the complement of structural causality and contextual causal-
ity [12, Definition 4.1]. Contextual causality is defined on labels [12, Proposition 4.2]. Structural
causality depends on whether the *i* components of the two labels occur in the same memory in a
specific relation [12, Definition 2.2]. However, one can notice that *i* can only occur in the memory
of one of the threads participating to the action (see [12, Table 1]), which are the same in transitions
in the same event. The thesis follows.
□

LEMMA 7.3. PCI holds in the LTSI for Rπ.

PROOF. Similar to the one above.

Using PCI and CIRE, we get the CS<sub>ci</sub> and CL<sub>ci</sub> safety and liveness properties. Applying mapping *g* from Section 6, we get a general pre-reversible LTSI satisfying IRE and IEC, so that CS<sub>t</sub> and CL<sub>t</sub> are satisfied. Notice that the notion of independence is not influenced by the abstraction on labels; hence the results can be reflected on the original LTSI of Rπ.

7.5 Reversible Internal π-calculus with Extrusion Histories (πIH)

The calculus πIH [19] is based on the work of Hildebrandt *et al.* [20], which uses extrusion histo-
ries and locations to define a stable non-interleaving early operational semantics for the π-calculus.
Locations and extrusion histories are used to define independence of actions. This notion of inde-
pendence differs from the ones considered in the other case studies in that it allows actions with
conflicting causes to be independent. Despite this major difference, it is shown in [19] that nearly
all our (non-structural) axioms are satisfied (SP, BTI, WF, PCI and IRE); the only exception is that
IEC fails, because a process can have independent transitions with conflicting causes without hav-
ing a single state where equivalent transitions can both be performed. We use IEC to show RPI
(Proposition 5.12). However RPI is shown in [19] for πIH without the need for IEC, using the fact
that independence is defined on transition labels. In fact, LG holds for πIH, from which we can
deduce PCI, IRE and RPI by Proposition 6.12. It follows that all the properties listed in Table 1 hold
for πIH, with the exception of IEC, IC and CLG.

7.6 Reversible Erlang

We consider the uncontrolled reversible (reduction) semantics for Erlang in [30]. We restrict our attention to reachable processes. In order to have more informative labels we can consider the annotations defined in [30, Section 4.1]. We can then define coinital transitions to be independent iff they are concurrent [30, Definition 12].
We next discuss the validity of our axioms in reversible Erlang. SP is proved in [30, Lemma 13] and BTI is trivial from the definition of concurrency [30, Definition 12]. WF holds since the pair of non-negative integers (total number of elements in history, total number of messages queued) ordered under lexicographic order decreases at each backward step. Intuitively, each step but the ones derived using the rule for reverse sched (see [30, Figure 11]) consumes an item of memory, and each step derived using rule reverse sched removes a message from a process queue. Finally, PCI and CIRE hold since CLG holds for the LTSI with annotated labels, and by Proposition 6.10.

Since this setting is very similar to the one of $HO_\pi$ (both calculi have a reduction semantics and a coin initial notion of independence defined on enriched labels), we get the same results as for $HO_\pi$ (described in Section 7.3), including CC, and causal safety and liveness.

## 7.7 Reversible occurrence nets

We consider occurrence nets, which are the result of unfolding Place/Transition nets, and their reversible versions [35–37]. Reversible occurrence nets are occurrence nets (1-safe and with no backward conflicts) extended with a backward (reverse in the terminology of [37]) transition name $\leftarrow t$ for each forward transition name $t$. We write $t, u$ (note the italic font) for forward or backward transition names, and $\leftarrow t, \leftarrow u$ for their backward or forward duals. We use “transition name” to mean forward or backward transition name. They give rise to an LTS where states are pairs $(N, m)$ with $N$ a net and $m$ a marking. A computation that represents firing a (forward or backward) transition name $t$ in $(N, m)$ and resulting in $(N, m')$ is given by a firing relation $(N, m) \xrightarrow{t} (N, m')^3$. Independence is the concurrency relation co which is defined between arbitrary firings as follows: two firings are concurrent if their transition names are concurrent, that is when they are not in conflict and do not cause each other [36, 37, Section 3]. The last two notions are defined in terms of conditions on pre- and postset relations on transition names. Hence, we get an LTSI with general independence. Note that transition names are unique.

Properties SP and PL are shown as [37, Lemma 4.3] and [37, Lemma 4.4], respectively. Then CC is proved (over several pages) as [37, Theorem 4.6] using SP and PL. The causal safety and causal liveness properties are not considered in [36, 37]. However, a form of such properties is discussed in [35] in the setting of reversible prime event structures; we discuss this point in Section 8.

We can obtain causal safety and causal liveness properties, as well as PL and CC, for reversible occurrence nets using our axiomatic approach. The following lemma will be helpful.

**LEMMA 7.4.** Let $t$ and $u$ be enabled and coinital (forward or backward) transition names. Then $t$ does not cause $u$. If additionally $t$ and $u$ are backward, then they are not in conflict.

**PROOF.** Assume for contradiction that $t$ causes $u$. So there is a place, say $a$, in the preset of $u$ such that $t$ causes $a$. Since $u$ is enabled there is a token in $a$. Also, since $t$ is enabled, after it fires a second token will arrive in $a$, thus contradicting the 1-safe property of occurrence nets.

Let $t$ and $u$ be $\leftarrow t$ and $\leftarrow u$ respectively. Assume for contradiction that they are in conflict. This means that they share a place, say $a$, in their presets. Hence, $t$ and $u$ share $a$ in their postsets, which contradicts the no backwards conflict property of occurrence nets. $\square$

We can now combine Lemma 7.4 with the conditions in [37, Lemma 3.3] of when enabled and coinital $t$ and $u$ are concurrent.

<footnote n="3">³We use “transition names” in this subsection to name the members of the set of transitions which, together with the set of places, are part of the definition of Place/Transition nets or occurrence nets. This distinguishes them from our transitions, which are called firings in Place/Transition nets and occurrence nets.</footnote>
We next discuss the validity of our axioms in reversible Erlang. SP is proved in [30, Lemma 13] and BTI is trivial from the definition of concurrency [30, Definition 12]. WF holds since the pair of non-negative integers (total number of elements in history, total number of messages queued) ordered under lexicographic order decreases at each backward step. Intuitively, each step but the ones derived using the rule for reverse sched (see [30, Figure 11]) consumes an item of memory, and each step derived using rule reverse sched removes a message from a process queue. Finally, PCI and CIRE hold since CLG holds for the LTSI with annotated labels, and by Proposition 6.10.

Since this setting is very similar to the one of $HO\pi$ (both calculi have a reduction semantics and a coinitial notion of independence defined on enriched labels), we get the same results as for $HO\pi$ (described in Section 7.3), including CC, and causal safety and liveness.

## 7.7 Reversible occurrence nets

We consider occurrence nets, which are the result of unfolding Place/Transition nets, and their reversible versions [35–37]. Reversible occurrence nets are occurrence nets (1-safe and with no backward conflicts) extended with a backward (reverse in the terminology of [37]) transition name $\leftarrow t$ for each forward transition name $t$. We write $t, u$ (note the italic font) for forward or backward transition names, and $\leftarrow t, \leftarrow u$ for their backward or forward duals. We use “transition name” to mean forward or backward transition name. They give rise to an LTS where states are pairs $(N, m)$ with $N$ a net and $m$ a marking. A computation that represents firing a (forward or backward) transition name $t$ in $(N, m)$ and resulting in $(N, m')$ is given by a firing relation $(N, m) \xrightarrow{t} (N, m')^3$. Independence is the concurrency relation co which is defined between arbitrary firings as follows: two firings are concurrent if their transition names are concurrent, that is when they are not in conflict and do not cause each other [36, 37, Section 3]. The last two notions are defined in terms of conditions on pre- and postset relations on transition names. Hence, we get an LTSI with general independence. Note that transition names are unique.

Properties SP and PL are shown as [37, Lemma 4.3] and [37, Lemma 4.4], respectively. Then CC is proved (over several pages) as [37, Theorem 4.6] using SP and PL. The causal safety and causal liveness properties are not considered in [36, 37]. However, a form of such properties is discussed in [35] in the setting of reversible prime event structures; we discuss this point in Section 8.

We can obtain causal safety and causal liveness properties, as well as PL and CC, for reversible occurrence nets using our axiomatic approach. The following lemma will be helpful.

**LEMMA 7.4.** Let $t$ and $u$ be enabled and coinital (forward or backward) transition names. Then $t$ does not cause $u$. If additionally $t$ and $u$ are backward, then they are not in conflict.

**PROOF.** Assume for contradiction that $t$ causes $u$. So there is a place, say $a$, in the preset of $u$ such that $t$ causes $a$. Since $u$ is enabled there is a token in $a$. Also, since $t$ is enabled, after it fires a second token will arrive in $a$, thus contradicting the 1-safe property of occurrence nets.

Let $t$ and $u$ be $\leftarrow t$ and $\leftarrow u$ respectively. Assume for contradiction that they are in conflict. This means that they share a place, say $a$, in their presets. Hence, $t$ and $u$ share $a$ in their postsets, which contradicts the no backwards conflict property of occurrence nets. $\square$

We can now combine Lemma 7.4 with the conditions in [37, Lemma 3.3] of when enabled and coinital $t$ and $u$ are concurrent.

<footnote n="3">³We use “transition names” in this subsection to name the members of the set of transitions which, together with the set of places, are part of the definition of Place/Transition nets or occurrence nets. This distinguishes them from our transitions, which are called firings in Place/Transition nets and occurrence nets.</footnote>
LEMMA 7.5. Let $t$ and $u$ be enabled and coinitial (forward or backward) transition names. Then $t$ co $u$ iff $t$ and $u$ are backward or they are not in an immediate conflict.

As a consequence, BTI holds.

LEMMA 7.6. BTI holds in the LTSI for reversible occurrence nets.

WF holds because there are no forward cycles of firings in occurrence nets, hence no infinite reverse paths. This gives us PL and CC. Next, we prove PCI.

LEMMA 7.7. PCI holds in the LTSI for reversible occurrence nets.

PROOF. Consider enabled coinitial firings $\phi_1, \phi_2$ with transition names $t, u$ respectively, and assume $\phi_1$ co $\phi_2$. Hence $t$ co $u$. We get a commuting diamond by SP, where the opposite sides have the same transition names. Since $t$ co $u$, we have $\overleftarrow{t}$ co $u$ by [37, Lemma 3.4], so PCI holds. $\square$

This gives us a pre-reversible LTSI, and thus $CS_{\mathrm{ci}}$ and $CS_{<}$ hold.

Given a pair of enabled coinitial concurrent transition names we get a commuting diamond by SP, and the pairs of coinitial transition names in all corners of the diamond are concurrent. Events can then be defined on firings in such diamonds as in Definition 4.1, and we can show IRE.

LEMMA 7.8. IRE holds in the LTSI for reversible occurrence nets.

PROOF. Let $\phi_1, \phi_2$ be firings with $t, u$ respectively, and let $\phi_1$ co $\phi_2$. This means that $t$ co $u$. Since any $\phi'_1$ equivalent to $\phi$ has the same transition name $t$, $t$ co $u$ gives us $\phi'_1$ co $\phi_2$. $\square$

Since IRE implies CIRE we obtain $CL_{\mathrm{ci}}$ (or $CL_{<}$). We also have $CS_t$ and $CL_t$ as IRE holds.

An alternative proof strategy would be to show CLG first, but we believe this approach leads to more complex technicalities, and we would still need to prove IRE, hence we have preferred the approach above.

## 7.8 Reversible sequential systems

In sequential systems there is no concurrency. Hence, in this section, we represent them as LTSIs where the independence relation, modelling concurrency, is empty. This is for instance the case for Janus programs [50] or CCSK processes without parallel composition such as the ones studied in [7]. In this setting, SP, PCI, IRE and IEC hold trivially. Moreover, BTI is equivalent to backward determinism, which is the main condition required for reversibility in a sequential setting (see, e.g., Janus [50]).

*Definition 7.9 (Backward determinism).* An LTSI is backward deterministic iff $P \stackrel{a}{\rightleftharpoons} Q$ and $P' \stackrel{a'}{\rightleftharpoons} Q$ imply $P = P'$ and $a = a'$.

PROPOSITION 7.10. A sequential system satisfies BTI iff it is backward deterministic.

PROOF. For the left to right implication, assume towards a contradiction that the system satisfies BTI but it is not backward deterministic. Then there are $P \stackrel{a}{\rightleftharpoons} Q$ and $P' \stackrel{a'}{\rightleftharpoons} Q$ with $P \neq P'$ or $a \neq a'$. By the Loop Lemma we have the reverse transitions, which are coinitial and backwards, hence by BTI they need to be independent, what is a contradiction since the independence relation is empty.

For the right to left implication, take two backward coinitial transitions $t, t'$. By applying the Loop Lemma there exist $\underline{t}, \underline{t}'$. One can notice that $\underline{t}, \underline{t}'$ satisfy the hypothesis of backward determinism. Hence, $\underline{t} = \underline{t}'$ and $t = t'$. Hence BTI trivially holds. $\square$
**LEMMA 7.5.** Let $t$ and $u$ be enabled and coinitial (forward or backward) transition names. Then $t$ co $u$ iff $t$ and $u$ are backward or they are not in an immediate conflict.

As a consequence, BTI holds.

**LEMMA 7.6.** *BTI holds in the LTSI for reversible occurrence nets.*

WF holds because there are no forward cycles of firings in occurrence nets, hence no infinite reverse paths. This gives us PL and CC. Next, we prove PCI.

**LEMMA 7.7.** *PCI holds in the LTSI for reversible occurrence nets.*

*PROOF.* Consider enabled coinitial firings $\phi_1, \phi_2$ with transition names $t, u$ respectively, and assume $\phi_1$ co $\phi_2$. Hence $t$ co $u$. We get a commuting diamond by SP, where the opposite sides have the same transition names. Since $t$ co $u$, we have $\overleftarrow{t}$ co $u$ by [37, Lemma 3.4], so PCI holds. $\square$

This gives us a pre-reversible LTSI, and thus $CS_{\mathrm{ci}}$ and $CS_{<}$ hold.

Given a pair of enabled coinitial concurrent transition names we get a commuting diamond by SP, and the pairs of coinitial transition names in all corners of the diamond are concurrent. Events can then be defined on firings in such diamonds as in Definition 4.1, and we can show IRE.

**LEMMA 7.8.** *IRE holds in the LTSI for reversible occurrence nets.*

*PROOF.* Let $\phi_1, \phi_2$ be firings with $t, u$ respectively, and let $\phi_1$ co $\phi_2$. This means that $t$ co $u$. Since any $\phi'_1$ equivalent to $\phi$ has the same transition name $t$, $t$ co $u$ gives us $\phi'_1$ co $\phi_2$. $\square$

Since IRE implies CIRE we obtain $CL_{\mathrm{ci}}$ (or $CL_{<}$). We also have $CS_t$ and $CL_t$ as IRE holds.

An alternative proof strategy would be to show CLG first, but we believe this approach leads to more complex technicalities, and we would still need to prove IRE, hence we have preferred the approach above.

## 7.8 Reversible sequential systems

In sequential systems there is no concurrency. Hence, in this section, we represent them as LTSIs where the independence relation, modelling concurrency, is empty. This is for instance the case for Janus programs [50] or CCSK processes without parallel composition such as the ones studied in [7]. In this setting, SP, PCI, IRE and IEC hold trivially. Moreover, BTI is equivalent to backward determinism, which is the main condition required for reversibility in a sequential setting (see, e.g., Janus [50]).

*Definition 7.9 (Backward determinism).* An LTSI is backward deterministic iff $P \stackrel{a}{\rightleftharpoons} Q$ and $P' \stackrel{a'}{\rightleftharpoons} Q$ imply $P = P'$ and $a = a'$.

**PROPOSITION 7.10.** *A sequential system satisfies BTI iff it is backward deterministic.*

*PROOF.* For the left to right implication, assume towards a contradiction that the system satisfies BTI but it is not backward deterministic. Then there are $P \stackrel{a}{\rightleftharpoons} Q$ and $P' \stackrel{a'}{\rightleftharpoons} Q$ with $P \neq P'$ or $a \neq a'$. By the Loop Lemma we have the reverse transitions, which are coinitial and backwards, hence by BTI they need to be independent, what is a contradiction since the independence relation is empty.

For the right to left implication, take two backward coinitial transitions $t, t'$. By applying the Loop Lemma there exist $\underline{t}, \underline{t}'$. One can notice that $\underline{t}, \underline{t}'$ satisfy the hypothesis of backward determinism. Hence, $\underline{t} = \underline{t}'$ and $t = t'$. Hence BTI trivially holds. $\square$
WF does not hold in general and needs to be assumed.

If we assume WF then all our results hold, but they all become trivial or almost trivial. E.g., all events are singletons. Also, all the notions of causal liveness coincide, and they state that the last transition can always be undone, but this is just one direction of the Loop Lemma. Similarly, all the notions of causal safety do coincide, and they require that only the last transition can be undone.

## 8 RELATED WORK

Causal Consistency (CC), Parabolic Lemma (PL) and informal versions of Causal Safety and Liveness (CS, CL), the main general properties of reversible computation considered in this paper, were proposed by Danos and Krivine [13]. Since then, many reversible process calculi or formalisms have been developed as we have described in the Introduction. Most of them use memories to save information lost when computing forwards, which can be easily retrieved when computing in reverse. Concurrency relation between coinitial transitions is typically defined in terms of structural conditions on the memories of the transitions. In order to show that reversibility is well-behaved, PL and then CC is proved. In contrast, CS and CL (in any of the variants we considered), or properties close to them, have not been widely considered.

Information needed for undoing of computation in a process calculus can be saved differently. An alternative method was proposed for reversing a process calculus given by a general format of SOS rules in [40, 42]. When applied to CCS it produces CCSK, where reversible processes maintain their syntax as they compute, and executed actions are marked with communication keys. When computation reverses, keys are removed, thus returning processes to their original form. This approach has a drawback in that it is not easy to define a concurrency relation purely on transition labels. As a result, proving CC in the traditional way is not straightforward. Hence, slightly different properties are proved to show that the resulting reversible calculi are well-behaved. The main property is Reverse Diamond (RD): if $Q \xrightarrow{a} P$, $R \xrightarrow{b} P$ and $Q \neq R$, then there is $S$ such that $S \xrightarrow{a} R$ and $S \xrightarrow{b} Q$. In our setting, RD can be proved from the Loop Lemma, BTI and SP. It is worth noting that PL can be shown for CCSK mainly using RD [42, Lemma 5.9]. Moreover, a form of CC for forward computation is shown [42, Proposition 5.15]: two forward computations from the same start to the same endpoint are homotopic [48], meaning that one computation can be transformed into the other by swapping adjacent transitions in commuting diamonds. In effect, concurrency is represented as commuting diamonds in the LTSs for reversible calculi obtained by applying the method in [40, 42].

A more abstract approach to defining desirable properties for reversibility was taken in [41]. General LTSs were considered instead of LTSs for specific reversible calculi, and two sets of axioms were proposed. The first set inherited RD and Forward Diamond (FD) from [40, 42], and also included WF, UT and Event Determinism (ED) [47, 48]: if $P \xrightarrow{a} Q$ and $P \xrightarrow{a} R$, and $(P, a, Q) \sim (P, a, R)$, then $Q = R$. ED is not a consequence of our basic axioms. Consider the LTS [41, Fig. 1], and add coinitial independence using BTI and PCI. The resulting LTSI is pre-reversible and satisfies CLG, yet it fails ED. LTSs satisfying the five axioms above are called *prime LTSs* and are shown to correspond to prime event structures. Several interesting properties were proved for prime LTSs, including RED (event determinism for backward transitions, which follows from BLD in our setting) and NRE which we also consider here. The second set of axioms aimed at providing local versions of FD, ED and RED.

As we have mentioned in the Introduction, a combined causal safety and liveness property has been formulated in [30, Corollary 22]. A form of causal safety and liveness properties has been defined in the setting of reversible event structures in [43, 44]. A reversible event structure is called *cause-respecting* if an event cannot be reversed until all events it has caused have also
WF does not hold in general and needs to be assumed.

If we assume WF then all our results hold, but they all become trivial or almost trivial. E.g., all events are singletons. Also, all the notions of causal liveness coincide, and they state that the last transition can always be undone, but this is just one direction of the Loop Lemma. Similarly, all the notions of causal safety do coincide, and they require that only the last transition can be undone.

# 8 RELATED WORK

Causal Consistency (CC), Parabolic Lemma (PL) and informal versions of Causal Safety and Liveness (CS, CL), the main general properties of reversible computation considered in this paper, were proposed by Danos and Krivine [13]. Since then, many reversible process calculi or formalisms have been developed as we have described in the Introduction. Most of them use memories to save information lost when computing forwards, which can be easily retrieved when computing in reverse. Concurrency relation between coinitial transitions is typically defined in terms of structural conditions on the memories of the transitions. In order to show that reversibility is well-behaved, PL and then CC is proved. In contrast, CS and CL (in any of the variants we considered), or properties close to them, have not been widely considered.

Information needed for undoing of computation in a process calculus can be saved differently. An alternative method was proposed for reversing a process calculus given by a general format of SOS rules in [40, 42]. When applied to CCS it produces CCSK, where reversible processes maintain their syntax as they compute, and executed actions are marked with communication keys. When computation reverses, keys are removed, thus returning processes to their original form. This approach has a drawback in that it is not easy to define a concurrency relation purely on transition labels. As a result, proving CC in the traditional way is not straightforward. Hence, slightly different properties are proved to show that the resulting reversible calculi are well-behaved. The main property is Reverse Diamond (RD): if $Q \stackrel{a}{\rightarrow} P$, $R \stackrel{b}{\rightarrow} P$ and $Q \neq R$, then there is $S$ such that $S \stackrel{a}{\rightarrow} R$ and $S \stackrel{b}{\rightarrow} Q$. In our setting, RD can be proved from the Loop Lemma, BTI and SP. It is worth noting that PL can be shown for CCSK mainly using RD [42, Lemma 5.9]. Moreover, a form of CC for forward computation is shown [42, Proposition 5.15]: two forward computations from the same start to the same endpoint are homotopic [48], meaning that one computation can be transformed into the other by swapping adjacent transitions in commuting diamonds. In effect, concurrency is represented as commuting diamonds in the LTSs for reversible calculi obtained by applying the method in [40, 42].

A more abstract approach to defining desirable properties for reversibility was taken in [41]. General LTSs were considered instead of LTSs for specific reversible calculi, and two sets of axioms were proposed. The first set inherited RD and Forward Diamond (FD) from [40, 42], and also included WF, UT and Event Determinism (ED) [47, 48]: if $P \stackrel{a}{\rightarrow} Q$ and $P \stackrel{a}{\rightarrow} R$, and $(P, a, Q) \sim (P, a, R)$, then $Q = R$. ED is not a consequence of our basic axioms. Consider the LTS [41, Fig. 1], and add coinitial independence using BTI and PCI. The resulting LTSI is pre-reversible and satisfies CLG, yet it fails ED. LTSs satisfying the five axioms above are called *prime LTSs* and are shown to correspond to prime event structures. Several interesting properties were proved for prime LTSs, including RED (event determinism for backward transitions, which follows from BLD in our setting) and NRE which we also consider here. The second set of axioms aimed at providing local versions of FD, ED and RED.

As we have mentioned in the Introduction, a combined causal safety and liveness property has been formulated in [30, Corollary 22]. A form of causal safety and liveness properties has been defined in the setting of reversible event structures in [43, 44]. A reversible event structure is called *cause-respecting* if an event cannot be reversed until all events it has caused have also
been reversed, and it is *causal* if it is cause-respecting and a reversible event can be reversed if all events it has caused have been reversed [44, Definition 3.34]. Causal reversible prime event structures are considered in [35] as well, where it is shown that they correspond precisely to reversible occurrence nets.

Another related work is [15], 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 [5], 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. An approach similar to that in [5, 42) is taken in [24], which focuses on systems modelled using reduction semantics. In order to prove properties of the reversible systems they build they use our theory (taken from the conference version of the present paper [31]), hence this can be taken as an additional case study for our results. Finally, [16] presents a number of properties such as, for example, backward confluence, which arise in the context of reversing of multiple transitions at the same time (called a step) in Place/Transition nets.

# 9 CONCLUSION AND FUTURE WORK

The literature on causal-consistent reversibility (see, for example the early survey [28]) has a number of proofs of results such as PL and CC, all of which are instantiated to a specific calculus, language or formalism. We have taken here a complementary and more general 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. Among the properties, we discussed in detail the formalisation of Causal Safety and Causal Liveness, which were mostly informally discussed in the literature.

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. Indeed, proving the axioms is usually much simpler than proving the properties directly. This is particularly relevant since causal-consistent reversibility is getting applied to more and more complex languages, such as Erlang [30], 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 mechanisms to control reversibility [26], such as a rollback operator [25] or irreversible actions [14]. For the latter we could take inspiration from the above-mentioned [15].

# ACKNOWLEDGMENTS

This work has been partially supported by COST Action IC1405 on Reversible Computation - Extending Horizons of Computing. The first author has also been partially supported by the French ANR project DCore ANR-18-CE25-0007 and by the INdAM-GNCS project CUP_E55F22000270001 *Proprietà Qualitative e Quantitative di Sistemi Reversibili*. The third author has been partially supported by the JSPS Invitation Fellowship S21050.

# REFERENCES

[1] Clément Aubert. 2022. Concurrency in reversible concurrent calculi. In *Proceedings of RC 2022 (LNCS, Vol. 13354)*, Claudio Antares Mezzina and Krzysztof Podlaski (Eds.). Springer, 146–163. https://doi.org/10.1007/978-3-031-09005-9_10

[2] Clément Aubert and Doriana Medic. 2021. Explicit identifiers and contexts in reversible concurrent calculus. In *Proceedings of RC 2021 (LNCS, Vol. 12805)*, Shigeru Yamashita and Tetsuo Yokoyama (Eds.). Springer, 144–162. https://doi.org/10.1007/978-3-030-79837-6_9
been reversed, and it is *causal* if it is cause-respecting and a reversible event can be reversed if all events it has caused have been reversed [44, Definition 3.34]. Causal reversible prime event structures are considered in [35] as well, where it is shown that they correspond precisely to reversible occurrence nets.

Another related work is [15], 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 [5], 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. An approach similar to that in [5, 42) is taken in [24], which focuses on systems modelled using reduction semantics. In order to prove properties of the reversible systems they build they use our theory (taken from the conference version of the present paper [31]), hence this can be taken as an additional case study for our results. Finally, [16] presents a number of properties such as, for example, backward confluence, which arise in the context of reversing of multiple transitions at the same time (called a step) in Place/Transition nets.

# 9 CONCLUSION AND FUTURE WORK

The literature on causal-consistent reversibility (see, for example the early survey [28]) has a number of proofs of results such as PL and CC, all of which are instantiated to a specific calculus, language or formalism. We have taken here a complementary and more general 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. Among the properties, we discussed in detail the formalisation of Causal Safety and Causal Liveness, which were mostly informally discussed in the literature.

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. Indeed, proving the axioms is usually much simpler than proving the properties directly. This is particularly relevant since causal-consistent reversibility is getting applied to more and more complex languages, such as Erlang [30], 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 mechanisms to control reversibility [26], such as a rollback operator [25] or irreversible actions [14]. For the latter we could take inspiration from the above-mentioned [15].

# ACKNOWLEDGMENTS

This work has been partially supported by COST Action IC1405 on Reversible Computation - Extending Horizons of Computing. The first author has also been partially supported by the French ANR project DCore ANR-18-CE25-0007 and by the INdAM-GNCS project CUP_E55F22000270001 *Proprietà Qualitative e Quantitative di Sistemi Reversibili*. The third author has been partially supported by the JSPS Invitation Fellowship S21050.

# REFERENCES

[1] Clément Aubert. 2022. Concurrency in reversible concurrent calculi. In Proceedings of RC 2022 (LNCS, Vol. 13354), Claudio Antares Mezzina and Krzysztof Podlaski (Eds.). Springer, 146–163. https://doi.org/10.1007/978-3-031-09005-9_10

[2] Clément Aubert and Doriana Medic. 2021. Explicit identifiers and contexts in reversible concurrent calculus. In Proceedings of RC 2021 (LNCS, Vol. 12805), Shigeru Yamashita and Tetsuo Yokoyama (Eds.). Springer, 144–162. https://doi.org/10.1007/978-3-030-79837-6_9
[3] Attila Bagossy and György Vaszil. 2022. Controlled reversibility in communicating reaction systems. *Theoretical Computer Science* 926 (2022), 3–20. https://doi.org/10.1016/j.tcs.2022.05.030

[4] Marek A. Bednarczyk. 1991. *Hereditary history preserving bisimulations or what is the power of the future perfect in program logics*. Technical Report ICS PAS. Polish Academy of Sciences.

[5] Alexis Bernadet and Ivan Lanese. 2016. A modular formalization of reversibility for concurrent models and languages. In *Proceedings of ICE 2016 (EPTCS, Vol. 223)*, Massimo Bartoletti, Ludovic Henrio, Sophia Knight, and Hugo Torres Vieira (Eds.). 98–112. https://doi.org/10.4204/EPTCS.223.7

[6] Marco Bernardo and Claudio Antares Mezzina. 2023. Bridging causal reversibility and time reversibility: A stochastic process algebraic approach. *Logical Methods in Computer Science* 19, 2 (2023). https://doi.org/10.46298/LMCS-19(2:6)2023

[7] Marco Bernardo and Sabina Rossi. 2023. Reverse bisimilarity vs. forward bisimilarity. In *Proceedings of FoSSaCS 2023 (LNCS, Vol. 13992)*, Orna Kupferman and Pawel Sobocinski (Eds.). Springer, 265–284. https://doi.org/10.1007/978-3-031-30829-1_13

[8] Laura Bocchi, Ivan Lanese, Claudio Antares Mezzina, and Shoji Yuen. 2022. The reversible temporal process language. In *Proceedings of FORTE 2022 (LNCS, Vol. 13273)*, Mohammad Reza Mousavi and Anna Philippou (Eds.). Springer, 31–49. https://doi.org/10.1007/978-3-031-08679-3_3

[9] Luca Cardelli and Cosimo Laneve. 2011. Reversible structures. In *Proceedings of CMSB 2011*. ACM, 131–140. https://doi.org/10.1145/2037509.2037529

[10] Christopher D. Carothers, Kalyan S. Perumalla, and Richard Fujimoto. 1999. Efficient optimistic parallel simulations using reverse computation. *ACM Transactions on Modeling and Computer Simulation* 9, 3 (1999), 224–253. https://doi.org/10.1145/347823.347828

[11] Ioana Cristescu. 2015. *Operational and denotational semantics for the reversible π-calculus*. Ph. D. Dissertation. Paris Centre Mathematical sciences Doctoral School. https://scholar.harvard.edu/files/cristescu/files/these.pdf.

[12] Ioana Cristescu, Jean Krivine, and Daniele Varacca. 2013. A compositional semantics for the reversible π-calculus. In *Proceedings of LICS 2013*. IEEE Computer Society, 388–397. https://doi.org/10.1109/LICS.2013.45

[13] Vincent Danos and Jean Krivine. 2004. Reversible communicating systems. In *Proceedings of CONCUR 2004 (LNCS, Vol. 3170)*, Philippa Gardner and Nobuko Yoshida (Eds.). Springer, 292–307. https://doi.org/10.1007/978-3-540-28644-8_19

[14] Vincent Danos and Jean Krivine. 2005. Transactions in RCCS. In *Proceedings of CONCUR 2005 (LNCS, Vol. 3653)*, Martín Abadi and Luca de Alfaro (Eds.). Springer, 398–412. https://doi.org/10.1007/11539452_31

[15] Vincent Danos, Jean Krivine, and Paweł Sobociński. 2006. General reversibility. In *Proceedings of EXPRESS 2007 (ENTCS, Vol. 175(3))*, Roberto M. Amadio and Iain Phillips (Eds.). Elsevier, 75–86. https://doi.org/10.1016/j.entcs.2006.07.036

[16] David de Frutos Escrig, Maciej Koutny, and Łukasz Mikulski. 2019. Reversing steps in Petri nets. In *Proceedings of Petri Nets 2019 (LNCS, Vol. 11522)*, Susanna Donelli and Stefan Haar (Eds.). Springer, 171–191. https://doi.org/10.1007/978-3-030-21571-2_11

[17] Elena Giachino, Ivan Lanese, and Claudio Antares Mezzina. 2014. Causal-consistent reversible debugging. In *Proceedings of FASE 2014 (LNCS, Vol. 8411)*, Stefania Gnesi and Arend Rensink (Eds.). Springer, 370–384. https://doi.org/10.1007/978-3-642-54804-8_26

[18] Elena Giachino, Ivan Lanese, Claudio Antares Mezzina, and Francesco Tiezzi. 2017. Causal-consistent rollback in a tuple-based language. *Journal of Logical and Algebraic Methods in Programming* 88 (2017), 99–120. https://doi.org/10.1016/j.jlamp.2016.09.003

[19] Eva Graversen, Iain Phillips, and Nobuko Yoshida. 2022. Event structures for the reversible early internal π-calculus. *Journal of Logical and Algebraic Methods in Programming* 124 (2022), 100720. https://doi.org/10.1016/j.jlamp.2021.100720

[20] Thomas Troels Hildebrandt, Christian Johansen, and Håkon Normann. 2019. A stable non-interleaving early operational semantics for the pi-calculus. *Journal of Logical and Algebraic Methods in Programming* 104 (2019), 227–253. https://doi.org/10.1016/j.jlamp.2019.02.006

[21] Stefan Kuhn and Irek Ulidowski. 2018. Local reversibility in a Calculus of Covalent Bonding. *Science of Computer Programming* 151 (2018), 18–47. https://doi.org/10.1016/j.scico.2017.09.008

[22] Pietro Lami, Ivan Lanese, Jean-Bernard Stefani, Claudio Sacerdoti Coen, and Giovanni Fabbretti. 2022. Reversibility in Erlang: imperative constructs. In *Proceedings of RC 2022 (LNCS, Vol. 13354)*, Claudio Antares Mezzina and Krzysztof Podlaski (Eds.). Springer, 187–203. https://doi.org/10.1007/978-3-031-09005-9_13

[23] Rolf Landauer. 1961. Irreversibility and heat generated in the computing process. *IBM Journal of Research and Development* 5 (1961), 183–191. https://doi.org/10.1147/rd.53.0183

[24] Ivan Lanese and Doriana Medic. 2020. A general approach to derive uncontrolled reversible semantics. In *Proceedings of CONCUR 2020 (LIPIcs, Vol. 171)*, Igor Konnov and Laura Kovács (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für
[3] Attila Bagossy and György Vaszil. 2022. Controlled reversibility in communicating reaction systems. *Theoretical Computer Science* 926 (2022), 3–20. https://doi.org/10.1016/j.tcs.2022.05.030

[4] Marek A. Bednarczyk. 1991. *Hereditary history preserving bisimulations or what is the power of the future perfect in program logics*. Technical Report ICS PAS. Polish Academy of Sciences.

[5] Alexis Bernadet and Ivan Lanese. 2016. A modular formalization of reversibility for concurrent models and languages. In *Proceedings of ICE 2016 (EPTCS, Vol. 223)*, Massimo Bartoletti, Ludovic Henrio, Sophia Knight, and Hugo Torres Vieira (Eds.). 98–112. https://doi.org/10.4204/EPTCS.223.7

[6] Marco Bernardo and Claudio Antares Mezzina. 2023. Bridging causal reversibility and time reversibility: A stochastic process algebraic approach. *Logical Methods in Computer Science* 19, 2 (2023). https://doi.org/10.46298/LMCS-19(2:6)2023

[7] Marco Bernardo and Sabina Rossi. 2023. Reverse bisimilarity vs. forward bisimilarity. In *Proceedings of FoSSaCS 2023 (LNCS, Vol. 13992)*, Orna Kupferman and Pawel Sobocinski (Eds.). Springer, 265–284. https://doi.org/10.1007/978-3-031-30829-1_13

[8] Laura Bocchi, Ivan Lanese, Claudio Antares Mezzina, and Shoji Yuen. 2022. The reversible temporal process language. In *Proceedings of FORTE 2022 (LNCS, Vol. 13273)*, Mohammad Reza Mousavi and Anna Philippou (Eds.). Springer, 31–49. https://doi.org/10.1007/978-3-031-08679-3_3

[9] Luca Cardelli and Cosimo Laneve. 2011. Reversible structures. In *Proceedings of CMSB 2011*. ACM, 131–140. https://doi.org/10.1145/2037509.2037529

[10] Christopher D. Carothers, Kalyan S. Perumalla, and Richard Fujimoto. 1999. Efficient optimistic parallel simulations using reverse computation. *ACM Transactions on Modeling and Computer Simulation* 9, 3 (1999), 224–253. https://doi.org/10.1145/347823.347828

[11] Ioana Cristescu. 2015. *Operational and denotational semantics for the reversible π-calculus*. Ph. D. Dissertation. Paris Centre Mathematical sciences Doctoral School. https://scholar.harvard.edu/files/cristescu/files/these.pdf.

[12] Ioana Cristescu, Jean Krivine, and Daniele Varacca. 2013. A compositional semantics for the reversible π-calculus. In *Proceedings of LICS 2013*. IEEE Computer Society, 388–397. https://doi.org/10.1109/LICS.2013.45

[13] Vincent Danos and Jean Krivine. 2004. Reversible communicating systems. In *Proceedings of CONCUR 2004 (LNCS, Vol. 3170)*, Philippa Gardner and Nobuko Yoshida (Eds.). Springer, 292–307. https://doi.org/10.1007/978-3-540-28644-8_19

[14] Vincent Danos and Jean Krivine. 2005. Transactions in RCCS. In *Proceedings of CONCUR 2005 (LNCS, Vol. 3653)*, Martín Abadi and Luca de Alfaro (Eds.). Springer, 398–412. https://doi.org/10.1007/11539452_31

[15] Vincent Danos, Jean Krivine, and Paweł Sobociński. 2006. General reversibility. In *Proceedings of EXPRESS 2007 (ENTCS, Vol. 175(3))*, Roberto M. Amadio and Iain Phillips (Eds.). Elsevier, 75–86. https://doi.org/10.1016/j.entcs.2006.07.036

[16] David de Frutos Escrig, Maciej Koutny, and Łukasz Mikulski. 2019. Reversing steps in Petri nets. In *Proceedings of Petri Nets 2019 (LNCS, Vol. 11522)*, Susanna Donelli and Stefan Haar (Eds.). Springer, 171–191. https://doi.org/10.1007/978-3-030-21571-2_11

[17] Elena Giachino, Ivan Lanese, and Claudio Antares Mezzina. 2014. Causal-consistent reversible debugging. In *Proceedings of FASE 2014 (LNCS, Vol. 8411)*, Stefania Gnesi and Arend Rensink (Eds.). Springer, 370–384. https://doi.org/10.1007/978-3-642-54804-8_26

[18] Elena Giachino, Ivan Lanese, Claudio Antares Mezzina, and Francesco Tiezzi. 2017. Causal-consistent rollback in a tuple-based language. *Journal of Logical and Algebraic Methods in Programming* 88 (2017), 99–120. https://doi.org/10.1016/j.jlamp.2016.09.003

[19] Eva Graversen, Iain Phillips, and Nobuko Yoshida. 2022. Event structures for the reversible early internal π-calculus. *Journal of Logical and Algebraic Methods in Programming* 124 (2022), 100720. https://doi.org/10.1016/j.jlamp.2021.100720

[20] Thomas Troels Hildebrandt, Christian Johansen, and Håkon Normann. 2019. A stable non-interleaving early operational semantics for the pi-calculus. *Journal of Logical and Algebraic Methods in Programming* 104 (2019), 227–253. https://doi.org/10.1016/j.jlamp.2019.02.006

[21] Stefan Kuhn and Irek Ulidowski. 2018. Local reversibility in a Calculus of Covalent Bonding. *Science of Computer Programming* 151 (2018), 18–47. https://doi.org/10.1016/j.scico.2017.09.008

[22] Pietro Lami, Ivan Lanese, Jean-Bernard Stefani, Claudio Sacerdoti Coen, and Giovanni Fabbretti. 2022. Reversibility in Erlang: imperative constructs. In *Proceedings of RC 2022 (LNCS, Vol. 13354)*, Claudio Antares Mezzina and Krzysztof Podlaski (Eds.). Springer, 187–203. https://doi.org/10.1007/978-3-031-09005-9_13

[23] Rolf Landauer. 1961. Irreversibility and heat generated in the computing process. *IBM Journal of Research and Development* 5 (1961), 183–191. https://doi.org/10.1147/rd.53.0183

[24] Ivan Lanese and Doriana Medic. 2020. A general approach to derive uncontrolled reversible semantics. In *Proceedings of CONCUR 2020 (LIPIcs, Vol. 171)*, Igor Konnov and Laura Kovács (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 33:1–33:24. https://doi.org/10.4230/LIPIcs.CONCUR.2020.33

[25] Ivan Lanese, Claudio Antares Mezzina, Alan Schmitt, and Jean-Bernard Stefani. 2011. Controlling reversibility in higher-order pi. In *Proceedings of CONCUR 2011 (LNCS, Vol. 6901)*, Joost-Pieter Katoen and Barbara König (Eds.). Springer, 297–311. https://doi.org/10.1007/978-3-642-23217-6_20

[26] Ivan Lanese, Claudio Antares Mezzina, and Jean-Bernard Stefani. 2012. Controlled reversibility and compensations. In *Proceedings of RC 2012 (LNCS, Vol. 7581)*, Robert Glück and Tetsuo Yokoyama (Eds.). Springer, 233–240. https://doi.org/10.1007/978-3-642-36315-3_19

[27] Ivan Lanese, Claudio Antares Mezzina, and Jean-Bernard Stefani. 2016. Reversibility in the higher-order π-calculus. *Theoretical Computer Science* 625 (2016), 25–84. https://doi.org/10.1016/j.tcs.2016.02.019

[28] Ivan Lanese, Claudio Antares Mezzina, and Francesco Tiezzi. 2014. Causal-consistent reversibility. *Bulletin of the EATCS* 114 (2014).

[29] Ivan Lanese, Naoki Nishida, Adrián Palacios, and Germán Vidal. 2018. CauDEr: A causal-consistent reversible debugger for Erlang. In *Proceedings of FLOPS 2018 (LNCS, Vol. 10818)*, John P. Gallagher and Martin Sulzmann (Eds.). Springer, 247–263. https://doi.org/10.1007/978-3-319-90686-7_16

[30] Ivan Lanese, Naoki Nishida, Adrián Palacios, and Germán Vidal. 2018. A theory of reversibility for Erlang. *Journal of Logical and Algebraic Methods in Programming* 100 (2018), 71–97. https://doi.org/10.1016/j.jlamp.2018.06.004

[31] Ivan Lanese, Iain Phillips, and Irek Ulidowski. 2020. An axiomatic approach to reversible computation. In *Proceedings of FoSSaCS 2020 (LNCS, Vol. 12077)*, Jean Goubault-Larrecq and Barbara König (Eds.). Springer, 442–461. https://doi.org/10.1007/978-3-030-45231-5_23

[32] Johan Sund Laursen, Ulrik Pagh Schultz, and Lars-Peter Ellekilde. 2015. Automatic error recovery in robot assembly operations using reverse execution. In *Proceedings of IROS 2015*. IEEE, 1785–1792. https://doi.org/10.1109/IROS.2015.7353609

[33] Michael Lienhardt, Ivan Lanese, Claudio Antares Mezzina, and Jean-Bernard Stefani. 2012. A reversible abstract machine and its space overhead. In *Proceedings of FMOODS/FORTE 2012 (LNCS, Vol. 7273)*, Holger Giese and Grigore Rosu (Eds.). Springer, 1–17. https://doi.org/10.1007/978-3-642-30793-5_1

[34] James McNellis, Jordi Mola, and Ken Sykes. 2017. Time travel debugging: root causing bugs in commercial scale software. CppCon talk, https://www.youtube.com/watch?v=l1YJTg_A914.

[35] Hernán C. Melgratti, Claudio Antares Mezzina, Iain Phillips, G. Michele Pinna, and Irek Ulidowski. 2020. Reversible occurrence nets and causal reversible prime event structures. In *Proceedings of RC 2020 (LNCS, Vol. 12227)*, Ivan Lanese and Mariusz Rawski (Eds.). Springer, 35–53. https://doi.org/10.1007/978-3-030-52482-1_2

[36] Hernán C. Melgratti, Claudio Antares Mezzina, and Irek Ulidowski. 2019. Reversing P/T nets. In *Proceedings of COORDINATION 2019 (LNCS, Vol. 11533)*, Hanne Riis Nielson and Emilio Tuosto (Eds.). Springer, 19–36. https://doi.org/10.1007/978-3-030-22397-7_2

[37] Hernán C. Melgratti, Claudio Antares Mezzina, and Irek Ulidowski. 2020. Reversing Place Transition nets. *Logical Methods in Computer Science* 16, 4 (2020). https://doi.org/10.23638/LMCS-16(4:5)2020

[38] Claudio Antares Mezzina. 2018. On reversibility and broadcast. In *Proceedings of RC 2018 (LNCS, Vol. 11106)*, Jarkko Kari and Irek Ulidowski (Eds.). Springer, 67–83. https://doi.org/10.1007/978-3-319-99498-7_5

[39] Mogens Nielsen and Glynn Winskel. 1995. Models for concurrency. In *Handbook of Logic in Computer Science*. Vol. 4. Oxford University Press, 1–148. https://doi.org/10.5555/218623.218630

[40] Iain Phillips and Irek Ulidowski. 2006. Reversing algebraic process calculi. In *Proceedings of FoSSaCS 2006 (LNCS, Vol. 3921)*, Luca Aceto and Anna Ingólfsdóttir (Eds.). Springer, 246–260. https://doi.org/10.1007/11690634_17

[41] Iain Phillips and Irek Ulidowski. 2007. Reversibility and models for concurrency. In *Proceedings of SOS 2007 (ENTCS, Vol. 192(1))*, Matthew C.B. Hennessy and Rob J. van Glabbeek (Eds.). Elsevier, 93–108. https://doi.org/10.1016/j.entsc.2007.08.018

[42] Iain Phillips and Irek Ulidowski. 2007. Reversing algebraic process calculi. *Journal of Logic and Algebraic Programming* 73, 1-2 (2007), 70–96. https://doi.org/10.1016/j.jlap.2006.11.002

[43] Iain Phillips and Irek Ulidowski. 2013. Reversibility and asymmetric conflict in event structures. In *Proceedings of CONCUR 2013 (LNCS, Vol. 8052)*, Pedro R. D'Argenio and Hernán C. Melgratti (Eds.). Springer, 303–318. https://doi.org/10.1007/978-3-642-40184-8_22

[44] Iain Phillips and Irek Ulidowski. 2015. Reversibility and asymmetric conflict in event structures. *Journal of Logical and Algebraic Methods in Programming* 84 (2015), 781–805. https://doi.org/10.1016/j.jlamp.2015.07.004

[45] Iain Phillips, Irek Ulidowski, and Shoji Yuen. 2012. A reversible process calculus and the modelling of the ERK signalling pathway. In *Proceedings of RC 2012 (LNCS, Vol. 7581)*, Robert Glück and Tetsuo Yokoyama (Eds.). Springer, 218–232. https://doi.org/10.1007/978-3-642-36315-3_18

[46] Jean-Eric Pin. 1987. On the language accepted by finite reversible automata. In *Proceedings of ICALP'87 (LNCS, Vol. 267)*, Thomas Ottmann (Ed.). Springer, 237–249. https://doi.org/10.1007/3-540-18088-5_19
Informatik, 33:1–33:24. https://doi.org/10.4230/LIPIcs.CONCUR.2020.33

[25] Ivan Lanese, Claudio Antares Mezzina, Alan Schmitt, and Jean-Bernard Stefani. 2011. Controlling reversibility in higher-order pi. In *Proceedings of CONCUR 2011 (LNCS, Vol. 6901)*, Joost-Pieter Katoen and Barbara König (Eds.). Springer, 297–311. https://doi.org/10.1007/978-3-642-23217-6_20

[26] Ivan Lanese, Claudio Antares Mezzina, and Jean-Bernard Stefani. 2012. Controlled reversibility and compensations. In *Proceedings of RC 2012 (LNCS, Vol. 7581)*, Robert Glück and Tetsuo Yokoyama (Eds.). Springer, 233–240. https://doi.org/10.1007/978-3-642-36315-3_19

[27] Ivan Lanese, Claudio Antares Mezzina, and Jean-Bernard Stefani. 2016. Reversibility in the higher-order π-calculus. *Theoretical Computer Science* 625 (2016), 25–84. https://doi.org/10.1016/j.tcs.2016.02.019

[28] Ivan Lanese, Claudio Antares Mezzina, and Francesco Tiezzi. 2014. Causal-consistent reversibility. *Bulletin of the EATCS* 114 (2014).

[29] Ivan Lanese, Naoki Nishida, Adrián Palacios, and Germán Vidal. 2018. CauDEr: A causal-consistent reversible debugger for Erlang. In *Proceedings of FLOPS 2018 (LNCS, Vol. 10818)*, John P. Gallagher and Martin Sulzmann (Eds.). Springer, 247–263. https://doi.org/10.1007/978-3-319-90686-7_16

[30] Ivan Lanese, Naoki Nishida, Adrián Palacios, and Germán Vidal. 2018. A theory of reversibility for Erlang. *Journal of Logical and Algebraic Methods in Programming* 100 (2018), 71–97. https://doi.org/10.1016/j.jlamp.2018.06.004

[31] Ivan Lanese, Iain Phillips, and Irek Ulidowski. 2020. An axiomatic approach to reversible computation. In *Proceedings of FoSSaCS 2020 (LNCS, Vol. 12077)*, Jean Goubault-Larrecq and Barbara König (Eds.). Springer, 442–461. https://doi.org/10.1007/978-3-030-45231-5_23

[32] Johan Sund Laursen, Ulrik Pagh Schultz, and Lars-Peter Ellekilde. 2015. Automatic error recovery in robot assembly operations using reverse execution. In *Proceedings of IROS 2015*. IEEE, 1785–1792. https://doi.org/10.1109/IROS.2015.7353609

[33] Michael Lienhardt, Ivan Lanese, Claudio Antares Mezzina, and Jean-Bernard Stefani. 2012. A reversible abstract machine and its space overhead. In *Proceedings of FMOODS/FORTE 2012 (LNCS, Vol. 7273)*, Holger Giese and Grigore Rosu (Eds.). Springer, 1–17. https://doi.org/10.1007/978-3-642-30793-5_1

[34] James McNellis, Jordi Mola, and Ken Sykes. 2017. Time travel debugging: root causing bugs in commercial scale software. CppCon talk, https://www.youtube.com/watch?v=l1YJTg_A914.

[35] Hernán C. Melgratti, Claudio Antares Mezzina, Iain Phillips, G. Michele Pinna, and Irek Ulidowski. 2020. Reversible occurrence nets and causal reversible prime event structures. In *Proceedings of RC 2020 (LNCS, Vol. 12227)*, Ivan Lanese and Mariusz Rawski (Eds.). Springer, 35–53. https://doi.org/10.1007/978-3-030-52482-1_2

[36] Hernán C. Melgratti, Claudio Antares Mezzina, and Irek Ulidowski. 2019. Reversing P/T nets. In *Proceedings of COORDINATION 2019 (LNCS, Vol. 11533)*, Hanne Riis Nielson and Emilio Tuosto (Eds.). Springer, 19–36. https://doi.org/10.1007/978-3-030-22397-7_2

[37] Hernán C. Melgratti, Claudio Antares Mezzina, and Irek Ulidowski. 2020. Reversing Place Transition nets. *Logical Methods in Computer Science* 16, 4 (2020). https://doi.org/10.23638/LMCS-16(4:5)2020

[38] Claudio Antares Mezzina. 2018. On reversibility and broadcast. In *Proceedings of RC 2018 (LNCS, Vol. 11106)*, Jarkko Kari and Irek Ulidowski (Eds.). Springer, 67–83. https://doi.org/10.1007/978-3-319-99498-7_5

[39] Mogens Nielsen and Glynn Winskel. 1995. Models for concurrency. In *Handbook of Logic in Computer Science*. Vol. 4. Oxford University Press, 1–148. https://doi.org/10.5555/218623.218630

[40] Iain Phillips and Irek Ulidowski. 2006. Reversing algebraic process calculi. In *Proceedings of FoSSaCS 2006 (LNCS, Vol. 3921)*, Luca Aceto and Anna Ingólfsdóttir (Eds.). Springer, 246–260. https://doi.org/10.1007/11690634_17

[41] Iain Phillips and Irek Ulidowski. 2007. Reversibility and models for concurrency. In *Proceedings of SOS 2007 (ENTCS, Vol. 192(1))*, Matthew C.B. Hennessy and Rob J. van Glabbeek (Eds.). Elsevier, 93–108. https://doi.org/10.1016/j.entsc.2007.08.018

[42] Iain Phillips and Irek Ulidowski. 2007. Reversing algebraic process calculi. *Journal of Logic and Algebraic Programming* 73, 1-2 (2007), 70–96. https://doi.org/10.1016/j.jlap.2006.11.002

[43] Iain Phillips and Irek Ulidowski. 2013. Reversibility and asymmetric conflict in event structures. In *Proceedings of CONCUR 2013 (LNCS, Vol. 8052)*, Pedro R. D'Argenio and Hernán C. Melgratti (Eds.). Springer, 303–318. https://doi.org/10.1007/978-3-642-40184-8_22

[44] Iain Phillips and Irek Ulidowski. 2015. Reversibility and asymmetric conflict in event structures. *Journal of Logical and Algebraic Methods in Programming* 84 (2015), 781–805. https://doi.org/10.1016/j.jlamp.2015.07.004

[45] Iain Phillips, Irek Ulidowski, and Shoji Yuen. 2012. A reversible process calculus and the modelling of the ERK signalling pathway. In *Proceedings of RC 2012 (LNCS, Vol. 7581)*, Robert Glück and Tetsuo Yokoyama (Eds.). Springer, 218–232. https://doi.org/10.1007/978-3-642-36315-3_18

[46] Jean-Eric Pin. 1987. On the language accepted by finite reversible automata. In *Proceedings of ICALP'87 (LNCS, Vol. 267)*, Thomas Ottmann (Ed.). Springer, 237–249. https://doi.org/10.1007/3-540-18088-5_19
[47] Vladimiro Sassone, Mogens Nielsen, and Glynn Winskel. 1996. Models of concurrency: Towards a classification. *Theoretical Computer Science* 170, 1-2 (1996), 297-348. https://doi.org/10.1016/S0304-3975(96)80710-9

[48] Rob J. van Glabbeek. 1996. History preserving process graphs. (1996). Draft 20 June 1996. http://boole.stanford.edu/~rvg/pub/history.draft.dvi.

[49] Rob J. van Glabbeek and Frits W. Vaandrager. 1997. The difference between splitting in *n* and *n* + 1. *Information and Computation* 136, 2 (1997), 109-142. https://doi.org/10.1006/inco.1997.2634

[50] Tetsuo Yokoyama and Robert Glück. 2007. A reversible programming language and its invertible self-interpreter. In *Proceedings of ACM SIGPLAN PEPM 2007*, Ganesan Ramalingam and Eelco Visser (Eds.). ACM, 144-153. https://doi.org/10.1145/1244381.1244404
[47] Vladimiro Sassone, Mogens Nielsen, and Glynn Winskel. 1996. Models of concurrency: Towards a classification. *Theoretical Computer Science* 170, 1-2 (1996), 297-348. https://doi.org/10.1016/S0304-3975(96)80710-9

[48] Rob J. van Glabbeek. 1996. History preserving process graphs. (1996). Draft 20 June 1996. http://boole.stanford.edu/~rvg/pub/history.draft.dvi.

[49] Rob J. van Glabbeek and Frits W. Vaandrager. 1997. The difference between splitting in *n* and *n* + 1. *Information and Computation* 136, 2 (1997), 109-142. https://doi.org/10.1006/inco.1997.2634

[50] Tetsuo Yokoyama and Robert Glück. 2007. A reversible programming language and its invertible self-interpreter. In *Proceedings of ACM SIGPLAN PEPM 2007*, Ganesan Ramalingam and Eelco Visser (Eds.). ACM, 144–153. https://doi.org/10.1145/1244381.1244404