# Relating Reversible Petri Nets and Reversible Event Structures, Categorically

Hernán Melgratti, Claudio Antares Mezzina, G. Michele Pinna

► To cite this version:

Hernán Melgratti, Claudio Antares Mezzina, G. Michele Pinna. Relating Reversible Petri Nets and Reversible Event Structures, Categorically. 43th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2023, Lisbon, Portugal. pp.206-223, 10.1007/978-3-031-35355-0_13 . hal-04731933

HAL Id: hal-04731933

https://inria.hal.science/hal-04731933v1

Submitted on 11 Oct 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
<figure><img src="image_2.png" /></figure>

ifip

International Federation for Information Processing

This document is the original author manuscript of a paper submitted to an IFIP
conference proceedings or other IFIP publication by Springer Nature. As such, there
may be some differences in the official published version of the paper. Such
differences, if any, are usually due to reformatting during preparation for publication or
minor corrections made by the author(s) during final proofreading of the publication
manuscript.
Relating Reversible Petri Nets
and Reversible Event Structures,
Categorically

Hernán Melgratti¹(✉), Claudio Antares Mezzina²(✉), and G. Michele Pinna³(✉)

¹ ICC - Universidad de Buenos Aires, Buenos Aires, Argentina
hmelgra@dc.uba.ar

² Dipartimento di Scienze Pure e Applicate, Università di Urbino, Urbino, Italy
claudio.mezzina@uniurb.it

³ Dipartimento di Matematica e Informatica, Università di Cagliari, Cagliari, Italy
gmpinna@unica.it

**Abstract.** Causal nets (CNs) are Petri nets where causal dependencies are modelled via inhibitor arcs. They play the role of occurrence nets when representing the behaviour of a concurrent and distributed system, even when reversibility is considered. In this paper we extend CNs to account also for asymmetric conflicts and study (i) how this kind of nets, and their reversible versions, can be turned into a category; and (ii) their relation with the categories of reversible asymmetric event structures.

# 1 Introduction

Reversible models of concurrent computation [1] have gained momentum in recent years, as witnessed by the variety of models available today: RCCS [6], CCSK [22], rhoπ [10], Rπ [5], reversible Petri nets [15], reversible event structures [20], to name a few. As expected, the attention has turned to the question of how these models relate to each other (see e.g. [9, 12, 13]). This work addresses such goal by revisiting, in the context of reversibility, the connection between *Event Structures* (ESes) [24] and *Petri Nets* (PNs) established by Winskel [17].

*Reversible Asymmetric Event Structures* (RAESes) [20] are a reversible counterpart of *Asymmetric Event Structures* (AESes) [3], which in turn are a generalisation of *Prime Event Structures* (PEEs) [17]. A PES describes a computational process as a set of events whose occurrence is constrained by two relations:

This work has been supported by the Italian MUR PRIN 2020 project *NiRvAna*, the French ANR project ANR-18-CE25-0007 *DCore*, the INdAM-GNCS project CUP_E55F22000270001 *Proprietà Qualitative e Quantitative di Sistemi Reversibili*, and the European Union - NextGenerationEU program Research and Innovation Program PE00000014 *SEcurity and RIghts in the CyberSpace* (SERICS), projects *Secure and TRaceable Identities in Distributed Environments* (STRIDE) and *Securing softWare frOm first PrincipleS* (SWOPS), the EU H2020 RISE programme under the Marie Skłodowska-Curie grant agreement 778233, UBACyT projects 202020170100544BA and 202020170100086BA.
<figure><img src="image_3.png" /><figcaption>Fig. 1. PES, AES, rAES and their transition systems.</figcaption></figure>

causality and (symmetric) conflicts. A simple PES is depicted in Fig. 1a, where causality ($<$) is drawn with straight lines (to be read from bottom to top) and conflicts (#) with curly lines. In this PES, *b* causally depends on *a* (i.e., *a* < *b*): *b* cannot occur if *a* does not occur first; additionally, *b* and *c* are in conflict (i.e., *b#c*): *b* and *c* are mutually exclusive and cannot occur in the same execution of the process. The behaviour of a PES can be understood in terms of a transition system defined over configurations (i.e., sets of events), as illustrated in Fig. 1b. For instance, the transition $\emptyset \to \{a, c\}$ indicates that the initial state $\emptyset$ (i.e., no event has been executed yet) may evolve to $\{a, c\}$ by concurrently executing *a* and *c*. Neither $\{b\}$ nor $\{a, b, c\}$ are configurations because *b* cannot occur without *a*; and *b* and *c* cannot happen in the same run.

In order to accommodate asymmetries that may arise, e.g., in shared-memory concurrency, AESes relax the notion of conflicts by considering weak causality. Intuitively, an event *e* weakly causes the event *e'* (written *e* ↗ *e'* if *e'* can happen after *e* but *e* cannot happen after *e'*. This can be considered as an asymmetric conflict because *e'* forbids *e* to take place, but not the other way round. Symmetric conflicts can be recovered by making a pair of conflicting events to weakly cause each other. The PES P in Fig. 1a can be rendered as the AES G in Fig. 1c, where weak causality is depicted with red, dashed arrows. Now the conflict between *b* and *c* is represented as $b \nearrow c$ and $c \nearrow b$. Unsurprisingly, the transition system associated with G coincides with that of P in Fig. 1b. Differently, the AES G' relaxes the conflict between *b* and *c* by making it asymmetric: we keep $b \nearrow c$ but drop $c \nearrow b$. Now *c* can be added to the configuration $\{a, b\}$ but *b* cannot be added to $\{a, c\}$, as rendered by the transition system in Fig. 1e.

A reversible model embodies two different flows of computation: the *forward* one and the *backward* one, which undoes the effects of the forward one. In rAESes, the backward flow is described in terms of a set of reversing events, each of them representing the undoing of some event of the forward flow. Two relations, dubbed *reverse causation* ($\prec$) and *prevention* ($\succ$), describe the backward flow and regulate the way in which reversing events occur: $\prec$ prescribes the events required for the undoing while $\succ$ stipulates those that preclude it. The rAES H in
Fig. 1f extends $G'$ with a backward flow represented by blue arrows: solid arrows correspond to reverse causation and dashed ones to prevention. Then, $a \prec \underline{a}$ says that $\underline{a}$ can be executed (meaning $a$ can be undone) only when $a$ has occurred. Prevention $\underline{a} \triangleleft c$ states that $a$ can be reversed only if $c$ has not occurred. The transition system of $\mathcal{H}$ is in Fig. 1g. Interestingly, $a$ can be reversed in $\{a, b\}$ leading to $\{b\}$, which is not reachable by the forward flow (black arrows). This is known as out-of-causal order reversibility [21].

Event structures have played a central role in developing denotational semantics for PNs [24]. It is well-known that different classes of ESes correspond to different classes of PNs [3,4,24] and that different relations in ESes translate into different operational mechanisms of PNs. Causality and conflicts are typically modelled in nets via places *shared* among transitions. However, shared places fall short when translating other kinds of dependencies, such as weak causality, which require contextual arcs [3]. Reversible ESes have introduced further questions about the required features of their operational counterpart, suggesting that shared places are not always a suitable choice ([13, 18, 19]). It has been shown that the operational model of (reversible) PESes can be recovered as a subclass of contextual Petri nets, called (*reversible*) *Causal Nets* (rCNs), in which causality is modelled via inhibitor arc instead of using a shared place in which one transition produces a token that another one consumes [13]. Inhibitor arcs neither produce nor consume tokens but check for the *absence* of them. This idea is rendered by the nets in Fig. 2. We recall that a PN gives an operational description of a computation in terms of *transitions* (boxes) that consume and produce *tokens* (bullets) in different *places* (circles). According to the black arrows in Fig. 2a, the transition *a* consumes a token from $s_1$ producing a token in $s_4$; similarly *b* consumes from $s_4$, $s_2$ and $s_3$ producing in $s_5$. Note that *b* and *c* are in mutual exclusion (i.e., conflict) because they both compete for the shared resource (i.e., token) in $s_3$. The arc connecting $s_4$ to *b* indicates that *b* cannot be fired if $s_4$ does not contain any token; consequently, *b* can happen only after *a* has produced the token in $s_4$. The causal relation between *a* and *b* arises because of $s_4$. The ES $P$ in Fig. 1a corresponds to $N_P$ in Fig. 2a. Causality and conflicts in $N_P$ could be represented instead via inhibitor arcs, as shown in Fig. 2b. The inhibitor arc (depicted as a red line ending with a circle) between $s_1$ and *b* models $a < b$, whereas the inhibitor arcs $(s_5, c)$ and $(s_6, b)$ represent the symmetric conflict between *b* and *c*. A reversible version of the net in Fig. 2b is obtained by adding a reversing transition for each reversible event, as shown in Fig. 2c (in gray). The added transitions $\underline{a}$ and $\underline{b}$ respectively reverse the effects of *a* and *b*: each of them consumes (produces) the tokens produced (resp., consumed) by the associated forward transition. Inhibitor arcs model also reverse causation and prevention as, e.g., the inhibitor arc connecting $\underline{a}$ with $s_6$ stands for $\underline{a} \triangleleft c$.

In this paper we generalise the results in [13] to deal with rAESes. We use inhibitor arcs for representing, not only causal dependencies, but also (symmetric) conflicts. Hence, all the dependencies are modelled *uniformly* via inhibitor arcs. We identify a subclass of rCNes, dubbed *reversible Asymmetric Causal Nets* (rACNES), which are the operational counterpart of rAESes. We show that the correspondence is tight and it is expressed in categorical terms (following
<figure><img src="image_4.png" /><figcaption>Fig. 2. Occurrence net $N_P$ and (Reversible) causal nets $N_R$ and $N'_R$</figcaption></figure>

the literature [17,24,25]). We first turn rAESes and rACNes into categories by providing suitable notions of morphisms. Then, we relate both categories via two functors. We show that the functor that associates rAESes with rACNes is the left adjoint of the one that gives rACNes out of rAESes.

## 2 Reversible Asymmetric Event Structures

In this section we recall the basics of Asymmetric Event Structures (AESes) [3] and their reversible version [8,20].

An AES consists of a set of events and two relations: causality ($<$) and weak causality or precedence ($\nearrow$). If $e$ weakly causes $e'$, written $e \nearrow e'$, then $e$ cannot occur after $e'$; i.e., if both events occur in a computation, then $e$ precedes $e'$. In this case we say that $e'$ is in an asymmetric conflict with $e$. Events $e$ and $e'$ are in (symmetric) conflict, written $e \# e'$, iff $e \nearrow e'$ and $e' \nearrow e$; intuitively, they cannot take place in the same computation.

**Definition 1.** An Asymmetric ES (AES) is a triple $G = (E, <, \nearrow)$ where

1. $E$ is a countable set of events;

2. $< \subseteq E \times E$ is an irreflexive partial order, called causality, defined such that $\forall e \in E$. $\lfloor e \rfloor = \{e' \in E \mid e' \le e\}$ is finite; and

3. $\nearrow \subseteq E \times E$, called weak causality, is defined such that for all $e, e' \in E$:

(a) $e < e' \Rightarrow e \nearrow e'$;

(b) $\nearrow \cap (\lfloor e \rfloor \times \lfloor e' \rfloor)$ is acyclic; and

(c) if $e \# e'$ and $e' < e''$ then $e \# e''$.

Each event has a finite set of causes (2). Moreover, weak causality is consistent with causality: if $e$ is a cause of $e'$, then $e$ is also a weak cause of $e'$ (3a); and there cannot be circular dependencies on the causes of an event (3b). Finally, (symmetric) conflicts (#) are required to be inherited along causality (3c).

**Example 1.** Each event of the AES in Fig. 3a has a finite set of causes, i.e., $\lfloor c \rfloor = \{a, b, c\}$, $\lfloor a \rfloor = \{a\}$ and $\lfloor b \rfloor = \{b\}$. Also $a < c$ implies $a \nearrow c$ and $b < c$ implies $b \nearrow c$. Moreover, $\nearrow$ is acyclic on $\lfloor a \rfloor$, $\lfloor b \rfloor$ and $\lfloor c \rfloor$; and $G$ does not have any symmetric conflict. On the contrary, the weak causality relation of the AES $G'$ in Fig. 3b induces symmetric conflicts, i.e. $b \#'a$ and $b \#'c$. Such conflicts are inherited along causality, i.e. $b \#'a$ and $a < c$ imply $b \#'c$.
<figure><img src="image_5.png" /><figcaption>Fig. 3. Two AESes and their configurations</figcaption></figure>

**Definition 2.** A configuration of an AES $G$ is a set $X$ of events such that

1. $\frown$ is well-founded on $X$ (events are not in conflict),

2. $\forall e \in X. \lfloor e \rfloor \subseteq X$ (it contains all the causes for each event); and

3. $\forall e \in X. \{e' \in X \mid e' \frown e\}$ is finite (events have finite sets of weak causes).

We write $\text{Conf}_{\text{AES}}(G)$ for the configurations of $G$. The configurations of the AESes $G$ and $G'$ in Example 1 are shown in Figs. 3c and 3d, respectively.

**Definition 3.** An AES-morphism $f: G_0 \to G_1$ is a partial function $f: E_0 \to E_1$ such that for all $e, e' \in E_0$

1. if $f(e) \neq \perp$ then $\lfloor f(e) \rfloor \subseteq f(\lfloor e \rfloor)$; and

2. if $f(e) \neq \perp \neq f(e')$ then

(a) $f(e) \frown_1 f(e') \Rightarrow e \frown_0 e'$; and

(b) $f(e) = f(e') \wedge e \neq e' \Rightarrow e \#_0 e'$.

AES-morphisms preserve causes (condition 1) and reflect weak causes (condition 2a). If two different events $e$ and $e'$ are mapped to the same event then they are in conflict (condition 2b).

We remark that AES-morphisms preserve computations (i.e., configurations), i.e. if $X \in \text{Conf}_{\text{AES}}(G_0)$, then $f(X) \in \text{Conf}_{\text{AES}}(G_1)$ [3]. Since AES-morphisms compose [3], we write **AES** for the category of AESes and AES-morphisms.

We now summarise the reversible AESes introduced in [8, 20]. Let $U$ be a set of events and $u \in U$ an event, we write $\underline{u}$ for the undoing of $u$, and $\underline{U} = \{\underline{u} \mid u \in U\}$ for undoings of $U$.

**Definition 4.** A Reversible AES is a sextuple $H = (E, U, <, \frown, \prec, \triangleleft)$ where $E$ is the set of events, $U \subseteq E$ is the set of reversible events, and

1. $\frown \subseteq E \times E$, called weak causality;

2. $\triangleleft \subseteq \underline{U} \times E$, called prevention;

3. $< \subseteq E \times E$, called causation, is an irreflexive relation defined such that for all $e \in E, \lfloor e \rfloor < = \{e' \in E \mid e' \le e\}$ is finite and $(\frown \cup <)$ is acyclic on $\lfloor e \rfloor <$;

4. $< \subseteq E \times \underline{U}$, called reverse causation, is defined such that

(a) $\forall u \in U. u \prec \underline{u}$;

(b) for all $u \in U, \lfloor u \rfloor < = \{e \in E \mid e \prec \underline{u}\}$ is finite and $(\frown \cup <)$ is acyclic on $\lfloor e \rfloor <$;

5. for all $e \in E, \underline{u} \in U. e \prec \underline{u} \Rightarrow \neg(\underline{u} \triangleleft e)$; and

6. $(E, \prec, \frown)$ with $\prec = < \cap \{(e, e') \mid e \notin U \text{ or } \underline{e} \triangleleft e'\}$ is an AES.
<figure><img src="image_6.png" /><figcaption>Fig. 4. Two rAESes and their configurations</figcaption></figure>

An rAES is defined in terms of a set of events $E$; the ones in $U$ are reversible. Causation ($<$) and weak causality ($\nearrow$) specify the forward flow, while reverse causation ($<$, drawn as solid blue arrows) and prevention ($<$, as dashed blue arrows) describe the backward flow. Weak causality plays the same role as in AESes: $e \nearrow e'$ states that $e$ cannot occur after $e'$. Prevention constrains the undoing of events: $e \nleq e'$ indicates that $e$ cannot be undone if $e'$ has occurred. Causation (like causality in AESes) indicates causal dependencies. As in AESes, every event has a finite set of causes $\lceil e \rceil_{<}$, which does not contain cyclic dependencies according to $< \cup \nearrow$ (Condition 3). Acyclicity of $\lceil e \rceil_{<}$ implies that for all $e, e' \in E$. $e < e' \Rightarrow \neg(e' \nearrow e)$. Reverse causation specifies the causes for the undoing of each event: $e \prec e'$ states that $e'$ can be undone only if $e$ has occurred. Hence, condition 4a simply states that an event $u$ can be undone only if it has occurred. Condition 4b establishes that each undoing has a finite set of causes. Condition 5 requires causation and weak causality to be consistent, i.e. an event cannot have precedence over some of its causes. Note that the definition does not require $(E, <, \nearrow)$ to be an AES, because conflicts may not be inherited along causation. Condition 6 relies instead on the sustained causation relation $\prec$, which is obtained from $<$ by removing those pairs $e < e'$ where $e$ can be undone even when $e'$ has occurred (i.e., when $e \nleq e'$ does not hold). This is essential for accommodating out-of-causal order reversibility (see the example below). When $U = \emptyset$, $\prec$ coincides with $<$ and $(E, \emptyset, <, \nearrow, \emptyset, \emptyset)$ is indeed an AES.<fnref n="1" />

*Example 2.* Consider the rAES $\mathbf{H}$ in Fig. 4a. The (forward) events are $\{a, b, c\}$, with $b$ reversible (i.e. $U = \{b\}$). Causation is such that $a < c$ and $b < c$, and weak causality states $a \nearrow c$, $b \nearrow c$, and $b \nearrow a$. Hence, $c$ is caused by $a$ and $b$, and $b$ is a weak cause of $a$. Reverse causation is such that $a \prec b$ and $b \prec b$, while prevention states that $b \nleq c$. Hence, $b$ can be reversed when $a$ is present and $c$ has not been executed. Sustained causation coincides with causation, because $b$ cannot be reversed when $c$, which causally depends on $b$, is present.

The rAES $\mathbf{H}'$ in Fig. 4b has the same events of $\mathbf{H}$ as well as the same causation and weak causality. In this case, both $b$ and $c$ are reversible, and reverse causation establishes also that $c \prec' \underline{c}$ (in addition to $a \prec' b$ and $b \prec' b$). Prevention is empty. Hence, $b$ can be reversed even when $c$, which causally depends on $b$, has occurred. The sustained causation in $\mathbf{H}'$ consists only of $a \prec' c$, i.e. the pair

<footnote n="1">¹ Definition 4 differs in style from the one in [20] where $<$ and $\prec$ are glued in one relation as also are $\nearrow$ and $\nleq$. We explicitly require $(E, \prec, \nearrow)$ to be an AES instead of restating conditions. The correspondence is straightforward.</footnote>
$b < c$ is removed because $b$ can be reversed despite $c$ has occurred, which is an out-of-causal order reversibility.

The definition for configurations of rAESes has an operational flavour, which relies on the notion of enabling. Let $\mathsf{H} = (E, U, <, \uparrow, \prec, \triangleleft)$ be an rAES and $X \subseteq E$ a set of events such that $\uparrow$ is acyclic on $X$. For $A \subseteq E$ and $B \subseteq U$, we say $A \cup B$ is enabled at $X$ if $A \cap X = \emptyset$, $B \subseteq X$, $\uparrow$ is acyclic on $A \cup X$ and

1. for every $e \in A$, if $e' < e$ then $e' \in X \setminus B$ and if $e \uparrow e'$ then $e' \notin X \cup A$; and

2. for every $u \in B$, if $e' \prec u$ then $e' \in X \setminus (B \setminus \{u\})$ and if $u \triangleleft e'$ then $e' \notin X \cup A$.

Thus $X$ must contain all the causes of the events in $A$ (to be added) and none of their preventing events. Furthermore $X$ must contain all the reverse causes of the events in $B$ (to be undone) and none of their preventing ones. If $A \cup B$ is enabled at $X$ then $X' = (X \setminus B) \cup A$ can be reached from $X$, written $X \xrightarrow{A \cup B} X'$.

Let $\mathsf{H}$ be an rAES and $X$ a set of events that is well-founded with respect to $(\uparrow \cup <)$. We say $X$ is a (reachable) configuration if there exist a sequences of pairs of sets $A_i$ and $B_i$, for $i = 1, \dots, n$, such that

- $A_i \subseteq E$ and $B_i \subseteq U$ for all $i$, and

- $X_i \xrightarrow{A_i \cup B_i} X_{i+1} \quad X_1 = \emptyset$ and $X_{n+1} = X$.

The set of configurations of $\mathsf{H}$ is denoted by $\text{Conf}_{r\text{AES}}(\mathsf{H})$.

*Example 3.* The configurations of the rAESes in the Example 2 (and how they are reached) are depicted in Figs. 4c and 4d. Note that $\{a, c\}$ is a configuration of $\mathsf{H}'$ but not of $\mathsf{H}$. It can be reached from $\{a, b, c\}$ by the undoing of $b$.

**Definition 5.** Let $\mathsf{H}_1$ and $\mathsf{H}_2$ be rAESes. An rAES-morphism $f: \mathsf{H}_0 \to \mathsf{H}_1$ is an AES-morphism $f: (E_0, <_0, \uparrow'_0) \to (E_1, <_1, \uparrow'_1)$ such that

- $f(U_0) \subseteq U_1$;

- for all $u \in U_0$, if $f(u) \neq \perp$ then $\lfloor f(u) \rfloor_{<_1} \subseteq f(\lfloor u \rfloor_{<_0})$; and

- for all $e \in E_0$ and $u \in U_0$, if $f(e) \neq \perp \neq f(u)$ then $f(u) \triangleleft_1 e$ ($f(u) \triangleleft_0 e$).

Recall that rAES-morphisms preserve causes (and reverse causes) of events (resp., reversing events), and reflect prevention. Hence, they preserve behaviour, i.e. if $X \in \text{Conf}_{r\text{AES}}(\mathsf{H}_0)$ then $f(X) \in \text{Conf}_{r\text{AES}}(\mathsf{H}_1)$.

As shown in [8], rAES-morphisms compose; hence rAESes and rAES-morphisms form a category, denoted by **RAES**. Moreover, **AES** is a full and faithful sub-category of **RAES**.

## 3 Nets with Inhibitor Arcs

We summarise the basics of Petri net with inhibitor arcs along the lines of [2, 16]. A *multiset* over a set $A$ is a function $m: A \to \mathbb{N}$, with $\mathbb{N}$ the natural numbers. We assume the usual operations of union (+) and difference (−) on multisets, and write $m \subseteq m'$ if $m(a) \le m'(a)$ for all $a \in A$. We write $\llbracket m \rrbracket$ for the underlying set of $m$, 0 for the multiset with empty underlying set, and $\mu A$ for the set of all multisets over $A$.
<figure><img src="image_7.png" /><figcaption>Fig. 5. Some simple IPTs</figcaption></figure>

**Definition 6.** A Petri net with inhibitor arcs (IPT for short) is a tuple $N = \langle S, T, F, I, m \rangle$, where $S$ is a set of places, $T$ is a set of transitions such that $S \cap T = \emptyset$, $F \subseteq (S \times T) \cup (T \times S)$ is the flow relation, $I \subseteq S \times T$ is the inhibiting relation, and $m \in \mu S$ is the initial marking.

Given an IPT $N = \langle S, T, F, I, m \rangle$ and $x \in S \cup T$, the pre- and postset of $x$ are respectively the (multi)sets $\bullet x = \{y \mid (y, x) \in F\}$ and $\bullet x = \{y \mid (x, y) \in F\}$. If $x \in S$ then $\bullet x \in \mu T$ and $\bullet x \in \mu T$; analogously, if $x \in T$ then $\bullet x \in \mu S$ and $\bullet x \in \mu S$. The inhibitor set of a transition $t$ is the (multi)set $\circ t = \{s \mid (s, t) \in I\}$. The definition of $\bullet$, $\circ$, $\bullet \circ$, $\circ \circ$ generalise straightforwardly to multisets of transitions.

*Example 4.* The IPT $N_1$ in Fig. 5a has six places (named $s_i$) and three transitions $a, b$, and $c$; the initial marking is $m = \{s_1, s_2, s_3\}$. For instance, the transition $b$ consumes a token from $s_2$ and produces a token in $s_5$ and it is inhibited by $s_1$, i.e., $\bullet b = \{s_2\}$, $b^\bullet = \{s_5\}$ and $\circ b = \{s_1\}$. In $N_2$ $a$ and $b$ are in asymmetric conflict which is a symmetric one in $N_3$.

A (multi)set of transitions $A \in \mu T$ is enabled at a marking $m \in \mu S$, written $m[A]$, if (i) $\bullet A \subseteq m$, (ii) $\circ A \cap [m] = \emptyset$, and (iii) $\forall t \in [A]$. $\circ t \cap (A - \{t\})^\bullet = \emptyset$. Intuitively, $A$ is enabled at $m$ if $m$ contains the tokens to be consumed by $A$ and none of the transitions in $A$ is inhibited in $m$. $\forall t \in [A]$. $\circ t \cap (A - \{t\})^\bullet = \emptyset$ avoids cases in which the firing of $t \in A$ produces tokens in inhibitor places of other transitions in $A$. $\circ$ is enabled at every marking. A set $A$ enabled at $m$ can fire and its firing produces the marking $m' = m - \bullet A + A^\bullet$, written $m[A]m'$. We assume that transitions cannot fire spontaneously, i.e. $\bullet t \neq \emptyset$ for all $t$.

A marking $m$ is reachable if there exists a sequence of firings $m_i[A_i]m_{i+1}$ originated in the initial marking and leading to $m$. We write $M_N$ for the set of reachable markings of $N$. An IPT $N$ is safe if every reachable marking is a set, i.e., $\forall m \in M_N$, $m = [m]$. From now on, we will only consider safe IPTs.

*Example 5.* Consider $N_4$ in Fig. 5d. Both $b$ and $c$ are enabled at $m = \{s_1, s_2, s_3\}$. On the contrary, $a$ is not enabled because it is inhibited by the token in $s_2$. The firing of $b$ on $m$ produces the marking $m' = \{s_1, s_3, s_5\}$, i.e. $m[b]m'$. The transition $a$ is enabled at $m'$ while $c$ is disabled and cannot be fired because of the token in $s_5$. The firing of $a$ on $m'$ produces $m'' = \{s_3, s_4, s_5\}$. The reachable markings of $N_4$ are $\{s_1, s_2, s_3\}$, $\{s_1, s_3, s_5\}$, $\{s_1, s_2, s_6\}$ and $\{s_3, s_4, s_5\}$.
# 4 Reversible Asymmetric Causal Nets

## 4.1 Asymmetric Causal Nets

We now introduce *Asymmetric Causal Nets*, a class of *IPTs* that generalises the *Causal Nets* of [13] to account for asymmetric conflicts. We focus on *IPTs* where all the dependencies between transitions arise because of *inhibitor* arcs. As in causal nets, $t^\bullet \cap \bullet t' = \emptyset$ holds for all $t, t'$: if a place appears in the preset of a transition, it does not appear in the postset of any transition, and vice versa. Hence, the flow relation induces an empty causal relation. However, causality can be recovered from inhibitor arcs. Intuitively, a transition $t$ connected via an inhibitor arc to some place in the preset of another transition $t'$ cannot be fired before $t'$ (if we assume that the preset of $t'$ is marked). This is the case, e.g., of the transitions $a$ and $b$ in Fig. 5d, where $a$ can be fired only after $b$. The induced (immediate) causality relation $\ll$ is defined by $t \ll t'$ iff $\bullet t \cap \circ t' \neq \emptyset$, i.e. the firing of $t$ consumes (at least) one of the tokens that inhibit the firing of $t'$.

Asymmetric causal nets additionally impose places not to be shared between the presets and postsets of transitions, i.e., $t^\bullet \cap t'^\bullet \neq \emptyset \lor t^\bullet \cap \bullet t' \neq \emptyset$ implies $t = t'$ for all $t, t'$. As a consequence, the flow relation does not introduce forward or backward conflicts, which need to be recovered from inhibitor arcs. Note that a transition $t$ inhibited by some place in the postset of another transition $t'$ cannot be fired if $t'$ has been fired, i.e., $t'$ prevents $t$. The induced prevention relation $\prec$ is defined by $t \prec t'$ iff $t^\bullet \cap \circ t' \neq \emptyset$. We write $\prec$ for the inverse of $\succ$. Observe that $\succ$ is analogous to the weak causality of an *AES*: if $t' \succ t$ then $t^\bullet \cap \circ t' \neq \emptyset$; hence $t'$ cannot be fired if $t$ has been fired, however $t$ can be fired after $t'$. As in *AES*, symmetric conflicts are recovered from prevention, i.e., $t$ and $t'$ are in symmetric conflict, written $t \leq t'$, whenever $t \prec t'$ and $t \succ t'$.

**Definition 7.** Let $C = \langle S, T, F, I, m \rangle$ be an *IPT*. $C$ is a pre asymmetric causal net ($pACN$) if the following conditions hold:

1. $\forall t, t' \in T. t^\bullet \cap \bullet t' = \emptyset$;

2. $\forall s \in S. |\bullet s| \le 1 \land |s^\bullet| \le 1 \text{ and } m = \bullet T$;

3. $\forall t \in T. |\bullet t| = |t^\bullet| = 1$;

4. $\ll^+$ is a partial order;

5. $\forall t \in T. [t]_\le = \{t' \in T \mid t' \ll^* t\}$ is finite and $(\succ \cup \ll)$ is acyclic on $[t]_\le$;

6. for all $t, t' \in T. t \ll^+ t'$ implies $t \ll t'$.

Condition 1 states that causal dependencies do not arise because of the flow relation. The second one implies that a place may appear in the preset/postset of at most one transition and that the places in the presets of all transitions are initially marked. Condition 3 forbids that transitions may fire spontaneously or tokens may disappear. Since $\ll$ is meant to model causal dependencies, we require its transitive closure $\ll^+$ to be a partial order (condition 4). Condition 5 requires each transition to have a finite set of causes; hence, $\ll^+$ is a well-founded partial order. By requiring $(\succ \cup \ll)$ to be acyclic on the causes of every transition
$t$ we ensure that the causes can be ordered so as to satisfy causality and prevention. More precisely, we exclude situations in which (i) prevention contradicts causality (e.g., $t \ll t'$ and $t' \rightsquigarrow t$), (ii) there are circular chains of prevention (i.e., $t_0 \rightsquigarrow t_1 \rightsquigarrow \dots \rightsquigarrow t_n \rightsquigarrow t_0$), where symmetric conflicts are a particular case, and (iii) self-blocked transitions (i.e., $\ll$ needs to be irreflexive and hence $\bullet t \cap \circ t = \emptyset$ for all $t$). Condition 6 imposes that all dependencies among transitions have to be explicitly represented in the structure of the net, namely causality is saturated.

**Definition 8.** Let $C = \langle S, T, F, I, \mathfrak{m} \rangle$ be a pACN. Then $C$ is an asymmetric causal net (ACN) whenever for all $t, t', t'' \in T$. $t \nvdash t' \land t' \ll t''$ imply $t \nvdash t''$.

The added condition implies that there are inhibitor arcs for all inherited symmetric conflicts.

**Example 6.** The IPTs in Fig. 5 are ACNs. The first two conditions of Definition 7 hold for the four nets since transitions do not share places in their pre and postsets. Moreover, the places in the presets of all transitions are the only ones that are initially marked. For $N_1$ (Fig. 5a), we have that $a \ll b$ and $b \ll c$; consequently, $\ll^+$ is a total order, and causality is saturated as we also have $a \ll c$. Moreover, $\ll$ is empty (because none of the transitions has an inhibitor arc connected to the postset of another transition). For $N_2$ in Fig. 5b, causality is empty while prevention contains the unique pair $a \ll b$. For $N_3$ in Fig. 5c, $a$ and $b$ are in symmetric conflict ($a \nvdash b$): their executions prevent each other. Figure 5d shows a net where $b \ll a$, $b \nvdash c$ and $a \nvdash c$, and conflicts are inherited along causality $\ll$.

For the definition of (p)ACNs morphisms we take into account that inhibitor arcs correspond to two different dependencies: causality and prevention. In particular, the inhibitor arcs representing prevention demand a peculiar treatment of markings if compared against the classical notions of morphisms for nets [24,25].

We introduce some technical machinery. A partial mapping $f : A \to B$ extends to a mapping $f : \mu A \to \mu B$ by stipulating that $f(\sum_{a \in A} n_a \cdot a) = \sum_{b \in B}(\sum_{a \in f^{-1}(b)} n_a) \cdot b$. A multirelation $f$ is a multiset on $A \times B$; it is finitary if $\{b \in B \mid f(a, b) > 0\}$ is finite for all $a$. A multirelation $f$ is a relation if $f = [[f]]$, i.e., if it is a set. The composition of two multirelations $f$ on $A \times B$ and $g$ on $B \times C$, written $f; g$, is the multirelation on $A \times C$ defined such that $[f; g](a, c) = \sum_{b \in B} f(a, b) \cdot g(b, c)$ for all $a \in A, c \in C$. A finitary multirelation $f$ on $A \times B$ induces a partial mapping from $\mu f : \mu A \to \mu B$ defined such that $\mu f(\sum_{a \in A} n_a \cdot a) = \sum_{b \in B} \sum_{a \in A}(n_a \cdot f(a, b)) \cdot b$. Conversely, a partial mapping $\mu f : \mu A \to \mu B$ induces a mapping $[[f]] : \mu A \to B$ defined such as $[[f]](m) = [[\mu f(m)]]$.

**Definition 9.** An ACN-morphism from $C_0$ to $C_1$ is a pair $(f_S, f_T)$ consisting of a relation $f_S \subseteq S_0 \times S_1$ and a partial function $f_T : T_0 \to T_1$ defined such that

1. for all $t \in T_0$ if $f_T(t) \neq \perp$ then
   (a) $\bullet f_T(t) = \mu f_S(\bullet t)$ and $f_T(t) \bullet = \mu f_S(t \bullet)$;
   (b) $\forall (s, f_T(t)) \in I_1$. $\forall s' \in f_S^{-1}(s)$. $(s', t) \in I_0$; and
2. $\forall t, t' \in T_0$ if $f_T(t) \neq \perp \neq f_T(t')$ then $f_T(t) = f_T(t') \Rightarrow t \nvdash_0 t'$;
<figure><img src="image_8.png" /><figcaption>Fig. 6. Two simple ACNs and a rACN</figcaption></figure>

3. $\forall s_1 \in S_1. \forall s_0, s'_0 \in f_S^{-1}(s_1). s_0 \neq s'_0$ implies $s_0 \vdash_0 s'_0$ or $\cdot s_0 \vdash_0 \cdot s'_0$;

4. $[[f_S]](m_0) = m_1$.

Conditions 1 and 2 are standard: presets and postsets are preserved and inhibitor arcs are reflected; only conflicting transitions can be identified. Differently from usual requirements, Condition 3 allows $f_S$ to *identify* different places in the preset of different transitions. This may be seen as problematic because a place in the target of the morphism may represent different tokens in the source, which in principle may evolve independently. However, according to Condition 3, $f_S$ may only identify places connected to transitions that are in (symmetric) conflict.

**Example 7.** Consider the ACNs $C_0$ and $C_1$ in Fig. 6. A morphism $(f_S, f_T) : C_0 \to C_1$ can be defined as follows. The mapping for transitions is $f_T(a) = a', f_T(b) = b'$ and $f_T(c) = c' = f_T(d)$. Note that the conflicting transitions $c$ and $d$ are identified. The relation on places is as expected, i.e., $f_S(s_i^0, s_i^1)$ for $1 \le i \le 6$, $f_S(s_7^0, s_3^1)$, and $f_S(s_8^0, s_6^1)$. The inhibitor arc $(s_3^1, b')$ of $C_1$ is reflected in the one $(s_3^0, b)$ of $C_0$. The remaining arcs of $C_0$ are not preserved by the mapping.

As expected, it can be shown that ACN-morphisms preserve the tokens game, i.e., if $m[A]m'$ then $[[f_S]](m)[\mu f_T(A)][[f_S]](m')$. Also, ACN-morphisms preserve behaviours and are closed under composition, as stated below.

**Lemma 1.** Let $(f_S, f_T) : C_0 \to C_1$ and $(g_S, g_T) : C_1 \to C_2$ be two ACN-morphisms. Then $(f_S; g_S, f_T; g_T) : C_0 \to C_2$ is an ACN-morphism as well.

pACNs and ACN-morphisms form a category, denoted by **pACN**. We write **ACN**, for the full and faithful subcategory that has ACNs as objects.

## 4.2 Reversible Asymmetric Causal Nets

Reversible Asymmetric Causal Nets are defined by following the approach in [13]: pACNs are enriched with *backward* transitions that undo the effects of previously executed *forward* transitions (i.e., the ordinary ones). We assume that the set $T$ of transitions is partitioned into a set $\bar{T}$ of forward transition and $\bar{T}$ of backward transition. Every backward transition $\underline{t} \in \bar{T}$ undoes the effect of one and only one forward transition $t \in \bar{T}$. However, there could be forward transitions that are irreversible. With slightly abuse of notation, we write $\underline{t}$ for the forward transition and $t$ for the associated reversing transition (when it exists).
<figure><img src="image_9.png" /><figcaption>Fig. 7. Simple rACNes</figcaption></figure>

**Definition 10.** An IPT $V = \langle S, T, F, I, m \rangle$ is a reversible Asymmetric Causal Net (rACN) if there exists a partition $\{\bar{T}, \bar{T}\}$ of $T$, with $\bar{T}$ the forward transitions and $\bar{T}$ the backward ones, such that:

1. $V_{\bar{T}} = \langle S, \bar{T}, F|_{\bar{T} \times \bar{T}}, I|_{\bar{T} \times \bar{T}}, m \rangle$ is a pACN net;

2. $\forall t \in \bar{T}. \exists! t \in \bar{T}$ such that $t^{\bullet} = \bullet t, \bullet t = \underline{t}^{\bullet}$, and $\bullet t \subseteq \circled{t}$;

3. $\forall t \in \bar{T}. K_{\underline{t}} = \{t' \in \bar{T} | \circled{t} \cap \bullet t' \neq \emptyset\}$ is finite and $\rightsquigarrow$ acyclic on $K_{\underline{t}}$;

4. $\forall t \in \bar{T}. \forall t \in \bar{T}$ if $\bullet t \cap \circled{t} \neq \emptyset$ then $t^{\bullet} \cap \circled{t} = \emptyset$;

5. $\forall t, t', t'' \in \bar{T}. t \nparallel t' \land t' \lll t'' \Rightarrow t \nparallel t''$ with $\lll$ being the transitive closure of $\ll \cap \{(t, t') | \underline{t} \notin \bar{T} \text{ or } \circled{t} \cap t'^{\bullet} \neq \emptyset\}$.

The underlying net $V_{\bar{T}}$ containing just the forward transitions of $V$ must be a pACN. Condition 2 establishes that each backward transition $\underline{t}$ reverses exactly one forward transition $t$. Note that $\underline{t}$ consumes the tokens produced by $t$ (i.e., $t^{\bullet} = \bullet \underline{t}$) and produces the tokens consumed by $t$ (i.e., $\underline{t}^{\bullet} = \bullet t$). The condition $\bullet t \subseteq \circled{t}$ amounts to saying that $\underline{t}$ (i.e., the reverse of $t$) cannot be fired if $t$ has not been executed: a transition can be reversed only if it has been fired. Condition 3 can be read as requiring a finite set of causes for the undoing of each transition; in fact, $\bullet K_{\underline{t}}$ contains all the forward transitions $t'$ that enable the execution of $\underline{t}$. By Condition 4, if a backward transition $\underline{t}'$ causally depends on the forward transition $t$ (i.e., $\bullet t \cap \circled{t}' \neq \emptyset$) then $\underline{t}'$ cannot be prevented by the same transition $t$, i.e. $t^{\bullet} \cap \circled{t}' = \emptyset$ since otherwise will be blocked. The relation $\lll$ in the last condition, which is analogous to the *sustained causation* of rAES, coincides with causality except for the cases in which a cause can be reversed even when a causally-dependent transition has been fired. The conflicts should be inherited along $\lll$, not along the $\ll$. We shall write $V^{\bar{T}}$ for a rACN $V$ whose set of backward transitions is $\bar{T}$.

Inhibitor arcs induce the previously discussed relations $\ll$ and $\rightsquigarrow$ over the forward flow (i.e. on $\bar{T} \times \bar{T}$). They also induce two relations regulating the backward flow (i.e. on $\bar{T} \times \bar{T}$): (i) the *reverse causation* $\ll$ defined by $t \ll \underline{t}'$ iff $\bullet t \cap \circled{t}' \neq \emptyset$; and (ii) the *prevention* $\triangleleft$ defined by $\underline{t}' \triangleleft t$ iff $t^{\bullet} \cap \circled{t}' \neq \emptyset$.

**Example 8.** Figure 7a shows the rACN $V_1$, exhibiting an asymmetric conflict between a and b, and b can be reversed (i.e., *b* can happen) only if a and b have been fired and c has not. Removing *b* we get the pACN $V_{1\{a,b,c\}}$ in Fig. 7b.
<figure><img src="image_10.png" /><figcaption>**Fig. 8.** Two rACNes related by a rACN-morphism</figcaption></figure>

*Example 9.* In the rACN $V_2$ in Fig. 7c both *b* and *c* are reversible and $V_{2\{a,b,c\}} = V_{1\{a,b,c\}}$. In this rACN the transition *c* depends on *b*, however *b* can be executed (*b* can be reversed) even if the transitions depending on *b* have not been reversed. In this way the configuration $\{a, c\}$ can be reached by mixing forward and backward computations, but not by only forward computations. This is an example of out-of-causal order reversibility in rACN.

Morphisms for rACNs are defined below.

**Definition 11.** Let $V^{T_0}$ and $V^{T_1}$ be two rACNs. An rACN-morphism is a pair $(f_S, f_T)$ consisting of a relation $f_S \subseteq S_0 \times S_1$ and a partial function $f_T : T_0 \to T_1$ satisfying the following conditions

1. $f_T(\bar{T}_0) \subseteq \bar{T}_1$ and $f_T(T_0) \subseteq T_1$;

2. $(f_S, f_T|_{\bar{T}_0}) : V_{\bar{T}_0} \to V_{\bar{T}_1}$ is a ACN-morphism,

3. $\forall \underline{t} \in T_0$. if $f_T(t) \neq \perp$ then

(a) $\tilde{f}_T(t) \neq \perp$ and $f_T(t) = f_T(t)$; and

(b) $\forall (s, f_T(t)) \in I_1$. $\forall s' \in \tilde{f}_S^{-1}(s)$. $(s', t) \in I_0$.

By Condition 1, forward (resp. backward) transitions are mapped to forward (resp. backward) transitions. Condition 2 implies that when we restrict $f_T$ to $\bar{T}_0$, i.e., only consider forward transitions, we obtain an ACN-morphism on the underlying nets consisting of forward transitions, i.e., $V_{\bar{T}_0}$ and $V_{\bar{T}_1}$. Condition 3a ensures that the transition $\underline{t}$ that reverses $t$ is mapped to the transition $f_T(t)$ that reverses $f_T(t)$. Condition 3b prevents the collapse of inhibitor arcs, i.e., it avoids the identification of different causes that may prevent the reversing of a transition.

*Example 10.* An rACN-morphism $(f_S, f_T) : V_0 \to V_1$ for the rACNs $V_0$ and $V_1$ in Fig. 8 is as follows: $f_S$ is as in Example 7 and $f_T$ is the mapping in Example 7 extended for the reversing transition $\underline{a}$ as $f_T(\underline{a}) = \underline{a}'$. Clearly $\underline{f}_T(\underline{a}) = f_T(\underline{a})$.

It can be shown that rACN-morphisms preserve behaviours [14], i.e. if $m[A]m'$ in $V^{T_0}$, then $[[f_S]](m) [\mu f_T(A)] [[f_S]](m')$ in $V^{T_1}$. Moreover, they are closed under composition as stated below.

**Lemma 2.** Let $(f_S, f_T) : V_0 \to V_1$ and $(g_S, g_T) : V_1 \to V_2$ be two rACN-morphisms. Then $(f_S; g_S, f_T; g_T) : V_0 \to V_2$ is a rACN-morphism as well.

rACNs and rACN-morphisms form a category, which is denoted by **RACN**.
# 5 Relating Models

We now study the relationship between the categories of (reversible) asymmetric causal nets and (reversible) asymmetric event structures. We start by showing how to recover an rAES out of the flow and inhibitor arcs of an rACN. The relations induced by the inhibitor arcs of a rACN, namely $\ll$ (causality), $\rightsquigarrow$ (weak causality), $<$ (reverse causality), $\lhd$ (prevention), and $\lll$ (sustained causation) contribute to the definition of the relations of the associated rAES.

**Definition 12.** Let $V^T = \langle S, T, F, I, \mathfrak{m} \rangle$ be an rACN. Then, $\mathcal{E}_r(V^T)$ is the tuple $(\bar{T}, U, \ll, \lll \cup \sim, \prec, \lhd)$ where $U = \{t \in \bar{T} \mid t \in T\}$ are the reversible events and $\ll, \sim, \prec, \lhd$ and $\lll$ are the causation, weak causality, reverse causality, prevention and sustained causation induced by F and I.

**Theorem 1.** $V^T$ be an rACN. Then $\mathcal{E}_r(V)$ is an rAES.

*Example 11.* Consider the rACN $V_1$ in Fig. 7, the corresponding rAES $\mathcal{E}_r(V_1)$ is $H_1$ in Example 2.

An rACN without reversing transitions (i.e., $V^\emptyset$) is an ACN, hence the construction in Definition 12 works also for ACNe: if C is an ACN then $\mathcal{E}_r(C)$ is an AES.

$\mathcal{E}_r$ extends to a functor by observing that an rACN-morphism $(f_S, f_T) : V_0 \to V_1$ induces an rAES-morphism $\mathcal{E}_r(f_S, f_T) = f_T$.

**Proposition 1.** $\mathcal{E}_r$: RACN $\to$ AES is a well-defined functor.

The construction that associates a net to an event structure follows the usual intuition: places are suitable subsets of events, and transitions are connected to places according to the relations in the event structure.

**Definition 13.** Let $\mathcal{H} = (E, U, <, \lceil, \prec, \lhd)$ be a rAES. Then, $N_r(\mathcal{H})$ is the net $\langle S, E \cup \{(u, \mathbf{r}) \mid u \in U\}, F, I, \mathfrak{m} \rangle$ where

$$S = \{(A, B) \mid A, B \subseteq E \wedge |A| \le |B| \le 1 \wedge A \subseteq B\}$$

$$F = \{((\emptyset, \{e\}), e) \mid e \in E\} \cup \{(e, \{e\}, \{e\}) \mid e \in E\} \cup \{((\{u\}, \{u\}), (\underline{u}, \mathbf{r})) \mid u \in U\} \cup \{(\underline{u}, \mathbf{r}), (\emptyset, \{u\}) \mid u \in U\}$$

$$I = \{((\emptyset, \{e'\}), e) \mid e' < e\} \cup \{((\{e'\}, \{e'\}), e) \mid e \lceil e' \wedge \neg(e' < e)\} \cup \{((\emptyset, \{e\}), (u, \mathbf{r})) \mid e < \underline{u}\} \cup \{((\{e\}, \{e\}), (u, \mathbf{r})) \mid \underline{u} \lhd e\}$$

$$\mathfrak{m} = \{(\emptyset, A) \mid (\emptyset, A) \in S\}$$

Events $E$ are the forward transitions, and each event $e$ has two associated places: $(\emptyset, \{e\})$ indicates that $e$ has not occurred whereas $(\{e\}, \{e\})$ indicates that it has occurred. A transition $(\underline{u}, \mathbf{r})$ reverses the forward transition $u$, i.e. it consumes from $(\{u\}, \{u\})$ and produces in $(\emptyset, \{u\})$. The inhibitor arcs in $I$ model causality (forward or backward) and precedence (forward or backward). the initially marked are those appearing in the preset of some forward transition.

**Theorem 2.** Let $\mathcal{H} = (E, U, <, \lceil, \prec, \lhd)$ be an rAES. Then $N_r(\mathcal{H})$ is an rACN.

Again, if $G = (E, <, \lceil)$ is an AES then $N_r((E, \emptyset, <, \lceil, \prec, \lhd, \emptyset))$ is an ACN.
**Example 12.** Consider the rAES $H'$ in Example 2. The associated net $N_r(H')$ has $(\emptyset, \emptyset)$, $(\emptyset, \{a\})$, $(\emptyset, \{b\})$, $(\emptyset, \{c\})$, $(\{a\}, \{a\})$, $(\{b\}, \{b\})$ and $(\{c\}, \{c\})$ as places, $a, b, c$ as forward transitions, and $(b, \mathbf{r})$, $(c, \mathbf{r})$ as reversing transitions. The flow arcs are as in Definition 13, while inhibitor arcs are those induced by the different relations in $H'$. The resulting net is analogous to the one in Fig. 7c, where places bear different names and the isolated place $(\emptyset, \emptyset)$ has been omitted.

$N_r$ extends to a functor. For an rAES-morphism $f: H_0 \to H_1$ and $N_r(H_i) = \langle S_i, E_i, F_i, I_i, m_i \rangle$ for $i=0,1$, we take $N_r(f) = (f_S, f_T)$ where $f_S \subseteq S_0 \times S_1$ is defined such that $(s_0, s_1) \in f_S$ iff one of the following holds:

$$ - s_0 = (\emptyset, A); s_1 = (\emptyset, B); A \subseteq f^{-1}(B); \text{ and } A = \emptyset \Rightarrow f^{-1}(B) = \emptyset; \text{ or} $$

$$ - s_0 = (A, A); \text{ and } s_1 = (f(A), f(A)); $$

and $f_T: E_0 \cup \{(\underline{u}, \mathbf{r}) \mid u \in U_0\} \to E_1 \cup \{(\underline{u}, \mathbf{r}) \mid u \in U_1\}$ defined such that

$$ - f_T(t) = f(e) \text{ if } e \in E_0; $$

$$ - f_T(\underline{u}, \mathbf{r}) = (f(u), \mathbf{r}) \text{ if } f(u) \neq \perp. $$

**Proposition 2.** Let $f: H_0 \to H_1$ be an rAES-morphism. Then $N_r(f): N_r(H_0) \to N_r(H_1)$ is a well defined rACN-morphism.

**Proposition 3.** $N_r$ : **RAES** → **RACN** is a well-defined functor.

Our main result below states the precise relation between **RACN** and **RAES**, namely, the functor $N_r$ is the left adjoint of $\mathcal{E}_r$.

**Theorem 3.** The functor $N_r$ : **RAES** → **RACN** is the left adjoint of the functor $\mathcal{E}_r$ : **RACN** → **RAES**.

Let $\mathcal{E}$ and $\mathcal{N}$ be the respective restrictions of the functors $\mathcal{E}_r$ and $N_r$ respectively on ACNs or AESes, i.e. we restrict our attention to the full and faithful subcategories of **ACN** and **AES**. Then, we have the following connection.

**Theorem 4.** The functor $\mathcal{N}$ : **AES** → **ACN** is the left adjoint of the functor $\mathcal{E}$ : **ACN** → **AES**.

# 6 Discussion

In this paper we complete previous efforts [13, 18, 19] aimed at relating classes of reversible event structures with classes of Petri nets. To the best of our knowledge, the only previous attempt to relate reversible event structures and nets is in [13]. In contrast to the (pre) causal nets proposed in [13], the notion of (pre) asymmetric causal net considers forward symmetric conflicts represented by asymmetric ones, rather than via shared places. As a result, racNs are obtained from pre acNs by incorporating reversibility. Regarding the philosophy behind our nets, it may be asked whether we adhere to the *individual token philosophy* or the *collective token philosophy*, as defined in [23]. In the individual token philosophy, each place can be uniquely marked, whereas in the collective token
philosophy, there can be multiple ways to place a token in a given place. If we only consider the forward flow of our nets, they adhere to the individual token philosophy. However, asymmetric conflicts suggest that the *past* of the transition putting a token in a given place may not be unique. Moreover, when considering the reversing flow, things become more complex, particularly with out-of-causal order reversibility, as a forward transition may only be executed because some reversing transition has been executed. To settle this question, it may be necessary to seek a different definition for the individual token philosophy, perhaps by focusing on the forward dependencies of the pre-asymmetric causal net in the rACN, rather than considering the entire rACN.

Establishing a correspondence between these two different models has not only theoretical relevance, but it can also be exploited in concrete scenarios. For instance, one successful application of reversibility is causal-consistent *reversible debugging* [7, 11]. Reversible debuggers extend classical ones by allowing the user to go back in the execution, thereby making it easier to find the source of a bug. Causal-consistent reversible debuggers further improve on reversible ones by leveraging causal information while undoing computations. While this technique has been applied to message-passing concurrent systems (e.g., actor-like languages), it has not been applied to shared-memory-based concurrency so far.

Consider the next snippet of code

```c
1 pthread_mutex_t m = //initialization
2 int *x=malloc(sizeof(int));
3 void thread(void *arg)
4 {
5     pthread_mutex_lock(&m);
6     if (x != NULL)
7     {
8         doSomething(x);
9     }
9 } int main()
10 {
11     pthread_t t;
12     pthread_create(&t, NULL, thread,
13                     NULL);
14     pthread_mutex_lock(&m);
15     free(x);
16     pthread_mutex_unlock(&m);
17     return 0;
}
```

The behaviour of the program can be thought in terms of events. Be *a* the event corresponding to the initialisation of *x* at line 2, *b* for the instruction at line 6 and *c* for the one at line 13. Both *b* and *c* causally depend on *a* (*a* < *b* and *a* < *c*); while *c* can happen after *b*, *b* cannot happen after *c*, that is *b* ∨ *c*. Moreover, the reversal of a complete execution of the program should ensure that *c* is reversed (i.e., the memory is allocated) before *b* is reversed, hence *b* < ∗c*. Consider instead a version of the program in which *c* is executed outside a critical section. In this case, the execution may raise a *segmentation fault*. When debugging such a faulty execution, the programmer would observe that the execution violates *b* ∨ *c* because *b* happened after *c*. On the one hand, an execution can be visualised in terms of events, i.e., the programmer can be provided with a high-level description of the current state of the system (a configuration of the event structure) along with the relevant dependencies. On the other hand, the instrumented execution of the program and of its reversal can be handled by the underlying operational model (i.e., a reversible causal net). Also, one could think of the undoing of an event as a backward breakpoint. That is, one could trigger the undoing of an event from the net and then the debugger will execute all the necessary backward steps in the code, to undo such event. The seamless integration of rAES and rACN with causal-consistent reversible debuggers can be a nice exploitation of our results, which we will consider in future work.
References

1. Aman, B., et al.: Foundations of reversible computation. In: Ulidowski, I., Lanese, I., Schultz, U.P., Ferreira, C. (eds.) RC 2020. LNCS, vol. 12070, pp. 1–40. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-47361-7_1

2. Baldan, P., Busi, N., Corradini, A., Pinna, G.M.: Domain and event structure semantics for petri nets with read and inhibitor arcs. Theor. Comput. Sci. 323(1–3), 129–189 (2004)

3. Baldan, P., Corradini, A., Montanari, U.: Contextual Petri nets, asymmetric event structures, and processes. Inf. Comput. 171(1), 1–49 (2001)

4. Boudol, G.: Flow event structures and flow nets. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 62–95. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-53479-2_4

5. Cristescu, I., Krivine, J., Varacca, D.: A compositional semantics for the reversible π-calculus. In: 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS, pp. 388–397 (2013)

6. Danos, V., Krivine, J.: Reversible communicating systems. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 292–307. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-28644-8_19

7. Giachino, E., Lanese, I., Mezzina, C.A.: Causal-consistent reversible debugging. In: Gnesi, S., Rensink, A. (eds.) FASE 2014. LNCS, vol. 8411, pp. 370–384. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54804-8_26

8. Graversen, E., Phillips, I., Yoshida, N.: Towards a categorical representation of reversible event structures. J. Log. Algebraic Methods Program. 104, 16–59 (2019)

9. Lanese, I., Medic, D., Mezzina, C.A.: Static versus dynamic reversibility in CCS. Acta Informatica 58(1–2), 1–34 (2021)

10. Lanese, I., Mezzina, C.A., Stefani, J.: Reversibility in the higher-order π-calculus. Theor. Comput. Sci. 625, 25–84 (2016)

11. Lanese, I., Nishida, N., Palacios, A., Vidal, G.: CauDEr: a causal-consistent reversible debugger for erlang. In: Gallagher, J.P., Sulzmann, M. (eds.) FLOPS 2018. LNCS, vol. 10818, pp. 247–263. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-90686-7_16

12. Medic, D., Mezzina, C.A., Phillips, I., Yoshida, N.: A parametric framework for reversible π-calculi. Inf. Comput. 275, 104644 (2020)

13. Melgratti, H.C., Mezzina, C.A., Pinna, G.M.: A distributed operational view of reversible prime event structures. In: 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS, pp. 1–13. IEEE (2021)

14. Melgratti, H.C., Mezzina, C.A., Pinna, G.M.: Relating reversible Petri nets and reversible event structures, categorically. Technical report (2023). https://arxiv.org/pdf/2302.14195.pdf

15. Melgratti, H.C., Mezzina, C.A., Ulidowski, I.: Reversing place transition nets. Log. Methods Comput. Sci. 16(4) (2020)

16. Montanari, U., Rossi, F.: Contextual nets. Acta Informatica 32(6), 545–596 (1995)

17. Nielsen, M., Plotkin, G., Winskel, G.: Petri nets, event structures and domains. In: Kahn, G. (ed.) Semantics of Concurrent Computation. LNCS, vol. 70, pp. 266–284. Springer, Heidelberg (1979). https://doi.org/10.1007/BFb0022474

18. Philippou, A., Psara, K.: A collective interpretation semantics for reversing Petri nets. Theor. Comput. Sci. 924, 148–170 (2022)

19. Philippou, A., Psara, K.: Reversible computation in nets with bonds. J. Log. Algebraic Methods Program. 124, 100718 (2022)
20. Phillips, I., Ulidowski, I.: Reversibility and asymmetric conflict in event structures. J. Log. Algebraic Methods Program. **84**(6), 781–805 (2015)

21. Phillips, I., Ulidowski, I., Yuen, S.: Modelling of bonding with processes and events. In: Dueck, G.W., Miller, D.M. (eds.) RC 2013. LNCS, vol. 7948, pp. 141–154. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38986-3_12

22. Phillips, I.C.C., Ulidowski, I.: Reversing algebraic process calculi. J. Log. Algebraic Methods Program. **73**(1–2), 70–96 (2007)

23. Glabbeek, R.J.: The individual and collective token interpretations of petri nets. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 323–337. Springer, Heidelberg (2005). https://doi.org/10.1007/11539452_26

24. Winskel, G.: Event structures. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) ACPN 1986. LNCS, vol. 255, pp. 325–392. Springer, Heidelberg (1987). https://doi.org/10.1007/3-540-17906-2_31

25. Winskel, G.: Petri nets, algebras, morphisms, and compositionality. Inf. Comput. **72**(3), 197–238 (1987)