1–LABEL:LastPageFeb. 13, 2018Sep. 28, 2018

# Event Structures for Petri nets with Persistence

Paolo Baldana  aUniversity of Padova, Italy<EMAIL_ADDRESS>,  Roberto
Brunib  bUniversity of Pisa, Italy  ,  Andrea Corradinib  ,  Fabio Gadduccib
<EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS>,
Hernan Melgrattic  cUniversity of Buenos Aires - Conicet, Argentina
<EMAIL_ADDRESS>and  Ugo Montanarib

###### Abstract.

Event structures are a well-accepted model of concurrency. In a seminal paper
by Nielsen, Plotkin and Winskel, they are used to establish a bridge between
the theory of domains and the approach to concurrency proposed by Petri. A
basic role is played by an unfolding construction that maps (safe) Petri nets
into a subclass of event structures, called prime event structures, where each
event has a uniquely determined set of causes. Prime event structures, in
turn, can be identified with their domain of configurations. At a categorical
level, this is nicely formalised by Winskel as a chain of coreflections.

Contrary to prime event structures, general event structures allow for the
presence of disjunctive causes, i.e., events can be enabled by distinct
minimal sets of events. In this paper, we extend the connection between Petri
nets and event structures in order to include disjunctive causes. In
particular, we show that, at the level of nets, disjunctive causes are well
accounted for by persistent places. These are places where tokens, once
generated, can be used several times without being consumed and where multiple
tokens are interpreted collectively, i.e., their histories are inessential.
Generalising the work on ordinary nets, Petri nets with persistence are
related to a new subclass of general event structures, called _locally
connected_ , by means of a chain of coreflections relying on an unfolding
construction.

###### Key words and phrases:

event structures, disjunctive causes, local connectedness, Petri nets,
persistence, concurrency, unfolding, coreflection

## Prelude

Among the multitude of his research interests, Furio has been working on the
foundations of concurrency with special attention to the mathematical domains
required for defining the semantics of concurrent systems. We like to recall
his work on hyperuniverses as models for processes and on the final semantics
of the pi-calculus achieved by means of an higher order presentation via
Logical Framework. It was in the context of the European Project MASK
(“Mathematical Structures for Concurrency”), led by Jaco De Bakker, that most
of us had the first chance of working closely together with Furio. Surely that
was one of the most relevant results of the project, paving the way for a
fruitful scientific collaboration that continued in the following years in the
framework of several research projects. This paper is heartfully dedicated to
him in the occasion of his 60th birthday.

##  1\. Introduction

Petri nets have been introduced in the Ph.D. Thesis of Carl Adam Petri [27]
and soon have become one of the best known models of concurrency [29, 16, 14].
The conceptual simplicity of the model (multiset rewriting) and its intuitive
graphical presentation have attracted the interest of both theoreticians and
practitioners. Nowadays Petri nets are widely adopted across Computer Science
and other disciplines such as Physics, Chemistry, and Biology [1, 18, 17].
They provide a basic model that, on the one hand, offers the ideal playground
to study basic concepts of concurrent and distributed computations [26, 13,
31] and, on the other hand, can be readily extended to experiment with
advanced features like structured data handling, read and inhibitor arcs,
mobility, reflection, time and stochastic behavior [15, 7, 25, 2, 30, 21, 28,
11, 20, 24, 12].

In this paper we are interested in the seminal work of Winskel [33] on net
unfolding, which has established a tight connection between Petri nets and
(prime algebraic) domains. There it is shown that a chain of coreflections
links the category of safe nets to the category of prime event structures,
which in turn is equivalent to the category of prime algebraic domains. This
is particularly satisfactory since a coreflection essentially establishes that
a sub-category of abstract models can be found in a category of concrete
models, such that each concrete model can be assigned the best possible
abstract model. The first step of the chain is an unfolding construction that
maps each net to a special kind of acyclic net (called non-deterministic
occurrence net) representing all behaviours of the original net. From this an
event structure can be easily defined, by forgetting the places of the net.
Later these results have been extended to the more general class of semi-
weighted nets [22, 23].

Petri nets semantics is based on consuming and producing data (i.e., tokens)
from repositories (i.e., places). Operationally, reading a piece of
information can be modelled by a transition that consumes a token from a place
and produces it again on the same place. However, from the point of view of
concurrency and causality such an encoding is not faithful as it disallows
concurrent readings. Moreover, in many situations one is interested in
representing persistent information that once created can be read but not
consumed and such that its multiplicity (the number of available instances) is
not important. This is the case for instance of classical logical conditions
that once established to hold can be used repeatedly for proving other
conditions. Another example is that of subversioning systems or cloud storage,
where data changes are logged and previous versions of stored files remain
accessible after an update. Persistent information is also used in [8] to
model security protocols, where the pool of messages exchanged by participants
over the network forms a knowledge base that remains available for inspection
and processing by attackers: in other words, sent messages cannot be removed.
In [6] persistent tokens are used to remove confusion from acyclic nets and
equip choices with standard probabilistic distributions. The equivalent
framework of CPR nets [5] has been proposed for modelling web services:
persistency is needed to capture service availability, and the formalism has
been used for describing protocols that are specified with the ontology-based
OWL-S language.

Read arcs have been introduced in the literature to handle multiple concurrent
readings [7] and their concurrent semantics has been widely investigated [32,
4]. From the point of view of causality, they are not expressive enough to
model another interesting phenomenon of persistent information that is the
absence of multiplicity: if the same piece of persistent data is created
several times, then its causes are merged and the events that read the
persistent data can inherit any of them disjunctively. Instead, when read arcs
are used, their event structure semantics records the exact causes.

The goal of this paper is to extend Winskel’s construction to Petri nets with
persistence, as defined in [8, 9], and to understand what is the right sub-
category of general event structures to exploit. Surely, prime event
structures are not expressive enough, as they allow for a unique set of
minimal causes for each event. Instead, as discussed above, the presence of
persistent data leads to events with multiple sets of minimal causes.
Consider, e.g., the net with persistence in Figure 1, which will serve as a
running example. As usual, places and transitions are represented by circles
and boxes, respectively. Persistent places, like $o$ in this case, are
represented by double circles. Intuitively, transition $c$ is immediately
enabled and can be fired many times (sequentially). As soon as $a$ or $b$
fires, place $o$ becomes marked. The number of tokens in $o$ as well as their
causal histories are irrelevant: once $o$ is marked, it will remain so
forever. At this point $d$ and $e$ become (concurrently) enabled. The firing
of $d$ disables $c$ but not $e$ since the token never leaves the persistent
place $o$.

$\textstyle{\bullet}$$\textstyle{\scriptstyle{p}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{q}}$$\textstyle{a}$$\textstyle{b}$$\textstyle{c}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{r}}$
$\textstyle{\scriptstyle{o}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{s}}$$\textstyle{d}$$\textstyle{e}$
$\textstyle{\scriptstyle{t}}$ $\textstyle{\scriptstyle{u}}$ Figure 1. Running
example

In a recent work [3] dealing with the semantics of formalisms with fusion and
with the corresponding phenomenon of disjunctive causality, the domains of
configurations of general event structures are characterised by resorting to a
weak form of prime algebraicity. _Connected event structures_ are identified
as canonical representations of general (possibly non-stable) event
structures, in the same way as prime event structures are representations of
stable event structures. In particular, the equivalence between the category
of prime algebraic domains and the one of prime event structures is
generalised to an equivalence between the category of weak prime domains and
that of connected event structures. In a connected event structure, an event
may have multiple causal histories, but they are required to be “connected”,
namely they must not be separable in two classes of pairwise incompatible
causal histories. The idea is that, if in a general event structure an event
has conflicting classes of causal histories, then it should split in several
copies when generating the corresponding connected event structure. Indeed, as
discussed in [3], connected event structures can be alternatively presented as
prime event structures where some events (intuitively, those having different
but not incompatible causal histories) are deemed equivalent. This establishes
a close connection with the work in [10], where, in order to model strategies
with disjunctive causes, the authors deal with _prime event structures with
equivalence_.

In this paper we rely on the aforementioned work. A major role is played by a
weakening of the connectedness property for event structures, referred to as
_local connectedness_. The underlying intuition is as follows. A causal
history can be seen as a conjunction of its events, thus an event with
different causal histories is enabled by a disjunction of conjunctions of
events. Connectedness amounts to the fact that the various conjuncts cannot be
split in conflicting subclasses. Moving to Petri nets with persistence, a
persistent place can be seen as the disjunction of all events that can fill
the place. In turn, an event needs all places in its pre-set to be filled,
hence it is enabled by a conjunction of disjunctions. The property of local
connectedness roughly amounts to the requirements that the different ways of
enabling a persistent place cannot be separated into conflicting classes. If
this were possible, one should split the place in different copies, one for
each class. The notion of local connectedness lifts to event structures and we
show that Winskel’s chain of coreflections can be generalised to link the
category of Petri nets with persistence to that of locally connected event
structures. The latter, in turn, coreflects into the category of connected
event structures.

The result can be read from two perspectives. From one viewpoint, where the
construction defines the event structure associated with a net, it
characterises the “right” concurrent semantics for dealing with formalisms
that handle persistent information. The interesting bit is that the notion of
connectedness from [3] is relaxed here to local connectedness. From the second
viewpoint, the construction builds a standard net that is the best
representative for the (locally connected) event structure at hand. The latter
is a more interesting viewpoint, because: (i) it shows that Petri nets with
persistence are expressive enough to account for disjunctive causes, advancing
towards the solution of a long-standing open question about finding the right
computational model for general event structures; and (ii) it confirms that
Petri nets offer the ideal playground to experiment with concurrency features.

###  1.1. Structure of the paper

In Section 2 we review the preliminaries on connected event structures and we
introduce the original class of locally connected event structures. In Section
3 we introduce Petri nets with persistence (p-nets) and the corresponding
category. In Section 4 we introduce occurrence p-nets and define a
coreflection between the category of p-nets and the one of occurrence p-nets.
The right-adjoint of the coreflection is the unfolding construction that
accounts for the description of concurrent computations of a p-net.
Technically, it is defined in two steps, going through a category of
occurrence p-nets with equivalence. In Section 5 we establish a coreflection
between the category of p-nets and the one of locally connected event
structures. Some concluding remarks are in Section 6.

##  2\. Event structures and (local) connectedness

In this section we review the basics of event structures [33] and the notion
of connected event structure from [3]. Then we single out a wider class of
event structures, referred to as _locally connected_ , that will play a
pivotal role in the paper.

We start by recalling the notion of event structure with binary conflict [33].
In the following, for $m,n\in\mathbb{N}$, we denote by $[{m},{n}]$ the set
$\\{m,m+1,\ldots,n\\}$. Also, given a set $E$, we denote by $\mathbf{2}^{E}$
the powerset of $E$ and by $\mathbf{2}_{f}^{E}$ the set of finite subsets of
$E$.

[event structure] An _event structure_ (es for short) is a tuple $\langle
E,\vdash,\\#\rangle$ such that

  * •

$E$ is a set of events;

  * •

${\vdash}\subseteq\mathbf{2}_{f}^{E}\times E$ is the _enabling_ relation
satisfying $X\vdash e$ and $X\subseteq Y$ implies $Y\vdash e$;

  * •

$\\#\subseteq E\times E$ is the _conflict_ relation.

Two events $e,e^{\prime}\in E$ are _consistent_ , written
$e\stackrel{{\scriptstyle}}{{\frown}}e^{\prime}$, if $\neg(e\\#e^{\prime})$. A
subset $X\subseteq E$ is _consistent_ if
$e\stackrel{{\scriptstyle}}{{\frown}}e^{\prime}$ for all $e,e^{\prime}\in X$.

An es $\langle E,\vdash,\\#\rangle$ is often denoted simply by $E$.
Computations are captured in the form of configurations.

[configuration, live es, concurrent events] A _configuration_ of an es $E$ is
a consistent $C\subseteq E$ which is _secured_ , i.e., for all $e\in C$ there
are $e_{1},\ldots,e_{n}\in C$ with $e_{n}=e$ such that
$\\{e_{1},\ldots,e_{k-1}\\}\vdash e_{k}$ for all $k\in[{1},{n}]$ (in
particular, $\emptyset\vdash e_{1}$). The set of configurations of an es $E$
is denoted by $\mathit{Conf}({E})$. An es is _live_ if it has no self-
conflicts, i.e., for all $e\in E$ we have $\neg(e\\#e)$, and conflict is
saturated, i.e., for all $e,e^{\prime}\in E$, if $\neg(e\\#e^{\prime})$ then
there is $C\in\mathit{Conf}({E})$ such that $\\{e,e^{\prime}\\}\subseteq C$.
Two events $e,e^{\prime}\in E$ are _concurrent_ if they are consistent
($e\stackrel{{\scriptstyle}}{{\frown}}e^{\prime}$) and there is
$C\in\mathit{Conf}({E})$ such that $C\vdash e$ and $C\vdash e^{\prime}$.

Thus in a live es conflict is saturated, a property that corresponds to
inheritance of conflict in prime ess, and each event is executable.

######  Remark 1.

In the paper we restrict to live es. Hence the qualification _live_ is
omitted.

The class of es can be turned into a category.

[category of es] A morphism of es $f:\langle
E_{1},\vdash_{1},\\#_{1}\rangle\to\langle E_{2},\vdash_{2},\\#_{2}\rangle$ is
a partial function $f:E_{1}\rightharpoonup E_{2}$ such that for all
$C_{1}\in\mathit{Conf}({E_{1}})$ and $e_{1},e_{1}^{\prime}\in E_{1}$ with
$f(e_{1})$, $f(e_{1}^{\prime})$ defined

  * •

if $f(e_{1})\,\\#_{2}\,f(e_{1}^{\prime})$ then
$e_{1}\,\\#_{1}\,e_{1}^{\prime}$

  * •

if $f(e_{1})=f(e_{1}^{\prime})$ and $e_{1}\neq e_{1}^{\prime}$ then
$e_{1}\,\\#_{1}\,e_{1}^{\prime}$;

  * •

if $C_{1}\vdash_{1}e_{1}$ then $f(C_{1})\vdash_{2}f(e_{1})$.

We denote by $\mathsf{ES}$ the category of es and their morphisms.

Since the enabling predicate is over finite sets of events, we can consider
minimal sets of events enabling a given one.

[minimal enabling, causality] Let $\langle E,\vdash,\\#\rangle$ be an es.
Given $e\in E$ and $C\in\mathit{Conf}({E})$ such that $C\vdash e$ we say that
$C$ is a _minimal enabling_ of $e$, and write $C\vdash_{0}e$, when for any
configuration $C^{\prime}\subseteq C$, if $C^{\prime}\vdash e$ then
$C^{\prime}=C$. We denote by $\mathbf{H}({e})=\\{C\mid C\vdash_{0}e\\}$ the
set of minimal enablings of event $e$. We write $e<e^{\prime}$ if $e\in C$ for
all $C\in\mathbf{H}({e^{\prime}})$.

The configurations of an es, ordered by subset inclusion, form a partial order
that is characterised in [3] as a weak prime algebraic domain, i.e., a
coherent finitary partial order where each element is the join of elements
satisfying a weak notion of primality. The relation is formalised as a
coreflection between the category $\mathsf{ES}$ and a category $\mathsf{wDom}$
of weak prime domains. A subclass of ess can be identified, called _connected
es_, that represents the exact counterpart of weak prime domains, in the same
way as prime ess are the counterpart of prime algebraic domains [33].

[connected es] Let $C,C^{\prime}\in\mathbf{H}({e})$. We write
$C\stackrel{{\scriptstyle e}}{{\frown}}C^{\prime}$ if $C\cup
C^{\prime}\cup\\{e\\}$ is consistent and we denote by $\stackrel{{\scriptstyle
e}}{{\frown}}^{*}$ the transitive closure of the relation
$\stackrel{{\scriptstyle e}}{{\frown}}$. An es is _connected_ if whenever
$C,C^{\prime}\in\mathbf{H}({e})$ then $C\stackrel{{\scriptstyle
e}}{{\frown}}^{*}C^{\prime}$. The full subcategory of $\mathsf{ES}$ having
connected es as objects is denoted by $\mathsf{cES}$.

The category $\mathsf{cES}$ is equivalent to the category $\mathsf{wDom}$ of
weak prime domains and thus it coreflects in $\mathsf{ES}$.

######  Proposition 2 (coreflection between $\mathsf{ES}$ and $\mathsf{cES}$
[3]).

The inclusion functor $\mathcal{I}:\mathsf{cES}\to\mathsf{ES}$ admits a right
adjoint $\mathcal{C}:\mathsf{ES}\to\mathsf{cES}$ establishing a coreflection.

As mentioned in the introduction, the concurrent semantics of Petri nets with
persistence will be given in terms of connected es through a chain of
transformations that first unfolds the net into an acyclic net and then
abstracts it to an es.

The connectedness condition has a natural logical interpretation. Given an
event $e$, we can capture its dependencies by stating that $e$ is caused by
the disjunction of its minimal enablings, where each minimal enabling can be
seen in turn as a conjunction of events, namely by
$\bigvee_{C\in\mathbf{H}({e})}\bigwedge C$. A conflict
$e^{\prime}\\#e^{\prime\prime}$ can be encoded as $\neg e^{\prime}\lor\neg
e^{\prime\prime}$. In this view, connectedness amounts to the impossibility of
partitioning $\mathbf{H}({e})$ in two subsets inducing mutually exclusive
minimal causal histories, i.e., we cannot decompose
$\mathbf{H}({e})=H_{1}\uplus H_{2}$ in a way that $\neg(\bigvee_{C\in
H_{1}}\bigwedge(C\cup\\{e\\}))\ \lor\ \neg(\bigvee_{C\in
H_{2}}\bigwedge(C\cup\\{e\\}))$. If this happened, to recover connectedness we
should split event $e$ in two events $e_{1}$ and $e_{2}$, with
$\mathbf{H}({e_{i}})=H_{i}$ for $i\in\\{1,2\\}$.

At the level of nets, events correspond to transitions. Each transition
requires that all the (possibly persistent) places in its pre-set are filled
in order to be enabled, hence it is enabled by a _conjunction_ of places. In
turn, each persistent place can be seen as the _disjunction_ of the
transitions in its pre-set. Summing up, at the level of nets we can represent
conjunctions of disjunctions of events, exploiting persistence. The natural
choice, when working with nets, will be to impose the connectedness condition
locally to each disjunct. This results in a property weaker than the “global”
connectedness from Definition 1. For this reason, the extraction of a
connected es from a net will pass through an intermediate class of es that we
call _locally connected_. We next formalise this idea.

[es in disjunctive form] Let $E$ be an es. Given $e\in E$, a _disjunct_ of $e$
is a minimal set $X\subseteq E$ such that $X\cap C\neq\emptyset$ for all
$C\in\mathbf{H}({e})$. It is _connected_ if for all $e,e^{\prime}\in X$ there
exists $n\geq 1$ and $e_{1},e_{2},...,e_{n}\in X$ such that
$e=e_{1}\stackrel{{\scriptstyle}}{{\frown}}e_{2}\stackrel{{\scriptstyle}}{{\frown}}\cdots\stackrel{{\scriptstyle}}{{\frown}}e_{n}=e^{\prime}$.

A _covering_ of $e$ is a set of disjuncts $D\subseteq\mathbf{2}^{E}$ such that
for any $C\in\mathit{Conf}({E})$, if $C\cap X\neq\emptyset$ for all $X\in D$
then $C\vdash e$.

Intuitively, $D$ is a covering of an event $e$ whenever condition
$\bigwedge_{X\in D}\bigvee X$ is necessary and sufficient for enabling $e$,
i.e., it is logically equivalent to the disjunction of the minimal enablings
$\bigvee_{C\in\mathbf{H}({e})}\bigwedge C$. A disjunct $X$ of $e$ is connected
whenever it cannot be partitioned as $X=X_{1}\uplus X_{2}$ with $\neg(\bigvee
X_{1})\lor\neg(\bigvee X_{2})$. Intuitively, we are moving from a
$\vee$-$\wedge$ form of the dependencies to a $\wedge$-$\vee$ form, and
transferring the connectedness condition from the outer to the inner
disjunctions. Expressing dependencies as a conjunction of disjunctive causes
makes it natural to associate a net with persistent places with the es: each
event $e$ becomes a transition and each disjunct $X$ of $e$ corresponds to a
persistent place $s$ in the pre-set of $e$, filled by the events in $X$. The
guarantee that the disjunctive causes cannot be split into inconsistent
subsets will provide a form of canonicity to the construction.

Note that an event enabled by the empty set has no disjuncts (the empty set,
which as a disjunct would correspond to “true”, is not admitted).

[locally connected es] An es $E$ is _locally connected_ if for all $e\in E$
there exists a covering $D$ such that any $X\in D$ is connected. We denote by
$\mathsf{{\ell}ES}$ the full subcategory of $\mathsf{ES}$ having locally
connected event structures as objects.

It can be easily shown that connectedness implies local connectedness. We
first observe that in an es every event admits a covering, which is the set of
all its disjuncts.

######  Lemma 3 (coverings always exist).

Let $E$ be an es and $e\in E$. Then $D_{e}=\\{X\mid X\subseteq E\land\
\mbox{$X$ is a disjunct of $e$}\\}$ is a covering of $e$.

######  Proof 2.1.

Let $C\in\mathit{Conf}({E})$ be a configuration such that $C\cap
X\neq\emptyset$ for all $X\in D_{e}$, and suppose by absurd that $C\not\vdash
e$. This means that for all $C^{\prime}\in\mathbf{H}({e})$ there is an event
$e_{C^{\prime}}\in C^{\prime}\setminus C$. Let $X^{\prime}$ be a minimal
subset of $\\{e_{C^{\prime}}\mid C^{\prime}\in\mathbf{H}({e})\\}$ such that
$X^{\prime}\cap C^{\prime}\not=\emptyset$ for all
$C^{\prime}\in\mathbf{H}({e})$: then clearly $X^{\prime}$ is a disjunct in
$D_{e}$, but $X^{\prime}\cap C=\emptyset$, yielding a contradiction.

######  Lemma 4 (connectedness vs local connectedness).

Let $E$ be an es. If $E$ is connected then it is locally connected.

######  Proof 2.2.

Let $E$ be a connected es and let $e\in E$ be an event. Let $X$ be any
disjunct of $e$ and consider $e_{1},e_{2}\in X$. By minimality of a disjunct,
we deduce that there must be $C_{1},C_{2}\in\mathbf{H}({e})$ such that
$e_{i}\in C_{i}$, for $i\in\\{1,2\\}$. Since $E$ is connected, we know that
$C_{1}\stackrel{{\scriptstyle e}}{{\frown}}^{*}C_{2}$. Then we can prove that
$e_{1}\stackrel{{\scriptstyle}}{{\frown}}^{*}e_{2}$ by induction on the length
of the chain of consistency $C_{1}\stackrel{{\scriptstyle
e}}{{\frown}}^{*}C_{2}$. The base case is trivial. For the inductive step,
assume that $C_{1}\stackrel{{\scriptstyle
e}}{{\frown}}^{*}C_{1}^{\prime}\stackrel{{\scriptstyle e}}{{\frown}}C_{2}$.
Take any $e_{1}^{\prime}\in C_{1}^{\prime}$. By inductive hypothesis we know
that $e_{1}\stackrel{{\scriptstyle}}{{\frown}}^{*}e_{1}^{\prime}$. Moreover,
since $C_{1}^{\prime}\stackrel{{\scriptstyle e}}{{\frown}}C_{2}$ we deduce
$e_{1}^{\prime}\stackrel{{\scriptstyle}}{{\frown}}e_{2}$. Thus we conclude
$e_{1}\stackrel{{\scriptstyle}}{{\frown}}^{*}e_{2}$ as desired.

The above result shows that $\mathsf{cES}$ is a full subcategory of
$\mathsf{{\ell}ES}$. Hence the coreflection between $\mathsf{ES}$ and
$\mathsf{cES}$ restricts to a coreflection between $\mathsf{{\ell}ES}$ and
$\mathsf{cES}$.

######  Proposition 5 (coreflection between $\mathsf{{\ell}ES}$ and
$\mathsf{cES}$).

The inclusion functor $\mathcal{I}:\mathsf{cES}\to\mathsf{{\ell}ES}$ is left
adjoint of the restriction
$\mathcal{C}_{|\mathsf{{\ell}ES}}:\mathsf{{\ell}ES}\to\mathsf{cES}$,
establishing a coreflection.

######  Proof 2.3.

Immediate consequence of Proposition 2 and Lemma 4.

Local connectedness is strictly weaker than connectedness. Let
$E=\\{a,b,c,d,e\\}$ be the es with $\emptyset\vdash_{0}a$,
$\emptyset\vdash_{0}b$, $\emptyset\vdash_{0}c$, $\emptyset\vdash_{0}d$,
$a\\#c$, $b\\#d$, $\\{a,b\\}\vdash_{0}e$ and $\\{c,d\\}\vdash_{0}e$. This is
not so, since $\mathbf{H}({e})=\\{\\{a,b\\},\\{c,d\\}\\}$ and
$\\{a,b\\}\stackrel{{\scriptstyle e}}{{\frown}}\\{c,d\\}$ does not hold. It is
locally connected, since $\\{\\{a,d\\},\\{b,c\\}\\}$ is a covering of $e$ and
the disjuncts $\\{a,d\\}$ and $\\{b,c\\}$ are connected since
$a\stackrel{{\scriptstyle}}{{\frown}}d$ and
$b\stackrel{{\scriptstyle}}{{\frown}}c$. Logically, the cause of $e$ in
$\vee$-$\wedge$ form is $(a\wedge b)\vee(c\wedge d)$. It is not connected
since $\neg(a\wedge b)\vee\neg(c\wedge d)$ (and thus $\neg(a\wedge b\wedge
e)\vee\neg(c\wedge d\wedge e)$). If we put the causes in $\wedge$-$\vee$ form
we get $(a\vee d)\wedge(b\vee c)$, where neither $\neg a\vee\neg d$ nor $\neg
b\vee\neg c$, whence local connectedness.

Dealing with (locally) connected es will play an essential role for
establishing a coreflection between occurrence nets with persistence and ess
(see Theorem 29). At an intuitive level, it ensures that or-causality is
preserved along morphisms and cannot be transformed in ordinary causality.
Instead, consider for instance the es $E_{1}$ and $E_{2}$ defined as follows

  * •

$E_{1}=\\{a_{1},a_{2},b\\}$ with $\emptyset\vdash_{0}a_{i}$,
$\\{a_{i}\\}\vdash_{0}b$ for $i\in\\{1,2\\}$ and $a_{1}\\#a_{2}$;

  * •

$E_{2}=\\{a,b\\}$ with $\emptyset\vdash_{0}a$ and $a\vdash_{0}b$

The es $E_{1}$ is not locally-connected, since $\\{a_{1},a_{2}\\}$ is the only
disjunct for $b$ and it is not connected. It is easy to realise that the
mapping $f:E_{1}\to E_{2}$ defined by $f(a_{1})=f(a_{2})=a$ and $f(b)=b$ is an
es morphism: merging $a_{1}$ and $a_{2}$ the or-causality of $b$ is
transformed into a proper causality $a<b$.

##  3\. Nets with Persistence

In this section we introduce Petri nets with persistence. Since the state of a
Petri net will be seen as a multiset, i.e., an element of a suitably defined
monoid, we start with some notation on sets and monoids. The irrelevance of
the number of tokens in persistent places is modelled by some form of
idempotency in the monoid.

Recall that, given a set $X$, we denote by $\mathbf{2}^{X}$ the powerset of
$X$ and by $\mathbf{2}_{f}^{X}$ the set of finite subsets of $X$. We denote by
${X}^{\oplus}=\\{u\mid u:X\to{\rm Nature}\\}$ the commutative monoid of
multisets on $X$ with the operation $\oplus$ and identity $\emptyset$ defined
in an obvious way. Elements of ${X}^{\oplus}$ are often represented by formal
sums $u=\bigoplus_{x\in X}u(x)\cdot x$. Given $u\in{X}^{\oplus}$ we denote by
$[\\!\\![{u}]\\!\\!]$ the underlying set $\\{x\mid x\in X\ \land\ u(x)>0\\}$.
We write $x\in u$ for $x\in[\\!\\![{u}]\\!\\!]$ and we say that $u$ is
_finite_ if $[\\!\\![{u}]\\!\\!]$ is finite. We identify a set
$u\in\mathbf{2}^{X}$ and the “corresponding” multiset $\bigoplus_{x\in
u}1\cdot x$. Given $u,u^{\prime}\in{X}^{\oplus}$ we say that $u$ _covers_
$u^{\prime}$, written $u^{\prime}\subseteq u$, if there is
$u^{\prime\prime}\in{X}^{\oplus}$ such that $u=u^{\prime}\oplus
u^{\prime\prime}$. For $u,u^{\prime}\in{X}^{\oplus}$ we write $u\cap
u^{\prime}$ for the largest $u^{\prime\prime}$ such that
$u^{\prime\prime}\subseteq u$ and $u^{\prime\prime}\subseteq u^{\prime}$.

When $X$ has a chosen subset $X^{\mathrm{p}}\subseteq X$, the commutative
monoid with idempotency is ${(X,X^{\mathrm{p}})}^{\oplus}=\\{u\mid u:X\to{\rm
Nature}\ \land\ \forall x\in X^{\mathrm{p}}.\,u(x)\leq 1\\}$. Elements are
still seen as formal sums $u=\bigoplus_{x\in X}u(x)\cdot x$, with an
idempotency axiom $x\oplus x=x$ for any $x\in X^{\mathrm{p}}$. As before,
given $u,u^{\prime}\in{(X,X^{\mathrm{p}})}^{\oplus}$ we say that $u$ _covers_
$u^{\prime}$, written $u^{\prime}\subseteq u$, if there is
$u^{\prime\prime}\in{X}^{\oplus}$ such that $u=u^{\prime}\oplus
u^{\prime\prime}$. Note however that due to idempotency there can be several
$u^{\prime\prime}$ such that $u=u^{\prime}\oplus u^{\prime\prime}$. More
precisely, the set $\\{u^{\prime\prime}\mid u=u^{\prime}\oplus
u^{\prime\prime}\\}$ forms a lattice with respect to $\subseteq$ and we write
$u\ominus u^{\prime}$ to denote the top element of the lattice. For example,
when $a\in X\setminus X^{\mathrm{p}}$ and $b,c\in X^{\mathrm{p}}$, although
$(a\oplus b)\oplus(a\oplus c)=2a\oplus b\oplus c$ we have $(2a\oplus b\oplus
c)\ominus(a\oplus b)=a\oplus b\oplus c$.

Given sets $X$, $Y$, a monoid homomorphism $f:{X}^{\oplus}\to{Y}^{\oplus}$ is
called _finitary_ if for all $x\in X$, $f(x)$ is finite. A function
$f:X\to{Y}^{\oplus}$ that is finitary (i.e., $f(x)$ finite for all $x\in X$)
can be extended to a finitary monoid homomorphism denoted
${f}^{\oplus}:{X}^{\oplus}\to{Y}^{\oplus}$, defined by
${f}^{\oplus}(\bigoplus_{x\in X}n_{x}\cdot x)=\bigoplus_{x\in X}n_{x}\cdot
f(x)$. Analogous notions can be defined for partial functions and when the
target or both the source and target are monoids with idempotency.

[net with persistence] An (unweighted marked P/T Petri) _net with persistence_
(_p-net_ , for short) is a tuple
$N=(S,S^{\mathrm{p}},T,\delta_{0},\delta_{1},u_{0})$, where $S$ is a set of
_places_ , $S^{\mathrm{p}}\subseteq S$ is the set of _persistent_ places, $T$
is a set of _transitions_ , $\delta_{0},\delta_{1}:T\to\mathbf{2}^{S}$ are
functions assigning sets called pre-set and post-set, respectively, to each
transition and $u_{0}\subseteq S^{\mathrm{n}}$ is the _initial marking_ ,
where $S^{\mathrm{n}}$ is the set of non-persistent places
$S^{\mathrm{n}}=S\setminus S^{\mathrm{p}}$.

Given a finite multiset of transitions $v\in{T}^{\oplus}$ we write ${\rm
Phys.~{}Rev.~{}E}{v}$ and ${v}{{}^{\bullet}}$ for ${\delta_{0}}^{\oplus}(v)$
and ${\delta_{1}}^{\oplus}(v)$. Given a place $s\in S$ we also write ${\rm
Phys.~{}Rev.~{}E}{s}$ for $\\{t\mid s\in{t}{{}^{\bullet}}\\}$ and
${s}{{}^{\bullet}}$ for $\\{t\mid s\in{\rm Phys.~{}Rev.~{}E}{t}\\}$.

Hereafter, for any p-net $N$ we assume
$N=(S,S^{\mathrm{p}},T,\delta_{0},\delta_{1},u_{0})$, with subscripts and
superscripts carrying over the names of the components. Note that we work with
nets that are not weighted (pre- and post-sets of transitions are sets, rather
than multisets). The results could be trivially extended, as in the ordinary
case, to semi-weighted nets (where the pre-set can be a proper multiset). The
restriction is adopted to ease the presentation.

The state of a p-net $N$ is represented by some
$u\in{(S,S^{\mathrm{p}})}^{\oplus}$, called a _marking_ of $N$. A transition
$t$ is _enabled_ by a marking $u$ if its pre-set is covered by $u$, i.e. if
${\rm Phys.~{}Rev.~{}E}{t}\subseteq u$. In this case, $t$ can be fired. The
firing of $t$ consumes the tokens in the non-persistent places in the pre-set,
leaves untouched the tokens in the persistent places and produces the tokens
in the post-set. More generally, this applies to finite multisets of
transitions. Formally, given a finite multiset $v\in{T}^{\oplus}$ and a
marking $u\in{(S,S^{\mathrm{p}})}^{\oplus}$, if ${\rm
Phys.~{}Rev.~{}E}{v}\subseteq u$, the firing rule is
$u[{v}\rangle(u\ominus{\rm Phys.~{}Rev.~{}E}{v})\oplus{v}{{}^{\bullet}}$.

A marking $u\in{S}^{\oplus}$ is _reachable_ if there exists a firing sequence
$u_{0}[{t_{1}}\rangle u_{1}[{t_{2}}\rangle\ldots[{t_{n}}\rangle u$ from the
initial marking to $u$. The p-net is _safe_ if every reachable marking is a
set.

Observe now that in the initial marking only non-persistent places can be
marked. Indeed, if a persistent place $p$ were marked in the initial marking
then its presence would be essentially useless, since any reachable marking
would contain one token in $p$. Therefore removing $p$ and all the incoming
and outgoing arcs would lead to an equivalent net that can perform the same
firing sequences and such that a marking $u$ is reachable if and only if the
marking $u\oplus p$ was reachable in the original net.

Let us consider the p-net in Figure 1 of our running example, whose initial
marking is $u_{0}=p\oplus q\oplus r\oplus s$. A sample firing sequence is

$u_{0}\ [{a}\rangle\ q\oplus r\oplus s\oplus o\ [{b}\rangle\ r\oplus s\oplus
o\ [{c}\rangle\ r\oplus s\oplus o\ [{d}\rangle\ t\oplus s\oplus o\
[{e}\rangle\ t\oplus u\oplus o$

Note that once the token in the persistent place $o$ is produced by the firing
of $a$, it is never possible to remove it, not even firing $d$ or $e$. Also
note that after $b$ fires, the multiplicity of $o$ remains $1$ due to the
idempotency axiom on persistent places. It is immediate to check that the
p-net is safe, as all reachable markings are sets.

######  Remark 6.

Our presentation of p-nets slightly differs from the original one in [9].
There: (i) arcs carry weight $1$ or $\infty$; (ii) an arc has weight $\infty$
if and only if it goes from a transition to a persistent place; (iii) markings
allows having either $0$ or infinitely many tokens in each persistent place;
(iv) even if a firing removes finitely many tokens from persistent place,
there remain infinitely many tokens available. As each marking associates only
one bit of information with each persistent place, here we find technically
more convenient to represent marked persistent places by assigning them
multiplicity $1$ and by exploiting idempotency to capture the fact that when
infinitely many tokens are added to a marked persistent place there still are
infinitely many tokens (indistinguishable one from the other).

######  Remark 7.

We use the term “net with persistence” to avoid confusion with the notion of
“persistent net” in the literature (see e.g. [19]), a behavioural property
defined as follows: A net is persistent if whenever $u[{t_{1}}\rangle$ and
$u[{t_{2}}\rangle$ for a reachable marking $u$, then $u[{t_{1}\oplus
t_{2}}\rangle$.

When dealing with unfolding and, more generally, with the causal semantics of
ordinary Petri nets, it is a standard constraint to assume that transitions
have a non-empty pre-set. This avoids the unnatural possibility of firing
infinitely many copies of the same transition in parallel. For p-nets, this
generalises to the requirement that each transition consumes tokens from at
least one non-persistent place. Additionally, since a persistent place will
never be emptied once it is filled with a token, whenever a persistent place
$s$ is in the post-set of a transition $t$ it is quite natural to forbid the
presence of an additional path from $t$ to $s$. This property is formalised by
using the flow relation $\rightsquigarrow_{N}$ for a net $N$, defined, for all
$x,y\in S\cup T$, by $x\rightsquigarrow_{N}y$ if $x\in{\rm
Phys.~{}Rev.~{}E}{y}$.

[well-formed net] A p-net $N$ is _well-formed_ if for all $t\in T$,
$\delta_{0}(t)\not\in{S^{\mathrm{p}}}^{\oplus}$ (_t-restrictedness_) and for
all $t\in T$, $s\in S^{\mathrm{p}}$, if $t\rightsquigarrow_{N}s$ then
$t\not\rightsquigarrow_{N}^{n}s$ for $n\geq 2$ (_irredundancy_).

Observe that, in particular, whenever a p-net is irredundant, it does not
include cycles over persistent places, i.e., for any $s\in S^{\mathrm{p}}$, it
is not the case that $s\rightsquigarrow_{N}^{+}s$. Hereafter all p-nets will
be tacitly assumed to be well-formed.

The notion of p-net morphism naturally arises from an algebraic view, where
places and transitions play the role of sorts and operators.

[p-net morphism] A _p-net morphism_ $f=\langle
f_{\mathrm{s}},f_{\mathrm{t}}\rangle:N\to N^{\prime}$ is a pair where

  1. (1)

$f_{\mathrm{s}}:{(S,S^{\mathrm{p}})}^{\oplus}\to{(S^{\prime},S^{\prime\mathrm{p}})}^{\oplus}$
is a finitary monoid homomorphism such that for $s\in S^{\mathrm{n}}$,
$f_{\mathrm{s}}(s)\in{S^{\prime\mathrm{n}}}^{\oplus}$ and the initial marking
is preserved, i.e. $f_{\mathrm{s}}(u_{0})=u^{\prime}_{0}$;

  2. (2)

$f_{\mathrm{t}}:T\rightharpoonup T^{\prime}$ is a partial function such that
for all finite $v\in{T}^{\oplus}$, ${\rm
Phys.~{}Rev.~{}E}{({f_{\mathrm{t}}}^{\oplus}(v))}=f_{\mathrm{s}}({\rm
Phys.~{}Rev.~{}E}{v})$ and
${({f_{\mathrm{t}}}^{\oplus}(v))}{{}^{\bullet}}=f_{\mathrm{s}}({v}{{}^{\bullet}})$;

  3. (3)

for all $t\in T$ and $s_{1},s_{2}\in{\rm Phys.~{}Rev.~{}E}{t}$ or
$s_{1},s_{2}\in{t}{{}^{\bullet}}$, if $f_{\mathrm{s}}(s_{1})\cap
f_{\mathrm{s}}(s_{2})\neq\emptyset$ then $s_{1}=s_{2}$.

The category of p-nets (as objects) and their morphisms (as arrows) is denoted
by $\mathsf{PN}$.

Observe that by the fact that
$f_{s}:{(S,S^{\mathrm{p}})}^{\oplus}\to{(S^{\prime},S^{\prime\mathrm{p}})}^{\oplus}$
is a monoid homomorphism and condition (1) we automatically get that $s\in
S^{\mathrm{p}}$ implies $f_{\mathrm{s}}(s)\in{S^{\prime\mathrm{p}}}^{\oplus}$.
Moreover, for all $u_{1},u_{2}\in{(S,S^{\mathrm{p}})}^{\oplus}$, with
$u_{2}\subseteq u_{1}$, it holds that $f_{\mathrm{s}}(u_{1}\ominus
u_{2})=f_{\mathrm{s}}(u_{1})\ominus f_{\mathrm{s}}(u_{2})$. Condition (2)
amounts to require that for any $t\in T$, if $f_{\mathrm{t}}(t)$ is defined
then ${\rm Phys.~{}Rev.~{}E}{{f_{\mathrm{t}}}(t)}=f_{\mathrm{s}}({\rm
Phys.~{}Rev.~{}E}{t})$ and
${{f_{\mathrm{t}}}(t)}{{}^{\bullet}}=f_{\mathrm{s}}({t}{{}^{\bullet}})$, and
$f_{\mathrm{s}}({\rm
Phys.~{}Rev.~{}E}{t})=f_{\mathrm{s}}({t}{{}^{\bullet}})=\emptyset$ otherwise.
Finally, condition (3) imposes injectivity of the morphism on the pre-set and
post-set of each transition, i.e., the morphism should not mix places in the
pre-set (and in the post-set) of the same transition. This is automatically
satisfied for non-persistent places, but it could be violated by persistent
places (due to idempotency), hence we require it explicitly.

In the sequel, when the meaning is clear from the context, we often omit the
subscripts from the morphism components, thus writing $f$ instead of
$f_{\mathrm{s}}$ and $f_{\mathrm{t}}$.

######  Lemma 8 (p-net morphisms are simulations).

Let $f:N\to N^{\prime}$ be a p-net morphism. If $u[{v}\rangle u^{\prime}$ is a
firing in $N$ then $f(u)[{{f}^{\oplus}(v)}\rangle f(u^{\prime})$ is a firing
in $N^{\prime}$.

######  Proof 3.1.

Since $f$ is a p-net morphism we have ${\rm
Phys.~{}Rev.~{}E}{({f}^{\oplus}(v))}=f({\rm Phys.~{}Rev.~{}E}{v})$ and
${({f}^{\oplus}(v))}{{}^{\bullet}}=f({v}{{}^{\bullet}})$. Since $u[{v}\rangle
u^{\prime}$, it must be the case that $u=u^{\prime\prime}\oplus{\rm
Phys.~{}Rev.~{}E}{v}$ for some $u^{\prime\prime}$, from which
$f(u)=f(u^{\prime\prime})\oplus f({\rm Phys.~{}Rev.~{}E}{v})$, i.e., $f({\rm
Phys.~{}Rev.~{}E}{v})\subseteq f(u)$ and thus ${f}^{\oplus}(v)$ is enabled at
$f(u)$. Therefore there is a firing

$f(u)[{{f}^{\oplus}(v)}\rangle(f(u)\ominus{\rm
Phys.~{}Rev.~{}E}{({f}^{\oplus}(v))})\oplus{({f}^{\oplus}(v))}{{}^{\bullet}}$

and the target $(f(u)\ominus{\rm
Phys.~{}Rev.~{}E}{({f}^{\oplus}(v))})\oplus{({f}^{\oplus}(v))}{{}^{\bullet}}=(f(u)\ominus
f({\rm Phys.~{}Rev.~{}E}{v}))\oplus f({v}{{}^{\bullet}})=f((u\ominus{\rm
Phys.~{}Rev.~{}E}{v})\oplus{v}{{}^{\bullet}})=f(u^{\prime})$, as it was
required.

##  4\. Unfolding Nets with Persistence

In this section we show how a p-net can be unfolded to a suitably defined
occurrence p-net that represents all possible occurrences of firing of
transitions and their dependencies. We first introduce the class of occurrence
p-nets, where each transition can occur at most once in a computation, but
possibly with different disjunctive causes. We next observe that occurrence
p-nets can be equivalently presented by forcing each transition to have a
uniquely determined set of causes and using an equivalence between transitions
to account for disjunctive causes. Finally, we present the unfolding
construction for a p-net, that works in two steps. First a p-net is unfolded
into an occurrence p-net without backward conflicts, where each item has a
uniquely determined causal history. The possibility of generating a token in
the same persistent place with different histories is captured by means of an
equivalence relation on places and transitions. Then the actual unfolding is
obtained as the quotient of the pre-unfolding with respect to the equivalence
relation.

###  4.1. Occurrence p-nets

In order to single out the class of occurrence p-nets, we start by defining
the possible dependencies in a p-net.

[enabling, conflict, causality, dependence, concurrency] Let $N$ be a p-net.

  * •

Enabling, written $\vdash_{N}$, is defined by letting, for
$X\in\mathbf{2}_{f}^{T}$ and $t\in T$, $X\vdash_{N}t$ if for all $s\in{\rm
Phys.~{}Rev.~{}E}{t}$ either $s\in u_{0}$ or there exists $t^{\prime}\in X$
such that $s\in{t^{\prime}}{{}^{\bullet}}$.

  * •

Conflict $\\#_{N}\subseteq\mathbf{2}^{S\cup T}$ is the least set-relation,
closed by superset, defined by

    1. (a)

if $t\neq t^{\prime}$ and ${\rm Phys.~{}Rev.~{}E}{t}\cap{\rm
Phys.~{}Rev.~{}E}{t^{\prime}}\not\subseteq S^{\mathrm{p}}$, then
$\\#_{N}\\{t,t^{\prime}\\}$;

    2. (b)

if ${\rm Phys.~{}Rev.~{}E}{s}\neq\emptyset$ and $\\#_{N}(X\cup\\{t\\})$ for
all $t\in{\rm Phys.~{}Rev.~{}E}{s}$, then $\\#_{N}(X\cup\\{s\\})$;

    3. (c)

if $\\#_{N}(X\cup\\{s\\})$ and $s\in{\rm Phys.~{}Rev.~{}E}{t}$, then
$\\#_{N}(X\cup\\{t\\})$.

We will often write $x\\#_{N}x^{\prime}$ instead of
$\\#_{N}\\{x,x^{\prime}\\}$. We say that $X$ is _consistent_ if it is not in
conflict. In particular, binary consistency is denoted
$\stackrel{{\scriptstyle}}{{\frown}}_{N}$, i.e.,
$x\stackrel{{\scriptstyle}}{{\frown}}_{N}x^{\prime}$ when
$\neg(x\\#_{N}x^{\prime})$. We say that $X$ is _connected_ by
$\stackrel{{\scriptstyle}}{{\frown}}_{N}$ if for all $x,x^{\prime}\in X$ there
exists $n\geq 1$ and $x_{1},x_{2},...,x_{n}\in X$ such that
$x=x_{1}\stackrel{{\scriptstyle}}{{\frown}}_{N}x_{2}\stackrel{{\scriptstyle}}{{\frown}}_{N}\cdots\stackrel{{\scriptstyle}}{{\frown}}_{N}x_{n}=x^{\prime}$.

  * •

Causality $\leq_{N}$ is the least transitive and reflexive relation $\leq_{N}$
on $S\cup T$ such that if $s\in{\rm Phys.~{}Rev.~{}E}{t}$ then $s\leq_{N}t$
and if ${\rm Phys.~{}Rev.~{}E}{s}=\\{t\\}$ then $t\leq_{N}s$. We write
$x<_{N}x^{\prime}$ when $x\leq_{N}x^{\prime}$ and $x\neq x^{\prime}$.

When the context is clear, we will omit the subscript $N$, writing $\vdash$,
$\\#$, $\leq$ and $\stackrel{{\scriptstyle}}{{\frown}}$ instead of
$\vdash_{N}$, $\\#_{N}$, $\leq_{N}$ and
$\stackrel{{\scriptstyle}}{{\frown}}_{N}$.

Differently from what happens for ordinary nets, in occurrence p-nets we will
allow different ways of enabling the same occurrence of a transition. This is
because tokens, once generated in persistent places, cannot be consumed and
all tokens in the same place are “merged” into one (by idempotency) in a way
that the resulting single token joins all the different possible causal
histories. For this reason it is convenient to resort to a general notion of
enabling where a transition naturally has several sets of transitions that
allow for its execution. Observe that if $X\vdash e$ and $X\subseteq
X^{\prime}$ then $X^{\prime}\vdash e$. As it happens for ess, when $X\vdash
e$, the set $X$ can be inconsistent. We will later impose a condition forcing
each transition to be enabled by at least one minimal consistent set.

Note that direct conflict is only binary, since it is determined by the
competition on non-persistent places. However, in order to define properly
inheritance of conflict along the enabling relation we need to work with a
conflict relation on generic sets. Consider for instance, the p-net in Figure
2a. and the set of places $\\{p,q,r\\}$. The rules for conflict allow us to
deduce that $\\#\\{p,q,r\\}$, while $\neg x\\#y$ for all $x,y\in\\{p,q,r\\}$.
Intuitively this happens because at most two places in the set $\\{p,q,r\\}$
can be filled. The formal derivation can be found in Figure 2b. The relation
between coverability and absence of conflicts will be characterised later via
the notion of concurrency, in Lemma 11.

We also introduce causality: when an item $x$ is a cause of an item $y$ the
intuition is that the presence of $y$ in a computation implies the presence of
$x$, i.e., $x$ is needed to “enable” $y$. This will play a role later.
However, note that causality alone would not completely characterise the
dependencies in the p-net as it does not account for disjunctive causes.

We next define the notion of securing sequence in the context of p-nets.

[securing sequence] Let $N$ be a p-net. Given a transition $t\in T$, a
_securing sequence_ for $t$ in $N$ is a sequence of distinct transitions
$t_{1},t_{2},\ldots,t_{n}=t$ such that for all $i,j\in[{1},{n}]$,
$\neg(t_{i}\\#t_{j})$ and for all $i\in[{1},{n}]$, $\\{t_{1}\ldots
t_{i-1}\\}\vdash t_{i}$.

A securing sequence for $t$ is intended to represent a firing sequence that
leads to the execution of $t$. This fact will be later formalised, for
occurrence p-nets, in Lemma 9.

$\textstyle{\bullet}$$\textstyle{\bullet}$$\textstyle{a_{1}}$$\textstyle{a_{2}}$$\textstyle{b_{1}}$$\textstyle{b_{2}}$$\textstyle{c_{1}}$$\textstyle{c_{2}}$
$\textstyle{\scriptstyle{p}}$ $\textstyle{\scriptstyle{q}}$
$\textstyle{\scriptstyle{r}}$

(a)

$\\#\\{p,q,r\\}\lx@proof@logical@and\\#\\{p,q,c_{1}\\}\lx@proof@logical@and\\#\\{p,b_{1},c_{1}\\}\\#\\{b_{1},c_{1}\\}{\rm
Phys.~{}Rev.~{}E}{b_{1}}\cap{\rm Phys.~{}Rev.~{}E}{c_{1}}\not\subseteq
S^{\mathrm{p}}\\#\\{p,b_{2},c_{1}\\}\lx@proof@logical@and\\#\\{a_{1},b_{2},c_{1}\\}\\#\\{a_{1},c_{1}\\}{\rm
Phys.~{}Rev.~{}E}{a_{1}}\cap{\rm Phys.~{}Rev.~{}E}{c_{1}}\not\subseteq
S^{\mathrm{p}}\\#\\{a_{2},b_{2},c_{1}\\}\\#\\{a_{2},b_{2}\\}{\rm
Phys.~{}Rev.~{}E}{a_{2}}\cap{\rm Phys.~{}Rev.~{}E}{b_{2}}\not\subseteq
S^{\mathrm{p}}\\#\\{p,q,c_{2}\\}\lx@proof@logical@and\\#\\{p,b_{1},c_{2}\\}\lx@proof@logical@and\\#\\{a_{1},b_{1},c_{2}\\}\\#\\{a_{1},b_{1}\\}{\rm
Phys.~{}Rev.~{}E}{a_{1}}\cap{\rm Phys.~{}Rev.~{}E}{b_{1}}\not\subseteq
S^{\mathrm{p}}\\#\\{a_{2},b_{1},c_{2}\\}\\#\\{a_{2},c_{2}\\}{\rm
Phys.~{}Rev.~{}E}{a_{2}}\cap{\rm Phys.~{}Rev.~{}E}{c_{2}}\not\subseteq
S^{\mathrm{p}}\\#\\{p,b_{2},c_{2}\\}\\#\\{b_{2},c_{2}\\}{\rm
Phys.~{}Rev.~{}E}{b_{2}}\cap{\rm Phys.~{}Rev.~{}E}{c_{2}}\not\subseteq
S^{\mathrm{p}}$

(b)

Figure 2. Non-binary conflict occurrence p-nets

Occurrence p-nets can now be defined as a subclass of p-nets. For historical
reasons, places and transitions of occurrence p-nets are called _conditions_
and _events_ , respectively. We will adopt this convention in the rest of the
paper, denoting occurrence p-nets by $O$, with components
$(B,B^{\mathrm{p}},E,\gamma_{0},\gamma_{1},v_{0})$, where $B$ is the set of
conditions and $E$ the set of events.

[occurrence p-net] A structure
$O=(B,B^{\mathrm{p}},E,\gamma_{0},\gamma_{1},v_{0})$ is an _occurrence p-net_
if it is a p-net such that

  1. (1)

the initial marking $v_{0}$ satisfies $v_{0}=\\{b\in B\mid{\rm
Phys.~{}Rev.~{}E}{b}=\emptyset\\}$;

  2. (2)

each event $e\in E$ admits a securing sequence in $O$;

  3. (3)

for all $e,e^{\prime}\in e$, if $e\neq e^{\prime}$ then
${e}{{}^{\bullet}}\cap{e^{\prime}}{{}^{\bullet}}\subseteq B^{\mathrm{p}}$;

  4. (4)

for all $b\in B$, ${\rm Phys.~{}Rev.~{}E}{b}$ is connected by
$\stackrel{{\scriptstyle}}{{\frown}}_{O}$.

An occurrence p-net is _without backward conflicts_ when for all
$e,e^{\prime}\in E$, if $e\neq e^{\prime}$ then
${e}{{}^{\bullet}}\cap{e^{\prime}}{{}^{\bullet}}=\emptyset$. We denote by
$\mathsf{ON}$ the full subcategory of $\mathsf{PN}$ with occurrence p-nets as
objects.

Observe that by the requiring all events secured (together with the fact that
the initial marking is made of the conditions with empty pre-set) an
occurrence p-net could only be cyclic for the presence of back-pointers to
persistent conditions. This latter possibility is excluded structurally by the
irredundancy assumption (Definition 7). The connectedness requirement for the
pre-set of conditions is trivially satisfied for non-persistent conditions,
since they can have at most one event in their pre-set by condition (3).
Instead, for persistent conditions it is an actual constraint: it imposes that
we cannot split the generators of the condition in two subsets not connected
by consistency. Again the idea is that, if this were the case, the condition
should be split into two occurrences each having an element of the partition
as pre-set. This is reminiscent of the local connectedness requirement for es
and, indeed, it will ensure that the es extracted from an occurrence p-net is
locally connected.

$\textstyle{\bullet}$$\textstyle{\scriptstyle{p}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{q}}$$\textstyle{a}$$\textstyle{b}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{r}}$ $\textstyle{\scriptstyle{o}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{s}}$$\textstyle{d}$$\textstyle{e}$ |
---|---
$\textstyle{{\\{a,b,d,e\\}}}$$\textstyle{{\\{a,d,e\\}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\\{a,b,d\\}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\\{a,b,e\\}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\\{b,d,e\\}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\\{a,d\\}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\\{a,e\\}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\\{a,b\\}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\\{b,d\\}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\\{b,e\\}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\\{a\\}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\\{b\\}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\emptyset}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$
Figure 3. An occurrence p-net and its domain of configurations

An occurrence p-net inspired by our running example is in Figure 3 (left).
Event $a$ has a unique securing sequence consisting of $a$ itself, and
similarly for $b$; $d$ instead has two minimal securing sequences: $ad$ and
$bd$. There is only one backward conflict, on the persistent condition $o$,
since ${a}{{}^{\bullet}}\cap{b}{{}^{\bullet}}=\\{o\\}\subseteq
S^{\mathrm{p}}$. The conflict relation is empty and there is no causality
between events. Note in particular, that ${\rm Phys.~{}Rev.~{}E}{o}$ is
connected by $\stackrel{{\scriptstyle}}{{\frown}}_{O}$ since
$a\stackrel{{\scriptstyle}}{{\frown}}_{O}b$.

Consider now, the p-net in Figure 4 (left). It satisfies all conditions of
Definition 2 but (4). In fact, now the pre-set of ${\rm
Phys.~{}Rev.~{}E}{o}=\\{a,b\\}$ is not connected by
$\stackrel{{\scriptstyle}}{{\frown}}_{N}$ since $a\\#_{N}b$. Intuitively, to
recover connectedness the place $o$ should be split in two places $o_{1}$ and
$o_{2}$, with pre-sets $\\{a\\}$ and $\\{b\\}$, respectively, thus getting the
occurrence p-net in Figure 4 (right). Indeed, this is the occurrence p-net
arising from the unfolding construction described below.

$\textstyle{\bullet}$$\textstyle{\scriptstyle{p}}$$\textstyle{a}$$\textstyle{b}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{r}}$
$\textstyle{\scriptstyle{o}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{s}}$$\textstyle{d}$$\textstyle{e}$
$\textstyle{\bullet}$$\textstyle{\scriptstyle{p}}$$\textstyle{a}$$\textstyle{b}$
$\textstyle{\scriptstyle{\
o_{1}}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{s}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{r}}$
$\textstyle{\scriptstyle{o_{2}\
}}$$\textstyle{d_{1}}$$\textstyle{e_{1}}$$\textstyle{d_{2}}$$\textstyle{e_{2}}$
Figure 4. A p-net that is not an occurrence one (left) and its unfolding
(right).

Note that, as in the case of ordinary occurrence nets, the initial marking is
determined by the structure of the net, i.e., it consists of the set of non-
persistent conditions with empty pre-set. Still, for the sake of clarity it
will be indicated explicitly. It can be easily seen that, in absence of
persistent conditions, Definition 2 gives the ordinary notion of occurrence
net. We have indeed that

  * •

there is no self-conflict because each event is secured;

  * •

there is no backward conflict because for all $e,e^{\prime}\in E$, if $e\neq
e^{\prime}$ then ${e}{{}^{\bullet}}\cap{e^{\prime}}{{}^{\bullet}}=\emptyset$.

Some proofs of results on occurrence p-nets will exploit induction on the
following notion of depth, that generalises the one of ordinary occurrence
nets.

[depth] Let $O=(B,B^{\mathrm{p}},E,\gamma_{0},\gamma_{1},v_{0})$ be an
occurrence p-net. We define the _depth_ of events and conditions as

$\displaystyle 0pt{e}$ $\displaystyle=$ $\displaystyle 1+\max\\{0pt{b}\mid
b\in{\rm Phys.~{}Rev.~{}E}{e}\\}$ $\displaystyle 0pt{b}$ $\displaystyle=$
$\displaystyle\left\\{\begin{array}[]{lcl}0&&\mbox{if $b\in v_{0}$}\\\
\min\\{0pt{e}\mid e\in{\rm
Phys.~{}Rev.~{}E}{b}\\}&&\mbox{otherwise}\end{array}\right.$

We introduce a notion of configuration for occurrence p-nets that is intended
to capture the concept of a (concurrent) computation.

[configuration of occurrence p-nets] Let
$O=(B,B^{\mathrm{p}},E,\gamma_{0},\gamma_{1},v_{0})$ be an occurrence p-net. A
configuration is a set of events $C\subseteq E$ such that each $e\in C$ admits
a securing sequence in $C$ and for all $e,e^{\prime}\in C$,
$\neg(e\\#_{N}e^{\prime})$. We denote by $\mathit{Conf}({O})$ the set of
configurations of $O$.

The configurations of the net in Figure 3 (left) occur on the right, ordered
by inclusion.

We next prove that configurations can be interpreted as representations of
classes of firing sequences where the order of independent firings is
abstracted.

######  Lemma 9 (configurations are executions).

Let $O=(B,B^{\mathrm{p}},E,\gamma_{0},\gamma_{1},v_{0})$ be an occurrence
p-net. Then the following statements are equivalent

  1. (1)

$C\in\mathit{Conf}({O})$ is a finite configuration;

  2. (2)

there exists a securing sequence of events $e_{1},\ldots,e_{n}$ such that
$C=\\{e_{1},\ldots,e_{n}\\}$;

  3. (3)

there exists a firing sequence $v_{0}[{e_{1}}\rangle
v_{1}[{e_{2}}\rangle\ldots[{e_{n}}\rangle v_{n}$ such that
$C=\\{e_{1},\ldots,e_{n}\\}$ and
$v_{n}=(v_{0}\cup\bigcup_{i=1}^{n}{e_{i}}{{}^{\bullet}})\ominus(\bigcup_{i=1}^{n}{\rm
Phys.~{}Rev.~{}E}{e_{i}})$.

######  Proof 4.1.

($1\leftrightarrow 2$) Let $C\in\mathit{Conf}({O})$ be a finite configuration.
We prove the result by induction on $|C|$. The base case $|C|=0$ is trivial.
If $|C|=n+1$ for some $n\in{\rm Nature}$, then for each $e\in C$ fix a single
securing sequence of minimal length $s_{e}=e_{1},\ldots,e_{k},e$ in $C$, which
exists by definition of configuration, and call $S=\\{s_{e}\mid e\in C\\}$ the
set of such securing sequences. Let $\hat{s}_{\hat{e}}\in S$ be one of such
sequences of maximal length in $S$, with $\hat{e}$ as last event. Clearly
$C^{\prime}=C\setminus\\{\hat{e}\\}$ is again a configuration because its
events are not in conflict (as they are in $C$) and for each $e\in C^{\prime}$
the securing sequence $s_{e}\in S$ consists of events in $C^{\prime}$ only,
otherwise the minimality of $\hat{s}_{\hat{e}}$ as a securing sequence for
$\hat{e}$ in $C$ would be violated. Then, by inductive hypothesis, there
exists a securing sequence $e_{1}\ldots e_{n}$ such that
$C^{\prime}=\\{e_{1},\ldots,e_{n}\\}$. It is immediate to see that
$e_{1},\ldots,e_{n},\hat{e}$ is the desired securing sequence for $C$.

The converse implication is immediate, just observing that securing sequences
are closed by prefix and conflict free.

($2\leftrightarrow 3$) Assume that there is a securing sequence
$e_{1},\ldots,e_{n}$ such that $C=\\{e_{1},\ldots,e_{n}\\}$. We proceed by
induction on $n$. The base case $n=0$ is trivial. For $n>0$, we know, by
inductive hypothesis that there exists a firing sequence $v_{0}[{e_{1}}\rangle
v_{1}[{e_{2}}\rangle\ldots[{e_{n-1}}\rangle v_{n-1}$ and
$v_{n-1}=(v_{0}\cup\bigcup_{i=1}^{n-1}{e_{i}}{{}^{\bullet}})\ominus(\bigcup_{i=1}^{n-1}{\rm
Phys.~{}Rev.~{}E}{e_{i}})$. By definition of securing sequence,
$\\{e_{1},\ldots,e_{n-1}\\}\vdash e_{n}$, we know that for all $b\in{\rm
Phys.~{}Rev.~{}E}{e_{n}}$ either $b\in v_{0}$ or there exists $i<n$ such that
$b\in{e_{i}}{{}^{\bullet}}$. Moreover, for all $i<n$, if $b\in{\rm
Phys.~{}Rev.~{}E}{e_{n}}\cap B^{\mathrm{n}}$, certainly $b\not\in{\rm
Phys.~{}Rev.~{}E}{e_{i}}$, otherwise we would have $e_{i}\\#e_{n}$. This
allows us to deduce that ${\rm Phys.~{}Rev.~{}E}{e_{n}}\subseteq v_{n}$. Hence
the firing sequence can be extended by $v_{n-1}[{e_{n}}\rangle v_{n}$, where
$v_{n}=(v_{n-1}\cup{e_{n}}{{}^{\bullet}})\ominus{\rm
Phys.~{}Rev.~{}E}{e_{n}}=(v_{0}\cup\bigcup_{i=1}^{n}{e_{i}}{{}^{\bullet}})\ominus(\bigcup_{i=1}^{n}{\rm
Phys.~{}Rev.~{}E}{e_{i}})$.

For the converse implication, let us start showing by induction on $n$ that if
$C=\\{e_{1},\ldots,e_{n}\\}$ is the set of events of a given firing sequence,
then

there cannot be $i,j\in[{1},{n}]$ such that $i\not=j$ and ${\rm
Phys.~{}Rev.~{}E}{e_{i}}\cap{\rm Phys.~{}Rev.~{}E}{e_{j}}\cap
B^{\mathrm{n}}\not=\emptyset$. (2)

For $n\leq 1$ the statement is trivial. Let $n>1$ and assume, by
contradiction, that there is a non-persistent place $b\in{\rm
Phys.~{}Rev.~{}E}{e_{n}}\cap{\rm Phys.~{}Rev.~{}E}{e_{i}}\cap B^{\mathrm{n}}$,
for $i<n$. Clearly $b\not\in v_{0}$, otherwise ${\rm
Phys.~{}Rev.~{}E}{b}=\emptyset$ and after the firing of $e_{i}$ there would be
no way of generating the token in $b$. Therefore ${\rm
Phys.~{}Rev.~{}E}{b}\neq\emptyset$. Let $e\in{\rm Phys.~{}Rev.~{}E}{b}$ be the
only event generating a token in $b$. Then necessarily there are $j<i$ and
$k<n$ such that $e_{j}=e_{k}=e$ and thus, since $O$ is t-restricted, ${\rm
Phys.~{}Rev.~{}E}{e_{j}}\cap{\rm Phys.~{}Rev.~{}E}{e_{k}}\cap
B^{\mathrm{n}}\not=\emptyset$, which is absurd because we assumed that the
statement holds for firing sequences shorter than $n$.

Now, by Definition 4.1 we have to show that (1) all events of $C$ are
distinct, (2) $\neg\\#C$, and (3) for all $i\in[{1},{n}]$, $\\{e_{1}\ldots
e_{i-1}\\}\vdash e_{i}$. Point (1) follows from (2) and t-restrictedness. For
(3), suppose by absurd that $\\{e_{1}\ldots e_{i-1}\\}\not\vdash e_{i}$ for
some $i\in[{1},{n}]$. Thus there is a place $b\in{\rm
Phys.~{}Rev.~{}E}{e_{i}}$ such that $b\not\in v_{0}$ and
$b\not\in{e_{j}}{{}^{\bullet}}$ for all $j\in[{1},{i-1}]$, but this is
impossible because by assumption $e_{i}$ is enabled in $v_{i-1}$.

For (2) we proceed by induction on $n$, the base case $n=0$ being obvious.
Suppose by absurd that $\\#C$ holds, and let $k\in[{1},{n}]$ be the minimal
index such that $\\#\\{e_{1},\ldots,e_{k}\\}$. By this assumption we know that
$\neg\\#\\{e_{1},\ldots,e_{k-1}\\}$, thus by induction hypothesis that
$\\{e_{1},\ldots,e_{k-1}\\}$ is a securing sequence, and by the implication
($2\to 3$) already proved that $v_{0}[{e_{1}}\rangle
v_{1}[{e_{2}}\rangle\ldots[{e_{k-1}}\rangle v_{k-1}$ is a firing sequence and
$v_{k-1}=(v_{0}\cup\bigcup_{i=1}^{k-1}{e_{i}}{{}^{\bullet}})\ominus(\bigcup_{i=1}^{k-1}{\rm
Phys.~{}Rev.~{}E}{e_{i}})$.

Now, since $\\#\\{e_{1},\ldots,e_{k}\\}$, by the clauses defining conflict in
Definition 4.1 either (clause (a)) there is an event $e_{h}$ with
$h\in[{1},{k-1}]$ such that ${\rm Phys.~{}Rev.~{}E}{e_{h}}\cap{\rm
Phys.~{}Rev.~{}E}{e_{k}}\not\subseteq B^{\mathrm{p}}$, but this is impossible
by (2) above, or (clause (c)) w.l.o.g. there is a place $b\in{\rm
Phys.~{}Rev.~{}E}{e_{k}}$ such that $\\#\\{e_{1},\ldots,e_{k-1},b\\}$. Since
$e_{k}$ is enabled in $v_{k-1}$, certainly $b\in
v_{k-1}=(v_{0}\cup\bigcup_{i=1}^{k-1}{e_{i}}{{}^{\bullet}})\ominus(\bigcup_{i=1}^{k-1}{\rm
Phys.~{}Rev.~{}E}{e_{i}})$, and as it cannot belong to the initial marking,
$b\in{e_{j}}{{}^{\bullet}}$ for some $j\in[{1},{k-1}]$. But by (clause (b))
from $\\#\\{e_{1},\ldots,e_{k-1},b\\}$ we can infer
$\\#\\{e_{1},\ldots,e_{k-1},e_{j}\\}$ and thus $\\#\\{e_{1},\ldots,e_{k-1}\\}$
because $j\in[{1},{k-1}]$, which is absurd by the choice of $k$.

By the above result, it is meaningful to define the marking reached after a
configuration for occurrence p-nets.

[marking after a configuration] Let $O$ be an occurrence p-net. Given
$C\in\mathit{Conf}({O})$, the marking after $C$ is
$\mathit{m}({C})=(v_{0}\cup\bigcup_{e\in
C}{e}{{}^{\bullet}})\ominus(\bigcup_{e\in C}{\rm Phys.~{}Rev.~{}E}{e})$.

We next observe that all occurrence p-nets are safe.

######  Proposition 10 (occurrence p-nets are safe).

Let $O$ be an occurrence p-net. Then, for each firing sequence
$v_{0}[{e_{1}}\rangle v_{1}[{e_{2}}\rangle\ldots[{e_{n}}\rangle v_{n}$ all
markings $v_{i}$ are sets.

######  Proof 4.2.

By Lemma 9 we know that $\\{e_{1},\ldots,e_{i}\\}$ is a securing sequence,
thus all the events in it are pairwise distinct. The fact that all markings
are safe immediately follows recalling that for non-persistent places $|{\rm
Phys.~{}Rev.~{}E}{b}|\leq 1$, and for persistent places idempotency ensures
that at most one token is in the place.

We next introduce a notion of concurrency for occurrence p-nets that, as
anticipated, is based on non-binary conflict .

[concurrency] Let $O$ be an occurrence p-net. A subset of conditions
$X\subseteq B$ is called _concurrent_ , written $\mathit{co}({X})$, if
$\neg\\#X$ and for all $b,b^{\prime}\in X$ if $b<b^{\prime}$ then $b\in
B^{\mathrm{p}}$.

Concurrency, as in the case of ordinary nets, is intended to provide a
structural characterisation of coverability. This is formalised below in Lemma
11. Quite intuitively, a concurrent set of conditions cannot include
conflicts. Note, instead, that causal dependencies from persistent places are
admitted, consistently with the fact that using a token in a persistent place
does not consume such token.

######  Lemma 11 (coverability vs concurrency).

Let $O$ be an occurrence p-net and $X\subseteq B$. Then $X$ is concurrent iff
there is a reachable marking that covers $X$.

######  Proof 4.3.

$(\Rightarrow)$ Let $\mathit{co}({X})$. In order to prove that $X$ is
coverable we proceed by induction on the pairs
$h_{X}=\langle\mathit{md}({X}),\mathit{\\#md}({X})\rangle$ where
$\mathit{md}({X})=max\\{0pt{b}\mid{b\in X}\\}$, and
$\mathit{\\#md}({X})=|\\{b\in X\mid 0pt{b}=\mathit{md}({X})\\}|$, ordered by
$\langle n,m\rangle<\langle n^{\prime},m^{\prime}\rangle$ if $n<n^{\prime}$ or
$n=n^{\prime}\wedge m<m^{\prime}$.

If $h_{X}=\langle 0,\\_\rangle$ then $X\subseteq v_{0}$, hence we conclude
immediately. If $\mathit{md}({X})>0$, take a condition $b\in X$ such that
$0pt{b}$ is maximal. Note that there must be $e\in{\rm Phys.~{}Rev.~{}E}{b}$
such that $Y=(X\setminus{e}{{}^{\bullet}})\cup{\rm Phys.~{}Rev.~{}E}{e}$ is
still concurrent, otherwise either $b$ would not be of maximal depth or, by
the rules defining conflict, $\\#X$. Clearly $h_{Y}<h_{X}$ hence, by inductive
hypothesis, $Y$ is coverable and we can conclude that $X$ is coverable.

$(\Leftarrow)$ We show that any reachable marking is concurrent. Since any
subset of a concurrent set is concurrent this allows us immediately to
conclude. Consider a firing sequence $v_{0}[{e_{1}}\rangle
v_{1}[{e_{2}}\rangle\ldots[{e_{n}}\rangle v_{n}$. We show by induction on $n$
that $\mathit{co}({v_{n}})$. For the base case we just need to observe that
$\mathit{co}({v_{0}})$, i.e., the initial marking is clearly concurrent. When
$n>0$, by inductive hypothesis we know that $\mathit{co}({v_{n-1}})$. This
allows us to deduce that also $v_{n}=(v_{n-1}\ominus{\rm
Phys.~{}Rev.~{}E}{e_{n}})\oplus{e_{n}}{{}^{\bullet}}$ is concurrent.

For instance, consider the occurrence p-net in Figure 2a. We already observed
that $\\#\\{p,q,r\\}$ and indeed such set is not coverable. Instead, each pair
of conditions in $\\{p,q,r\\}$ is concurrent and thus coverable. Interestingly
enough, this shows that differently from what happens for ordinary occurrence
nets, pairwise coverability does not imply coverability.

We can now show that morphisms of occurrence p-nets preserve concurrency.

######  Lemma 12 (morphisms preserve concurrency).

Let $f:O\to O^{\prime}$ be a morphism of occurrence p-nets and $X\subseteq B$.
If $\mathit{co}({X})$ then $\mathit{co}({f_{\mathrm{s}}(X)})$.

######  Proof 4.4.

Since morphisms are simulations (see Lemma 8) they preserve coverability. By
Lemma 11, coverability is the same as concurrency. Hence $\mathit{co}({X})$
implies $\mathit{co}({f_{\mathrm{s}}(X)})$.

###  4.2. Occurrence p-nets with equivalence

We now introduce the notion of occurrence p-net with equivalence, which will
be the target of the pre-unfolding construction. The intuition is that, in an
occurrence p-net with equivalence, occurrences of items that depend on
different disjunctive causes are kept separate, but related by the
equivalence. This is technically useful in the development of the unfolding
construction.

Let $A$ be a set and ${\sim}\subseteq A\times A$ an equivalence relation on
$A$. Given $x\in A$ we write $[{x}]_{\scriptscriptstyle{\sim}}=\\{y\in A\mid
x\sim y\\}$ for the equivalence class of $x$. Moreover, given $X\subseteq A$
we write $[{X}]_{\scriptscriptstyle{\sim}}$ for the set
$\\{[{x}]_{\scriptscriptstyle{\sim}}\mid x\in X\\}$.

Given two subsets $X,Y\subseteq A$ we write $X\sim Y$ instead of
$[{X}]_{\scriptscriptstyle{\sim}}=[{Y}]_{\scriptscriptstyle{\sim}}$. Should
the equivalence be used (as it will always be the case) for sets $X$ and $Y$
each consisting of pairwise non-equivalent elements, from $X\sim Y$ it follows
that there is a bijection from $X$ to $Y$ mapping each element $x\in X$ to the
only $y\in Y$ such that $x\sim y$. If moreover $A$ is partially ordered by
$\leq$, we write $X\leq Y$ if for all $x\in X$, $y\in Y$ we have $x\leq y$.
The notation will be used only for $|X|\leq 1$. Observe that $\emptyset\leq Y$
trivially holds, while $\\{x\\}\leq Y$ reduces to $x\leq y$ for all $y\in Y$.

[occurrence p-net with equivalence] An occurrence p-net with equivalence is a
pair $\langle O,\sim\rangle$ where
$O=(B,B^{\mathrm{p}},E,\gamma_{0},\gamma_{1},v_{0})$ is an occurrence p-net
without backward conflicts and ${\sim}\subseteq(B\times B)\cup(E\times E)$ is
an equivalence such that

  1. (1)

for all $b,b^{\prime}\in B$ with $b\sim b^{\prime}$

    1. (a)

either $b,b^{\prime}\in B^{\mathrm{p}}$ or $b,b^{\prime}\in B^{\mathrm{n}}$;

    2. (b)

if $b\neq b^{\prime}$ then $\neg({\rm Phys.~{}Rev.~{}E}{b}\leq{\rm
Phys.~{}Rev.~{}E}{b^{\prime}})$ and $\\{b,b^{\prime}\\}\not\subseteq{\rm
Phys.~{}Rev.~{}E}{e}$ for all $e\in E$;

    3. (c)

if $b,b^{\prime}\in B^{\mathrm{n}}$ then ${\rm Phys.~{}Rev.~{}E}{b}\sim{\rm
Phys.~{}Rev.~{}E}{b^{\prime}}$;

    4. (d)

if $b,b^{\prime}\in B^{\mathrm{p}}$ then either ${\rm
Phys.~{}Rev.~{}E}{b}\sim{\rm Phys.~{}Rev.~{}E}{b^{\prime}}$ or
$b\,(\sim\setminus~{}\\#)^{*}\,b^{\prime}$;

  2. (2)

for all $e,e^{\prime}\in E$, if $e\sim e^{\prime}$ and $e\neq e^{\prime}$ then
${\rm Phys.~{}Rev.~{}E}{e}\sim{\rm Phys.~{}Rev.~{}E}{e^{\prime}}$, ${\rm
Phys.~{}Rev.~{}E}{e}\neq{\rm Phys.~{}Rev.~{}E}{e^{\prime}}$, and
${e}{{}^{\bullet}}\sim{e^{\prime}}{{}^{\bullet}}$;

  3. (3)

for all $X,X^{\prime}\subseteq B$, if $X\sim X^{\prime}$ then $\\{e\mid{\rm
Phys.~{}Rev.~{}E}{e}=X\\}\sim\\{e^{\prime}\mid{\rm
Phys.~{}Rev.~{}E}{e^{\prime}}=X^{\prime}\\}$.

In words, an occurrence p-net with equivalence is an occurrence p-net where
the absence of backward conflicts implies that each item has a uniquely
determined causal history. The possibility of joining the different histories
of tokens in persistent places is captured by an equivalence that can equate
persistent places. Events are equated when they have equivalent pre-sets and,
in turn, this implies that also their post-sets are equivalent.

More precisely, by condition (1a) equivalence respects the sort of places: two
equivalent places are either both non-persistent or both persistent. By the
second part of condition (1b) the pre-set of each event consists of pairwise
non-equivalent places. The first part is slightly more complex. First note
that whenever $b\in v_{0}$, i.e. ${\rm Phys.~{}Rev.~{}E}{b}=\emptyset$, the
inequality ${\rm Phys.~{}Rev.~{}E}{b}\leq{\rm Phys.~{}Rev.~{}E}{b^{\prime}}$
is trivially satisfied. Thus, places in the initial marking are not equivalent
to any other place and, in particular, the initial marking consists of
pairwise non-equivalent places. If instead ${\rm
Phys.~{}Rev.~{}E}{b}=\\{e\\}$, then $b$ cannot be equated to any place
$b^{\prime}$ caused by $e$. In particular, this implies that the places in the
post-set of each event are pairwise non-equivalent. More generally, this
condition plays a role in ensuring that the quotiented p-net is irredundant
(Definition 7). By condition (1c) non-persistent places can be equivalent only
when they are generated by equivalent events. Finally, condition (1d) states
that persistent places can be equivalent even if they are not generated by
equivalent events, but in this case they must be connected by a chain of
consistency in the equivalence class. This ensures that, once quotiented, the
pre-set of the condition will satisfy the connectedness condition (see
Definition 2).

Condition (2) says that events are equivalent only when they have equivalent
pre-sets and in this case they also have equivalent post-sets. Moreover,
equivalent events must differ in their pre-set.

Finally, by condition (3), whenever two sets of conditions $X,X^{\prime}$ are
equivalent then the sets of events having $X$ and $X^{\prime}$ as pre-sets are
equivalent. Note that since ${\rm Phys.~{}Rev.~{}E}{e}=X$, by condition (1b),
the set $X$ cannot contain equivalent conditions. The same applies to
$X^{\prime}$ and thus $X\sim X^{\prime}$ implies that there is a bijection
from $X$ to $X^{\prime}$ mapping each element $b_{1}\in X$ to the only
$b_{2}\in X^{\prime}$ such that $b_{1}\sim b_{2}$. Moreover, also the set
$\\{e\mid{\rm Phys.~{}Rev.~{}E}{e}=X\\}$ contains pairwise non-equivalent
events by condition (2). The same applies to $\\{e^{\prime}\mid{\rm
Phys.~{}Rev.~{}E}{e^{\prime}}=X^{\prime}\\}$, hence, also in this case, the
requirement $\\{e\mid{\rm Phys.~{}Rev.~{}E}{e}=X\\}\sim\\{e^{\prime}\mid{\rm
Phys.~{}Rev.~{}E}{e^{\prime}}=X^{\prime}\\}$ implies a one-to-one
correspondence between equivalent events.

An example of occurrence p-net with equivalence is in Figure 5, where
equivalent elements are linked by dotted lines.

$\textstyle{\bullet}$$\textstyle{\scriptstyle{p}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{q}}$$\textstyle{a}$$\textstyle{b}$
$\textstyle{\scriptstyle{o_{1}}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{r}}$
$\textstyle{\scriptstyle{o_{2}}}$$\textstyle{d_{1}}$$\textstyle{d_{2}}$ Figure
5. An occurrence p-net with equivalence

The fact that occurrence p-nets with equivalence do not have backward
conflicts allows us to restrict only to binary conflicts. Formally, the
following holds.

######  Lemma 13 (conflicts in occurrence p-nets with equivalence).

Let $\langle O,\sim\rangle$ be an occurrence p-net with equivalence and
$X\subseteq B\cup E$. Then $\\#X$ holds if and only if there are
$x,x^{\prime}\in X$ such that $x\\#x^{\prime}$.

######  Proof 4.5.

Straightforward using the definition of conflict (see Definition 4.1).

For occurrence p-nets with equivalence we will need a notion of concurrency on
sets of places stronger than that in Definition 4.2.

[strong concurrency] Let $\langle O,\sim\rangle$ be an occurrence p-net with
equivalence. A subset of conditions $X\subseteq B$ is _strongly concurrent_ ,
written $\mathit{sco}({X})$, if $\mathit{co}({X})$ and for all
$b,b^{\prime}\in X$, if $b\neq b^{\prime}$ then $\neg(b\sim b^{\prime})$.

The idea is that if a set of conditions is strongly concurrent it can be
produced by a computation using only a specific instance for each equivalence
class of persistent resources.

######  Lemma 14 (pre- and post-sets are strongly concurrent).

Let $\langle O,\sim\rangle$ be an occurrence p-net with equivalence. Then for
any $e\in E$ its pre-set ${\rm Phys.~{}Rev.~{}E}{e}$ and post-set
${e}{{}^{\bullet}}$ are strongly concurrent.

######  Proof 4.6.

Let $e\in E$ be an event of $O$. Then ${\rm Phys.~{}Rev.~{}E}{e}$ and
${e}{{}^{\bullet}}$ are concurrent since $O$ is an occurrence p-net, thus $e$
can be fired and hence pre- and post-sets of events are coverable, whence
concurrent by Lemma 11. They are also strongly concurrent, since, by
Definition 4.2, condition (1b), they cannot contain equivalent conditions.

Occurrence p-nets with equivalence can be turned into a category by
introducing a suitable notion of morphism.

[category of occurrence p-nets with equivalence] A morphism of occurrence
p-nets with equivalence $f:\langle O,\sim\rangle\to\langle
O^{\prime},\sim^{\prime}\rangle$ is a morphism $f:O\to O^{\prime}$ of p-nets
such that for all $b_{1},b_{2}\in B$, if $b_{1}\sim b_{2}$ then
$f_{\mathrm{s}}(b_{1})\sim^{\prime}f_{\mathrm{s}}(b_{2})$. We denote by
$\mathsf{OE}$ the category of occurrence p-nets with equivalence.

In words, a morphism of occurrence p-nets is required to preserve the
equivalence. This is essential to ensure that it induces a function on the
quotient nets.

[quotient of an occurrence p-net with equivalence] Let $\langle O,\sim\rangle$
be an occurrence p-net with equivalence. Its _quotient_ is the structure

$\mathcal{Q}({\langle
O,\sim\rangle})=([{B}]_{\scriptscriptstyle{\sim}},[{B^{\mathrm{p}}}]_{\scriptscriptstyle{\sim}},[{E}]_{\scriptscriptstyle{\sim}},\gamma_{0}^{\sim},\gamma_{1}^{\sim},[{v_{0}}]_{\scriptscriptstyle{\sim}})$

where
$\gamma_{j}^{\sim}([{e}]_{\scriptscriptstyle{\sim}})=[{\gamma_{j}(e)}]_{\scriptscriptstyle{\sim}}$
for $j\in\\{0,1\\}$.

The quotient of the net in Figure 5 is depicted in Figure 6. Note that the
quotient has introduced a backward conflict on the place $o$.

$\textstyle{\bullet}$$\textstyle{\scriptstyle{p}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{q}}$$\textstyle{a}$$\textstyle{b}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{r}}$
$\textstyle{\scriptstyle{o}}$$\textstyle{d}$ Figure 6. The quotient of the
occurrence p-net with equivalence in Figure 5

We want to show that the quotient of an occurrence p-net with equivalence is
indeed an occurrence p-net. To this aim we first observe some facts.

######  Lemma 15 (properties of the quotient).

Let $\langle O,\sim\rangle$ be an occurrence p-net with equivalence and
$\mathcal{Q}({\langle O,\sim\rangle})$ the corresponding quotient. Then

  1. (1)

for all $b\in B^{\mathrm{n}}$, ${\rm
Phys.~{}Rev.~{}E}{[{b}]_{\scriptscriptstyle{\sim}}}=[{{\rm
Phys.~{}Rev.~{}E}{b}}]_{\scriptscriptstyle{\sim}}$;

  2. (2)

for all $b\in B^{\mathrm{p}}$, ${\rm
Phys.~{}Rev.~{}E}{[{b}]_{\scriptscriptstyle{\sim}}}=[{\bigcup_{b^{\prime}\sim
b}{\rm Phys.~{}Rev.~{}E}{b^{\prime}}}]_{\scriptscriptstyle{\sim}}$;

  3. (3)

for all $e\in E$, ${\rm
Phys.~{}Rev.~{}E}{[{e}]_{\scriptscriptstyle{\sim}}}=[{{\rm
Phys.~{}Rev.~{}E}{e}}]_{\scriptscriptstyle{\sim}}$ and
${[{e}]_{\scriptscriptstyle{\sim}}}{{}^{\bullet}}=[{{e}{{}^{\bullet}}}]_{\scriptscriptstyle{\sim}}$;

  4. (4)

for all $X\subseteq E$ and $e\in E$, if $X\vdash e$ then
$[{X}]_{\scriptscriptstyle{\sim}}\vdash[{e}]_{\scriptscriptstyle{\sim}}$;

  5. (5)

for all $e,e^{\prime}\in E$, if $e\sim e^{\prime}$ and $e\not=e^{\prime}$ then
$e\\#e^{\prime}$;

  6. (6)

for all $e,e^{\prime}\in E$, if
$[{e}]_{\scriptscriptstyle{\sim}}\\#[{e^{\prime}}]_{\scriptscriptstyle{\sim}}$
then $e\\#e^{\prime}$.

######  Proof 4.7.

The proofs are mostly routine.

For point (1) observe that, by Definition 4.2(1c), if $b,b^{\prime}\in
B^{\mathrm{n}}$ then ${\rm Phys.~{}Rev.~{}E}{b}\sim{\rm
Phys.~{}Rev.~{}E}{b^{\prime}}$. Point (2) is just a consequence of the
definition of quotient. For point (3) observe that, by definition, if $e\sim
e^{\prime}$ then ${\rm Phys.~{}Rev.~{}E}{e}\sim{\rm
Phys.~{}Rev.~{}E}{e^{\prime}}$ and
${e}{{}^{\bullet}}\sim{e^{\prime}}{{}^{\bullet}}$.

Point (4) follows from the observation that, by (3), ${\rm
Phys.~{}Rev.~{}E}{[{e}]_{\scriptscriptstyle{\sim}}}=[{{\rm
Phys.~{}Rev.~{}E}{e}}]_{\scriptscriptstyle{\sim}}$. Moreover, for all
$b\in{\rm Phys.~{}Rev.~{}E}{e}$, if $b\in v_{0}$ then
$[{b}]_{\scriptscriptstyle{\sim}}\in[{v_{0}}]_{\scriptscriptstyle{\sim}}$.
Otherwise, there is $e^{\prime}\in X$ such that
$b\in{e^{\prime}}{{}^{\bullet}}$ and thus, by (3),
$[{b}]_{\scriptscriptstyle{\sim}}\in{[{e^{\prime}}]_{\scriptscriptstyle{\sim}}}{{}^{\bullet}}$.

Concerning point (5), let $e\sim e^{\prime}$. Since in a p-net ${\rm
Phys.~{}Rev.~{}E}{e^{\prime}}\not\subseteq B^{\mathrm{p}}$, we can fix some
$b\in{\rm Phys.~{}Rev.~{}E}{e}\cap B^{\mathrm{n}}$. By definition of
occurrence p-net with equivalence (Definition 4.2(1c)), ${\rm
Phys.~{}Rev.~{}E}{e}\sim{\rm Phys.~{}Rev.~{}E}{e^{\prime}}$, hence there must
be $b^{\prime}\in{\rm Phys.~{}Rev.~{}E}{e^{\prime}}\cap B^{\mathrm{n}}$ such
that $b\sim b^{\prime}$. We proceed by induction on the depth $h$ of $e$. When
$h=0$, we have $b\in v_{0}$. Again, by Definition 4.2(1c), ${\rm
Phys.~{}Rev.~{}E}{b}\sim{\rm Phys.~{}Rev.~{}E}{b^{\prime}}$, and thus also
$b^{\prime}\in v_{0}$. Since $b\sim b^{\prime}$ we deduce that $b=b^{\prime}$
and thus $e\\#e^{\prime}$. If $h>0$, there are $e_{1}\in{\rm
Phys.~{}Rev.~{}E}{b}$ and $e_{1}^{\prime}\in{\rm
Phys.~{}Rev.~{}E}{b^{\prime}}$ and, since $b,b^{\prime}\in B^{\mathrm{n}}$, it
holds $e_{1}\sim e_{1}^{\prime}$. Hence by induction hypothesis
$e_{1}\\#e_{1}^{\prime}$ and thus $e\\#e^{\prime}$.

Finally, for point (6), we can proceed by induction on the derivation on rules
that define conflict (see Definition 4.1). Let
$[{e}]_{\scriptscriptstyle{\sim}}\\#[{e^{\prime}}]_{\scriptscriptstyle{\sim}}$.
If there is $[{b}]_{\scriptscriptstyle{\sim}}\in{\rm
Phys.~{}Rev.~{}E}{[{e}]_{\scriptscriptstyle{\sim}}}\cap{\rm
Phys.~{}Rev.~{}E}{[{e^{\prime}}]_{\scriptscriptstyle{\sim}}}\cap[{B^{\mathrm{n}}}]_{\scriptscriptstyle{\sim}}$
then we conclude by point (3) that $e\\#e^{\prime}$. If instead there are
$[{b}]_{\scriptscriptstyle{\sim}}\in{\rm
Phys.~{}Rev.~{}E}{[{e}]_{\scriptscriptstyle{\sim}}}=[{{\rm
Phys.~{}Rev.~{}E}{e}}]_{\scriptscriptstyle{\sim}}$ and
$[{b^{\prime}}]_{\scriptscriptstyle{\sim}}\in{\rm
Phys.~{}Rev.~{}E}{[{e^{\prime}}]_{\scriptscriptstyle{\sim}}}=[{{\rm
Phys.~{}Rev.~{}E}{e^{\prime}}}]_{\scriptscriptstyle{\sim}}$ with
$[{b}]_{\scriptscriptstyle{\sim}}\\#[{b^{\prime}}]_{\scriptscriptstyle{\sim}}$,
$b\in{\rm Phys.~{}Rev.~{}E}{e}$ and $b^{\prime}\in{\rm
Phys.~{}Rev.~{}E}{e^{\prime}}$ it means that for any
$[{e_{1}}]_{\scriptscriptstyle{\sim}}\in{\rm
Phys.~{}Rev.~{}E}{[{b}]_{\scriptscriptstyle{\sim}}}$ and any
$[{e_{2}}]_{\scriptscriptstyle{\sim}}\in{\rm
Phys.~{}Rev.~{}E}{[{b^{\prime}}]_{\scriptscriptstyle{\sim}}}$ we have
$[{e_{1}}]_{\scriptscriptstyle{\sim}}\\#[{e_{2}}]_{\scriptscriptstyle{\sim}}$.
In particular, for $e_{1}\in{\rm Phys.~{}Rev.~{}E}{b}$ and $e_{2}\in{\rm
Phys.~{}Rev.~{}E}{b^{\prime}}$ (that are uniquely determined as the underlying
occurrence p-net as no backward conflict) by inductive hypothesis we have
$e_{1}\\#e_{2}$ and thus $b\\#b^{\prime}$ and $e\\#e^{\prime}$.

We can now reach the desired conclusion.

######  Lemma 16 (quotient is an occurrence p-net).

Let $\langle O,\sim\rangle$ be an occurrence p-net with equivalence. Then
$\mathcal{Q}({\langle O,\sim\rangle})$ is an occurrence p-net.

######  Proof 4.8.

Easy consequence of Lemma 15. In particular, for any event $e\in E$, by Lemma
15(3) we have that ${\rm
Phys.~{}Rev.~{}E}{[{e}]_{\scriptscriptstyle{\sim}}}=[{{\rm
Phys.~{}Rev.~{}E}{e}}]_{\scriptscriptstyle{\sim}}$. Then connectedness follows
from Lemma 15(6). In order to conclude we have to observe that
$\mathcal{Q}({\langle O,\sim\rangle})$ is a well-formed p-net.
T-restrictedness follows immediately from t-restrictedness of $O$. Concerning
irredundancy, consider a generic persistent place in $\mathcal{Q}({\langle
O,\sim\rangle})$ that will be of the kind $[{b}]_{\scriptscriptstyle{\sim}}$
for $b\in B^{\mathrm{p}}$ and take any event
$[{e}]_{\scriptscriptstyle{\sim}}\in{\rm
Phys.~{}Rev.~{}E}{[{b}]_{\scriptscriptstyle{\sim}}}$. By Lemma 15(2), ${\rm
Phys.~{}Rev.~{}E}{[{b}]_{\scriptscriptstyle{\sim}}}=[{\bigcup_{b^{\prime}\sim
b}{\rm Phys.~{}Rev.~{}E}{b^{\prime}}}]_{\scriptscriptstyle{\sim}}$, hence we
can assume $e\in{\rm Phys.~{}Rev.~{}E}{b}$. In order to violate irredundancy,
there should exist $e^{\prime}\sim e$ and $b^{\prime}\sim b$ such that
$e^{\prime}\rightsquigarrow_{O}^{n}b^{\prime}$ with $n\geq 2$. It is easy to
see that this cannot happen thanks to conditions (1b) and (2) of Definition
4.2.

We can thus consider a quotient functor from the category of p-nets with
equivalence to the category of occurrence p-nets.

[quotient functor] We denote by $\mathcal{Q}({}):\mathsf{OE}\to\mathsf{ON}$
the functor taking an occurrence p-net with equivalence to its quotient.

The fact that the functor is well-defined on objects follows from Lemma 16. On
arrows it is immediate from the definition of morphism of occurrence net with
equivalence (Definition 4.6).

######  Lemma 17 (occurrence p-net with equivalence vs occurrence p-nets).

Let $\langle O,\sim\rangle$ be an occurrence p-net with equivalence. For any
finite configuration $C\in\mathit{Conf}({O})$,
$[{C}]_{\scriptscriptstyle{\sim}}\in\mathit{Conf}({\mathcal{Q}({O})})$ and
$\mathit{m}({[{C}]_{\scriptscriptstyle{\sim}}})=[{\mathit{m}({C})}]_{\scriptscriptstyle{\sim}}$.

######  Proof 4.9.

Immediate from Lemma 15, points (4) and (6).

###  4.3. Unfolding

As mentioned above, the first phase of the unfolding construction produces an
occurrence p-net with equivalence, which is then quotiented to an occurrence
p-net. We will use $\pi$ to denote the projection on the first component of a
pair, i.e., given sets $A$ and $B$, we let $\pi:A\times B\to A$ be defined as
$\pi(a,b)=a$ for all $(a,b)\in A\times B$.

[unfolding] Let $N=(S,S^{\mathrm{p}},T,\delta_{0},\delta_{1},u_{0})$ be a
p-net. Define the _pre-unfolding_
$\mathcal{U}^{pre}({N})=(B,B^{\mathrm{p}},E,\gamma_{0},\gamma_{1},v_{0})$ as
the least occurrence p-net with an equivalence $\sim_{N}$ on $B\cup E$ such
that

  * •

$v_{0}=\\{\langle s,\bot\rangle\mid s\in u_{0}\\}\subseteq B$

  * •

if $t\in T$ and $X\subseteq B$ such that $\mathit{sco}({X})$ and $\pi(X)={\rm
Phys.~{}Rev.~{}E}{t}$ then $e=\langle t,X\rangle\in E$, $Y=\\{\langle
s,e\rangle\mid s\in{t}{{}^{\bullet}}\\}\subseteq B$ and ${\rm
Phys.~{}Rev.~{}E}{e}=X$, ${e}{{}^{\bullet}}=Y$.

The equivalence $\sim_{N}$ is the least equivalence relation that satisfies

$\langle s,e\rangle\sim_{N}\langle s,e^{\prime}\rangle\lx@proof@logical@and
s\in S^{\mathrm{p}}\
e\stackrel{{\scriptstyle}}{{\frown}}_{N}e^{\prime}\quad\quad\langle
t,X\rangle\sim_{N}\langle t,X^{\prime}\rangle
X\sim_{N}X^{\prime}\quad\quad\langle s,e\rangle\sim_{N}\langle
s,e^{\prime}\rangle e\sim_{N}e^{\prime}$

The unfolding $\mathcal{U}({N})$ is obtained as the quotient
${\mathcal{U}^{pre}({N})}_{\scriptscriptstyle{\sim_{N}}}$ with the _folding
morphism_ $\varepsilon_{N}:\mathcal{U}({N})\to N$ defined as
$\varepsilon_{N}([{x}]_{\scriptscriptstyle{\sim_{N}}})=\pi(x)$.

Note that if the net $N$ does not contain persistent places, the equivalence
relation $\sim_{N}$ is just the identity relation, strong concurrency coincide
with concurrency and the pre-unfolding coincides with the ordinary unfolding.
Observe that $\varepsilon_{N}$ is injective on pre- and post-sets of
transitions, as implied by the definition of p-net morphism.

---
$\textstyle{\bullet}$$\textstyle{\scriptstyle{s}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{p}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{q}}$$\textstyle{a}$$\textstyle{b}$
$\textstyle{\scriptstyle{o_{1}}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{r_{1}}}$
$\textstyle{\scriptstyle{o_{2}}}$$\textstyle{e_{1}}$$\textstyle{d_{1}}$$\textstyle{c_{1}}$$\textstyle{d_{2}}$$\textstyle{e_{2}}$
$\textstyle{\scriptstyle{r_{2}}}$
$\textstyle{d_{3}}$$\textstyle{c_{2}}$$\textstyle{d_{4}}$
$\textstyle{\scriptstyle{r_{3}}}$
$\textstyle{d_{5}}$$\textstyle{c_{3}}$$\textstyle{d_{6}}$
$\textstyle{\scriptstyle{r_{4}}}$ Figure 7. Pre-unfolding of our running
example

As an example, consider the (fragment of the) pre-unfolding of our running
example in Figure 7, where we have used convenient names for places and
transitions in order to improve readability. Since $o_{1}$ and $o_{2}$ are
instances of the same persistent place $o$, they are related by the
equivalence. Then $\\{o_{1},r_{1}\\}\sim\\{o_{2},r_{1}\\}$ and
$\\{o_{1},s\\}\sim\\{o_{2},s\\}$, thus $d_{1}\sim d_{2}$ and $e_{1}\sim e_{2}$
and the equivalence is propagated to their post-sets. The same pattern is
iterated for any instance of $r$ created by the subsequent firing of (the
instances of) $c$. The corresponding unfolding is obtained as the quotient in
Figure 8.

For the p-net in Figure 4 (left), the pre-unfolding is the occurrence p-net in
Figure 4 (right). Note that $o_{1}$ and $o_{2}$ are not equivalent since their
generating events are in conflict and are not connected by a chain of
consistency. Since $\sim_{N}$ here is the identity, the unfolding coincides
with the pre-unfolding.

---
$\textstyle{\bullet}$$\textstyle{\scriptstyle{s}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{p}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{q}}$$\textstyle{a}$$\textstyle{b}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{r_{1}}}$
$\textstyle{\scriptstyle{o_{2}}}$$\textstyle{c_{1}}$$\textstyle{d_{2}}$$\textstyle{e_{2}}$
$\textstyle{\scriptstyle{r_{2}}}$ $\textstyle{c_{2}}$$\textstyle{d_{4}}$
$\textstyle{\scriptstyle{r_{3}}}$ $\textstyle{c_{3}}$$\textstyle{d_{6}}$
$\textstyle{\scriptstyle{r_{4}}}$ Figure 8. Unfolding of our running example

We can consider the inclusion functor
$\mathcal{I}({}):\mathsf{ON}\to\mathsf{PN}$ that acts as identity on objects
and morphisms. We next observe that the unfolding $\mathcal{U}({N})$ and the
folding morphism $\varepsilon_{N}$ are cofree over $N$. Therefore
$\mathcal{U}({})$ extends to a functor that is right adjoint of
$\mathcal{I}({})$ and establishes a coreflection between $\mathsf{PN}$ and
$\mathsf{ON}$.

It is easy to show that the pre-unfolding is an occurrence p-net with
equivalence.

######  Lemma 18 (pre-unfolding is an occurrence p-net with equivalence).

Let $N$ be a p-net. Then $\langle\mathcal{U}^{pre}({N}),\sim_{N}\rangle$ is an
occurrence p-net with equivalence.

######  Proof 4.10.

The fact that $\langle\mathcal{U}^{pre}({N}),\sim_{N}\rangle$ satisfies the
properties in Definition 4.2 follows almost directly by construction. The less
immediate property is (1b), specifically the fact that if $b\neq b^{\prime}$
then $\neg({\rm Phys.~{}Rev.~{}E}{b}\leq{\rm Phys.~{}Rev.~{}E}{b^{\prime}})$.
This is a consequence of the fact that if $e\sim e^{\prime}$ and $e\neq
e^{\prime}$ then $e\\#e^{\prime}$.

As a preliminary step we show that the pre-unfolding construction
$\mathcal{U}^{pre}({})$ extends to a functor that, together with the quotient
functor $\mathcal{Q}({})$, establishes an equivalence between the categories
$\mathsf{ON}$ and $\mathsf{OE}$.

######  Lemma 19 (mapping from the pre-unfolding).

Let $O$ be an occurrence p-net and $\pi:\mathcal{U}^{pre}({O})\to O$ the
mapping from the pre-unfolding. Then

  1. (1)

for all finite $C\in\mathit{Conf}({O})$ there exists
$C^{\prime}\in\mathit{Conf}({\mathcal{U}^{pre}({O})})$ such that
$\pi(C^{\prime})=C$ and $\mathit{m}({C})=\pi(\mathit{m}({C^{\prime}}))$;

  2. (2)

for all
$C^{\prime},C^{\prime\prime}\in\mathit{Conf}({\mathcal{U}^{pre}({O})})$, if
$\pi(C^{\prime})=\pi(C^{\prime\prime})$ then
$C^{\prime}\sim_{N}C^{\prime\prime}$.

######  Proof 4.11.

Point (1) can be shown by induction on $|C|$. The base case $|C|=0$ is
trivial. If $|C|=n>0$, by Lemma 9, we have $C=\\{e_{1},\ldots,e_{n}\\}$ and
there is a firing sequence $v_{0}[{e_{1}}\rangle
v_{1}[{e_{2}}\rangle\ldots[{e_{n}}\rangle v_{n}$. By the same lemma
$C_{1}=\\{e_{1},\ldots,e_{n-1}\\}$ is a configuration of $O$. Hence by
inductive hypothesis there exists a configuration
$C_{1}^{\prime}\in\mathit{Conf}({\mathcal{U}^{pre}({O})})$ such that
$\pi(C_{1}^{\prime})=C_{1}$ and
$v_{n}=\mathit{m}({C_{1}})=\pi(\mathit{m}({C_{1}^{\prime}}))$ and
$\mathit{co}({\mathit{m}({C_{1}^{\prime}})})$. Since ${\rm
Phys.~{}Rev.~{}E}{e_{n}}\subseteq v_{n-1}$, by definition of
$\mathcal{U}^{pre}({})$ there is an event $e_{n}^{\prime}=\langle
e_{n},X\rangle$, where $X\subseteq v_{n-1}$ is such that $\mathit{sco}({X})$
and $\pi(X)={\rm Phys.~{}Rev.~{}E}{e_{n}}$. Note that we can always choose $X$
such that $\mathit{sco}({X})$ since equivalent conditions have the same
$\pi$-image. If we define $C^{\prime}=C_{1}\cup\\{e_{n}^{\prime}\\}$, we have
that $\pi(C^{\prime})=C$.

Point (2) can be proved by an easy induction on $|C^{\prime}|$.

######  Proposition 20 (equivalence).

The categories $\mathsf{ON}$ and $\mathsf{OE}$ are equivalent via the functors
$\mathcal{Q}({})$ and $\mathcal{U}^{pre}({})$.

######  Proof 4.12.

Let us first observe that, on objects, the functors are inverse of each other.
First, for an occurrence p-net $O$ let us define
$q:\mathcal{Q}({\mathcal{U}^{pre}({O})})\to O$ by letting
$q([{x}]_{\scriptscriptstyle{\sim}})=\pi(x)$.

In order to show that $q$ is an isomorphism we resort to Lemma 19. By (1) we
can show that $q$ is surjective. In fact, for each event $e$ in $O$ there is
$e^{\prime}$ in $\mathcal{U}^{pre}({O})$ such that $\pi(e^{\prime})=e$. Hence
$q([{e^{\prime}}]_{\scriptscriptstyle{\sim}})=e$. Moreover, it is injective,
since by (2) it follows that if
$q([{x}]_{\scriptscriptstyle{\sim}})=q([{y}]_{\scriptscriptstyle{\sim}})$ then
$x\sim y$.

For the converse, define $\epsilon:\mathcal{U}^{pre}({\mathcal{Q}({\langle
O,\sim\rangle})})\to\langle O,\sim\rangle$ inductively as follows.

The initial marking of $\mathcal{U}^{pre}({\mathcal{Q}({O,\sim\rangle})})$
consists of the places
$b^{\prime}=\langle[{b}]_{\scriptscriptstyle{\sim}},\bot\rangle$ with $b\in
v_{0}$. We define $\epsilon(b^{\prime})=b$.

For the inductive step, consider an event
$e^{\prime}=\langle[{e}]_{\scriptscriptstyle{\sim}},X^{\prime}\rangle$ where
$[{e}]_{\scriptscriptstyle{\sim}}$ is an event in $\mathcal{Q}({\langle
O,\sim\rangle})$ and $X^{\prime}\subseteq B^{\prime}$ such that
$\mathit{sco}({X})$ and $\pi(X)={\rm
Phys.~{}Rev.~{}E}{[{e}]_{\scriptscriptstyle{\sim}}}$. Since $X$ is strongly
concurrent and $\epsilon$ preserves strong concurrency (Lemma 12), we have
that $\epsilon(X)$ is strong concurrent. Moreover, by Lemma 15(3) we have
$\pi(X)={\rm Phys.~{}Rev.~{}E}{[{e}]_{\scriptscriptstyle{\sim}}}=[{{\rm
Phys.~{}Rev.~{}E}{e}}]_{\scriptscriptstyle{\sim}}$. Hence $\epsilon(X)\sim{\rm
Phys.~{}Rev.~{}E}{e}$ and therefore, by definition of occurrence p-net with
equivalence, there exists a unique $e_{1}$ in $O$ such that $e_{1}\sim e$ and
${\rm Phys.~{}Rev.~{}E}{e_{1}}=\epsilon(X)$. It exists by Definition 4.2(3)
and it is unique by Definition 4.2(2). We define $\epsilon(e^{\prime})=e_{1}$.
Finally, $\epsilon$ is extended to ${e^{\prime}}{{}^{\bullet}}$ by letting
$\epsilon(\langle b,e^{\prime}\rangle)=b_{1}$, where
$b_{1}\in{e_{1}}{{}^{\bullet}}$ is the unique condition in
${e_{1}}{{}^{\bullet}}$ such that $b_{1}\sim b$. In this way
$\epsilon({e^{\prime}}{{}^{\bullet}})={e_{1}}{{}^{\bullet}}$.

It is easy to see that $\epsilon$ is injective. Surjectivity follows from
Lemma 17.

We finally show that for any occurrence p-net $O$, for any occurrence p-net
with equivalence $\langle O^{\prime},\sim\rangle$ and for any morphism
$f:\mathcal{Q}({\langle O^{\prime},\sim\rangle})\to O$ there exists a unique
morphism $h:\langle O^{\prime},\sim\rangle\to\mathcal{U}^{pre}({O})$ such that
the following diagram commutes

---
$\textstyle{{\mathcal{Q}({\mathcal{U}^{pre}({O})})}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\varepsilon_{O}}$$\textstyle{{O}}$$\textstyle{{\mathcal{Q}({\langle
O^{\prime},\sim\rangle})}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathcal{Q}({h})}$$\scriptstyle{f}$

We define $h$ by induction on the depth $k$ of the items.

$\mathsf{(k=0)}$ Only conditions in the initial marking have depth $0$. Let
$b^{\prime}\in B^{\prime}$ with $0pt{b^{\prime}}=0$. Hence $b^{\prime}\in
v_{0}^{\prime}$ and thus $[{b^{\prime}}]_{\scriptscriptstyle{\sim}}$ is in the
initial marking of $\mathcal{Q}({\langle O^{\prime},\sim\rangle})$. Therefore
$f_{\mathrm{s}}([{b^{\prime}}]_{\scriptscriptstyle{\sim}})=b\in v_{0}$ and we
can define $h_{\mathrm{s}}(b^{\prime})=\langle b,\bot\rangle$, which is in the
initial marking of $\mathcal{U}^{pre}({O})$.

$\mathsf{(k>0)}$ Let $e^{\prime}\in E^{\prime}$ be an event such that
$0pt{e^{\prime}}=k>0$. Therefore conditions in ${\rm
Phys.~{}Rev.~{}E}{e^{\prime}}$ have depth less than $k$. Hence their
$h$-images have been already defined. Moreover, since ${\rm
Phys.~{}Rev.~{}E}{e^{\prime}}$ is concurrent, by Lemma 12, also
$h_{\mathrm{s}}({\rm Phys.~{}Rev.~{}E}{e^{\prime}})$ is. Moreover, on pre-sets
morphisms preserve equivalence, hence $h$ is injective on ${\rm
Phys.~{}Rev.~{}E}{e^{\prime}}$ and $h_{\mathrm{s}}({\rm
Phys.~{}Rev.~{}E}{e^{\prime}})$ does not include equivalent conditions, hence
$\mathit{sco}({h_{\mathrm{s}}({\rm Phys.~{}Rev.~{}E}{e^{\prime}})})$.
Therefore the unfolding contains an event $e=\langle
f_{\mathrm{t}}(e^{\prime}),h_{\mathrm{s}}({\rm
Phys.~{}Rev.~{}E}{e^{\prime}})\rangle$ and we define
$h_{\mathrm{t}}(e^{\prime})=e$. The mapping is then extended to the post-set
of $e^{\prime}$ by defining, for each $b\in{e^{\prime}}{{}^{\bullet}}$,
$h_{\mathrm{s}}(b)=\langle
f_{\mathrm{s}}([{b}]_{\scriptscriptstyle{\sim}}),e\rangle$.

Uniqueness follows by noticing that at each level we were forced to define $h$
as we did to ensure commutativity.

We can finally prove the desired theorem, by showing that
$\mathcal{U}^{pre}({}):\mathsf{PN}\to\mathsf{OE}$ is right adjoint to
$\mathcal{Q}({}):\mathsf{OE}\to\mathsf{PN}$.

######  Proposition 21.

$\mathcal{Q}({})\dashv\mathcal{U}^{pre}({})$

######  Proof 4.13.

Let $N=(S,S^{\mathrm{p}},T,\delta_{0},\delta_{1},u_{0})$ be a p-net, let
$\mathcal{U}^{pre}({N})=\langle O,\sim_{N}\rangle$ be its pre-unfolding with
$O=\langle B,B^{\mathrm{p}},E,\gamma_{0},\gamma_{1},v_{0}\rangle$, and let
$\varepsilon_{N}:\mathcal{Q}({\mathcal{U}^{pre}({N})})\to N$ be the folding
morphism. We have to show that for any occurrence p-net with equivalence
$\langle O^{\prime},\sim\rangle$ with $O^{\prime}=\langle
B^{\prime},B^{\prime\mathrm{p}},E^{\prime},\gamma_{0}^{\prime},\gamma_{1}^{\prime},v_{0}^{\prime}\rangle$
and for any morphism $f:\mathcal{Q}({\langle O^{\prime},\sim\rangle})\to N$
there exists a unique morphism $h:\langle
O^{\prime},\sim\rangle\to\mathcal{U}^{pre}({N})$ such that the following
diagram commutes:

---
$\textstyle{{\mathcal{Q}({\mathcal{U}^{pre}({N})})}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\varepsilon_{N}}$$\textstyle{{N}}$$\textstyle{{\mathcal{Q}({\langle
O^{\prime},\sim\rangle})}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathcal{Q}({h})}$$\scriptstyle{f}$

We define $h$ by induction on the depth $k$ of the items.

$\mathsf{(k=0)}$ Only conditions in the initial marking have depth $0$. Let
$b^{\prime}\in B^{\prime}$ with $0pt{b^{\prime}}=0$. Hence $b^{\prime}\in
v_{0}^{\prime}$ and thus
$[{b^{\prime}}]_{\scriptscriptstyle{\sim}}=\\{b^{\prime}\\}$ is in the initial
marking of $\mathcal{Q}({\langle O^{\prime},\sim\rangle})$. Therefore
$f_{\mathrm{s}}([{b^{\prime}}]_{\scriptscriptstyle{\sim}})=b\in v_{0}$ and we
can define $h_{\mathrm{s}}(b^{\prime})=\langle b,\bot\rangle$, which is in the
initial marking of $\mathcal{U}^{pre}({O})$.

$\mathsf{(k>0)}$ Let $e^{\prime}\in E^{\prime}$ be an event such that
$0pt{e^{\prime}}=k>0$. Therefore conditions in ${\rm
Phys.~{}Rev.~{}E}{e^{\prime}}$ have depth less than $k$. Hence their
$h$-images have been already defined. We have to define $h_{\mathrm{t}}$ on
$e^{\prime}$ and $h_{\mathrm{s}}$ on its post-set.

  * •

If $h_{\mathrm{t}}([{e^{\prime}}]_{\scriptscriptstyle{\sim}})$ is undefined
then necessarily also $h_{\mathrm{t}}(e^{\prime})$ is undefined and
$h_{\mathrm{s}}(b^{\prime})=0$ for all
$b^{\prime}\in{e^{\prime}}{{}^{\bullet}}$.

  * •

If instead $h_{\mathrm{t}}([{e^{\prime}}]_{\scriptscriptstyle{\sim}})=t$
observe that since ${\rm Phys.~{}Rev.~{}E}{e^{\prime}}$ is strongly concurrent
by Lemma 12 also $h_{\mathrm{s}}({\rm Phys.~{}Rev.~{}E}{e^{\prime}})$ is so.
And, as argued in the proof of Proposition 20, $h_{\mathrm{s}}({\rm
Phys.~{}Rev.~{}E}{e^{\prime}})$ is strongly concurrent. Now, since $f$ is a
p-net morphism $f_{\mathrm{s}}({\rm
Phys.~{}Rev.~{}E}{[{e^{\prime}}]_{\scriptscriptstyle{\sim}}})={\rm
Phys.~{}Rev.~{}E}{t}$. Hence, we have

> $\begin{array}[]{ll}f_{\mathrm{s}}({\rm
> Phys.~{}Rev.~{}E}{[{e^{\prime}}]_{\scriptscriptstyle{\sim}}})=&\\\
> \quad={\varepsilon_{N}}_{\mathrm{s}}(\mathcal{Q}({h})_{\mathrm{s}}({\rm
> Phys.~{}Rev.~{}E}{[{e^{\prime}}]_{\scriptscriptstyle{\sim}}}))&\mbox{[by
> commutativity (up to depth $k$)]}\\\
> \quad={\varepsilon_{N}}_{\mathrm{s}}([{h_{\mathrm{s}}({\rm
> Phys.~{}Rev.~{}E}{e^{\prime}})}]_{\scriptscriptstyle{\sim}})&\mbox{[by
> definition of $\mathcal{Q}({})$]}\\\ \end{array}$

Recalling the definition of $\varepsilon_{N}$, the above equality implies that
$\pi(\mathcal{Q}({h})_{\mathrm{s}}({\rm
Phys.~{}Rev.~{}E}{e^{\prime}}))=f_{\mathrm{s}}({\rm
Phys.~{}Rev.~{}E}{[{e^{\prime}}]_{\scriptscriptstyle{\sim}}})={\rm
Phys.~{}Rev.~{}E}{t}$. Hence the unfolding contains an event $e=\langle
t,h_{\mathrm{s}}({\rm Phys.~{}Rev.~{}E}{e^{\prime}})\rangle$ and we define
$h_{\mathrm{t}}(e^{\prime})=e$. The mapping is then extended to the post-set
of $e^{\prime}$ by defining, for each $b\in{e^{\prime}}{{}^{\bullet}}$,
$h_{\mathrm{s}}(b)=\langle
f_{\mathrm{s}}([{b}]_{\scriptscriptstyle{\sim}}),e\rangle$.

Uniqueness follows by noticing that at each level we were forced to define $h$
as we did to ensure commutativity.

######  Corollary 22 (coreflection between $\mathsf{PN}$ and $\mathsf{ON}$).

$\mathcal{I}({})\dashv\mathcal{U}({})$

######  Proof 4.14.

Immediate corollary of Propositions 20 and 21.

##  5\. Locally Connected Event Structures from Occurrence p-Nets

In this section we show how an es can be extracted from an occurrence p-net,
thus providing an es semantics to p-nets via the unfolding semantics. The
transformation maps occurrence p-nets to locally connected ess and it is shown
to be functorial. Conversely, we show how a canonical occurrence p-net can be
associated to any locally connected es. The two transformations are shown to
establish a coreflection.

An occurrence p-net can be easily mapped to an es by forgetting the conditions
and keeping the events and the enabling and conflict relations on events. The
transformation gives rise to a functor from the category of occurrence p-nets
to the category of locally connected es.

[es for an occurrence p-net] The functor
$\mathcal{E}({}):\mathsf{ON}\to\mathsf{{\ell}ES}$ is defined as follows. Let
$O=(B,B^{\mathrm{p}},E,\delta_{0},\delta_{1},v_{0})$ be an occurrence p-net.
The corresponding es is
$\mathcal{E}({O})=(E,\vdash_{\mathcal{U}({N})},\\#_{\mathcal{U}({N})})$. For
any morphism $f:O_{1}\to O_{2}$ we let $\mathcal{E}({f})=f_{\mathrm{t}}$.

The es associated with a p-net is obtained from its unfolding by forgetting
the places and keeping the events and their dependencies. We first show that
$\mathcal{E}({})$ is well-defined on objects.

######  Lemma 23 (occurrence p-nets to locally connected es).

Let $O$ be an occurrence p-net. Then $\mathcal{E}({O})$ is a locally connected
$\mathsf{ES}$.

######  Proof 5.1.

Let $e\in\mathcal{E}({O})$ be an event. Since $O$ is an occurrence p-net, for
all $b\in{\rm Phys.~{}Rev.~{}E}{e}$ the pre-set ${\rm Phys.~{}Rev.~{}E}{b}$ is
connected. Moreover, if ${\rm Phys.~{}Rev.~{}E}{b}\neq\emptyset$ then ${\rm
Phys.~{}Rev.~{}E}{b}$ is a disjunct for $e$. In fact, clearly, for each
configuration $C\in\mathit{Conf}({\mathcal{E}({O})})$ such that $C\vdash e$ we
have $C\cap{\rm Phys.~{}Rev.~{}E}{b}\neq\emptyset$. Still ${\rm
Phys.~{}Rev.~{}E}{b}$ might not be a disjunct for the failure of minimality,
i.e., for the existence of an event $e^{\prime}\in{\rm Phys.~{}Rev.~{}E}{b}$
such that ${\rm Phys.~{}Rev.~{}E}{b}\setminus\\{e^{\prime}\\}$ still
intersects any configuration enabling $e$. However, it is easy to see that
this would imply the existence of an event $e^{\prime\prime}\in{\rm
Phys.~{}Rev.~{}E}{b}$ such that
$e^{\prime\prime}\rightsquigarrow_{O}e^{\prime}$, violating the irredundancy
assumption.

It is also immediate to see that $\\{{\rm Phys.~{}Rev.~{}E}{b}\mid b\in{\rm
Phys.~{}Rev.~{}E}{e}\ \land\ {\rm Phys.~{}Rev.~{}E}{b}\neq\emptyset\\}$ is a
covering. Hence we conclude.

The fact that $\mathcal{E}({})$ is well-defined on morphisms is a consequence
of the lemma below. For an occurrence p-net $O$, let us denote by $\prec_{O}$
immediate causality on events, i.e., $e\prec_{O}e^{\prime}$ if there is
$b\in{\rm Phys.~{}Rev.~{}E}{e^{\prime}}$ such that ${\rm
Phys.~{}Rev.~{}E}{b}=\\{e\\}$. Note that causality $\leq_{O}$ on events is the
transitive closure of $\prec_{O}$.

######  Lemma 24 (properties of occurrence p-net morphisms).

Let $O$, $O^{\prime}$ be occurrence p-nets and $f:O\to O^{\prime}$ a morphism.
Then for all $C\in\mathit{Conf}({O})$ and $e_{1},e_{2}\in E$ with $f(e_{1})$,
$f(e_{2})$ defined

  * •

if $f_{\mathrm{t}}(e_{1})=f_{\mathrm{t}}(e_{2})$ and $e_{1}\neq e_{2}$ then
$e_{1}\,\\#_{O}\,e_{2}$;

  * •

if $f_{\mathrm{t}}(e_{1})\,\\#_{O^{\prime}}\,f_{\mathrm{t}}(e_{2})$ then
$e_{1}\,\\#_{O}\,e_{2}$;

  * •

if $C\vdash_{O}e_{1}$ then
$f_{\mathrm{t}}(C)\vdash_{O^{\prime}}f_{\mathrm{t}}(e_{1})$.

######  Proof 5.2.

(1) Let $f_{\mathrm{t}}(e_{1})=f_{\mathrm{t}}(e_{2})$ and $e_{1}\neq e_{2}$.
Consider a causal chain of events in $O^{\prime}$, starting from the initial
marking and passing through non-persistent conditions only, namely consider
$e_{1}^{\prime},e_{2}^{\prime},\ldots,e^{\prime}_{n-1},e_{n}^{\prime}=f_{\mathrm{t}}(e_{1})=f_{\mathrm{t}}(e_{2})$
and conditions $b_{1}^{\prime},\ldots,b_{n}^{\prime}\in B^{\prime\mathrm{n}}$
such that $b_{1}\in v_{0}^{\prime}$ and for all $i\in[{1},{n-1}]$ it holds
$b_{i}\in{e_{i}^{\prime}}{{}^{\bullet}}\cap{\rm
Phys.~{}Rev.~{}E}{e_{i+1}^{\prime}}$; note that such a chain exists because
$O^{\prime}$ is t-restricted. It is easy to see that there must be
corresponding causal chains $e_{j}^{1},\ldots,e_{j}^{n}=e_{j}$ and
$b_{j}^{1},\ldots,b_{j}^{n}\in B^{\mathrm{n}}$, for $j\in\\{1,2\\}$, such that
$b_{j}^{1}\in v_{0}$ and for all $i\in[{1},{n-1}]$ it holds
$b_{j}^{i}\in{e_{j}^{i}}{{}^{\bullet}}\cap{\rm
Phys.~{}Rev.~{}E}{e_{j}^{i+1}}$, which are mapped to the causal chain in
$O^{\prime}$, i.e., $f_{\mathrm{t}}(e_{j}^{i})=e_{i}^{\prime}$ and
$b_{i}^{\prime}\in f_{\mathrm{s}}(b_{j}^{i})$ for all $i\in[{1},{n}]$,
$j\in\\{1,2\\}$.

Consider the least $i$ such that $e_{1}^{i}\neq e_{2}^{i}$. If $i=1$, i.e.,
$e_{1}^{1}\neq e_{2}^{1}$ then, since $b_{1}^{1},b_{2}^{1}\in v_{0}$,
$b_{1}^{\prime}\in f_{\mathrm{s}}(b_{1}^{1})$ and $b_{1}^{\prime}\in
f_{\mathrm{s}}(b_{2}^{1})$, recalling that
$f_{\mathrm{s}}(v_{0})=v_{0}^{\prime}$ and $b_{1}^{\prime}$, by safety of the
initial marking, must have multiplicity at most $1$, we conclude that
necessarily $b_{1}^{1}=b_{2}^{1}$ and thus $e_{1}^{1}\,\\#_{O}\,e_{2}^{1}$,
hence, by inheritance, $e_{1}=e_{1}^{n}\,\\#_{O}\,e_{2}^{n}=e_{2}$, as
desired.

Otherwise, if $i>1$, i.e., $e_{1}^{i-1}=e_{2}^{i-1}$, then just observe that
$b_{1}^{i-1},b_{2}^{i-1}\in{e_{1}^{i-1}}{{}^{\bullet}}={e_{2}^{i-1}}{{}^{\bullet}}$,
and, by safety of ${e_{j}^{i-1}}{{}^{\bullet}}$, as above, we conclude
$e_{1}^{i}\,\\#_{O}\,e_{2}^{i}$, and thus $e_{1}\,\\#_{O}\,e_{2}$, as desired.

(2) Let $f_{\mathrm{t}}(e_{1})\,\\#_{O^{\prime}}\,f_{\mathrm{t}}(e_{2})$ in
$O^{\prime}$. We proceed by induction on the length of the derivation of the
conflict. If such length is $0$, i.e., the conflict is direct, then there is
$b^{\prime}\in{\rm Phys.~{}Rev.~{}E}{f_{\mathrm{t}}(e_{1})}\cap{\rm
Phys.~{}Rev.~{}E}{f_{\mathrm{t}}(e_{2})}\cap B^{\prime\mathrm{n}}$. Thus, for
$j\in\\{1,2\\}$, there are $b_{j}\in{\rm Phys.~{}Rev.~{}E}{e_{j}}\cap
B^{\mathrm{n}}$, such that $b^{\prime}\in f_{\mathrm{s}}(b_{j})$. If
$b_{1}=b_{2}$ then $e_{1}\,\\#_{O}\,e_{2}$, and we conclude. Otherwise,
observe that $b_{1},b_{2}\not\in v_{0}$, otherwise (again by safety of the
initial marking) they could not have a common image. Therefore ${\rm
Phys.~{}Rev.~{}E}{b_{1}}=\\{e_{1}^{\prime}\\}$ and ${\rm
Phys.~{}Rev.~{}E}{b_{2}}=\\{e_{2}^{\prime}\\}$ for suitable $e_{1},e_{2}\in E$
(the pre-set is a singleton since $b_{1}$ and $b_{2}$ are not persistent).
Moreover
$b^{\prime}\in{f_{\mathrm{t}}(e_{1}^{\prime})}{{}^{\bullet}}={f_{\mathrm{t}}(e_{2}^{\prime})}{{}^{\bullet}}$
hence it must be
$f_{\mathrm{t}}(e_{1}^{\prime})=f_{\mathrm{t}}(e_{2}^{\prime})$. From point
(1), $e_{1}^{\prime}\,\\#_{O}\,e_{2}^{\prime}$ and thus
$e_{1}\,\\#_{O}\,e_{2}$, by inheritance.

If instead the conflict
$f_{\mathrm{t}}(e_{1})\,\\#_{O^{\prime}}\,f_{\mathrm{t}}(e_{2})$ is inherited,
we must have $b_{1}^{\prime}\in{\rm Phys.~{}Rev.~{}E}{f_{\mathrm{t}}(e_{1})}$
and $b_{2}^{\prime}\in{\rm Phys.~{}Rev.~{}E}{f_{\mathrm{t}}(e_{2})}$ such that
$b_{1}^{\prime}\\#_{O^{\prime}}b_{2}^{\prime}$. In turn this means that ${\rm
Phys.~{}Rev.~{}E}{b_{1}^{\prime}},{\rm
Phys.~{}Rev.~{}E}{b_{2}^{\prime}}\neq\emptyset$ and for all
$e_{1}^{\prime}\in{\rm Phys.~{}Rev.~{}E}{b_{1}^{\prime}}$,
$e_{2}^{\prime}\in{\rm Phys.~{}Rev.~{}E}{b_{2}^{\prime}}$,
$e_{1}^{\prime}\\#_{O^{\prime}}e_{2}^{\prime}$.

Consider $b_{1}\in{\rm Phys.~{}Rev.~{}E}{e_{1}}$, $b_{2}\in{\rm
Phys.~{}Rev.~{}E}{e_{2}}$ such that $b_{1}^{\prime}\in f_{\mathrm{s}}(b_{1})$
and $b_{2}^{\prime}\in f_{\mathrm{s}}(b_{2})$. Necessarily,
$b_{1},b_{2}\not\in v_{0}$, hence ${\rm Phys.~{}Rev.~{}E}{b_{1}},{\rm
Phys.~{}Rev.~{}E}{b_{2}}\neq\emptyset$. Moreover, for all $e_{3}\in{\rm
Phys.~{}Rev.~{}E}{b_{1}}$, $f_{\mathrm{t}}(e_{3})\in{\rm
Phys.~{}Rev.~{}E}{b_{1}^{\prime}}$ and for all $e_{4}\in{\rm
Phys.~{}Rev.~{}E}{b_{2}}$, $f_{\mathrm{t}}(e_{4})\in{\rm
Phys.~{}Rev.~{}E}{b_{2}^{\prime}}$. Hence, by the observation above,
$f_{\mathrm{t}}(e_{3})\,\\#_{O^{\prime}}\,f_{\mathrm{t}}(e_{4})$, and the
derivation of such conflict is shorter than that of
$f_{\mathrm{t}}(e_{1})\,\\#_{O^{\prime}}\,f_{\mathrm{t}}(e_{2})$. Thus, by
inductive hypothesis, $e_{3}\,\\#_{O}\,e_{4}$. By definition of conflict, this
implies that $b_{1}\,\\#_{O}\,b_{2}$ and thus $e_{1}\,\\#_{O}\,e_{2}$, as
desired.

(3) By Definition 4.1 we have to show that for each $b^{\prime}\in{\rm
Phys.~{}Rev.~{}E}{f_{\mathrm{t}}(e_{1})}$ either $b^{\prime}\in
u^{\prime}_{0}$ or there is an $e^{\prime}\in f_{\mathrm{t}}(C)$ such that
$b^{\prime}\in{e^{\prime}}{{}^{\bullet}}$. Given $b^{\prime}\in{\rm
Phys.~{}Rev.~{}E}{f_{\mathrm{t}}(e_{1})}$, since $f$ is a morphism there is a
$b\in{\rm Phys.~{}Rev.~{}E}{e_{1}}$ such that $b^{\prime}\in
f_{\mathrm{s}}(b)$. Since $C\vdash_{O}e_{1}$, either $b\in u_{0}$, and in this
case $b^{\prime}\in f_{\mathrm{s}}(u_{0})=u^{\prime}_{0}$, or there is an
$e\in C$ such that $b\in{e}{{}^{\bullet}}$. In the last case we have
$b^{\prime}\in f_{\mathrm{s}}(b)\subseteq
f_{\mathrm{s}}({e}{{}^{\bullet}})={f_{\mathrm{t}}(e)}{{}^{\bullet}}$, where
$f_{\mathrm{t}}(e)\in f_{\mathrm{t}}(C)$, as desired.

Conversely, we show how to freely generate an occurrence p-net from a locally
connected es. Roughly, the idea is to insert suitable conditions that induce
exactly the dependencies (enabling and conflict) of the original es.

[occurrence p-net for an es] Let $(E,\vdash,\\#)$ be a locally connected es.
We define the occurrence p-net
$\mathcal{O}({E})=(B,B^{\mathrm{p}},E,\gamma_{0},\gamma_{1},u_{0})$ as
follows. The set of places $B$ consists of

  * •

non-persistent places $\langle X,Y\rangle$ with $X,Y\subseteq E$, $|X|\leq 1$
such that $e<e^{\prime}$ for all $e\in X$, $e^{\prime}\in Y$ and
$e^{\prime}\\#e^{\prime\prime}$ for all $e^{\prime},e^{\prime\prime}\in Y$,
$e^{\prime}\neq e^{\prime\prime}$;

  * •

persistent places $\langle X,Y\rangle$ with $X,Y\subseteq E$, $X$ disjunct of
all $e\in Y$ and $X$ $\stackrel{{\scriptstyle}}{{\frown}}$-connected.

Furthermore, for all $e\in E$ let $\gamma_{0}(e)=\\{\langle X,Y\rangle\in
B\mid e\in Y\\}$, and $\gamma_{1}(e)=\\{\langle X,Y\rangle\in B\mid e\in
X\\}$. Finally, let the initial marking be
$u_{0}=\\{\langle\emptyset,Y\rangle\mid Y\subseteq E\ \land\
\langle\emptyset,Y\rangle\in B\\}$.

The intuition is the following. For any possible set of events $Y$ pairwise in
conflict that have a common cause $e$ we insert a non-persistent place
$b=\langle\\{e\\},Y\rangle$, produced by $e$ and consumed by the events in
$Y$, inducing such dependencies. By the same clause, for any possible set of
events $Y$ pairwise in conflict, we insert a non-persistent place
$b=\langle\emptyset,Y\rangle$ consumed by the events in $Y$. Moreover, for any
pair of sets of events $\langle X,Y\rangle$ such that $X$ includes an event
for each minimal enabling of each $e\in Y$, we introduce a persistent
condition $\langle X,Y\rangle$ that is generated by all events in $X$ and used
by all events in $Y$. In this way, whenever a minimal enabling set for some
$e\in Y$ has been executed, all the pre-set of $e$ is covered. Conversely,
when all the pre-set of $e$ is covered, since we generate conditions that
include at least one event for each minimal enabling of each $e\in Y$, at
least one minimal enabling has been completely executed. The request that for
$b=\langle X,Y\rangle\in B^{\mathrm{p}}$ the set $X={\rm Phys.~{}Rev.~{}E}{b}$
is a disjunct connected by $\stackrel{{\scriptstyle}}{{\frown}}$ will ensure
that the pre-set of conditions is connected, as required by the definition of
occurrence p-net. The fact that $X$ is a disjunct will guarantee irredundancy.
Formally, the fact that the construction above produces a well-defined
occurrence p-net will be a consequence of Lemma 25.

We next observe that for all locally connected ess, if we build the
corresponding occurrence p-net and then we take the underlying es we get an es
isomorphic to the original one. First we prove a technical result.

######  Lemma 25 (dependencies in the occurrence p-net for an es).

Let $E$ be a locally connected es and
$\mathcal{O}({E})=(B,B^{\mathrm{p}},E,\gamma_{0},\gamma_{1},v_{0})$. Then

  1. (1)

for all $e,e^{\prime}\in E$, $e\\#e^{\prime}$ iff
$e\\#_{\mathcal{O}({E})}e^{\prime}$;

  2. (2)

for all $C\in\mathit{Conf}({E})$, $C\vdash e$ implies
$C\vdash_{\mathcal{O}({E})}e$;

  3. (3)

for all $C\in\mathit{Conf}({\mathcal{O}({E})})$, $C\vdash_{\mathcal{O}({E})}e$
implies $C\vdash e$.

######  Proof 5.3.

(1) _Only if part._ Suppose that $e\\#e^{\prime}$ for $e,e^{\prime}\in E$.
Then, by Definition 5.2, $\mathcal{O}({E})$ contains a non-persistent place
$\langle\emptyset,\\{e,e^{\prime}\\}\rangle\in{\rm
Phys.~{}Rev.~{}E}{e}\cap{\rm Phys.~{}Rev.~{}E}{e^{\prime}}$, thus
$e\,\\#_{\mathcal{O}({E})}\,e^{\prime}$.

_If part._ We prove, more generally, that for $A\subseteq E$, if
$\\#_{\mathcal{O}({E})}A$ then there is no configuration
$C\in\mathit{Conf}({E})$ such that $A\subseteq C$. Then for binary conflict
the thesis follows from the fact that $E$ is saturated.

We proceed by induction on the length of the derivation of the conflict. If
the length is $0$, i.e., the conflict is direct, there are $e,e^{\prime}\in A$
and $b\in{\rm Phys.~{}Rev.~{}E}{e}\,\cap\,{\rm
Phys.~{}Rev.~{}E}{e^{\prime}}\,\cap\,B^{\mathrm{n}}$. By Definition 5.2 this
means that $b=\langle\\{e^{\prime\prime}\\},Y\rangle$ with $e,e^{\prime}\in Y$
and therefore $e\\#e^{\prime}$ by construction and we are done.

If instead the conflict $\\#_{\mathcal{O}({E})}\,A$ is inherited, we must have
$e\in A$ such that $\\#_{\mathcal{O}({E})}\,(A\setminus\\{e\\})\cup{\rm
Phys.~{}Rev.~{}E}{e}$. This means that if we consider any $A_{e}\subseteq E$
such that $A_{e}\cap{\rm Phys.~{}Rev.~{}E}{b}\neq\emptyset$ for all $b\in{\rm
Phys.~{}Rev.~{}E}{e}$ then $\\#_{\mathcal{O}({E})}\,(A\setminus\\{e\\})\cup
A_{e}$. The derivations of the latter conflicts are shorter than that of
$\\#_{\mathcal{O}({E})}\,A$, and thus by induction hypothesis we can infer
that there is no configuration $C\in\mathit{Conf}({E})$ such that
$(A\setminus\\{e\\})\cup A_{e}\subseteq C$. Now, assume by absurd that
$A\subseteq\hat{C}$ for a configuration $\hat{C}$. Since $e\in\hat{C}$, there
is a configuration $\hat{C}_{e}\subset\hat{C}$ such that $\hat{C}_{e}\vdash
e$. By construction $\\{X\mid X\neq\emptyset\ \land\ b=\langle
X,Y\rangle\in{\rm Phys.~{}Rev.~{}E}{e}\\}=\\{{\rm Phys.~{}Rev.~{}E}{b}\mid
b\in{\rm Phys.~{}Rev.~{}E}{e}\ \land\ {\rm
Phys.~{}Rev.~{}E}{b}\neq\emptyset\\}$ is a covering of $e$, therefore
$\hat{C}_{e}\cap{\rm Phys.~{}Rev.~{}E}{b}\neq\emptyset$ for all $b\in{\rm
Phys.~{}Rev.~{}E}{e}$. But clearly
$(A\setminus\\{e\\})\cup\hat{C}_{e}\subseteq\hat{C}$, contradicting the
inductive hypothesis.

(2) Let $C\in\mathit{Conf}({E})$ such that $C\vdash e$. In order to conclude
that $C\vdash_{\mathcal{O}({E})}e$ we have to prove that for all $b\in{\rm
Phys.~{}Rev.~{}E}{e}$, either $b\in v_{0}$ or there exists $e^{\prime}\in C$
such that $b\in{e^{\prime}}{{}^{\bullet}}$. We distinguish two cases.

If $b$ is not persistent, then $b=\langle\\{e^{\prime}\\},Y\rangle$ with $e\in
Y$, hence $e^{\prime}<e$. Then $b\in{e^{\prime}}{{}^{\bullet}}$.

If $b$ is persistent, then $b=\langle X,Y\rangle$ with $e\in Y$ and, by
definition of $\mathcal{O}({E})$, $X\cap C\neq\emptyset$. Let $e^{\prime}\in
X\cap C$. Then $e^{\prime}\in C$ and $b\in{e^{\prime}}{{}^{\bullet}}$.

(3) We prove that for all finite $C\in\mathit{Conf}({\mathcal{O}({E})})$ it
holds that $C\in\mathit{Conf}({E})$ and, for any $e\in E$, if
$C\vdash_{\mathcal{O}({E})}e$ then $C\vdash e$.

The proof proceeds by induction on the cardinality $|C|$. The base case
$|C|=0$ is immediate. If $|C|>0$, we know by Lemma 9 that
$C=\\{e_{1},\ldots,e_{n}\\}$ and there exists a firing sequence
$v_{0}[{e_{1}}\rangle v_{1}[{e_{2}}\rangle\ldots[{e_{n}}\rangle v_{n}$. Since
$C^{\prime}=\\{e_{1},\ldots,e_{n-1}\\}\in\mathit{Conf}({\mathcal{O}({E})})$
and $C^{\prime}\vdash_{\mathcal{O}({E})}e_{n}$, by inductive hypothesis
$C^{\prime}\in\mathit{Conf}({E})$ and $C^{\prime}\vdash e_{n}$. From this and
point (1), we deduce that $C=C^{\prime}\cup\\{e\\}\in\mathit{Conf}({E})$.

For the second part, let $e\in E$ be such that $C\vdash_{\mathcal{O}({E})}e$.
By the first part, $C\in\mathit{Conf}({E})$ and by definition of enabling in
occurrence p-nets, for all $b\in{\rm Phys.~{}Rev.~{}E}{e}$, either $b\in
v_{0}$ or there exists $e^{\prime}\in C$ such that
$b\in{e^{\prime}}{{}^{\bullet}}$. This means that $C\cap{\rm
Phys.~{}Rev.~{}E}{b}\neq\emptyset$ for all $b\in{\rm Phys.~{}Rev.~{}E}{e}$,
${\rm Phys.~{}Rev.~{}E}{b}\neq\emptyset$ and this is a covering of $e$. Hence
by definition of covering, $C\vdash e$.

######  Corollary 26 ($\mathcal{O}({E})$ is well-defined).

Let $E$ be a locally connected es. Then $\mathcal{O}({E})$ is a well-defined
occurrence p-net.

######  Proof 5.4.

The fact that $\mathcal{O}({E})$ satisfies the structural properties (a) and
(c) of Definition 2 is immediate by construction. Property (b), i.e., the fact
that each transition $e\in T$ admits a securing sequence follows by the
analogous property of es, recalling that by Lemma 25, enabling and conflict
coincide in $E$ and $\mathcal{O}({E})$. Similarly, the fact that for each
condition $b\in B$, the set ${\rm Phys.~{}Rev.~{}E}{b}$ is connected is true
by construction after Lemma 25, showing that conflict, and thus the notion of
connectedness, coincide in $E$ and $\mathcal{O}({E})$. Finally, we observe
that $\mathcal{O}({E})$ is well-formed. T-restrictedness holds by
construction. Irredundancy follows from the fact that for each $b=\langle
X,Y\rangle\in B^{\mathrm{p}}$, the pre-set ${\rm Phys.~{}Rev.~{}E}{b}=X$ is a
disjunct. Hence given $e\in X={\rm Phys.~{}Rev.~{}E}{b}$ there cannot be an
additional path $e\rightsquigarrow_{\mathcal{O}({E})}^{n}$ with $n\geq 2$ into
$b$. In fact, if this were the case, since by Lemma 25, enabling coincides in
$E$ and $\mathcal{O}({E})$, event $e$ could be omitted, i.e.,
$X^{\prime}=X\setminus\\{e\\}$ would still intersect any configuration
enabling $e$, contradicting the minimality of $X$.

######  Corollary 27 (unit).

Let $E$ be a locally connected es. Then
$\eta_{E}:E\to\mathcal{E}({\mathcal{O}({E})})$ defined as the identity on
events is an isomorphism.

######  Proof 5.5.

The function $\eta_{E}$ is obviously a bijection. The fact that it is an
isomorphism of es follows immediately from Lemma 25.

In order to conclude we need to show that the construction of the occurrence
p-net associated with an es $E$ and the isomorphism
$\eta_{E}:E\to\mathcal{E}({\mathcal{O}({E})})$ are free over $E$. The next
lemma states some properties of occurrence p-net morphisms that guide the
proof.

######  Lemma 28.

Let $h:O\to O^{\prime}$ be an occurrence p-net morphism. Then for $b\in B$ and
$b^{\prime}\in B^{\prime}$ such that $b^{\prime}\in h_{\mathrm{s}}(b)$ it
holds

  1. (1)

if $b\in B^{\mathrm{n}}$ then (a) $h_{\mathrm{t}}({\rm
Phys.~{}Rev.~{}E}{b})={\rm Phys.~{}Rev.~{}E}{b^{\prime}}$ and
${b}{{}^{\bullet}}=\\{e_{1}\in E\mid e_{1}\in
h_{\mathrm{t}}^{-1}({b}{{}^{\bullet}})\ \land\ {\rm Phys.~{}Rev.~{}E}{b}\leq
e_{1}\\}$, where ${\rm Phys.~{}Rev.~{}E}{b}\leq e_{1}$ means $e\leq e_{1}$
when ${\rm Phys.~{}Rev.~{}E}{b}=\\{e\\}$ and it is a vacuous requirement,
otherwise;

  2. (2)

if $b\in B^{\mathrm{p}}$ then (a) ${\rm Phys.~{}Rev.~{}E}{b}\subseteq
h_{\mathrm{t}}^{-1}({\rm Phys.~{}Rev.~{}E}{b^{\prime}})$ and (b)
${b}{{}^{\bullet}}\subseteq h_{\mathrm{t}}^{-1}({b^{\prime}}{{}^{\bullet}})$.

######  Proof 5.6.

Point (1) is analogous to the one in the ordinary case. Point (2) easily
follows from the definition of morphism.

######  Theorem 29 (coreflection between $\mathcal{O}({})$ and
$\mathcal{E}({})$).

The construction $\mathcal{E}({})$ extends to a functor that is left adjoint
to $\mathcal{O}({})$, and they establish a coreflection.

######  Proof 5.7.

Let $E$ be a locally connected es. We show the freeness of
$\eta_{E}:E\to\mathcal{E}({\mathcal{O}({E})})$ as defined in Corollary 27. We
have to show that for any occurrence p-net $O^{\prime}=\langle
B^{\prime},B^{\prime\mathrm{p}},E^{\prime},\gamma_{0}^{\prime},\gamma_{1}^{\prime},v_{0}^{\prime}\rangle$
and for any es morphism $f:E\to\mathcal{E}({O^{\prime}})$ there exists a
unique morphism $h:\mathcal{O}({E})\to O^{\prime}$ such that the following
diagram commutes

$\textstyle{{E}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\eta_{E}}$$\scriptstyle{f}$$\textstyle{{\mathcal{E}({\mathcal{O}({E})})}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathcal{E}({h})}$$\textstyle{{\mathcal{E}({O^{\prime}})}}$

The transition component of $h$ is determined as $h_{\mathrm{t}}=f$. It can be
extended to a p-net morphism by defining the place component as follows:

  1. (1)

on non-persistent places $b=\langle X,Y\rangle$, define

$h_{\mathrm{s}}(b)=\\{b^{\prime}\in B^{\prime\mathrm{n}}\mid{\rm
Phys.~{}Rev.~{}E}{b^{\prime}}=h_{\mathrm{t}}(X)\ \land\ Y=\\{e_{1}\in E\mid
e_{1}\in h_{\mathrm{t}}^{-1}({b^{\prime}}{{}^{\bullet}})\land\ X<e_{1}\\}\\}$.

  2. (2)

on persistent places $b=\langle X,Y\rangle$, say that $b$ is a potential pre-
image of $b^{\prime}\in B^{\prime\mathrm{n}}$ if $X\subseteq
h_{\mathrm{t}}^{-1}({\rm Phys.~{}Rev.~{}E}{b^{\prime}})$ and $Y\subseteq
h_{\mathrm{t}}^{-1}({b^{\prime}}{{}^{\bullet}})$. It is maximal if for any
potential pre-image $b_{1}=\langle X_{1},Y_{1}\rangle$ of $b^{\prime}$, with
$X_{1}\cap X\neq\emptyset$ it holds $Y_{1}\subseteq Y$. Then we define

$h_{\mathrm{s}}(b)=\\{b^{\prime}\in B^{\prime\mathrm{n}}\mid\mbox{$b$ maximal
potential pre-image of $b^{\prime}$}\\}$.

It is not difficult to prove that this is a morphism. Uniqueness follows from
the fact that, for non-persistent places (point (1)) we defined the morphism
in the only possible way, according to Lemma 28(1). For persistent places,
each $b^{\prime}\in B^{\prime\mathrm{p}}$ must be in the image of exactly one
potential pre-image. In fact, according to Lemma 28(2), it must be in the
image of at least one potential pre-image and, by injectivity on pre- and
post-sets of transitions, it can be in the image of at most one of the
potential pre-images. Using preservation of pre- and post-sets, we then
conclude that $h_{\mathrm{s}}(s)$ must be defined as we did in point (2).

As a side remark, note that the es induced by $\mathcal{U}^{pre}({N})$ (before
quotienting) is a prime es. If endowed with the equivalence $\sim_{N}$
restricted to events, it corresponds to the notion of prime es with
equivalence [10, 3]. More precisely, if we denote by $\\#_{N}^{\mu}$ the
immediate conflict relation, then the prime es obtained from the pre-
unfolding, by forgetting the conditions and the direct conflicts between
equivalent events, i.e., $\langle(E,\leq_{\mathcal{U}({N})},\\#),\sim\rangle$,
where
$\\#=\\#_{\mathcal{U}({N})}\setminus(\\#_{\mathcal{U}({N})}^{\mu}\cap\sim_{N})$
and $\sim=\sim_{N}\cap(E\times E)$, is a prime es in the sense of [3]. Its
events arise, as explained in [3], as the irreducible elements of the domain
associated with $N$.

##  6\. Conclusions

Persistence is the continuance of an effect after its causes ceased to exist.
In this paper we have studied the effect of adding persistence to Petri nets
at the level of es semantics. Interestingly, we have extended Winskel’s chain
of coreflection from the category of p-nets to the newly defined category of
locally connected ess, which is a full subcategory of the category of general
ess. Since the category of connected ess is included in the one of locally
connected ess, the coreflection can serve to explain in basic terms the
phenomenon of fusion arising in the context of graph grammars and that induces
(connected) disjunctive causes. On the one hand, this confirms our intuition
that Petri nets and their natural extensions keep capturing all phenomena of
concurrency within easy-to-understand operational models. On the other hand,
our results show that while non-prime ess were actually underestimated in the
literature, at least in some cases they are natural, expressive and equipped
with an interesting theory even at the operational level.

The result has been proved for the class of well-formed persistent nets, where
redundant paths to persistent places are forbidden. Despite the fact that this
is a natural restriction, preliminary investigations suggest that the result
could be extended, at the price of some technical complications, to the more
general setting.

## Acknowledgment

The authors wish to thank the anonymous reviewers for their careful reading
and their insightful comments on the submitted version on the paper.

## References

  * [1] Samson Abramsky.  Petri nets, discrete physics, and distributed quantum computation.  In Pierpaolo Degano, Rocco De Nicola, and José Meseguer, editors, Concurrency, Graphs and Models, Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday, volume 5065 of Lecture Notes in Computer Science, pages 527–543. Springer, 2008.
  * [2] Andrea Asperti and Nadia Busi.  Mobile Petri nets.  Mathematical Structures in Computer Science, 19(6):1265–1278, 2009\.
  * [3] Paolo Baldan, Andrea Corradini, and Fabio Gadducci.  Domains and event structures for fusions.  In LICS 2017, pages 1–12. IEEE Computer Society, 2017.  Extended version available as arXiv:1701.02394.
  * [4] Paolo Baldan, Andrea Corradini, and Ugo Montanari.  Contextual Petri nets, asymmetric event structures and processes.  Information and Computation, 171(1):1–49, 2001.
  * [5] Filippo Bonchi, Antonio Brogi, Sara Corfini, and Fabio Gadducci.  A net-based approach to web services publication and replaceability.  Fundamenta Informaticae, 94(3-4):305–330, 2009.
  * [6] Roberto Bruni, Hernán C. Melgratti, and Ugo Montanari.  Concurrency and probability: Removing confusion, compositionally.  In LICS 2018, pages 195–204. ACM, 2018.
  * [7] Søren Christensen and Niels Damgaard Hansen.  Coloured Petri nets extended with place capacities, test arcs and inhibitor arcs.  In Marco Ajmone Marsan, editor, ICATPN 1993, volume 691 of Lecture Notes in Computer Science, pages 186–205. Springer, 1993.
  * [8] Federico Crazzolara and Glynn Winskel.  Events in security protocols.  In Michael K. Reiter and Pierangela Samarati, editors, CCS 2001, pages 96–105. ACM, 2001.
  * [9] Federico Crazzolara and Glynn Winskel.  Petri nets with persistence.  In Nadia Busi, Roberto Gorrieri, and Fabio Martinelli, editors, WISP 2004, volume 121 of Electronic Notes in Theoretical Computer Science, pages 143–155. Elsevier, 2005.
  * [10] Marc de Visme and Glynn Winskel.  Strategies with parallel causes.  In Valentin Goranko and Mads Dam, editors, CSL 2017, volume 82 of LIPIcs, pages 41:1–41:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
  * [11] Joanne Bechta Dugan, Kishor S. Trivedi, Robert Geist, and Victor F. Nicola.  Extended stochastic Petri nets: Applications and analysis.  In Erol Gelenbe, editor, Performance 1984, pages 507–519. North-Holland, 1985.
  * [12] Yrvann Emzivat, Benoît Delahaye, Didier Lime, and Olivier H. Roux.  Probabilistic time Petri nets.  In Fabrice Kordon and Daniel Moldt, editors, ICATPN 2016, volume 9698 of Lecture Notes in Computer Science, pages 261–280. Springer, 2016.
  * [13] Claude Girault and Rüdiger Valk.  Petri Nets for Systems Engineering - A Guide to Modeling, Verification, and Applications.  Springer, 2003.
  * [14] Roberto Gorrieri.  Process Algebras for Petri nets - The Alphabetization of Distributed Systems.  Springer, 2017.
  * [15] Kurt Jensen.  Coloured Petri nets.  In Wilfried Brauer, Wolfgang Reisig, and Grzegorz Rozenberg, editors, Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part I, volume 254 of Lecture Notes in Computer Science, pages 248–299. Springer, 1987.