# An Axiomatic Theory for Reversible Computation

Ivan Lanese, Iain Phillips, Irek Ulidowski

► To cite this version:

Ivan Lanese, Iain Phillips, Irek Ulidowski. An Axiomatic Theory for Reversible Computation. ACM Transactions on Computational Logic, 2024, 25 (2), pp.1-40. 10.1145/3648474. hal-04575972

HAL Id: hal-04575972

https://inria.hal.science/hal-04575972

Submitted on 15 May 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# An Axiomatic Theory for Reversible Computation

IVAN LANESE, Olas Team, University of Bologna/INRIA, Italy

IAIN PHILLIPS, Imperial College London, England

IREK ULIDOWSKI, University of Leicester, England; AGH University of Science and Technology, Poland

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

CCS Concepts: • **Theory of computation** → **Concurrency**; *Process calculi*; • **Computing methodologies** → *Concurrent programming languages*.

Additional Key Words and Phrases: Reversible Computation, Labelled Transition System with Independence, Causal Consistency, Causal Safety, Causal Liveness

**ACM Reference Format:**

Ivan Lanese, Iain Phillips, and Irek Ulidowski. 2024. An Axiomatic Theory for Reversible Computation. *ACM Trans. Comput. Logic* 1, 1, Article 1 (January 2024), 40 pages. https://doi.org/10.1145/3648474

## 1 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 [23], simulation [10], robotics [32], biological modelling [9, 45] and debugging [29, 34].

Authors' addresses: Ivan Lanese, Olas Team, University of Bologna/INRIA, Bologna, Italy, ivan.lanese@gmail.com; Iain Phillips, Imperial College London, London, England, i.phillips@imperial.ac.uk; Irek Ulidowski, University of Leicester, Leicester, England; and AGH University of Science and Technology, Kraków, Poland, i.ulidowski@leicester.ac.uk.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org.

© 2024 Copyright held by the owner/author(s). Publication rights licensed to ACM.

ACM 1529-3785/2024/1-ART1

https://doi.org/10.1145/3648474
# An Axiomatic Theory for Reversible Computation

IVAN LANESE, Olas Team, University of Bologna/INRIA, Italy

IAIN PHILLIPS, Imperial College London, England

IREK ULIDOWSKI, University of Leicester, England; AGH University of Science and Technology, Poland

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

CCS Concepts: • **Theory of computation** → **Concurrency**; *Process calculi*; • **Computing methodologies** → *Concurrent programming languages*.

Additional Key Words and Phrases: Reversible Computation, Labelled Transition System with Independence, Causal Consistency, Causal Safety, Causal Liveness

**ACM Reference Format:**

Ivan Lanese, Iain Phillips, and Irek Ulidowski. 2024. An Axiomatic Theory for Reversible Computation. *ACM Trans. Comput. Logic* 1, 1, Article 1 (January 2024), 40 pages. https://doi.org/10.1145/3648474

# 1 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 [23], simulation [10], robotics [32], biological modelling [9, 45] and debugging [29, 34].

Authors' addresses: Ivan Lanese, Olas Team, University of Bologna/INRIA, Bologna, Italy, ivan.lanese@gmail.com; Iain Phillips, Imperial College London, London, England, i.phillips@imperial.ac.uk; Irek Ulidowski, University of Leicester, Leicester, England; and AGH University of Science and Technology, Kraków, Poland, i.ulidowski@leicester.ac.uk.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org.

© 2024 Copyright held by the owner/author(s). Publication rights licensed to ACM.

ACM 1529-3785/2024/1-ART1

https://doi.org/10.1145/3648474
There is widespread agreement in the literature about what properties characterise reversible computation in the classical sequential (hence deterministic) a notion of reversibility suited for con-current systems called *causal-consistent reversibility* (other notions were also used later on, e.g., to model biological systems [45]). According to an informal account of causal-consistent reversibility, any action can be undone provided that its consequences<fnref n="1" /> if any, are undone beforehand. Follow-ing [13] 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 [13, 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) [13, Theorem 1], stating that
coinitial computations are causal equivalent if and only if they are cofinal. Our new proof of CC
(Proposition 3.8) shows that it holds in essentially any reversible formalism satisfying the Loop
Lemma (roughly, any action can be undone) and the Parabolic Lemma (roughly, any computation
is equivalent to a backward computation followed by a forward one), 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 [30, Corollary 22], stating that a forward transition *t* can be undone after a derivation if and only if all the consequences of *t*, if any, are undone beforehand. We are not aware of other discussions trying to formalise such a notion, except for [44], in the setting of reversible event structures. In [44], 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 [44, Definition 3.34].

We provide (Section 5) 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 5.7, 5.8 and 5.9), 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 and 6). This is in sharp contrast with the large part of works in the literature, which consider specific frameworks such as CCS [13], CCS with broadcast [38], CCB [21], π-calculus [12], higher-order π [27], Klaim [18], Petri nets [36], µOz [33] and Erlang [30], 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.8);

<footnote n="1">¹By consequence we mean any subsequent transition which could not be permuted with *t* while preserving the resulting state.</footnote>
There is widespread agreement in the literature about what properties characterise reversible computation in the classical sequential (hence deterministic) a notion of reversibility suited for con-current systems called *causal-consistent reversibility* (other notions were also used later on, e.g., to model biological systems [45]). According to an informal account of causal-consistent reversibility, any action can be undone provided that its consequences<fnref n="1" /> if any, are undone beforehand. Follow-ing [13] 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 [13, 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) [13, Theorem 1], stating that
coinital computations are causal equivalent if and only if they are cofinal. Our new proof of CC
(Proposition 3.8) shows that it holds in essentially any reversible formalism satisfying the Loop
Lemma (roughly, any action can be undone) and the Parabolic Lemma (roughly, any computation
is equivalent to a backward computation followed by a forward one), 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 [30, Corollary 22], stating that a forward transition *t* can be undone after a derivation if and only if all the consequences of *t*, if any, are undone beforehand. We are not aware of other discussions trying to formalise such a notion, except for [44], in the setting of reversible event structures. In [44], 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 [44, Definition 3.34].

We provide (Section 5) 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 5.7, 5.8 and 5.9), 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 and 6). This is in sharp contrast with the large part of works in the literature, which consider specific frameworks such as CCS [13], CCS with broadcast [38], CCB [21], π-calculus [12], higher-order π [27], Klaim [18], Petri nets [36], µOz [33] and Erlang [30], 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.8);

<footnote n="1">¹By consequence we mean any subsequent transition which could not be permuted with *t* while preserving the resulting state.</footnote>
<table><caption>Table 1. Axioms and properties for causal reversibility. 'Str. Ax.' abbreviates 'Structural Axiom' and 'Pre-rev.' abbreviates 'Pre-reversible', namely SP, BTI, WF, PCI (cf. Def. 4.3). We call statements in the bottom part of the table, namely from PL to CL<, properties.</caption><thead><tr><th>Acronym</th><th>Name</th><th>Defined in</th><th>Proved in</th><th>Using</th></tr></thead><tbody><tr><td>SP</td><td>Square Property</td><td>Def. 3.1</td><td>Axiom</td><td>-</td></tr><tr><td>BTI</td><td>Backward Transitions are Independent</td><td>Def. 3.1</td><td>Axiom</td><td>-</td></tr><tr><td>WF</td><td>Well-Founded</td><td>Def. 3.1</td><td>Axiom</td><td>-</td></tr><tr><td>PCI</td><td>Propagation of Coinitial Independence</td><td>Def. 4.2</td><td>Axiom</td><td>implied by LG or CLG</td></tr><tr><td>IRE</td><td>Independence Respects Events</td><td>Def. 5.3</td><td>Axiom</td><td>implied by LG</td></tr><tr><td>CIRE</td><td>Coinitial Independence Respects Events</td><td>Def. 5.21</td><td>Axiom</td><td>implied by IRE or CLG</td></tr><tr><td>BFCIRE</td><td>Backward-Forward CIRE</td><td>Def. 5.28</td><td>Axiom</td><td>implied by CIRE</td></tr><tr><td>IEC</td><td>Independence of Events is Coinitial</td><td>Def. 5.10</td><td>Axiom</td><td>-</td></tr><tr><td>CLG</td><td>Coinitial Label-Generated</td><td>Def. 6.9</td><td>Str. Ax.</td><td>-</td></tr><tr><td>LG</td><td>Label-Generated</td><td>Def. 6.11</td><td>Str. Ax.</td><td>-</td></tr><tr><td>IC</td><td>Independence is Coinitial</td><td>Def. 6.1</td><td>Str. Ax.</td><td>implied by CLG</td></tr><tr><td>PL</td><td>Parabolic Lemma</td><td>Def. 3.3</td><td>Prop. 3.4</td><td>BTI, SP</td></tr><tr><td>CC</td><td>Causal Consistency</td><td>Def. 3.7</td><td>Prop. 3.8</td><td>WF, PL</td></tr><tr><td>UT</td><td>Unique Transition</td><td>Def. 3.11</td><td>Cor. 3.12</td><td>CC</td></tr><tr><td>BLD</td><td>Backward Label Determinism</td><td>Def. 4.5</td><td>Prop. 4.6</td><td>SP, BTI, PCI</td></tr><tr><td>ID</td><td>Independence of Diamonds</td><td>Def. 4.9</td><td>Prop. 4.10</td><td>BTI, PCI</td></tr><tr><td>NRE</td><td>No Repeated Events</td><td>Def. 4.18</td><td>Prop. 4.21</td><td>Pre-rev.</td></tr><tr><td>RPI</td><td>Reversing Preserves Independence</td><td>Def. 5.11</td><td>Prop. 5.12</td><td>SP, PCI, IRE, IEC</td></tr><tr><td>CS<sub>t</sub></td><td>Causal Safety</td><td>Def. 5.1</td><td>Thm. 5.5</td><td>Pre-rev., IRE</td></tr><tr><td>CL<sub>t</sub></td><td>Causal Liveness</td><td>Def. 5.1</td><td>Thm. 5.6</td><td>Pre-rev., IRE</td></tr><tr><td>ECh</td><td>Event Coherence</td><td>Def. 5.13</td><td>Prop. 5.14</td><td>Pre-rev., (IRE or IEC)</td></tr><tr><td>CS<sub>ci</sub></td><td>coinitial Causal Safety</td><td>Def. 5.19</td><td>Thm. 5.20</td><td>Pre-rev.</td></tr><tr><td>CL<sub>ci</sub></td><td>coinitial Causal Liveness</td><td>Def. 5.19</td><td>Thm. 5.29</td><td>Pre-rev., BFCIRE</td></tr><tr><td>CS<sub>&lt;</sub></td><td>ordered Causal Safety</td><td>Def. 5.37</td><td>Prop. 5.39</td><td>Pre-rev.</td></tr><tr><td>CL<sub>&lt;</sub></td><td>ordered Causal Liveness</td><td>Def. 5.37</td><td>Prop. 5.39</td><td>Pre-rev., BFCIRE</td></tr></tbody></table>

<figure><img src="image_1.png" /><figcaption>Fig. 1. Irreversible transition systems in CCS.</figcaption></figure>

* hold for a number of reversible calculi which have been proposed, such as RCCS [13] and reversible Erlang [30] (Section 7).

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 CCS processes and their transitions as in Figure 1:

a.0 $\xrightarrow{a}$ 0, b.0 $\xrightarrow{b}$ 0: from state 0 one does not know whether to go back to a.0 or to b.0;
<table><caption>Table 1. Axioms and properties for causal reversibility. 'Str. Ax.' abbreviates 'Structural Axiom' and 'Pre-rev.' abbreviates 'Pre-reversible', namely SP, BTI, WF, PCI (cf. Def. 4.3). We call statements in the bottom part of the table, namely from PL to CL<sub>&lt;</sub>, properties.</caption><thead><tr><th>Acronym</th><th>Name</th><th>Defined in</th><th>Proved in</th><th>Using</th></tr></thead><tbody><tr><td>SP</td><td>Square Property</td><td>Def. 3.1</td><td>Axiom</td><td>-</td></tr><tr><td>BTI</td><td>Backward Transitions are Independent</td><td>Def. 3.1</td><td>Axiom</td><td>-</td></tr><tr><td>WF</td><td>Well-Founded</td><td>Def. 3.1</td><td>Axiom</td><td>-</td></tr><tr><td>PCI</td><td>Propagation of Coinitial Independence</td><td>Def. 4.2</td><td>Axiom</td><td>implied by LG or CLG</td></tr><tr><td>IRE</td><td>Independence Respects Events</td><td>Def. 5.3</td><td>Axiom</td><td>implied by LG</td></tr><tr><td>CIRE</td><td>Coinitial Independence Respects Events</td><td>Def. 5.21</td><td>Axiom</td><td>implied by IRE or CLG</td></tr><tr><td>BFCIRE</td><td>Backward-Forward CIRE</td><td>Def. 5.28</td><td>Axiom</td><td>implied by CIRE</td></tr><tr><td>IEC</td><td>Independence of Events is Coinitial</td><td>Def. 5.10</td><td>Axiom</td><td>-</td></tr><tr><td>CLG</td><td>Coinitial Label-Generated</td><td>Def. 6.9</td><td>Str. Ax.</td><td>-</td></tr><tr><td>LG</td><td>Label-Generated</td><td>Def. 6.11</td><td>Str. Ax.</td><td>-</td></tr><tr><td>IC</td><td>Independence is Coinitial</td><td>Def. 6.1</td><td>Str. Ax.</td><td>implied by CLG</td></tr><tr><td>PL</td><td>Parabolic Lemma</td><td>Def. 3.3</td><td>Prop. 3.4</td><td>BTI, SP</td></tr><tr><td>CC</td><td>Causal Consistency</td><td>Def. 3.7</td><td>Prop. 3.8</td><td>WF, PL</td></tr><tr><td>UT</td><td>Unique Transition</td><td>Def. 3.11</td><td>Cor. 3.12</td><td>CC</td></tr><tr><td>BLD</td><td>Backward Label Determinism</td><td>Def. 4.5</td><td>Prop. 4.6</td><td>SP, BTI, PCI</td></tr><tr><td>ID</td><td>Independence of Diamonds</td><td>Def. 4.9</td><td>Prop. 4.10</td><td>BTI, PCI</td></tr><tr><td>NRE</td><td>No Repeated Events</td><td>Def. 4.18</td><td>Prop. 4.21</td><td>Pre-rev.</td></tr><tr><td>RPI</td><td>Reversing Preserves Independence</td><td>Def. 5.11</td><td>Prop. 5.12</td><td>SP, PCI, IRE, IEC</td></tr><tr><td>CS<sub>t</sub></td><td>Causal Safety</td><td>Def. 5.1</td><td>Thm. 5.5</td><td>Pre-rev., IRE</td></tr><tr><td>CL<sub>t</sub></td><td>Causal Liveness</td><td>Def. 5.1</td><td>Thm. 5.6</td><td>Pre-rev., IRE</td></tr><tr><td>ECh</td><td>Event Coherence</td><td>Def. 5.13</td><td>Prop. 5.14</td><td>Pre-rev., (IRE or IEC)</td></tr><tr><td>CS<sub>ci</sub></td><td>coinitial Causal Safety</td><td>Def. 5.19</td><td>Thm. 5.20</td><td>Pre-rev.</td></tr><tr><td>CL<sub>ci</sub></td><td>coinitial Causal Liveness</td><td>Def. 5.19</td><td>Thm. 5.29</td><td>Pre-rev., BFCIRE</td></tr><tr><td>CS<sub>&lt;</sub></td><td>ordered Causal Safety</td><td>Def. 5.37</td><td>Prop. 5.39</td><td>Pre-rev.</td></tr><tr><td>CL<sub>&lt;</sub></td><td>ordered Causal Liveness</td><td>Def. 5.37</td><td>Prop. 5.39</td><td>Pre-rev., BFCIRE</td></tr></tbody></table>

<figure><img src="image_2.png" /><figcaption>Fig. 1. Irreversible transition systems in CCS.</figcaption></figure>

* hold for a number of reversible calculi which have been proposed, such as RCCS [13] and reversible Erlang [30] (Section 7).

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 CCS processes and their transitions as in Figure 1:

a.0 $\xrightarrow{a}$ 0, b.0 $\xrightarrow{b}$ 0: from state 0 one does not know whether to go back to a.0 or to b.0;
a.0 + b.0 $\xrightarrow{a}$ 0, a.0 + b.0 $\xrightarrow{b}$ 0: as above, but starting from the same process, hence showing that it is not enough to remember the initial configuration;

$P \xrightarrow{a} P \text{ where } P \stackrel{def}{=} a.P$: in state $P$ one does not know whether action $a$ has been performed, and, if it has been performed, then how many times. Due to this lack of information, one could go back an arbitrary number of times from $P$ to $P$. In this work, we do not permit an arbitrary number of backward moves, because it goes 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.

The paper is organised as follows. The next section introduces labelled transition systems with independence (LTSIs). Three basic axioms for reversibility (SP, BTI and WF) are defined in Section 3, and are used to prove the Parabolic Lemma and Causal Consistency. Events are defined in Section 4, where another basic axiom (PCI) is formulated. In Section 5 we discuss and define CS and CL properties, and introduce three further basic axioms (IRE, CIRE and IEC) that are used to prove them. We consider three versions of CS and CL: those based on independence of transitions, on independence of events, and on ordering of events, and we study their relationships. We also show that axioms SP, BTI, WF, PCI and IEC, together with any one of IRE, CIRE and BFCIRE, are independent of each other. Section 6 considers two structured forms of independence, namely independence defined on coinitial transitions only, and independence defined on labels only. Eight case studies of reversible formalisms are presented in Section 7, where we demonstrate that our basic axioms are very effective in proving the main reversibility properties. Section 8 discusses relations with other works in the literature. The final section contains concluding remarks and suggests potential future work.

This paper is an extended version of [31]. The paper has been fully restructured, and now includes a number of additional or refined results. Beyond this, it includes full proofs of our results, as well as additional case studies, examples and explanations. We remark that the preliminary results in [31] have already been exploited in [1–3, 6, 8, 22, 24], which can be seen as further case studies for our approach.

## 2 LABELLED TRANSITION SYSTEMS WITH INDEPENDENCE

We want to study reversibility in a setting as general as possible. Thus, we adopt initially only the core of the notion of labelled transition system with independence (LTSI) [47, Definition 3.7], and explore what can be achieved by adding various axioms on the independence relation. This is in contrast with the approach taken in [47], which requires a fixed number of axioms to hold in LTSIs. Also, we extend LTSIs with reverse transitions, since we study reversible systems. We first define 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 $(\text{Proc}, \text{Lab}, \rightarrow)$, where *Proc* is the set of states (or processes), *Lab* is the set of action labels and $\rightarrow \subseteq \text{Proc} \times \text{Lab} \times \text{Proc}$ is a transition relation.

We let $P, Q, \dots$ range over processes, $a, b, c, \dots$ range over labels, and $t, u, v, \dots$ range over transitions (namely, elements of the transition relation). We can write $t : P \xrightarrow{a} Q$ to denote that $t = (P, a, Q)$. We call $a$-transition a transition with label $a$.
$a.0 + b.0 \stackrel{a}{\rightarrow} 0$, $a.0 + b.0 \stackrel{b}{\rightarrow} 0$: as above, but starting from the same process, hence showing that it is not enough to remember the initial configuration;

$P \stackrel{a}{\rightarrow} P \text{ where } P \stackrel{def}{=} a.P$: in state $P$ one does not know whether action $a$ has been performed, and, if it has been performed, then how many times. Due to this lack of information, one could go back an arbitrary number of times from $P$ to $P$. In this work, we do not permit an arbitrary number of backward moves, because it goes 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.

The paper is organised as follows. The next section introduces labelled transition systems with independence (LTSIs). Three basic axioms for reversibility (SP, BTI and WF) are defined in Section 3, and are used to prove the Parabolic Lemma and Causal Consistency. Events are defined in Section 4, where another basic axiom (PCI) is formulated. In Section 5 we discuss and define CS and CL properties, and introduce three further basic axioms (IRE, CIRE and IEC) that are used to prove them. We consider three versions of CS and CL: those based on independence of transitions, on independence of events, and on ordering of events, and we study their relationships. We also show that axioms SP, BTI, WF, PCI and IEC, together with any one of IRE, CIRE and BFCIRE, are independent of each other. Section 6 considers two structured forms of independence, namely independence defined on coinitial transitions only, and independence defined on labels only. Eight case studies of reversible formalisms are presented in Section 7, where we demonstrate that our basic axioms are very effective in proving the main reversibility properties. Section 8 discusses relations with other works in the literature. The final section contains concluding remarks and suggests potential future work.

This paper is an extended version of [31]. The paper has been fully restructured, and now includes a number of additional or refined results. Beyond this, it includes full proofs of our results, as well as additional case studies, examples and explanations. We remark that the preliminary results in [31] have already been exploited in [1–3, 6, 8, 22, 24], which can be seen as further case studies for our approach.

## 2 LABELLED TRANSITION SYSTEMS WITH INDEPENDENCE

We want to study reversibility in a setting as general as possible. Thus, we adopt initially only the core of the notion of *labelled transition system with independence* (LTSI) [47, Definition 3.7], and explore what can be achieved by adding various axioms on the independence relation. This is in contrast with the approach taken in [47], which requires a fixed number of axioms to hold in LTSIs. Also, we extend LTSIs with reverse transitions, since we study reversible systems. We first define 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 $(\text{Proc}, \text{Lab}, \rightarrow)$, where *Proc* is the set of states (or processes), *Lab* is the set of action labels and $\rightarrow \subseteq \text{Proc} \times \text{Lab} \times \text{Proc}$ is a transition relation.

We let $P, Q, \dots$ range over processes, $a, b, c, \dots$ range over labels, and $t, u, v, \dots$ range over transitions (namely, elements of the transition relation). We can write $t : P \stackrel{a}{\rightarrow} 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, →, t) is an LTS with independence (LTSI) if (Proc, Lab, →) is an LTS and t is an irreflexive symmetric binary relation on transitions.

In many cases (see Section 7), 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 processes, 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 [13, Lemma 6] holds. This does not hold in models of reversibility with control mechanisms [26] such as irreversible actions [14] or a rollback operator [25]. 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 [18, 30]. The present work helps with the first step.

*Definition 2.3 (Reverse and combined LTS).* Given an LTS (Proc, Lab, →), let the reverse LTS be (Proc, Lab, ⇄), where $P \stackrel{a}{月至} Q$ iff $Q \stackrel{a}{月至} P$. It is convenient to combine the two LTSs (forward and reverse): let the reverse labels be $\underline{Lab} = \{\underline{a} : a \in Lab\}$, and define the combined LTS to be $\rightarrow \subseteq \text{Proc} \times (Lab \cup \underline{Lab}) \times \text{Proc}$ by $P \stackrel{a}{月至} Q$ iff $P \stackrel{a}{月至} Q$ and $P \stackrel{a}{月至} Q$ iff $P \stackrel{a}{月至} Q$.

We stipulate that the union $Lab \cup \underline{Lab}$ is disjoint. We let $\alpha, \beta, \dots$ range over Lab $\cup \underline{Lab}$. For $\alpha \in Lab \cup \underline{Lab}$, the *underlying* action label $\text{und}(\alpha)$ is defined as $\text{und}(a) = a$ and $\text{und}(\underline{a}) = \underline{a}$. Let $\underline{a} = a$ for $a \in Lab$. Given $t : P \stackrel{\underline{a}}{月至} Q$, let $\underline{t} : Q \stackrel{\underline{\underline{a}}}{月至} P$ be the transition which reverses $t$. We define a labelling function $\ell$ from transitions to $Lab \cup \underline{Lab}$ by setting $\ell((P, \alpha, Q)) = \alpha$.

We let $\rho, \sigma, \dots$ range over finite sequences $\alpha_1 \dots \alpha_n$, with $\varepsilon$ representing the empty sequence. A *path* is a sequence of forward or reverse transitions of the form $P_0 \xrightarrow{\alpha_1} P_1 \dots \xrightarrow{\alpha_n} P_n$. We let $r, s, \dots$ range over paths. We may write $r : P \xrightarrow{\rho} * Q$ where the intermediate states are understood. On occasion we may refer to a path simply by its sequence of labels $\rho$. The concatenation of paths $r$ and $s$ is written $rs$. Given a path $r : P \xrightarrow{\rho} * Q$, the inverse path is $\underline{r} : Q \xrightarrow{\underline{\rho}} * P$ where $\underline{\rho} = \rho$ and $\underline{\alpha\rho} = \underline{\alpha}$. The length of a path $r$ (notated $|r|$) is the number of transitions in the path. Paths $P \xrightarrow{*} Q$ and $\underline{R} \xrightarrow{\underline{\underline{\sigma}}} * 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; similarly a path is *backward-only* if it contains no forward transitions. Sometimes we let $f, \dots$ and $b, \dots$ range over forward-only and backward-only paths, respectively; it will be clear from the context whether $b$ represents an action label or a path.

The irreversible processes in an LTS (Proc, Lab, →) are $\text{Irr} = \{P \in \text{Proc} : P \prec \prec\}$.

*A rooted path* is a path $P \xrightarrow{\rho} * Q$ such that $P \in \text{Irr}$.

In the following we consider LTSIs obtained by adding a notion of independence to combined LTSs as above. We call the result a *combined LTSI*.

*Remark 2.4.* From now on, unless stated otherwise, we consider a combined LTSI (Proc, Lab, →, t).
We will refer to it simply as an LTSI.

## 3 BASIC PROPERTIES

In this section we show that most of the properties in the reversibility literature (see, e.g., [13, 27, 30, 42]), 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 2.2 (LTS with independence).* We say that (Proc, Lab, →, t) is an LTS with independence (LTSI) if (Proc, Lab, →) is an LTS and t is an irreflexive symmetric binary relation on transitions.

In many cases (see Section 7), 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 processes, 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 [13, Lemma 6] holds. This does not hold in models of reversibility with control mechanisms [26] such as irreversible actions [14] or a rollback operator [25]. 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 [18, 30]. The present work helps with the first step.

*Definition 2.3 (Reverse and combined LTS).* Given an LTS (Proc, Lab, →), let the reverse LTS be (Proc, Lab, ⇄), where $P \stackrel{a}{月至} Q$ iff $Q \stackrel{a}{月至} P$. It is convenient to combine the two LTSs (forward and reverse): let the reverse labels be $\underline{Lab} = \{\underline{a} : a \in Lab\}$, and define the combined LTS to be $\rightarrow \subseteq \text{Proc} \times (Lab \cup \underline{Lab}) \times \text{Proc}$ by $P \stackrel{a}{月至} Q$ iff $P \stackrel{a}{月至} Q$ and $P \stackrel{a}{月至} Q$ iff $P \stackrel{a}{月至} Q$.

We stipulate that the union $Lab \cup \underline{Lab}$ is disjoint. We let $\alpha, \beta, \dots$ range over Lab $\cup \underline{Lab}$. For $\alpha \in Lab \cup \underline{Lab}$, the *underlying* action label $\text{und}(\alpha)$ is defined as $\text{und}(a) = a$ and $\text{und}(\underline{a}) = \underline{a}$. Let $\underline{a} = a$ for $a \in Lab$. Given $t : P \stackrel{\underline{a}}{月至} Q$, let $\underline{t} : Q \stackrel{\underline{\underline{a}}}{月至} P$ be the transition which reverses $t$. We define a labelling function $\ell$ from transitions to $Lab \cup \underline{Lab}$ by setting $\ell((P, \alpha, Q)) = \alpha$.

We let $\rho, \sigma, \dots$ range over finite sequences $\alpha_1 \dots \alpha_n$, with $\varepsilon$ representing the empty sequence. A *path* is a sequence of forward or reverse transitions of the form $P_0 \xrightarrow{\alpha_1} P_1 \dots \xrightarrow{\alpha_n} P_n$. We let $r, s, \dots$ range over paths. We may write $r : P \xrightarrow{\rho} * Q$ where the intermediate states are understood. On occasion we may refer to a path simply by its sequence of labels $\rho$. The concatenation of paths $r$ and $s$ is written $rs$. Given a path $r : P \xrightarrow{\rho} * Q$, the inverse path is $\underline{r} : Q \xrightarrow{\underline{\rho}} * P$ where $\underline{\rho} = \rho$ and $\underline{\alpha\rho} = \underline{\alpha}$. The length of a path $r$ (notated $|r|$) is the number of transitions in the path. Paths $P \xrightarrow{*} Q$ and $\underline{R} \xrightarrow{\underline{\underline{\sigma}}} * 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; similarly a path is *backward-only* if it contains no forward transitions. Sometimes we let $f, \dots$ and $b, \dots$ range over forward-only and backward-only paths, respectively; it will be clear from the context whether $b$ represents an action label or a path.

The irreversible processes in an LTS (Proc, Lab, →) are $\text{Irr} = \{P \in \text{Proc} : P \prec \prec\}$.

*A rooted path* is a path $P \xrightarrow{\rho} * Q$ such that $P \in \text{Irr}$.

In the following we consider LTSIs obtained by adding a notion of independence to combined LTSs as above. We call the result a *combined LTSI*.

*Remark 2.4.* From now on, unless stated otherwise, we consider a combined LTSI (Proc, Lab, →, t).
We will refer to it simply as an LTSI.

## 3 BASIC PROPERTIES

In this section we show that most of the properties in the reversibility literature (see, e.g., [13, 27, 30, 42]), 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).* We say an LTSI satisfies:

**Square property (SP):** if whenever $t : P \xrightarrow{\alpha} Q$, $u : P \xrightarrow{\beta} R$ with $t \prec u$ then there are cofinal transitions $u' : Q \xrightarrow{\beta} S$ and $t' : R \xrightarrow{\alpha} S$;

**Backward transitions are independent (BTI):** if whenever $t : P \stackrel{a}{\rightleftharpoons} Q$ and $t' : P \stackrel{b}{\rightleftharpoons} Q'$ and $t \neq t'$ then $t \prec t'$;

**Well-founded (WF):** if there is no infinite reverse computation, i.e. we do not have $P_i$ (not necessarily distinct) such that $P_{i+1} \stackrel{a_i}{\rightarrow} P_i$ for all $i = 0, 1, \dots$.

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 [13, 27, 30], 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., [46] for finite state automata and [50] 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". We will show in Proposition 7.10 that the two definitions are equivalent when no transitions are independent, which is the common setting in sequential computing. Note that BTI and SP together rule out examples $a.0 \xrightarrow{a} 0$, $b.0 \xrightarrow{b} 0$ as well as $a.0 + b.0 \xrightarrow{a} 0$, $a.0 + b.0 \xrightarrow{b} 0$ from the Introduction. 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. WF rules out example $P \xrightarrow{a} P$ where $P = a.P$ from the Introduction.

Axioms SP and BTI are related to properties which are part of the definition of (occurrence) transition systems with independence in [47, Definitions 3.7, 4.1]. WF was used as an axiom in [41].

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

*Definition 3.2 (Causal equivalence, cf. [13, Definition 9]).* Consider an LTSI satisfying SP. Let $\approx$ be the smallest equivalence relation on paths closed under composition and satisfying:

(1) (swap) if $t : P \xrightarrow{\alpha} Q$, $u : P \xrightarrow{\beta} R$ are independent, and $u' : Q \xrightarrow{\beta} S$, $t' : R \xrightarrow{\alpha} S$ (which exist by SP) then $tu' \approx ut'$;

(2) (cancellation) $\underline{tt} \approx \varepsilon$ and $\underline{t}t \approx \varepsilon$.

We first consider the Parabolic Lemma [13, Lemma 10], which states that each path is causal equivalent to a backward path followed by a forward path.

*Definition 3.3. Parabolic Lemma property (PL):* for any path $r$ there are forward-only paths $s, s'$ such that $r \approx \underline{s}s'$ and $|s| + |s'| \le |r|$.

**PROPOSITION 3.4.** *Suppose an LTSI satisfies BTI and SP. Then PL holds.*

**PROOF.** Suppose BTI and SP hold. Define a function on paths as follows: $d(r)$ is the number of pairs of forward transitions $(t, u)$ such that $t$ occurs in any position to the left of $u$ in $r$. We say $r$ is parabolic iff $d(r) = 0$. We have to show that each path is causal equivalent to a parabolic one.

Suppose $d(r) > 0$. We show that there is $s \approx r$ with $|s| \le |r|$ and $d(s) < d(r)$. Since $d(r) > 0$, we have $r = s_1 \underline{t} u \underline{s_2}$ with $s_1 : P \xrightarrow{\sigma_1} R$, $t : R \xrightarrow{\sigma_1} S$, $u : S \xrightarrow{\sigma_2} T$ and $s_2 : T \xrightarrow{\sigma_2} Q$. If $t = u$, then we obtain
*Definition 3.1 (Basic axioms).* We say an LTSI satisfies:

**Square property (SP):** if whenever $t : P \xrightarrow{\alpha} Q$, $u : P \xrightarrow{\beta} R$ with $t \prec u$ then there are cofinal transitions $u' : Q \xrightarrow{\beta} S$ and $t' : R \xrightarrow{\alpha} S$;

**Backward transitions are independent (BTI):** if whenever $t : P \stackrel{a}{\rightleftharpoons} Q$ and $t' : P \stackrel{b}{\rightleftharpoons} Q'$ and $t \neq t'$ then $t \prec t'$;

**Well-founded (WF):** if there is no infinite reverse computation, i.e. we do not have $P_i$ (not necessarily distinct) such that $P_{i+1} \stackrel{a_i}{\rightarrow} P_i$ for all $i = 0, 1, \dots$.

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 [13, 27, 30], 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., [46] for finite state automata and [50] 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". We will show in Proposition 7.10 that the two definitions are equivalent when no transitions are independent, which is the common setting in sequential computing. Note that BTI and SP together rule out examples $a.0 \xrightarrow{a} 0$, $b.0 \xrightarrow{b} 0$ as well as $a.0 + b.0 \xrightarrow{a} 0$, $a.0 + b.0 \xrightarrow{b} 0$ from the Introduction. 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. WF rules out example $P \xrightarrow{a} P$ where $P = a.P$ from the Introduction.

Axioms SP and BTI are related to properties which are part of the definition of (occurrence) transition systems with independence in [47, Definitions 3.7, 4.1]. WF was used as an axiom in [41].

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

*Definition 3.2 (Causal equivalence, cf. [13, Definition 9]).* Consider an LTSI satisfying SP. Let $\approx$ be the smallest equivalence relation on paths closed under composition and satisfying:

(1) (swap) if $t : P \xrightarrow{\alpha} Q$, $u : P \xrightarrow{\beta} R$ are independent, and $u' : Q \xrightarrow{\beta} S$, $t' : R \xrightarrow{\alpha} S$ (which exist by SP) then $tu' \approx ut'$;

(2) (cancellation) $tt \approx \varepsilon$ and $\underline{t}t \approx \varepsilon$.

We first consider the Parabolic Lemma [13, Lemma 10], which states that each path is causal equivalent to a backward path followed by a forward path.

*Definition 3.3. Parabolic Lemma property (PL):* for any path $r$ there are forward-only paths $s, s'$ such that $r \approx \underline{s}s'$ and $|s| + |s'| \le |r|$.

**PROPOSITION 3.4.** *Suppose an LTSI satisfies BTI and SP. Then PL holds.*

**PROOF.** Suppose BTI and SP hold. Define a function on paths as follows: $d(r)$ is the number of pairs of forward transitions $(t, u)$ such that $t$ occurs in any position to the left of $u$ in $r$. We say $r$ is parabolic iff $d(r) = 0$. We have to show that each path is causal equivalent to a parabolic one.

Suppose $d(r) > 0$. We show that there is $s \approx r$ with $|s| \le |r|$ and $d(s) < d(r)$. Since $d(r) > 0$, we have $r = s_1 \underline{t} u \underline{s_2}$ with $s_1 : P \xrightarrow{\sigma_1} R$, $t : R \xrightarrow{\sigma_1} S$, $u : S \xrightarrow{\sigma_2} T$ and $s_2 : T \xrightarrow{\sigma_2} Q$. If $t = u$, then we obtain
<figure><img src="image_2.png" /><figcaption>Fig. 2. Proof of Proposition 3.4, case $t \neq u$.</figcaption></figure>

$r = s_1 t u s_2 \approx s_1 s_2$. Clearly $r \approx s_1 s_2$ with $|s_1 s_2| < |r|$ and $d(s_1 s_2) < d(r)$. So suppose $t \neq u$. By BTI we have $\underline{t} \prec \underline{u}$. By SP there are $S'$ and transitions $u' : S' \xrightarrow{b} R$, $t' : S' \xrightarrow{a} T$. See Figure 2. Then $\underline{t} \underline{u}' \approx \underline{u} \underline{t}'$. Hence, $r = s_1 t \underline{u} s_2 \approx s_1 \underline{t} \underline{u} \underline{t}' s_2 \approx s_1 \underline{t} \underline{u} \underline{t}' s_2 \approx s_1 \underline{u}' \underline{t}' s_2 = s$ as required. Given that $|s_1 \underline{u}' \underline{t}' s_2| = |r|$ and $d(s_1 \underline{u}' \underline{t}' s_2) = d(r) - 1$ the thesis follows. $\square$

The proof of Proposition 3.4 is very similar to that of [13, 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 forwards-reachable states in a different order. This is relevant, e.g., in reversible debugging of concurrent systems [17, 30], where one wants to find bugs that actually occur in forward-only computations.

**COROLLARY 3.5.** *Suppose an LTSI satisfies PL. If a process *P* is reachable from some irreversible process *Q*, then it is also forward reachable from *Q*.*

**PROOF.** By hypothesis, there is some path $r : Q \to_* P$. Thanks to PL, there are forward-only paths $s, s'$ such that $\underline{s} \underline{s}' : Q \to_* P$. Since $Q$ is irreversible, $s = \varepsilon$, hence $s' : Q \to_* P$ as desired. $\square$

When WF and PL hold, each process is reachable from a unique irreversible process.

**PROPOSITION 3.6.** *Suppose an LTSI satisfies WF and PL. For any process *P* there is a unique irreversible process *I* such that *P* is reachable from *I*.*

**PROOF.** Let $P$ be any process. We use WF to deduce that there is an irreversible process $I$ such that $P$ is (forward) reachable from $I$ via some path $r$. Suppose now that $I'$ is irreversible and there is a path $r'$ from $I'$ to $P$. Then $r' \underline{r} : I' \to_* I$. By PL there are forward-only paths $s, s'$ such that $\underline{s} \underline{s}' : I' \to_* I$. But since $I$ and $I'$ are irreversible, both $s = \varepsilon$ and $s' = \varepsilon$. Hence $I' = I$ as required. $\square$

We now move to causal consistency [13, Theorem 1].

**Definition 3.7.** *Causal Consistency (CC):* if $r$ and $s$ are coinital and cofinal paths then $r \approx 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 coinital 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, such as the one of [13, Theorem 1] for RCCS and the one of [30, Theorem 21] for reversible Erlang.

**PROPOSITION 3.8.** *Suppose an LTSI satisfies WF and PL. Then CC holds.*
<figure><img src="image_3.png" /><figcaption>Fig. 2. Proof of Proposition 3.4, case $t \neq u$.</figcaption></figure>

$r = s_1 t u s_2 \approx s_1 s_2$. Clearly $r \approx s_1 s_2$ with $|s_1 s_2| < |r|$ and $d(s_1 s_2) < d(r)$. So suppose $t \neq u$. By BTI we have $\underline{t} \prec \underline{u}$. By SP there are $S'$ and transitions $u' : S' \xrightarrow{b} R$, $t' : S' \xrightarrow{a} T$. See Figure 2. Then $\underline{t} \underline{u}' \approx \underline{u} \underline{t}'$. Hence, $r = s_1 t \underline{u} s_2 \approx s_1 \underline{t} \underline{u} \underline{t}' s_2 \approx s_1 \underline{t} \underline{u} \underline{t}' s_2 \approx s_1 \underline{u}' \underline{t}' s_2 = s$ as required. Given that $|s_1 \underline{u}' \underline{t}' s_2| = |r|$ and $d(s_1 \underline{u}' \underline{t}' s_2) = d(r) - 1$ the thesis follows. $\square$

The proof of Proposition 3.4 is very similar to that of [13, 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 forwards-reachable states in a different order. This is relevant, e.g., in reversible debugging of concurrent systems [17, 30], where one wants to find bugs that actually occur in forward-only computations.

**COROLLARY 3.5.** *Suppose an LTSI satisfies PL. If a process *P* is reachable from some irreversible process *Q*, then it is also forward reachable from *Q*.*

**PROOF.** By hypothesis, there is some path $r : Q \to_* P$. Thanks to PL, there are forward-only paths $s, s'$ such that $\underline{s} \underline{s}' : Q \to_* P$. Since $Q$ is irreversible, $s = \varepsilon$, hence $s' : Q \to_* P$ as desired. $\square$

When WF and PL hold, each process is reachable from a unique irreversible process.

**PROPOSITION 3.6.** *Suppose an LTSI satisfies WF and PL. For any process *P* there is a unique irreversible process *I* such that *P* is reachable from *I*.*

**PROOF.** Let $P$ be any process. We use WF to deduce that there is an irreversible process $I$ such that $P$ is (forward) reachable from $I$ via some path $r$. Suppose now that $I'$ is irreversible and there is a path $r'$ from $I'$ to $P$. Then $r' \underline{r} : I' \to_* I$. By PL there are forward-only paths $s, s'$ such that $\underline{s} \underline{s}' : I' \to_* I$. But since $I$ and $I'$ are irreversible, both $s = \varepsilon$ and $s' = \varepsilon$. Hence $I' = I$ as required. $\square$

We now move to causal consistency [13, Theorem 1].

**Definition 3.7.** *Causal Consistency (CC):* if $r$ and $s$ are coinital and cofinal paths then $r \approx 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 coinital 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, such as the one of [13, Theorem 1] for RCCS and the one of [30, Theorem 21] for reversible Erlang.

**PROPOSITION 3.8.** *Suppose an LTSI satisfies WF and PL. Then CC holds.*
**PROOF.** Let $r : P \xrightarrow{\rho} * Q$ and $r' : P \xrightarrow{\rho'} * Q$. Using WF, let $I, s$ be such that $s : I \xrightarrow{\sigma} * P, I \in \text{Irr}$. Now $sr_{\underline{s}r'}$ 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 \approx sr_{\underline{s}r'}$. But $I \in \text{Irr}$ and so $r_1 = \varepsilon$ and $r_2 = \varepsilon$. Thus $\varepsilon \approx sr_{\underline{s}r'}$, so that $sr \approx sr'$ and (by composing with $\underline{s}$ on the left) $r \approx r'$ as required. □

Causal equivalent computations are strongly related in terms of the number of transitions with a given label they contain.

**PROPOSITION 3.9.** If $r \approx s$ then for any action *a* the number of *a*-transitions in *r* is the same as in *s*, where we count reverse transitions negatively.

**PROOF.** Straightforward, by induction on the derivation of $r \approx s$. □

*Remark 3.10.* One consequence of Proposition 3.9 is that if $r \approx s$ and $r$ and $s$ are both forward-only, then $|r| = |s|$.

Causal consistency implies the unique transition property.

**Definition 3.11.** *Unique transition (UT)*: if either $P \xrightarrow{a} Q$ and $P \xrightarrow{b} Q$ or $P \xrightarrow{a} Q$ and $P \xrightarrow{b} Q$ then $a = b$.

**COROLLARY 3.12.** If an LTSI satisfies CC then it satisfies UT.

**PROOF.** Since $P \xrightarrow{a} Q$ and $P \xrightarrow{b} Q$ are coinitial and cofinal then they are causal equivalent. By Proposition 3.9 the counting of actions should be the same, hence $a = b$. □

UT was shown in the forward-only setting of occurrence TSIs in [47, Corollary 4.4]; it was taken as an axiom in [41].

**Example 3.13 (PL alone does not imply WF or CC).** Consider the LTSI with states $P_i$ for $i = 0, 1, \dots$ and transitions $t_i : P_{i+1} \xrightarrow{a} P_i, u_i : P_{i+1} \xrightarrow{b} P_i$ with $a \neq b$ and $t_i \prec 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 \neq b$, so that UT fails, and hence CC fails using Corollary 3.12. Note that the *ab diamonds* here have the same side states so are degenerate (cf. Lemma 4.7). ◦

We have seen that SP is assumed when defining causal equivalence $\approx$. Assuming SP, we give a diagram (Figure 3) to show implications between the remaining two axioms presented so far (BTI, WF) and the two main properties introduced so far (PL, CC). We remark that the implications shown are strict (reverse implication does not hold). We provide below counterexamples showing strictness of implications:

**Example 3.14 (SP, WF and CC do not imply PL).** Consider the LTSI with states $P, Q, R$ and transitions $t : P \xrightarrow{a} R, u : Q \xrightarrow{b} R$, with an empty independence relation. Then clearly BTI and PL fail. However SP, WF and CC (and therefore UT) hold.

For CC, note that we can use cancellation to reduce each path to a unique shortest normal form with respect to $\approx$. There are various cases to check, depending on the initial and final states of the path, both ranging over $P, Q, R$. Let $r : R \xrightarrow{\rho} * R$ be any path from $R$ to $R$. If $r$ is non-empty, it must be of the form either $r = \underline{t}tr'$ or $r = \underline{u}ur''$. We can use cancellation to get either $r \approx r'$ or $r \approx r''$. Iterating the argument we see that $r \approx \varepsilon$. Now let $r : P \xrightarrow{\rho} * R$ be any path from $P$ to $R$. Then $r = tr'$ where $r'$ is a path from $R$ to $R$. Hence $r \approx t$. Now let $r : P \xrightarrow{\rho} * P$ be any path from $P$ to $P$. Then $r = tr'\underline{t}$ where $r'$ is a path from $R$ to $R$. Hence $r \approx \underline{t}t \approx \varepsilon$. Next let $r : P \xrightarrow{\rho} * Q$ be any path from $P$ to $Q$. Then $r = tr'\underline{u}$ where $r'$ is a path from $R$ to $R$. Hence $r \approx \underline{t}u$. The remaining cases are similar. ◦
<figure><img src="image_3.png" /><figcaption>Fig. 3. Implications between the main properties discussed in Section 3. We assume SP throughout.</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>Fig. 4. Rotations within a diamond (Example 3.16).</figcaption></figure>

**Example 3.15 (SP, WF, PL and CC do not imply BTI).** Consider the LTSI with states *P*, *Q*, *R*, *S* and transitions *t*: *P* $\stackrel{a}{\rightarrow}$ *Q*, *u*: *P* $\stackrel{b}{\rightarrow}$ *R*, *t'*: *R* $\stackrel{a}{\rightarrow}$ *S* and *u'*: *Q* $\stackrel{b}{\rightarrow}$ *S*, with *t* ≀≀ *u*. Then BTI fails for *t'* and *u'*. However SP, WF and PL hold, and therefore CC also holds.

We show PL. As in the proof of Proposition 3.4, for a path $r$ let $d(r)$ be the number of pairs of forward transitions $(t, u)$ such that $t$ occurs to the left of $\underline{u}$ in $r$. Then $r$ is parabolic iff $d(r) = 0$.

Suppose $d(r) > 0$. We show that there is $s \approx r$ with $|s| \le |r|$ and $d(s) < d(r)$. Since $d(r) > 0$, we have $r = s_1 t'' \underline{u''} s_2$. If $t'' = u''$, then we can use cancellation as in the proof of Proposition 3.4. So suppose $t'' \ne u''$. Since the target of $t''$ must be the same as the source of $u''$, the only possibilities are $t'' = t'$, $u'' = u'$ or dually $t'' = u', u'' = t'$. We consider $t'' = t'$, $u'' = u'$; the other case is similar. So $r = s_1 t' \underline{u}' s_2$. Since $t \triangleleft u$ we have $tu' \approx ut'$. Hence $\underline{u}tu'\underline{u}' \approx \underline{u}ut'\underline{u}'$, and so $\underline{u}t \approx t'\underline{u}'$. So $r \approx s = s_1 \underline{u}ts_2$ and $\overline{d(s)} = d(r) - 1$, $|s| = |r|$. ◇

**Example 3.16 (SP and WF do not imply CC (or PL)).** Consider the LTSI of Example 3.15, but without $t \triangleleft u$. Clearly SP and WF hold. However CC fails, since there are paths $tu'$ and $ut'$ from *P* to *S*, but $tu' \not\approx ut'$. To see this, imagine that the four transitions of the diamond correspond to rotations around the centre of the diamond (see Figure 4). Measuring anti-clockwise rotation in radians we see that *t* and *u'* each give a rotation of $-\pi/2$, while *u* and *t'* each yield $+\pi/2$. Let us define the rotation of a path to be the sum of the rotations of its transitions. Path $tu'$ has rotation $-\pi$ while $ut'$ has $+\pi$. Since there are no independent transitions, the only operation of causal equivalence we can perform is to use $t\underline{t} \approx \epsilon$. This clearly preserves the rotation of a path. Hence $tu' \not\approx ut'$ as required.
<figure><img src="image_4.png" /><figcaption>Fig. 3. Implications between the main properties discussed in Section 3. We assume SP throughout.</figcaption></figure>

<figure><img src="image_5.png" /><figcaption>Fig. 4. Rotations within a diamond (Example 3.16).</figcaption></figure>

**Example 3.15 (SP, WF, PL and CC do not imply BTI).** Consider the LTSI with states *P*, *Q*, *R*, *S* and transitions *t*: *P* $\stackrel{a}{\to}$ *Q*, *u*: *P* $\stackrel{b}{\to}$ *R*, *t'*: *R* $\stackrel{a}{\to}$ *S* and *u'*: *Q* $\stackrel{b}{\to}$ *S*, with *t* ≀≀ *u*. Then BTI fails for *t'* and *u'*. However SP, WF and PL hold, and therefore CC also holds.

We show PL. As in the proof of Proposition 3.4, for a path $r$ let $d(r)$ be the number of pairs of forward transitions $(t, u)$ such that $t$ occurs to the left of $\underline{u}$ in $r$. Then $r$ is parabolic iff $d(r) = 0$.

Suppose $d(r) > 0$. We show that there is $s \approx r$ with $|s| \le |r|$ and $d(s) < d(r)$. Since $d(r) > 0$, we have $r = s_1 t'' \underline{u''} s_2$. If $t'' = u''$, then we can use cancellation as in the proof of Proposition 3.4. So suppose $t'' \ne u''$. Since the target of $t''$ must be the same as the source of $u''$, the only possibilities are $t'' = t'$, $u'' = u'$ or dually $t'' = u', u'' = t'$. We consider $t'' = t'$, $u'' = u'$; the other case is similar. So $r = s_1 t' \underline{u}' s_2$. Since $t \ı u$ we have $tu' \approx ut'$. Hence $\underline{tu'}\underline{u}' \approx \underline{u}u'\underline{u}'$, and so $\underline{u}t \approx t'\underline{u}'$. So $r \approx s = s_1 \underline{u}t s_2$ and $\underline{d}(s) = d(r) - 1$, $|s| = |r|$. ◇

**Example 3.16 (SP and WF do not imply CC (or PL)).** Consider the LTSI of Example 3.15, but without $t \ı u$. Clearly SP and WF hold. However CC fails, since there are paths $tu'$ and $ut'$ from *P* to *S*, but $tu' \not\approx ut'$. To see this, imagine that the four transitions of the diamond correspond to rotations around the centre of the diamond (see Figure 4). Measuring anti-clockwise rotation in radians we see that *t* and *u'* each give a rotation of $-\pi/2$, while *u* and *t'* each yield $+\pi/2$. Let us define the rotation of a path to be the sum of the rotations of its transitions. Path $tu'$ has rotation $-\pi$ while $ut'$ has $+\pi$. Since there are no independent transitions, the only operation of causal equivalence we can perform is to use $t\underline{t} \approx \epsilon$. This clearly preserves the rotation of a path. Hence $tu' \not\approx ut'$ as required.
PL does not hold either, otherwise CC would follow from Proposition 3.8. ◇

*Example 3.17 (SP, BTI and CC do not imply WF).* Consider the LTSI with states $P_i$ for $i = 0, 1, \dots$ and transitions $t_i : P_{i+1} \xrightarrow{a} P_i$. Clearly WF does not hold. However SP, BTI (and hence PL) hold; also CC (and hence UT) hold, noting that any path is causally equivalent to a path which is entirely forward or entirely reverse. ◇

# 4 EVENTS

In order to define and study causal safety and liveness (Section 5), we first need the concept of event (once further axioms are introduced, we will be able to simplify the definition below, see Definition 4.8).

*Definition 4.1 (Event, general definition).* Consider an LTSI. Let $\sim$ be the smallest equivalence relation satisfying: if $t: P \xrightarrow{\alpha} Q, u: P \xrightarrow{\beta} R, u': Q \xrightarrow{\beta} S, t': R \xrightarrow{\alpha} S$, and $t \prec u, \underline{u} \prec t', \underline{t'} \prec \underline{u'}, u' \prec \underline{t}$, and

* $Q \neq R$ if $\alpha$ and $\beta$ are both forwards or both backwards;

* $P \neq S$ otherwise;

then $t \sim t'$. The equivalence classes of transitions, written $[t]$ or $[P, \alpha, Q]$, are the *events*. We say that an event is *forward* if it is the equivalence class of a forward transition; similarly for *reverse* events. Given an event $e = [t]$ we let $\underline{e} = [\underline{t}]$. Also, we let $\text{und}(e) = e$ if $e$ is forward, $\text{und}(e) = \underline{e}$ if $e$ is backward.

Intuitively, events are the equivalence classes generated by equating transitions on the opposite sides of commuting squares. Events are introduced as a derived notion in an LTS with independence in [47], in the context of forward-only computation. We have changed their definition by using coinital independence at all corners of the diamond, yielding rotational symmetry. This reflects our view that forward and backward transitions have equal status.

The labelling function $\ell$ can be extended to events since the label does not depend on the choice of the representative inside the equivalence class.

## 4.1 Pre-reversible LTSIs

Our definition of event can be simplified if the LTSI, and independence in particular, are well-behaved. Thus, we now add a further axiom related to independence. This leads us to pre-reversible LTSIs.

*Definition 4.2. Propagation of coinital independence (PCI)<fnref n="2" />:* if $t: P \xrightarrow{\alpha} Q, u: P \xrightarrow{\beta} R, u': Q \xrightarrow{\beta} S$ and $t' : R \xrightarrow{\alpha} S$ with $t \prec u$, then $u' \prec \underline{t}$.

PCI 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 (Pre-reversible LTSI).* If an LTSI satisfies axioms SP, BTI, WF and PCI, 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 (Lemma 4.12). Pre-reversible axioms are separated from further axioms by a dashed line in Table 1.

A first consequence of PCI is that coinital transitions with labels $\alpha$ and $\underline{\alpha}$ are not independent.

<footnote n="2">²PCI was called CPI (coinital propagation of independence) in [31]; we changed the terminology following a suggestion from Marco Bernardo to better match the intuition.</footnote>
PL does not hold either, otherwise CC would follow from Proposition 3.8. ◇

*Example 3.17 (SP, BTI and CC do not imply WF).* Consider the LTSI with states $P_i$ for $i = 0, 1, \dots$ and transitions $t_i : P_{i+1} \xrightarrow{a} P_i$. Clearly WF does not hold. However SP, BTI (and hence PL) hold; also CC (and hence UT) hold, noting that any path is causally equivalent to a path which is entirely forward or entirely reverse. ◇

# 4 EVENTS

In order to define and study causal safety and liveness (Section 5), we first need the concept of event (once further axioms are introduced, we will be able to simplify the definition below, see Definition 4.8).

*Definition 4.1 (Event, general definition).* Consider an LTSI. Let $\sim$ be the smallest equivalence relation satisfying: if $t: P \xrightarrow{\alpha} Q, u: P \xrightarrow{\beta} R, u': Q \xrightarrow{\beta} S, t': R \xrightarrow{\alpha} S$, and $t \prec u, \underline{u} \prec t', \underline{t'} \prec \underline{u'}, u' \prec \underline{t}$, and

* $Q \neq R$ if $\alpha$ and $\beta$ are both forwards or both backwards;

* $P \neq S$ otherwise;

then $t \sim t'$. The equivalence classes of transitions, written $[t]$ or $[P, \alpha, Q]$, are the *events*. We say that an event is *forward* if it is the equivalence class of a forward transition; similarly for *reverse* events. Given an event $e = [t]$ we let $\underline{e} = [\underline{t}]$. Also, we let $\text{und}(e) = e$ if $e$ is forward, $\text{und}(e) = \underline{e}$ if $e$ is backward.

Intuitively, events are the equivalence classes generated by equating transitions on the opposite sides of commuting squares. Events are introduced as a derived notion in an LTS with independence in [47], 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.

The labelling function $\ell$ can be extended to events since the label does not depend on the choice of the representative inside the equivalence class.

## 4.1 Pre-reversible LTSIs

Our definition of event can be simplified if the LTSI, and independence in particular, are well-behaved. Thus, we now add a further axiom related to independence. This leads us to pre-reversible LTSIs.

*Definition 4.2. Propagation of coinitial independence (PCI)<fnref n="2" />:* if $t: P \xrightarrow{\alpha} Q, u: P \xrightarrow{\beta} R, u': Q \xrightarrow{\beta} S$ and $t' : R \xrightarrow{\alpha} S$ with $t \prec u$, then $u' \prec \underline{t}$.

PCI 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 (Pre-reversible LTSI).* If an LTSI satisfies axioms SP, BTI, WF and PCI, 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 (Lemma 4.12). Pre-reversible axioms are separated from further axioms by a dashed line in Table 1.

A first consequence of PCI is that coinitial transitions with labels $\alpha$ and $\underline{\alpha}$ are not independent.

<footnote n="2">²PCI was called CPI (coinitial propagation of independence) in [31]; we changed the terminology following a suggestion from Marco Bernardo to better match the intuition.</footnote>
**LEMMA 4.4.** *Suppose that an LTSI satisfies PCI. If $t: P \xrightarrow{\alpha} Q$ and $u: P \xrightarrow{\alpha} R$ are coinitial transitions, then $t \prec u$.*

**PROOF.** Suppose that $t: P \xrightarrow{\alpha} Q$ and $u: P \xrightarrow{\alpha} R$ are independent. Consider the degenerate diamond with two copies of $P$ and transitions $t, u, \dot{t}, \underline{u}$. By applying PCI we deduce $\dot{t} \prec \underline{t}$, which contradicts irreflexivity of $\prec$. $\square$

Additionally, we cannot have two different coinitial backward transitions with the same label.

**Definition 4.5. Backward label determinism (BLD):** if $t: P \stackrel{a}{\rightleftharpoons} Q$ and $u: P \stackrel{a}{\rightleftharpoons} R$ are coinitial backward transitions with the same label then $t = u$.

**PROPOSITION 4.6.** *Suppose that an LTSI satisfies SP, BTI and PCI. Then it satisfies BLD.*

**PROOF.** Suppose $t: P \stackrel{a}{\rightleftharpoons} Q$ and $u: P \stackrel{a}{\rightleftharpoons} R$. Then if $t \neq u$ we have $t \prec u$ by BTI. We can complete a diamond with $Q \stackrel{a}{\rightleftharpoons} S, R \stackrel{a}{\rightleftharpoons} S$ by SP. But then $Q \xrightarrow{\beta} P$ and $Q \stackrel{a}{\rightleftharpoons} S$ are independent by PCI. This is a contradiction of Lemma 4.4. $\square$

A consequence of Lemma 4.4 is that an LTSI satisfying BTI and PCI cannot include a diamond $P \xrightarrow{\alpha} Q \xrightarrow{\alpha} S, P \xrightarrow{\alpha} R \xrightarrow{\alpha} S$ where all four transitions have the same label. This can be seen as ruling out *autoconcurrency* [4].

The following non-degeneracy property was shown for occurrence transition systems with independence in [47, page 312], which considers forward transitions only. We have to cope with backward as well as forward transitions.

**LEMMA 4.7.** *Suppose that an LTSI is pre-reversible. If we have a diamond $t: P \xrightarrow{\alpha} Q, u: P \xrightarrow{\beta} R$ with $t \prec u$ together with cofinal transitions $u': Q \xrightarrow{\beta} S$ and $t': R \xrightarrow{\alpha} S$, then the diamond is non-degenerate, meaning that $P, Q, R, S$ are distinct states.*

**PROOF.** We note that CC holds; hence UT holds thanks to Corollary 3.12. By WF we see that $P \neq Q \neq S \neq R \neq P$. It remains to show $Q \neq R$ and $P \neq S$.

Suppose $Q = R$. By $t \prec u$ we know $t \neq u$. So $\alpha \neq \beta$. But if $\alpha$ and $\beta$ are both forward or both backward this is impossible by UT. If one is forward and the other is backward then this is impossible by WF. Hence $Q \neq R$.

Suppose $P = S$. If $\alpha$ and $\beta$ are both forward or both backward this is impossible by WF. If one is forward and the other is backward then by UT this implies that $\alpha = \beta$. Then $t \prec u$ by Lemma 4.4, which is a contradiction. Hence $P \neq S$. $\square$

If an LTSI is pre-reversible then by Lemma 4.7 and the use of PCI we can simplify the statement of Definition 4.1 to:

**Definition 4.8 (Event, simplified definition).** Consider a pre-reversible LTSI. Let $\sim$ be the smallest equivalence relation satisfying: if $t: P \xrightarrow{\alpha} Q, u: P \xrightarrow{\beta} R, u': Q \xrightarrow{\beta} S, t': R \xrightarrow{\alpha} S$, and $t \prec u$, then $t \sim t'$.

We are now able to show independence of diamonds (ID), which can be seen as dual of SP.

**Definition 4.9. Independence of diamonds (ID):** if we have a diamond $t: P \xrightarrow{\alpha} Q, u: P \xrightarrow{\beta} R, u': Q \xrightarrow{\beta} S$ and $t': R \xrightarrow{\alpha} S$, with

* $Q \neq R$ if $\alpha$ and $\beta$ are both forwards or both backwards;

* $P \neq S$ otherwise;
**LEMMA 4.4.** *Suppose that an LTSI satisfies PCI. If $t: P \xrightarrow{\alpha} Q$ and $u: P \xrightarrow{\alpha} R$ are coinitial transitions, then $t \prec u$.*

**PROOF.** Suppose that $t: P \xrightarrow{\alpha} Q$ and $u: P \xrightarrow{\alpha} R$ are independent. Consider the degenerate diamond with two copies of $P$ and transitions $t, u, \dot{t}, \underline{u}$. By applying PCI we deduce $\dot{t} \prec \underline{t}$, which contradicts irreflexivity of $\prec$. □

Additionally, we cannot have two different coinitial backward transitions with the same label.

**Definition 4.5. Backward label determinism (BLD):** if $t: P \stackrel{a}{\rightleftharpoons} Q$ and $u: P \stackrel{a}{\rightleftharpoons} R$ are coinitial backward transitions with the same label then $t = u$.

**PROPOSITION 4.6.** *Suppose that an LTSI satisfies SP, BTI and PCI. Then it satisfies BLD.*

**PROOF.** Suppose $t: P \stackrel{a}{\rightleftharpoons} Q$ and $u: P \stackrel{a}{\rightleftharpoons} R$. Then if $t \neq u$ we have $t \prec u$ by BTI. We can complete a diamond with $Q \stackrel{a}{\rightleftharpoons} S, R \stackrel{a}{\rightleftharpoons} S$ by SP. But then $Q \xrightarrow{\beta} P$ and $Q \stackrel{a}{\rightleftharpoons} S$ are independent by PCI. This is a contradiction of Lemma 4.4. □

A consequence of Lemma 4.4 is that an LTSI satisfying BTI and PCI cannot include a diamond $P \xrightarrow{\alpha} Q \xrightarrow{\alpha} S, P \xrightarrow{\alpha} R \xrightarrow{\alpha} S$ where all four transitions have the same label. This can be seen as ruling out *autoconcurrency* [4].

The following non-degeneracy property was shown for occurrence transition systems with independence in [47, page 312], which considers forward transitions only. We have to cope with backward as well as forward transitions.

**LEMMA 4.7.** *Suppose that an LTSI is pre-reversible. If we have a diamond $t: P \xrightarrow{\alpha} Q, u: P \xrightarrow{\beta} R$ with $t \prec u$ together with cofinal transitions $u': Q \xrightarrow{\beta} S$ and $t': R \xrightarrow{\alpha} S$, then the diamond is non-degenerate, meaning that $P, Q, R, S$ are distinct states.*

**PROOF.** We note that CC holds; hence UT holds thanks to Corollary 3.12. By WF we see that $P \neq Q \neq S \neq R \neq P$. It remains to show $Q \neq R$ and $P \neq S$.

Suppose $Q = R$. By $t \prec u$ we know $t \neq u$. So $\alpha \neq \beta$. But if $\alpha$ and $\beta$ are both forward or both backward this is impossible by UT. If one is forward and the other is backward then this is impossible by WF. Hence $Q \neq R$.

Suppose $P = S$. If $\alpha$ and $\beta$ are both forward or both backward this is impossible by WF. If one is forward and the other is backward then by UT this implies that $\alpha = \beta$. Then $t \prec u$ by Lemma 4.4, which is a contradiction. Hence $P \neq S$. □

If an LTSI is pre-reversible then by Lemma 4.7 and the use of PCI we can simplify the statement of Definition 4.1 to:

**Definition 4.8 (Event, simplified definition).** Consider a pre-reversible LTSI. Let $\sim$ be the smallest equivalence relation satisfying: if $t: P \xrightarrow{\alpha} Q, u: P \xrightarrow{\beta} R, u': Q \xrightarrow{\beta} S, t': R \xrightarrow{\alpha} S$, and $t \prec u$, then $t \sim t'$.

We are now able to show independence of diamonds (ID), which can be seen as dual of SP.

**Definition 4.9. Independence of diamonds (ID):** if we have a diamond $t: P \xrightarrow{\alpha} Q, u: P \xrightarrow{\beta} R, u': Q \xrightarrow{\beta} S$ and $t': R \xrightarrow{\alpha} S$, with

* $Q \neq R$ if $\alpha$ and $\beta$ are both forwards or both backwards;

* $P \neq S$ otherwise;
then $t \prec u$.

**PROPOSITION 4.10.** If an LTSI satisfies BTI and PCI then it satisfies ID.

**PROOF.** Suppose we have a diamond $t: P \stackrel{\alpha}{\rightarrow} Q, u: P \stackrel{\beta}{\rightarrow} R, u': Q \stackrel{\beta}{\rightarrow} S$ and $t': R \stackrel{\alpha}{\rightarrow} S$, with

* $Q \neq R$ if $\alpha$ and $\beta$ are both forwards or both backwards;

* $P \neq S$ otherwise.

We must show $t \prec u$. There are various cases, depending on whether $\alpha$ and $\beta$ are forwards or backwards. If they are both forwards, then $Q \neq R$. Hence $t' \neq u'$ and by BTI we have $t' \prec u'$. By PCI, $u' \prec t$ and again by PCI $t \prec u$ as required. Other cases are similar. □

In the proof of the above proposition it must be the case that $\text{und}(\alpha) \neq \text{und}(\beta)$, or else we get a contradiction using Lemma 4.4.

## 4.2 Counting occurrences of events

We now consider the interaction between events and causal equivalence. We need some notation first.

**Definition 4.11.** Let $r$ be a path and $e$ be an event of the same LTSI. Let $\#(r, e)$ be the number of occurrences of transitions $t$ in $r$ such that $t \in e$, minus the number of occurrences of transitions $t$ in $r$ such that $t \in \underline{e}$. We define $\#(r, e)$ by induction on the length of $r$ as follows:

$$ \#(\varepsilon, e) = 0 \\ \#(tr, e) = \begin{cases} \#(r, e) + 1 & \text{if } [t] = e \\ \#(r, e) - 1 & \text{if } [t] = \underline{e} \\ \#(r, e) & \text{otherwise} \end{cases} $$

We now show that $\#(r, e)$ is invariant under causal equivalence.

**LEMMA 4.12.** Assume an LTSI is pre-reversible. Let $r \approx s$. Then for each event $e$ we have that $\#(r, e) = \#(s, e)$.

**PROOF.** We prove the thesis for $r$ and $s$ being derived by a single application of the axioms; the thesis will follow since equality is an equivalence relation.

If $r = r_1tu'r_2$ and $s = r_1ut'r_2$ then we have by definition of causal equivalence (Definition 3.2) that $t \prec u$. Hence, $[t] = [t']$ and $[u] = [u']$ using Definition 4.8. The thesis follows.

If $r = r_1t\underline{u}'r_2$ and $s = r_1r_2$ (the other case is analogous) then the contribution of $t$ and $\underline{t}$ to $\#(r, [t])$ (as well as to $\#(r, e)$ for $t \notin e$) is 0; hence the thesis follows. □

Lemma 4.12 generalises what was shown for the forward-only setting in [47, Corollary 4.3].

**PROPOSITION 4.13.** If an LTSI is pre-reversible, then for any rooted path $r$ and any forward event $e$ we have $\#(r, e) \ge 0$.

**PROOF.** Let $r$ be a rooted path. Using PL (Proposition 3.4), we obtain a coinitial and cofinal forward-only path $s$ such that $s \approx r$. Let $e$ be any forward event. Clearly $\#(s, e) \ge 0$. Hence $\#(r, e) \ge 0$ by Lemma 4.12. □

We can lift independence from transitions to events.

**Definition 4.14 (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 \prec t'$.
then $t \prec u$.

**PROPOSITION 4.10.** If an LTSI satisfies BTI and PCI then it satisfies ID.

**PROOF.** Suppose we have a diamond $t: P \stackrel{\alpha}{\rightarrow} Q, u: P \stackrel{\beta}{\rightarrow} R, u': Q \stackrel{\beta}{\rightarrow} S$ and $t': R \stackrel{\alpha}{\rightarrow} S$, with

* $Q \neq R$ if $\alpha$ and $\beta$ are both forwards or both backwards;

* $P \neq S$ otherwise.

We must show $t \prec u$. There are various cases, depending on whether $\alpha$ and $\beta$ are forwards or backwards. If they are both forwards, then $Q \neq R$. Hence $t' \neq u'$ and by BTI we have $t' \prec u'$. By PCI, $u' \prec t$ and again by PCI $t \prec u$ as required. Other cases are similar. □

In the proof of the above proposition it must be the case that $\mathrm{und}(\alpha) \neq \mathrm{und}(\beta)$, or else we get a contradiction using Lemma 4.4.

## 4.2 Counting occurrences of events

We now consider the interaction between events and causal equivalence. We need some notation first.

**Definition 4.11.** Let $r$ be a path and $e$ be an event of the same LTSI. Let $\#(r, e)$ be the number of occurrences of transitions $t$ in $r$ such that $t \in e$, minus the number of occurrences of transitions $t$ in $r$ such that $t \in \underline{e}$. We define $\#(r, e)$ by induction on the length of $r$ as follows:

$$ \#(\varepsilon, e) = 0 \\ \#(tr, e) = \begin{cases} \#(r, e) + 1 & \text{if } [t] = e \\ \#(r, e) - 1 & \text{if } [t] = \underline{e} \\ \#(r, e) & \text{otherwise} \end{cases} $$

We now show that $\#(r, e)$ is invariant under causal equivalence.

**LEMMA 4.12.** Assume an LTSI is pre-reversible. Let $r \approx s$. Then for each event $e$ we have that $\#(r, e) = \#(s, e)$.

**PROOF.** We prove the thesis for $r$ and $s$ being derived by a single application of the axioms; the thesis will follow since equality is an equivalence relation.

If $r = r_1tu'r_2$ and $s = r_1ut'r_2$ then we have by definition of causal equivalence (Definition 3.2) that $t \prec u$. Hence, $[t] = [t']$ and $[u] = [u']$ using Definition 4.8. The thesis follows.

If $r = r_1t\underline{u}'r_2$ and $s = r_1r_2$ (the other case is analogous) then the contribution of $t$ and $\underline{t}$ to $\#(r, [t])$ (as well as to $\#(r, e)$ for $t \notin e$) is 0; hence the thesis follows. □

Lemma 4.12 generalises what was shown for the forward-only setting in [47, Corollary 4.3].

**PROPOSITION 4.13.** If an LTSI is pre-reversible, then for any rooted path $r$ and any forward event $e$ we have $\#(r, e) \ge 0$.

**PROOF.** Let $r$ be a rooted path. Using PL (Proposition 3.4), we obtain a coinital and cofinal forward-only path $s$ such that $s \approx r$. Let $e$ be any forward event. Clearly $\#(s, e) \ge 0$. Hence $\#(r, e) \ge 0$ by Lemma 4.12. □

We can lift independence from transitions to events.

**Definition 4.14 (Coinitially independent events).** Let events $e, e'$ be coinitially independent, written $e$ ci $e'$, iff there are coinital transitions $t, t'$ such that $[t] = e, [t'] = e'$ and $t \prec t'$.
<figure><img src="image_5.png" /><figcaption>Fig. 5. The ladder of diamonds in the proof of Lemma 4.19.</figcaption></figure>

**LEMMA 4.15.** *Assume an LTSI is pre-reversible. If e ci e' then we have also e ci e'.*

**PROOF.** Suppose that $e \text{ ci } e'$. Then there are coinitial $t, u$ such that $[t] = e, [u] = e'$ and $t \ı u$. Use SP to complete a diamond with transitions $t' \sim t, u' \sim u$. By PCI we have $\underline{t} \ı \underline{u}'$. Hence $\underline{e} \text{ ci } e'$ as required. □

Thus in pre-reversible LTSIs, ci is fully determined just considering forward events. By Lemma 4.15, if we know $e \text{ ci } e'$ then we know und($e$) ci und($e'$).

**PROPOSITION 4.16.** *Assume an LTSI is pre-reversible. Then ci is irreflexive.*

**PROOF.** Suppose for a contradiction that $e \text{ ci } e$ for some event $e$. By Lemma 4.15, we can assume that $e$ is forward. Then there are coinitial transitions $t, u \in e$ such that $t \ı u$. We can use SP to complete a square with $t' \sim t$ and $u' \sim u$. This square is non-degenerate by Lemma 4.7. But now $\underline{t}'$ and $\underline{u}'$ are two distinct coinitial backward transitions with the same label, contradicting BLD (Proposition 4.6). □

We can slightly strengthen the previous result as follows:

**PROPOSITION 4.17.** *Assume an LTSI is pre-reversible. If $t: P \xrightarrow{\alpha} Q$ and $u: R \xrightarrow{\beta} S$ with $[t] \text{ ci } [u]$ then und($\alpha$) $\neq$ und($\beta$).*

**PROOF.** Similar to the proof of Proposition 4.16. □

In pre-reversible LTSIs each event can occur at most once in a rooted path.

**Definition 4.18.** **No repeated events (NRE):** for any rooted path $r$ and any forward event $e$ we have $\#(r, e) \le 1$.

In order to prove NRE we need the following lemmas.

**LEMMA 4.19 (LADDER LEMMA).** *Assume an LTSI is pre-reversible. Suppose that $t: P \xrightarrow{\alpha} Q$ and $t': P' \xrightarrow{\alpha} Q'$ with $t \sim t'$. Then there is a path $s$ from $Q$ to $Q'$ such that for all $u$ in $s$ we have $[t] \text{ ci } [u]$.*

**PROOF.** By the definition of $\sim$ there is a ladder of diamonds (see Figure 5) connecting $t$ to $t'$. This gives a path $s$ from $Q$ to $Q'$. Take any $u$ in $s$, and consider the diamond containing $u$. Let $u'$ be on the opposite side from $u$, so that $u' \sim u$, and let $t''$ be the rung nearest to $t$, so that $t \sim t''$. We have $t'' \ı u'$. Hence, the result follows. □

**LEMMA 4.20.** *Let $\mathcal{L}$ be a pre-reversible LTSI. Suppose $t: P \xrightarrow{\alpha} Q$ and $t': P' \xrightarrow{\alpha} Q'$ with $t \sim t'$, and suppose $r$ is a path from $Q$ to $Q'$. Then $\#(r, [t]) = 0$.*
<figure><img src="image_6.png" /><figcaption>Fig. 5. The ladder of diamonds in the proof of Lemma 4.19.</figcaption></figure>

**LEMMA 4.15.** *Assume an LTSI is pre-reversible. If e ci e' then we have also e ci e'.*

**PROOF.** Suppose that $e \text{ ci } e'$. Then there are coinitial $t, u$ such that $[t] = e, [u] = e'$ and $t \ı u$. Use SP to complete a diamond with transitions $t' \sim t, u' \sim u$. By PCI we have $\underline{t} \ı \underline{u}'$. Hence $\underline{e} \text{ ci } e'$ as required. □

Thus in pre-reversible LTSIs, ci is fully determined just considering forward events. By Lemma 4.15, if we know $e \text{ ci } e'$ then we know $\text{und}(e) \text{ ci und}(e')$.

**PROPOSITION 4.16.** *Assume an LTSI is pre-reversible. Then ci is irreflexive.*

**PROOF.** Suppose for a contradiction that $e \text{ ci } e$ for some event $e$. By Lemma 4.15, we can assume that $e$ is forward. Then there are coinitial transitions $t, u \in e$ such that $t \ı u$. We can use SP to complete a square with $t' \sim t$ and $u' \sim u$. This square is non-degenerate by Lemma 4.7. But now $\underline{t}'$ and $\underline{u}'$ are two distinct coinitial backward transitions with the same label, contradicting BLD (Proposition 4.6). □

We can slightly strengthen the previous result as follows:

**PROPOSITION 4.17.** *Assume an LTSI is pre-reversible. If $t: P \xrightarrow{\alpha} Q$ and $u: R \xrightarrow{\beta} S$ with $[t] \text{ ci } [u]$ then $\text{und}(\alpha) \neq \text{und}(\beta)$.*

**PROOF.** Similar to the proof of Proposition 4.16. □

In pre-reversible LTSIs each event can occur at most once in a rooted path.

**Definition 4.18.** **No repeated events (NRE):** for any rooted path $r$ and any forward event $e$ we have $\#(r, e) \le 1$.

In order to prove NRE we need the following lemmas.

**LEMMA 4.19 (LADDER LEMMA).** *Assume an LTSI is pre-reversible. Suppose that $t: P \xrightarrow{\alpha} Q$ and $t': P' \xrightarrow{\alpha} Q'$ with $t \sim t'$. Then there is a path $s$ from $Q$ to $Q'$ such that for all $u$ in $s$ we have $[t] \text{ ci } [u]$.*

**PROOF.** By the definition of $\sim$ there is a ladder of diamonds (see Figure 5) connecting $t$ to $t'$. This gives a path $s$ from $Q$ to $Q'$. Take any $u$ in $s$, and consider the diamond containing $u$. Let $u'$ be on the opposite side from $u$, so that $u' \sim u$, and let $t''$ be the rung nearest to $t$, so that $t \sim t''$. We have $t'' \ı u'$. Hence, the result follows. □

**LEMMA 4.20.** *Let $\mathcal{L}$ be a pre-reversible LTSI. Suppose $t: P \xrightarrow{\alpha} Q$ and $t': P' \xrightarrow{\alpha} Q'$ with $t \sim t'$, and suppose $r$ is a path from $Q$ to $Q'$. Then $\#(r, [t]) = 0$.*
<figure><img src="image_6.png" /><figcaption>Fig. 6. The LTSI in Example 4.22.</figcaption></figure>

PROOF. By Lemma 4.19 there is a path $s$ from $Q$ to $Q'$ such that for all $u$ in $s$ we have $[t]$ ci $[u]$. Let $\ell(u) = \beta$. By Proposition 4.17 we have und($\alpha$) $\neq$ und($\beta$). Hence $\#(s, [t]) = 0$, and by Lemma 4.12 $\#(r, [t]) = 0$ as required. □

PROPOSITION 4.21. If an LTSI is pre-reversible then it satisfies NRE.

PROOF. Let $e$ be a forward event and $r$ be a rooted path from $I$ to $R$, and suppose for a contradiction that $\#(r, e) > 1$. Using PL we can obtain a forward-only path $r'$ from $I$ to $R$ with $r \approx r'$. By Lemma 4.12, $\#(r', e) > 1$. Hence, $r'$ contains (at least) two transitions for $e$; let us denote them as $t: P \xrightarrow{a} Q$ and $t': P' \xrightarrow{a} Q'$. Without loss of generality, we assume that $t$ occurs before $t'$ in $r$. Let $r''$ be the portion of $r'$ from $Q$ to $P'$. By Lemma 4.20 applied to $t, t'$ and path $r''t'$ we have $\#(r''t', [t]) = 0$. This is a contradiction since $r''$ is forward-only. □

NRE was shown in the forward-only setting of occurrence transition systems with independence in [47, Corollary 4.6]. It was also shown in the reversible setting without independence in [41, Proposition 2.10].

*Example 4.22.* Consider the LTSI in Figure 6. Independence holds only between coinital transitions and is given by closing under BTI and propagating independence around the corners of diamonds as in PCI whenever possible. Note, however, that PCI does not hold, since we have coinital independent *a* and *a*-transitions, contradicting Lemma 4.4. On the other hand, in addition to BTI, axioms SP and WF hold, so that CC holds. All *a*-transitions belong to the same event, and all *b*-transitions belong to the same event. We have rooted paths where the same event is repeated, contradicting NRE. Note also that BLD fails and that ci is reflexive. ◇

## 4.3 Polychotomy

We now show what we call *polychotomy*, which states that if forward events do not cause each other and are not in conflict, then they must be independent. This will help us to relate the different notions of causal safety and liveness (Section 5). We first define causality and conflict relations on forward events.

*Definition 4.23 (Causality relation on forward events).* Let $e, e'$ be forward events of some LTSI. Let $e \le e'$ iff for all rooted paths $r$, if $\#(r, e') > 0$ then $\#(r, e) > 0$. As usual $e < e'$ means $e \le e'$ and $e \ne e'$. If $e < e'$ we say that $e$ is a *cause* of $e'$.

As expected, the causality relation is a partial ordering (i.e., a reflexive, transitive and antisymmetric relation).

LEMMA 4.24. If an LTSI is pre-reversible then $\le$ is a partial ordering on events.

PROOF. Reflexivity and transitivity are immediate. For antisymmetry, suppose that $e_1 \le e_2$ and $e_2 \le e_1$, where $e_1, e_2$ are forward events. Then for all rooted $r$, $\#(r, e_1) > 0$ iff $\#(r, e_2) > 0$. Since
<figure><img src="image_7.png" /><figcaption>Fig. 6. The LTSI in Example 4.22.</figcaption></figure>

**PROOF.** By Lemma 4.19 there is a path $s$ from $Q$ to $Q'$ such that for all $u$ in $s$ we have $[t]$ ci $[u]$. Let $\ell(u) = \beta$. By Proposition 4.17 we have und($\alpha$) $\neq$ und($\beta$). Hence $\#(s, [t]) = 0$, and by Lemma 4.12 $\#(r, [t]) = 0$ as required. $\square$

**PROPOSITION 4.21.** If an LTSI is pre-reversible then it satisfies NRE.

**PROOF.** Let $e$ be a forward event and $r$ be a rooted path from $I$ to $R$, and suppose for a contradiction that $\#(r, e) > 1$. Using PL we can obtain a forward-only path $r'$ from $I$ to $R$ with $r \approx r'$. By Lemma 4.12, $\#(r', e) > 1$. Hence, $r'$ contains (at least) two transitions for $e$; let us denote them as $t: P \xrightarrow{a} Q$ and $t': P' \xrightarrow{a} Q'$. Without loss of generality, we assume that $t$ occurs before $t'$ in $r$. Let $r''$ be the portion of $r'$ from $Q$ to $P'$. By Lemma 4.20 applied to $t, t'$ and path $r''t'$ we have $\#(r''t', [t]) = 0$. This is a contradiction since $r''$ is forward-only. $\square$

NRE was shown in the forward-only setting of occurrence transition systems with independence in [47, Corollary 4.6]. It was also shown in the reversible setting without independence in [41, Proposition 2.10].

**Example 4.22.** Consider the LTSI in Figure 6. Independence holds only between coinital transitions and is given by closing under BTI and propagating independence around the corners of diamonds as in PCI whenever possible. Note, however, that PCI does not hold, since we have coinital independent *a* and *a*-transitions, contradicting Lemma 4.4. On the other hand, in addition to BTI, axioms SP and WF hold, so that CC holds. All *a*-transitions belong to the same event, and all *b*-transitions belong to the same event. We have rooted paths where the same event is repeated, contradicting NRE. Note also that BLD fails and that ci is reflexive. ◇

## 4.3 Polychotomy

We now show what we call *polychotomy*, which states that if forward events do not cause each other and are not in conflict, then they must be independent. This will help us to relate the different notions of causal safety and liveness (Section 5). We first define causality and conflict relations on forward events.

**Definition 4.23 (Causality relation on forward events).** Let $e, e'$ be forward events of some LTSI. Let $e \le e'$ iff for all rooted paths $r$, if $\#(r, e') > 0$ then $\#(r, e) > 0$. As usual $e < e'$ means $e \le e'$ and $e \neq e'$. If $e < e'$ we say that $e$ is a *cause* of $e'$.

As expected, the causality relation is a partial ordering (i.e., a reflexive, transitive and antisymmetric relation).

**LEMMA 4.24.** If an LTSI is pre-reversible then $\le$ is a partial ordering on events.

**PROOF.** Reflexivity and transitivity are immediate. For antisymmetry, suppose that $e_1 \le e_2$ and $e_2 \le e_1$, where $e_1, e_2$ are forward events. Then for all rooted $r$, $\#(r, e_1) > 0$ iff $\#(r, e_2) > 0$. Since
the LTSI is pre-reversible, by Proposition 4.13, for all rooted $r$, $\#(r, e_1) \ge 0$ and $\#(r, e_2) \ge 0$. Let $r$ be a shortest rooted path such that $\#(r, e_1) > 0$. We can use WF to show that $r$ must exist. Then $\#(r, e_2) > 0$. Also $r = r't$, where $\#(r', e_1) = 0$ (otherwise $r$ would not be a shortest path) and so $\#(r', e_2) = 0$. We see that both $[t] = e_1$ and $[t] = e_2$, showing that $e_1 = e_2$ as required. $\square$

In [41, 49], orderings on forward events have been defined using forward-only rooted paths; in fact, the definitions coincide for pre-reversible LTSIs.

*Definition 4.25* ([41, 49]). Let $e, e'$ be forward events of some LTSI. Let $e \le_f e'$ iff for all forward-only rooted paths $r$, if $\#(r, e') > 0$ then $\#(r, e) > 0$.

**LEMMA 4.26.** For any LTSI, and any forward events $e, e'$, $e \le e'$ implies $e \le_f e'$. If an LTSI is pre-reversible then $e \le_f e'$ implies $e \le e'$.

**PROOF.** Straightforward using PL and Lemma 4.12. $\square$

*Definition 4.27.* Two forward events $e, e'$ are in conflict, written $e \# e'$, iff 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 [41, 49]; in fact, the definitions coincide for pre-reversible LTSIs. We omit the details.

We can now introduce the main result of this section.

*Definition 4.28* (Polychotomy). Let $\mathcal{L}$ be a pre-reversible LTSI. We say that $\mathcal{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 \text{ ci } e'$.

**PROPOSITION 4.29** (POLYCHOTOMY). Assume an LTSI is pre-reversible. Then polychotomy holds.

**PROOF.** Consider two forward events $e$ and $e'$ which may or may not be equal.

We first check mutual exclusivity. Suppose $e = e'$. Then $e < e$ is impossible by definition of $<$. Also $e$ cannot be in conflict with itself (we can use WF to show that there is at least one rooted path). Finally, $e \text{ ci } e$ is impossible by Proposition 4.16. From now on we assume $e \neq e'$.

Next suppose $e < e'$. We can rule out $e' < e$ using Lemma 4.24.

Using Lemma 4.26, we know that $e <_f e'$, hence there must be some forward-only rooted path with $e$ followed by $e'$ (WF ensures at least one rooted path exists), and so $e$ and $e'$ are not in conflict. Finally $e \text{ ci } e'$ implies that there are two coinital transitions $t \in e, t' \in e'$ which are independent. Using SP to complete the square we see that $e < e'$ is impossible by NRE, which holds by Proposition 4.21.

Similarly we see that $e' < e$ implies that $e$ and $e'$ are not in conflict and not independent.

Next suppose that $e \# e'$. If $e \text{ ci } e'$ then there are two coinital transitions $t \in e, t' \in e'$ which are independent. Using SP to complete the square and WF we see that we have a forward-only rooted path containing occurrences of both $e$ and $e'$ contradicting them being in conflict.

Suppose that none of (1)-(4) hold. We must show (5). Since $e, e'$ do not conflict, there is a rooted path $r$ starting at some irreversible $I$ such that $\#(r, e) > 0$ and $\#(r, e') > 0$. If more than one such path exists, choose one of minimal length. W.l.o.g. suppose that $r$ finishes with $t' \in e'$ at $P$. Since not $e < e'$, using Lemma 4.26 also $e <_f e'$ does not hold; hence there is another forward-only path $r'$ from some irreversible $I'$ finishing with $t'' \in e'$ at $Q$ such that $\#(r', e) = 0$. By Lemma 4.19
the LTSI is pre-reversible, by Proposition 4.13, for all rooted $r$, $\#(r, e_1) \ge 0$ and $\#(r, e_2) \ge 0$. Let $r$ be a shortest rooted path such that $\#(r, e_1) > 0$. We can use WF to show that $r$ must exist. Then $\#(r, e_2) > 0$. Also $r = r't$, where $\#(r', e_1) = 0$ (otherwise $r$ would not be a shortest path) and so $\#(r', e_2) = 0$. We see that both $[t] = e_1$ and $[t] = e_2$, showing that $e_1 = e_2$ as required. $\square$

In [41, 49], orderings on forward events have been defined using forward-only rooted paths; in fact, the definitions coincide for pre-reversible LTSIs.

*Definition 4.25* ([41, 49]). Let $e, e'$ be forward events of some LTSI. Let $e \le_f e'$ iff for all forward-only rooted paths $r$, if $\#(r, e') > 0$ then $\#(r, e) > 0$.

**LEMMA 4.26.** For any LTSI, and any forward events $e, e'$, $e \le e'$ implies $e \le_f e'$. If an LTSI is pre-reversible then $e \le_f e'$ implies $e \le e'$.

**PROOF.** Straightforward using PL and Lemma 4.12. $\square$

*Definition 4.27.* Two forward events $e, e'$ are in conflict, written $e \# e'$, iff 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 [41, 49]; in fact, the definitions coincide for pre-reversible LTSIs. We omit the details.

We can now introduce the main result of this section.

*Definition 4.28* (Polychotomy). Let $\mathcal{L}$ be a pre-reversible LTSI. We say that $\mathcal{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 \text{ ci } e'$.

**PROPOSITION 4.29** (POLYCHOTOMY). Assume an LTSI is pre-reversible. Then polychotomy holds.

**PROOF.** Consider two forward events $e$ and $e'$ which may or may not be equal.

We first check mutual exclusivity. Suppose $e = e'$. Then $e < e$ is impossible by definition of $<$. Also $e$ cannot be in conflict with itself (we can use WF to show that there is at least one rooted path). Finally, $e \text{ ci } e$ is impossible by Proposition 4.16. From now on we assume $e \neq e'$.

Next suppose $e < e'$. We can rule out $e' < e$ using Lemma 4.24.

Using Lemma 4.26, we know that $e <_f e'$, hence there must be some forward-only rooted path with $e$ followed by $e'$ (WF ensures at least one rooted path exists), and so $e$ and $e'$ are not in conflict. Finally $e \text{ ci } e'$ implies that there are two coinital transitions $t \in e, t' \in e'$ which are independent. Using SP to complete the square we see that $e < e'$ is impossible by NRE, which holds by Proposition 4.21.

Similarly we see that $e' < e$ implies that $e$ and $e'$ are not in conflict and not independent.

Next suppose that $e \# e'$. If $e \text{ ci } e'$ then there are two coinital transitions $t \in e, t' \in e'$ which are independent. Using SP to complete the square and WF we see that we have a forward-only rooted path containing occurrences of both $e$ and $e'$ contradicting them being in conflict.

Suppose that none of (1)-(4) hold. We must show (5). Since $e, e'$ do not conflict, there is a rooted path $r$ starting at some irreversible $I$ such that $\#(r, e) > 0$ and $\#(r, e') > 0$. If more than one such path exists, choose one of minimal length. W.l.o.g. suppose that $r$ finishes with $t' \in e'$ at $P$. Since not $e < e'$, using Lemma 4.26 also $e <_f e'$ does not hold; hence there is another forward-only path $r'$ from some irreversible $I'$ finishing with $t'' \in e'$ at $Q$ such that $\#(r', e) = 0$. By Lemma 4.19
<figure><img src="image_7.png" /><figcaption>Fig. 7. Implications between properties all assuming pre-reversible. Note that $CS_{ci}$ holds for pre-reversible LTSIs (Theorem 5.20). All implications are strict, and there are no further implications between the sixteen properties shown, in view of the examples cited.</figcaption></figure>

there is a path $s$ from $Q$ to $P$ such that $e'$ ci $[u]$ for every $u$ in $s$. Using Proposition 3.6 we deduce that $l' = l$. By CC $r \approx r'$s and so by Lemma 4.12 $\#(s, e) > 0$ and $s$ must contain $u \in e$, yielding $e$ ci $e'$ as required. $\square$

# 5 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” (see, e.g., [30]). 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 formalisations of such properties, based on independence of transitions (Section 5.1), independence of events (Section 5.2), and ordering of events (Section 5.3), and study their relationships. In Figure 7 we show the relationships between the various axioms and properties we shall study in this section and Section 6.

## 5.1 CS and CL via independence of transitions

We first define causal safety and liveness using the independence relation.

*Definition 5.1.* Let $\mathcal{L}$ be an LTSI.
<figure><img src="image_8.png" /><figcaption>Fig. 7. Implications between properties all assuming pre-reversible. Note that $CS_{ci}$ holds for pre-reversible LTSIs (Theorem 5.20). All implications are strict, and there are no further implications between the sixteen properties shown, in view of the examples cited.</figcaption></figure>

there is a path $s$ from $Q$ to $P$ such that $e'$ ci $[u]$ for every $u$ in $s$. Using Proposition 3.6 we deduce that $l' = l$. By CC $r \approx r'$s and so by Lemma 4.12 $\#(s, e) > 0$ and $s$ must contain $u \in e$, yielding $e$ ci $e'$ as required. □

# 5 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” (see, e.g., [30]). 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 formalisations of such properties, based on independence of transitions (Section 5.1), independence of events (Section 5.2), and ordering of events (Section 5.3), and study their relationships. In Figure 7 we show the relationships between the various axioms and properties we shall study in this section and Section 6.

## 5.1 CS and CL via independence of transitions

We first define causal safety and liveness using the independence relation.

*Definition 5.1.* Let $\mathcal{L}$ be an LTSI.
(1) We say that $\mathcal{L}$ is *causally safe (CS<sub>l</sub>)* if whenever $t_0 : P \xrightarrow{a} Q$, $r : Q \xrightarrow{\rho_*} R$, $\#(r, [t_0]) = 0$ and $t_0^\dagger : S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$, then $\underline{t_0} \prec t$ for all $t$ in $r$ such that $\#(r, [t]) > 0$.

(2) We say that $\mathcal{L}$ is *causally live (CL<sub>l</sub>)* if whenever $t_0 : P \xrightarrow{a} Q$, $r : Q \xrightarrow{\rho_*} R$ and $\#(r, [t_0]) = 0$ and $\underline{t_0} \prec t$, for all $t$ in $r$ such that $\#(r, [t]) > 0$, then we have $t_0^\dagger : S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$.

Properties CS<sub>l</sub> and CL<sub>l</sub> both consider a (forward) transition $t_0 : P \xrightarrow{a} Q$ followed by a path $r$ where the number of occurrences in $r$ of transitions that belong to the same event as $t_0$ is zero. CS<sub>l</sub> states that if after path $r$ a transition $t_0^\dagger$ can be undone, where $t_0$ and $t_0^\dagger$ belong to the same event, then the reverse of $t_0$ is independent of all transitions $t$ where the number of occurrences in $r$ of the event of $t$ is positive. Dually, CL<sub>l</sub> requires that if the reverse of $t_0$ is independent of all transitions whose events have a positive number of occurrences in $r$, then it can be undone.

**Remark 5.2.** In the definition of CS<sub>l</sub> the condition that $\#(r, [t_0]) = 0$ can be deduced from the other conditions using Lemma 4.20, provided that the LTSI is pre-reversible.

We use the reverse of $t_0$ when considering independence from $t$ because our axioms BTI, SP and PCI focus on *coinitial* independence rather than independence of consecutive transitions in a trace. Take the simplest case where $r$ is a single transition $t : Q \xrightarrow{b} R$. First assume $\underline{t_0} \prec t$; note that this is *coinitial independence*. We can use SP and PCI to get $t_0^\dagger : S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$, which is an example of *causal liveness*. Conversely, if we assume $t_0^\dagger : S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$, we can use BTI, SP, BLD and PCI to get a diamond with $\underline{t_0} \prec t$, which is an example of *causal safety*.

Note that in the discussion above to prove causal safety we need to consider also the case $r = \underline{tt}$. Since $[\underline{t}]$ has a negative number of occurrences, we only need to show that $\underline{t_0} \prec t$, which can be proved as above. However, if we replaced the condition $\#(r, [t]) > 0$ with $\#(r, [t]) \neq 0$, we would also need to show $\underline{t_0} \prec \underline{t}$, which does not follow from the axioms above. Intuitively, requiring $\underline{t_0} \prec \underline{t}$ would make little sense, since all the occurrences of $\underline{t}$ could be simplified with corresponding occurrences of $t$. This is why we decided to require $\#(r, [t]) > 0$.

We have seen in the last two paragraphs that existing axioms are sufficient to show CS<sub>l</sub> and CL<sub>l</sub> in the case where trace $r$ consists of a single transition. However, existing axioms are not enough for general $r$, as we will show in Examples 5.7 and 5.8. Thus, we introduce the following axiom, which states that independence does not depend on the choice of the representative inside an event.

**Definition 5.3.** *Independence respects events (IRE):* Whenever $t \sim t' \prec u$ we have $t \prec u$.

IRE is one of the conditions in the definition of transition systems with independence [47, Definition 3.7].

IRE allows us to relate *coinitial independence* on events and independence on transitions.

**LEMMA 5.4.** *Assume an LTSI satisfies IRE. If $[t]$ ci $[u]$ then $t \prec u$.*

**PROOF.** Immediate. $\square$

Together with the axioms for pre-reversibility, IRE is enough to show both CS<sub>l</sub> and CL<sub>l</sub>.

**Theorem 5.5.** *Let a pre-reversible LTSI satisfy IRE. Then it satisfies CS<sub>l</sub>.*

**PROOF.** Suppose $t_0 : P \xrightarrow{a} Q$, $r : Q \xrightarrow{\rho_*} R$ and $t_0^\dagger : S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$. By Lemma 4.19 there is a path $s$ from $Q$ to $R$ such that for all $u$ in $s$ we have $[t_0]$ ci $[u]$. We deduce by Lemmas 4.15 and 5.4 that for all $u$ in $s$ we have $\underline{t_0} \prec u$. By CC, $r \approx s$.
(1) We say that $\mathcal{L}$ is *causally safe* ($CS_l$) if whenever $t_0 : P \xrightarrow{a} Q$, $r : Q \xrightarrow{\rho_*} R$, $\#(r, [t_0]) = 0$ and $t_0^\dagger : S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$, then $\underline{t_0} \prec t$ for all $t$ in $r$ such that $\#(r, [t]) > 0$.

(2) We say that $\mathcal{L}$ is *causally live* ($CL_l$) if whenever $t_0 : P \xrightarrow{a} Q$, $r : Q \xrightarrow{\rho_*} R$ and $\#(r, [t_0]) = 0$ and $\underline{t_0} \prec t$, for all $t$ in $r$ such that $\#(r, [t]) > 0$, then we have $t_0^\dagger : S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$.

Properties $CS_l$ and $CL_l$ both consider a (forward) transition $t_0 : P \xrightarrow{a} Q$ followed by a path $r$ where the number of occurrences in $r$ of transitions that belong to the same event as $t_0$ is zero. $CS_l$ states that if after path $r$ a transition $t_0^\dagger$ can be undone, where $t_0$ and $t_0^\dagger$ belong to the same event, then the reverse of $t_0$ is independent of all transitions $t$ where the number of occurrences in $r$ of the event of $t$ is positive. Dually, $CL_l$ requires that if the reverse of $t_0$ is independent of all transitions whose events have a positive number of occurrences in $r$, then it can be undone.

**Remark 5.2.** In the definition of $CS_l$, the condition that $\#(r, [t_0]) = 0$ can be deduced from the other conditions using Lemma 4.20, provided that the LTSI is pre-reversible.

We use the reverse of $t_0$ when considering independence from $t$ because our axioms BTI, SP and PCI focus on *coinitial* independence rather than independence of consecutive transitions in a trace. Take the simplest case where $r$ is a single transition $t : Q \xrightarrow{b} R$. First assume $\underline{t_0} \prec t$; note that this is *coinitial independence*. We can use SP and PCI to get $t_0^\dagger : S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$, which is an example of *causal liveness*. Conversely, if we assume $t_0^\dagger : S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$, we can use BTI, SP, BLD and PCI to get a diamond with $\underline{t_0} \prec t$, which is an example of *causal safety*.

Note that in the discussion above to prove causal safety we need to consider also the case $r = \underline{tt}$. Since $[\underline{t}]$ has a negative number of occurrences, we only need to show that $\underline{t_0} \prec t$, which can be proved as above. However, if we replaced the condition $\#(r, [t]) > 0$ with $\#(r, [t]) \neq 0$, we would also need to show $\underline{t_0} \prec \underline{t}$, which does not follow from the axioms above. Intuitively, requiring $\underline{t_0} \prec \underline{t}$ would make little sense, since all the occurrences of $\underline{t}$ could be simplified with corresponding occurrences of $t$. This is why we decided to require $\#(r, [t]) > 0$.

We have seen in the last two paragraphs that existing axioms are sufficient to show $CS_l$ and $CL_l$ in the case where trace $r$ consists of a single transition. However, existing axioms are not enough for general $r$, as we will show in Examples 5.7 and 5.8. Thus, we introduce the following axiom, which states that independence does not depend on the choice of the representative inside an event.

**Definition 5.3.** *Independence respects events (IRE):* Whenever $t \sim t' \prec u$ we have $t \prec u$.

IRE is one of the conditions in the definition of transition systems with independence [47, Definition 3.7].

IRE allows us to relate *coinitial independence* on events and independence on transitions.

**LEMMA 5.4.** *Assume an LTSI satisfies IRE. If $[t]$ ci $[u]$ then $t \prec u$.*

**PROOF.** Immediate. $\square$

Together with the axioms for pre-reversibility, IRE is enough to show both $CS_l$ and $CL_l$.

**Theorem 5.5.** *Let a pre-reversible LTSI satisfy IRE. Then it satisfies $CS_l$.*

**PROOF.** Suppose $t_0 : P \xrightarrow{a} Q$, $r : Q \xrightarrow{\rho_*} R$ and $t_0^\dagger : S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$. By Lemma 4.19 there is a path $s$ from $Q$ to $R$ such that for all $u$ in $s$ we have $[t_0]$ ci $[u]$. We deduce by Lemmas 4.15 and 5.4 that for all $u$ in $s$ we have $\underline{t_0} \prec u$. By CC, $r \approx s$.
<figure><img src="image_8.png" /><figcaption>Fig. 8. The LTSIs in Examples 5.7 and 5.8.</figcaption></figure>

Take $t$ in $r$ such that $\#(r, [t]) > 0$. Then $\#(s, [t]) > 0$, thanks to Lemma 4.12. But then there is $u$
in $s$ such that $u \sim t$. We have $t_0 \prec u$ and so $t_0 \prec t$, using IRE, as desired. $\square$

**Theorem 5.6.** Let a pre-reversible LTSI satisfy IRE. Then it satisfies $CL_t$.

*PROOF.* Suppose $t_0 : P \xrightarrow{a} Q, r : Q \xrightarrow{\rho} * R$ and $\#(r, [t_0]) = 0$ and $t_0 \prec t$, for all $t$ in $r$ such that $\#(r, [t]) > 0$. We have to show that there is $t_0^\dagger : S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$.

Thanks to PL, there is $T$ such that $b : P \xrightarrow{\rho b} * T$ and $f : T \xrightarrow{\rho f} * R$, with $b$ backward and $f$ forward. By CC, $t_0 r \approx bf$. Since $\#(r, [t_0]) = 0$, thanks to Lemma 4.12 we have $\#(bf, [t_0]) = 1$. As a consequence, there is a transition $t'_0 : P' \xrightarrow{a} Q' \in [t_0]$ in $f$. This $t'_0$ is in fact the unique transition in $[t_0]$ belonging to $f$ by Proposition 4.21. Let $f'$ be the portion of $f$ from $Q'$ to $R$. If we can show that $t'_0 \prec t''$ for each transition $t''$ in $f'$, then the thesis will follow by commuting $t'_0$ with all such transitions using SP and IRE.

By Lemma 4.19 there is a path $s$ from $Q$ to $Q'$ such that $[t_0]$ ci $[u]$ for all $u$ in $s$. By CC, $r \approx sf'$. Take any $t''$ in $f'$. By Lemma 4.12, $\#(r, [t'']) = \#(s, [t'']) + \#(f', [t''])$. If $\#(s, [t'']) < 0$ then there is $u$ in $s$ such that $u \sim t''$. Now $[t_0]$ ci $[u] = [t'']$. Therefore $[t_0]$ ci $[t'']$ by Lemma 4.15, and $t_0 \prec t''$ by Lemma 5.4. Suppose instead $\#(s, [t'']) \ge 0$. Since $\#(f', [t'']) > 0$, we have $\#(r, [t'']) > 0$. So there is $u$ in $r$ such that $u \sim t''$, and by hypothesis $t_0 \prec u$, so that $t'_0 \prec t''$ using IRE. $\square$

We now give examples of LTSIs which are pre-reversible and where $CS_t$ and $CL_t$ fail.

*Example 5.7.* Consider the LTSI shown in Figure 8 including the dashed transitions. We add coinitial independence as generated by BTI and PCI. BTI gives $(Q', \underline{b}, Q) \prec (Q', \underline{a}, P')$ and $(R, \underline{c}, Q') \prec (R, \underline{a}, S)$. Assuming $t_0 : P \xrightarrow{a} Q$ and $t_0^\dagger : S \xrightarrow{a} R$, PCI gives three additional independence pairs for each of the two diamonds: $(Q, b, Q') \prec t_0$, $t_0 \prec (P, b, P')$ and $(P', \underline{b}, P) \prec (P', a, Q')$ for the diamond with the source $P$, and $(Q', c, R) \prec (Q', \underline{a}, P')$, $(P', a, Q') \prec (P', c, S)$ and $(S, \underline{c}, P') \prec t_0^\dagger$ for the other diamond. The LTSI is pre-reversible. However $CS_t$ fails. Transition $t_0$ is followed by a path $Q \xrightarrow{bc} * R$ and the transition $t_0^\dagger$ satisfies $t_0 \sim t_0^\dagger$. If $CS_t$ held we could deduce that $t_0 \prec (Q', c, R)$, which is not the case. Similarly, we see that IRE fails, since $t_0 \sim (Q', \underline{a}, P') \prec (Q', c, R)$ but not $t_0 \prec (Q', c, R)$. Note, however, that $CL_t$ holds, since only transitions inside the same diamond are independent, and transitions on one side of the diamond are undone by the corresponding transition on the opposite side. $\diamond$

*Example 5.8.* Consider the LTSI shown in Figure 8 excluding the dashed transitions. We add coinitial independence as given by BTI and PCI, similarly to the previous example. We also add $(Q, \underline{a}, P) \prec (Q', c, R)$. The LTSI is pre-reversible. However $CL_t$ fails. We have $t_0 : P \xrightarrow{a} Q, Q \xrightarrow{bc} * R$ and $t_0 \prec (Q, b, Q')$, $t_0 \prec (Q', c, R)$. Clearly $CL_t$ fails, since we cannot reverse the $a$-transition at $R$. IRE fails since $(Q', \underline{a}, P') \sim t_0 \prec (Q', c, R)$ but not $(Q', \underline{a}, P') \prec (Q', c, R)$. Note, however, that $CS_t$ holds since the only way to undo transitions is with transitions on the opposite side of the same
<figure><img src="image_9.png" /><figcaption>Fig. 8. The LTSIs in Examples 5.7 and 5.8.</figcaption></figure>

Take $t$ in $r$ such that $\#(r, [t]) > 0$. Then $\#(s, [t]) > 0$, thanks to Lemma 4.12. But then there is $u$
in $s$ such that $u \sim t$. We have $t_0 \prec u$ and so $t_0 \prec t$, using IRE, as desired. $\square$

**Theorem 5.6.** Let a pre-reversible LTSI satisfy IRE. Then it satisfies $CL_t$.

*PROOF.* Suppose $t_0 : P \xrightarrow{a} Q, r : Q \xrightarrow{\rho}_* R$ and $\#(r, [t_0]) = 0$ and $t_0 \prec t$, for all $t$ in $r$ such that $\#(r, [t]) > 0$. We have to show that there is $t_0^\dagger : S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$.

Thanks to PL, there is $T$ such that $b : P \xrightarrow{\rho b}_* T$ and $f : T \xrightarrow{\rho f}_* R$, with $b$ backward and $f$ forward. By CC, $t_0 r \approx bf$. Since $\#(r, [t_0]) = 0$, thanks to Lemma 4.12 we have $\#(bf, [t_0]) = 1$. As a consequence, there is a transition $t'_0 : P' \xrightarrow{a} Q' \in [t_0]$ in $f$. This $t'_0$ is in fact the unique transition in $[t_0]$ belonging to $f$ by Proposition 4.21. Let $f'$ be the portion of $f$ from $Q'$ to $R$. If we can show that $t'_0 \prec t''$ for each transition $t''$ in $f'$, then the thesis will follow by commuting $t'_0$ with all such transitions using SP and IRE.

By Lemma 4.19 there is a path $s$ from $Q$ to $Q'$ such that $[t_0]$ ci $[u]$ for all $u$ in $s$. By CC, $r \approx sf'$. Take any $t''$ in $f'$. By Lemma 4.12, $\#(r, [t'']) = \#(s, [t'']) + \#(f', [t''])$. If $\#(s, [t'']) < 0$ then there is $u$ in $s$ such that $u \sim t''$. Now $[t_0]$ ci $[u] = [t'']$. Therefore $[t_0]$ ci $[t'']$ by Lemma 4.15, and $t_0 \prec t''$ by Lemma 5.4. Suppose instead $\#(s, [t'']) \ge 0$. Since $\#(f', [t'']) > 0$, we have $\#(r, [t'']) > 0$. So there is $u$ in $r$ such that $u \sim t''$, and by hypothesis $t_0 \prec u$, so that $t'_0 \prec t''$ using IRE. $\square$

We now give examples of LTSIs which are pre-reversible and where $CS_t$ and $CL_t$ fail.

*Example 5.7.* Consider the LTSI shown in Figure 8 including the dashed transitions. We add coinitial independence as generated by BTI and PCI. BTI gives $(Q', \underline{b}, Q) \prec (Q', \underline{a}, P')$ and $(R, \underline{c}, Q') \prec (R, \underline{a}, S)$. Assuming $t_0 : P \xrightarrow{a} Q$ and $t_0^\dagger : S \xrightarrow{a} R$, PCI gives three additional independence pairs for each of the two diamonds: $(Q, b, Q') \prec t_0$, $t_0 \prec (P, b, P')$ and $(P', \underline{b}, P) \prec (P', a, Q')$ for the diamond with the source $P$, and $(Q', c, R) \prec (Q', \underline{a}, P')$, $(P', a, Q') \prec (P', c, S)$ and $(S, \underline{c}, P') \prec t_0^\dagger$ for the other diamond. The LTSI is pre-reversible. However $CS_t$ fails. Transition $t_0$ is followed by a path $Q \xrightarrow{bc}_* R$ and the transition $t_0^\dagger$ satisfies $t_0 \sim t_0^\dagger$. If $CS_t$ held we could deduce that $t_0 \prec (Q', c, R)$, which is not the case. Similarly, we see that IRE fails, since $t_0 \sim (Q', \underline{a}, P') \prec (Q', c, R)$ but not $t_0 \prec (Q', c, R)$. Note, however, that $CL_t$ holds, since only transitions inside the same diamond are independent, and transitions on one side of the diamond are undone by the corresponding transition on the opposite side. $\diamond$

*Example 5.8.* Consider the LTSI shown in Figure 8 excluding the dashed transitions. We add coinitial independence as given by BTI and PCI, similarly to the previous example. We also add $(Q, \underline{a}, P) \prec (Q', c, R)$. The LTSI is pre-reversible. However $CL_t$ fails. We have $t_0 : P \xrightarrow{a} Q, Q \xrightarrow{bc}_* R$ and $t_0 \prec (Q, b, Q')$, $t_0 \prec (Q', c, R)$. Clearly $CL_t$ fails, since we cannot reverse the $a$-transition at $R$. IRE fails since $(Q', \underline{a}, P') \sim t_0 \prec (Q', c, R)$ but not $(Q', \underline{a}, P') \prec (Q', c, R)$. Note, however, that $CS_t$ holds since the only way to undo transitions is with transitions on the opposite side of the same
diamond, and the path connecting them is another transition of the same diamond. Hence, the
condition on independence holds, thanks to BTI and PCI.
◇

Examples 5.7 and 5.8 show that the stipulation of IRE cannot be omitted in the statements of
Theorems 5.5 and 5.6, respectively. These examples also show that we cannot deduce CS<sub>t</sub> or CL<sub>t</sub>
from CC, nor one from the other.

*Example 5.9 (CS<sub>t</sub> and CL<sub>t</sub> do not imply CC).* Consider the LTSI with states *P*, *Q*, *R*, *S* and transitions *t*: *P* →<sub>*a*</sub> *Q*, *u*: *P* →<sub>*b*</sub> *R*, *t*': *R* →<sub>*a'</sub> *S* and *u*': *Q* →<sub>*b'</sub> *S*, with empty independence relation. This is essentially the same as Example 3.16, except that we have disambiguated the transition labels, to reflect that the four transitions form four different events. Then CC does not hold, but we claim that both CS<sub>t</sub> and CL<sub>t</sub> hold.

CS<sub>t</sub>: There are four possible cases to check, depending on the initial forward transition. Consider first *t*: *P* →<sub>*a*</sub> *Q* and some *r*: *Q* →<sub>*ρ*</sub> *Q*', *P* →<sub>*a'</sub> *Q*', where ♯(*r*, [*t*]) = 0 and (*P*, *a*, *Q*) ~ (*P*', *a*, *Q*'). Clearly *P*' = *P* and *Q*' = *Q*. To verify CS<sub>t</sub> in this case, it is enough to show that ♯(*r*, [*u*]) = ♯(*r*, [*t*']) = ♯(*r*, [*u*']) = 0. Since *r* is a circuit, it enters each state as often as it leaves it. Furthermore, since ♯(*r*, [*t*]) = 0, *r* enters *Q* from *P* as often as it leaves *Q* towards *P*. Hence *r* must enter *Q* from *S* as often as it leaves *Q* towards *S*, meaning that ♯(*r*, [*u*']) = 0. We can similarly deduce that ♯(*r*, [*t*']) = 0 and ♯(*r*, [*u*]) = 0. The remaining three cases with initial transitions *u*, *t*′ and *u*′ are similar to the case for *t*.

CL<sub>t</sub>: Again there are four cases to check, depending on the initial forward transition. Consider first *t*: *P* →<sub>*a*</sub> *Q* and some *r*: *Q* →<sub>*ρ*</sub> *Q*′ where ♯(*r*, [*t*]) = 0 and for all *t*′′ in *r* we have ♯(*r*, [*t*′′]) ≤ 0 (indeed, if ♯(*r*, [*t*′′]) > 0 we would require *t*′ ⊢ *t*′′, which is false since the independence relation is empty, hence the condition for CL<sub>t</sub> would hold trivially). However, if ♯(*r*, [*t*′′]) < 0 then there is *t*′′′ in *r* with [*t*′′′] = [*t*′′] (in this example actually *t*′′′ = *t*′′) and ♯(*r*, [*t*′′]) > 0, but, for the same reason as above, we cannot have ♯(*r*, [*t*′′]) > 0 since the independence relation is empty. Hence for each *t*′′ we have ♯(*r*, [*t*′′]) = 0, which implies *Q*′ = *Q*, since the net rotation (cfr. Figure 4) of each transition is zero, and so the net rotation of *r* is zero. The thesis follows trivially. The remaining three cases with initial transitions *u*, *t*′ and *u*′ are similar to the case for *t*.
◇

The next axiom states that independence is fully determined by its restriction to coin initial tran-
sitions. It is related to axiom (E) of [47, page 325], but here we allow reverse as well as forward
transitions.

*Definition 5.10. Independence of events is coin initial (IEC):* if $t_1 \prec t_2$ then $[t_1] \text{ ci } [t_2]$.

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

*Definition 5.11. Reversing preserves independence (RPI):* if $t \prec t'$ then $\underline{t} \prec t'$.

**PROPOSITION 5.12.** If an LTSI satisfies SP, PCI, IRE, IEC then it also satisfies RPI.

*PROOF.* Suppose $t \prec u$. We must show $\underline{t} \prec u$. By IEC we have $t' \sim t$, $u' \sim u$ such that $t' \prec u'$ and $t', u'$ are coin initial. By SP there is a diamond $t', u', t''$, $u''$ with $t' \sim t''$, $u' \sim u''$. Then $\underline{t'} \prec u''$ using PCI. Then $\underline{t} \sim \underline{t'} \prec u'' \sim u$ and so by IRE $\underline{t} \prec u$ as required. $\square$

We can use IEC or IRE to show that transitions which are part of the same event cannot be
independent.

*Definition 5.13. Event coherence (ECh):* if $t \sim t'$ then $t \precceq t'$.

**PROPOSITION 5.14.** If a pre-reversible LTSI satisfies either IRE or IEC then it also satisfies ECh.

*Definition 5.10. Independence of events is coin initial (IEC):* if $t_1 \prec t_2$ then $[t_1] \text{ ci } [t_2]$.

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

*Definition 5.11. Reversing preserves independence (RPI):* if *t* ⊢ *t'* then *t* ⊢ *t*′.

PROPOSITION 5.12. If an LTSI satisfies SP, PCI, IRE, IEC then it also satisfies RPI.

PROOF. Suppose $t \prec u$. We must show $\underline{t} \prec u$. By IEC we have $t' \sim t$, $u' \sim u$ such that $t' \prec u'$ and $t', u'$ are coinital. By SP there is a diamond $t', u', t''$, $u''$ with $t' \sim t''$, $u' \sim u''$. Then $\underline{t'} \prec u''$ using PCI. Then $\underline{t} \sim \underline{t'} \prec u'' \sim u$ and so by IRE $\underline{t} \prec u$ as required. $\square$

We can use IEC or IRE to show that transitions which are part of the same event cannot be
independent.

*Definition 5.13. Event coherence (ECh):* if $t \sim t'$ then $t \precceq t'$.

PROPOSITION 5.14. If a pre-reversible LTSI satisfies either IRE or IEC then it also satisfies ECh.
diamond, and the path connecting them is another transition of the same diamond. Hence, the
condition on independence holds, thanks to BTI and PCI.
◇

Examples 5.7 and 5.8 show that the stipulation of IRE cannot be omitted in the statements of
Theorems 5.5 and 5.6, respectively. These examples also show that we cannot deduce CS<sub>t</sub> or CL<sub>t</sub>
from CC, nor one from the other.

*Example 5.9 (CS<sub>t</sub> and CL<sub>t</sub> do not imply CC).* Consider the LTSI with states *P*, *Q*, *R*, *S* and transitions *t*: *P* →<sub>*a*</sub> *Q*, *u*: *P* →<sub>*b*</sub> *R*, *t*': *R* →<sub>*a'</sub> *S* and *u*': *Q* →<sub>*b'</sub> *S*, with empty independence relation. This is essentially the same as Example 3.16, except that we have disambiguated the transition labels, to reflect that the four transitions form four different events. Then CC does not hold, but we claim that both CS<sub>t</sub> and CL<sub>t</sub> hold.

CS<sub>t</sub>: There are four possible cases to check, depending on the initial forward transition. Consider first *t*: *P* →<sub>*a*</sub> *Q* and some *r*: *Q* →<sub>*ρ*</sub>*Q*', *P* →<sub>*a'</sub> *Q*', where ♯(*r*, [*t*]) = 0 and (*P*, *a*, *Q*) ~ (*P*', *a*, *Q*'). Clearly *P* = *P* and *Q* = *Q*. To verify CS<sub>t</sub> in this case, it is enough to show that ♯(*r*, [*u*]) = ♯(*r*, [*t*']) = ♯(*r*, [*u*']) = 0. Since *r* is a circuit, it enters each state as often as it leaves it. Furthermore, since ♯(*r*, [*t*]) = 0, *r* enters *Q* from *P* as often as it leaves *Q* towards *P*. Hence *r* must enter *Q* from *S* as often as it leaves *Q* towards *S*, meaning that ♯(*r*, [*u*']) = 0. We can similarly deduce that ♯(*r*, [*t*']) = 0 and ♯(*r*, [*u*]) = 0. The remaining three cases with initial transitions *u*, *t*′ and *u*′ are similar to the case for *t*.

CL<sub>t</sub>: Again there are four cases to check, depending on the initial forward transition. Consider first *t*: *P* →<sub>*a*</sub> *Q* and some *r*: *Q* →<sub>*ρ*</sub>*Q*′ where ♯(*r*, [**t*′*]) = 0 and for all *t*′′ in *r* we have ♯(*r*, [**t*′′*]) ≤ 0 (indeed, if ♯(*r*, [**t*′′*]) > 0 we would require *t*′ ⊢ *t*′′, which is false since the independence relation is empty, hence the condition for CL<sub>t</sub> would hold trivially). However, if ♯(*r*, [**t*′′*]) < 0 then there is *t*′′′ in *r* with [**t*′′′*] = [**t*′′*] (in this example actually *t*′′′ = *t*′′) and ♯(*r*, [**t*′′*]) > 0, but, for the same reason as above, we cannot have ♯(*r*, [**t*′′*]) > 0 since the independence relation is empty. Hence for each *t*′′ we have ♯(*r*, [**t*′′*]) = 0, which implies *Q*′ = *Q*, since the net rotation (cfr. Figure 4) of each transition is zero, and so the net rotation of *r* is zero. The thesis follows trivially. The remaining three cases with initial transitions *u*, *t*′ and *u*′ are similar to the case for *t*.
◇

The next axiom states that independence is fully determined by its restriction to coin initial tran-
sitions. It is related to axiom (E) of [47, page 325], but here we allow reverse as well as forward
transitions.

*Definition 5.10. Independence of events is coinital (IEC)*: if $t_1 \prec t_2$ then $[t_1] \text{ ci } [t_2]$.

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

*Definition 5.11. Reversing preserves independence (RPI)*: if *t* ⊢ *t'* then *t* ⊢ *t*′.

PROPOSITION 5.12. If an LTSI satisfies SP, PCI, IRE, IEC then it also satisfies RPI.

PROOF. Suppose $t \vdash u$. We must show $\underline{t} \vdash u$. By IEC we have $t' \sim t$, $u' \sim u$ such that $t' \vdash u'$ and $t', u'$ are coinital. By SP there is a diamond $t', u', t'', u''$ with $t' \sim t'', u' \sim u''$. Then $\underline{t}' \vdash u''$ using PCI. Then $\underline{t} \sim \underline{t}' \vdash u'' \sim u$ and so by IRE $\underline{t} \vdash u$ as required. $\square$

We can use IEC or IRE to show that transitions which are part of the same event cannot be
independent.

*Definition 5.13. Event coherence (ECh)*: if *t* ~ *t'* then *t* ≁ *t'*.

PROPOSITION 5.14. If a pre-reversible LTSI satisfies either IRE or IEC then it also satisfies ECh.
**PROOF.** Assume for a contradiction that $t \sim t'$ and $t \lhd t'$. First suppose that IRE holds. We deduce $t \lhd t$, contradicting irreflexivity of $\iota$. Now suppose that IEC holds. Then $[t]$ ci $[t']$, and so $[t]$ ci $[t]$, contradicting irreflexivity of ci (Proposition 4.16). $\square$

All the axioms that we have introduced so far are independent, i.e. none is derivable from the remaining axioms.

The next example shows that IRE is not implied by other axioms.

*Example 5.15.* Let $t: P \xrightarrow{a} Q, u: P \xrightarrow{b} R, u': Q \xrightarrow{b} S, t': R \xrightarrow{a} S$, with $t \lhd u, \underline{u} \lhd t', \underline{t'} \lhd \underline{u}', u' \lhd \underline{t}$, namely we have independence at all corners of the diamond. Here we have two forward events, labelled with *a* and *b* respectively. We have $t' \sim t \lhd u$ but not $t' \lhd u$, so that IRE fails. However axioms SP, BTI, WF, PCI and IEC hold. ◇

The next example shows that IEC is not implied by other axioms.

*Example 5.16.* Let $t: P \xrightarrow{a} Q, u: R \xrightarrow{b} S$, where all states are distinct, and let $t \lhd u$. Then IEC fails; however axioms SP, BTI, WF, PCI and IRE hold. ◇

The counterexample above remains valid also if $Q = R$, as shown below.

*Example 5.17.* Let $t: P \xrightarrow{a} Q, u: Q \xrightarrow{b} S$, and let $t \lhd u$. Then IEC fails; however axioms SP, BTI, WF, PCI and IRE hold. ◇

We can now prove the independence result.

**PROPOSITION 5.18.** *The axioms SP, BTI, WF, PCI, IRE and IEC are independent of each other.*

**PROOF.** For each of the six axioms we give an LTSI which satisfies the other five axioms but not the axiom itself. In each case it is straightforward to check that the remaining axioms hold.

**SP:** Let $t: P \xrightarrow{a} Q$ and $u: P \xrightarrow{b} R$ with $t \lhd u$.

**BTI:** Let $P \xrightarrow{a} R$ and $Q \xrightarrow{b} R$ with an empty independence relation (Example 3.14).

**WF:** Let $P_{i+1} \xrightarrow{a} P_i$ for $i = 0, 1, \dots$ with an empty independence relation.

**PCI:** Let $t: P \xrightarrow{a} Q, u: P \xrightarrow{b} R, u': Q \xrightarrow{b} S, t': R \xrightarrow{a} S$, with $\underline{t'} \lhd \underline{u'}$.

**IRE:** See Example 5.15.

**IEC:** See Example 5.16 or Example 5.17. $\square$

## 5.2 CS and CL via independent events

We now introduce a second version of causal safety and liveness, which uses independence like $CS_i$ and $CL_i$, but on events rather than on transitions. More precisely, we use coinitial independence ci.

*Definition 5.19.* Let $\mathcal{L} = (\text{Proc}, \text{Lab}, \rightarrow, \iota)$ be an LTSI.

(1) We say that $\mathcal{L}$ is *coinitially causally safe* ($CS_{ci}$) if whenever $t_0: P \xrightarrow{a} Q, r: Q \xrightarrow{\rho_*} R$, $\#(r, [t_0]) = 0$ and $t_0^\dagger: S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$, then $[t_0]$ ci $e$ for all events $e$ such that $\#(r, e) > 0$.

(2) We say that $\mathcal{L}$ is *coinitially causally live* ($CL_{ci}$) if whenever $t_0: P \xrightarrow{a} Q, r: Q \xrightarrow{\rho_*} R$ and $\#(r, [t_0]) = 0$ and $[t_0]$ ci $e$, for all events $e$ such that $\#(r, e) > 0$, then we have $t_0^\dagger: S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$.

Note that in Definition 5.19 we operate at the level of events, rather than at the level of transitions as in Definition 5.1. Also note that we could replace $[t_0]$ ci $e$ by $[t_0]$ ci $e$ using Lemma 4.15. We have used the former for compatibility with Definition 5.1.
**PROOF.** Assume for a contradiction that $t \sim t'$ and $t \lhd t'$. First suppose that IRE holds. We deduce $t \lhd t$, contradicting irreflexivity of $\iota$. Now suppose that IEC holds. Then $[t]$ ci $[t']$, and so $[t]$ ci $[t]$, contradicting irreflexivity of ci (Proposition 4.16). $\square$

All the axioms that we have introduced so far are independent, i.e. none is derivable from the
remaining axioms.

The next example shows that IRE is not implied by other axioms.

*Example 5.15.* Let $t: P \xrightarrow{a} Q, u: P \xrightarrow{b} R, u': Q \xrightarrow{b} S, t': R \xrightarrow{a} S$, with $t \lhd u, \underline{u} \lhd t', \underline{t'} \lhd \underline{u}', u' \lhd \underline{t}'$, namely we have independence at all corners of the diamond. Here we have two forward events, labelled with *a* and *b* respectively. We have $t' \sim t \lhd u$ but not $t' \lhd u$, so that IRE fails. However *axioms SP, BTI, WF, PCI and IEC hold*. $\diamond$

The next example shows that IEC is not implied by other axioms.

*Example 5.16.* Let $t: P \xrightarrow{a} Q, u: R \xrightarrow{b} S$, where all states are distinct, and let $t \lhd u$. Then IEC fails; however axioms SP, BTI, WF, PCI and IRE hold. $\diamond$

The counterexample above remains valid also if $Q = R$, as shown below.

*Example 5.17.* Let $t: P \xrightarrow{a} Q, u: Q \xrightarrow{b} S$, and let $t \lhd u$. Then IEC fails; however axioms SP, BTI, WF, PCI and IRE hold. $\diamond$

We can now prove the independence result.

**PROPOSITION 5.18.** *The axioms SP, BTI, WF, PCI, IRE and IEC are independent of each other.*

**PROOF.** For each of the six axioms we give an LTSI which satisfies the other five axioms but not the axiom itself. In each case it is straightforward to check that the remaining axioms hold.

SP: Let $t: P \xrightarrow{a} Q$ and $u: P \xrightarrow{b} R$ with $t \lhd u$.

BTI: Let $P \xrightarrow{a} R$ and $Q \xrightarrow{b} R$ with an empty independence relation (Example 3.14).

WF: Let $P_{i+1} \xrightarrow{a} P_i$ for $i = 0, 1, \dots$ with an empty independence relation.

PCI: Let $t: P \xrightarrow{a} Q, u: P \xrightarrow{b} R, u': Q \xrightarrow{b} S, t': R \xrightarrow{a} S$, with $\underline{t'} \lhd \underline{u'}$.

IRE: See Example 5.15.

IEC: See Example 5.16 or Example 5.17.

$\square$

**5.2 CS and CL via independent events**

We now introduce a second version of causal safety and liveness, which uses independence like $CS_i$ and $CL_i$, but on events rather than on transitions. More precisely, we use coinitial independence ci.

*Definition 5.19.* Let $\mathcal{L} = (\text{Proc}, \text{Lab}, \rightarrow, \iota)$ be an LTSI.

(1) We say that $\mathcal{L}$ is *coinitially causally safe* ($CS_{ci}$) if whenever $t_0: P \xrightarrow{a} Q, r: Q \xrightarrow{\rho_*} R$, $\#(r, [t_0]) = 0$ and $t_0^\dagger: S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$, then $[t_0]$ ci $e$ for all events $e$ such that $\#(r, e) > 0$.

(2) We say that $\mathcal{L}$ is *coinitially causally live* ($CL_{ci}$) if whenever $t_0: P \xrightarrow{a} Q, r: Q \xrightarrow{\rho_*} R$ and $\#(r, [t_0]) = 0$ and $[t_0]$ ci $e$, for all events $e$ such that $\#(r, e) > 0$, then we have $t_0^\dagger: S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$.

Note that in Definition 5.19 we operate at the level of events, rather than at the level of transi-
tions as in Definition 5.1. Also note that we could replace $[t_0]$ ci $e$ by $[t_0]$ ci $e$ using Lemma 4.15.
We have used the former for compatibility with Definition 5.1.
<figure><img src="image_9.png" /><figcaption>Fig. 9. The LTSI in Example 5.23.</figcaption></figure>

**Theorem 5.20.** If an LTSI is pre-reversible then it satisfies CS<sub>ci</sub>.

PROOF. Suppose $t_0 : P \xrightarrow{a} Q, r : Q \xrightarrow{\rho_*} R$ and $t_0^\dagger : S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$. By Lemma 4.19 there is a path $s$ from $Q$ to $R$ such that for all $u$ in $s$ we have $[t_0] \text{ ci } [u]$. By CC, $r \approx s$.

Suppose that $e$ is an event and $\#(r, e) > 0$. Then $\#(s, e) > 0$, thanks to Lemma 4.12. Hence there is $u$ in $s$ such that $[u] = e$. Since $[t_0] \text{ ci } [u]$, also $[t_0] \text{ ci } e$. Hence $[t_0] \text{ ci } e$ using Lemma 4.15. $\square$

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

*Definition 5.21. Coinitial IRE (CIRE):* if $[t] \text{ ci } [u]$ and $t, u$ are coinitial then $t \prec u$.

It is easy to see that IRE implies CIRE. By considering Example 5.15 we see that an LTSI can be pre-reversible and satisfy CIRE (and IEC) but not IRE. Also, CIRE is not sufficient to ensure ECh (Definition 5.13) holds, as shown by the next example.

*Example 5.22.* Let $t : P \xrightarrow{a} Q, u : P \xrightarrow{b} R, u' : Q \xrightarrow{b} S, t' : R \xrightarrow{a} S$. We add independence between all pairs of distinct transitions drawn from $t, u, t', u'$. We furthermore add those independent pairs derived from closing under RPI. We see that the LTSI is pre-reversible. It satisfies CIRE and RPI, but not ECh, since $t \sim t'$ and also $t \prec t'$.
$\diamond$

The next example shows that notions of CS/CL based on independence on transitions and on coinitial independence of events are not equivalent.

*Example 5.23.* Consider the LTSI in Figure 9. Independence is given by closing under BTI and PCI. Clearly WF and SP hold; hence the LTSI is pre-reversible and satisfies CS<sub>ci</sub>. There are three events, labelled *a*, *b*, *c*, which are all independent of each other. Furthermore IEC holds, but not CIRE (noting that the leftmost *b* and *c* transitions are coinitial but not independent, while the corresponding events are coinitially independent thanks to the rightmost square). Also CL<sub>ci</sub> fails: consider $P \xrightarrow{a} Q \xrightarrow{b} R$, where *a* cannot be reversed at *R* even though $[Q \xrightarrow{a} P] \text{ ci } [Q \xrightarrow{b} R]$. Differently from CS<sub>ci</sub>, CS<sub>t</sub> fails: e.g., from the leftmost corner one can do *bacb*, reversing *b*, but the inverse of the first *b*-transition is not independent with the *c*-transition. Differently from CL<sub>ci</sub>, CL<sub>t</sub> holds: the only state at which any event that has occurred cannot be immediately reversed is *R*. So we can restrict attention to instances of $P' \xrightarrow{a} Q', r : Q' \xrightarrow{\rho_*} R$. Furthermore *r* must finish with either $Q \xrightarrow{b} R$ or the *c* transition to *R*. These two transitions are not independent with any inverse *a* transition. Hence CL<sub>t</sub> holds in these cases vacuously. $\diamond$

**PROPOSITION 5.24.** Let $\mathcal{L}$ be a pre-reversible LTSI. If $\mathcal{L}$ satisfies CS<sub>t</sub> and RPI then $\mathcal{L}$ also satisfies CIRE.

PROOF. Assume that $\mathcal{L}$ satisfies CS<sub>t</sub>. Suppose that $t, u$ are coinitial transitions such that $[t] \text{ ci } [u]$. We must show that $t \prec u$. We can suppose that at least one of $t$ and $u$ is forward; otherwise we
<figure><img src="image_10.png" /><figcaption>Fig. 9. The LTSI in Example 5.23.</figcaption></figure>

**Theorem 5.20.** If an LTSI is pre-reversible then it satisfies CS<sub>ci</sub>.

PROOF. Suppose $t_0 : P \xrightarrow{a} Q, r : Q \xrightarrow{\rho_*} R$ and $t_0^\dagger : S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$. By Lemma 4.19 there is a path $s$ from $Q$ to $R$ such that for all $u$ in $s$ we have $[t_0] \text{ ci } [u]$. By CC, $r \approx s$.

Suppose that $e$ is an event and $\#(r, e) > 0$. Then $\#(s, e) > 0$, thanks to Lemma 4.12. Hence there is $u$ in $s$ such that $[u] = e$. Since $[t_0] \text{ ci } [u]$, also $[t_0] \text{ ci } e$. Hence $[t_0] \text{ ci } e$ using Lemma 4.15. $\square$

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

*Definition 5.21. Coinitial IRE (CIRE):* if $[t] \text{ ci } [u]$ and $t, u$ are coinitial then $t \prec u$.

It is easy to see that IRE implies CIRE. By considering Example 5.15 we see that an LTSI can be pre-reversible and satisfy CIRE (and IEC) but not IRE. Also, CIRE is not sufficient to ensure ECh (Definition 5.13) holds, as shown by the next example.

*Example 5.22.* Let $t : P \xrightarrow{a} Q, u : P \xrightarrow{b} R, u' : Q \xrightarrow{b} S, t' : R \xrightarrow{a} S$. We add independence between all pairs of distinct transitions drawn from $t, u, t', u'$. We furthermore add those independent pairs derived from closing under RPI. We see that the LTSI is pre-reversible. It satisfies CIRE and RPI, but not ECh, since $t \sim t'$ and also $t \prec t'$.
$\diamond$

The next example shows that notions of CS/CL based on independence on transitions and on coinitial independence of events are not equivalent.

*Example 5.23.* Consider the LTSI in Figure 9. Independence is given by closing under BTI and PCI. Clearly WF and SP hold; hence the LTSI is pre-reversible and satisfies CS<sub>ci</sub>. There are three events, labelled *a*, *b*, *c*, which are all independent of each other. Furthermore IEC holds, but not CIRE (noting that the leftmost *b* and *c* transitions are coinitial but not independent, while the corresponding events are coinitially independent thanks to the rightmost square). Also CL<sub>ci</sub> fails: consider $P \xrightarrow{a} Q \xrightarrow{b} R$, where *a* cannot be reversed at *R* even though $[Q \xrightarrow{a} P] \text{ ci } [Q \xrightarrow{b} R]$. Differently from CS<sub>ci</sub>, CS<sub>t</sub> fails: e.g., from the leftmost corner one can do *bacb*, reversing *b*, but the inverse of the first *b*-transition is not independent with the *c*-transition. Differently from CL<sub>ci</sub>, CL<sub>t</sub> holds: the only state at which any event that has occurred cannot be immediately reversed is *R*. So we can restrict attention to instances of $P' \xrightarrow{a} Q', r : Q' \xrightarrow{\rho_*} R$. Furthermore *r* must finish with either $Q \xrightarrow{b} R$ or the *c* transition to *R*. These two transitions are not independent with any inverse *a* transition. Hence CL<sub>t</sub> holds in these cases vacuously. $\diamond$

**PROPOSITION 5.24.** Let $\mathcal{L}$ be a pre-reversible LTSI. If $\mathcal{L}$ satisfies CS<sub>t</sub> and RPI then $\mathcal{L}$ also satisfies CIRE.

PROOF. Assume that $\mathcal{L}$ satisfies CS<sub>t</sub>. Suppose that $t, u$ are coinitial transitions such that $[t] \text{ ci } [u]$. We must show that $t \prec u$. We can suppose that at least one of $t$ and $u$ is forward; otherwise we
<figure><img src="image_10.png" /><figcaption>Fig. 10. LTSI of Examples 5.32 and 5.25</figcaption></figure>

can obtain $t \prec u$ from BTI. Without loss of generality, suppose that $t : P \xrightarrow{a} Q$ is forward. Since $[t] \text{ ci } [u]$, there are coinitial $t' : P' \xrightarrow{a} Q'$ and $u'$ such that $t \sim t' \prec u' \sim u$. By SP we can complete a square containing $t'$, $u'$ and two further transitions $t'' \sim t'$ and $u'' \sim u'$ both with the same target $R$.

By Lemma 4.19 there is a path $s : Q \xrightarrow{\rho} Q_*$. Let $r' = \underline{t}u\underline{u}ts$ (a path from $Q$ to $Q'$), and consider the path $r = r'u''$ from $Q$ to $R$. We see that $\#(r, [t]) = 0$, using Lemma 4.20 applied to $t, t''$ and $r$. Hence $CS_t$ applies to $t$ together with $r$ and $t''$. We deduce that $\underline{t} \prec u_1$ for all $u_1$ in $r$ such that $\#(r, [u_1]) > 0$. We see that $\#(tr', [u]) = 0$ using Lemma 4.20 applied to $\underline{u}, \underline{u}''$ and $tr'$. Noting that $\text{und}([t]) \neq \text{und}([u])$ by Proposition 4.17, we obtain $\#(r, [u]) = 1$ and so $\underline{t} \prec u$. We deduce $t \prec u$ using RPI. $\square$

We cannot omit the assumption of RPI in Proposition 5.24, in view of the following example.

*Example 5.25.* Consider the ‘half cube’ LTSI with transitions *a*, *b*, *c* in Figure 10. We add independence as given by BTI and PCI, and also between all pairs of transitions *t*, *u* where at least one of *t*, *u* is backward, and *t* ≁ *u*, *t* ≁ *u*. Clearly RPI does not hold. The LTSI is pre-reversible, and IEC holds. CIRE does not hold; note that the *a* and *b*-events are independent, but after performing *c* there are coin initial *a* and *b*-transitions which are not independent. Both $CL_{ci}$ and $CL_t$ hold: note that at any state, all events that have occurred can be reversed immediately. We have ensured that $CS_t$ holds, since all independence deducible from $CS_t$ must involve a backward transition $\underline{t_0}$ and a transition $u$ such that $t_0 \not\prec u$ and $t_0 \not\prec \underline{u}$.
$\diamond$

We can characterise CIRE as being equivalent to coin initial transitions with a common derivative
process being independent.

PROPOSITION 5.26. Let $\mathcal{L}$ be a pre-reversible LTSI. The following are equivalent:

(1) $\mathcal{L}$ satisfies CIRE;

(2) If $t : P \xrightarrow{\alpha} Q, r : Q \xrightarrow{\rho} S$ and $u : P \xrightarrow{\beta} R, s : R \xrightarrow{\sigma} S$ where $\text{und}(\alpha) \neq \text{und}(\beta)$ and $\#(r, [t]) = \#(s, [u]) = 0$ then $t \prec u$.

PROOF. Assume (1). Let $t: P \xrightarrow{\alpha} Q, r: Q \xrightarrow{\rho} S$ and $u: P \xrightarrow{\beta} R, s: R \xrightarrow{\sigma} S$ where $\text{und}(\alpha) \neq \text{und}(\beta)$ and $\#(r, [t]) = \#(s, [u]) = 0$. We must show $t \prec u$. Since the LTSI is pre-reversible, polychotomy holds for events $[t]$ and $[u]$ (Proposition 4.29). We can exclude $[t] = [u]$ since $\text{und}(\alpha) \neq \text{und}(\beta)$. There is a rooted path $r_0$ from some irreversible *I* to *P*. Since NRE holds (Proposition 4.21), $\#(r_0, [t]) = \#(r_0, [u])$. By considering the paths $r_0t$ and $r_0u$ we deduce that neither $[u] < [t]$ nor $[t] < [u]$ hold. By CC applied to $tr$ and $us$ we see that $\#(r, [u]) = 1$. Hence $r_0tr$ is a rooted path with $\#(r_0tr, [t]) = \#(r_0tr, [u]) = 1$, so that we can exclude $[t] \# [u]$. By polychotomy we conclude that $[t] \text{ ci } [u]$. Then $t \prec u$ by CIRE.
<figure><img src="image_11.png" /><figcaption>Fig. 10. LTSI of Examples 5.32 and 5.25</figcaption></figure>

can obtain $t \prec u$ from BTI. Without loss of generality, suppose that $t : P \xrightarrow{a} Q$ is forward. Since $[t] \text{ ci } [u]$, there are coinitial $t' : P' \xrightarrow{a} Q'$ and $u'$ such that $t \sim t' \prec u' \sim u$. By SP we can complete a square containing $t'$, $u'$ and two further transitions $t'' \sim t'$ and $u'' \sim u'$ both with the same target $R$.

By Lemma 4.19 there is a path $s : Q \xrightarrow{\rho} Q_*$. Let $r' = \underline{t}u\underline{u}ts$ (a path from $Q$ to $Q'$), and consider the path $r = r'u''$ from $Q$ to $R$. We see that $\#(r, [t]) = 0$, using Lemma 4.20 applied to $t, t''$ and $r$. Hence $CS_t$ applies to $t$ together with $r$ and $t''$. We deduce that $\underline{t} \prec u_1$ for all $u_1$ in $r$ such that $\#(r, [u_1]) > 0$. We see that $\#(tr', [u]) = 0$ using Lemma 4.20 applied to $\underline{u}, \underline{u}''$ and $tr'$. Noting that $\text{und}([t]) \neq \text{und}([u])$ by Proposition 4.17, we obtain $\#(r, [u]) = 1$ and so $\underline{t} \prec u$. We deduce $t \prec u$ using RPI. $\square$

We cannot omit the assumption of RPI in Proposition 5.24, in view of the following example.

*Example 5.25.* Consider the ‘half cube’ LTSI with transitions *a*, *b*, *c* in Figure 10. We add independence as given by BTI and PCI, and also between all pairs of transitions *t*, *u* where at least one of *t*, *u* is backward, and *t* ≁ *u*, *t* ≁ *u*. Clearly RPI does not hold. The LTSI is pre-reversible, and IEC holds. CIRE does not hold; note that the *a* and *b*-events are independent, but after performing *c* there are coinitial *a* and *b*-transitions which are not independent. Both $CL_{ci}$ and $CL_t$ hold: note that at any state, all events that have occurred can be reversed immediately. We have ensured that $CS_t$ holds, since all independence deducible from $CS_t$ must involve a backward transition $\underline{t_0}$ and a transition $u$ such that $t_0 \not\prec u$ and $t_0 \not\preceq u$.
$\diamond$

We can characterise CIRE as being equivalent to coinitial transitions with a common derivative process being independent.

**PROPOSITION 5.26.** Let $\mathcal{L}$ be a pre-reversible LTSI. The following are equivalent:

(1) $\mathcal{L}$ satisfies CIRE;

(2) If $t : P \xrightarrow{\alpha} Q$, $r : Q \xrightarrow{\rho} S$ and $u : P \xrightarrow{\beta} R$, $s : R \xrightarrow{\sigma} S$ where $\text{und}(\alpha) \neq \text{und}(\beta)$ and $\#(r, [t]) = \#(s, [u]) = 0$ then $t \prec u$.

**PROOF.** Assume (1). Let $t : P \xrightarrow{\alpha} Q$, $r : Q \xrightarrow{\rho} S$ and $u : P \xrightarrow{\beta} R$, $s : R \xrightarrow{\sigma} S$ where $\text{und}(\alpha) \neq \text{und}(\beta)$ and $\#(r, [t]) = \#(s, [u]) = 0$. We must show $t \prec u$. Since the LTSI is pre-reversible, polychotomy holds for events $[t]$ and $[u]$ (Proposition 4.29). We can exclude $[t] = [u]$ since $\text{und}(\alpha) \neq \text{und}(\beta)$. There is a rooted path $r_0$ from some irreversible *I* to *P*. Since NRE holds (Proposition 4.21), $\#(r_0, [t]) = \#(r_0, [u])$. By considering the paths $r_0t$ and $r_0u$ we deduce that neither $[u] < [t]$ nor $[t] < [u]$ hold. By CC applied to *tr* and *us* we see that $\#(r, [u]) = 1$. Hence $r_0tr$ is a rooted path with $\#(r_0tr, [t]) = \#(r_0tr, [u]) = 1$, so that we can exclude $[t] \notin [u]$. By polychotomy we conclude that $[t] \text{ ci } [u]$. Then $t \prec u$ by CIRE.
Assume (2). Let $[t]$ ci $[u]$ where $t: P \xrightarrow{\alpha} Q$ and $u: P \xrightarrow{\beta} R$ are coinital. We must show $t \ı u$.
First note that und($\alpha$) $\ne$ und($\beta$) by Proposition 4.17. We have $t \sim t' \ı u'$ $\sim u$ where $t': P' \xrightarrow{\alpha} Q'$
and $u': P' \xrightarrow{\beta} R'$ are coinital. By SP we have $t'': R' \xrightarrow{\alpha} S$ and $u'': Q' \xrightarrow{\beta} S$. By Lemma 4.19 we
have $r': Q \xrightarrow{\rho_*} Q'$ such that for all $u_1$ in $r'$ we have $[t]$ ci $[u_1]$, and $s': R \xrightarrow{\sigma_*} R'$ such that for
all $u_2$ in $s'$ we have $[u]$ ci $[u_2]$. Let $r = r'u''$ and $s = s't''$. We have $\#(r, [t]) = \#(s, [u]) = 0$ using
Lemma 4.20. Hence $t \ı u$ as required, using the hypothesis.
$\square$

Notably, in the proof of (1) $\Rightarrow$ (2), CIRE is only used in the last step. Hence, the result could be rephrased by stating that any pre-reversible LTSI satisfies (2), with a conclusion of $[t]$ ci $[u]$ rather than $t \ı u$.

The independence result in Proposition 5.18 holds also if we replace IRE by CIRE.

**PROPOSITION 5.27.** The axioms SP, BTI, WF, PCI, CIRE and IEC are independent of each other.

**PROOF.** For each of the six axioms we need to give an LTSI which satisfies the other five axioms but not the axiom itself. Since IRE implies CIRE, for all axioms apart from CIRE we can reuse the examples given in the proof of Proposition 5.18. Example 5.23 provides an LTSI where CIRE fails and the remaining five axioms hold.
$\square$

We can distinguish three mutually exclusive cases for CIRE (Definition 5.21):

**forward case:** both transitions are forward;

**backward-forward case:** one transition is backward, one is forward;

**backward case:** both transitions are backward (implied by BTI).

The second case is particularly relevant for the characterisation of $CL_{ci}$; hence we state it as a separate axiom.

*Definition 5.28. Backward-Forward CIRE (BFCIRE):* if $t: P \xrightarrow{a} Q$ and $u: Q \xrightarrow{b} R$ and $[t]$ ci $[u]$ then $t \ı u$.

Thus BFCIRE is just CIRE specialised to the case where one of the coinital transitions is backward and one is forward. It has some similarity with one of the properties of transition systems with independence in [39] and [47, Definition 4.1], and Sideways Diamond properties in [1, 41]. However, all of these properties state that if two consecutive forward transitions are independent then they are two sides of a commuting diamond.

Analogously to what was done in Theorem 5.6 for $CL_t$, we give below conditions for ensuring $CL_{ci}$. Notably, here BFCIRE is necessary and sufficient, while for $CL_t$ we required IRE, which was sufficient but not necessary.

**Theorem 5.29.** Let $\mathcal{L}$ be a pre-reversible LTSI. Then the following are equivalent:

(1) $\mathcal{L}$ satisfies BFCIRE;

(2) $\mathcal{L}$ satisfies $CL_{ci}$.

**PROOF.** Assume (1). Suppose $t_0: P \xrightarrow{a} Q$, $r: Q \xrightarrow{\rho_*} R$ and $\#(r, [t_0]) = 0$ and $[t_0]$ ci $e$, for all $e$ such that $\#(r, e) > 0$. We have to show that there is $t_0^\dagger: S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$.

Thanks to PL, there is $T$ such that $b: P \xrightarrow{\rho_b}_* T$ and $f: T \xrightarrow{\rho_f}_* R$, with $b$ backward and $f$ forward. By CC, $t_0 r \approx bf$. Since $\#(r, [t_0]) = 0$, thanks to Lemma 4.12 $\#(bf, [t_0]) = 1$. As a consequence, there is a transition $t_0': P' \xrightarrow{a} Q' \in [t_0]$ in $f$ (which is unique by Proposition 4.21). Let $f'$ be the portion of $f$ from $Q'$ to $R$.
Assume (2). Let $[t]$ ci $[u]$ where $t: P \xrightarrow{\alpha} Q$ and $u: P \xrightarrow{\beta} R$ are coinital. We must show $t \ı u$.
First note that und($\alpha$) $\ne$ und($\beta$) by Proposition 4.17. We have $t \sim t' \ı u'$ $\sim u$ where $t': P' \xrightarrow{\alpha} Q'$
and $u': P' \xrightarrow{\beta} R'$ are coinital. By SP we have $t'': R' \xrightarrow{\alpha} S$ and $u'': Q' \xrightarrow{\beta} S$. By Lemma 4.19 we
have $r': Q \xrightarrow{\rho_*} Q'$ such that for all $u_1$ in $r'$ we have $[t]$ ci $[u_1]$, and $s': R \xrightarrow{\sigma_*} R'$ such that for
all $u_2$ in $s'$ we have $[u]$ ci $[u_2]$. Let $r = r'u''$ and $s = s't''$. We have $\#(r, [t]) = \#(s, [u]) = 0$ using
Lemma 4.20. Hence $t \ı u$ as required, using the hypothesis.
$\square$

Notably, in the proof of (1) $\Rightarrow$ (2), CIRE is only used in the last step. Hence, the result could be rephrased by stating that any pre-reversible LTSI satisfies (2), with a conclusion of $[t]$ ci $[u]$ rather than $t \ı u$.

The independence result in Proposition 5.18 holds also if we replace IRE by CIRE.

**PROPOSITION 5.27.** The axioms SP, BTI, WF, PCI, CIRE and IEC are independent of each other.

**PROOF.** For each of the six axioms we need to give an LTSI which satisfies the other five axioms but not the axiom itself. Since IRE implies CIRE, for all axioms apart from CIRE we can reuse the examples given in the proof of Proposition 5.18. Example 5.23 provides an LTSI where CIRE fails and the remaining five axioms hold.
$\square$

We can distinguish three mutually exclusive cases for CIRE (Definition 5.21):

**forward case:** both transitions are forward;

**backward-forward case:** one transition is backward, one is forward;

**backward case:** both transitions are backward (implied by BTI).

The second case is particularly relevant for the characterisation of $CL_{ci}$; hence we state it as a separate axiom.

*Definition 5.28. Backward-Forward CIRE (BFCIRE):* if $t: P \xrightarrow{a} Q$ and $u: Q \xrightarrow{b} R$ and $[t]$ ci $[u]$ then $t \ı u$.

Thus BFCIRE is just CIRE specialised to the case where one of the coinital transitions is backward and one is forward. It has some similarity with one of the properties of transition systems with independence in [39] and [47, Definition 4.1], and Sideways Diamond properties in [1, 41]. However, all of these properties state that if two consecutive forward transitions are independent then they are two sides of a commuting diamond.

Analogously to what was done in Theorem 5.6 for $CL_t$, we give below conditions for ensuring $CL_{ci}$. Notably, here BFCIRE is necessary and sufficient, while for $CL_t$ we required IRE, which was sufficient but not necessary.

**Theorem 5.29.** Let $\mathcal{L}$ be a pre-reversible LTSI. Then the following are equivalent:

(1) $\mathcal{L}$ satisfies BFCIRE;

(2) $\mathcal{L}$ satisfies $CL_{ci}$.

**PROOF.** Assume (1). Suppose $t_0: P \xrightarrow{a} Q$, $r: Q \xrightarrow{\rho_*} R$ and $\#(r, [t_0]) = 0$ and $[t_0]$ ci $e$, for all $e$ such that $\#(r, e) > 0$. We have to show that there is $t_0^\dagger: S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$.

Thanks to PL, there is $T$ such that $b: P \xrightarrow{\rho_b}_* T$ and $f: T \xrightarrow{\rho_f}_* R$, with $b$ backward and $f$ forward. By CC, $t_0 r \approx bf$. Since $\#(r, [t_0]) = 0$, thanks to Lemma 4.12 $\#(bf, [t_0]) = 1$. As a consequence, there is a transition $t_0': P' \xrightarrow{a} Q' \in [t_0]$ in $f$ (which is unique by Proposition 4.21). Let $f'$ be the portion of $f$ from $Q'$ to $R$.
If we can show that $[t_0]$ ci $[t'']$ for each transition $t''$ in $f'$, then the thesis will follow by commuting $t'_0$ with all such transitions using SP and BFCIRE.

By Lemma 4.19 there is a path $s$ from $Q$ to $Q'$ such that $[t_0] \prec [u]$ for all $u$ in $s$. By CC, $r \approx sf'$. Take any $t''$ in $f'$. By Lemma 4.12, $\#(r, [t'']) = \#(s, [t'']) + \#(f', [t''])$. If $\#(s, [t'']) < 0$ then there is $u$ in $s$ such that $u \sim \underline{t''}$. Now $[t_0]$ ci $[u]$, and so $[t_0]$ ci $[t'']$ using Lemma 4.15. So suppose $\#(s, [t'']) \ge 0$. Since $\#(f', [t'']) > 0$, we have $\#(r, [t'']) > 0$. So there is $u$ in $r$ such that $u \sim t''$, and by hypothesis $[t_0]$ ci $[u]$, so that $[t_0]$ ci $[t'']$.

Assume (2). Suppose that $t_0 : P \xrightarrow{a} Q$ and $u : Q \xrightarrow{b} R$ and $[t_0]$ ci $[u]$. Clearly $\#(u, [t_0]) = 0$. By $\mathrm{CL}_{ci}$ we have $t_0^\dagger : S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$. Using BTI and SP we can complete a square starting with $\underline{u}$ and $t_0^\dagger$. Using BLD this square must include $t_0$. Using PCI we see that $t_0 \prec u$ as required. $\square$

$\mathrm{CL}_{ci}$ (and BFCIRE) do not imply CIRE, as shown by Example 5.25.

**LEMMA 5.30.** *Let a pre-reversible LTSI satisfy $CS_i$. Then it satisfies BFCIRE.*

*PROOF.* Suppose $t_0 : P \xrightarrow{a} Q$ and $u : Q \xrightarrow{b} R$ and $[t_0]$ ci $[u]$. We must show that $t_0 \prec u$.

By Lemma 4.15 $[t_0]$ ci $[u]$ and so there are coinital $t'_0 : P' \xrightarrow{a} Q'$ and $u' : P' \xrightarrow{b} R'$ with $t_0 \sim t'_0 \prec u' \sim u$. Using SP we can complete a square with $t_0^\dagger : R' \xrightarrow{a} S'$ and $u'' : Q' \xrightarrow{b} S'$. By Lemma 4.19 applied to $u$ and $u''$ we have a path $s$ from $R$ to $S'$. Let $r = us$. Then $\#(r, [t_0]) = 0$ using Lemma 4.20. Also $\#(s, [u]) = 0$ using Lemma 4.20, so that $\#(r, [u]) > 0$. By $\mathrm{CS}_i$ applied to $t_0, t_0^\dagger$ and $r$ we deduce $\underline{t_0} \prec u$ as required. $\square$

Perhaps surprisingly, we can now relate safety with independence of transitions to liveness with independence of events.

**PROPOSITION 5.31.** *Let a pre-reversible LTSI satisfy $CS_i$. Then it satisfies $\mathrm{CL}_{ci}$.*

*PROOF.* By Lemma 5.30 and Theorem 5.29. $\square$

$\mathrm{CL}_{ci}$ (and BFCIRE) do not imply $\mathrm{CS}_i$, as shown by the next example.

*Example 5.32.* Consider the ‘half cube’ LTSI with transitions $a, b, c$ in Figure 10. We add independence as given by BTI and PCI. The LTSI is pre-reversible. As in Example 5.25, CIRE does not hold while both $\mathrm{CL}_{ci}$ (hence BFCIRE) and $\mathrm{CL}_i$ hold. All pairs of independent transitions are coinital. $\mathrm{CS}_i$ however does not hold: consider $t_0 : P \xrightarrow{c} Q$, $r : Q \xrightarrow{ab}_* R$, $S \xrightarrow{c} R$—here we do not have $t_0 \prec (Q', b, R)$. $\diamond$

**PROPOSITION 5.33.** *Let $\mathcal{L}$ be a pre-reversible LTSI satisfying IEC. If $\mathcal{L}$ satisfies $\mathrm{CL}_{ci}$ then $\mathcal{L}$ satisfies $\mathrm{CL}_i$.*

*PROOF.* Immediate from the definitions. $\square$

We next give an example where CC holds but not $\mathrm{CS}_{ci}$ (and not PCI).

*Example 5.34.* Consider the cube with transitions $a, b, c$ on the left in Figure 11, where the forward direction is from left to right. We add independence as given by BTI. So SP, BTI, WF hold, but not PCI. Consider the bold path from the leftmost end: we have an $a$-transition followed by a path $r = bc$ followed by $\underline{a}$. For $\mathrm{CS}_{ci}$ to hold, we want $\underline{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 (ac and ab). Transitions $b$ and $c$ at P are independent (by BTI) so we obtain $\underline{bc} \approx \underline{cb}$, where $\underline{bc}$ is dashed and $\underline{cb}$ is bold. Since $\approx$ is closed under composition, we get $bc \approx cb$.
If we can show that $[t_0]$ ci $[t'']$ for each transition $t''$ in $f'$, then the thesis will follow by commuting $t'_0$ with all such transitions using SP and BFCIRE.

By Lemma 4.19 there is a path $s$ from $Q$ to $Q'$ such that $[t_0] \prec [u]$ for all $u$ in $s$. By CC, $r \approx sf'$. Take any $t''$ in $f'$. By Lemma 4.12, $\#(r, [t'']) = \#(s, [t'']) + \#(f', [t''])$. If $\#(s, [t'']) < 0$ then there is $u$ in $s$ such that $u \sim \underline{t''}$. Now $[t_0]$ ci $[u]$, and so $[t_0]$ ci $[t'']$ using Lemma 4.15. So suppose $\#(s, [t'']) \ge 0$. Since $\#(f', [t'']) > 0$, we have $\#(r, [t'']) > 0$. So there is $u$ in $r$ such that $u \sim t''$, and by hypothesis $[t_0]$ ci $[u]$, so that $[t_0]$ ci $[t'']$.

Assume (2). Suppose that $t_0 : P \xrightarrow{a} Q$ and $u : Q \xrightarrow{b} R$ and $[t_0]$ ci $[u]$. Clearly $\#(u, [t_0]) = 0$. By $\mathrm{CL}_{ci}$ we have $t_0^\dagger : S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$. Using BTI and SP we can complete a square starting with $\underline{u}$ and $t_0^\dagger$. Using BLD this square must include $t_0$. Using PCI we see that $t_0 \prec u$ as required. $\square$

$\mathrm{CL}_{ci}$ (and BFCIRE) do not imply CIRE, as shown by Example 5.25.

**LEMMA 5.30.** Let a pre-reversible LTSI satisfy $CS_i$. Then it satisfies BFCIRE.

*PROOF.* Suppose $t_0 : P \xrightarrow{a} Q$ and $u : Q \xrightarrow{b} R$ and $[t_0]$ ci $[u]$. We must show that $t_0 \prec u$.

By Lemma 4.15 $[t_0]$ ci $[u]$ and so there are coinital $t'_0 : P' \xrightarrow{a} Q'$ and $u' : P' \xrightarrow{b} R'$ with $t_0 \sim t'_0 \prec u' \sim u$. Using SP we can complete a square with $t_0^\dagger : R' \xrightarrow{a} S'$ and $u'' : Q' \xrightarrow{b} S'$. By Lemma 4.19 applied to $u$ and $u''$ we have a path $s$ from $R$ to $S'$. Let $r = us$. Then $\#(r, [t_0]) = 0$ using Lemma 4.20. Also $\#(s, [u]) = 0$ using Lemma 4.20, so that $\#(r, [u]) > 0$. By $\mathrm{CS}_i$ applied to $t_0, t_0^\dagger$ and $r$ we deduce $\underline{t_0} \prec u$ as required. $\square$

Perhaps surprisingly, we can now relate safety with independence of transitions to liveness with independence of events.

**PROPOSITION 5.31.** Let a pre-reversible LTSI satisfy $CS_i$. Then it satisfies $\mathrm{CL}_{ci}$.

*PROOF.* By Lemma 5.30 and Theorem 5.29. $\square$

$\mathrm{CL}_{ci}$ (and BFCIRE) do not imply $\mathrm{CS}_i$, as shown by the next example.

*Example 5.32.* Consider the ‘half cube’ LTSI with transitions $a, b, c$ in Figure 10. We add independence as given by BTI and PCI. The LTSI is pre-reversible. As in Example 5.25, CIRE does not hold while both $\mathrm{CL}_{ci}$ (hence BFCIRE) and $\mathrm{CL}_i$ hold. All pairs of independent transitions are coinital. $\mathrm{CS}_i$ however does not hold: consider $t_0 : P \xrightarrow{c} Q$, $r : Q \xrightarrow{ab}_* R$, $S \xrightarrow{c} R$—here we do not have $t_0 \prec (Q', b, R)$. $\diamond$

**PROPOSITION 5.33.** Let $\mathcal{L}$ be a pre-reversible LTSI satisfying IEC. If $\mathcal{L}$ satisfies $\mathrm{CL}_{ci}$ then $\mathcal{L}$ satisfies $\mathrm{CL}_i$.

*PROOF.* Immediate from the definitions. $\square$

We next give an example where CC holds but not $\mathrm{CS}_{ci}$ (and not PCI).

*Example 5.34.* Consider the cube with transitions $a, b, c$ on the left in Figure 11, where the forward direction is from left to right. We add independence as given by BTI. So SP, BTI, WF hold, but not PCI. Consider the bold path from the leftmost end: we have an $a$-transition followed by a path $r = bc$ followed by $\underline{a}$. For $\mathrm{CS}_{ci}$ to hold, we want $\underline{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 (ac and ab). Transitions $b$ and $c$ at P are independent (by BTI) so we obtain $\underline{bc} \approx \underline{cb}$, where $\underline{bc}$ is dashed and $\underline{cb}$ is bold. Since $\approx$ is closed under composition, we get $bc \approx cb$.
<figure><img src="image_11.png" /><figcaption>Fig. 11. The LTSIs in Examples 5.34 and 5.35. In the left-hand diagram, forward transitions are from left to right, and we use different line styles to make discussion of the diagram clearer.</figcaption></figure>

However the bold *b* is a different event from the event of the top *bs* since the bold-dashed *bc* face does not have independence at each corner. Therefore we do not get [*a*] ci [*b*] for the bold *a* and bold *b*, and CS<sub>ci</sub> fails. However, we note that we do have [*a*] ci [*b*] for the bold *a* and the dashed *b* since *a* and *b* at *Q* are independent.

We next give an example where $CS_{ci}$ and $CL_{ci}$ hold but not CC.

**Example 5.35.** Consider the LTSI with $Q_i \xrightarrow{b} P_i, P_{i+1} \xrightarrow{c} P_i, Q_{i+1} \xrightarrow{c} Q_i, P_{i+1} \xrightarrow{a} Q_i$ for $i = 0, 1, \dots$. This is shown on the right in Figure 11. Clearly WF does not hold. We add coinital independence to make BTI and PCI hold. Then also SP and CIRE hold. However, CC fails since, for example $P_1 \xrightarrow{a} Q_0 \xrightarrow{b} P_0$ and $P_1 \xrightarrow{c} P_0$ are coinital 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. In more detail, if we have a path *ara* with $\#(r, a) = 0$ then $\#(r, b) = 0$, and if we have a path *brb* with $\#(r, b) = 0$ then $\#(r, a) = 0$. ◇

The independence result in Proposition 5.27 holds also if we replace CIRE by BFCIRE.

**PROPOSITION 5.36.** *The axioms SP, BTI, WF, PCI, BFCIRE and IEC are independent of each other.*

**PROOF.** For each of the six axioms we need to give an LTSI which satisfies the other five axioms but not the axiom itself. Since CIRE implies BFCIRE, for all axioms apart from BFCIRE we can reuse the examples given in the proofs of Proposition 5.27 (and of Proposition 5.18). Example 5.23 provides an LTSI where BFCIRE (equivalent to $CL_{ci}$) fails and the remaining five axioms hold. □

## 5.3 CS and CL via ordering of forward events

We now give definitions of causal safety and causal liveness using ordering on forward events. To this end, we exploit the causality relation $\le$ on such events (see Definition 4.23).

*Definition 5.37.* Let $\mathcal{L} = (\text{Proc}, \text{Lab}, \xrightarrow{\cdot}, t)$ be an LTSI.

(1) We say that $\mathcal{L}$ is *ordered causally safe (CS<sub>≤</sub>)* if whenever $t_0 : P \xrightarrow{a} Q, r : Q \xrightarrow{\rho} * R, \#(r, [t_0]) = 0$ and $t_0^\dagger : S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$, then $[t_0] \not\le e'$ for all forward events $e'$ such that $\#(r, e') > 0$.

(2) We say that $\mathcal{L}$ is *ordered causally live (CL<sub>≤</sub>)* if whenever $t_0 : P \xrightarrow{a} Q, r : Q \xrightarrow{\rho} * R$ and $\#(r, [t_0]) = 0$ and $[t_0] \not\le e'$ for all forward events $e'$ such that $\#(r, e') > 0$ then we have $t_0^\dagger : S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$.
<figure><img src="image_12.png" /><figcaption>Fig. 11. The LTSIs in Examples 5.34 and 5.35. In the left-hand diagram, forward transitions are from left to right, and we use different line styles to make discussion of the diagram clearer.</figcaption></figure>

However the bold *b* is a different event from the event of the top *bs* since the bold-dashed *bc* face does not have independence at each corner. Therefore we do not get [*a*] ci [*b*] for the bold *a* and bold *b*, and CS<sub>ci</sub> fails. However, we note that we do have [*a*] ci [*b*] for the bold *a* and the dashed *b* since *a* and *b* at *Q* are independent.

We next give an example where $CS_{ci}$ and $CL_{ci}$ hold but not CC.

**Example 5.35.** Consider the LTSI with $Q_i \xrightarrow{b} P_i, P_{i+1} \xrightarrow{c} P_i, Q_{i+1} \xrightarrow{c} Q_i, P_{i+1} \xrightarrow{a} Q_i$ for $i = 0, 1, \dots$. This is shown on the right in Figure 11. Clearly WF does not hold. We add coinital independence to make BTI and PCI hold. Then also SP and CIRE hold. However, CC fails since, for example $P_1 \xrightarrow{a} Q_0 \xrightarrow{b} P_0$ and $P_1 \xrightarrow{c} P_0$ are coinital 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. In more detail, if we have a path *ara* with $\#(r, a) = 0$ then $\#(r, b) = 0$, and if we have a path *brb* with $\#(r, b) = 0$ then $\#(r, a) = 0$. ◇

The independence result in Proposition 5.27 holds also if we replace CIRE by BFCIRE.

**PROPOSITION 5.36.** *The axioms SP, BTI, WF, PCI, BFCIRE and IEC are independent of each other.*

**PROOF.** For each of the six axioms we need to give an LTSI which satisfies the other five axioms but not the axiom itself. Since CIRE implies BFCIRE, for all axioms apart from BFCIRE we can reuse the examples given in the proofs of Proposition 5.27 (and of Proposition 5.18). Example 5.23 provides an LTSI where BFCIRE (equivalent to $CL_{ci}$) fails and the remaining five axioms hold. □

## 5.3 CS and CL via ordering of forward events

We now give definitions of causal safety and causal liveness using ordering on forward events. To this end, we exploit the causality relation $\le$ on such events (see Definition 4.23).

*Definition 5.37.* Let $\mathcal{L} = (\text{Proc}, \text{Lab}, \xrightarrow{\cdot}, t)$ be an LTSI.

(1) We say that $\mathcal{L}$ is *ordered causally safe (CS<sub>≤</sub>)* if whenever $t_0 : P \xrightarrow{a} Q, r : Q \xrightarrow{\rho} * R, \#(r, [t_0]) = 0$ and $t_0^\dagger : S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$, then $[t_0] \not\le e'$ for all forward events $e'$ such that $\#(r, e') > 0$.

(2) We say that $\mathcal{L}$ is *ordered causally live (CL<sub>≤</sub>)* if whenever $t_0 : P \xrightarrow{a} Q, r : Q \xrightarrow{\rho} * R$ and $\#(r, [t_0]) = 0$ and $[t_0] \not\le e'$ for all forward events $e'$ such that $\#(r, e') > 0$ then we have $t_0^\dagger : S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$.
The only difference between $CS_{<}$ and $CS_{\vdash}$ (Definition 5.1) is that the former ensures $[t_0] \not\prec [t]$ instead of $t_0 \not\prec t$ for all transitions $t$ such that $[t]$ has a positive number of occurrences in $r$. Similarly for CL. Notably, we do not require $[t_0] \not\prec [t]$ since $<$ is defined on forward events and $t_0$ is forward.

It may seem that the definition above does not take into account backward events that may occur in $r$, but the next lemma shows that such events are necessarily independent from $[t_0]$. This allows us to connect ordered safety and liveness with safety and liveness based on independence of events.

**LEMMA 5.38.** *Suppose that an LTSI is pre-reversible. Suppose $t_0 : P \xrightarrow{a} Q, e = [t_0], r : Q \xrightarrow{\rho}_* R$ and $\#(r, e) = 0$. Let $e'$ be a forward event:*

(1) if $\#(r, e') > 0$ then exactly one of $e$ ci $e'$ and $e < e'$ holds;

(2) if $\#(r, e') < 0$ then $e$ ci $e'$.

**PROOF.** We know that polychotomy holds by Proposition 4.29. Also NRE holds by Proposition 4.21. Suppose $t_0 : P \xrightarrow{a} Q, e = [t_0], r : Q \xrightarrow{\rho}_* R$ and $\#(r, e) = 0$ and $\#(r, e') \neq 0$ where $e'$ is a forward event. We first note that $e \neq e'$, since $\#(r, e) = 0$ and $\#(r, e') \neq 0$. By WF, there is a rooted path $s$ from some irreversible $I$ to $P$.

(1) Suppose first that $\#(r, e') > 0$. Since $\#(st_0r, e) > 0$ and $\#(st_0r, e') > 0$ we do not have $e \# e'$. Furthermore, if $e' < e$ then we must have $\#(s, e') > 0$, so that $\#(st_0r, e') > 1$, contradicting NRE. Then the result follows by polychotomy.

(2) Now suppose that $\#(r, e') < 0$. By Proposition 4.13 we must have $\#(s, e') > 0$. We deduce that $e \not\prec e'$. Since $\#(st_0, e) > 0$ and $\#(st_0, e') > 0$ we do not have $e \# e'$. Furthermore $\#(st_0r, e) > 0$ and $\#(st_0r, e') = 0$ (since $\#(st_0, e') = 1$ combining $\#(st_0, e') > 0$ shown above and NRE). Hence $e' \not\prec e$. By polychotomy, $e$ ci $e'$.
$\square$

**PROPOSITION 5.39.** *Suppose that an LTSI $\mathcal{L}$ is pre-reversible. Then*

(1) $\mathcal{L}$ satisfies $CS_{<}$.

(2) $\mathcal{L}$ satisfies $CL_{ci}$ iff $\mathcal{L}$ satisfies $CL_{<}$.

**PROOF.** (1) We know $CS_{ci}$ holds by Theorem 5.20. Assume that $t_0 : P \xrightarrow{a} Q, e = [t_0], r : Q \xrightarrow{\rho}_* R, \#(r, e) = 0$ and $t_0^{\dagger} : S \xrightarrow{a} R$ with $t_0 \sim t_0^{\dagger}$. Take any forward $e'$ such that $\#(r, e') > 0$. By Lemma 5.38 we know that exactly one of $e$ ci $e'$ or $e < e'$ holds. By $CS_{ci}$ we have $e$ ci $e'$, and therefore $e \not\prec e'$ as required.

(2) Suppose that $CL_{ci}$ holds. Assume that $P \xrightarrow{a} Q, e = [t_0], r : Q \xrightarrow{\rho}_* R$ and $\#(r, e) = 0$ and $e \not\prec e'$ for all forward $e'$ such that $\#(r, e') > 0$. Let event $e'$ be such that $\#(r, e') > 0$. Suppose first that $e'$ is forward. By assumption $e \not\prec e'$. So by Lemma 5.38(1) we obtain $e$ ci $e'$. Suppose instead that $e'$ is reverse, so that $e'$ is forward, and $\#(r, e') < 0$. By Lemma 5.38(2) we obtain $e$ ci $e'$, and hence $e$ ci $e'$ using Lemma 4.15. We deduce that $e$ ci $e'$ for all $e'$ such that $\#(r, e') > 0$. Hence by $CL_{ci}$ we have $t_0^{\dagger} : S \xrightarrow{a} R$ with $t_0 \sim t_0^{\dagger}$.

Conversely, suppose that $CL_{<}$ holds. Assume that $P \xrightarrow{a} Q, e = [t_0], r : Q \xrightarrow{\rho}_* R$ and $\#(r, e) = 0$ and $e$ ci $e'$ for all $e'$ such that $\#(r, e') > 0$. By Lemma 5.38(1) we know that $e \not\prec e'$ for all forward $e'$ such that $\#(r, e') > 0$. Hence by $CL_{<}$ we have $t_0^{\dagger} : S \xrightarrow{a} R$ with $t_0 \sim t_0^{\dagger}$. $\square$

## 5.4 Implications between the different formalisations of CS/CL

We have introduced three different formalisations of causal safety and liveness. The implications between them, assuming pre-reversibility holds, are shown in Figure 12.
The only difference between $CS_{<}$ and $CS_{\vdash}$ (Definition 5.1) is that the former ensures $[t_0] \not\prec [t]$ instead of $t_0 \not\prec t$ for all transitions $t$ such that $[t]$ has a positive number of occurrences in $r$. Similarly for CL. Notably, we do not require $[t_0] \not\prec [t]$ since $<$ is defined on forward events and $t_0$ is forward.

It may seem that the definition above does not take into account backward events that may occur in $r$, but the next lemma shows that such events are necessarily independent from $[t_0]$. This allows us to connect ordered safety and liveness with safety and liveness based on independence of events.

**LEMMA 5.38.** *Suppose that an LTSI is pre-reversible. Suppose $t_0 : P \xrightarrow{a} Q, e = [t_0], r : Q \xrightarrow{\rho}_* R$ and $\#(r, e) = 0$. Let $e'$ be a forward event:*

(1) if $\#(r, e') > 0$ then exactly one of $e$ ci $e'$ and $e < e'$ holds;

(2) if $\#(r, e') < 0$ then $e$ ci $e'$.

**PROOF.** We know that polychotomy holds by Proposition 4.29. Also NRE holds by Proposition 4.21. Suppose $t_0 : P \xrightarrow{a} Q, e = [t_0], r : Q \xrightarrow{\rho}_* R$ and $\#(r, e) = 0$ and $\#(r, e') \neq 0$ where $e'$ is a forward event. We first note that $e \neq e'$, since $\#(r, e) = 0$ and $\#(r, e') \neq 0$. By WF, there is a rooted path $s$ from some irreversible $I$ to $P$.

(1) Suppose first that $\#(r, e') > 0$. Since $\#(st_0r, e) > 0$ and $\#(st_0r, e') > 0$ we do not have $e \# e'$. Furthermore, if $e' < e$ then we must have $\#(s, e') > 0$, so that $\#(st_0r, e') > 1$, contradicting NRE. Then the result follows by polychotomy.

(2) Now suppose that $\#(r, e') < 0$. By Proposition 4.13 we must have $\#(s, e') > 0$. We deduce that $e \not\prec e'$. Since $\#(st_0, e) > 0$ and $\#(st_0, e') > 0$ we do not have $e \# e'$. Furthermore $\#(st_0r, e) > 0$ and $\#(st_0r, e') = 0$ (since $\#(st_0, e') = 1$ combining $\#(st_0, e') > 0$ shown above and NRE). Hence $e' \not\prec e$. By polychotomy, $e$ ci $e'$.
$\square$

**PROPOSITION 5.39.** *Suppose that an LTSI $\mathcal{L}$ is pre-reversible. Then*

(1) $\mathcal{L}$ satisfies $CS_{<}$.

(2) $\mathcal{L}$ satisfies $CL_{ci}$ iff $\mathcal{L}$ satisfies $CL_{<}$.

**PROOF.** (1) We know $CS_{ci}$ holds by Theorem 5.20. Assume that $t_0 : P \xrightarrow{a} Q, e = [t_0], r : Q \xrightarrow{\rho}_* R, \#(r, e) = 0$ and $t_0^\dagger : S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$. Take any forward $e'$ such that $\#(r, e') > 0$. By Lemma 5.38 we know that exactly one of $e$ ci $e'$ or $e < e'$ holds. By $CS_{ci}$ we have $e$ ci $e'$, and therefore $e \not\prec e'$ as required.

(2) Suppose that $CL_{ci}$ holds. Assume that $P \xrightarrow{a} Q, e = [t_0], r : Q \xrightarrow{\rho}_* R$ and $\#(r, e) = 0$ and $e \not\prec e'$ for all forward $e'$ such that $\#(r, e') > 0$. Let event $e'$ be such that $\#(r, e') > 0$. Suppose first that $e'$ is forward. By assumption $e \not\prec e'$. So by Lemma 5.38(1) we obtain $e$ ci $e'$. Suppose instead that $e'$ is reverse, so that $e'$ is forward, and $\#(r, e') < 0$. By Lemma 5.38(2) we obtain $e$ ci $e'$, and hence $e$ ci $e'$ using Lemma 4.15. We deduce that $e$ ci $e'$ for all $e'$ such that $\#(r, e') > 0$. Hence by $CL_{ci}$ we have $t_0^\dagger : S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$.

Conversely, suppose that $CL_{<}$ holds. Assume that $P \xrightarrow{a} Q, e = [t_0], r : Q \xrightarrow{\rho}_* R$ and $\#(r, e) = 0$ and $e$ ci $e'$ for all $e'$ such that $\#(r, e') > 0$. By Lemma 5.38(1) we know that $e \not\prec e'$ for all forward $e'$ such that $\#(r, e') > 0$. Hence by $CL_{<}$ we have $t_0^\dagger : S \xrightarrow{a} R$ with $t_0 \sim t_0^\dagger$. $\square$

## 5.4 Implications between the different formalisations of CS/CL

We have introduced three different formalisations of causal safety and liveness. The implications between them, assuming pre-reversibility holds, are shown in Figure 12.
<figure><img src="image_12.png" /><figcaption>Fig. 12. Implications between causal safety and causal liveness properties and some of the related axioms, all assuming pre-reversibility. Note that both $CS_{ci}$ and $CS_{<}$ are implied by pre-reversibility.</figcaption></figure>

As can be seen in Table 1, only two causal safety properties, namely $CS_{ci}$ and $CS_{<}$, hold for pre-reversible LTSIs. The causal liveness versions of these properties, namely $CL_{ci}$ and $CL_{<}$, additionally require BFCIRE. Actually, BFCIRE is equivalent to both $CL_{ci}$ and $CL_{<}$. The last two properties, $CS_{i}$ and $CL_{i}$, which are defined over general independence of transitions, require IRE. No other implications hold beyond those shown. Counterexamples for lack of other implications in Figure 12 are pointed to in Figure 7.

We postpone discussion of which particular version of CS or CL is most relevant in a specific setting until Section 6.3, after we have introduced some structural axioms to better relate them.

# 6 STRUCTURED NOTIONS OF INDEPENDENCE

In this section we consider two structured notions of independence, namely independence defined on coinitial transitions only and independence determined by labels only. To this end, we introduce ‘structural axioms’ in Definitions 6.1, 6.9 and 6.11. These have a different status from the axioms already introduced: rather than expressing fundamental properties that are desirable in LTSIs, they are properties that hold in various reversible formalisms (as we shall see in Section 7), are easy to verify, and can be used to derive other axioms in a generic fashion.

## 6.1 Coinitial independence

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

*Definition 6.1. Independence is coinitial (IC):* for all transitions *t*, *u*, if *t* ⊢ *u* then *t* and *u* are coinitial.

We say that an LTSI $\mathcal{L}$ is coinitial if it satisfies IC. We also say that its independence relation $|$ is coinitial.

Coinitial independence is of interest since in many cases it is easier to define independence only on coinitial transitions. Indeed, coinitial independence arises, e.g., from the notions of concurrency in [13, Definition 7] for RCCS and in [30, Definition 5] for Core Erlang.
<figure><img src="image_13.png" /><figcaption>Fig. 12. Implications between causal safely and causal liveness properties and some of the related axioms, all assuming pre-reversibility. Note that both $CS_{ci}$ and $CS_{<}$ are implied by pre-reversibility.</figcaption></figure>

As can be seen in Table 1, only two causal safety properties, namely $CS_{ci}$ and $CS_{<}$, hold for pre-reversible LTSIs. The causal liveness versions of these properties, namely $CL_{ci}$ and $CL_{<}$, additionally require BFCIRE. Actually, BFCIRE is equivalent to both $CL_{ci}$ and $CL_{<}$. The last two properties, $CS_{i}$ and $CL_{i}$, which are defined over general independence of transitions, require IRE. No other implications hold beyond those shown. Counterexamples for lack of other implications in Figure 12 are pointed to in Figure 7.

We postpone discussion of which particular version of CS or CL is most relevant in a specific setting until Section 6.3, after we have introduced some structural axioms to better relate them.

# 6 STRUCTURED NOTIONS OF INDEPENDENCE

In this section we consider two structured notions of independence, namely independence defined on coinitial transitions only and independence determined by labels only. To this end, we introduce 'structural axioms' in Definitions 6.1, 6.9 and 6.11. These have a different status from the axioms already introduced: rather than expressing fundamental properties that are desirable in LTSIs, they are properties that hold in various reversible formalisms (as we shall see in Section 7), are easy to verify, and can be used to derive other axioms in a generic fashion.

## 6.1 Coinitial independence

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

*Definition 6.1. Independence is coinitial (IC):* for all transitions *t*, *u*, if *t* ⊢ *u* then *t* and *u* are coinitial.

We say that an LTSI $\mathcal{L}$ is coinitial if it satisfies IC. We also say that its independence relation $|$ is coinitial.

Coinitial independence is of interest since in many cases it is easier to define independence only on coinitial transitions. Indeed, coinitial independence arises, e.g., from the notions of concurrency in [13, Definition 7] for RCCS and in [30, Definition 5] for Core Erlang.
<figure><img src="image_13.png" /><figcaption>Fig. 13. The LTSI in Example 6.2.</figcaption></figure>

The next example satisfies IC and all and only the properties in Figure 7 implied by it. In particular, it shows that IC does not imply $CL_t$, $CL_{ci}$, or $CS_t$ (this last follows from Proposition 5.31).

**Example 6.2.** Consider the LTSI in Figure 13. Independence between transitions is generated by applying BTI and PCI and, as such, is coinicial as in Definition 6.1. Moreover, the LTSI is pre-reversible. There are three events, which we denote by $e_a, e_b, e_c$, with labels $a, b, c$, respectively. $CL_t$ fails: let $t: P \xrightarrow{a} Q$ and let $r$ from $Q$ to $R$ be $\underline{bb}$ (dashed transitions). We have $\nabla(r, e_b) = 0$; however $a$ cannot be reversed at $R$, as $CL_t$ would yield. Also $CS_t$ fails: let $t: P \xrightarrow{a} Q$ and let $r'$ be $\underline{c\underline{b}}$ from $Q$ to $S$ (bold transitions). After $r'$, $\underline{a}$ is possible. However $\underline{t}$ is not independent with the $\underline{b}$ transition, as $CS_t$ would yield. Also $CL_{ci}$ fails: let $t_0$ be the $a$ following the leftmost $b$, and let $r''$ be the $c$ transition with target $R$. We have $e_a$ ci $e_c$. However $a$ cannot be reversed at $R$, as $CL_{ci}$ would yield. ◇

Coinicial independence is inconsistent with the axiom IRE, showing that IRE is only appropriate for the setting of general, rather than coinicial independence:

**PROPOSITION 6.3.** Let a pre-reversible LTSI have a non-empty independence relation, and satisfy IC. Then IRE does not hold.

**PROOF.** Suppose for a contradiction that IRE holds. Since the independence relation is non-empty and IC holds, we have $t \prec u$ with $t, u$ coinicial. By SP and PCI we can complete a diamond with $t' \sim t, u' \sim u$. Since $t' \sim t \prec u$ we deduce by IRE that $t' \prec u$. However $t'$ and $u$ are not coinicial, contradicting IC. □

We define a mapping $c$ restricting general independence to coinicial transitions and a mapping $g$ extending independence along events.

**Definition 6.4.** Given an LTSI $\mathcal{L}$, define $t g(t) u$ iff $t \sim t' \prec u'$ $u$ for some $t', u'$. Furthermore, define $t c(t) u$ iff $t \prec u$ and $t, u$ are coinicial.

We extend $c$ and $g$ to LTSIs (Proc, Lab, $\rightarrow, \prec$): they behave as the identity of the first three components, and as expected on the fourth. Similarly, we write $c(\sim)$ and $g(\sim)$ for the equivalence relations in $c(\mathcal{L})$ and $g(\mathcal{L})$, respectively.

We now show that $c$ and $g$ play well with events.

**LEMMA 6.5.** Given an LTSI $\mathcal{L}$, $\sim = c(\sim)$.

**PROOF.** Follows by noticing that the definition of event only exploits independence on coinicial transitions. □
<figure><img src="image_14.png" /><figcaption>Fig. 13. The LTSI in Example 6.2.</figcaption></figure>

The next example satisfies IC and all and only the properties in Figure 7 implied by it. In particular, it shows that IC does not imply $CL_t$, $CL_{ci}$, or $CS_t$ (this last follows from Proposition 5.31).

**Example 6.2.** Consider the LTSI in Figure 13. Independence between transitions is generated by applying BTI and PCI and, as such, is coinicial as in Definition 6.1. Moreover, the LTSI is pre-reversible. There are three events, which we denote by $e_a, e_b, e_c$, with labels $a, b, c$, respectively. $CL_t$ fails: let $t: P \xrightarrow{a} Q$ and let $r$ from $Q$ to $R$ be $\underline{bb}$ (dashed transitions). We have $\nabla(r, e_b) = 0$; however $a$ cannot be reversed at $R$, as $CL_t$ would yield. Also $CS_t$ fails: let $t: P \xrightarrow{a} Q$ and let $r'$ be $\underline{c\underline{b}}$ from $Q$ to $S$ (bold transitions). After $r'$, $\underline{a}$ is possible. However $\underline{t}$ is not independent with the $\underline{b}$ transition, as $CS_t$ would yield. Also $CL_{ci}$ fails: let $t_0$ be the $a$ following the leftmost $b$, and let $r''$ be the $c$ transition with target $R$. We have $e_a$ ci $e_c$. However $a$ cannot be reversed at $R$, as $CL_{ci}$ would yield. ◇

Coinicial independence is inconsistent with the axiom IRE, showing that IRE is only appropriate for the setting of general, rather than coinicial independence:

**PROPOSITION 6.3.** Let a pre-reversible LTSI have a non-empty independence relation, and satisfy IC. Then IRE does not hold.

**PROOF.** Suppose for a contradiction that IRE holds. Since the independence relation is non-empty and IC holds, we have $t \prec u$ with $t, u$ coinicial. By SP and PCI we can complete a diamond with $t' \sim t, u' \sim u$. Since $t' \sim t \prec u$ we deduce by IRE that $t' \prec u$. However $t'$ and $u$ are not coinicial, contradicting IC. □

We define a mapping $c$ restricting general independence to coinicial transitions and a mapping $g$ extending independence along events.

**Definition 6.4.** Given an LTSI $\mathcal{L}$, define $t g(t) u$ iff $t \sim t' \prec u'$ $u$ for some $t', u'$. Furthermore, define $t c(t) u$ iff $t \prec u$ and $t, u$ are coinicial.

We extend $c$ and $g$ to LTSIs (Proc, Lab, $\rightarrow, \prec$): they behave as the identity of the first three components, and as expected on the fourth. Similarly, we write $c(\sim)$ and $g(\sim)$ for the equivalence relations in $c(\mathcal{L})$ and $g(\mathcal{L})$, respectively.

We now show that $c$ and $g$ play well with events.

**LEMMA 6.5.** Given an LTSI $\mathcal{L}$, $\sim = c(\sim)$.

**PROOF.** Follows by noticing that the definition of event only exploits independence on coinicial transitions. □
**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}, \rightarrow, \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).