stix@largesymbols”0E stix@largesymbols”0F

[a]

[b]

[c]

# Relating Reversible Petri Nets and Reversible Event Structures,
categorically

Hernán Melgratti0000-0003-0760-0618  ,  Claudio Antares
Mezzina0000-0003-1556-2623  and  G. Michele Pinna0000-0001-8911-1580  ICC -
Universidad de Buenos Aires - Conicet, Argentina  Dipartimento di Scienze Pure
e Applicate, Università di Urbino, Italy  Università di Cagliari, Italy

###### 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.

###### Key words and phrases:

Petri Nets and Event Structures and Concurrency and Categories.

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 Marie Skłodowska-Curie grant
agreement 778233, UBACyT projects 20020170100544BA and 20020170100086BA

##  1\. Introduction

_Event structures_ (eses) [38] are a denotational formalism to describe the
behaviour of concurrent systems as a set of event occurences and constraints
on such events, regulating how such events can happen. _Prime event
structures_ (${{\textsc{pes}}{}es}$) are the simplest form of event
structures. A Prime event structure describes a computational process as a set
of events whose occurrence is constrained by two relations: _causality_ and
(symmetric) _conflicts_. A simple pes is depicted in Fig. 1(a), where
causality ($<$) is drawn with straight lines (to be read from bottom to top)
and conflicts ($\\#$) with curly lines. In this case, $b$ causally depends on
$a$ (i.e., $a<b$) meaning that $b$ cannot occur if $a$ does not occur first;
additionally, $b$ and $c$ are in conflict (i.e., $b\\#c$) meaning that $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. 1(b). For instance, the transition $\emptyset\rightarrow\\{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, _Asymmetric Event Structures_ (aeses) relax the notion of
conflicts by considering instead _weak causality_. Intuitively, an event $e$
weakly causes the event $e^{\prime}$ (written $e\nearrow e^{\prime}$) if
$e^{\prime}$ can happen after $e$ but $e$ cannot happen after $e^{\prime}$.
This can be considered as an asymmetric conflict because $e^{\prime}$ forbids
$e$ to take place, but not the other way round. Let us consider the following
shared memory scenario:

$\begin{array}[]{l||lr}\textbf{Thread 1}&\textbf{Thread 2}&\textbf{Possible
Values}\\\ 1:\mathtt{lock(m);}&1:\mathtt{lock(m);}&\mathtt{x=0;\,y=1}\\\
2:\mathtt{if(y==0)}&2:\mathtt{y++;}&\mathtt{x=1;\,y=1}\\\
3:\;\;\mathtt{then\;x=1;}&1:\mathtt{unlock(m);}\\\
4:\mathtt{unlock(m);}\end{array}$

in which two variables $x$ and $y$ are shared among two threads. Let us
suppose, for simplicity, that the two variables are initialised to $0$.
Assuming strong consistency, the actions of the two threads can be scheduled
into two different ways leading to two different final configurations: either
$x=0$ and $y=1$ or both variables are equal to $1$. If we represent the
behaviour of the above snippet as an event structure, we can identify two
relevant events: the assignment of $1$ to $x$ and the increment of $y$. Let us
call such events $x_{1}$ and $y_{1}$. We can observe that if $x_{1}$ happens
then $y_{1}$ can happen, while if $y_{1}$ happens, then $x_{1}$ cannot. And
this means that the $x_{1}$ weakly causes $y_{1}$, that is $x_{1}\nearrow
y_{1}$.

However, symmetric conflicts can be recovered by making a pair of conflicting
events to weakly cause each other. For instance, the pes $\mathsf{P}$ in Fig.
1(a) can be rendered as the aes $\mathsf{G}$ in Fig. 1(c), 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$ (the additional weak
causal dependency $a\nearrow b$ is required by consistency with the causality
relation). Unsurprisingly, the transition system associated with $\mathsf{G}$
coincides with that of $\mathsf{P}$ in Fig. 1(b). Differently, the aes
$\mathsf{G}^{\prime}$ relaxes the conflict between $b$ and $c$ by making it
asymmetric: we keep $b\nearrow c$ but drop $c\nearrow b$. Hence, $c$ can be
added to the configuration $\\{a,b\\}$ but $b$ cannot be added to $\\{a,c\\}$,
as rendered in the transition system in Fig. 1(e).

Since their introduction [38], eses have played a central role in the
development of denotational semantics for concurrency models; in particular,
for Petri nets (pns). It is well-known that different classes of eses
correspond to different classes of pns [38, 3, 4]. Moreover, 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 requires contextual arcs
[3].

Reversible computing has been studied in the 70’s for its promise of achieving
low-energy computation [15]. Lately [1, 25] is gaining interests for its
application in different fields: from modelling bio-chemical reactions, to
improve parallel discrete events simulation, to model fault tollerant
primitives and finally to debugging. In a model of reversible computation we
can distinguish two different flows of computation, i.e., in addition to the
description of the standard forward execution, there is a backward flow that
expresses the way in which the effects of the forward computation can be
undone. If in a sequential setting it is pretty clear what is the backward
flow of a computation (i.e. it is the exact inverse of the forward one), and
the only challenge is on how to record computational history [14, 40]. In a
concurrent setting it is more complicated. Different proposal have arisen in
the last years trying to cope with different models: _causal-consistent
reversibility_ [7] has been shown to be the right notion to model primitives
for fault-handling systems such as transactions [8, 16] or roll-back recovery
schemas [36, 26, 37], or to reverse-debug concurrent systems; while _out-of-
causal_ order reversibility [32] has been shown as being able to model bio-
chemical reactions and compensations. Different models of concurrent
computation [1] are available today: RCCS [7], CCSK [33], rho$\pi$ [18],
R$\pi$ [6], reversible Petri nets [24], reversible event structures [31], to
name a few. As expected, the attention has turned to the question of how these
models relate to each other (see e.g. [17, 20, 21, 22, 12]). This work
addresses such goal by revisiting, in the context of reversibility, the
connection between Event Structures (eses) [38] and Petri Nets (pns)
established by Winskel [28].

On the event structure side, we focus on the _reversible Asymmetric Event
Structures_ (raeses) introduced in [31], which are a reversible counterpart of
_Asymmetric Event Structures_ (aeses) [3], which in turn are a generalisation
of Prime Event Structures (peses) [28].

$b$$a$$c$

(a) pes $\mathsf{P}$

$\\{a,b\\}$$\\{a,c\\}$$\\{a\\}$$\\{c\\}$$\emptyset$$\\{c\\}$

(b) Transition system of $P$

$b$$a$$c$

(c) aes $\mathsf{G}$

$b$$a$$c$

(d) aes $\mathsf{G}^{\prime}$

$\\{a,b\\}$$\\{a,c\\}$$\\{a\\}$$\\{c\\}$$\emptyset$$\\{c\\}$$\\{a,b,c\\}$

(e) Transition system of $\mathsf{G}^{\prime}$

$b$$a$$\underline{b}$$\underline{a}$$c$

(f) raes $\mathsf{H}$

$\\{a,b\\}$$\\{a,c\\}$$\\{b,c\\}$$\\{a\\}$$\\{c\\}$$\emptyset$$\\{b\\}$$\\{a,b,c\\}$

(g) Transition system of ${\mathsf{H}}$

Figure 1. A simple pes, aes, and raes along with their associated transition
systems.

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. For the aes $\mathsf{G^{\prime}}$ in Fig. 1(d), with
$\\{\underline{a},\underline{b}\\}$ we indicate that $a$ and $b$ are
reversible, while $c$ is not. Two relations, dubbed _reverse causation_
($\prec$) and _prevention_ ($\triangleleft$), describe the backward flow and
regulate the way in which reversing events occur: $\prec$ prescribes the
events required for the undoing while $\triangleleft$ stipulates those that
preclude it. The raes $\mathsf{H}$ in Fig. 1(f) consists of the forward flow
defined by $\mathsf{G^{\prime}}$ extended 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 (the pair
$b\prec\underline{b}$ is analogous). The prevention arc
$\underline{a}\triangleleft c$ states that $a$ can be reversed only if $c$ has
not occurred. The transition system associated with $\mathsf{H}$ is in Fig.
1(g): transitions corresponding to the forward flow (i.e., the ones in black
mimicking those in Fig. 1(e)) add events to configurations; on the contrary,
reversing transitions (in blue) remove events from configurations. For
instance, the transition $\\{a,b\\}\rightarrow\\{a\\}$ accounts for the fact
that $b$ is reversible and can always be undone. Note that $a$ can be reversed
both in $\\{a\\}$ and $\\{a,b\\}$ but not in $\\{a,c\\}$ since the prevention
relation (i.e., $\underline{a}\triangleleft c$) forbids $a$ to be reversed if
$c$ has already occurred. Interestingly, $a$ can be reversed in $\\{a,b\\}$
leading to the configuration $\\{b\\}$, which is not reachable by the forward
flow (black arrows). This is known as out-of-causal order reversibility [32].

$s_{1}$$s_{2}$$s_{3}$$s_{4}$$s_{5}$$s_{6}$$a$$b$$c$

$a<b$ and $b\\#c$

(a) $N_{P}$

$s_{1}$$s_{2}$$s_{3}$$s_{4}$$s_{5}$$s_{6}$$a$$b$$c$

$a<b$, $b\nearrow c$ and $c\nearrow b$

(b) $N_{R}$

$s_{1}$$s_{2}$$s_{3}$$s_{4}$$s_{5}$$s_{6}$$a$$\underline{a}$$b$$\underline{b}$$c$

$\underline{a}\triangleleft c$, $\underline{a}\prec a$ and $\underline{b}\prec
b$

(c) $N^{\prime}_{R}$

Figure 2. An occurrence net $N_{P}$, its associated causal net $N_{R}$, and
its reversible causal net $N^{\prime}_{R}$.

Reversible eses have introduced further questions about the required features
of their operational counterpart, suggesting that shared places are not always
a suitable choice ([29, 30, 21]). It has been recently shown that the
operational model behind (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 [21] rather than relying on a shared
place in which one transition produces a token to be consumed by another one.
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
(depicted as boxes) that consume and produce tokens (bullets) in different
places (circles). According to the black arrows in Fig. 2(a), the transition
$a$ consumes a token from $s_{1}$ producing a token in $s_{4}$; similarly the
transition $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 contains 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}$. $N_{P}$ in Fig. 2(a) is the _classical_ operational
counterpart of the es $P$ in Fig. 1(a). However, we note that both the
causalities and conflicts in $N_{P}$ can be alternatively represented by using
inhibitor arcs instead of shared places, as shown in Fig. 2(b). 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$. The net in Fig. 2(b) can be made
reversible by adding a reversing transition for each reversible event, as
shown in Fig. 2(c) (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 are also used for modelling 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 ideas presented in [21] so to be able to deal
with raeses (and not just with the subclass of reversible peses). This is
achieved by using inhibitor arcs to represent, not only causal dependencies,
but also (symmetric) conflicts. In this way, all the dependencies between
transitions are modelled _uniformly_ by using inhibitor arcs. Concretely, 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 by following the long tradition of comparing
concurrency models in categorical terms [28, 38, 39]. To do so we first turn
raeses and racnes into categories by providing suitable notions of morphisms,
then we introduce two functors relating these categories and finally we show
that the functor that associates raeses to racnes is the left adjoint of the
one that that give racnes out of raeses. Besides establishing a correspondence
between raeses and racnes, this allows us to reinterpret the results in [21]
categorically.

This paper is an extended and enhanced version of [23]. In this presentation,
we have refined the concept of morphisms for causal nets, specifically by
relaxing the requirements on inhibitor arcs that capture causality when
conflicting transitions are collapsed in the morphism’s image. Additionally,
we include technical details omitted in the conference paper, and we furnish
complete proofs of the results. Additional examples and explanations have been
added. Also, Section 5 is completely new. Finally, the whole presentation has
been thoroughly refined and improved.

##### Structure of the paper

This paper is structured as follows: in Section 2 we recall Asymmetric Event
Structures and their reversible variants, along with their corresponding
categories. In Section 3 Asymmetric Causal Nets, reversible Asymmetric Causal
Nets and their categories are presented. The main results about categorical
connection are showns in Section 4. Section 5 discusses about some
applications of our results. Finally, Section 6 concludes the paper.

##  2\. Reversible Asymmetric Event Structures

In this section we recall the basics of Asymmetric Event Structures (aeses)
[3] and their reversible version introduced in [31, 11].

###  2.1. Asymmetric Event Structures

An aes consists of a set of events and two relations: _causality_ ($<$) and
_weak causality_ or _precedence_ ($\nearrow$). If $e$ weakly causes
$e^{\prime}$, written $e\nearrow e^{\prime}$, then $e$ cannot occur after
$e^{\prime}$; i.e., if both events occur in a computation, then $e$ precedes
$e^{\prime}$. In this case we say that $e^{\prime}$ is in an _asymmetric_
conflict with $e$. Events $e$ and $e^{\prime}$ are in (symmetric) conflict,
written $e\\#e^{\prime}$, iff $e\nearrow e^{\prime}$ and $e^{\prime}\nearrow
e$; intuitively, they cannot take place in the same computation.

An _Asymmetric Event Structure_ (aes) is a triple $\mathsf{G}=(E,<,\nearrow)$
where

  1. (1)

$E$ is a countable set of _events_ ;

  2. (2)

$<\ \subseteq E\times E$ is an irreflexive partial order, called _causality_ ,
defined such that $\forall e\in E$. $\lfloor e\rfloor=\\{{e^{\prime}\in
E}\mid{e^{\prime}\leq e}\\}$ is finite; and

  3. (3)

$\nearrow\ \subseteq E\times E$, called weak causality, is defined such that
for all $e,e^{\prime}\in E$:

    1. (a)

$e<e^{\prime}\ \Rightarrow\ e\nearrow e^{\prime}$;

    2. (b)

${\nearrow}\cap{(\lfloor e\rfloor\times\lfloor e\rfloor)}$ is acyclic; and

    3. (c)

if $e\\#e^{\prime}$ and $e^{\prime}<e^{\prime\prime}$ then
$e\\#e^{\prime\prime}$.

Each event can be attributed to a finite set of causes, as specified in
Condition 2. Moreover, weak causality is consistent with causality: if $e$ is
a cause of $e^{\prime}$, then $e$ is also a weak cause of $e^{\prime}$ (as
stated in Condition 3a). Additionally, circular dependencies among the causes
of an event are precluded by Condition 3b. Finally, (symmetric) conflicts
($\\#$) must be inherited along causality, as required by Condition 3c.

$b$$a$$c$

(a) aes $\mathsf{G}$

$a$$b$$c$

(b) aes $\mathsf{G}^{\prime}$

$\emptyset$$\\{b\\}$$\\{a\\}$$\\{a,b\\}$$\\{a,b,c\\}$

(c) $\mathsf{Conf}_{{{\textsc{aes}}}}(\mathsf{G})$

$\emptyset$$\\{a\\}$$\\{b\\}$$\\{a,c\\}$

(d) $\mathsf{Conf}_{{{\textsc{aes}}}}(\mathsf{G}^{\prime})$

Figure 3. Two aeses and their associated configurations.

Consider the aes $\mathsf{G}=(E,<,\nearrow)$ depicted in Figure 3(a), where
the set of events is $E=\\{a,b,c\\}$, the causality relation is defined such
that $a<c$ and $b<c$, and the weak causality is such that $a\nearrow b$,
$a\nearrow c$, and $b\nearrow c$. The set $E$ is finite, and hence countable
(Condition 1). It is straightforward to check that $<$ is an irreflexive
partial order and also that each event possesses a finite set of causes
(Condition 2), being $\lfloor a\rfloor=\\{a\\}$, $\lfloor b\rfloor=\\{b\\}$,
and $\lfloor c\rfloor=\\{a,b,c\\}$. Additionally, we have that $a<c$ and
$a\nearrow c$; and also $b<c$ and $b\nearrow c$, in accordance with Condition
3a. It is immediate to check that $\nearrow$ is acyclic on $\lfloor
a\rfloor,\lfloor b\rfloor$ and $\lfloor c\rfloor$ (Condition 3b). Moreover,
the conflict relation $\\#$ is empty, and hence Condition 3c is trivially
satisfied.

In the aes $\mathsf{G}^{\prime}=(E^{\prime},<^{\prime},\nearrow^{\prime})$ of
Fig. 3(b), the causality relation contains just $a<^{\prime}c$ and the weak
causality is
$a\nearrow^{\prime}b,b\nearrow^{\prime}a,a\nearrow^{\prime}c,b\nearrow^{\prime}c,c\nearrow^{\prime}b$.
In this case $\nearrow^{\prime}$ induces a symmetric conflict among $a$ and
$b$ and one among $b$ and $c$, hence $b\\#^{\prime}a$ and $b\\#^{\prime}c$,
and also the inheritance of conflicts along the causality relation is verified
(Condition 3c).

In the aes $\mathsf{G}^{\prime}=(E^{\prime},<^{\prime},\nearrow^{\prime})$
illustrated in Fig. 3(b), the causality relation comprises only
$a<^{\prime}c$, while weak causality is defined by $a\nearrow^{\prime}b$,
$b\nearrow^{\prime}a$, $a\nearrow^{\prime}c$, $b\nearrow^{\prime}c$, and
$c\nearrow^{\prime}b$. In this case, $\nearrow^{\prime}$ results in a
symmetric conflict between $a$ and $b$, as well as one between $b$ and $c$. As
a result, $b\\#^{\prime}a$ and $b\\#^{\prime}c$, satisfying the inheritance of
conflicts along causality (Condition 3c).

A _configuration_ of an aes $\mathsf{G}=(E,<,\nearrow)$ is a set $X\subseteq
E$ of events such that

  1. (1)

$\nearrow$ is well-founded on $X$;

  2. (2)

$\forall e\in X.\ \lfloor e\rfloor\subseteq X$; and

  3. (3)

$\forall e\in X$ the set $\\{{e^{\prime}\in X}\mid{e^{\prime}\nearrow e}\\}$
is finite.

The set of configurations of $\mathsf{G}$ is denoted by
$\mathsf{Conf}_{{{\textsc{aes}}}}(\mathsf{G})$.

A configuration comprises a set of events representing a potential partial
execution of $\mathsf{G}$. Condition 1 ensures that events in $X$ are not in
conflict, as circular weak-causal dependencies are forbidden. In accordance
with Condition 2, $X$ contains all the causes of its constituent events: an
event may occur only if its causes have already occurred. While a
configuration may be infinite, as in a non-terminating execution, each event
within a configuration has a finite set of weak causes (Condition 3).

For any pair of sets $X,Y\subseteq E$ where $X\subseteq Y$, we say that $Y$
_extends_ $X$ if, for all $e\in X$ and $e^{\prime}\in Y\setminus X$, there is
no weak-causal dependency ($\neg(e^{\prime}\nearrow e)$). In the context of
configurations, if $X$ and $Y$ are configurations, then $Y$ is considered
reachable from $X$.

The sets of configurations of the aeses $\mathsf{G}$ and $\mathsf{G}^{\prime}$
introduced in Section 2.1 are shown in Figs. 3(c) and 3(d) respectively. The
arrows represent the _extends_ relation. Straightforwardly configurations
satisfy the conditions in Definition 2.1.

A (finite) configuration $X=\\{e_{1},\dots,e_{n},\dots\\}$ of an aes
$\mathsf{G}$ is _reachable_ whenever the events in $X$ can be ordered in such
a way that for each $j\geq 1$ $\\{e_{1},\dots,e_{j}\\}$ extends
$\\{e_{1},\dots,e_{j-1}\\}$ and each
$\\{e_{1},\dots,e_{j}\\}\in\mathsf{Conf}_{{{\textsc{aes}}}}(\mathsf{G})$.

A morphism between aeses is a (possibly partial) mapping of events that
preserves computations (i.e., configurations).

Let $\mathsf{G}_{0}=(E_{0},<_{0},\nearrow_{0})$ and
$\mathsf{G}_{1}=(E_{1},<_{1},\nearrow_{1})$ be aeses. An aes-morphism, denoted
as $f:\mathsf{G}_{0}\rightarrow\mathsf{G}_{1}$, is defined as a partial
function $f:E_{0}\rightarrow E_{1}$ such that for all $e,e^{\prime}\in E_{0}$

  1. (1)

if $f(e)\neq\bot$ then $\lfloor f(e)\rfloor\subseteq f(\lfloor e\rfloor)$; and

  2. (2)

if $f(e)\neq\bot\neq f(e^{\prime})$ then

    1. (a)

$f(e)\nearrow_{1}f(e^{\prime})$ implies $e\nearrow_{0}e^{\prime}$; and

    2. (b)

$f(e)=f(e^{\prime})$ and $e\neq e^{\prime}$ imply $e\\#_{0}e^{\prime}$.

An aes-morphism preserves the causes of each mapped event (Condition 1) and
reflects its weak causes (Condition 2a). Additionally, it allows the mapping
of two distinct events to the same event only when those events are in
conflict (Condition 2b). The aforementioned conditions collectively guarantee
that morphisms preserve computations, or configurations, as stated below.

######  Proposition 1 ([3, Lemma 3.6]).

Let $f:\mathsf{G}_{0}\rightarrow\mathsf{G}_{1}$ be an aes-morphism and $X$ a
configuration of $\mathsf{G}_{0}$, i.e.,
$X\in\mathsf{Conf}_{{{\textsc{aes}}}}(\mathsf{G}_{0})$. Then,
$f(X)\in\mathsf{Conf}_{{{\textsc{aes}}}}(\mathsf{G}_{1})$.

Since aes-morphisms compose [3], aeses and aes-morphisms turn into a category,
which we denote by $\mathbf{AES}$.

###  2.2. Reversible aeses

We now provide a summary of _reversible_ aeses, introduced in [31, 11] as the
reversible counterparts ofaeses. Given a set $U$ of events and $u\in U$, we
write $\underline{u}$ for the undoing of $u$, and
$\underline{U}=\\{{\underline{u}}\mid{u\in U}\\}$ for the set of _undoings_ of
$U$.

A _Reversible Asymmetric Event Structure_ (raes) is a sextuple
$\mathsf{H}=(E,U,<,\nearrow,\prec,\lhd)$ where $E$ is the set of events,
$U\subseteq E$ is the set of _reversible_ events, and

  1. (1)

$\nearrow\ \subseteq E\times E$, called weak causality;

  2. (2)

$\lhd\subseteq\underline{U}\times E$, called _prevention_ ;

  3. (3)

$<\ \subseteq E\times E$, called causation, is an irreflexive relation defined
such that for all $e\in E$, $\lfloor e\rfloor_{<}=\\{{e^{\prime}\in
E}\mid{e^{\prime}\leq e}\\}$ is finite and ($\nearrow\cup<$) is acyclic on
$\lfloor e\rfloor_{<}$;

  4. (4)

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

    1. (a)

for all $u\in U.\ u\prec\underline{u}$;

    2. (b)

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

  5. (5)

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

  6. (6)

$(E,\prec\\!\\!\prec,\nearrow)$ with
${\prec\\!\\!\prec}={<}\cap{\\{(e,e^{\prime})\ |\ e\not\in U\textit{ or
}\underline{e}\lhd e^{\prime}\\}}$ is an aes.

An raes is defined in terms of a set of events $E$, with those in $U$ being
reversible.

Causation ($<$) and weak causality ($\nearrow$) delineate the forward flow,
while reverse causation ($\prec$, depicted as solid blue arrows) and
prevention ($\lhd$, represented by dashed blue arrows) describe the backward
flow. Weak causality serves the same role as in aeses, wherein $e\nearrow
e^{\prime}$ asserts that event $e$ cannot occur after event $e^{\prime}$.
Prevention, on the other hand, governs the undoing of events:
$\underline{e}\lhd e^{\prime}$ indicates that event $e$ cannot be undone if
event $e^{\prime}$ has occurred. Similar to causality in aeses, causation
indicates causal dependencies. Consistent with aeses, each event has the
finite set of causes $\lfloor e\rfloor_{<}$, and these sets do not contain
cyclic dependencies induced by causation and weak causality (Condition 3). The
acyclicity of $\lfloor e\rfloor_{<}$ implies that for all $e,e^{\prime}\in E$,
if $e<e^{\prime}$, then $\neg(e^{\prime}\nearrow e)$. Reverse causation
specifies the causes for the undoing of each event:
$e\prec\underline{e^{\prime}}$ states that $e^{\prime}$ 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, which is analogous to Condition
3, establishes that each undoing has a finite set of causes. Reverse causation
precisely states the causes for undoing each event:
$e\prec\underline{e^{\prime}}$ asserts that event $e^{\prime}$ can be undone
only if event $e$ has occurred. Therefore, Condition 4a straightforwardly
defines that an event $u$ can be undone only if it has occurred. Condition 4b,
akin to Condition 3, establishes that each undoing has a finite set of causes.
Just as causation and weak causality demand consistency, wherein an event
cannot have precedence over some of its causes (as defined in Condition 3), a
similar requirement is imposed on the backward flow by Condition 5.
Specifically, reverse causation must align with prevention: a cause $e$ of the
undoing of $u$ (i.e., $e\prec\underline{u}$) cannot prevent the undoing, i.e.,
$\neg(\underline{u}\lhd e)$. The final condition is the most intricate. It’s
noteworthy that the definition of raes does not mandate $(E,<,\nearrow)$ to be
an aes, particularly because conflicts may not be inherited along causation.
This flexibility is crucial for accommodating out-of-causal-order
reversibility (see the example below). Condition 5 considers instead the
relation $\prec\\!\\!\prec$, dubbed _sustained causation_. The sustained
causation is derived by excluding from causation all pairs $e<e^{\prime}$
where event $e$ can be undone even when $e^{\prime}$ has occurred (i.e.,
$\underline{e}\lhd e^{\prime}$ does not hold). It’s worth noting that
$\prec\\!\\!\prec$ coincides with $<$ when $U=\emptyset$; thus,
$(E,\emptyset,<,\nearrow,\emptyset,\emptyset)$ indeed constitutes an aes.

$\underline{b}$$a$$b$$c$

(a) raes $\mathsf{H}$

$\underline{b}$$\underline{c}$$a$$b$$c$

(b) raes $\mathsf{H}^{\prime}$

$\emptyset$$\\{a\\}$$\\{b\\}$$\\{a,b\\}$$\\{a,b,c\\}$

(c) $\mathsf{Conf}_{{{r\textsc{aes}}}}(\mathsf{H})$

$\emptyset$$\\{a\\}$$\\{b\\}$$\\{a,b\\}$$\\{a,c\\}$$\\{a,b,c\\}$

(d) $\mathsf{Conf}_{{{r\textsc{aes}}}}(\mathsf{H}^{\prime})$

Figure 4. Two raeses and their associated configurations.

Consider $\mathsf{H}=(E,U,<,\nearrow,\prec,\lhd)$ as depicted in Figure 4(a).
The (forward) events are $\\{a,b,c\\}$, where $b$ is the only reversible one
($U=\\{b\\}$). _Causation_ is defined such that $a<c$ and $b<c$, and weak
causality states $a\nearrow c,b\nearrow c,b\nearrow a$. _Reverse causation_ is
such that $a\prec\underline{b}$ and $b\prec\underline{b}$, and prevention is
$\underline{b}\lhd c$. Note that $c$ is caused by $a$ and $b$, with $b$ weakly
causing $a$ (or $a$ being in asymmetric conflict with $b$). Moreover, $b$ can
be reversed only when $a$ is present and $c$ has not been executed. In this
case, _sustained causation_ coincides with causation because the only
reversible event $b$ cannot be reversed if $c$ (which causally depends on $b$)
is present. It is routine to check that $(E,\prec\\!\\!\prec,\nearrow)$ is an
aes, and $\mathsf{H}$ is an raes.

Consider
$\mathsf{H}^{\prime}=(E,U^{\prime},<,\nearrow,\prec^{\prime},\lhd^{\prime})$
shown in Fig. 4(b), which has the same set of events, causation, and weak
causality as $\mathsf{H}$ but also takes $c$ as reversible (i.e.,
$U^{\prime}=\\{b,c\\}$). Reverse causation is extended with the pairs
$c\prec^{\prime}\underline{c}$, $a\prec^{\prime}\underline{b}$, and
$b\prec^{\prime}\underline{b}$. Observe that $b$ can be reversed even if the
event $c$ (which depends on $b$) has occurred. This is known as out-of-causal-
order reversibility. In this case, sustained causation consists only of
$a\prec\\!\\!\prec^{\prime}c$, i.e., the pair $b<c$ is removed because $b$ can
be reversed despite $c$ (which causally depends on $b$) having occurred. It
can be checked that $(E,\prec\\!\\!\prec^{\prime},\nearrow)$ is an aes, and
$\mathsf{H^{\prime}}$ is an raes.

For the sake of the presentation, Section 2.2 deviates in style from the
original definition in [31], where causation and reverse causation are merged,
and weak causality and prevention are combined in a single relation.
Additionally, we explicitly stipulate that $(E,\prec\\!\\!\prec,\nearrow)$
must constitute an aes, eliminating the need to restate conditions. Further
discussion is available in the Appendix.

The definition of configurations in raeses has an operational flavor grounded
in the concept of enabling. Consider $\mathsf{H}=(E,U,<,\nearrow,\prec,\lhd)$
as an raes, and let $X\subseteq E$ be a set of events such that $\nearrow$ is
acyclic on $X$. For $A\subseteq E$ and $B\subseteq U$, we say that
$A\cup\underline{B}$ is enabled at $X$ if $A\cap X=\emptyset$, $B\subseteq X$,
$\nearrow$ is acyclic on $A\cup X$, and

  1. (1)

for every $e\in A$, if $e^{\prime}<e$ then $e^{\prime}\in X\setminus B$ and if
$e\nearrow e^{\prime}$ then $e^{\prime}\not\in X\cup A$; and

  2. (2)

for every $u\in B$, if $e^{\prime}\prec\underline{u}$ then $e^{\prime}\in
X\setminus(B\setminus\\{u\\})$ and if $\underline{u}\lhd e^{\prime}$ then
$e^{\prime}\not\in X\cup A$.

The first condition ensures that $X$ contains all the causes of the events to
be added (i.e., those in $A$) but none of their preventing events. The second
condition asserts that $X$ includes the reverse causes of the events to be
undone (i.e., those in $B$) but none of the preventing ones. If
$A\cup\underline{B}$ is _enabled_ at $X$, then $X^{\prime}=(X\setminus B)\cup
A$ can be reached from $X$, denoted as $X\
\xlongrightarrow{A\cup\underline{B}}\ X^{\prime}$. The initial condition above
can be restated as follows: $\forall e\in A.\lfloor e\rfloor_{<}\subseteq X$
and $X\cup A$ extends $X$. Let $\mathsf{H}=(E,U,<,\nearrow,\prec,\lhd)$ be an
raes and $X\subseteq E$ a set of events that is well-founded with respect to
$(\nearrow\cup<)$. Then, $X$ is a _(reachable) configuration_ if there exist
two sequences of sets $A_{i}$ and $B_{i}$, for $i=1,\ldots,n$, such that

  1. (1)

$A_{i}\subseteq E$ and $B_{i}\subseteq U$ for all $i$, and

  2. (2)

$X_{i}\ \xlongrightarrow{A_{i}\cup\underline{B_{i}}}\ X_{i+1}$ for all $i$,
and $X_{1}=\emptyset$ and $X_{n+1}=X$.

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

The configurations of the raeses in Example 2.2 (along with the steps to reach
them) are illustrated in Figures 4(c) and 4(d). Notice that $\\{a,c\\}$—a
configuration of $\mathsf{H}^{\prime}$ but not of $\mathsf{H}$—is reached from
the configuration $\\{a,b,c\\}$ by undoing $b$.

Let $\mathsf{H}_{i}=(E_{i},U_{i},<_{i},\nearrow_{i},\prec_{i},\lhd_{i})$ with
$i=0,1$ be two raeses. An raes-morphism
$f:\mathsf{H}_{0}\rightarrow\mathsf{H}_{1}$ is an aes-morphism
$f:(E_{0},<_{0},\nearrow_{0})\rightarrow(E_{1},<_{1},\nearrow_{1})$ such that

  1. (1)

$f(U_{0})\subseteq U_{1}$;

  2. (2)

for all $u\in U_{0}$, if $f(u)\neq\bot$ then
$\lfloor\underline{f({u})}\rfloor_{\prec_{1}}\subseteq
f(\lfloor\underline{u}\rfloor_{\prec_{0}})$; and

  3. (3)

for all $e\in E_{0}$ and ${u}\in{U_{0}}$, if $f(e)\neq\bot\neq f(u)$ then
$\underline{f({u})}\lhd_{1}f(e)\ \Rightarrow\underline{u}\lhd_{0}e$.

Observe that $(E_{0},<_{0},\nearrow_{0})$ and $(E_{1},<_{1},\nearrow_{1})$ are
not necessarily aeses, but here it is enough that $f$ works on causation and
weak causality as an aes-morphism. Notice that raes-morphisms preserve the
causes (and the reverse causes) of each event (resp., reversing event), and
reflect preventions.

######  Proposition 2.

Let $f:\mathsf{H}_{0}\rightarrow\mathsf{H}_{1}$ be an raes-morphism and let
$X\in\mathsf{Conf}_{{{r\textsc{aes}}}}(\mathsf{H}_{0})$. Then
$f(X)\in\mathsf{Conf}_{{{r\textsc{aes}}}}(\mathsf{H}_{1})$.

######  Proof 2.1.

It suffices to demonstrate that, given $X\subseteq E_{0}$ such that
$\nearrow_{0}$ is acyclic on $X$, if $A\cup\underline{B}$ is enabled at $X$
(with $A\subseteq E_{0}$ and $B\subseteq U_{0}$), and $X\
\xlongrightarrow{A\cup\underline{B}}\ X^{\prime}$ (with
$X^{\prime}=(X\setminus B)\cup A$), then $f(A)\cup\underline{f(B)}$ is enabled
at $f(X)$. Observe that $f(A)\cap f(X)=\emptyset$ since $A\cap X=\emptyset$
and $f(B)\subseteq f(X)$ due to $B\subseteq X$. We now prove that
$\nearrow_{1}$ is acyclic on $f(X\cup A)=f(X)\cup f(A)$ by contradiction.
Suppose there exists a sequence of events $f(e_{0}),\dots,f(e_{n})$ in
$f(X\cup A)$ such that $f(e_{i})\nearrow_{1}f(e_{i+1})$, with $0\leq i<n$, and
$f(e_{n})\nearrow_{1}f(e_{0})$. However, as
$f:(E_{0},<_{0},\nearrow_{0})\rightarrow(E_{1},<1,\nearrow_{1})$ is an aes-
morphism, we have $e_{i}\nearrow_{0}e{i+1}$ for all $i\in\\{0,n-1\\}$, and
$e_{n}\nearrow_{0}e_{0}$, contradicting the acyclicity of $\nearrow_{0}$ on
$X\cup A$.

Now consider $e\in A$ such that $f(e)$ is defined and take $e^{\prime}<_{0}e$
such that $f(e^{\prime})$ is defined. As $f$ is an aes-morphism, if
$e^{\prime}\in X\setminus B$, then $f(e^{\prime})\in f(X)\setminus f(B)$, and
if $f(e)\nearrow_{1}f(e^{\prime})$, we have $e\nearrow_{0}e^{\prime}$,
implying that $e^{\prime}\not\in X\cup A$. Therefore, $f(e^{\prime})\not\in
f(X)\cup f(A)$.

Finally, consider $u\in B$ and assume $f(u)$ is defined. Take
$e^{\prime}\prec_{0}u$. If $f(e^{\prime})$ is defined, and since
$\lfloor\underline{f({u})}\rfloor_{\prec_{1}}\subseteq
f(\lfloor\underline{u}\rfloor_{\prec_{0}})$, we have that $f(e^{\prime})\in
f(X)\setminus(f(B)\setminus\\{f(u)\\})$ because $e^{\prime}\in
X\setminus(B\setminus\\{u\\})$. Now, consider
$\underline{f(u)}\lhd_{1}f(e^{\prime})$, which implies $f(e^{\prime})\not\in
f(X)\cup f(A)$ because $\underline{f(u)}\lhd_{1}f(e^{\prime})$ implies
$u\lhd_{0}e^{\prime}$ and $e^{\prime}\not\in X\cup A$. Hence $f(X)\
\xlongrightarrow{f(A)\cup\underline{f(B)}}\ f(X^{\prime})$. Observing that
configurations are subsets of events reachable from the empty one, we
establish the thesis.

As shown in [11], raes-morphisms compose; hence raeses and raes-morphisms are
a category, denoted with $\mathbf{RAES}$. Moreover, $\mathbf{AES}$ is a full
and faithful subcategory of $\mathbf{RAES}$.

###  2.3. Constructions

We conclude the section showing a categorical construction for raes. The
category of raeses has coproduct, as shown in [11]. We recall here the
construction adapting it to our definition of raes which is equivalent to the
one in [31] and [11], as we discuss in the appendix.

######  Proposition 3.

Let $\mathsf{H}_{0}=(E_{0},U_{0},<_{0},\nearrow_{0},\prec_{0},\lhd_{0})$ and
$\mathsf{H}_{1}=(E_{1},U_{1},<_{1},\nearrow_{1},\prec_{1},\lhd_{1})$ be two
raeses. Then $\mathsf{H}_{0}+\mathsf{H}_{1}=(E,U,<,\nearrow,\prec,\lhd)$ where

  * •

$E=\\{0\\}\times E_{0}\cup\\{1\\}\times E_{1}$;

  * •

$U=\\{0\\}\times U_{0}\cup\\{1\\}\times U_{1}$;

  * •

$(i,e)<(j,e^{\prime})$ whenever $i=j$ and $e<_{i}e^{\prime}$;

  * •

$(i,e)\nearrow(j,e^{\prime})$ whenever either $i=j$ and
$e\nearrow_{i}e^{\prime}$ or $i\neq j$;

  * •

$(i,e)\prec(j,u)$ whenever $i=j$ and $e\prec_{i}u$; and

  * •

$(i,u)\lhd(j,e)$ whenever either $i=j$ and $u\lhd_{i}e$ or $i\neq j$,

is their _coproduct_ and
$\iota_{i}:\mathsf{H}_{i}\to\mathsf{H}_{0}+\mathsf{H}_{1}$ defined as
$\iota_{i}(e)=(i,e)$ are the injections.

######  Proof 2.2.

$\mathsf{H}_{0}+\mathsf{H}_{1}$ is clearly a raes. To show that it is indeed a
coproduct, we consider any other raes
$\mathsf{H}^{\prime}=(E^{\prime},U^{\prime},<^{\prime},\nearrow^{\prime},\prec^{\prime},\lhd^{\prime})$
together with two morphisms $f_{i}:\mathsf{H}_{i}\to\mathsf{H}^{\prime}$. We
now show that the mapping
$g:\mathsf{H}_{0}+\mathsf{H}_{1}\to\mathsf{H}^{\prime}$ defined as
$g(i,e)=f_{i}(e)$ is a raes-morphism and it is unique. Clearly $\lfloor
g(i,e)\rfloor_{<^{\prime}}=\lfloor f_{i}(e)\rfloor_{<^{\prime}}\subseteq
f_{i}(\lfloor e\rfloor_{<_{i}})$ as $f_{i}$ is a raes-morphism, moreover if
$g(i,e)$ and $g(j,e^{\prime})$ are defined and
$g(i,e)\nearrow^{\prime}g(j,e^{\prime})$ we have two cases: either $i=j$ and
then $g(i,e)=f_{i}(e)$, $g(j,e^{\prime})=f_{i}(e^{\prime})$ and
$f_{i}(e)\nearrow f_{i}(e^{\prime})$ is because $e\nearrow_{i}e^{\prime}$, or
$i\neq j$, but in this case by construction we have $g(i,e)\nearrow
g(j,e^{\prime})$. Assume now that $g(i,e)$ and $g(j,e^{\prime})$ are defined
and equal. There are two cases: if $i=j$ then $f_{i}(e)\\#f_{i}(e^{\prime})$
and $e\\#_{i}e^{\prime}$, and if $i\neq j$ then we have again $g(i,e)\nearrow
g(j,e^{\prime})$ and $g(j,e^{\prime})\nearrow g(i,e)$ which implies
$g(i,e)\\#g(j,e^{\prime})$. Turning to the reverse part, clearly
$g(\\{0\\}\times U_{0}\cup\\{1\\}\times U_{1})=g(\\{0\\}\times U_{0})\cup
g(\\{1\\}\times U_{1})=f_{0}(U_{0})\cup f_{1}(U_{1})\subseteq U^{\prime}$, and
$\lfloor\underline{g(i,u)}\rfloor_{\prec^{\prime}}=\lfloor\underline{f_{i}(u)}\rfloor_{\prec^{\prime}}\subseteq
f_{i}(\lfloor\underline{u}\rfloor_{\prec})$ being $f_{i}$ a raes-morphism, and
for $g(i,u)\lhd^{\prime}g(j,e^{\prime})$ the reasoning goes as for
$\nearrow^{\prime}$, hence $(i,u)\lhd(j,e^{\prime})$, as required. Uniqueness
follows from the fact that the events are a coproduct in the category of sets
and partial mapping.

A direct construction of the product in the category of $\mathbf{RAES}$ is not
available.

##  3\. Reversible Asymmetric Causal Nets

We now introduce Asymmetric Causal Nets as a subclass of nets with inhibitor
arcs, wherein standard notions of causality and conflicts among transitions
are modelled via inhibitor arcs.

Firstly, we revisit the notion of nets with inhibitor arcs and subsequently
introduce asymmetric causal nets along with their reversible versions. We
develop appropriate notions of morphisms, turning asymmetric causal nets and
reversible asymmetric causal nets into categories.

###  3.1. Nets with inhibitor arcs

We summarise the basics of Petri net with inhibitor arcs along the lines of
[27, 2]. We write ${\rm Nature}$ for the set of natural numbers. A _multiset_
over a set $A$ is a function $m:A\rightarrow{\rm Nature}$. We assume the usual
operations of union ($+$) and difference ($-$) on multisets, and write
$m\subseteq m^{\prime}$ if $m(a)\leq m^{\prime}(a)$ for all $a\in A$. We will
use $\lBrace{\ldots\rBrace}$ when enumerating the elements of a multiset. The
multiset $[\\![{m}]\\!]$ is defined such that $[\\![{m}]\\!](a)=1$ if $m(a)>0$
and $[\\![{m}]\\!](a)=0$ otherwise. We often confuse a multiset $m$ with the
set $\\{{a\in A}\mid{m(a)\neq 0}\\}$ when $m=[\\![{m}]\\!]$. In such cases,
$a\in m$ denotes $m(a)\neq 0$, and $m\subseteq A$ signifies that $m(a)=1$
implies $a\in A$ for all $a$. The underlying set of a multiset $m$, namely the
one formed by the elements $a$ with $m(a)$, is precisely $[\\![{m}]\\!]$.
Additionally, we will employ standard set operations like $\cap$, $\cup$, or
$\setminus$. The set of all multisets over $A$ is denoted as $\mu A$; the
symbol $\mathsf{0}$ stands for the unique multiset defined such that
$[\\![{\mathsf{0}}]\\!]=\emptyset$.

A _Petri net with inhibitor arcs_ (ipt for short) is a tuple $N=\langle
S,T,F,I,\mathsf{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 $\mathsf{m}\in\mu S$ is the _initial marking_.

Given an ipt $N=\langle S,T,F,I,\mathsf{m}\rangle$ and $x\in S\cup T$, the
pre- and postset of $x$ are respectively defined as the (multi)sets ${\rm
Phys.~{}Rev.~{}E}{x}=\\{{y}\mid{(y,x)\in F}\\}$ and
${x}^{\bullet}=\\{{y}\mid{(x,y)\in F}\\}$. If $x\in S$ then ${\rm
Phys.~{}Rev.~{}E}{x}\in\mu T$ and ${x}^{\bullet}\in\mu T$; analogously, if
$x\in T$ then ${\rm Phys.~{}Rev.~{}E}{x}\in\mu S$ and ${x}^{\bullet}\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 ${\rm
Phys.~{}Rev.~{}E}{\cdot},{\cdot}^{\bullet},{}^{\circ}{\cdot}$ generalise
straightforwardly to multisets of transitions.

$s_{1}$$s_{2}$$s_{3}$$s_{4}$$s_{5}$$s_{6}$$a$$b$$c$

(a) $N_{1}$

$s_{1}$$s_{2}$$s_{3}$$s_{4}$$a$$b$

(b) $N_{2}$

$s_{1}$$s_{2}$$s_{3}$$s_{4}$$a$$b$

(c) $N_{3}$

$s_{1}$$s_{4}$$s_{2}$$s_{3}$$s_{5}$$s_{6}$$a$$b$$c$

(d) $N_{4}$

Figure 5. Some ipts.

Figure 5 introduces some ipts. The ipt $N_{1}$ in Figure 5(a) has six places
(named $s_{i}$) and three transitions $a$, $b$, and $c$. The initial marking
is $\mathsf{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}$, meaning its pre-, post-, and inhibiting sets are ${\rm
Phys.~{}Rev.~{}E}b=\\{s_{2}\\}$, ${b}^{\bullet}=\\{s_{5}\\}$, and
${}^{\circ}{b}=\\{s_{1}\\}$, respectively.

A (multiset of) transition(s) $A\in\mu T$ is enabled at a marking $m\in\mu S$,
written $m\,[\/{A}\/\rangle\,$, if ${{\rm Phys.~{}Rev.~{}E}{A}}\subseteq m$,
${}^{\circ}{A}\cap\ [\\![{m}]\\!]=\emptyset$ and $\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$ (${{\rm
Phys.~{}Rev.~{}E}{A}}\subseteq m$) and none of the transitions in $A$ is
inhibited in $m$ (${}^{\circ}{A}\cap\ [\\![{m}]\\!]=\emptyset$). The last
condition avoids cases in which a transition in $A$ produces tokens that
inhibit other transition in $A$. Observe that the multiset $\mathsf{0}$ is
enabled at every marking. If $A$ is enabled at $m$, then it can _fire_ and its
firing produces the marking $m^{\prime}=m-{\rm
Phys.~{}Rev.~{}E}{A}+{A}^{\bullet}$, which is written
$m\,[\/{A}\/\rangle\,m^{\prime}$. Hereafter, we assume that each transition
$t$ is defined such that ${\rm Phys.~{}Rev.~{}E}{t}\neq\emptyset$, i.e., it
cannot fire _spontaneously_ without consuming tokens.

A marking $m$ is _reachable_ if there exists a sequence of firings
$m_{i}\,[\/{A_{i}}\/\rangle\,m_{i+1}$ originated in the initial marking and
leading to $m$; $\mathcal{M}_{N}$ stands 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\mathcal{M}_{N}.m=[\\![{m}]\\!]$. From now on, we will only consider safe
ipts.

Consider the ipt $N_{4}$ in Figure 5(d). Both $b$ and $c$ are enabled at
marking $m=\\{s_{1},s_{2},s_{3}\\}$. On the contrary, $a$ is not enabled
because it is inhibited by the token in the place $s_{2}$. The firing of $b$
on $m$ produces the marking $m^{\prime}=\\{s_{1},s_{3},s_{5}\\}$, i.e.
$m\,[\/{b}\/\rangle\,m^{\prime}$. The transition $a$ is enabled at
$m^{\prime}$ while $c$ is disabled and cannot be fired because of the token in
$s_{5}$. The firing of $a$ on $m^{\prime}$ produces
$m^{\prime\prime}=\\{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}\\}$.

###  3.2. Asymmetric Causal Nets

In this section, we introduce Asymmetric Causal Nets, a class of ipts that
generalises the concept of Causal Nets introduced in [21] to accommodate
asymmetric conflicts. Broadly speaking, we focus on ipts where dependencies
between transitions arise solely from _inhibitor_ arcs. Similar to causal
nets, the property ${t}^{\bullet}\cap{\rm
Phys.~{}Rev.~{}E}{t^{\prime}}=\emptyset$ holds for all transitions $t$ and
$t^{\prime}$. This means that if a place appears in the preset of a
transition, it does not appear in the postset of any transition, and vice
versa. Consequently, the flow relation induces an empty causal relation.
However, causality can be recovered through inhibitor arcs. Intuitively, a
transition $t$ connected via an inhibitor arc to some place in the preset of
another transition $t^{\prime}$ cannot be fired before $t^{\prime}$ if we
assume that the preset of $t^{\prime}$ is marked. This is exemplified by
transitions $a$ and $b$ in Figure 5(d), where $a$ can only be fired after $b$.
The induced (immediate) causality relation $\lessdot$ is defined by $t\lessdot
t^{\prime}$ if and only if ${\rm
Phys.~{}Rev.~{}E}{t}\cap{}^{\circ}{t^{\prime}}\neq\emptyset$, signifying that
the firing of $t$ consumes (at least) one of the tokens inhibiting the firing
of $t^{\prime}$.

Additionally, asymmetric causal nets impose that places should not be shared
between the presets and postsets of transitions. Formally,
${t}^{\bullet}\cap{t^{\prime}}^{\bullet}\neq\emptyset\ \lor\ {\rm
Phys.~{}Rev.~{}E}{t}\cap{\rm Phys.~{}Rev.~{}E}{t^{\prime}}\neq\emptyset$
implies $t=t^{\prime}$ for all transitions $t$ and $t^{\prime}$. This ensures
that 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^{\prime}$ cannot be
fired if $t^{\prime}$ has been fired, i.e., $t^{\prime}$ prevents $t$. This is
exemplified by transitions $b$ and $a$ in Figure 5(b), where $b$ cannot be
fired after $a$ (i.e., $b$ is prevented by $a$). Therefore, the induced
prevention relation  $\leadsto$ is defined by
$t{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\
\mbox{\reflectbox{$\leadsto$}}\ }t^{\prime}$ if and only if
${t}^{\bullet}\cap{}^{\circ}{t^{\prime}}\neq\emptyset$. We use
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}$
to denote the inverse of  $\leadsto$ . It is important to note that
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}$
is analogous to the weak causality of aeses: if $t^{\prime}\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\
t$, then ${t}^{\bullet}\cap{}^{\circ}{t^{\prime}}\neq\emptyset$, indicating
that $t^{\prime}$ cannot be fired if $t$ has been fired; however, $t$ can be
fired after $t^{\prime}$. Similar to AES, _symmetric_ conflicts are retrieved
from prevention. That is, transitions $t$ and $t^{\prime}$ are in _symmetric_
conflict, denoted as $t{\natural}t^{\prime}$, whenever
$t{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\
\mbox{\reflectbox{$\leadsto$}}\ }t^{\prime}$ and $t\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\
t^{\prime}$.

Let $C=\langle S,T,F,I,\mathsf{m}\rangle$ be an ipt. $C$ is a _pre asymmetric
causal net_ (pacn) if the following conditions hold:

  1. (1)

$\forall t,t^{\prime}\in T.\ {t}^{\bullet}\cap{\rm
Phys.~{}Rev.~{}E}{t^{\prime}}=\emptyset$;

  2. (2)

$\forall t\in T$. $|{\rm Phys.~{}Rev.~{}E}{t}|=|{t}^{\bullet}|=1$;
$\mathsf{m}=S\setminus{T}^{\bullet}$; and ${}^{\circ}{T}\subseteq{\rm
Phys.~{}Rev.~{}E}T\cup{T}^{\bullet}$;

  3. (3)

$\lessdot^{+}$ is a partial order;

  4. (4)

$\forall t\in T.\ \lfloor t\rfloor_{\lessdot}=\\{{t^{\prime}\in
T}\mid{t^{\prime}\lessdot^{\ast}t}\\}$ is finite and
$({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\cup\lessdot)$
is acyclic on $\lfloor t\rfloor_{\lessdot}$; and

  5. (5)

$\forall t,t^{\prime}\in T.$ if ${\rm
Phys.~{}Rev.~{}E}{t}\cap{}^{\circ}{t^{\prime}}\neq\emptyset$ then
${t}^{\bullet}\cap{}^{\circ}{t^{\prime}}=\emptyset$ and if
${t}^{\bullet}\cap{}^{\circ}{t^{\prime}}\neq\emptyset$ then ${\rm
Phys.~{}Rev.~{}E}{t}\cap{}^{\circ}{t^{\prime}}=\emptyset$.

The first condition asserts that causal dependencies in a pacn are not
established through the flow relation. The second condition stipulates that a
place may appear in the preset or postset of at most one transition, and
places that are either isolated or part of the presets of all transitions are
initially marked.The condition on inhibitor arcs, denoted as
${}^{\circ}{T}\subseteq{\rm Phys.~{}Rev.~{}E}T\cup{T}^{\bullet}$, specifies
that these arcs should not link transitions to isolated places. This is
because their purpose is to represent dependencies between transitions that
are associated via the flow relation to those places. Since $\lessdot$ is
meant to model causal dependencies, the third condition requires its
transitive closure $\lessdot^{+}$ to form a partial order. The fourth
condition mandates that each transition $t$ has a finite set of causes,
ensuring that $\lessdot^{+}$ is a well-founded partial order. By enforcing the
acyclicity of
$({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\cup\lessdot)$
on the causes of every transition $t$, we ensure that causes of each
transition can be ordered to satisfy both causality and prevention. This
constraint excludes situations where (i) prevention contradicts causality
(e.g., $t\lessdot t^{\prime}$ and
$t^{\prime}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}t$),
(ii) circular chains of prevention exist (i.e.,
$t_{0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}t_{1}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\ldots{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}t_{n}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}t_{0}$),
where symmetric conflicts are a particular case, and (iii) self-blocked
transitions occur (i.e., $\lessdot$ needs to be irreflexive, implying ${{\rm
Phys.~{}Rev.~{}E}{t}}\cap{{}^{\circ}{t}}=\emptyset$ for all transitions $t$).
The last condition simply says that a transition cannot depends on one that
prevents it.

A pacn $C=\langle S,T,F,I,\mathsf{m}\rangle$ is an _asymmetric causal net_
(acn) if

  1. (1)

for all $t,t^{\prime}\in T$. $t\lessdot^{+}t^{\prime}$ implies $t\lessdot
t^{\prime}$;

  2. (2)

for all $t,t^{\prime}\in T$. $t\lessdot t^{\prime}$ implies $t\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\
t^{\prime}$; and

  3. (3)

for all $t,t^{\prime},t^{\prime\prime}\in T$, $t{\natural}t^{\prime}\land\
t^{\prime}\lessdot t^{\prime\prime}$ imply $t{\natural}t^{\prime\prime}$.

The additional conditions imposed on acns entails that all dependencies among
transitions must be explicitly represented in the structure of the net; in
other words, causality is saturated (Condition 1) and that all conflicts must
be explicitly represented in the net’s structure, ensuring the presence of
inhibitor arcs for all inherited symmetric conflicts (Condition 3). Condition
2 simply states that it ${\rm
Phys.~{}Rev.~{}E}{t}\cap{}^{\circ}{t^{\prime}}\neq\emptyset$ then
${t^{\prime}}^{\bullet}\cap{}^{\circ}{t}\neq\emptyset$. The inhibitor arc
$(s,t)$ with $\\{s\\}={t^{\prime}}^{\bullet}$ is somehow superflous, but it
follow the intuition that in an aes causality implies weak causality.

The ipts depicted in Figure 5 satisfy the conditions of acns. The first two
conditions of section 3.2 are met by all four nets, as transitions do not
share places in their pre and postsets. Additionally, the places in the
presets of all transitions are the only ones initially marked. For $N_{1}$
(Figure 5(a)), we observe that $a\lessdot b$ and $b\lessdot c$, making
$\lessdot^{+}$ a total order, and causality is saturated with the inclusion of
$a\lessdot c$. Furthermore,  $\leadsto$ is empty (as no transitions have
inhibitor arcs connected to the postset of other transitions), thus satisfying
the fourth condition. In the case of the net $N_{2}$ (Figure 5(b)), the
causality relation is empty, while prevention contains the sole pair
$a{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\
\mbox{\reflectbox{$\leadsto$}}\ }b$: $b$ cannot be fired after $a$, but $a$
can be executed after $b$. Figure 5(c) presents a similar net where $a$ and
$b$ are in symmetric conflict ($a{\natural}b$), meaning the execution of one
prevents the other. Finally, Figure 5(d) illustrates a net where $b\lessdot
a$, $b{\natural}c$, and $a{\natural}c$, with conflicts being inherited along
the causality relation $\lessdot$.

###  3.3. Configurations of a (pre) Asymmetric Causal Nets

We introduce additional concepts and findings related to (pre) acnes, in line
with our previous work in [21].

Given a function $f:A\to B$, the domain of $f$ is defined as
$\mathit{dom}(f)=\\{{a\in A}\mid{\exists b\in B.\ f(a)=b}\\}$. A sequence of
elements in $A$ is a (possibly partial) mapping $\rho:{\rm Nature}\rightarrow
A$ defined such that $n\in\mathit{dom}(\rho)$ implies
$n^{\prime}\in\mathit{dom}(\rho)$ for all $n^{\prime}<n$. Its length, denoted
by $\mathit{len}(\rho)$, is defined as the cardinality of its domain, i.e.,
$\mathit{len}(\rho)=|\mathit{dom}(\rho)|$. We say that $\rho$ is finite when
its length is so (i.e., $\mathit{len}(\sigma)<\infty$). We often write a
sequence $\rho$ as $a_{1}a_{2}\cdots$ where $a_{i}=\rho(i)$. Note that all
elements in a sequence are distinct if the the mapping is injective.

A _firing sequence_ $\sigma$ (abbreviated as fs $\sigma$) of an ipt $N=\langle
S,T,F,I,\mathsf{m}\rangle$ is a sequence of markings defined such that for
each $i\in dom(\sigma)$ there is a multiset of transitions $A_{i}$ enabled at
$\sigma(i)$ and $\sigma(i)\,[\/{A_{i}}\/\rangle\,\sigma(i+1)$. A fs $\sigma$
is written as $m_{0}\,[\/{A_{0}}\/\rangle\,m_{1}$ $\cdots$
$m_{n}\,[\/{A_{n}}\/\rangle\,m_{n+1}$ $\cdots$. Additionally,
$\mathit{start}(\sigma)$ indicates its initial marking $\sigma(0)=m_{0}$. If
$\sigma$ is finite, $\mathit{lead}(\sigma)$ designates its final marking
$\sigma(\mathit{len}(\sigma))$. We say that $\sigma$ starts at a marking $m$
if $\mathit{start}(\sigma)=m$, and let $\mathcal{R}^{N}_{m}$ denote the set of
all firing sequences of the ipt $N$ that start at $m$. A marking $m$ is
_reachable_ in $N$ if there exists an fs
$\sigma\in\mathcal{R}^{N}_{\mathsf{m}}$ such that $m=\mathit{lead}(\sigma)$.
The set of all reachable markings of $N$ is
$\mathcal{M}_{N}=\\{{\mathit{lead}(\sigma)}\mid{\sigma\in\mathcal{R}^{N}_{\mathsf{m}}}\\}$.

Let $C=\langle S,T,F,I,\mathsf{m}\rangle$ be a pacn. A set of transitions
$X\subseteq T$ is a _configuration_ of $C$ if

  1. (1)

$\forall t\in X$. $\lfloor t\rfloor_{\lessdot}\subseteq X$ (i.e., $X$ is _left
closed_ with respect to $\lessdot$); and

  2. (2)

${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\cup\lessdot$
is acyclic on $X$.

The set of configurations of a pacn $C$ is denoted by
$\mathsf{Conf}_{{p{\text{\sc acn}}}}(C)$.

The conditions imposed in the definition of acn ensure that
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\
\mbox{\reflectbox{$\leadsto$}}\ }$. In such case, the second condition can be
alternatively expressed as $\forall t,t^{\prime}\in X.\
\neg(t{\natural}t^{\prime})$.

If $X\in\mathsf{Conf}_{{p{\text{\sc acn}}}}(C)$, then the transitions of $X$
can be partially ordered with respect to $\lessdot\cup\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\
\mbox{\reflectbox{$\leadsto$}}\ }$. This means that there exists a sequence
$t_{1},\dots,t_{n}$ of the transitions in $X$ such that $t_{i}\lessdot t_{j}$
or $t_{i}\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\
t_{j}$ imply $i<j$.

######  Lemma 4.

Let $C=\langle S,T,F,I,\mathsf{m}\rangle$ be an pacn and let $X\subseteq T$ a
_configuration_ of $C$. Then $X$ can be partially ordered with respect to
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\cup\lessdot$.

######  Proof 3.1.

Take $X\in\mathsf{Conf}_{{p{\text{\sc acn}}}}(C)$. As $X$ is acyclic with
respect to
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\cup\lessdot$,
then we have that
$({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\cup\lessdot)^{\ast}\cap(X\times
X)$ is a partial order and then we have the thesis.

It is important to note a close correspondence between the configurations of a
acn and its reachable markings: any reachable marking corresponds to a
configuration of the net, and conversely.

######  Proposition 5.

Let $C=\langle S,T,F,I,\mathsf{m}\rangle$ be an pacn. Then,

  1. (1)

if $m^{\prime}\in\mathcal{M}_{C}$ then ${\rm
Phys.~{}Rev.~{}E}{m^{\prime}}\in\mathsf{Conf}_{{p{\text{\sc acn}}}}(C)$; and

  2. (2)

if $X\in\mathsf{Conf}_{{p{\text{\sc acn}}}}(C)$ is a reachable configuration
then $\mathsf{m}-{\rm Phys.~{}Rev.~{}E}{X}+{X}^{\bullet}\in\mathcal{M}_{C}$.

######  Proof 3.2.

  1. (1)

If $m^{\prime}\in\mathcal{M}_{C}$, then there exists a firing sequence
$\sigma$ such that $m^{\prime}=\mathit{lead}(\sigma)$. We prove by induction
on the length of the firing sequence that ${\rm
Phys.~{}Rev.~{}E}{m^{\prime}}\in\mathsf{Conf}_{{p{\text{\sc acn}}}}(C)$.

     * •

_Base case_ ($\mathit{len}(\sigma)=0)$. Then,
$\mathit{lead}(\sigma)=\mathsf{m}$ and ${\rm
Phys.~{}Rev.~{}E}{\mathsf{m}}=\emptyset$, which is a configuration in
$\mathsf{Conf}_{{p{\text{\sc acn}}}}(C)$.

     * •

_Inductive step_ ($\mathit{len}(\sigma)=n+1$). Then,
$\sigma=\sigma^{\prime}\,[\/{A}\/\rangle\,m^{\prime}$ with
$\mathit{len}(\sigma^{\prime})=n$. By inductive hypothesis on
$\sigma^{\prime}$, ${\rm
Phys.~{}Rev.~{}E}{\sigma(n)}\in\mathsf{Conf}_{{p{\text{\sc acn}}}}(C)$. Define
$X^{\prime}={\rm Phys.~{}Rev.~{}E}{\sigma(n)}$. From
$\sigma(n)\,[\/{A}\/\rangle\,$, we conclude that $A\cap X^{\prime}=\emptyset$,
because transitions cannot be fired twice in a pacn. Also, for all $t\in A$
and $t^{\prime}\lessdot t$, we have that $t^{\prime}\in X^{\prime}$ because
${}^{\circ}{t}\cap{\rm Phys.~{}Rev.~{}E}{t^{\prime}}\neq\emptyset$ (otherwise
$t$ would not be enabled at $\sigma(n)$). This implies that $X^{\prime}\cup A$
is left-closed with respect to $\lessdot$, i.e., $\lfloor
A\rfloor_{\lessdot}\subseteq X^{\prime}\cup A$.

It remains to show that
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\cup\lessdot$
is acyclic on $X^{\prime}\cup A$. Since $X^{\prime}$ is a configuration, its
transitions can be partially ordered according to
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\cup\lessdot$.
Moreover, $\forall t^{\prime}\in X^{\prime}$,
${t^{\prime}}^{\bullet}\subseteq\sigma(n)$. Hence, $t^{\prime}\in X^{\prime}$
implies
$\neg(t^{\prime}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}t)$
for all $t\in A$ (otherwise, $t$ would not be enabled at $\sigma(n)$). Since
$A$ is enabled, for all $t,t^{\prime}\in A$, neither
$t{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}t^{\prime}$
nor
$t{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}t^{\prime}$,
because $A$ enabled ensures that $\forall t\in[\\![{A}]\\!].\
{}^{\circ}{t}\cap{(A-\\{t\\})}^{\bullet}=\emptyset$. Consequently,
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\cup\lessdot$
is also acyclic on $X^{\prime}\cup A={\rm Phys.~{}Rev.~{}E}{m^{\prime}}$.

Therefore, we conclude that $m^{\prime}\in\mathcal{M}_{C}$ implies ${\rm
Phys.~{}Rev.~{}E}{m^{\prime}}\in\mathsf{Conf}_{{p{\text{\sc acn}}}}(C)$.

  2. (2)

Let $X$ be a reachable configuration. By Lemma 4, the elements of $X$ can be
partially ordered. That is, there exists a sequence $t_{1},\dots,t_{n}$ of the
elements of $X$ such that $t_{i}\lessdot t_{j}$ or $t_{i}\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\
t_{j}$ imply $i<j$. We prove by induction on the size $n$ of $X$ that
$m_{0}\,[\/{t_{1}}\/\rangle\,m_{1}\,[\/{t_{2}}\/\rangle\,\cdots
m_{n-1}\,[\/{t_{n}}\/\rangle\,m_{n}$ with $\mathsf{m}=m_{0}$ is a firing
sequence and $\forall i\in\\{1,\dots n\\}$, ${\rm
Phys.~{}Rev.~{}E}{m_{i}}=\\{t_{1},\dots,t_{i}\\}$ and $\mathsf{m}-{\rm
Phys.~{}Rev.~{}E}{X}+{X}^{\bullet}\in\mathcal{M}_{C}$.

     * •

_Base case_ ($n=0$). Hence, $X=\emptyset$. Then, the firing sequence is empty,
with $m_{0}=\mathsf{m}$. Moreover, ${\rm Phys.~{}Rev.~{}E}{m_{0}}=\emptyset=X$
and also $m_{0}=\mathsf{m}=\mathsf{m}-{\rm
Phys.~{}Rev.~{}E}\emptyset+{\emptyset}^{\bullet}=\mathsf{m}-{\rm
Phys.~{}Rev.~{}E}X+{X}^{\bullet}$.

     * •

_Inductive step_ ($n=k+1$). By inductive hypothesis, there exists a firing
sequence $m_{0}\,[\/{t_{1}}\/\rangle\,m_{1}\,[\/{t_{2}}\/\rangle\,\cdots
m_{k-1}\,[\/{t_{k}}\/\rangle\,m_{k}$ such that ${\rm
Phys.~{}Rev.~{}E}{m_{k}}=X\setminus\\{t_{k+1}\\}$ and $m_{k}=\mathsf{m}-{\rm
Phys.~{}Rev.~{}E}{(X\setminus\\{t_{k+1}\\})}+{(X\setminus\\{t_{k+1}\\})}^{\bullet}$.
Since $X$ is a configuration, $\lfloor t_{k+1}\rfloor_{\lessdot}\subseteq X$.
This implies that ${}^{\circ}{t_{k+1}}\cap m_{k}=\emptyset$. Additionally, if
$t^{\prime}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}t_{k+1}$
then $t^{\prime}\not\in X\setminus\\{t_{k+1}\\}$ (otherwise, $X$ would not be
a configuration). Hence, ${\rm
Phys.~{}Rev.~{}E}{m_{k}}\,[\/{t_{k+1}}\/\rangle\,$. Then, we can conclude that
$m_{0}\,[\/{t_{1}}\/\rangle\,m_{1}\,[\/{t_{2}}\/\rangle\,\cdots
m_{k-1}\,[\/{t_{k}}\/\rangle\,m_{k}\,[\/{t_{k+1}}\/\rangle\,m_{k+1}$ is a
reachable marking. Moreover, $m_{k+1}=m_{k}-{\rm
Phys.~{}Rev.~{}E}{t_{k+1}}+{t_{k+1}}^{\bullet}=\mathsf{m}-{\rm
Phys.~{}Rev.~{}E}{(X\setminus\\{t_{k+1}\\})}+{(X\setminus\\{t_{k+1}\\})}^{\bullet}-{\rm
Phys.~{}Rev.~{}E}{t_{k+1}}+{t_{k+1}}^{\bullet}=\mathsf{m}-{\rm
Phys.~{}Rev.~{}E}{X}+{X}^{\bullet}$ (where the last equality holds because
transitions do not share places). Also, ${\rm
Phys.~{}Rev.~{}E}{m_{k}}=X\setminus\\{t_{k+1}\\}$ implies that ${\rm
Phys.~{}Rev.~{}E}{m_{k+1}}=X$ because ${\rm Phys.~{}Rev.~{}E}{({\rm
Phys.~{}Rev.~{}E}{t_{k+1}})}=\emptyset$ and ${\rm
Phys.~{}Rev.~{}E}{({t_{k+1}}^{\bullet})}=t_{k+1}$.

We emphasize that the previous results remain valid even if the nets are acn,
as the inheritance of conflicts along the $\lessdot$ relation does not play
any role in the proofs above.

###  3.4. Morphisms for (pre) Asymmetric Causal Nets

We introduce a suitable notion of morphisms for pacns, which takes into
account that inhibitor arcs correspond to two distinct types of dependencies:
causality and prevention. In particular, inhibitor arcs representing
prevention demand a specific treatment of markings when compared to classical
notions of morphisms for nets [38, 39].

Let $C_{0}=\langle S_{0},T_{0},F_{0},I_{0},\mathsf{m}_{0}\rangle$ and
$C_{1}=\langle S_{1},T_{1},F_{1},I_{1},\mathsf{m}_{1}\rangle$ be pacns. An
acn-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}\rightarrow T_{1}$ defined such that

  1. (1)

for all $t\in T_{0}$ if $f_{T}(t)\neq\bot$ then

    1. (a)

${\rm Phys.~{}Rev.~{}E}{f_{T}(t)}=f_{S}({\rm Phys.~{}Rev.~{}E}{t})$ and
${f_{T}(t)}^{\bullet}=f_{S}({t}^{\bullet})$;

    2. (b)

$\forall(s,f_{T}(t))\in I_{1}$.

      1. (i)

if ${\rm Phys.~{}Rev.~{}E}{s}=\emptyset$ then $\exists s^{\prime}\in
f_{S}^{-1}(s)$. $(s^{\prime},t)\in I_{0}$;

      2. (ii)

if ${\rm Phys.~{}Rev.~{}E}{s}\neq\emptyset$ then $\forall s^{\prime}\in
f_{S}^{-1}(s)$. $(s^{\prime},t)\in I_{0}$.

  2. (2)

$\forall t,t^{\prime}\in T_{0}$ if $f_{T}(t)\neq\bot\neq f_{T}(t^{\prime})$
then $f_{T}(t)=f_{T}(t^{\prime})\ \Rightarrow\ t\ {\natural}_{0}\ t^{\prime}$.

  3. (3)

$\forall s_{1}\in S_{1}.\ \forall s_{0},s_{0}^{\prime}\in f_{S}^{-1}(s_{1}).$
$s_{0}\neq s_{0}^{\prime}$ implies ${s_{0}}^{\bullet}\ {\natural}_{0}\
{s_{0}^{\prime}}^{\bullet}$ or ${\rm Phys.~{}Rev.~{}E}{s_{0}}\ {\natural}_{0}\
{\rm Phys.~{}Rev.~{}E}{s_{0}^{\prime}}$;

  4. (4)

$[\\![{f_{S}(\mathsf{m}_{0})}]\\!]=\mathsf{m}_{1}$.

The initial two conditions adhere to the standard criteria for morphisms
between safe nets: the preservation of presets and postsets (Condition 1a),
and the reflection of inhibitor arcs (Conditions 1(b)i and 1(b)ii). The
inhibitor arcs modeling causality have to be reflected by finding a witness of
the causality, whereas those representing preventions have to be reflected in
every possible instance. Notably, Condition 1b implies that
${}^{\circ}{f_{T}(t)}\subseteq[\\![{f_{S}({}^{\circ}{t})}]\\!]$. Furthermore,
only conflicting transitions can be identified, as stipulated by Condition 2.

In contrast to conventional requirements, Condition 3 permits $f_{S}$ to
actively _identify_ places in the preset of different transitions. This might
raise concerns, as a place in the target of the morphism could represent
different tokens in the source, potentially evolving independently. However,
under the constraints of Condition 3, $f_{S}$ is only allowed to identify
places connected to transitions that are in (symmetric) conflict. Moreover,
the initial markings corresponds via the relation $f_{S}$ (Condition 4). It is
worth noting that the notion of morphisms remains unaffected by the
inheritance of symmetric conflicts along the causality relation, making these
conditions applicable to acnes as well.

Examine the acns $C_{0}$ and $C_{1}$ illustrated in Figure 6. The morphism
$(f_{S},f_{T}):C_{0}\rightarrow C_{1}$ is defined as follows. For transitions,
the mapping $f_{T}$ is defined by $f_{T}(a)=a^{\prime}$,
$f_{T}(b)=b^{\prime}$, and $f_{T}(c)=c^{\prime}=f_{T}(d)$, thereby identifying
the conflicting transitions $c$ and $d$. The relationship on places is
established as expected, specifically $f_{S}(s^{0}_{i},s^{1}_{i})$ for $1\leq
i\leq 6$, $f_{S}(s^{0}_{7},s^{1}_{3})$, and $f_{S}(s^{0}_{8},s^{1}_{6})$. The
inhibitor arc $(s^{1}_{3},b^{\prime})$ in $C_{1}$ is reflected by the arc
$(s^{0}_{3},b)$ in $C_{0}$. It is noteworthy that the mapping does not
preserve the remaining arcs of $C_{0}$.

$s_{1}^{0}$$s_{2}^{0}$$s_{3}^{0}$$s_{7}^{0}$$s_{4}^{0}$$s_{5}^{0}$$s_{6}^{0}$$s_{8}^{0}$$a$$b$$c$$d$

(a) $C_{0}$

$s_{1}^{1}$$s_{2}^{1}$$s_{3}^{1}$$s_{4}^{1}$$s_{5}^{1}$$s_{6}^{1}$$a^{\prime}$$b^{\prime}$$c^{\prime}$

(b) $C_{1}$

$s_{1}$$s_{2}$$s_{3}$${s_{4}}$${s_{5}}$${s_{6}}$$a$$b$$c$$\underline{b}$

(c) $V$

Figure 6.

The following result is instrumental for the following developments, and
ensures that any place in the preset of a transition (in the target of an acn-
morphisms) possesses a corresponding pre-image within the morphism.

######  Lemma 6.

Let $C_{0}=\langle S_{0},T_{0},F_{0},I_{0},\mathsf{m}_{0}\rangle$ and
$C_{1}=\langle S_{1},T_{1},F_{1},I_{1},\mathsf{m}_{1}\rangle$ be pacns, and
$(f_{S},f_{T}):C_{0}\rightarrow C_{1}$ an acn-morphism. Then, for all
$s_{1}\in S_{1}$, if ${\rm Phys.~{}Rev.~{}E}{s_{1}}=\emptyset$, then
$f_{S}^{-1}(s_{1})\neq\emptyset$.

######  Proof 3.3.

By contradiction. Assume $f_{S}^{-1}(s_{1})=\emptyset$. Hence, there does does
not exists $s_{0}\in S_{0}$ such that $f_{S}(s_{0})=s_{1}$. Hence,
$s_{1}\not\in f_{S}(\mathsf{m}_{0})$; and consequently,
$[\\![{f_{S}(\mathsf{m}_{0})}]\\!]\neq\mathsf{m}_{1}$, which contradicts the
hypothesis that $(f_{S},f_{T})$ is an acn-morphism (Section 3.4(4)).

In connection with a previous lemma, it is noteworthy that this property does
not hold for transitions, which do not have a guaranteed pre-image.
Additionally, places in the postset of transitions that are outside of the
image of the morphism, may not necessarily be within the image of the
morphism.

Now, our focus is on demonstrating that acn-morphisms preserve the token game;
specifically, a firing ($m\,[\/{A}\/\rangle\,m^{\prime}$) in the source net is
correspondingly translated to a firing in the target net. It is noteworthy
that not every marking is meaningful in a acn. For instance, we anticipate
that a marking should not simultaneously contain tokens for both the pre- and
postset of the same transition. Similarly, a valid marking is not expected to
place tokens in the postset of conflicting transitions. The upcoming
definition introduces the concept of markings that are coherent for acns.

Given a acn $C$, we say $m$ is a _coherent marking_ for $C$ if
$[\\![{m}]\\!]=m$,

  1. (1)

for all $t$, ${\rm Phys.~{}Rev.~{}E}{t}\in m$ iff ${t}^{\bullet}\not\in m$.

  2. (2)

for all $t,t^{\prime}$, $t\ {\natural}\ t^{\prime}$ and ${t}^{\bullet}\in m$
implies ${t^{\prime}}^{\bullet}\not\in m$.

Another important consideration is that an acn-morphism may collapse different
conflicting transitions in the source into a single transition in the target.
In other words, two conflicting transitions $t$ and $t^{\prime}$ may be mapped
to the same transition in the target, denoted as $f_{T}(t)=f_{T}(t^{\prime})$.
Consequently, $f_{S}({\rm Phys.~{}Rev.~{}E}t)=f_{S}({\rm
Phys.~{}Rev.~{}E}{t^{\prime}})$ and
$f_{S}({t}^{\bullet})=f_{S}({t^{\prime}}^{\bullet})$. Therefore, a coherent
marking in the source that includes ${t}^{\bullet}$ and ${\rm
Phys.~{}Rev.~{}E}{t^{\prime}}$ corresponds to an execution where the conflict
has been resolved–—$t$ has been fired, and subsequently, $t^{\prime}$ is
precluded. When mapping such a marking to the target, the conventional
approach in morphisms for Petri nets, applying $f_{S}$ to the marking, would
include both $f_{S}({t}^{\bullet})$ and $f_{S}({\rm
Phys.~{}Rev.~{}E}{t^{\prime}})$ in the target marking. Since
$f_{T}(t)=f_{T}(t^{\prime})$, this would result in a marking that is not
coherent for the net in the target of the morphism. Therefore, when mapping a
marking, it is imperative to account for conflicts that have already been
resolved. Specifically, tokens in the preset of transitions that were in
conflict with others that have been fired must be disregarded. This is
formally addressed by the next definition, which defines the relevant
information of a marking.

The next results establish the correspondence among firing between acns
related via a morphism.

Let $(f_{S},f_{T}):C_{0}\rightarrow C_{1}$ be an acn-morphism, and $m$ a
coherent marking of $C_{0}$. The _relevant information of_ $m$ is
$\underline{m}=m-\lBrace{s}\mid{s,s^{\prime}\in m\land s\in{\rm
Phys.~{}Rev.~{}E}{t}\land s^{\prime}\in{t^{\prime}}^{\bullet}\land t\
{\natural}\ t^{\prime}}\rBrace$

######  Proposition 7.

Let $(f_{S},f_{T}):C_{0}\rightarrow C_{1}$ be an acn-morphism, and $m$ a
coherent marking of $C_{0}$. Then, $m\,[\/{A}\/\rangle\,m^{\prime}$ implies
$m^{\prime}$ coherent and
$[\\![{f_{S}(\underline{m})}]\\!]\,[\/{f_{T}(A)}\/\rangle\,[\\![{f_{S}(\underline{m^{\prime}})}]\\!]$.

######  Proof 3.4.

Assume $m\,[\/{A}\/\rangle\,$. Since $A$ is enabled at $m$, we have (i) ${{\rm
Phys.~{}Rev.~{}E}{A}}\subseteq m$, (ii) ${}^{\circ}{A}\cap\
[\\![{m}]\\!]=\emptyset$, and (iii) $\forall t\in[\\![{A}]\\!].\
{}^{\circ}{t}\cap{(A-\\{t\\})}^{\bullet}=\emptyset$. Firstly, we show that
$f_{S}({\rm Phys.~{}Rev.~{}E}{A})=[\\![{f_{S}({\rm
Phys.~{}Rev.~{}E}{A})}]\\!]$. Suppose the contrary, i.e., $f_{S}({\rm
Phys.~{}Rev.~{}E}{A})\neq[\\![{f_{S}({\rm Phys.~{}Rev.~{}E}{A})}]\\!]$. Since,
$m$ is a set, then all transitions in $A$ are different, otherwise $A$ would
not be enabled at $A$. Since $C_{0}$ is an acns, each of its transitions has
just one place in its preset; i.e., for all $t\in C_{0}$, ${\rm
Phys.~{}Rev.~{}E}{t}$ is a singleton. Consequently, there should be two
different transitions $t\neq t^{\prime}\in A$ whose preset is mapped to the
same place, i.e., $f_{S}({\rm Phys.~{}Rev.~{}E}{t})=f_{S}({\rm
Phys.~{}Rev.~{}E}{t^{\prime}})$. Since $(f_{S},f_{T})$ is a pacn morphism, $t\
{\natural}_{0}\ t^{\prime}$ by Section 3.4(2), which contradicts the
assumption that $A$ is enabled at $m$. Hence, $f_{S}({\rm
Phys.~{}Rev.~{}E}{A})=[\\![{f_{S}({\rm Phys.~{}Rev.~{}E}{A})}]\\!]$. From (i),
we conclude that $[\\![{f_{S}({\rm
Phys.~{}Rev.~{}E}{A})}]\\!]\subseteq[\\![{f_{S}(m)}]\\!]$. By contradiction,
we show that $[\\![{f_{S}({\rm
Phys.~{}Rev.~{}E}{A})}]\\!]\subseteq[\\![{f_{S}(m)}]\\!]$ implies
$[\\![{f_{S}({\rm
Phys.~{}Rev.~{}E}{A})}]\\!]\subseteq[\\![{f_{S}(\underline{m})}]\\!]$. Suppose
there is $s\in{f_{S}({\rm Phys.~{}Rev.~{}E}{A})}$, $s\in f_{S}(m)$, and
$s\not\in f_{S}(\underline{m})$. Hence, there exist $s^{\prime}$ and
$t^{\prime}$ such that $s^{\prime}\in m$,
$s^{\prime}\in{t^{\prime}}^{\bullet}$ and $t^{\prime}\ {\natural}t$. But this
implies $t$ is not enabled at $m$, contradicting (ii). Hence,
$[\\![{f_{S}({\rm
Phys.~{}Rev.~{}E}{A})}]\\!]\subseteq[\\![{f_{S}(\underline{m})}]\\!]$. Since
$(f_{S},f_{T})$ is a pacn morphism, ${\rm
Phys.~{}Rev.~{}E}{f_{T}(A)}=f_{S}({\rm Phys.~{}Rev.~{}E}{A})=[\\![{f_{S}({\rm
Phys.~{}Rev.~{}E}{A})}]\\!]$; and consequently, ${\rm
Phys.~{}Rev.~{}E}{f_{T}(A)}\subseteq[\\![{f_{S}(\underline{m})}]\\!]$.

Secondly, we show that ${}^{\circ}{f_{T}(A)}\cap\
[\\![{f_{S}(\underline{m})}]\\!]=\emptyset$. We proceed by contradiction.
Assume that there exist $t\in A$ and $s\in[\\![{f_{S}(\underline{m})}]\\!]$
such that $s$ inhibits $f_{T}(t)$, i.e., $s\in{}^{\circ}{f_{T}(t)}$. We have
two cases:

  * •

${\rm Phys.~{}Rev.~{}E}s=\emptyset$: Since
$s\in[\\![{f_{S}(\underline{m})}]\\!]$, we conclude
$f_{S}^{-1}(s)\neq\emptyset$. Hence, there exists $s^{\prime}\in S_{0}$ such
that $(s^{\prime},s)\in f_{S}$ and $s^{\prime}\in{}^{\circ}{t}$, because
inhibitor arcs are reflected by Section 3.4(1(b)i). Since $C_{0}$ is an acn,
there exists exactly one transition $t^{\prime}\in T_{0}$ such that
$s^{\prime}\in{\rm Phys.~{}Rev.~{}E}{t^{\prime}}$. There are two cases:

    * –

$s^{\prime}\in\underline{m}$: Hence, we have $s^{\prime}\in m$ and
$s^{\prime}\in{}^{\circ}{t}$, $t\in A$; which is in contradiction with (ii).

    * –

$s^{\prime}\not\in\underline{m}$. Since
$f_{S}(s^{\prime})\in[\\![{f_{S}(\underline{m})}]\\!]$, there should exist
$s^{\prime\prime}\in\underline{m}$ such that
$f(s^{\prime\prime})=f(s)^{\prime}=s$. Let $t^{\prime\prime}$ be the
transition such that $s^{\prime\prime}\in{\rm
Phys.~{}Rev.~{}E}t^{\prime\prime}$. Since $(f_{S},f_{T})$ is an acn-morphism,
${s^{\prime}}^{\bullet}\ {\natural}\ {s^{\prime\prime}}^{\bullet}$ (Section
3.4(3)). Hence, $t^{\prime}\ {\natural}\ t^{\prime\prime}$. Since $m$ is a
coherent marking, $s^{\prime}\not\in m$ implies ${t^{\prime}}^{\bullet}\in m$.
Since ${t^{\prime}}^{\bullet}\in m$ and $t^{\prime}\ {\natural}\
t^{\prime\prime}$, by definition of relevant information of a marking, we
conclude that ${\rm Phys.~{}Rev.~{}E}t^{\prime\prime}\not\in\underline{m}$,
which contradicts the assumption $s^{\prime\prime}\in\underline{m}$.

  * •

${\rm Phys.~{}Rev.~{}E}s\neq\emptyset$. Since
$s\in[\\![{f_{S}(\underline{m})}]\\!]$, then there exist
$s^{\prime}\in\underline{m}\subseteq m$ such that $f_{S}(s^{\prime})=s$. By
Section 3.4(1(b)ii), inhibitor arcs are reflected, and hence
$s^{\prime}\in{}^{\circ}{t}$, which contradicts (ii).

Finally, we show that $\forall t\in[\\![{f_{T}(A)}]\\!].\
{}^{\circ}{t}\cap{(f_{T}(A)-\\{t\\})}^{\bullet}=\emptyset$. If this were not
the case, then there would exist $t_{1}\in f_{T}(A)$ such that $t_{1}\neq t$
and ${}^{\circ}{t}\cap{t_{1}}^{\bullet}\neq\emptyset$. Since $(f_{S},f_{T})$
is a pacn morphism, there would exists $t^{\prime},t_{1}^{\prime}\in A$ such
that $f_{S}(t^{\prime})=t$ and $f_{S}(t_{1}^{\prime})=t_{1}$ and
${}^{\circ}{t}^{\prime}\cap{t_{1}^{\prime}}^{\bullet}$, which contradicts
(iii). Consequently, ${f_{T}(A)}$ is enabled at
$[\\![{f_{S}(\underline{m})}]\\!]$. Moreover,
$[\\![{f_{S}(\underline{m})}]\\!]\,[\/{f_{T}(A)}\/\rangle\,[\\![{f_{S}(\underline{m}^{\prime})}]\\!]$
as
$[\\![{f_{S}(\underline{m}^{\prime})}]\\!]=[\\![{f_{S}(\underline{m})}]\\!]-[\\![{f_{S}({\rm
Phys.~{}Rev.~{}E}{A})}]\\!]+[\\![{f_{S}({A}^{\bullet})}]\\!]$.

The next results shows that acn-morphisms are closed under composition.

######  Lemma 8.

Let $(f_{S},f_{T}):C_{0}\rightarrow C_{1}$ and $(g_{S},g_{T}):C_{1}\rightarrow
C_{2}$ be two acn-morphisms. Then $(f_{S};g_{S},f_{T};g_{T}):C_{0}\rightarrow
C_{2}$ is a acn-morphism as well.

######  Proof 3.5.

We check the conditions of Section 3.4.

  1. (1)

Take $t\in T_{0}$ if $f_{T};g_{T}(t)\neq\bot$ then

    1. (a)

Since $f_{T}$ and $g_{T}$ define morphisms, we have that ${\rm
Phys.~{}Rev.~{}E}(f_{T};g_{T})(t)={\rm Phys.~{}Rev.~{}E}g_{T}(f_{T}({\rm
Phys.~{}Rev.~{}E}t))=g_{S}(f_{S}({\rm
Phys.~{}Rev.~{}E}{t}))=(f_{S};g_{S})({\rm Phys.~{}Rev.~{}E}t)$. By analogous
reasoning, we deduce that
${(f_{T};g_{T})(t)}^{\bullet}=(f_{S};g_{S})({t}^{\bullet})$.

    2. (b)

Consider $(s,f_{T};g_{T}(t))\in I_{2}$.

      1. (i)

Assume ${s}^{\bullet}\neq\emptyset$, and
$f_{S}^{-1}(g_{S}^{-1}(s))\neq\emptyset$. By the definition of
$(g_{S},g_{T})$, there exists $\tilde{s}\in g_{S}^{-1}(s)$.
$(\tilde{s},f_{T}(t))\in I_{1}$. Furthermore
${\tilde{s}}^{\bullet}\neq\emptyset$. Again by definition of $(f_{S},f_{T})$,
we have again that there is an $s^{\prime}\in g_{T}^{-1}(g_{S}^{-1}(s))$ such
that $(s^{\prime},t)\in I_{0}$. We can conclude that if $(s,f_{T};g_{T}(t))\in
I_{2}$ and if $f_{S}^{-1}(g_{S}^{-1}(s))\neq\emptyset$ then we have that there
exists $s^{\prime}\in(f_{T};g_{T})^{-1}(s))$, $(s^{\prime},t)\in I_{0}$.

      2. (ii)

Assume ${s}^{\bullet}=\emptyset$. By the definition of $(g_{S},g_{T})$, for
all $\tilde{s}\in g_{S}^{-1}(s)$. $(\tilde{s},f_{T}(t))\in I_{1}$. Furthermore
${\tilde{s}}^{\bullet}=\emptyset$. Again by definition of $(f_{S},f_{T})$, we
have that for all $s^{\prime}\in g_{T}^{-1}(g_{S}^{-1}(s))$ we have
$(s^{\prime},t)\in I_{0}$. We can conclude that if $(s,f_{T};g_{T}(t))\in
I_{2}$, then for all $s^{\prime}\in(f_{T};g_{T})^{-1}(s))$ we have
$(s^{\prime},t)\in I_{0}$.

  2. (2)

Assume $f_{T};g_{T}(t)=f_{T};g_{T}(t^{\prime})$. There are two cases:

     * •

$f_{T}(t)=f_{T}(t^{\prime})$. Then, $t\ {\natural}_{0}\ t^{\prime}$ because
$(f_{S},f_{T})$ is an acn morphism.

     * •

$f_{T}(t)\neq f_{T}(t^{\prime})$ and $g_{T}(t)=g_{T}(t^{\prime})$. Since,
$(g_{S},g_{T})$ is an acn morphism, $f_{S}(t)\ {\natural}_{1}\
f_{s}(t^{\prime})$. By definition of symmetric conflicts,
${f_{S}(t)}^{\bullet}\ \cap\ {}^{\circ}{f_{S}(t^{\prime})}\neq\emptyset$ and
${f_{S}(t^{\prime})}^{\bullet}\ \cap\ {}^{\circ}{f_{S}(t)}\neq\emptyset$.
Since pacn are defined such that the postset of every transition is a
singleton, we have that ${f_{S}(t)}^{\bullet}\ \subseteq\
{}^{\circ}{f_{S}(t^{\prime})}$ and ${f_{S}(t^{\prime})}^{\bullet}\ \subseteq\
{}^{\circ}{f_{S}(t)}$. Since $(f_{S},f_{T})$ is a pacn-morphism, we have that
${t^{\prime}}^{\bullet}\ \subseteq\ {}^{\circ}{t}$ and ${t}^{\bullet}\
\subseteq\ {}^{\circ}{t^{\prime}}$, by Section 3.4(1b). Consequently, $t\
{\natural}_{0}\ t^{\prime}$.

  3. (3)

We check that $\forall s_{2}\in S_{2}$, $\forall s_{0},s_{0}^{\prime}\in
f_{S}^{-1}(g_{S}^{-1}(s_{2}))$ either ${s_{0}}^{\bullet}\ {\natural}_{0}\
{s_{0}^{\prime}}^{\bullet}$ or ${\rm Phys.~{}Rev.~{}E}{s_{0}}\ {\natural}_{0}\
{\rm Phys.~{}Rev.~{}E}{s_{0}^{\prime}}$. Therefore, either there exists a
place $s_{1}\in g_{S}^{-1}(s_{2})$ such that both $s_{0}$ and $s_{0}^{\prime}$
belong to $f_{S}^{-1}(s_{1})$, or there are two places $s_{1}$ and
$s_{1}^{\prime}$ in $g_{S}^{-1}(s_{2})$ and $s_{0}$ and $s_{0}^{\prime}$ are
both in $f_{S}^{-1}(\\{s_{1},s_{1}^{\prime}\\})$. In the first case
${s_{0}}^{\bullet}\ {\natural}_{0}\ {s_{0}^{\prime}}^{\bullet}$ or ${\rm
Phys.~{}Rev.~{}E}{s_{0}}\ {\natural}_{0}\ {\rm
Phys.~{}Rev.~{}E}{s_{0}^{\prime}}$ holds as $(f_{S},f_{T})$ is an acn-
morphism; in the second case we have ${s_{1}}^{\bullet}\ {\natural}_{1}\
{s_{1}^{\prime}}^{\bullet}$ or ${\rm Phys.~{}Rev.~{}E}{s_{1}}\ {\natural}_{1}\
{\rm Phys.~{}Rev.~{}E}{s_{1}^{\prime}}$ as $(g_{S},g_{T})$ is a acn-morphism.
Since, conflicts are reflected, also ${s_{0}}^{\bullet}\ {\natural}_{0}\
{s_{0}^{\prime}}^{\bullet}$ or ${\rm Phys.~{}Rev.~{}E}{s_{0}}\ {\natural}_{0}\
{\rm Phys.~{}Rev.~{}E}{s_{0}^{\prime}}$ holds.

  4. (4)

Condition $[\\![{f_{S};g_{S}(m_{0})}]\\!]=m_{2}$ straightforwardly follows by
the definitions of $f_{S}$ and $g_{S}$ that ensure
$[\\![{f_{S}(m_{0})}]\\!]=m_{1}$ and $[\\![{g_{S}(m_{1})}]\\!]=m_{2}$.

We designate the category of pacns and acn-morphisms as $\mathbf{pACN}$.
Within this category, there exists a full and faithful subcategory denoted as
$\mathbf{ACN}$, wherein the objects are acns. This subcategory,
$\mathbf{ACN}$, is the specific category of interest.

####  3.4.1. Morphisms and configurations:

We conclude this part by noticing that morphisms preserve configurations, a
fact established through the lemma presented below.

######  Lemma 9.

Let $(f_{S},f_{T}):C_{0}\rightarrow C_{1}$ be an acn-morphism. Then

  1. (1)

for all $t\in T_{0}$, if $f_{T}(t)\neq\bot$ then $\lfloor
f_{T}(t)\rfloor_{\lessdot_{1}}\subseteq f_{T}(\lfloor
t\rfloor_{\lessdot_{0}})$; and

  2. (2)

for all $t_{0},t_{0}^{\prime}\in T_{0}$ such that $f_{T}(t_{0})\neq\bot\neq
f_{T}(t_{0}^{\prime})$, if
$f_{T}(t_{0}){\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\
\mbox{\reflectbox{$\leadsto$}}\ }_{1}\ f_{T}(t_{0}^{\prime})$ then
$t_{0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\
\mbox{\reflectbox{$\leadsto$}}\ }_{0}\ t_{0}^{\prime}$.

######  Proof 3.6.

  1. (1)

Take $t\in T_{0}$ such that $f_{T}(t)\neq\bot$. For each $t_{0}\in\lfloor
f_{T}(t)\rfloor_{\lessdot_{1}}$ we have that either ${\rm
Phys.~{}Rev.~{}E}{t_{0}}\cap{}^{\circ}{f_{T}(t)}\neq\emptyset$ or there exists
transitions $t_{1},\dots,t_{n}\in\lfloor f_{T}(t_{0})\rfloor_{\lessdot_{1}}$
such that $({\rm Phys.~{}Rev.~{}E}{t_{0}},t_{1}),({\rm
Phys.~{}Rev.~{}E}{t_{1}},t_{2}),\dots,$ $({\rm
Phys.~{}Rev.~{}E}{t_{n}},f_{T}(t))\in I_{1}$. Since $(f_{S},f_{T})$ is a acn-
morphism, this leads to either a place $s_{0}\in S_{0}$ with
${s_{0}}^{\bullet}=t_{0}^{\prime}$, $f_{T}(t)=t_{0}^{\prime}$ and
$(s_{0},t_{0}^{\prime})\in I_{0}$, or the existence of
$s_{0},s_{1},\dots,s_{n}$ such that ${s_{i}}^{\bullet}=t_{i}^{\prime}$,
$f_{T}(t_{i}^{\prime})=t_{i}$ and $(s_{i},t_{i}^{\prime})\in I_{0}$. This
implies $f_{T}(t_{0}^{\prime})=t_{0}\in f_{T}(\lfloor
t_{0}\rfloor_{\lessdot_{1}})$. Thus, the inclusion is established.

  2. (2)

Assume
$f_{T}(t_{0}){\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\
\mbox{\reflectbox{$\leadsto$}}\ }_{1}\ f_{T}(t_{0}^{\prime})$, then
$(s,f_{T}(t_{0}))\in I_{1}$ and $s\in{f_{T}(t_{0}^{\prime})}^{\bullet}$, but
then for all $s^{\prime}\in f_{S}^{-1}(s)$ we have $(s^{\prime},t_{0})\in
I_{0}$ and there must be an $s^{\prime}\in{t_{0}^{\prime}}^{\bullet}$. But
then
$t_{0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\
\mbox{\reflectbox{$\leadsto$}}\ }_{0}\ t_{0}^{\prime}$.

######  Proposition 10.

Let $(f_{S},f_{T}):C_{0}\rightarrow C_{1}$ be an acn-morphism. If
$X\in\mathsf{Conf}_{{p{\text{\sc acn}}}}(C_{0})$, then
$f_{T}(X)\in\mathsf{Conf}_{{p{\text{\sc acn}}}}(C_{1})$.

######  Proof 3.7.

Take $X\in\mathsf{Conf}_{{p{\text{\sc acn}}}}(C_{0})$. Hence, for every
$t_{1}\in f_{T}(X)$, there exists $t_{0}\in X$ such that $f_{T}(t_{0})=t_{1}$.
By Proposition 9 $\lfloor f_{T}(t_{0})\rfloor_{\lessdot_{1}}\subseteq
f_{T}(\lfloor t_{0}\rfloor_{\lessdot_{0}})$. Then, it follows that $\lfloor
t_{1}\rfloor_{\lessdot_{1}}\subseteq f_{T}(X)$. It remains to show that
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}_{1}\cup\lessdot_{1}$
is acyclic on $f_{T}(X)$. We proceed by contradiction. Assume that
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}_{1}\cup\lessdot_{1}$
has a cycle on $f_{T}(X)$. Since both relations are induced by inhibitor arcs,
which are reflected by acn-morphisms, this implies that
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}_{0}\cup\lessdot_{0}$
has a cycle on $X$, which contradicts the assumption that $X$ is a
configuration. Therefore,
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}_{1}\cup\lessdot_{1}$
is acyclic on $f_{T}(X)$ and $f_{T}(X)\in\mathsf{Conf}_{{p{\text{\sc
acn}}}}(C_{1})$.

######  Corollary 11.

Let $(f_{S},f_{T}):C_{0}\rightarrow C_{1}$ be an acn-morphism and
$C_{0},C_{1}$ be two acnes. If $X\in\mathsf{Conf}_{{{\text{\sc acn}}}}(C_{0})$
then $f_{T}(X)\in\mathsf{Conf}_{{{\text{\sc acn}}}}(C_{1})$.

###  3.5. Reversible Asymmetric Causal Nets

In this section, we introduce the concept of Reversible Asymmetric Causal
Nets, following the approach outlined in [21]. We extend acns by incorporating
_backward_ transitions, responsible for undoing or reversing the effects of
previously executed _forward_ transitions, i.e., ordinary transitions. We
assume that the set $T$ of transitions in a net is divided into two sets:
$\overline{{T}}$ for forward transitions and $\underline{{T}}$ for backward
transitions. Furthermore, each backward transition
${\underline{t}}\in\underline{{T}}$ is designed to undo the effect of
precisely one forward transition ${t}\in\overline{{T}}$. Nonetheless, there
may be forward transitions that are irreversible. For simplicity, we will use
${t}$ to refer to the forward transition and ${\underline{t}}$ to denote its
associated reversing transition, when applicable.

An ipt $V=\langle S,T,F,I,\mathsf{m}\rangle$ is a _reversible Asymmetric
Causal Net_ (racn) if there exists a partition
$\\{\overline{{T}},\underline{{T}}\\}$ of $T$ (where $\overline{{T}}$
represents the forward transitions, and $\underline{{T}}$ denotes the backward
transitions) satisfying the following conditions:

  1. (1)

${V_{\overline{{T}}}}=\langle
S,\overline{{T}},F_{|\overline{{T}}\times\overline{{T}}},I_{|\overline{{T}}\times\overline{{T}}},\mathsf{m}\rangle$
is a pacn net;

  2. (2)

$\forall{\underline{t}}\in\underline{{T}}.\ \exists!\ {t}\in\overline{{T}}$
such that ${{t}}^{\bullet}={\rm Phys.~{}Rev.~{}E}{{\underline{t}}}$, ${\rm
Phys.~{}Rev.~{}E}{{t}}={{\underline{t}}}^{\bullet}$, and ${\rm
Phys.~{}Rev.~{}E}{{t}}\subseteq{}^{\circ}{{\underline{t}}}$;

  3. (3)

$\forall{\underline{t}}\in\underline{{T}}$.
$K_{{\underline{t}}}=\\{{{t}^{\prime}\in\overline{{T}}}\mid{{}^{\circ}{{\underline{t}}}\cap{\rm
Phys.~{}Rev.~{}E}{{t}^{\prime}{}}\neq\emptyset}\\}$ is finite and
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}$
acyclic on $K_{{\underline{t}}}$;

  4. (4)

$\forall{\underline{t}}\in\underline{{T}}.\ \forall{t}\in\overline{{T}}$ if
${\rm Phys.~{}Rev.~{}E}{t}\cap{}^{\circ}{{\underline{t}}}{}\neq\emptyset$ then
${{t}}^{\bullet}\cap{}^{\circ}{{\underline{t}}}{}=\emptyset$;

  5. (5)

$\forall{t},{t}^{\prime},{t}^{\prime\prime}\in\overline{{T}}.\ {t}\
{\natural}\ {t}^{\prime}\ \land\ {t}^{\prime}\lll{t}^{\prime\prime}\
\Rightarrow\ {t}\ {\natural}\ {t}^{\prime\prime}$ with $\lll$ being the
transitive closure of $\lessdot\cap\\{({t},{t}^{\prime})\ |\
{\underline{t}}\not\in\underline{{T}}\ \textit{or}\
{}^{\circ}{{\underline{t}}}\cap{{t}^{\prime}}^{\bullet}\neq\emptyset\\}$.

Sometimes we use ${V^{\underline{{T}}}}$ to represent a racn $V$ with the set
$\underline{{T}}$ of backward transitions.

In accordance with Condition 1, the underlying net ${V_{\overline{{T}}}}$,
encompassing solely the forward transitions of $V$, is a pacn. The insistence
on it being a pacn rather than an acn stems from the fact that the conflict
relation is not always inherited along $\lessdot$, which serves as the
causation relationship. This deviation is due to the fact that reversing
transitions may allow potentially conflicting transitions to be executed.
Condition 2 stipulates that each backward transition ${\underline{t}}$
unequivocally reverses one and only one forward transition ${t}$.
Consequently, ${\underline{t}}$ consumes the tokens produced by ${t}$
(${{t}}^{\bullet}={\rm Phys.~{}Rev.~{}E}{{\underline{t}}}$) and generates the
tokens consumed by ${t}$ (${{\underline{t}}}^{\bullet}={\rm
Phys.~{}Rev.~{}E}{{t}}$). The requirement ${\rm
Phys.~{}Rev.~{}E}{{t}}\subseteq{}^{\circ}{{\underline{t}}}$ in Condition 2
signifies that the reversal of ${t}$ (i.e., ${\underline{t}}$) can only occur
if ${t}$ has been executed. In other words, a transition can only be reversed
if it has been fired. Condition 3 requires a finite set of causes for undoing
each transition; in essence, ${\rm Phys.~{}Rev.~{}E}{K_{{\underline{t}}}}$
encompasses all the forward transitions ${t}^{\prime}$ that enable the
execution of ${\underline{t}}$. Condition 4 asserts that if a backward
transition ${\underline{t}}^{\prime}$ causally depends on the forward
transition ${t}$ (i.e., ${\rm
Phys.~{}Rev.~{}E}{t}\cap{}^{\circ}{{\underline{t}}^{\prime}}{}\neq\emptyset$),
then ${\underline{t}}^{\prime}$ cannot be prevented by the same transition
${t}$ (${{t}}^{\bullet}\cap{}^{\circ}{{\underline{t}}^{\prime}}{}=\emptyset$),
as otherwise, it would be blocked. Condition 5 introduces the relation $\lll$,
which is analogous to the _sustained causation_ in raes. This relation
coincides with causality, except in cases in which a cause can be reversed
even after a causally-dependent transition has been fired. Note that conflicts
should be inherited along $\lll$ rather than along the $\lessdot$ relation.

The inhibitor arcs of an racn $V$ induce four distinct relations. Two of these
pertain to the forward flow, defined on $\overline{{T}}\times\overline{{T}}$,
and correspond to those found in pacns, namely $\lessdot$ and
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}$.
Additionally, two relations concern the backward flow. These are _reverse
causation_ ${\prec}\subseteq{\overline{{T}}\times\underline{{T}}}$,
characterized by $t\prec\underline{t^{\prime}}$ if and only if ${\rm
Phys.~{}Rev.~{}E}{t}\cap{}^{\circ}{\underline{t}^{\prime}}\neq\emptyset$, and
_prevention_ ${\lhd}\subseteq{\underline{{T}}\times\overline{{T}}}$, defined
by $\underline{t^{\prime}}\lhd t$ if and only if
${t}^{\bullet}\cap{}^{\circ}{\underline{t}^{\prime}}\neq\emptyset$.

$s_{1}$$s_{2}$$s_{3}$${s_{4}}$${s_{5}}$${s_{6}}$$a$$b$$\underline{b}$$c$

(a) $V_{1}$

$s_{1}$$s_{2}$$s_{3}$${s_{4}}$${s_{5}}$${s_{6}}$$a$$b$$c$

(b) $V_{1_{\\{a,b,c\\}}}$

$s_{1}$$s_{2}$$s_{3}$${s_{4}}$${s_{5}}$${s_{6}}$$a$$b$$\underline{b}$$c$$\underline{c}$

(c) $V_{2}$

Figure 7.

Verifying that the ipt $V_{1}$ in Figure 7(a) is an racn is straightforward.
Note that $c$ causally depends on $a$ and $b$ due to the inhibitor arcs
connecting $c$ with the presets of $a$ and $b$. Moreover, $a$ and $b$ are in
asymmetric conflict: the inhibitor arc linking $s_{4}$ and $b$ indicates that
$b$ is prevented by $a$. The sole reversible transition is $b$, and its
associated undoing $\underline{b}$ causally depends on both $a$ and $b$ and is
prevented by $c$. In other words, the reversal of $b$ can only occur after the
firing of $a$ and $b$, but only if $c$ has not taken place.

The net $V_{1_{a,b,c}}$ in Figure 7(b) is obtained by eliminating the
transition $\underline{b}$ along with the connected inhibitor arcs from
$V_{1}$. It is immediate that $V_{1_{a,b,c}}$ is a acn.

The net $V_{2}$ in Figure 7(c) by extending $V_{1}$ with the reversal of $c$,
i.e., $\underline{c}$. If $\underline{b}$ and $\underline{c}$ along with their
associated inhibitor arcs are removed from $V_{2}$, we obtain the acn depicted
in Fig. 7(b).

Consider the net $V$ in Fig. 6. Note that the removal of the reversing
transition $\underline{b}$ does not yield a acn, as the conflict between $a$
and $b$ is not inherited along $b\lessdot c$. It is noteworthy that the
following represents a valid execution of $V$: initiating with $b$, followed
by $c$, and then reversing $b$ (performing $\underline{b}$), enabling the
subsequent execution of $a$. The ability to execute $a$ after the firing and
reversal of $b$ would be forbidden if the conflict between $a$ and $b$ were
inherited along $b\lessdot c$.

###  3.6. Configurations of racnes

We now introduce the concept of configuration for racns. In contrast to the
configuration for standard nets, which is typically defined in terms of
causality, a configuration of racn is simply required reachable via a firing
sequence.

Let ${V^{\underline{{T}}}}=\langle S,T,F,I,\mathsf{m}\rangle$ be a racn. A
_configuration_ of ${V^{\underline{{T}}}}$ is any subset
$X\subseteq\overline{{T}}$ of forward transitions such that there exists a
firing sequence $\mathsf{m}\,[\/{A_{1}}\/\rangle\,\dots m^{\prime}$ with
$X={\rm Phys.~{}Rev.~{}E}{m^{\prime}}\cap\overline{{T}}$.

Consider the net $V_{2}$ in Fig. 7(c); one of its configuration is
$\\{a,c\\}$, obtained by executing $b$ first, followed by $a$, then $c$ and
subsequently undoing $b$ (executing $\underline{b}$). This configuration is
only reachable by undoing $b$ since, given that $b$ is a cause of $c$, the
presence of $b$ is necessary to execute $c$.

###  3.7. Morphisms for Reversible Asymmetric Causal Nets

The notion of morphisms for racns is given below.

Let ${V^{\underline{{T_{0}}}}}=\langle
S_{0},T_{0},F_{0},I_{0},\mathsf{m}_{0}\rangle$ and
${V^{\underline{{T_{1}}}}}=\langle
S_{1},T_{1},F_{1},I_{1},\mathsf{m}_{1}\rangle$ be two racns. A 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}\rightarrow T_{1}$ satisfying the
following conditions

  1. (1)

$f_{T}(\overline{{T_{0}}})\subseteq\overline{{T_{1}}}$ and
$f_{T}(\underline{{T_{0}}})\subseteq\underline{{T_{1}}}$;

  2. (2)

$(f_{S},f_{T}|_{\overline{{T_{0}}}}):{V_{\overline{{T_{0}}}}}\rightarrow{V_{\overline{{T_{1}}}}}$
is an acn-morphism,

  3. (3)

$\forall{\underline{t}}\in\underline{{T_{0}}}.$ if $f_{T}(t)\neq\bot$ then

    1. (a)

$f_{T}({\underline{t}})\neq\bot$ and
$f_{T}({\underline{t}})=\underline{f_{T}({t})}$; and

    2. (b)

$\forall(s,f_{T}({\underline{t}}))\in I_{1}$.

      1. (i)

if ${s}^{\bullet}\cap\overline{{T_{1}}}\neq\emptyset$,
$f_{S}^{-1}(s)\neq\emptyset$ implies $\exists$ $s^{\prime}\in f_{S}^{-1}(s)$.
$(s^{\prime},{\underline{t}})\in I_{0}$; and

      2. (ii)

if ${s}^{\bullet}\cap\overline{{T_{1}}}=\emptyset$, $\forall$ $s^{\prime}\in
f_{S}^{-1}(s)$. $(s^{\prime},{\underline{t}})\in I_{0}$.

The first condition stipulates that forward and backward transitions are
respectively mapped to forward and backward transitions. According to
Condition 2, when considering forward transitions only (i.e., the restriction
of $f_{T}$ to ${\overline{{T_{0}}}}$) we have an acn-morphism on the
underlying ${V_{\overline{{T_{0}}}}}$ and ${V_{\overline{{T_{1}}}}}$ (i.e.,
the nets consisting only of forward transitions). Condition 3a ensures that
the transition ${\underline{t}}$, responsible for reversing $t$, must be
mapped to the transition $\underline{f_{T}({t})}$, which, in turn, reverses
$f_{T}({t})$. Finally, Condition 3(b)i prevents the merging of inhibitor arcs,
meaning that the distinction between various causes that might prevent the
reversal of a transition is preserved, whereas Condition 3(b)ii assures that
is a prevention is present in the target then all the reverse images of this
prevention must be present in the origin. We have to restrict our attention to
${s}^{\bullet}\cap\overline{{T_{1}}}$ as we have to consider the relations
induced by the inhibitor arcs in this case that are either reverse causation
or reverse prevention, and these are defined among forward transitions and
backward ones.

$s_{1}^{0}$$s_{2}^{0}$$s_{3}^{0}$$s_{7}^{0}$$s_{4}^{0}$$s_{5}^{0}$$s_{6}^{0}$$s_{8}^{0}$$a$$\underline{a}$$b$$c$$d$

(a) $V_{0}$

$s_{1}^{1}$$s_{2}^{1}$$s_{3}^{1}$$s_{4}^{1}$$s_{5}^{1}$$s_{6}^{1}$$a^{\prime}$$\underline{a^{\prime}}$$b^{\prime}$$c^{\prime}$

(b) $V_{1}$

Figure 8. Two racn

An racn-morphism $(f_{S},f_{T}):V_{0}\rightarrow V_{1}$ for the racns $V_{0}$
and $V_{1}$ in Fig. 8 is as follows. Consider the multirelation $f_{S}$ on
places, as detailed in Section 3.4, and define the mapping on transitions
$f_{T}$ such that it mirrors the one in Section 3.4 for forward transitions.
On the reversing transition $\underline{a}$, set
$f_{T}(\underline{a})=\underline{a}^{\prime}$. It is evident that
$\underline{f_{T}(a)}=f_{T}(\underline{a})$. The other conditions are
straightforwardly satisfied.

The following two results state that racn-morphisms preserve behaviours and
that they are closed under composition.

We first need to specialize the notion of coherent marking for racn. The idea
is that we have to focus on forward transitions only. Therefore given a
marking $m$ of the racn $V={V^{\underline{{T}}}}$, $m$ is coherent if it is
coherent in $V|_{\overline{{T}}}$ (recall that the places in $V$ and
$V|_{\overline{{T}}}$ are the same). Similarly let
$(f_{S},f_{T}):{V^{\underline{{T_{0}}}}}\rightarrow{V^{\underline{{T_{1}}}}}$
be an racn-morphism, and let $m$ be a coherent marking of
${V^{\underline{{T_{0}}}}}$. The relevant information of $m$ are the relevant
information of the marking $m$ in $V|_{\overline{{T_{0}}}}$.

######  Proposition 12.

Let
$(f_{S},f_{T}):{V^{\underline{{T_{0}}}}}\rightarrow{V^{\underline{{T_{1}}}}}$
be a racn-morphism. Let $m$ be a coherent marking of
${V^{\underline{{T_{0}}}}}$. Then, $m\,[\/{A}\/\rangle\,m^{\prime}$ implies
$m^{\prime}$ coherent and
$[\\![{f_{S}(\underline{m})}]\\!]\,[\/{f_{T}(A)}\/\rangle\,[\\![{f_{S}(\underline{m^{\prime}})}]\\!]$.

######  Proof 3.8.

We notice that conditions 3a and 3b of Section 3.7 are essentially the same of
a acn-morphism, thus without distinguish among reverse transitions and forward
ones, we have that a racn-morphism is a acn-morphism. Consequently, the tokens
game is preserved.

######  Lemma 13.

Let $(f_{S},f_{T}):V_{0}\rightarrow V_{1}$ and $(g_{S},g_{T}):V_{1}\rightarrow
V_{2}$ be two racn-morphisms. Then $(f_{S};g_{S},f_{T};g_{T}):V_{0}\rightarrow
V_{2}$ is a racn-morphism as well.

######  Proof 3.9.

The proof follows the same lines as the one in Proposition 8.

Therefore, racns and racn-morphisms constitute a category, which is denoted by
$\mathbf{RACN}$.

####  3.7.1. Configurations and morphisms:

We show that morphisms preserve configurations.

######  Proposition 14.

Let
$(f_{S},f_{T}):{V^{\underline{{T_{0}}}}}\rightarrow{V^{\underline{{T_{1}}}}}$
be a racn-morphism and $X$ a configuration, i.e.,
$X\in\mathsf{Conf}_{{{r\text{\sc acn}}}}({V^{\underline{{T_{0}}}}})$. Then,
$f_{T}(X)\in\mathsf{Conf}_{{{r\text{\sc acn}}}}({V^{\underline{{T_{1}}}}})$.

######  Proof 3.10.

It is sufficient to observe that configurations in racn are characterized by
reachable markings, and racn-morphisms preserve them.

###  3.8. Constructions

Similarly to what we have done for raes, we have a coproduct also in the
category of racn.

######  Proposition 15.

Let ${V^{\underline{{T_{0}}}}_{0}}=(S_{0},T_{0},F_{0},I_{0},\mathsf{m}_{0})$
and ${V^{\underline{{T_{1}}}}_{1}}=(S_{1},T_{1},F_{1},I_{1},\mathsf{m}_{1})$
be two racns. Then
${V^{\underline{{T_{0}}}}_{0}}+{V^{\underline{{T_{1}}}}_{1}}=(S,T,F,I,\mathsf{m})$
where

  * •

$S=\\{0\\}\times S_{0}\cup\\{1\\}\times S_{1}$;

  * •

$T=\\{0\\}\times T_{0}\cup\\{1\\}\times T_{1}$;

  * •

$\forall(i,a)\in S\cup T,\ \forall(j,b)\in S\cup T.\ ((i,a),(j,b))\in F$
whenever $i=j$ and $(a,b)\in F_{i}$;

  * •

$\forall(i,s)\in S,\ \forall(j,t)\in T.\ ((i,s),(j,t))\in I$ whenever either
$i=j$ and $(s,t)\in I_{i}$ or $i\neq j$; and

  * •

$\forall(i,s)\in S.\ \mathsf{m}(i,s)=\mathsf{m}_{i}(s)$

is their _coproduct_ and
$(\mathit{in}^{i}_{S},\mathit{in}^{i}_{T}):{V^{\underline{{T_{i}}}}_{i}}\to{V^{\underline{{T_{0}}}}_{0}}+{V^{\underline{{T_{1}}}}_{1}}$
defined as $(s,(i,s))\in\mathit{in}^{i}_{S}$ and
$\mathit{in}^{i}_{T}(t)=(i,t)$ are the injections.

######  Proof 3.11.

${V^{\underline{{T_{0}}}}_{0}}+{V^{\underline{{T_{1}}}}_{1}}$ is clearly an
racn. It remains to prove that is indeed a coproduct in the category
$\mathbf{RACN}$. Consider an racn ${V^{\underline{{T_{2}}}}_{2}}$ and two
morphisms
$(f_{S},f_{T}):{V^{\underline{{T_{0}}}}_{0}}\to{V^{\underline{{T_{2}}}}_{2}}$
and
$(g_{S},g_{T}):{V^{\underline{{T_{1}}}}_{1}}\to{V^{\underline{{T_{2}}}}_{2}}$,
we show that there exists a unique morphisms
$(h_{S},h_{T}):{V^{\underline{{T_{0}}}}_{0}}+{V^{\underline{{T_{1}}}}_{1}}\to{V^{\underline{{T_{2}}}}_{2}}$.
Define $h_{S}$ as the relation comprising the pairs $((i,s),s^{\prime})$ if
either $(s,s^{\prime})\in f_{S}$ or $(s,s^{\prime})\in g_{S}$ and the mapping
on transitions $h_{T}(i,t)$ equal to $f_{T}(t)$ if $i=0$ and to $g_{T}(t)$ if
$i=1$. We check first that this is indeed an racn-morphism. Consider $(i,t)\in
T$ such that $h_{T}(i,t)$ is defined. Then we have that ${\rm
Phys.~{}Rev.~{}E}{h_{T}(i,t)}={\rm Phys.~{}Rev.~{}E}{f_{T}(t)}$ if $i=0$ and
${\rm Phys.~{}Rev.~{}E}{h_{T}(i,t)}={\rm Phys.~{}Rev.~{}E}{g_{T}(t)}$ if $i=1$
and as $(f_{S},f_{T})$ and $(g_{S},g_{T})$ are morphisms we have that either
${\rm Phys.~{}Rev.~{}E}{h_{T}(i,t)}=\mu f_{S}({\rm Phys.~{}Rev.~{}E}{t})$ or
${\rm Phys.~{}Rev.~{}E}{h_{T}(i,t)}=\mu g_{S}({\rm Phys.~{}Rev.~{}E}{t})$ and
similarly for ${h_{T}(i,t)}^{\bullet}=\mu f_{S}({t}^{\bullet})$ or
${h_{T}(i,t)}^{\bullet}=\mu g_{S}({t}^{\bullet})$. Consider now
$((i,s),h_{T}(j,t))\in I_{2}$ and $s^{\prime}\in f_{S}^{-1}(i,s)\cup
g_{S}^{-1}(i,s)$. If $s^{\prime}\in f_{S}^{-1}(i,s)$ and $j=0=i$ then
$((i,s^{\prime}),(i,t))\in I$ and if $i\neq j$ then $((i,s^{\prime}),(j,t))\in
I$ by construction. The case $s^{\prime}\in g_{S}^{-1}(i,s)$ is the same.
Assume now $h_{T}(i,t)$ and $h_{T}(j,t^{\prime})$ are both defined and equal.
If $i=j$ then $(i,t)\ {\natural}\ (i,t^{\prime})$ and if $i\neq j$ we have
$(i,t)\ {\natural}\ (j,t^{\prime})$ as well as each transition of the first
one is prevented by the happening of a transition of the second one and vice
versa. Condition 3 of Section 3.4 is proven similarly to the previous one, and
the same argument is used to show that fact that
$[\\![{h_{S}}]\\!](\mathsf{m})=\mathsf{m}_{2}$. Observing that forward
transitions are mapped to forward ones and backward transitions are mapped to
backward ones, and if $(i,\underline{t})\in\underline{{T}}$ and $h_{T}(i,t)$
is defined we have that $h_{T}(i,\underline{t})$ is defined and
$h_{T}(i,\underline{t})=\underline{h_{T}(i,t)}$ as $(f_{S},f_{T})$ and
$(g_{S},g_{T})$ are morphisms. The racn-morphism $(h_{S},h_{T})$ is unique as
$h_{T}$ is unique and there is just one $h_{S}$ satisfying the requirements.

Also the category $\mathbf{RACN}$ does not have products.

##  4\. Relating models

In this section, we explore the interplay between the categories of
(reversible) asymmetric causal nets and (reversible) asymmetric event
structures. We establish functors and demonstrate the emergence of an
adjunction.

We delve into the connection between raeses and racnes. The following
definition outlines the process of recovering an raes from the flow and
inhibitor arcs of an racn.

As expected, the relations induced by an raes —–namely $\lessdot$ (causality),
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}$
(weak causality), $\prec$ (reverse causality), $\lhd$ (prevention), and $\lll$
(sustained causation)—play a crucial role in defining the relations of the
corresponding raes.

Let ${V^{\underline{{T}}}}=\langle S,T,F,I,\mathsf{m}\rangle$ be an racn, and
let $\lessdot$,
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}$,
$\prec$, $\lhd$ and $\lll$ denote the causation, weak causality, reverse
causality, prevention and sustained causation induced by $F$ and $I$. Then,
the corresponding structure $\mathcal{E}_{r}({V^{\underline{{T}}}})$ is the
tuple
$(\overline{{T}},U,\lessdot,{\lll}\cup{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}}$,
$\prec,\lhd)$, where $U=\\{t\in\overline{{T}}\ |\
{\underline{t}}\in\underline{{T}}\\}$ represents the reversible events.

The following result ensures that the above construction generates an raes.

######  Theorem 16.

Let ${V^{\underline{{T}}}}$ be an racn. Then
$\mathcal{E}_{r}({V^{\underline{{T}}}})$ is an raes.

######  Proof 4.1.

We show that the conditions in Section 2.2 are satisfied:

  1. (1)

Weak causality is set to
${\lll}\cup{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}}$.
By definition, both ${\lll}$ and
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}$
are relations over $\overline{{T}}\times\overline{{T}}$. Hence,
$({\lll}\cup{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}})\subseteq\overline{{T}}\times\overline{{T}}$.

  2. (2)

Prevention corresponds to $\lhd$, which, by definition satisfies
$\lhd\subseteq\underline{{T}}\times\overline{{T}}$.

  3. (3)

Firstly, causation is set to $\lessdot$, which, by definition, satisfies
$\lessdot\subseteq\overline{{T}}\times\overline{{T}}$. Moreover, since
${V^{\underline{{T}}}}$ is an racn, ${V_{\overline{{T}}}}$ is an acn by
Section 3.5(1). Hence, $\lessdot$ is irreflexive because of Section 3.2(4). By
Section 3.2(4), $\forall t\in\overline{{T}}.\ \lfloor
t\rfloor_{\lessdot}=\\{{t^{\prime}\in\overline{{T}}}\mid{t^{\prime}\lessdot^{\ast}t}\\}$
is finite and
$({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\cup\lessdot)$
is acyclic on $\lfloor t\rfloor_{\lessdot}$. By Section 3.5(5),
${\lll}\subset{\lessdot}$, hence
$({\lll}\cup{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}}\cup{\lessdot})=({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}}\cup{\lessdot})$.
Therefore,
$({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}}\cup{\lessdot})$
acyclic on $\lfloor t\rfloor_{\lessdot}$ implies
$({\lll}\cup{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}}\cup{\lessdot})$
acyclic on $\lfloor t\rfloor_{\lessdot}$.

  4. (4)

Reverse causation is set to $\prec$, which is by definition $\prec\
\subseteq\overline{{T}}\times\underline{{T}}$.

    1. (a)

By Section 3.5(2), $\forall{\underline{t}}\in\underline{{T}}$, ${\rm
Phys.~{}Rev.~{}E}{{t}}\subseteq{}^{\circ}{{\underline{t}}}$. Hence,
$t\prec\underline{t}$.

    2. (b)

By Section 3.5(3), for all ${\underline{t}}\in\underline{{T}}$,
$K_{{\underline{t}}}=\\{{{t}^{\prime}\in\overline{{T}}}\mid{{}^{\circ}{{\underline{t}}}\cap{\rm
Phys.~{}Rev.~{}E}{{t}^{\prime}{}}\neq\emptyset}\\}$ is finite and
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}$
acyclic on $K_{{\underline{t}}}$. Note that
$K_{{\underline{t}}}=\\{{{t}^{\prime}\in\overline{{T}}}\mid{t\prec{\underline{t^{\prime}}}}\\}=\lfloor\underline{t}\rfloor_{\prec}$.
Hence, $\lfloor\underline{t}\rfloor_{\prec}$ is finite. It remains to show
that
${\lll}\cup{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}}\cup\lessdot$
is acyclic on $K_{{\underline{t}}}$. As in the previous item,
$({\lll}\cup{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}}\cup\lessdot)=({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}}\cup\lessdot)$.
Hence, we need to show that
$({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}}\cup\lessdot)$
is acyclic on $K_{{\underline{t}}}$. We know that
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}$
is acyclic on $K_{{\underline{t}}}$, and $\lessdot^{+}$ is a partial order
since $\mathcal{E}_{r}({V^{\underline{{T}}}})$ is a racn. Hence, acyclicity on
$K_{{\underline{t}}}$ can only be violated if, for any two
$t^{\prime},t^{\prime\prime}\in\lfloor\underline{t}\rfloor_{\prec}$, we have
$t^{\prime}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}t^{\prime\prime}$
and $t^{\prime\prime}\lessdot t^{\prime}$. However, this implies that
${t^{\prime\prime}}^{\bullet}\cap{}^{\circ}{t^{\prime}}\neq\emptyset$ and
${\rm
Phys.~{}Rev.~{}E}{t^{\prime\prime}}\cap{}^{\circ}{t^{\prime}}\neq\emptyset$,
which contradicts the fact that $\mathcal{E}_{r}({V^{\underline{{T}}}})$ is an
racn.

  5. (5)

for all $t\in\overline{{T}},\underline{t^{\prime}}\in\underline{{T}}$.
$t\prec\underline{t^{\prime}}\ \Rightarrow\neg(\underline{t^{\prime}}\lhd t$).
Note that $t\prec\underline{t^{\prime}}$ implies that ${\rm
Phys.~{}Rev.~{}E}{t}\cap{}^{\circ}{\underline{t^{\prime}}}\neq\emptyset$.
Consequently, ${t}^{\bullet}\cap{}^{\circ}{\underline{t^{\prime}}}=\emptyset$,
indicating that $\neg(\underline{t^{\prime}}\lhd t)$.

  6. (6)

We need to show that
$(\overline{{T}},\prec\\!\\!\prec,{\lll}\cup{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}})$
with ${\prec\\!\\!\prec}={\lessdot}\cap{\\{(t,t^{\prime})\ |\ t\not\in
U\textit{ or }\underline{t}\lhd t^{\prime}\\}}$ is an aes. We now check the
conditions of Section 2.1. First note that $\prec\\!\\!\prec\ =\lll$ by the
definition of $\lll$.

    1. (a)

We need to show that $\prec\\!\\!\prec\
\subseteq\overline{{T}}\times\overline{{T}}$ is an irreflexive partial order
defined such that $\forall t\in\overline{{T}}$. $\lfloor
t\rfloor_{\prec\\!\\!\prec}$ is finite. The fact that $\prec\\!\\!\prec$
irreflexive and antisymmetric because $\lll\subseteq\lessdot+$ and
$\lessdot^{+}$ is an irreflexive partial order. Transitivity follows from the
definition of $\lll$ (Section 3.5(5)).

$\lfloor t\rfloor_{\prec\\!\\!\prec}$ is finite because
$\prec\\!\\!\prec=\lll\subseteq\lessdot$ and $\lfloor t\rfloor_{\lessdot}$ is
finite (Section 3.2(4)).

    2. (b)

$({\lll}\cup{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}})\subseteq\overline{{T}}\times\overline{{T}}$
by definition. We need to show that for all $t,t^{\prime}\in\overline{{T}}$:

      1. (i)

$t\lll t^{\prime}\ \Rightarrow\ t\
({\lll}\cup{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}})\
t^{\prime}$; which immediately follows because
${\lll}\subseteq{(\lll\cup{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto})}$.

      2. (ii)

$({\lll}\cup{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}})\cap(\lfloor
t\rfloor_{\prec\\!\\!\prec}\times\lfloor t\rfloor_{\prec\\!\\!\prec})$ is
acyclic. Note that
$({\lll}\cup{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}})\cap(\lfloor
t\rfloor_{\prec\\!\\!\prec}\times\lfloor
t\rfloor_{\prec\\!\\!\prec})=({\lll}\cup{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}})\cap(\lfloor
t\rfloor_{\lll}\times\lfloor t\rfloor_{\lll})=(\lfloor
t\rfloor_{\lll}\times\lfloor t\rfloor_{\lll})\subseteq(\lfloor
t\rfloor_{\lessdot}\times\lfloor t\rfloor_{\lessdot})$, which is acyclic
because ${V_{\overline{{T}}}}$ is an acn (Section 3.2(4)).

      3. (iii)

if $t\\#t^{\prime}$ and $t^{\prime}\prec\\!\\!\prec t^{\prime\prime}$ then
$t\\#t^{\prime\prime}$. It follows from Section 3.5(5).

We can conclude that $\mathcal{E}_{r}(V)$ is indeed an raes.

Consider the racn $V_{1}$ Figure 7. The corresponding raes
$\mathcal{E}_{r}(V_{1})$ is defined as $\mathsf{H}_{1}$ in Section 2.2. In
fact, within $V_{1}$, causality is characterized by $b\lessdot c$ and
$a\lessdot c$ due to the conditions ${\rm
Phys.~{}Rev.~{}E}{a}\cap{}^{\circ}{c}\neq\emptyset$ and ${\rm
Phys.~{}Rev.~{}E}{b}\cap{}^{\circ}{c}\neq\emptyset$. Moreover, weak causality
includes $b\nearrow a$ as a consequence of $b\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\
a$, and also encompasses $a\nearrow c$ and $b\nearrow c$ induced by the
sustained causation, which coincides with $\lessdot$. On the other hand,
reverse causality encompasses $b\prec\underline{b}$ and $a\prec\underline{b}$,
while prevention is limited to $\underline{b}\lhd c$.

Recall that an racn lacking reversing transitions (i.e., ${V^{\emptyset}}$) is
essentially an acn. Consequently, the construction outlined in Section 4 is
applicable to acnes as well.

######  Corollary 17.

Let $C=\langle S,T,F,I,\mathsf{m}\rangle$ be 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}\rightarrow V_{1}$ induces an raes-morphism
$\mathcal{E}_{r}(f_{S},f_{T})=f_{T}$.

######  Proposition 18.

$\mathcal{E}_{r}:\mathbf{RACN}\rightarrow\mathbf{RAES}$ is a well-defined
functor.

The construction linking a net to an event structure adheres to the
conventional intuition, where places represent appropriate subsets of events,
and transitions are connected to places based on the relations specified in
the event structure. In our context, the event subsets have a cardinality of
at most one, meaning they are either the empty set or a singleton. To
streamline notation, we will use the symbol $e$ to represent the singleton set
$\\{e\\}$ and, consequently, avoid the use of braces.

Let $\mathsf{H}=(E,U,<,\nearrow,\prec,\lhd)$ be an raes. Then, the associated
net $\mathcal{N}_{r}(\mathsf{H})$ is defined as $\langle
S,E\cup\\{{\underline{u}}\mid{u\in U}\\},F,I,\mathsf{m}\rangle$ where

$\begin{array}[]{r@{\ }c@{\ }l@{\ }c@{\ }l@{\ }c@{\ }l}S&=&\\{{\
(\emptyset,e)\ }\mid{\ e\in E}\\}&\cup&\\{{\ (e,e)\ }\mid{\ e\in
E}\\}&\cup&\\{\ (\emptyset,\emptyset)\ \\}\\\\[6.0pt] F&=&\\{{\
((\emptyset,{e}),e)\hskip 6.544pt}\mid{\ e\in E}\\}&\cup&\\{{\ (e,({e},{e}))\
}\mid{\ e\in E}\\}&\cup\\\ &&\\{{\ (({u},{u}),\underline{u})\ }\mid{\,u\in
U}\\}&\cup&\\{{\ (\underline{u},(\emptyset,{u}))}\mid{\ u\in U}\\}\\\\[6.0pt]
I&=&\\{{\ ((\emptyset,{e^{\prime}}),e)\ }\mid{\ e^{\prime}<e}\\}&\cup&\\{{\
(({e^{\prime}},{e^{\prime}}),e)\ }\mid{\ e\nearrow e^{\prime}}\\}&\cup\\\
&&\\{{\ ((\emptyset,{e}),\underline{u})\hskip 5.12128pt}\mid{\
e\prec\underline{u}\,}\\}&\cup&\\{{\ (({e},{e}),\underline{u})}\mid{\
\underline{u}\lhd e}\\}\\\\[6.0pt] \mathsf{m}&=&\\{{\ (\emptyset,{e})\ }\mid{\
e\in E}\\}&\cup&\\{\ (\emptyset,\emptyset)\ \\}\end{array}$

Events in $E$ are mapped to the forward transitions of the net. For each event
$e$, two associated places are considered: $(\emptyset,e)$ signifies that the
event $e$ has not occurred, while $(e,e)$ indicates its execution. As a
result, the preset of the forward transition $e$ is ${(\emptyset,e)}$, and its
postset is ${(e,e)}$. A transition $\underline{u}$ corresponds to the undoing
of the forward transition $u$. This transition consumes tokens from $(u,u)$
and produces them in $(\emptyset,u)$. The inclusion of the special place
$(\emptyset,\emptyset)$ serves no operational purpose; its motivation is
purely technical. Its significance will become clearer when demonstrating that
the mapping extends to a functor, as explained in the subsequent discussion.
The inhibitor arcs in $I$ model both causality (forward or backward) and
precedence (forward or backward). Additionally, all places not appearing in
the postset of forward transitions are initially marked.

######  Theorem 19.

If $\mathsf{H}=(E,U,<,\nearrow,\prec,\lhd)$ is a raes, then
$\mathcal{N}_{r}(\mathsf{H})$ is an racn.

######  Proof 4.2.

Consider the raes $\mathsf{H}=(E,U,<,\nearrow,\prec,\lhd)$ and
$\mathcal{N}_{r}(\mathsf{H})=\langle S,E\cup\\{{\underline{u}}\mid{u\in
U}\\},F,I,\mathsf{m}\rangle$ as defined in Section 4. Initially, we show that
the net $\langle S,E,F^{\prime},I^{\prime},\mathsf{m}\rangle$, where
$F^{\prime}$ and $I^{\prime}$ are the restrictions of $F$ and $I$ to the
transitions in $E$, is a pacn. The first three conditions of Section 3.2
follow through a straightforward examination of the definition of
$\mathcal{N}_{r}(\mathsf{H})$. The fourth condition is a consequence of
$\mathsf{H}$ being an raes, satisfying Section 2.2(3), which translates to
Condition 4 in Section 3.2. The final condition is implied by the fact that
$(E,\prec\\!\\!\prec,\nearrow)$ constitutes an aes with
${\prec\\!\\!\prec}\subseteq{<}$.

For each transition in $\\{{\underline{u}}\mid{u\in U}\\}$, there is precisely
one corresponding transition in $E$, represented by $u$, as dictated by
$\mathsf{H}$ being an raes. Condition 3 in Section 3.5—–asserting that
$K_{\underline{u}}$ is finite—stems from $\lfloor\underline{u}\rfloor_{\prec}$
being finite in an raes. For the same reason, causation and weak causality are
acyclic on such sets. Hence, Condition 4 is also satisfied by construction.
The condition 5 of Section 3.5 is verified as it mimic the requirement of
sustained causality of the raes $\mathsf{H}$. The final condition depends
again on the analogous one in raes. We can conclude that indeed
$\mathcal{N}_{r}(\mathsf{H})$ is an racn.

Consider the raes $\mathsf{H^{\prime}}$ from Section 2.2. The places are
$(\emptyset,\emptyset)$, $(\emptyset,{a})$, $(\emptyset,{b})$,
$(\emptyset,{c})$, $({a},{a})$, $({b},{b})$ and $({c},{c})$. The corresponding
transitions are $a,b,c$ (forward ones) and $\underline{b},\underline{c}$
(reversing ones). The flow arcs adhere to the specifications outlined in
Section 4, while the inhibitor arcs are determined by the relations within
$\mathsf{H^{\prime}}$. The resulting net bears resemblance to the one depicted
in Figure 7(c), with distinct place labels and the exclusion of the isolated
place $(\emptyset,\emptyset)$.

######  Corollary 20.

If $\mathsf{G}=(E,<,\nearrow)$ is an aes, then
$\mathcal{N}_{r}(E,\emptyset,<,\nearrow,\emptyset,\emptyset)$ is an acn.

We establish the extension of the mapping $\mathcal{N}_{r}$ to a functor by
demonstrating that any raes-morphism
$f:\mathsf{H}_{0}\rightarrow\mathsf{H}_{1}$ induces a racn-morphism
$\mathcal{N}_{r}(f):\mathcal{N}_{r}(\mathsf{H}_{0})\rightarrow\mathcal{N}_{r}(\mathsf{H}_{1})$.

Let $f:\mathsf{H}_{0}\rightarrow\mathsf{H}_{1}$ be raes-morphism. Assume
$\mathcal{N}_{r}(\mathsf{H}_{i})=\langle
S_{i},E_{i}\cup\\{{\underline{u}}\mid{u\in
U_{i}}\\},F_{i},I_{i},\mathsf{m}_{i}\rangle$ for $i=0,1$. We define
$\mathcal{N}_{r}(f)=(f_{S},f_{T})$ as follows:

  1. (1)

$f_{S}\subseteq S_{0}\times S_{1}$ where

$(s_{0},s_{1})\in f_{S}\iff\begin{cases}s_{0}=s_{1}=(\emptyset,\emptyset);\
or\\\ s_{0}=(\emptyset,\emptyset)\ \land\ s_{1}=(\emptyset,e)\ \land\
f^{-1}(e)=\bot;\ or\\\ s_{0}=(\emptyset,e)\ \land\ f(e)\neq\bot\ \land\
s_{1}=(\emptyset,f(e));\ or\\\ s_{0}=(e,e)\ \land\ f(e)\neq\bot\ \land\
s_{1}=(f(e),f(e)).\end{cases}$

  2. (2)

$f_{T}:E_{0}\cup\\{{\underline{u}}\mid{u\in U_{0}}\\}\rightarrow
E_{1}\cup\\{{\underline{u}}\mid{u\in U_{1}}\\}$ is defined as follows:

$f_{T}(t)=\begin{cases}f(t)&\text{if }t\in E_{0},\ \land\ f(e)\neq\bot\\\
\underline{f(u)}&\text{if }t=\underline{u}\text{ and
}f(u)\neq\bot.\end{cases}$

According to Condition (1), the relation $f_{S}$ is established to associate
the place $(\emptyset,\emptyset)$ in the source with its counterpart
$(\emptyset,\emptyset)$ in the target. Additionally, it is linked to all the
places $(\emptyset,e)$ in the target, where $e$ is not in the image of the
morphism $f$. This connection is crucial to guarantee that the definition
satisfies the condition regarding the initial markings of acn-morphisms
(Section 3.4(4)). Each place in the source, denoted as $(\emptyset,e)$, which
corresponds to the preset of the event $e$, is paired with the place in the
target representing the preset of the corresponding event $f(e)$; denoted as
$(\emptyset,f(e))$. Similarly, each place in the source, denoted as $(e,e)$,
indicating the postset of the event $e$, is associated with its counterpart in
the target representing the postset of the corresponding event $f(e)$;
designated as $(f(e),f(e))$. The mapping for transitions is straightforward. A
transition representing a forward event $e$ is mapped to a transition
representing the corresponding event $f(e)$. Reversing transitions are
similarly mapped to reversing transitions.

The following result ensures that the construction above actually gives an
racn-morphism.

######  Proposition 21.

If $f:\mathsf{H}_{0}\rightarrow\mathsf{H}_{1}$ is an raes-morphism, then
$\mathcal{N}_{r}(f):\mathcal{N}_{r}(\mathsf{H}_{0})\rightarrow\mathcal{N}_{r}(\mathsf{H}_{1})$
is a well-defined racn-morphism.

######  Proof 4.3.

We verify that $\mathcal{N}_{r}(f)$ constitutes an racn-morphism from
$\mathcal{N}_{r}(\mathsf{H}_{0})$ to $\mathcal{N}_{r}(\mathsf{H}_{1})$ by
checking the conditions of Section 3.7. Assume
$\mathcal{N}_{r}(\mathsf{H}_{i})=\langle
S_{i},T_{i},F_{i},I_{i},\mathsf{m}_{i}\rangle$ for $i=0,1$. By definition of
$\mathcal{N}_{r}(\mathsf{H}_{i})$, note that $\overline{{T_{i}}}=E_{i}$ and
$\underline{{T_{i}}}=\\{{\underline{u}}\mid{u\in U_{i}}\\}$.

  1. (1)

By definition of $\mathcal{N}_{r}(f)$,
$f_{T}(\overline{{T_{0}}})=f_{T}(E_{0})\subseteq
f_{T}(E_{1})=\overline{{T_{1}}}$. Similarly,
$f_{T}(\underline{{T_{0}}})=f_{T}(\\{{\underline{u}}\mid{u\in
U_{0}}\\})\subseteq f_{T}(\\{{\underline{u}}\mid{u\in
U_{1}}\\})=\underline{{T_{1}}}$.

  2. (2)

We need to show that
$(f_{S},f_{T}|_{E_{0}}):{V_{E_{0}}}\rightarrow{V_{E_{1}}}$ is an acn-morphism.
Hence, we check the conditions of Section 3.4.

    1. (a)

for all $e\in E_{0}$ if $f_{T}(e)\neq\bot$ then

      1. (i)

We show that ${\rm Phys.~{}Rev.~{}E}{f_{T}(e)}=f_{S}({\rm
Phys.~{}Rev.~{}E}{e})$ and ${f_{T}(e)}^{\bullet}=f_{S}({e}^{\bullet})$

$\displaystyle{\rm Phys.~{}Rev.~{}E}{f_{T}(e)}$ $\displaystyle={\rm
Phys.~{}Rev.~{}E}{f(e)}$ $\displaystyle\text{By def. of }f_{T}(e).$
$\displaystyle=\\{(\emptyset,f(e))\\}$ $\displaystyle\text{By def. of }F_{0}.$
$\displaystyle=f_{S}(\\{(\emptyset,e)\\})$ $\displaystyle\text{By def. of
}f_{S}.$ $\displaystyle=f_{S}({\rm Phys.~{}Rev.~{}E}{e})$
$\displaystyle\text{By def. of }F_{0}.$

Analogously,
${f_{T}(t)}^{\bullet}={f(e)}^{\bullet}=\\{(f(e),f(e))\\}=f_{S}(\\{(e,e)\\})=f_{S}({t}^{\bullet})$.

      2. (ii)

Assume now $(s,f_{T}(e))\in I_{1}$. We distinguish two cases, either
${s}^{\bullet}\neq\emptyset$ or ${s}^{\bullet}=\emptyset$.

In the first case, if $f_{S}^{-1}(s)=\emptyset$ we have nothing to prove, thus
assume that $f_{S}^{-1}(s)\neq\emptyset$ By Section 4, if $(s,f_{T}(e))\in
I_{1}$, then there are two cases:

         * •

$s=(\emptyset,e^{\prime})$ and $e^{\prime}<_{1}f_{T}(e)$: Since $f$ is an
raes-morphism, it is also an aes-morphism. Consequently, it preserves causes
(Section 2.1(1)). Therefore, it should hold that $\lfloor f(e)\rfloor\subseteq
f(\lfloor e\rfloor)$. Since $e^{\prime}\in\lfloor f(e)\rfloor$, there must be
$e_{0}\in\lfloor e\rfloor$ such that $f(e_{0})=e^{\prime}$. Then, it suffices
to consider $s^{\prime}=(\emptyset,e_{0})$. It is immediate that
$s^{\prime}\in f_{S}^{-1}(s)$ because $f(e_{0})=e^{\prime}$. Moreover,
$((\emptyset,e_{0}),e)\in I_{0}$ because $e_{0}<_{0}e$ (Section 4).

         * •

$s=(e^{\prime},e^{\prime})$ and $f_{T}(e)\nearrow e^{\prime}$. As
$f_{S}^{-1}(s)\neq\emptyset$, we can consider all $e_{0}\in E_{0}$ such that
$f(e_{0})=e^{\prime}$. Since $f$ is an raes-morphism, it reflects weak
causality (Section 2.1(2a)). Hence, for all $e_{0}$ such that
$f(e_{0})=e^{\prime}$, we have that $e\nearrow e_{0}$. Hence,
$((e_{0},e_{0}),e)\in I_{0}$ by Section 4.

    2. (b)