17416 LABEL:LastPageDec. 02, 2020Dec. 02, 2021

# A new operational representation of dependencies in Event Structures

G. Michele Pinna  Dipartimento di Matematica e Informatica, Università di
Cagliari, Cagliari, Italy<EMAIL_ADDRESS>
###### Abstract.

The execution of an event in a complex and distributed system where the
dependencies vary during the evolution of the system can be represented in
many ways, and one of them is to use Context-Dependent Event structures. Event
structures are related to Petri nets. The aim of this paper is to propose what
can be the appropriate kind of Petri net corresponding to Context-Dependent
Event structures, giving an operational flavour to the dependencies
represented in a Context/Dependent Event structure. Dependencies are often
operationally represented, in Petri nets, by tokens produced by activities and
consumed by others. Here we shift the perspective using contextual arcs to
characterize what has happened so far and in this way to describe the
dependencies among the various activities.

###### Key words and phrases:

Petri Nets, Event Structures, Operational Semantics, Contextual Nets

##  1\. Introduction

Since the introduction of the notion of Event structure ([NPW81] and [Win86])
the close relationship between this notion and suitable nets has been
investigated. The ingredients of an event structure are, beside a set of
events, a number of relations used to express which events can be part of a
configuration (the snapshot of a concurrent system), modeling a consistency
predicate, and how events can be added to reach another configuration,
modeling the dependencies among the (sets of) events. On the nets side we have
transitions, modeling the activities, and places, modeling resources the
activities may need, consume or produces. These ingredients, together with
some constraints on how places and transitions are related (via flow,
inhibitor or read arcs satisfying suitable properties), can give also a more
_operational_ description of a concurrent and distributed system. Indeed the
relationship between event structures and nets is grounded on the observation
that also in (suitable) Petri nets the relations among events are
representable, as it has been done in [GR83] for what concern the partial
order and [NPW81] for the partial order and conflict.

Since then several notions of event structures have been proposed. We recall
just few of them: the classical _prime_ event structures [Win86] where the
dependency between events, called _causality_ , is modeled by a partial order
and the consistency is described by a symmetric _conflict_ relation. Then
_flow_ event structures [Bou90] drop the requirement that the dependency
should be a partial order on the whole set of events, _bundle_ event
structures [Lan93] represent OR-causality by allowing each event to be caused
by a unique member of a bundle of events (and this constraint may be relaxed).
_Asymmetric_ event structures [BCM01], via notion of weak causality, model
asymmetric conflicts, whereas _Inhibitor_ event structures [BBCP04] are able
to faithfully capture the dependencies among events which arise in the
presence of read and inhibitor arcs in safe nets. In [BCP15] a notion of event
structures where the causality relation may be circular is investigated, and
in [AKPN18] the notion of dynamic causality is considered. Finally, we mention
the quite general approach presented in [vGP09], where there is a unique
relation, akin to a _deduction relation_. To each of the mentioned event
structures a particular class of nets is related. Prime event structures have
a correspondence in _occurrence nets_ , flow event structures have flow nets
whereas _unravel nets_ [CP14] are related to bundle event structures.
Continuing we have that asymmetric and inhibitor event structures have a
correspondence with _contextual nets_ [BCM01, BBCP04], and event structures
with circular causality with _lending nets_ [BCP15], finally to those with
dynamic causality we have _inhibitor unravel nets_ [CP17b] and to the
configuration structures presented in [vGP09] we have the notion of
_1-occurrence nets_. Most of the approaches relating nets with event
structures are based on the equation “event = transition”, even if many of the
events represent the same _high level_ activity. The idea that some of the
transitions may be somehow identified as they represent the same activity is
the one pursued in many works aiming at reducing the size of the net, like
_merged processes_ ([KKKV06]), _trellis processes_ ([Fab07]), _merging
relation_ approach ([CP17a]) or _spread nets_ ([FP18] and [PF20]), but these
approaches are mostly unrelated with event structure of any kind.

[Pin19] and [Pin20b] propose the notion of _context-dependent_ event
structures as the event structure where (almost all) the variety of
dependencies which may arise among events can be modeled. This is achieved
using just one fairly general dependency relation, called _context-dependency_
relation. Context-dependent event structure are more general than many kind of
event structures, as proved in [Pin20b], with the exception of event structure
with circular causality. It should however be observed that circular
dependencies may be understood as dependencies where the justification for the
happening of an event can be given at a later point, which is not the case of
the kind of event structures considered in this paper, thus we may say that
context-dependent event structure are more general than event structures where
each event may happen if a complete justification for its happening is
present. In this paper we address the usual problem: given an event structure,
in our case a context-dependent event structures, which could be the kind of
net which may _correspond_ to it. To understand the characteristics of the net
to be related to context-dependent event structures we first observe that in
these event structures each event may happen in many different and often
unrelated contexts, hence the same event cannot have (almost) the same _past_
event up to suitable equivalences, as it happens in many approaches, e.g. in
unravel nets, trellis processes or spread nets among others. The second
observation, which has been used also in [Pin19] and [Pin20b], is that
dependencies among transitions (events) in nets may be represented in
different ways. The usual way to represent dependencies is using the flow
relation of the net, and the dependency is then _signaled_ by a _shared_
place, but dependencies can be described also using _contextual_ arcs, _i.e._
arcs testing for the presence or absence of tokens. Following these two
observations we argue that each of the context that are _allowing_ an event to
happen can be modeled with _inhibitor_ ([JK95]) and/or _read_ arcs ([MR95]),
yielding the notion of _causal_ nets. It should be stressed that these kind of
arcs have been introduced for different purposes, but never for nets which are
meant to describe the behaviour of another one.

Usually places in a net modeling the behaviour of a concurrent and distributed
systems are seen as resources that one (or more) activities may produce and
that are consumed by anothers. Instead of, in a causal net, we consider places
as _control points_ : they simply signal what events have been executed and
thus the marking alone determines the _configuration_ of the net, without the
need of reconstructing which events have been executed before. This shift in
perspective, namely considering places as control points rather than resources
to be produced and consumed, gives further generality that can be used to
model more composite relations. Indeed we observe that this idea has been used
in [MMP21] to model the so called _out of causal order_ reversibility when
relating _reversible_ prime event structures [PU15] and nets, which otherwise
would have been impossible, as noticed in [MMP+20].

We have also to stress that, having activities quite different contexts, it is
natural to _implement_ the same activity in different ways to reflect the
different context. In causal nets, which are labeled nets, the same label may
be associated to various transitions that have to be considered as the
different incarnations of the same activity (label). This is precisely what it
is done in _unfoldings_ , the main difference being that in causal net we look
at the event itself with different _incarnations_ whereas in the classical
approaches the event is identified with an unique incarnation.

The approach we pursue here originated in the one we adopted for dynamic event
structures in [CP17b], though there the _classical_ dependencies among events
(those called causal dependencies) are represented using the standard
machinery, namely using places as resources. There we also argued that the
proper net corresponding to these kind of event structure, which are meant to
give an _operational_ representation of what _denotationally_ is characterized
by a single event, have to be represented as different transitions with the
same label. The approach is a conservative one: the dependencies represented
in other kinds on nets can be represented also in causal nets, possibly with
some further constraint, and to suitably characterized causal nets it is
possible to associate the corresponding context-dependent event structure.
Indeed, we will show that causal nets are more general than occurrence and
unravel nets. It should be stressed that the conflicts between events in
causal nets are explicitly represented and cannot be inferred otherwise.

This paper is an extended and revised version of [Pin20a]. We have added some
examples and compared the notion of causal net with other _semantics_ net like
occurrence nets and unravel nets, and we have made more precise the
relationships among those. The constructions associating event structures and
nets turn out to follow a common pattern once that the idea of dependency
shifts from the classical _produce/consume_ relationship toward the one where
contextual arcs (testing positively or negatively but without consuming),
giving in our opinion further evidence that this new operational view has a
solid ground.

### Organization of the paper.

In the next section we recall the notions of contextual nets, on which the
notion of _causal_ net is based. Section 3 reviews the more classical
approaches relating nets and event structures, namely occurrence net and prime
event structure and also unravel net and bundle event structure. Furthermore
the relationships occurrence nets - prime event structures and unravel nets -
bundle event structures are exhibited. In Section 4 we recall the notion of
context-dependent event structure and we discuss how a canonical
representation can be obtained. In Section 5 we introduce the notion of
_causal_ net and we show also how occurrence nets and unravel nets can be seen
as causal nets. We also give a direct translation from prime event structures
to causal net and vice versa. In Section 6 we discuss how to associate a
causal net to a context-dependent event structure and vice versa, showing that
the notion of causal net is adequate. Some conclusions end the paper.

##  2\. Preliminaries

We denote with ${\rm Nature}$ the set of natural numbers. Given a set $A$ with
$\mathbf{2}^{A}$ we denote the set of subsets of $A$ and with
$\mathbf{2}_{\mathit{fin}}^{A}$ the set of the finite subsets of $A$.

Let $A$ be a set, a _multiset_ of $A$ is a function $m:A\rightarrow{\rm
Nature}$. The set of multisets of $A$ is denoted by $\mu A$. A multiset $m$
over $A$ is sometimes written as $\sum m(a)\cdot a$ and $m(a)$ is the number
of occurrence of $a$ in $\sum m(a)\cdot a$. We assume the usual operations on
multisets such as union $+$ and difference $-$. We write $m\subseteq
m^{\prime}$ if $m(a)\leq m^{\prime}(a)$ for all $a\in A$. For $m\in\mu A$, we
denote with $[\\![{m}]\\!]$ the multiset defined as $[\\![{m}]\\!](a)=1$ if
$m(a)>0$ and $[\\![{m}]\\!](a)=0$ otherwise. When a multiset $m$ of $A$ is a
set, _i.e._ $m=[\\![{m}]\\!]$, we write $a\in m$ to denote that $m(a)\neq 0$,
and often confuse the multiset $m$ with the set $\\{{a\in A}\mid{m(a)\neq
0}\\}$ or a subset $X\subseteq A$ with the multiset $X(a)=1$ if $a\in A$ and
$X(a)=0$ otherwise. Furthermore we use the standard set operations like
$\cap$, $\cup$ or $\setminus$.

Given a set $A$ and a relation $<\ \subseteq A\times A$, we say that $<$ is an
irreflexive partial order whenever it is irreflexive and transitive. We shall
write $\leq$ for the reflexive closure of an irreflexive partial order $<$.
Given an irreflexive relation $\prec\ \subseteq A\times A$, with $\prec^{+}$
we denote its transitive closure.

Given a function $f:A\to B$, $\mathit{dom}(f)=\\{{a\in A}\mid{\exists b\in B.\
f(a)=b}\\}$ is the domain of $f$, and $\mathit{codom}(f)=\\{{b\in
B}\mid{\exists a\in A.\ f(a)=b}\\}$ is the codomain of $f$.

Given a set $A$, a sequence of elements in $A$ is a partial mapping $\rho:{\rm
Nature}\rightharpoonup A$ such that, given any $n\in{\rm Nature}$, if
$\rho(n)$ is defined and equal to $a\in A$ then $\forall i\leq n$ also
$\rho(i)$ is defined. A sequence is finite if $|\mathit{dom}(\rho)|$ is
finite, and the length of a sequence $\rho$, denoted with
$\mathit{size}(\rho)$, is the cardinality of $\mathit{dom}(\rho)$. A sequence
$\rho$ is often written as $a_{1}a_{2}\cdots$ where $a_{i}=\rho(i)$. With
$\overline{\rho}$ we denote the codomain of $\rho$. Requiring that a sequence
$\rho$ has distinct elements accounts to stipulate that $\rho$ is injective on
$\mathit{dom}(\rho)$. The sequence $\rho$ such that
$\mathit{dom}(\rho)=\emptyset$, the _empty_ sequence, is denoted with
$\epsilon$. Finally with $\cdot$ we denote the _concatenation_ operator that
take a finite sequence $\rho$ and a sequence $\rho^{\prime}$ and gives the
sequence $\rho^{\prime\prime}$ defined as $\rho^{\prime\prime}(i)=\rho(i)$ if
$i\leq\mathit{size}(\rho)$ and
$\rho^{\prime\prime}(i)=\rho^{\prime}(i-\mathit{size}(\rho))$ otherwise.

###  2.1. Contextual Petri nets

We briefly review the notion of (labeled) Petri net ([Rei85, Rei13]) and its
variant enriched with contextual arcs ([MR95] and [BBCP04]) along with some
auxiliary notions.

Fixed a set $\mathsf{L}$ of _labels_ , we recall that a _net_ is the 4-tuple
$N=\langle S,T,F,\mathsf{m}\rangle$ where $S$ is a set of _places_ (usually
depicted with circles) and $T$ is a set of _transitions_ (usually depicted as
squares) and $S\cap T=\emptyset$, $F\subseteq(S\times T)\cup(T\times S)$ is
the _flow_ relation and $\mathsf{m}\in\mu S$ is called the _initial marking_.
A _labeled_ net is a net equipped with a _labeling_ mapping
$\ell:T\to\mathsf{L}$.

######  Definition .

A (labelled) _contextual Petri net_ is the tuple $N=\langle
S,T,F,I,R,\mathsf{m},\ell\rangle$, where

  * •

$\langle S,T,F,\mathsf{m}\rangle$ is a net,

  * •

$I\subseteq S\times T$ are the _inhibitor_ arcs,

  * •

$R\subseteq S\times T$ are the _read_ arcs, and

  * •

$\ell:T\to\mathsf{L}$ is the labeling mapping and $\ell$ is a total function.

Inhibitor arcs depicted as lines with a circle on one end, and read arcs as
plain lines. We sometimes omit the $\ell$ mapping when $\mathsf{L}$ is $T$ and
$\ell$ is the identity. We will often call a contextual Petri net as Petri net
or simply net. In the following figure a contextual Petri net is depicted.

$s_{1}$$s_{2}$$s_{3}$$s_{4}$$s_{5}$$s_{6}$$t_{1}$$t_{2}$$t_{3}$

Figure 1. A contextual Petri net

The arc connecting the place $s_{6}$ to the transition $t_{1}$ is a read arc,
and the one connecting the place $s_{2}$ to the same transition is an
inhibitor one.

Given a net $N=\langle S,T,F,I,R,\mathsf{m}\rangle$ and $x\in S\cup T$, we
define the following (multi)sets: ${\rm
Phys.~{}Rev.~{}E}{x}=\\{{y}\mid{(y,x)\in F}\\}$ and
${x}{{}^{\bullet}}=\\{{y}\mid{(x,y)\in F}\\}$. If $x\in S$ then ${\rm
Phys.~{}Rev.~{}E}{x}\in\mu T$ and ${x}{{}^{\bullet}}\in\mu T$; analogously, if
$x\in T$ then ${\rm Phys.~{}Rev.~{}E}{x}\in\mu S$ and ${x}{{}^{\bullet}}\in\mu
S$. Given a transition $t$, with $\\!~{}^{\circ}{t}$ we denote the (multi)set
$\\{{s}\mid{(s,t)\in I}\\}$ and with $\underline{t}$ the (multi)set
$\\{{s}\mid{(s,t)\in R}\\}$.

A transitions $t\in T$ is enabled at a marking $m\in\mu S$, denoted by
$m\,[\/{t}\/\rangle\,$, whenever ${\rm
Phys.~{}Rev.~{}E}{t}+\underline{t}\subseteq m$ and $\forall
s\in[\\![{\\!~{}^{\circ}{t}}]\\!].\ m(s)=0$. A transition $t$ enabled at a
marking $m$ can _fire_ and its firing produces the marking $m^{\prime}=m-{\rm
Phys.~{}Rev.~{}E}{t}+{t}{{}^{\bullet}}$. The firing of $t$ at a marking $m$ is
denoted by $m\,[\/{t}\/\rangle\,m^{\prime}$. $\underline{t}$ and
$\\!~{}^{\circ}{t}$ are the _contexts_ in which the transition $t$ may fire at
a marking $m$ provided that ${\rm Phys.~{}Rev.~{}E}{t}\subseteq m$.
$\underline{t}$ is the _positive_ context as tokens must be present in the
places connected to $t$ with a read arcs whereas $\\!~{}^{\circ}{t}$ is a
_negative_ one as no token must be present in a place connected to a
transition with an inhibitor arc. The tokens (or their absence) are just
tested. In the net in Figure 1 the transition $t_{1}$ is enabled when the
places $s_{1}$ and $s_{6}$ are marked and the place $s_{2}$ is unmarked. In
particular the token in the place $s_{6}$ is just tested for presence, whereas
the place $s_{2}$ is tested for the absence of a token.

We assume that each transition $t$ of a net $N$ is such that ${\rm
Phys.~{}Rev.~{}E}{t}\neq\emptyset$, meaning that no transition may fire
without _consuming_ some token, even if the contexts would allow it.

Given a generic marking $m$ (not necessarily the initial one), the _firing
sequence_ (shortened as fs) of $N=\langle S,T,F,I,R,\mathsf{m}\rangle$
starting at $m$ is defined as the sequence (finite or infinite)
$m_{0}\,[\/{t_{1}}\/\rangle\,m_{1}\,[\/{t_{2}}\/\rangle\,m_{2}\cdots
m_{n-1}\,[\/{t_{n}}\/\rangle\,m_{n}\cdots$ such that for all $i$ it holds that
$m_{i}\,[\/{t_{i+1}}\/\rangle\,m_{i+1}$ and where $m_{0}=m$. The set of firing
sequences of a net $N$ starting at a marking $m$ is denoted by
$\mathcal{R}^{N}_{m}$ and it is ranged over by $\sigma$. Given a fs
$\sigma=m\,[\/{t_{1}}\/\rangle\,\sigma^{\prime}$, we denote with
$\mathit{start}(\sigma)$ the marking $m$ and, if the firing sequence $\sigma$
is finite and $\sigma=m\,[\/{t_{1}}\/\rangle\,m_{1}\cdots
m_{n-1}\,[\/{t_{n}}\/\rangle\,m_{n}$, with $\mathit{lead}(\sigma)$ we denote
the marking $m_{n}$. The _length_ of a fs, written as $\mathit{len}(\sigma)$,
is defined as follows: $\mathit{len}(\sigma)=0$ if $\sigma=m$,
$\mathit{len}(\sigma)=1+\mathit{len}(\sigma^{\prime})$ if
$\sigma=m\,[\/{t}\/\rangle\,\sigma^{\prime}$ and $\sigma$ is a finite firing
sequence, and $\mathit{len}(\sigma)=\infty$ otherwise. Given a fs
$\sigma=m_{0}\,[\/{t_{1}}\/\rangle\,m_{1}\,[\/{t_{2}}\/\rangle\,m_{2}\cdots
m_{n-1}\,[\/{t_{n}}\/\rangle\,m_{n}\cdots$, with $\sigma(i)$ we denote the fs
$m_{0}\,[\/{t_{1}}\/\rangle\,m_{1}\,[\/{t_{2}}\/\rangle\,m_{2}\cdots
m_{i-1}\,[\/{t_{i}}\/\rangle\,m_{i}$ for all $i$ less or equal to the length
of the fs. Given a net $N$, a marking $m$ is _reachable_ iff there exists a fs
$\sigma\in\mathcal{R}^{N}_{\mathsf{m}}$ such that $\mathit{lead}(\sigma)$ is
$m$. The set of reachable markings of $N$ is
$\mathcal{M}_{N}=\\{{\mathit{lead}(\sigma)}\mid{\sigma\in\mathcal{R}^{N}_{\mathsf{m}}}\\}$.

######  Definition .

Let $N=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ be a labeled contextual Petri
net. Let $\sigma=\mathsf{m}\,[\/{t_{1}}\/\rangle\,m_{1}\cdots
m_{n-1}\,[\/{t_{n}}\/\rangle\,m^{\prime}$ be a fs, then
$X_{\sigma}=\sum_{i=1}^{n}\\{t_{i}\\}$ is a _state_ of $N$. The set of states
is $\mathsf{St}(N)=\\{{X_{\sigma}\in\mu
T}\mid{\sigma\in\mathcal{R}^{N}_{\mathsf{m}}}\\}$.

A state is just the multiset of the transitions that have been fired in a fs.

######  Definition .

Let $N=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ be a labeled contextual Petri
net. The set of _configurations_ of $N$, denoted with $\mathsf{Conf}(N)$, is
the set $\\{{\ell(X)}\mid{X\in\mathsf{St}(N)}\\}$.

Thus a configuration is just the multiset of labels associated to a state. If
the net belongs to a specific kind, say “net”, we may add a subscript
$\mathsf{Conf}_{\textsc{net}}(N)$ to stress that the set of configurations
refers to this kind of net.

Given a fs $\sigma$, we can extract the sequence of the fired transitions.
Formally $\mathsf{tr}(\sigma)=\epsilon$ if $\mathit{len}(\sigma)=0$ and
$\mathsf{tr}(\sigma)=\ell(t)\cdot\mathsf{tr}(\sigma^{\prime})$ if
$\sigma=m\,[\/{t}\/\rangle\,\sigma^{\prime}$.

######  Definition .

Let $N=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ be a labeled contextual Petri
net, and $\sigma\in\mathcal{R}^{N}_{\mathsf{m}}$ be a fs of $N$. Then the set
of _traces_ of $N$ is
$\mathsf{Tr}(N)=\\{{\mathsf{tr}(\sigma)}\mid{\sigma\in\mathcal{R}^{N}_{\mathsf{m}}}\\}$.

######  Example .

Consider the contextual Petri net in Figure 1. At the initial marking $t_{2}$
and $t_{3}$ are enabled whereas $t_{1}$ is not. After the execution of $t_{2}$
no other transition is enabled. After the firing of $t_{3}$ the transition
$t_{1}$ is enabled, as no token is present in the place $s_{2}$ and a token is
present in the place $s_{6}$, the former being connected to transition $t_{1}$
with an inhibitor arc and the latter being connected to transition $t_{1}$
with a read arc. The states of this net are $\\{t_{2}\\}$ and
$\\{t_{3},t_{1}\\}$. Assume now that $\ell(t_{1})=\mathsf{b}$ and
$\ell(t_{2})=\ell(t_{3})=\mathsf{a}$, then the configurations are
$\\{\mathsf{a}\\}$ and $\\{\mathsf{a},\mathsf{b}\\}$. Finally the traces of
this net are $\mathsf{a}$ and $\mathsf{a}\mathsf{b}$.

The following definitions characterize nets from a _semantical_ point of view.

######  Definition .

A net $N=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ is said to be _safe_ if
each marking $m\in\mathcal{M}_{N}$ is such that $m=[\\![{m}]\\!]$.

In this paper we will consider safe nets, where each place contains at most
one token. The following definitions outline nets with respect to states,
configurations and traces.

######  Definition .

A net $N=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ is said to be a _single
execution_ net if each state $X\in\mathsf{St}(N)$ is such that
$X=[\\![{X}]\\!]$.

In a single execution net a transition $t$ in a firing sequence may be fired
just once, as the net in Example 2.1. In [vGP95] and [vGP09] these nets
(without inhibitor and read arcs) are called _1-occurrence_ net, and the name
itself stress this characteristic.

######  Definition .

A net $N=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ is said to be an
_unfolding_ if each configuration $C\in\mathsf{Conf}(N)$ is such that
$C=[\\![{C}]\\!]$.

Clearly each unfolding is also a single execution net, but the vice versa does
not hold. Observe that if the labeling of the unfolding is an injective
mapping then states and configurations may be confused as $\mathsf{Conf}(N)$
and $\mathsf{St}(N)$ are bijectively related.

######  Remark .

In literature _unfolding_ is often used to denote not only a net with suitable
characteristic (among them the fact that each transition is fired just once in
each execution), but also how this net is related to another one (the one to
be unfolded). Here we use it to stress that each configuration is a set and
also to point out that the nets we are considering are labeled ones, and
labels suggest that a labeled transition is associated to some activity, as it
happens in _classical_ unfoldings.

We consider two nets _equivalent_ when they have the same set of transitions,
the same labeling, and the same set of states (which means that they have also
the same configurations and the same set of firing sequences).

######  Definition .

Let $N=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ and $N^{\prime}=\langle
S^{\prime},T^{\prime},F^{\prime},I^{\prime},R^{\prime},\mathsf{m}^{\prime},\ell^{\prime}\rangle$
be two nets. $N$ is _equivalent_ to $N^{\prime}$, written as $N\equiv
N^{\prime}$ whenever $T=T^{\prime}$, $\ell=\ell^{\prime}$ and
$\mathsf{St}(N)=\mathsf{St}(N^{\prime})$.

Though the equivalence relation on nets implies that the nets have the same
firing sequences, it does not imply that the sets of reachable markings is the
same, hence $N\equiv N^{\prime}$ does not imply that
$\mathcal{M}_{N}=\mathcal{M}_{N^{\prime}}$.

Observe that different traces may be associated to the same configuration of
the net. In an unfolding the following propositions hold.

######  Proposition .

Let $N=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ be an unfolding. Then, for
each $\rho\in\mathsf{Tr}(N)$ it holds that
$\overline{\rho}\in\mathsf{Conf}(N)$.

###### Proof.

In an unfolding each configuration is a set, hence the thesis. ∎

######  Proposition .

Let $N=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ be an unfolding. Then, for
each $X\in\mathsf{Conf}(N)$ there exists a trace $\rho\in\mathsf{Tr}(N)$ such
that $\overline{\rho}=X$.

###### Proof.

As $X\in\mathsf{Conf}(N)$ then there is a fs $\sigma$ such that
$X_{\sigma}=X$, and take $\rho=\mathsf{tr}(\sigma)$. By Proposition 2.1 it
follows that $\overline{\rho}=X$. ∎

The following definition give a _structural_ characterization of when two
transitions, which we say are _conflicting_ transitions, never happen together
in any execution of a net.

######  Definition .

Let $N=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ be a net. We say that $N$ is
_conflict saturated_ if for all $t,t^{\prime}\in T$ such that $\forall
X\in\mathsf{St}(N).\ \\{t,t^{\prime}\\}\not\subseteq[\\![{X}]\\!]$, it holds
that ${\rm Phys.~{}Rev.~{}E}{t}\cap{\rm
Phys.~{}Rev.~{}E}{t^{\prime}}\neq\emptyset$.

In a conflict saturated net the fact that two transitions never happen in a
state is also justified by the existence of a place in their preset, and this
suggests that in certain kind of nets conflicts can be characterized
structurally. Indeed each single execution net can be transformed into an
equivalent one conflict saturated.

######  Proposition .

Let $N=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ be a single execution net.
Let $\mathit{Confl}(N)$ be the set $\\{{\\{t,t^{\prime}\\}}\mid{\forall
X\in\mathsf{St}(N).\ \\{t,t^{\prime}\\}\not\subseteq[\\![{X}]\\!]}\\}$. Then
the net $N^{\\#}=\langle S\cup S^{\\#},T,F\cup\\{{(s_{A},t)}\mid{s_{A}\in
S^{\\#}\ \land\ t\in A}\\},I,R,\mathsf{m}\cup S^{\\#},\ell\rangle$, where
$S^{\\#}=\\{{s_{A}}\mid{A\in\mathit{Confl}(N)}\\}$, is conflict saturated and
$N\equiv N^{\\#}$.

###### Proof.

It is enough to prove that $\mathsf{St}(N)=\mathsf{St}(N^{\\#})$. Observe
first that the added places $S^{\\#}$ in $N^{\\#}$ do not have any incoming
arcs and are initially marked. This implies that
$\mathsf{St}(N^{\\#})\subseteq\mathsf{St}(N)$. For the vice versa, consider
$X\in\mathsf{St}(N)$. $X=X_{\sigma}$ for some fs
$\sigma\in\mathcal{R}^{N}_{\mathsf{m}}$. We construct, by induction on the
length of $\sigma$, a fs $\widehat{\sigma}\in\mathcal{R}^{N^{\\#}}_{m}$, with
$m=\mathsf{m}\cup S^{\\#}$, such that
$X_{\widehat{\sigma}}\in\mathsf{St}(N^{\\#})$ and $X=X_{\widehat{\sigma}}$. If
$\mathit{len}(\sigma)=0$ then $\mathit{lead}(\sigma)=\mathsf{m}$ and it
suffices to set $\widehat{\sigma}=\mathsf{m}\cup S^{\\#}$. Assume it holds for
$n$ and consider $\sigma=\sigma_{1}\,[\/{t}\/\rangle\,m$ of length $n+1$. To
$\sigma_{1}$ in $\mathcal{R}^{N}_{\mathsf{m}}$ a $\widehat{\sigma_{1}}$ in
$\mathcal{R}^{N^{\\#}}_{m}$ corresponds, so it is enough to verify that
$\mathit{lead}(\widehat{\sigma_{1}})\,[\/{t}\/\rangle\,$. If
$\neg\mathit{lead}(\widehat{\sigma_{1}})\,[\/{t}\/\rangle\,$ it should be that
a conflicting transition $t^{\prime}$ has been executed in
$\widehat{\sigma_{1}}$, but this implies that the conflicting transition has
been executed in $\sigma$ as well, which cannot be. Hence
$\mathit{lead}(\widehat{\sigma_{1}})\,[\/{t}\/\rangle\,$ and the reached
marking is $\mathit{lead}(\sigma)\cup(S^{\\#}\setminus{\rm
Phys.~{}Rev.~{}E}{X_{\sigma}})$, which implies that
$X=X_{\widehat{\sigma}}\in\mathsf{St}(N^{\\#})$. $N^{\\#}$ is then conflict
saturated by construction, as the conflicting transitions in $N^{\\#}$ are the
same as in $N$, and it equivalent to $N$ as well. ∎

A subnet of a net is a net obtained restricting places and transitions, and
correspondingly restricting also the flow and the context relations as well as
the initial marking and the labeling.

######  Definition .

Let $N=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ be a net and let
$T^{\prime}\subseteq T$ be a subset of transitions. Then the subnet generated
by $T^{\prime}$ is the net $N|_{T^{\prime}}=\langle
S^{\prime},T^{\prime},F^{\prime},I^{\prime},R^{\prime},\mathsf{m}^{\prime},\ell^{\prime}\rangle$,
where

  * •

$S^{\prime}=\\{{s\in S}\mid{\exists t\in T^{\prime}.\ (s,t)\in F\ \lor\
(t,s)\in F}\\}$,

  * •

$F^{\prime}$, $I^{\prime}$ and $R^{\prime}$ are the restriction of $F$, $I$
and $R$ to $S^{\prime}$ and $T^{\prime}$,

  * •

$\mathsf{m}^{\prime}$ is the multiset on $S^{\prime}$ obtained by $\mathsf{m}$
restricting to places in $S^{\prime}$, and

  * •

$\ell^{\prime}$ is the restriction of $\ell$ to transitions in $T^{\prime}$.

The subnet is _generated_ by a subset $T^{\prime}$ of transitions, hence the
places to be considered are those connected with the transitions in
$T^{\prime}$.

##  3\. Nets and event structures

In this section we revise and the more classical relations between nets and
event structures, in particular we recall the relationship between _occurrence
nets_ and _prime event structures_ and the one between _unravel nets_ and
_bundle event structures_. Though the latter one is not entirely _classic_ the
notion of unravel net is closely related to the one of _flow_ net and bundle
event structures to _flow_ event structures.

###  3.1. Occurrence nets and prime event structure

We recall the notion of _occurrence_ net, and as it has no inhibitor or read
arc nor a labeling, we omit $I$, $R$ and $\ell$ in the following, assuming
that $I=\emptyset=R$ and $\ell$ being the identity on transitions. Given a net
$N=\langle S,T,F,\mathsf{m}\rangle$, we write $<_{N}$ for transitive closure
of $F$. We say $N$ is _acyclic_ if $\leq_{N}$ is a partial order. For
occurrence nets, we adopt the usual convention: places and transitions are
called as _conditions_ and _events_ , and use $B$ and $E$ for the sets of
conditions and events. We may confuse conditions with places and events with
transitions. The initial marking is denoted with $\mathsf{c}$.

######  Definition .

An _occurrence net_ (on) $O=\langle B,E,F,\mathsf{c}\rangle$ is an acyclic,
safe net satisfying the following restrictions:

  * •

$\forall b\in B$. ${\rm Phys.~{}Rev.~{}E}{b}$ is either empty or a singleton,
and $\forall b\in\mathsf{c}$. ${\rm Phys.~{}Rev.~{}E}{b}=\emptyset$,

  * •

$\forall b\in B$. $\exists b^{\prime}\in\mathsf{c}$ such that
$b^{\prime}\leq_{O}b$,

  * •

for all $e\in E$ the set $\lfloor e\rfloor=\\{{e^{\prime}\in
E}\mid{e^{\prime}\leq_{O}e}\\}$ is finite, and

  * •

$\\#$ is an irreflexive and symmetric relation defined as follows:

    * –

$e\ \\#_{0}\ e^{\prime}$ iff $e,e^{\prime}\in E$, $e\neq e^{\prime}$ and ${\rm
Phys.~{}Rev.~{}E}{e}\cap{\rm Phys.~{}Rev.~{}E}{e^{\prime}}\neq\emptyset$,

    * –

$x\ \\#\ x^{\prime}$ iff $\exists y,y^{\prime}\in E$ such that $y\ \\#_{0}\
y^{\prime}$ and $y\leq_{O}x$ and $y^{\prime}\leq_{O}x^{\prime}$.

The intuition behind occurrence nets is the following: each condition $b$
represents the occurrence of a token, which is produced by the _unique_ event
in ${\rm Phys.~{}Rev.~{}E}{b}$, unless $b$ belongs to the initial marking, and
it is used by only one transition (hence if
$e,e^{\prime}\in{b}{{}^{\bullet}}$, then $e\ \\#\ e^{\prime}$). On an
occurrence net $O$ it is natural to define a notion of _causality_ among
elements of the net: we say that $x$ is _causally dependent_ on $y$ iff
$y\leq_{O}x$. Occurrence nets are often the result of the _unfolding_ of a
(safe) net. In this perspective an occurrence net is meant to describe
precisely the non-sequential semantics of a net, and each reachable marking of
the occurrence net corresponds to a reachable marking in the net to be
unfolded. Here we focus purely on occurrence nets and not on the nets they are
the unfolding of.

######  Proposition .

Let $O=\langle B,E,F,\mathsf{c}\rangle$ be an occurrence net. Then $O$ is a
single execution net and it is an unfolding.

###### Proof.

$O$ is acyclic and safe, hence no transition in $E$ can be executed more than
once, hence it is a single execution one, and it is an unfolding as
configuration and states coincide, being the _labelling_ injective. ∎

Occurrence nets are relevant as they are tightly related to _prime event
structures_ , which we briefly recall here ([Win86]).

######  Definition .

A _prime event structure ( pes)_ is a triple $\mathsf{P}=(E,<,\\#)$, where

  * •

$E$ is a countable set of _events_ ,

  * •

$<\ \subseteq E\times E$ is an irreflexive partial order called the _causality
relation_ , such that $\forall e\in E$. $\\{{e^{\prime}\in
E}\mid{e^{\prime}<e}\\}$ is finite, and

  * •

$\\#\ \subseteq E\times E$ is a _conflict relation_ , which is irreflexive,
symmetric and _hereditary_ relation with respect to $<$: if $e\ \\#\
e^{\prime}<e^{\prime\prime}$ then $e\ \\#\ e^{\prime\prime}$ for all
$e,e^{\prime},e^{\prime\prime}\in E$.

Given an event $e\in E$, $\lfloor e\rfloor$ denotes the set $\\{{e^{\prime}\in
E}\mid{e^{\prime}\leq e}\\}$. A subset of events $X\subseteq E$ is left-closed
if $\forall e\in X.\lfloor e\rfloor\subseteq X$. Given a subset $X\subseteq E$
of events, $X$ is _conflict free_ iff for all $e,e^{\prime}\in X$ it holds
that $e\neq e^{\prime}\ \Rightarrow\ \neg(e\ \\#\ e^{\prime})$, and we denote
it with $\mathsf{CF}(X)$. Given $X\subseteq E$ such that $\mathsf{CF}(X)$ and
$Y\subseteq X$, then also $\mathsf{CF}(Y)$.

######  Definition .

Let $\mathsf{P}=(E,<,\\#)$ be a pes. Then $X\subseteq E$ is a _configuration_
if $\mathsf{CF}(X)$ and $\forall e\in X.\ \lfloor e\rfloor\subseteq X$. The
set of configurations of the pes $\mathsf{P}$ is denoted by
$\mathsf{Conf}_{\textsc{pes}}(\mathsf{P})$.

Occurrence nets and prime event structures are connected as follows ([Win86]).
Proofs are omitted as they are standard and can be found in literature.

######  Proposition .

Let $O=\langle B,E,F,\mathsf{c}\rangle$ be an on, and define
$\mathcal{E}_{\textsc{on}}^{\textsc{pes}}(O)$ as the triple $(E,<_{C},\\#)$
where $<_{C}$ is the irreflexive and transitive relation obtained by $F$
restricting to $E\times E$ and $\\#$ is the irreflexive and symmetric relation
associated to $O$. Then $\mathcal{E}_{\textsc{on}}^{\textsc{pes}}(O)$ is a
pes, and
$\mathsf{Conf}_{\textsc{on}}(O)=\mathsf{Conf}_{\textsc{pes}}(\mathcal{E}_{\textsc{on}}^{\textsc{pes}}(O))$.

Also the vice versa is possible, namely given a prime event structure one can
associate to it an occurrence net. The construction is indeed quite standard
(see [Win86, BCP15] among many others).

######  Definition .

Let $\mathsf{P}=(E,\leq,\\#)$ be a pes. Define
$\mathcal{N}_{\textsc{pes}}^{\textsc{on}}(\mathsf{P})$ as the net $\langle
B,E,F,\mathsf{c}\rangle$ where

  * •

$B=\\{{(\ast,e)}\mid{e\in E}\\}\cup\\{{(e,\ast)}\mid{e\in
E}\\}\cup\\{{(e,e^{\prime},<)}\mid{e<e^{\prime}}\\}\cup\\{{(\\{e,e^{\prime}\\},\\#)}\mid{e\
\\#\ e^{\prime}}\\}$,

  * •

$F=\\{{(e,b)}\mid{b=(e,\ast)}\\}\ \cup\ \\{{(e,b)}\mid{b=(e,e^{\prime},<)}\\}\
\cup\ \\{{(b,e)}\mid{b=(\ast,e)}\\}\ \cup\
\\{{(b,e)}\mid{b=(e^{\prime},e,<)}\\}\ \cup\ \\{{(b,e)}\mid{b=(Z,\\#)\ \land\
e\in Z}\\}$, and

  * •

$\mathsf{c}=\\{{(\ast,e)}\mid{e\in
E}\\}\cup\\{{(\\{e,e^{\prime}\\},\\#)}\mid{e\ \\#\ e^{\prime}}\\}$.

######  Proposition .

Let $\mathsf{P}=(E,\leq,\\#)$ be a pes. Then
$\mathcal{N}_{\textsc{pes}}^{\textsc{on}}(\mathsf{P})=\langle
B,E,F,\mathsf{c}\rangle$ as defined in Definition 3.1 is an on, and
$\mathsf{Conf}_{\textsc{pes}}(\mathsf{P})=\mathsf{Conf}_{\textsc{on}}(\mathcal{N}_{\textsc{pes}}^{\textsc{on}}(\mathsf{P}))$

In essence an occurrence net is fully characterized by the partial order
relation and the _saturated_ conflict relation. This observation, together
with the fact that an immediate conflict in a safe net is represented by a
common place in the preset of the conflicting events, suggests that conflicts
may be modeled directly, which is the meaning of the following proposition.

######  Proposition .

Let $O=\langle B,E,F,\mathsf{c}\rangle$ be an on and let $\\#$ be the
associated conflict relation. Then $O^{\\#}=\langle B\cup B^{\\#},E,F\cup
F^{\\#},\mathsf{c}\cup B^{\\#}\rangle$ where
$B^{\\#}=\\{{\\{e,e^{\prime}\\}}\mid{e\ \\#\ e^{\prime}}\\}$ and
$F^{\\#}=\\{{(A,e)}\mid{A\in B^{\\#}\ \land\ e\in A}\\}$, is an on such that
$\mathsf{Conf}_{\textsc{on}}(O)=\mathsf{Conf}_{\textsc{on}}(C^{\\#})$.

###### Proof.

Along the same lines of Proposition 2.1. ∎

###  3.2. Unravel nets and bundle event structure

We recall the notion of _unravel_ net ([Pin11, CP14, PF20] or [CP17b]).
Similarly to on, also unravel nets do not have inhibitor arcs or read arcs,
and the labeling is injective, hence also here $I,R$ and $\ell$ are omitted.

We say that a net $N=\langle S,T,F,\mathsf{m}\rangle$ is _conflict-free_ if
$\forall s\in S$ it holds that ${s}{{}^{\bullet}}$ is at most a singleton, and
it is acyclic if the reflexive and transitive closure of $F$ is a partial
order over $S\cup T$. As we are considering safe nets we will confuse
multisets with sets.

######  Definition .

An _unravel net_ (un) $U=\langle S,T,F,\mathsf{m}\rangle$ is a safe net such
that

  * •

for each state $X\in\mathsf{St}(U)$ the net $U|_{X}$ is acyclic and conflict-
free, and

  * •

for each $t\in T$ there exists a state $X\in\mathsf{St}(U)$ such that
$t\in[\\![{X}]\\!]$.

Thus the whole unravel net is not constrained to be either acyclic or
conflict-free, but each of its executions gives an acyclic and conflict-free
net. uns can be considered as the easiest generalization of occurrence nets,
and indeed the following proposition shows that ons are uns as well, as each
execution of an on is clearly acyclic (as the whole on is acyclic) and
conflict-free. The _firability_ of each event in an occurrence net is a
consequence of the structural constraint posed on this kind of net.

######  Proposition .

Let $O$ be an on. Then $O$ is an un as well.

###### Proof.

A on $O$ is by definition acyclic, and if one consider a configuration, the
subnet generated by the transitions (events) in this configuration gives a
conflict-free one. Finally each transition (event) belongs to a configuration
as each place (condition) is connected to an initially marked one. ∎

The followings propositions will be helpful in associating a bes to an un.

######  Proposition .

Let $U=\langle S,T,F,\mathsf{m}\rangle$ be an un and let $s\in S$ such that
$s\in[\\![{\mathsf{m}}]\\!]$ then ${\rm Phys.~{}Rev.~{}E}{s}=\emptyset$.

###### Proof.

Assume ${\rm Phys.~{}Rev.~{}E}{s}\neq\emptyset$, then there exists a
transition $t\in T$ such that $t\in{\rm Phys.~{}Rev.~{}E}{s}$. Now, as $U$ is
an unravel net, $t$ can be executed, hence there exists a fs $\sigma$ such
that $\sigma\,[\/{t}\/\rangle\,m^{\prime}$. We have two cases:

  1. (1)

each transition $t^{\prime}$ in $\sigma$ is such that $s\notin{\rm
Phys.~{}Rev.~{}E}{t^{\prime}}$, but then $m^{\prime}(s)=2$, contradicting the
safeness of $U$, or

  2. (2)

there is a transition $t^{\prime}$ in $\sigma$ such that $s\in{\rm
Phys.~{}Rev.~{}E}{t^{\prime}}$, but then $U|_{[\\![{X_{\sigma}}]\\!]}$ is
cyclic, contradicting the hypothesis that $U$ is an unravel net. ∎

######  Proposition .

Let $U=\langle S,T,F,\mathsf{m}\rangle$ be an un, then $U$ is a single
execution net.

###### Proof.

Assume it is not, then there exists a state $X\in\mathsf{St}(U)$ and a
transition $t\in T$ such that $X(t)>1$. This implies that there is a fs
$\sigma$ such that
$\sigma=\sigma^{\prime}\,[\/{t}\/\rangle\,\sigma^{\prime\prime}\,[\/{t}\/\rangle\,\sigma^{\prime\prime\prime}$
but then, being $U$ a safe net, it should be that
$U|_{[\\![{X_{\sigma}}]\\!]}$ is cyclic as some transitions in
$[\\![{X_{\sigma^{\prime\prime}}}]\\!]$ should put a token in a place
$s\in{\rm Phys.~{}Rev.~{}E}{t}$, contradicting the assumption that $U$ is an
unravel net. ∎

Given an un $U=\langle S,T,F,\mathsf{m}\rangle$, we define a _semantic_
conflict relation, and we say that $t\ \\#\ t^{\prime}$ iff $\forall
X\in\mathsf{St}(U)$ it holds that
$\\{t,t^{\prime}\\}\not\subseteq[\\![{X}]\\!]$. Note that this semantic
conflict relation has already been implicitly used in showing how to construct
an equivalent conflict saturated net.

The following two propositions say that two transitions in an un are in
conflict if they have a common place either in their presets or in their
postsets. The common place in the preset suggests that their conflict is
immediate, the common place implies that only one of the two transitions can
belong to the _history_ (firing sequence) marking that place, as the proof
itself shows.

######  Proposition .

Let $U=\langle S,T,F,\mathsf{m}\rangle$ be an un, let $s\in S$ be a place and
$t,t^{\prime}\in T$ be two transitions of the un. If
${t}{{}^{\bullet}}\cap{t^{\prime}}{{}^{\bullet}}\neq\emptyset$ then $t\ \\#\
t^{\prime}$.

###### Proof.

Let $s\in{t}{{}^{\bullet}}\cap{t^{\prime}}{{}^{\bullet}}$. Assume that
$\neg(t\ \\#\ t^{\prime})$, then either there exists a fs $\sigma$ such that
$\sigma=\sigma^{\prime}\,[\/{t}\/\rangle\,\sigma^{\prime\prime}\,[\/{t^{\prime}}\/\rangle\,\sigma^{\prime\prime\prime}$
or there exists
$\sigma=\sigma^{\prime}\,[\/{t^{\prime}}\/\rangle\,\sigma^{\prime\prime}\,[\/{t}\/\rangle\,\sigma^{\prime\prime\prime}$.
Assume
$\sigma=\sigma^{\prime}\,[\/{t}\/\rangle\,\sigma^{\prime\prime}\,[\/{t^{\prime}}\/\rangle\,\sigma^{\prime\prime\prime}$.
Take the marking
$\mathit{lead}(\sigma^{\prime}\,[\/{t}\/\rangle\,\sigma^{\prime\prime})$. If
$\mathit{lead}(\sigma^{\prime}\,[\/{t}\/\rangle\,\sigma^{\prime\prime})(s)=1$
then firing $t^{\prime}$ the place $s$ get marked twice, and if
$\mathit{lead}(\sigma^{\prime}\,[\/{t}\/\rangle\,\sigma^{\prime\prime})(s)=0$
then the net $U|_{[\\![{X_{\sigma}}]\\!]}$ is not acyclic, in both cases
contradicting the assumption that $U$ is an unravel net. ∎

######  Proposition .

Let $U=\langle S,T,F,\mathsf{m}\rangle$ be an un, and let $t,t^{\prime}\in T$
be two transition of the un. Then ${\rm Phys.~{}Rev.~{}E}{t}\cap{\rm
Phys.~{}Rev.~{}E}{t^{\prime}}\neq\emptyset$ implies that $t\ \\#\ t^{\prime}$.

###### Proof.

Assume that $\neg(t\ \\#\ t^{\prime})$ and let $s\in{\rm
Phys.~{}Rev.~{}E}{t}\cap{\rm Phys.~{}Rev.~{}E}{t^{\prime}}$. Then exists a fs
$\sigma$ such that
$\sigma^{\prime}\,[\/{t}\/\rangle\,\sigma^{\prime\prime}\,[\/{t^{\prime}}\/\rangle\,\sigma^{\prime\prime\prime}$
or
$\sigma^{\prime}\,[\/{t^{\prime}}\/\rangle\,\sigma^{\prime\prime}\,[\/{t}\/\rangle\,\sigma^{\prime\prime\prime}$.
Using the same argument of Proposition 3.2 we have that $s$ would get marked
twice violating the acyclicity of $U|_{[\\![{X_{\sigma}}]\\!]}$. ∎

We recall now the notion of _bundle event structures_ [Lan93] (bes). In a bes
causality is represented by pairs $(X,e)$, the _bundles_ , where $X$ is a non
empty set of events and $e\not\in X$ an event. The meaning of a bundle
$(X,{e})$ is that if ${e}$ happens then one (and only one) event of $X$ has to
have happened before (events in $X$ are pairwise conflicting). An event ${e}$
can be caused by several bundles, in that case, for each bundle an event in it
should have happened.

######  Definition .

A _bundle event structure_ is a triple $\mathsf{B}=(E,\mapsto,\\#)$, where

  * •

${E}$ is a set of events,

  * •

$\\#$ is an irreflexive and symmetric binary relation on ${E}$ (the _conflict_
relation),

  * •

$\mapsto\ \subseteq\ \mathbf{2}_{\mathit{fin}}^{{E}}\times{E}$ is the
_enabling_ relation such that if $X\mapsto{e}$ then for all
${e}_{1},{e}_{2}\in X$. ${e}_{1}\neq{e}_{2}$ implies ${e}_{1}\ \\#\ {e}_{2}$,
and

  * •

for each ${e}\in E$ it holds that the set $\bigcup\\{{X}\mid{X\mapsto{e}}\\}$
is finite.

The final condition is an analogous of the finite cause requirement for prime
event structures. Indeed this requirement rules out situations like the
following one. Consider an event $s$ such that $\forall i\in{\rm Nature}$
there is a bundle $\\{e_{i}\\}\mapsto e$. Then the event $e$ has infinite
causes which we want to rule out.

The configurations of a bes are defined as follows.

######  Definition .

Let $\mathsf{B}=({E},\mapsto,\\#)$ be a bes and $X\subseteq{E}$ be a set of
events. Then $X$ is a _configuration_ of $\mathsf{B}$ iff

  1. (1)

it is _conflict free_ , _i.e._ $\forall{e},{e}^{\prime}\in X$.
${e}\neq{e}^{\prime}\ \Rightarrow\ \neg({e}\ \\#{e}^{\prime})$, and

  2. (2)

there exists a linearization $\\{{e}_{1},\dots,{e}_{n},\dots\\}$ of the events
in $X$ such that $\forall i\in{\rm Nature}$ and for all bundles
$X_{j_{i}}\mapsto{e}_{i}$ it holds that
$X_{j_{i}}\cap\\{{e}_{1},\dots,{e}_{i-1}\\}\neq\emptyset$.

The set of configurations of a bes $\mathsf{B}$ is denoted with
$\mathsf{Conf}_{\textsc{bes}}(\mathsf{B})$.

The requirements are the usual ones: it must be conflict free and each event
must have all of its causes. The causes of an event in a bes, as said before,
have to be chosen using all the bundles involving the event.

Clearly bes are a conservative extension of pes. Indeed each pes
$P=({E},\leq,\\#)$ can be seen as the bes stipulating that the bundles are
$\mapsto=\\{{(\\{{e^{\prime}}\\},{e})}\mid{{e^{\prime}}<{e}}\\}$. bes are more
expressive than pes, as they are able to model _or_ -causality. In fact we may
have the following bes ${a}\ \\#\ {b}$ (symmetric pair omitted) and
$\\{{a},{b}\\}\mapsto{c}$ stipulating that the same event may have two
different and alternative pasts, namely one containing ${a}$ and the other
${b}$.

Like pes and on, also bes and un are closely related. The intuition is rather
simple: to each place in the preset of a transition $t$ we associate a bundle
$X$ for the correspondent event $t$ in the event structure, and the bundle is
formed by the transitions putting a token in that place.

######  Proposition .

Let $U=\langle S,T,F,\mathsf{m}\rangle$ be an un, then
$\mathcal{E}_{\textsc{un}}^{\textsc{bes}}(U)=(T,\mapsto,\\#)$ is a bes, where

  * •

$t\ \\#\ t^{\prime}$ in $\mathcal{E}_{\textsc{un}}^{\textsc{bes}}(U)$ iff $t\
\\#\ t^{\prime}$ in $U$, and

  * •

for each $t\in T$, for each $s\in{\rm Phys.~{}Rev.~{}E}{t}$, we have ${\rm
Phys.~{}Rev.~{}E}{s}\mapsto t$.

Furthermore
$\mathsf{Conf}_{\textsc{un}}(U)=\mathsf{Conf}_{\textsc{bes}}(\mathcal{E}_{\textsc{un}}^{\textsc{bes}}(U))$.

###### Proof.

We show that $\mathcal{E}_{\textsc{un}}^{\textsc{bes}}(U)$ is indeed an bes.
The conflict relation in $\mathcal{E}_{\textsc{un}}^{\textsc{bes}}(U)$ is
antisymmetric and irreflexive because it is so in $U$. Since we are are
dealing with unravel nets, all the transitions putting tokens in the same
place are in conflict, so the bundles respect Definition 3.2. We show that
$\mathsf{Conf}_{\textsc{un}}(U)=\mathsf{Conf}_{\textsc{bes}}(\mathcal{E}_{\textsc{un}}^{\textsc{bes}}(U))$.
Consider $X\in\mathsf{Conf}_{\textsc{un}}(U)$, then there is a fs $\sigma$
such that $X_{\sigma}=X$ and for each $i\in\mathit{dom}(\mathsf{tr}(\sigma))$
we have that $\sigma(i-1)(s)=1$ for each $s\in{\rm Phys.~{}Rev.~{}E}{t_{i}}$.
It is easy to see that $\overline{\mathsf{tr}(\sigma)}$ is a configuration of
$\mathcal{E}_{\textsc{un}}^{\textsc{bes}}(U)$ as for each
$i\in\mathit{dom}(\mathsf{tr}(\sigma))$ it holds that
$\overline{\mathsf{tr}(\sigma)(i-1)}\cap{\rm
Phys.~{}Rev.~{}E}{s}\neq\emptyset$ for each ${\rm Phys.~{}Rev.~{}E}{s}\mapsto
t_{i}$. Conflict-freeness is trivial. ∎

######  Proposition .

Let $\mathsf{B}=(E,\mapsto,\\#)$ be a bes such that $\forall{e}\in{E}$
$\exists X\in\mathsf{Conf}_{\textsc{bes}}(\mathsf{B}).\ e\in X$. Then
$\mathcal{N}_{\textsc{bes}}^{\textsc{un}}(\mathsf{B})=\langle
S,E,F,\mathsf{m}\rangle$ where

  * •

$S=\\{{({e},\ast)}\mid{{e}\in E}\\}\cup\\{{\\{e,e^{\prime}\\}}\mid{{e}\ \\#\
{e}^{\prime}}\\}\cup\\{{(Y,e)}\mid{Y\mapsto{e}}\\}\cup\\{{(\ast,e)}\mid{{e}\in
E}\\}$,

  * •

$F=\\{{(s,e)}\mid{s=(e,\ast)\lor s=(Y,e)\lor
s=\\{e,e^{\prime}\\}}\\}\cup\\{{(e,s)}\mid{s=(\ast,e)\lor(s=(Y,{e}^{\prime})\land
e\in Y)}\\}$, and

  * •

$\mathsf{m}=\\{{({e},\ast)}\mid{{e}\in
E}\\}\cup\\{{\\{e,e^{\prime}\\}}\mid{{e}\ \\#\ {e}^{\prime}}\\}$

is an unravel net and
$\mathsf{Conf}_{\textsc{bes}}(\mathsf{B})=\mathsf{Conf}_{\textsc{un}}(\mathcal{N}_{\textsc{bes}}^{\textsc{un}}(\mathsf{B}))$.

###### Proof.

The safeness of $\mathcal{N}_{\textsc{bes}}^{\textsc{un}}(\mathsf{B})$ results
from the fact that the places $({e},i)$ allows only one execution of each
transitions ${e}$ as they have no incoming arc, and the places with more that
one incoming arc, the $S_{B}$ ones, cannot be marked by more than one
transition because of the conflicts in the bundle set, finally the places
$\\{e,e^{\prime}\\}$ does not allow the execution of conflicting transitions
in the same run.

Let $\sigma$ be a fs of $\mathcal{N}_{\textsc{bes}}^{\textsc{un}}(\mathsf{B})$
and be $\mathsf{tr}(\sigma)=e_{1}e_{2}e_{3}\cdots e_{n}\cdots$ the associated
trace. By induction on the indexes in $\mathit{dom}(\mathsf{tr}(\sigma))$ we
show that $\mathcal{N}_{\textsc{bes}}^{\textsc{un}}(\mathsf{B})|_{X}$ where
$X=X_{\sigma(i)}$ is a conflict-free causal net.

  * •

The empty trace gives a trivial net (a net without places and transitions)
which is vacuously a conflict-free causal net,

  * •

consider the trace $\mathsf{tr}(\sigma(n)){e}_{1}\cdots{e}_{n-1}{e}_{n}$ and
let $\overline{\mathsf{tr}(\sigma(n))}$ be the state
$\\{{e}_{1},\dots,{e}_{n-1}{e}_{n}\\}$ associated to $\mathsf{tr}(\sigma(n))$.
As $\mathsf{tr}(\sigma(n-1))={e}_{1}\cdots{e}_{n-1}$ is a trace as well, by
inductive hypothesis
$\mathcal{N}_{\textsc{bes}}^{\textsc{un}}(\mathsf{B})|_{\overline{\mathsf{tr}(\sigma(n-1))}}=\langle
S_{n-1},E_{n-1},F_{n-1},\mathsf{m}_{n-1}\rangle$ is a conflict-free causal net
where $S_{n-1}={\rm
Phys.~{}Rev.~{}E}{\overline{\mathsf{tr}(\sigma(n-1))}}\cup{\overline{\mathsf{tr}(\sigma(n-1))}}{{}^{\bullet}}$,
$E_{n-1}=\overline{\mathsf{tr}(\sigma(n-1))}$, $F_{n-1}$ is the restriction of
$F$ to the transitions in $E_{n-1}$ and the places in $S_{n-1}$, and
$\mathsf{m}_{n-1}$ is the restriction of $\mathsf{m}$ to the places in
$S_{n-1}$. Consider now that subnet
$\mathcal{N}_{\textsc{bes}}^{\textsc{un}}(\mathsf{B})|_{\overline{\mathsf{tr}(\sigma(n))}}$
and assume that a place $s$ in ${{e}_{n}}{{}^{\bullet}}$ already belongs to
$S_{n-1}$. Then $s$ must be a place of the kind $(Y,{e}_{i})$, for some
${e}_{i}\in\overline{\mathsf{tr}(\sigma(n-1))}$, but then there must be a
${e}_{j}$ in $\overline{\mathsf{tr}(\sigma(n-1))}$ such that ${e}_{j}\in Y$,
which this contradicts the fact that $\overline{\mathsf{tr}(\sigma(n-1))}$ is
conflict-free as ${e}_{j}\ \\#\ {e}_{i}$. So ${e}_{n}$ cannot mark places
already marked in the past, and the subnet
$\mathcal{N}_{\textsc{bes}}^{\textsc{un}}(\mathsf{B})|_{\overline{\mathsf{tr}(\sigma(n))}}$
is a conflict-free causal net.

The proof that
$\mathsf{Conf}_{\textsc{bes}}(\mathsf{B})=\mathsf{Conf}_{\textsc{un}}(\mathcal{N}_{\textsc{bes}}^{\textsc{un}}(\mathsf{B}))$
goes along the same reasoning of the previous proposition. ∎

##  4\. Context-Dependent Event Structure

We recall the notion of _Context-Dependent_ event structure introduced in
[Pin19] and further studied in [Pin20b]. The idea is that the happening of an
event depends on a set of modifiers (the _context_) and on a set of _real_
dependencies, which are activated by the set of modifiers. Context-Dependent
event structures are characterized by a novel _context-dependency_ relation
which subsumes all the others dependency relations studied in literature. In
presenting them we follow closely the approach taken in [Pin19] and [Pin20b],
thus we present them in their full generality and then show that the _context-
dependency_ relation can have a suitable and simpler form, yielding the notion
of _elementary_ cdes.

######  Definition .

A _context-dependent event structure_ (cdes) is a triple
$\mathsf{E}=(E,\\#,\gg)$ where

  * •

$E$ is a set of _events_ ,

  * •

$\\#\ \subseteq E\times E$ is an irreflexive and symmetric relation, called
_conflict relation_ , and

  * •

$\gg\ \subseteq\mathbf{2}^{\mathsf{A}}\times E$, where
$\mathsf{A}\subseteq\mathbf{2}_{\mathit{fin}}^{E}\times\mathbf{2}_{\mathit{fin}}^{E}$,
is a relation, called the _context-dependency_ relation (cd-relation), which
is such that for each $\mathsf{Z}\gg e$ it holds that

    * –

$\mathsf{Z}\neq\emptyset$ and $|\mathsf{Z}|$ is finite,

    * –

for each $(X,Y)\in\mathsf{Z}$ it holds that $\mathsf{CF}(X)$ and
$\mathsf{CF}(Y)$, and

    * –

for each $(X,Y),(X^{\prime},Y^{\prime})\in\mathsf{Z}$ if $X=X^{\prime}$ then
$Y=Y^{\prime}$.

The cd-relation models, for each event, which are the possible contexts in
which the event may happen (the first component of each pair) and for each
context which are the events that have to be occurred (the second component).
The idea conveyed by this relation is originated by the possibility that
dependencies of an event may vary, e.g. growing or shrinking depending on the
happening of suitable modifiers, like in the event structures presented in
[AKPN15, AKPN18], or like what happen in [vGP04] where conflicts can be
resolved. The cd-relation is capable of modeling this dynamicity. We will
later see that this dynamicity can be represented in suitable nets with
contextual arcs. The requirement posed on the $\gg$ are rather few. The first
one is that for $\mathsf{Z}\gg e$ the set $Z$ is finite and not empty. The
finiteness requirement mimics the usual requirement that an event has a finite
set of causes, whereas the non emptiness is justified by the fact that an
event need a context to happen, and though the context may be the empty one,
it should in any case be present. The second is again rather obvious, contexts
must be conflict-free subset of events. For the last one the intuition is that
for each context, the other component should be unique. The few constrains
posed on the $\gg$ relation have the drawback that this relation can be less
_informative_.

We now recall the notion of enabling of an event. We have to determine, for
each $\mathsf{Z}\gg e$, which of the contexts $X_{i}$ should be considered. To
do so we define the _context_ associated to each entry of the cd-relation.
Given $\mathsf{Z}\gg e$, where
$\mathsf{Z}=\\{(X_{1},Y_{1}),\dots,(X_{n},Y_{n})\\}$, with
$\textsc{Cxt}(\mathsf{Z})$ we denote the set of events
$\bigcup_{i=1}^{|Z|}X_{i}$, and this is the one regarding $\mathsf{Z}\gg e$.

######  Definition .

Let $\mathsf{E}=(E,\\#,\gg)$ be a cdes and $C\subseteq E$ be a subset of
events. Then the event $e\not\in C$ is _enabled_ at $C$, denoted with
$C[\/{e}\/\rangle$, if for each $\mathsf{Z}\gg e$, with
$\mathsf{Z}=\\{(X_{1},Y_{1}),\dots,(X_{n},Y_{n})\\}$, there is a pair
$(X_{i},Y_{i})\in\mathsf{Z}$ such that $\textsc{Cxt}(\mathsf{Z})\cap C=X_{i}$
and $Y_{i}\subseteq C$.

Observe that requiring the non emptiness of the set $\mathsf{Z}$ in
$\mathsf{Z}\gg e$ guarantees that an event $e$ may be enabled at some subset
of events.

######  Definition .

Let $\mathsf{E}=(E,\\#,\gg)$ be a cdes. Let $C$ be a subset of $E$. We say
that $C$ is a _configuration_ of the cdes $\mathsf{E}$ iff there exists a
sequence of distinct events $\rho=e_{1}e_{2}\cdots$ over $E$ such that

  * •

$\overline{\rho}=C$,

  * •

$\overline{\rho}$ is conflict-free, and

  * •

$\forall 1\leq i\leq\mathit{size}(\rho).\
\overline{\rho}_{i-1}[\/{e_{i}}\/\rangle$.

With $\mathsf{Conf}_{\textsc{cdes}}(\mathsf{E})$ we denote the set of
configurations of the cdes $\mathsf{E}$.

We illustrate this kind of event structure with some examples, mainly taken
from [Pin19] and [Pin20b].

######  Example .

Consider three events $\mathsf{a},\mathsf{b}$ and $\mathsf{c}$. All the events
are singularly enabled but $\mathsf{a}$ and $\mathsf{b}$ are in conflict
unless $\mathsf{c}$ has not happened (we will see later that this are called
_resolvable_ conflicts). Hence for the event $\mathsf{a}$ we stipulate

$\\{(\emptyset,\emptyset),(\\{\mathsf{b}\\},\\{\mathsf{c}\\})\\}\gg\mathsf{a}$

that should be interpreted as follows: if the context is $\emptyset$ then
$\mathsf{a}$ is enabled without any further condition (the $Y$ are the empty
set), if the context is $\\{\mathsf{b}\\}$ then also $\\{\mathsf{c}\\}$ should
be present. The set
$\textsc{Cxt}(\\{(\emptyset,\emptyset),(\\{\mathsf{b}\\},\\{\mathsf{c}\\})\\})$
is $\\{\mathsf{b}\\}$. Similarly, for the event $\mathsf{b}$ we stipulate

$\\{(\emptyset,\emptyset),(\\{\mathsf{a}\\},\\{\mathsf{c}\\})\\}\gg\mathsf{b}$

which is justified as above and finally for the event $\mathsf{c}$ we
stipulate

$\\{(\emptyset,\emptyset)\\}\gg\mathsf{c}$

namely any context allows to add the event. The empty set $\emptyset$ is a
configuration, and so are the singletons $\\{\mathsf{a}\\}$,
$\\{\mathsf{b}\\}$ and $\\{\mathsf{c}\\}$ which are reached from $\emptyset$
as $\mathsf{a},\mathsf{b}$ and $\mathsf{c}$ are enabled at this configuration,
$\\{\mathsf{a},\mathsf{c}\\}$ is a configuration and can be reached from
$\\{\mathsf{c}\\}$ adding $\mathsf{a}$ or from $\\{\mathsf{a}\\}$ adding
$\mathsf{c}$, and analogously $\\{\mathsf{b},\mathsf{c}\\}$ is a
configuration, and finally $\\{\mathsf{a},\mathsf{b},\mathsf{c}\\}$ is a
configuration that can be reached from $\\{\mathsf{a},\mathsf{c}\\}$ adding
$\mathsf{b}$ or from $\\{\mathsf{b},\mathsf{c}\\}$ adding $\mathsf{a}$.
$\\{\mathsf{a},\mathsf{b}\\}$ it is not a configuration as it cannot be
reached from $\\{\mathsf{a}\\}$ adding $\mathsf{b}$ and also from
$\\{\mathsf{b}\\}$ adding $\mathsf{c}$. In fact, to add $\mathsf{a}$ to
$\\{\mathsf{b}\\}$ one has the context $\\{\mathsf{b}\\}$ but
$\\{\mathsf{c}\\}$ is not contained in $\\{\mathsf{b}\\}$.

######  Example .

Consider three events $\mathsf{a},\mathsf{b}$ and $\mathsf{c}$, and assume
that $\mathsf{c}$ depends on $\mathsf{a}$ unless the event $\mathsf{b}$ has
occurred, and in this case this dependency is removed. Thus there is a classic
causality between $\mathsf{a}$ and $\mathsf{c}$, but it can dropped if
$\mathsf{b}$ occurs. Clearly $\mathsf{a}$ and $\mathsf{b}$ are always enabled.
The cd-relation is $\\{(\emptyset,\emptyset)\\}\gg\mathsf{a}$,
$\\{(\emptyset,\emptyset)\\}\gg\mathsf{b}$ and
$\\{(\emptyset,\\{\mathsf{a}\\}),(\\{\mathsf{b}\\},\emptyset)\\}\gg\mathsf{c}$.
In this case the configurations are $\emptyset$, $\\{\mathsf{a}\\}$,
$\\{\mathsf{b}\\}$, $\\{\mathsf{a},\mathsf{c}\\}$ (reachable from
$\\{\mathsf{a}\\}$), $\\{\mathsf{b},\mathsf{c}\\}$ (reachable from
$\\{\mathsf{b}\\}$), $\\{\mathsf{a},\mathsf{b}\\}$ and
$\\{\mathsf{a},\mathsf{b},\mathsf{c}\\}$ (reachable from
$\\{\mathsf{a},\mathsf{b}\\}$, $\\{\mathsf{b},\mathsf{c}\\}$ and
$\\{\mathsf{a},\mathsf{c}\\}$).

######  Example .

Consider three events $\mathsf{a},\mathsf{b}$ and $\mathsf{c}$, and assume
that $\mathsf{c}$ depends on $\mathsf{a}$ just when the event $\mathsf{b}$ has
occurred, and in this case this dependency is added, otherwise it may happen
without. Thus classic causality relation between $\mathsf{a}$ and $\mathsf{c}$
is added if $\mathsf{b}$ occurs. Again $\mathsf{a}$ and $\mathsf{b}$ are
always enabled. The cd-relation is $\\{(\emptyset,\emptyset)\\}\gg\mathsf{a}$,
$\\{(\emptyset,\emptyset)\\}\gg\mathsf{b}$ and
$\\{(\emptyset,\emptyset),(\\{\mathsf{b}\\},\\{\mathsf{a}\\})\\}\gg\mathsf{c}$.
The configurations of this cdes are $\emptyset$, $\\{\mathsf{a}\\}$,
$\\{\mathsf{b}\\}$, $\\{\mathsf{c}\\}$, $\\{\mathsf{a},\mathsf{c}\\}$
(reachable from $\\{\mathsf{a}\\}$), $\\{\mathsf{a},\mathsf{b}\\}$ and
$\\{\mathsf{a},\mathsf{b},\mathsf{c}\\}$, which is for instance reachable from
$\\{\mathsf{a},\mathsf{b}\\}$ adding $\mathsf{c}$. The configuration
$\\{\mathsf{b},\mathsf{c}\\}$ is reachable from $\\{\mathsf{c}\\}$ adding
$\mathsf{b}$ but not from the configuration $\\{\mathsf{b}\\}$.

These examples should clarify how the cd-relation is used and also that each
event may be _implemented_ by a different pair $(X,Y)$ of modifiers and
dependencies.

In [Pin19] and [Pin20b] we have shown that many event structures can be seen
as a cdes, and this is obtained taking the configurations of an event
structure and from these synthesizing the conflict and the $\gg$ relations.

To characterize how the configurations of a cdes are organized we recall the
notion of _event automaton_ [PP95].

######  Definition .

Let $E$ be a set of _events_. An _event automaton_ over $E$ (ea) is the tuple
$\mathsf{A}=\langle E,\mathsf{S},\rightarrowtail,\mathit{s}_{0}\rangle$ such
that

  * •

$\mathsf{S}\subseteq\mathbf{2}^{E}$, and

  * •

$\rightarrowtail\subseteq\mathsf{S}\times\mathsf{S}$ is such that
$s\rightarrowtail s^{\prime}$ implies that $s\subset s^{\prime}$.

$\mathit{s}_{0}\in\mathsf{S}$ is the initial state.

An event automaton is just a set of subsets of events and a reachability
relation $\rightarrowtail$ with the minimal requirements that if two states
$s,s^{\prime}$ are related by the $\rightarrowtail$ relation, namely
$s\rightarrowtail s^{\prime}$, then $s^{\prime}$ is _reached_ by $s$ adding at
least one event.

In [Pin19, Pin20b] we have proven that, given a cdes $\mathsf{E}=(E,\\#,\gg)$,
the quadruple $\langle E,\mathsf{S},\rightarrowtail,\mathit{s}_{0}\rangle$,
where $\mathsf{S}=\mathsf{Conf}_{\textsc{cdes}}(\mathsf{E})$,
$\rightarrowtail\subseteq\mathsf{Conf}_{\textsc{cdes}}(\mathsf{E})\times\mathsf{Conf}_{\textsc{cdes}}(\mathsf{E})$
is such that $C\rightarrowtail C^{\prime}$ iff $C^{\prime}\setminus C=\\{e\\}$
and $\mathit{s}_{0}=\emptyset$, is an ea. The event automaton associated to
$\mathsf{E}$ is denoted with $\mathcal{A}(\mathsf{E})$.

With the aid of ea we can establish when two cdes are _equivalent_.

######  Definition .

Let $\mathsf{E}=(E,\\#,\gg)$ and
$\mathsf{E}^{\prime}=(E^{\prime},\\#^{\prime},\gg^{\prime})$ be two cdes. Then
$\mathsf{E}$ is _equivalent_ to $\mathsf{E}^{\prime}$, written as
$\mathsf{E}\cong\mathsf{E}^{\prime}$, whenever $E=E^{\prime}$ and
$\mathcal{A}(\mathsf{E})=\mathcal{A}(\mathsf{E}^{\prime})$.

We list some property an ea may enjoy.

######  Definition .

Let $\mathsf{A}=\langle E,\mathsf{S},\rightarrowtail,\mathit{s}_{0}\rangle$ be
an ea. We say that $\mathsf{A}$ is _simple_ if $\forall e\in E$. $\exists
s\in\mathsf{S}$ such that $s\cup\\{e\\}\in\mathsf{S}$, $s\rightarrowtail
s\cup\\{e\\}$ and $s\in\mathbf{2}_{\mathit{fin}}^{E}$.

In a simple event automaton, for each event, there is a finite state such that
this can be reached by adding just this event.

On states of an ea we can define an operator
$\mathsf{reach}(X)=\\{\mathit{s}_{0}\\}\cup\\{{s^{\prime}\in\mathsf{S}}\mid{\exists
s\in X.\ s\rightarrowtail s^{\prime}}\\}$, and this is clearly a monotone and
continuous operator on subset of states, hence we can calculate the least
fixed point of it, namely $\mathit{lfp}(\mathsf{reach})$

######  Definition .

Let $\mathsf{A}=\langle E,\mathsf{S},\rightarrowtail,\mathit{s}_{0}\rangle$ be
an ea. We say that the event automaton $\mathsf{A}$ is _complete_ iff
$\mathit{lfp}(\mathsf{reach})=\mathsf{S}$.

In a complete ea each state is reachable from the initial one.

######  Definition .

Let $\mathsf{A}=\langle E,\mathsf{S},\rightarrowtail,\mathit{s}_{0}\rangle$ be
an ea. We say that $\mathsf{A}$ is _finitely caused_ if $\forall{e}\in E$.
$\exists\mathcal{C}(\mathsf{A},e)=\\{X_{1},\dots,X_{n}\\}$ such that each
$X_{i}\in\mathbf{2}_{\mathit{fin}}^{E}$ and $\forall s\in\mathsf{S}$. if
$s\rightarrowtail s\cup\\{e\\}$ then $\exists X\in\mathcal{C}(\mathsf{A},e)$
and $X\subseteq s$.

In a finitely caused ea each event that can be added to a state has a finite
number of justifying subsets, which again resemble a kind of finite causes
principle. We observe that in a finitely caused ea $\mathsf{A}$ the sets
$\mathcal{C}(\mathsf{A},e)$ can be effectively calculated.

Beside the notion of finitely caused we have to stipulate that an event cannot
be _inhibited_ in different infinite ways: we want to rule out the case that
the event $e$ is such that $\mathsf{Z}\gg e$ with $\mathsf{Z}$ infinite, as it
would be, for instance, in an ea with states $\emptyset,\bigcup_{i\in{\rm
Nature}}\\{e_{i}\\}$ and $\bigcup_{i\in{\rm Nature}}\\{e_{i},e\\}$ with
$\rightarrowtail$ defined as $\emptyset\rightarrowtail\\{e_{i}\\}$ and
$\\{e_{i}\\}\rightarrowtail\\{e_{i},e\\}$. In this ea the event $e$ can be
added to each singleton state, and the unique context allowing it would be the
empty one, and these states are infinite.

######  Definition .

Let $\mathsf{A}=\langle E,\mathsf{S},\rightarrowtail,\mathit{s}_{0}\rangle$ be
an ea. We say that $\mathsf{A}$ is _finitely inhibited_ if $\forall{e}\in E$
the set $\mathcal{I}(\mathsf{A},e)=\\{{s\in\mathsf{S}}\mid{e\not\in s\ \land\
\exists s^{\prime}\in\mathsf{S}.\ s\cup\\{e\\}\subseteq s^{\prime}\ \land\
\forall s^{\prime}\in\mathsf{S}.\ e\in s^{\prime}\ \Rightarrow\
\neg(s\rightarrowtail s^{\prime})}\\}$ is finite.

The intuition behind a finitely inhibited ea $\mathsf{A}$ is the indeed the
one hinted before: the number of states $s$ where an event $e$ cannot be added
but there is another containing both the events in $s$ and $e$ is finite.

######  Proposition .

Let $\mathsf{E}=(E,\\#,\gg)$ be a cdes and let $\mathcal{A}(\mathsf{E})$ be
the associated ea. Then $\mathcal{A}(\mathsf{E})$ is simple, complete,
finitely caused and finitely inhibited.

###### Proof.

$\mathcal{A}(\mathsf{E})$ is simple as each event $e$ belongs to a
configuration $C$ and to $C$ a sequence $\rho=e_{1}e_{2}\cdots$ is associated.
Assume $e$ is $e_{i}$ then $\overline{\rho_{i-1}}$ is a state and
$\overline{\rho_{i-1}}\rightarrowtail\overline{\rho_{i-1}}\cup\\{e\\}$.
Completeness depends on the fact that each configuration is reachable. The
fact that it is finitely caused depends on the finiteness of $\mathsf{Z}$. The
finiteness of $\mathsf{Z}$ for each event in the $\gg$ relation implies also
that $\mathcal{A}(\mathsf{E})$ is finitely inhibited as otherwise there would
be infinite states where an event can be added and these states have nothing
in common, which contradicts the fact that $\mathcal{A}(\mathsf{E})$ is
finitely caused. ∎

On the events of an ea it is easy to define an irreflexive and symmetric
conflict relation.

######  Definition .

Let $\mathsf{A}=\langle E,\mathsf{S},\rightarrowtail,\mathit{s}_{0}\rangle$ be
an ea. We define a symmetric and irreflexive conflict relation
$\\#_{\textsc{ea}}$ as follows: $e\ \\#_{\textsc{ea}}\ e^{\prime}$ iff for
each $s\in\mathsf{S}$. $\\{e,e^{\prime}\\}\not\subseteq s$.

We show how to associate to an ea a cdes.

######  Theorem .

Let $\mathsf{A}=\langle E,\mathsf{S},\rightarrowtail,\mathit{s}_{0}\rangle$ be
a simple, complete, finitely caused and finitely inhibited ea such that
$E=\bigcup_{s\in\mathsf{S}}s$. Then
$\mathcal{F}_{\textsc{ea}}({\mathsf{A}})=(E,\\#,\gg)$ is a cdes, where $\\#$
is the relation $\\#_{\textsc{ea}}$ of Definition 4, and for each $e\in E$ we
have
$\\{{(X,\emptyset)}\mid{X\in\mathcal{C}(\mathsf{A},e)}\\}\cup\\{{(X,\\{e\\})}\mid{X\in\mathcal{I}(\mathsf{A},e)}\\}\gg
e$, and $\mathcal{A}(\mathcal{F}_{\textsc{ea}}({\mathsf{A}}))=\mathsf{A}$.

###### Proof.

Along the same line of Theorem 4.12 of [Pin20b]. ∎

We show here that it is possible to obtain the $\gg$ relation where for each
event $e$ there is just one entry $\mathsf{Z}\gg e$.

######  Definition .

Let $\mathsf{E}=(E,\\#,\gg)$ be a cdes. We say that $\mathsf{E}$ is
_elementary_ if $\forall e\in E$ there is just one entry $\mathsf{Z}\gg e$.

The cdes in the Examples 4, 4 and 4 are elementary ones.

######  Theorem .

Let $\mathsf{E}=(E,\\#,\gg)$ be a cdes. Then there exists a elementary cdes
$\mathsf{E}^{\prime}=(E,\\#^{\prime},\gg^{\prime})$ such that
$\mathsf{Conf}_{\textsc{cdes}}(\mathsf{E})=\mathsf{Conf}_{\textsc{cdes}}(\mathsf{E}^{\prime})$.

###### Proof.

It is enough to observe that the cdes obtained in Theorem 4 is an elementary
one. ∎

We assume that the cdes we will consider are elementary ones.

##  5\. Causal nets

We introduce a notion that will play the same role of occurrence net or
unravel net when related to context-dependent event structure.

Given a contextual Petri net $N=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$, we
can associate to it a relation on transitions, denoted with $\prec_{N}$ and
defined as $t\prec_{N}t^{\prime}$ when ${\rm
Phys.~{}Rev.~{}E}{t}\cap\\!~{}^{\circ}{t^{\prime}}\neq\emptyset$ or
${t}{{}^{\bullet}}\cap\underline{t^{\prime}}\neq\emptyset$, with the aim of
establishing the _dependencies_ among transitions related by inhibitor or read
arcs. Similarly we can introduce a conflict relation among transitions, which
is a _semantic_ one. For this is enough to stipulate that two transitions
$t,t^{\prime}\in T$ are in conflict, denoted with $t\ \\#_{N}\ t^{\prime}$ if
$\forall X\in\mathsf{St}(N).\ \\{t,t^{\prime}\\}\not\subseteq[\\![{X}]\\!]$.
With the aid of these relations we can introduce the notion of pre-_causal_
net.

######  Definition .

Let $N=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ be a labeled Petri net over
the set of label $\mathsf{L}$. Then $N$ is a pre-_causal_ net (pcn net) if the
following further conditions are satisfied:

  1. (1)

$<_{N}\cap(T\times T)=\emptyset$, $\forall t\in T$. ${\rm
Phys.~{}Rev.~{}E}{t}\cap\\!~{}^{\circ}{t}=\emptyset$ and
${t}{{}^{\bullet}}\cap\underline{t}=\emptyset$,

  2. (2)

$\forall t\in T.\ \forall s\in\\!~{}^{\circ}{t}.\
|\ell({s}{{}^{\bullet}})|=1$,

  3. (3)

$\forall t,t^{\prime}\in T$, $t\prec_{N}t^{\prime}\ \Rightarrow
t^{\prime}\not\prec_{N}t$,

  4. (4)

$\forall t\in T$ the set $\\!~{}^{\circ}{t}\cup\underline{t}$ is finite,

  5. (5)

$\forall t,t^{\prime}\in T.\ t\ \\#_{N}\ t^{\prime}\ \Rightarrow\ {\rm
Phys.~{}Rev.~{}E}{t}\cap{\rm Phys.~{}Rev.~{}E}{t^{\prime}}\neq\emptyset$, and

  6. (6)

$\forall t,t^{\prime}\in T.\ (t\neq t^{\prime}\ \land\
\ell(t)=\ell(t^{\prime}))\ \Rightarrow\ t\ \\#_{N}\ t^{\prime}$.

The first requirement implies that $\forall t,t^{\prime}\in T$ we have that
${t}{{}^{\bullet}}\cap{\rm Phys.~{}Rev.~{}E}{t}^{\prime}=\emptyset$, hence in
this kind of net the dependencies do not arise from the flow relation,
furthermore inhibitor and read arcs do not interfere with the flow relation.
The second condition implies that if a token in a place inhibits the happening
of a transition, then all the transitions removing this token have the same
label, the third is meant to avoid cycles between transitions arising from
inhibitor and read arcs, the fourth one implies that for each transition $t$
the set $\\{{t^{\prime}\in T}\mid{t^{\prime}\prec_{U}t}\\}$ is finite, the
fifth one stipulates that two conflicting transitions (which never appear
together in any execution of the net) consume the same token from a place, and
the last one that two different transitions bearing the same label are in
conflict.

######  Example .

Consider the net below. It is a pcn. Condition (2) of the definition is
fulfilled as, for instance, considering
$\\!~{}^{\circ}{t_{4}}=\\{s_{3},s_{1}\\}$, we have that all the transitions in
${s_{1}}{{}^{\bullet}}$ have the same label, and similarly for the unique
transition in ${s_{3}}{{}^{\bullet}}$. Condition (3) is fulfilled as we have,
e.g., $t_{1}\prec t_{3}$ as
${t_{3}}{{}^{\bullet}}\cap\underline{t_{1}}\neq\emptyset$, $t_{1}\prec t_{4}$
as ${\rm Phys.~{}Rev.~{}E}{t_{1}}\cap\\!~{}^{\circ}{t_{4}}\neq\emptyset$, and
$t_{2}\prec t_{4}$ as ${\rm
Phys.~{}Rev.~{}E}{t_{2}}\cap\\!~{}^{\circ}{t_{4}}\neq\emptyset$, but never the
vice versa. Also the other conditions are easily checked.

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

Based on the notion of pcn we can introduce the one of _causal_ net.

######  Definition .

Let $K=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ be a pre-_causal_ net over
the set of label $\mathsf{L}$. Then $K$ is a _causal_ net (cn net) if

  1. (1)

$\forall X\in\mathsf{St}(K)$ $\prec_{K}^{\ast}$ is a partial order on $X$, and

  2. (2)

$\forall t\in T\ \exists X\in\mathsf{St}(K).\ t\in[\\![{X}]\\!]$.

The added conditions with respect to the ones in Definition 5 implies that the
executions of the transitions in a fs is compatible with the dependency
relation when the transitions in the state associated to the fs are
considered, and each transition can be executed. The pcn in Example 5 is a cn
as each transition can be executed and the transitive closure of the $\prec$
relation is a partial order on states.

From the previous example it should be clear that the conditions posed on pre-
causal nets and causal nets are meant to mimic some of the conditions posed on
an occurrence nets (e.g. finiteness of causes) or on similar one, like for
instance _unravel_ nets or flow nets ([Bou90]), e.g. that when considering an
execution, an order can be found among the various transitions, and they
should assure that it is comprehensible what a computation in such a net can
be looking at labels, as the main intuition is that for the same activity
(label) there may be several incarnations. In fact, differently from ons and
uns, the labeling mapping is not necessarily the identity and if two
transitions share a place, then they are in conflict.

######  Example .

The following one is a causal net:

$t_{1}$$\mathsf{b}$$t_{2}$$\mathsf{c}$$t_{3}$$\mathsf{c}$$t_{4}$$\mathsf{a}$

All the conditions of Definitions 5 and 5 are fulfilled. The two transitions
bearing the same label ($t_{2}$ and $t_{3}$) are conflicting ones, namely they
never appear together in any computation though the activity realized by these
two transitions ($\mathsf{c}$) appears in all maximal computations.

The first observation we make on causal nets is that they are good candidates
to be seen as a _semantic_ net, namely a net meant to represent the behaviour
of a system properly modeling dependencies and conflicts of any kind.

######  Proposition .

Let $K=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ be a causal net. Then $K$ is
conflict saturated.

###### Proof.

A pre-causal net is conflict saturated by construction, as it is required that
two conflicting transitions share a place in their presets. ∎

######  Proposition .

Let $K=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ be a causal net. Then $K$ is
an single execution net.

###### Proof.

Obvious, as $\forall t,t^{\prime}\in T$ it holds that
${t}{{}^{\bullet}}\cap{\rm Phys.~{}Rev.~{}E}{t^{\prime}}=\emptyset$ hence once
that a transition is executed the places in its preset cannot be marked again.
∎

######  Proposition .

Let $K=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ be a causal net. Then $K$ is
an unfolding.

###### Proof.

The transitions bearing the same label are in conflict, hence the thesis. ∎

In the following we show that classical notions like occurrence nets or
unravel nets can be seen as causal ones, showing that this notion is adequate
to be related to prime or bundle event structures. In the next section we will
see that it is also suitable to be related to cdes as well.

###  5.1. Occurrence nets and causal nets

We show that each occurrence net can be turned into a causal one, thus this is
a conservative extension of this notion. The idea behind the construction is
simple: to each event of the occurrence net a transition in the causal net is
associated, the places in the preset of all transitions are initially marked
and they are not in the postset of any other transition. The dependencies
between events are modeled using inhibitor arcs. All the conflicts are modeled
like in a conflict saturated net (with suitable marked places).

######  Proposition .

Let $O=\langle B,E,F,\mathsf{c}\rangle$ be an occurrence net. The net
$\mathcal{G}_{\textsc{on}}(O)$ defined as $\langle
S,E,F^{\prime},I,\emptyset,\mathsf{m},\ell\rangle$ where

  * •

$S=\\{{(\ast,e)}\mid{e\in E}\\}\cup\\{{(e,\ast)}\mid{e\in
E}\\}\cup\\{{\\{e,e^{\prime}\\}}\mid{e\ \\#\ e^{\prime}}\\}$,

  * •

$F^{\prime}=\\{{(s,e)}\mid{s=(\ast,e)}\\}\cup\\{{(s,e)}\mid{e\in
s}\\}\cup\\{{(e,s)}\mid{s=(e,\ast)}\\}$,

  * •

$I=\\{{(s,e)}\mid{s=(\ast,e^{\prime})\ \land\ e^{\prime}<_{O}e}\\}$,

  * •

$\mathsf{m}:S\to{\rm Nature}$ is such that $\mathsf{m}(s)=0$ if $s=(e,\ast)$
and $\mathsf{m}(s)=1$ otherwise, and

  * •

$\ell$ is the identity,

is a causal net over the set of label $E$, and
$\mathsf{Conf}_{\textsc{on}}(O)=\mathsf{Conf}_{\textsc{cn}}(\mathcal{G}_{\textsc{on}}(O))$.

###### Proof.

First we recall that the labeling mapping is the identity, therefore states
and configurations coincide. An easy inspection show that the conditions of
Definition 5 are fulfilled by construction. Consider
$X\in\mathsf{St}(\mathcal{G}_{\textsc{on}}(O))$ and assume that
$\prec^{\ast}_{\mathcal{G}_{\textsc{on}}(O)}$ is not a partial order. Then we
have that for some $e,e^{\prime}\in[\\![{X}]\\!]$, with $e\neq e^{\prime}$ we
have that $e\prec^{\ast}_{\mathcal{G}_{\textsc{on}}(O)}e^{\prime}$ and
$e^{\prime}\prec^{\ast}_{\mathcal{G}_{\textsc{on}}(O)}e$. Without loss of
generality we can assume that
$e\prec_{\mathcal{G}_{\textsc{on}}(O)}e^{\prime}$ and
$e^{\prime}\prec_{\mathcal{G}_{\textsc{on}}(O)}e$, but as
$\mathcal{G}_{\textsc{on}}(O)$ is a pre-causal net by construction, this is
impossible. $\mathcal{G}_{\textsc{on}}(O)$ satisfies also the other
requirement of Definition 5, as clearly each transition can be executed.
Assume that there is a transition $e$ in $\mathcal{G}_{\textsc{on}}(O)$ which
is never executed, but it is in $O$, as the latter is an occurrence net. As
$e$ is executable in $O$ there is a firing sequence
$\sigma=\sigma^{\prime}\,[\/{e}\/\rangle\,m$ and the trace associated to this
fs $\mathsf{tr}(\sigma)$ is such that $\overline{\mathsf{tr}(\sigma)}=\lfloor
e\rfloor$. Now assume that for each $i<\mathit{size}(\mathsf{tr}(\sigma))$ it
holds that $\mathsf{tr}(\sigma)(i)=e_{i}$ can be executed also in
$\mathcal{G}_{\textsc{on}}(O)$, and $\\!~{}^{\circ}{e}$ in
$\mathcal{G}_{\textsc{on}}(O)$ contains precisely the places
$\\{{(e_{i},\ast)}\mid{e_{i}\in\overline{\mathsf{tr}(\sigma)}}\\}$, which
implies that also $e$ is executable in $\mathcal{G}_{\textsc{on}}(O)$.

To show that
$\mathsf{Conf}_{\textsc{on}}(O)=\mathsf{Conf}_{\textsc{cn}}(\mathcal{G}_{\textsc{on}}(O))$
we prove that if $X\in\mathsf{Conf}_{\textsc{on}}(O)$ then $\mathsf{m}-{\rm
Phys.~{}Rev.~{}E}{X}+{X}{{}^{\bullet}}$ is a reachable marking in
$\mathcal{G}_{\textsc{on}}(O)$. The proof is done by induction of the size of
$X$. If $X$ is the emptyset then we are done. Assume it holds for
$\mathit{size}(X)=n$, hence $m^{\prime}=\mathsf{m}-{\rm
Phys.~{}Rev.~{}E}{X}+{X}{{}^{\bullet}}$ is a reachable marking in
$\mathcal{G}_{\textsc{on}}(O)$. Consider now the configuration $X\cup\\{e\\}$
for some $e\in E$. As it is a configuration we know that $\lfloor
e\rfloor\subseteq X$, hence for all $e^{\prime}\in\lfloor e\rfloor$ we have
that $m^{\prime}((\ast,e))=0$, hence $m^{\prime}\,[\/{e}\/\rangle\,(m-{\rm
Phys.~{}Rev.~{}E}{e}\cup{e}{{}^{\bullet}})$, which means that to
$X\cup\\{e\\}\in\mathsf{Conf}_{\textsc{on}}(O)$ a reachable marking in
$\mathcal{G}_{\textsc{on}}(O)$ corresponds, and the thesis holds. The vice-
versa, namely that if
$X\in\mathsf{Conf}_{\textsc{cn}}(\mathcal{G}_{\textsc{on}}(O))$ then also
$X\in\mathsf{Conf}_{\textsc{on}}(O)$, is proved analogously. ∎

Below we depict a simple occurrence net (on the left) and the associated
causal one. The causal net on the right is conflict saturated.

$\mathsf{a}$$\mathsf{b}$$\mathsf{c}$$\mathsf{a}$$\mathsf{b}$$\mathsf{c}$

Dependencies in a causal net corresponding to an occurrence net are here
represented with inhibitor arcs, but an alternative choice would have been to
use read arcs instead. Thus if $e<_{O}e^{\prime}$ in the occurrence net,
instead of stipulating the existence of an inhibitor arc connecting the place
$(\ast,e)$ to the transition $e$, one can introduce a read arc from the place
$(e,\ast)$ to the transition $e$.

The obvious consequence of the previous Proposition is the following one.

######  Proposition .

Let $O$ be an occurrence net and $\mathcal{G}_{\textsc{on}}(O)$ be the
associated causal net. Then $\mathcal{G}_{\textsc{on}}(O)$ is an unfolding.

We remark that in a causal net, it is a bit more tiring to dig out
dependencies with respect to what happens in an occurrence net.

The causal nets corresponding to occurrence nets have some further
characteristic. In fact the dependency relation $\prec$ and the conflict
relation have a particular shape.

######  Definition .

Let $K=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ be a causal net. $K$ is said
to be an _occurrence causal_ net whenever $R=\emptyset$, $\ell$ is injective,
$\prec^{\ast}_{K}$ is a partial order over $T$, and if $t\ \\#_{K}\
t^{\prime}\prec^{\ast}_{K}t^{\prime\prime}$ then $t\ \\#_{K}\
t^{\prime\prime}$.

The above definition simply guarantees that the dependencies give a partial
order and that the conflict relation is inherited along the reflexive and
transitive closure of the dependency relation.

######  Proposition .

Let $O$ be an occurrence net and $\mathcal{G}_{\textsc{on}}(O)$ be the
associated causal net. Then $\mathcal{G}_{\textsc{on}}(O)$ is an occurrence
causal net.

###### Proof.

By construction $R=\emptyset$ and $\ell$ is the identity, hence it it
injective. $\prec^{\ast}_{\mathcal{G}_{\textsc{on}}(O)}$ is a partial order as
we have that $e\prec_{\mathcal{G}_{\textsc{on}}(O)}e^{\prime}$ when
$(\ast,e)\in\\!~{}^{\circ}{e^{\prime}}$ and this happen if $e<e^{\prime}$ in
the occurrence net $O$, thus $\prec^{\ast}_{\mathcal{G}_{\textsc{on}}(O)}$ is
a partial order as $<$ is a partial order. As $\mathcal{G}_{\textsc{on}}(O)$
is conflict saturated, it is clear that conflicts are inherited along the
$\prec^{\ast}_{\mathcal{G}_{\textsc{on}}(O)}$ relation. ∎

###  5.2. Causal nets and prime event structure

Proposition 5.1, together with the connection among pes and on (Definition 3.1
and Proposition 3.1), suggests that a relation between pes and cn can be
established. Here the intuition is to use the same construction hinted in
Proposition 5.1.

######  Definition .

Let $\mathsf{P}=(E,<,\\#)$ be a pes. Define
$\mathcal{N}_{\textsc{pes}}^{\textsc{cn}}(\mathsf{P})$ as the labeled
contextual Petri net $\langle S,E,F,I,\emptyset,\mathsf{m},\ell\rangle$ where

  * •

$S=\\{{(\ast,e)}\mid{e\in E}\\}\cup\\{{(e,\ast)}\mid{e\in
E}\\}\cup\\{{(\\{e,e^{\prime}\\},\\#)}\mid{e\ \\#\ e^{\prime}}\\}$,

  * •

$F=\\{{(e,s)}\mid{s=(e,\ast)}\\}\ \cup\ \\{{(s,e)}\mid{s=(\ast,e)\lor\
(s=(W,\\#)\ \land\ e\in W)}\\}$,

  * •

$I=\\{{(s,e)}\mid{s=(\ast,e^{\prime})\ \land\ e^{\prime}<e}\\}$,

  * •

$\mathsf{m}=\\{{(\ast,e)}\mid{e\in
E}\\}\cup\\{{(\\{e,e^{\prime}\\},\\#)}\mid{e\ \\#\ e^{\prime}}\\}$, and

  * •

$\ell$ is the identity.

######  Proposition .

Let $\mathsf{P}$ be a pes, and
$\mathcal{N}_{\textsc{pes}}^{\textsc{cn}}(\mathsf{P})$ be the associated Petri
net. Then $\mathcal{N}_{\textsc{pes}}^{\textsc{cn}}(\mathsf{P})$ is a causal
net and
$\mathsf{Conf}_{\textsc{pes}}(\mathsf{P})=\mathsf{Conf}_{\textsc{cn}}(\mathcal{N}_{\textsc{pes}}^{\textsc{cn}}(\mathsf{P}))$.

###### Proof.

Trivial, by observing that
$\mathcal{N}_{\textsc{pes}}^{\textsc{cn}}(\mathsf{P})$ is the same
construction of Proposition 5.1. ∎

The construction gives an occurrence causal net.

######  Proposition .

Let $\mathsf{P}$ be a pes, and
$\mathcal{N}_{\textsc{pes}}^{\textsc{cn}}(\mathsf{P})$ be the associated Petri
net. Then $\mathcal{N}_{\textsc{pes}}^{\textsc{cn}}(\mathsf{P})$ is an
occurrence causal net.

###### Proof.

Easy inspection of the construction in Definition 5.2. ∎

We show that also the vice versa is feasible provided that we restrict our
attention to occurrence causal net.

######  Proposition .

Let $K=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ be an occurrence causal net.
Then $\mathcal{E}_{\textsc{cn}}^{\textsc{pes}}(K)=(T,\prec^{+}_{K},\\#_{K})$
is a pes, and
$\mathsf{Conf}_{\textsc{cn}}(K)=\mathsf{Conf}_{\textsc{pes}}(\mathcal{E}_{\textsc{cn}}^{\textsc{pes}}(K))$.

###### Proof.

We have just to show that
$\mathsf{Conf}_{\textsc{cn}}(K)=\mathsf{Conf}_{\textsc{pes}}(\mathcal{E}_{\textsc{cn}}^{\textsc{pes}}(K))$,
as $\prec^{+}_{K}$ is a partial order being $K$ an occurrence causal net and
it is inherited along the conflict relation $\\#_{K}$. Take
$X\in\mathsf{Conf}_{\textsc{cn}}(K)$, then we have that $X$ is conflict free
and for each $t\in X$ it holds that all the transitions $t^{\prime}\prec_{K}t$
have been executed as $t^{\prime}={s}{{}^{\bullet}}$ for
$s\in\\!~{}^{\circ}{t}$, but this account to say that $\lfloor
t\rfloor\subseteq X$ and this prove that
$X\in\mathsf{Conf}_{\textsc{pes}}(\mathcal{E}_{\textsc{cn}}^{\textsc{pes}}(K))$
as well. For the other inclusion, consider
$X\in\mathsf{Conf}_{\textsc{pes}}(\mathcal{E}_{\textsc{cn}}^{\textsc{pes}}(K))$.
$X$ can be seen as the sequence $t_{1}t_{2}t_{3}\dots$ compatible with
$\prec_{K}$. Take $t_{n}\in X$, we show that $m_{n}\,[\/{t_{n}}\/\rangle\,$
where $m_{n}=\mathsf{m}-{\rm
Phys.~{}Rev.~{}E}{\\{T_{1},\dots,t_{n-1}\\}}+{\\{T_{1},\dots,t_{n-1}\\}}{{}^{\bullet}}$.
For all $t\in\lfloor t_{n}\rfloor$ we have that $m_{n}(s)=0$ for $s\in{\rm
Phys.~{}Rev.~{}E}{t}$ and as $t^{\prime}\in\lfloor t_{n}\rfloor$ we have that
there is an inhibitor arc from an $s\in{\rm Phys.~{}Rev.~{}E}{t^{\prime}}$ and
$t$, but then $m_{n}\,[\/{t_{n}}\/\rangle\,$, and the thesis follows. ∎

An important consequence of this proposition is that we can associate an
occurrence net to an occurrence causal one, simply by associating to the
occurrence causal net the corresponding pes as in Proposition 5.2 and then
apply the construction in Definition 3.1.

######  Proposition .

Let $K=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ be an occurrence causal net,
then $\langle B,T,F^{\prime},\mathsf{c}\rangle$ where

  * •

$B=\\{{(\ast,e)}\mid{e\in E}\\}\cup\\{{(e,\ast)}\mid{e\in
E}\\}\cup\\{{(e,e^{\prime},\prec_{K})}\mid{e\prec_{K}e^{\prime}}\\}\cup\\{{(\\{e,e^{\prime}\\},\\#)}\mid{e\
\\#_{K}\ e^{\prime}}\\}$,

  * •

$F=\\{{(e,b)}\mid{b=(e,\ast)}\\}\ \cup\
\\{{(e,b)}\mid{b=(e,e^{\prime},\prec_{K})}\\}\ \cup\
\\{{(b,e)}\mid{b=(\ast,e)}\\}\ \cup\
\\{{(b,e)}\mid{b=(e^{\prime},e,\prec_{K})}\\}\ \cup\
\\{{(b,e)}\mid{b=(Z,\\#_{K})\ \land\ e\in Z}\\}$, and

  * •

$\mathsf{c}=\\{{(\ast,e)}\mid{e\in
E}\\}\cup\\{{(\\{e,e^{\prime}\\},\\#)}\mid{e\ \\#\ e^{\prime}}\\}$

is an occurrence net.

###### Proof.

By Propositions 5.2 and 3.1. ∎

The following theorem indeed assures that the notion of (occurrence) causal
net is adequate as the notion of occurrence net with respect to the classical
notion of occurrence net in the relationship with prime event structure.

######  Theorem .

Let $K$ be an occurrence causal net and $\mathsf{P}$ be a prime event
structure. Then
$K\cong\mathcal{N}_{\textsc{pes}}^{\textsc{cn}}(\mathcal{E}_{\textsc{cn}}^{\textsc{pes}}(K))$
and
$\mathsf{P}\equiv\mathcal{E}_{\textsc{cn}}^{\textsc{pes}}(\mathcal{N}_{\textsc{pes}}^{\textsc{cn}}(\mathsf{P}))$.

###### Proof.

By Propositions 5.2 and 5.2. ∎

###  5.3. Unravel nets and causal nets

In an unravel net the same transitions may have various causes, conflicting
one. In a causal net we may have various incarnations of the same _activity_ ,
depending on different contexts. In associating a causal net to an unravel one
$U$ we have to establish, for each transition in $U$, the possible sets of
causes.

######  Definition .

Let $U=\langle S,T,F,\mathsf{m}\rangle$ be an un, and let $t\in T$ be a
transition. Then the set $\mathsf{Caus}(t)$ defined as $\\{{Y\subseteq
T}\mid{\forall s\in{\rm Phys.~{}Rev.~{}E}{t}.{\rm
Phys.~{}Rev.~{}E}{s}\neq\emptyset\ \Rightarrow\ |{\rm Phys.~{}Rev.~{}E}{s}\cap
Y|=1}\\}\cup\\{{\emptyset}\mid{\forall s\in{\rm Phys.~{}Rev.~{}E}{t}.{\rm
Phys.~{}Rev.~{}E}{s}=\emptyset}\\}$ is the set of all possible dependencies
for $t$.

We add the $\emptyset$ when $t$ does not depend on any other occurrence of a
transition.

We show how to associate a causal net to an unravel one. The idea is to create
a copy of the transition $t$ for each of its possible dependencies in the
unravel net, and each of these dependencies are then implemented with
inhibitor arcs.

######  Proposition .

Let $U=\langle S,T,F,\mathsf{m}\rangle$ be an un. The net
$\mathcal{G}_{\textsc{un}}(U)=\langle
S,T^{\prime},F^{\prime},I,\emptyset,\hat{\mathsf{m}},\ell\rangle$ where

  * •

$S=\\{{(\ast,t)}\mid{t\in T}\\}\cup\\{{(t,\ast)}\mid{t\in
T}\\}\cup\\{{\\{t,t^{\prime}\\}}\mid{t\ \\#\ t^{\prime}}\\}$,

  * •

$T^{\prime}=\\{{(t,Y)}\mid{t\in T\ \land\ Y\in\mathsf{Caus}(t)}\\}$,

  * •

$F^{\prime}=\\{{(s,(t,-))}\mid{s=(\ast,t)}\\}\cup\\{{(s,(t,-))}\mid{t\in
s}\\}\cup\\{{((t,-),s)}\mid{s=(t,\ast)}\\}$,

  * •

$I=\\{{(s,(t,Y))}\mid{s=(\ast,t^{\prime})\ \land\ t^{\prime}\in Y}\\}$,

  * •

$\hat{\mathsf{m}}:S\to{\rm Nature}$ is such that $\hat{\mathsf{m}}(s)=0$ if
$s=(t,\ast)$ and $\hat{\mathsf{m}}(s)=1$ otherwise, and

  * •

$\ell(t,-)=t$ is the labeling mapping,

is a causal net over the set of label $T$, and
$\mathsf{Conf}_{\textsc{un}}(U)=\mathsf{Conf}_{\textsc{cn}}(\mathcal{G}_{\textsc{un}}(U))$.

###### Proof.

We check the various conditions of Definitions 5 and 5. We start with the ones
of Definition 5. Conditions (1), (3) and (5) are trivially satisfied by
construction. For the second condition, take any transition $(t,Y)\in
T^{\prime}$, with $t\in T$ and $Y\subseteq T$ and $Y\neq\emptyset$, and
consider $s\in\\!~{}^{\circ}{(t,Y)}$. We have that $s$ is of the form
$(\ast,t^{\prime})$ for some $t^{\prime}\in Y$. Clearly
${s}{{}^{\bullet}}=\\{(t^{\prime},Y^{\prime}_{1}),\dots(t^{\prime},Y^{\prime}_{k})\\}$
and $\ell({s}{{}^{\bullet}})=\\{t^{\prime}\\}$, thus
$|\ell({s}{{}^{\bullet}})|=1$. Given a $t\in T^{\prime}$, finiteness of
$\\!~{}^{\circ}{t}$ derives by the fact that in the un $U$ there is no place
with infinite incoming arcs, and the last condition follows by the fact that
equally labeled transitions $t$ and $t^{\prime}$ in $T^{\prime}$ share a
common input place: $(\ast,\ell(t))$.

To show that
$\mathsf{Conf}_{\textsc{un}}(U)=\mathsf{Conf}_{\textsc{cn}}(\mathcal{G}_{\textsc{un}}(U))$
we proceed as follows: consider $\sigma$ a fs in $U$ and $X$ the corresponding
state. We show that there is a fs $\widehat{\sigma}$ in
$\mathcal{G}_{\textsc{un}}(U)$ such that
$\mathsf{tr}(\sigma)=\mathsf{tr}(\widehat{\sigma})$. In particular we prove
that if $\sigma=\sigma^{\prime}\,[\/{t}\/\rangle\,\sigma^{\prime\prime}$ then
there is a transition $(t,Y)$ such that
$\widehat{\sigma}=\widehat{\sigma^{\prime}}\,[\/{(t,Y)}\/\rangle\,\widehat{\sigma^{\prime\prime}}$
with $\mathsf{tr}(\sigma^{\prime})=\mathsf{tr}(\widehat{\sigma^{\prime}})$. By
induction on the length of the firing sequence $\sigma^{\prime}$, we have that
if $\mathit{len}(\sigma^{\prime})=0$ then $\sigma^{\prime}=\mathsf{m}$ and
consider $t$ enabled at $\mathsf{m}$. Then
$\widehat{\sigma^{\prime}}=\hat{\mathsf{m}}$ and $(t,\emptyset)$ is clearly
enabled at this marking. Consider then $\sigma^{\prime}$,
$\overline{\mathsf{tr}(\sigma^{\prime})}$ and a transition $t$ enabled at
$\mathit{lead}(\sigma^{\prime})$, we have that for exactly one
$Y\subseteq\overline{\mathsf{tr}(\sigma^{\prime})}$ it holds that $(t,Y)$ is
enabled at the marking $\mathit{lead}(\widehat{\sigma^{\prime}})$ as the
transitions in $Y$ are those that have marked the preset of $t$ in $U$. A
similar argument show that to each firing sequence $\widehat{\sigma}$ in
$\mathcal{G}_{\textsc{un}}(U)$ a firing sequence $\sigma$ in $U$ corresponds
and $\mathsf{tr}(\sigma)=\mathsf{tr}(\widehat{\sigma})$. Thus
$\mathsf{Conf}_{\textsc{un}}(U)=\mathsf{Conf}_{\textsc{cn}}(\mathcal{G}_{\textsc{un}}(U))$.
∎

######  Example .

Below we depict a simple unravel net (on the left) and the associated causal
one.

$\mathsf{a}$$\mathsf{c}$$\mathsf{c}$$\mathsf{b}$$\mathsf{a}$$\mathsf{b}$$\mathsf{c}$

Observe that there are two incarnations for the same transition $\mathsf{c}$
in the corresponding cn one, namely $(\mathsf{c},\\{\mathsf{a}\\})$ for the
one on the left and $(\mathsf{c},\\{\mathsf{b}\\})$ for the one on the right.

On a cn net we can define a conflict relation involving the labels. Given the
cn $K=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ over the set of labels
$\mathsf{L}$, we say that $a\ \sharp\ b$ whenever $\forall t\in\ell^{-1}(a)\
\forall t^{\prime}\in\ell^{-1}(b).\ t\ \\#\ t^{\prime}$: in this conflict
relation, defined on labels, we represent the fact that all the possible
incarnations of the activities $a$ and $b$ are in conflict.

The cn obtained from an unravel net has a peculiar shape when looking at the
contextual arcs representing the dependencies: inhibitor arcs connecting
places and transitions are such that the places have no incoming arcs.
Furthermore two equally labeled transitions $t$ and $t^{\prime}$ are
_inhibited_ by the same number of _transitions_ and the labels of these
inhibiting transitions are either in conflict or they are the same.

######  Definition .

Let $K=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ be a cn over the set of
labels $\mathsf{L}$, we say that $K$ is _plainly caused_ whenever

  * •

$R=\emptyset$,

  * •

$\forall t\in T\ \forall s\in\\!~{}^{\circ}{t}.\ {\rm
Phys.~{}Rev.~{}E}{s}=\emptyset$,

  * •

$\forall a\in\ell(T).\ \forall t,t\in\ell^{-1}(a).\
|\\!~{}^{\circ}{t}|=|\\!~{}^{\circ}{t^{\prime}}|$, and

  * •

$\forall t,t^{\prime}\in T.\ (\ell(t)=\ell(t^{\prime})\ \land\ t\neq
t^{\prime})\ \Rightarrow\ \forall s\in\\!~{}^{\circ}{t}\ \forall
s^{\prime}\in\\!~{}^{\circ}{t}.\
(\ell({s}{{}^{\bullet}})=\ell({s^{\prime}}{{}^{\bullet}})\ \lor\
\ell({s}{{}^{\bullet}})\ \sharp\ \ell({s^{\prime}}{{}^{\bullet}}))$.

The cns obtained either by an on or by an un are plainly caused (we have
already observed that an occurrence net is an unravel net as well).

######  Proposition .

Let $U$ be an un and $\mathcal{G}_{\textsc{un}}(U)$ be the associated cn. Then
$\mathcal{G}_{\textsc{un}}(U)$ is plainly caused.

###### Proof.

The first three conditions are clear by the construction in Proposition 5.3,
and for the last one it is enough to observe how $\mathsf{Caus}(t)$ is formed.
∎

Given a label $a\in\mathsf{L}$ and a cn $K=\langle
S,T,F,I,R,\mathsf{m},\ell\rangle$, the set of the possible dependencies of the
transitions $t\in\ell^{-1}(a)$ is defined as
$\mathsf{PD}(a)=\\{{\ell({s}{{}^{\bullet}})}\mid{s\in\\!~{}^{\circ}{t}\ \land\
t\in\ell^{-1}(a)}\\}$. Given an event $a$, this set contains all the labels
(events) that should have happened in order to allow to one of the transitions
labeled with $a$ to occur. From this set it is possible to extract maximal
subsets of conflicting labels, which we denote with
$\mathsf{MaxB}(a)=\\{{Y\subseteq\mathsf{PD}(a)}\mid{\forall b,b^{\prime}\in
Y.\ b\ \sharp\ b^{\prime}\ \land\ Y\ \mbox{ is maximal}}\\}$. Maximality is
required as otherwise some events would not occur in the associated bes as the
required _dependency_ has been left out.

######  Example .

Consider the $K$ net in Example 5.3. Then $\mathsf{PD}(\mathsf{a})=\emptyset$,
$\mathsf{PD}(\mathsf{b})=\emptyset$ and
$\mathsf{PD}(\mathsf{c})=\\{\mathsf{a},\mathsf{b}\\}$. The components of the
bundles are determined using $\mathsf{MaxB}(\cdot)$ and in this case we have
$\mathsf{MaxB}(\mathsf{c})=\\{\\{\mathsf{a},\mathsf{b}\\}\\}$. Observe that
maximality is required as otherwise one could infer, e.g.,
$\\{\mathsf{a}\\}\mapsto\mathsf{c}$, which is not correct.

######  Proposition .

Let $K=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ be a plainly caused cn over
the set of labels $E$. Then
$\mathcal{E}_{\textsc{cn}}^{\textsc{bes}}(K)=(E,\mapsto,\sharp)$ where
$Y\mapsto e$ whenever $Y\in\mathsf{MaxB}(e)$ is a bes, and
$\mathsf{Conf}_{\textsc{cn}}(K)=\mathsf{Conf}_{\textsc{bes}}(\mathcal{E}_{\textsc{cn}}^{\textsc{bes}}(K))$.

###### Proof.

Along the same lines as Proposition 5.2.
$\mathcal{E}_{\textsc{cn}}^{\textsc{bes}}(K)$ is a bes as each
$Y\in\mathsf{MaxB}(e)$ is made of conflicting events, and the conflict
relation is irreflexive and symmetric by construction. To show that the
configurations coincide, consider $X\in\mathsf{Conf}_{\textsc{cn}}(K)$, and
assume that $X=X_{\sigma}$ for some $\sigma\in\mathcal{R}^{K}_{\mathsf{m}}$.
To prove that
$X\in\mathsf{Conf}_{\textsc{bes}}(\mathcal{E}_{\textsc{cn}}^{\textsc{bes}}(K))$
as well, we take $\mathsf{tr}(\sigma)$. Clearly $\mathsf{tr}(\sigma)(1)=e_{1}$
is such that $\mathsf{PD}(e_{1})=\emptyset$ as $K$ is plainly caused, hence
$\\{e_{1}\\}\in\mathsf{Conf}_{\textsc{bes}}(\mathcal{E}_{\textsc{cn}}^{\textsc{bes}}(K))$.
Assume now that
$\sigma=\sigma^{\prime}\,[\/{t}\/\rangle\,\sigma^{\prime\prime}$ and that
$\overline{\mathsf{tr}(\sigma^{\prime})}\in\mathsf{Conf}_{\textsc{bes}}(\mathcal{E}_{\textsc{cn}}^{\textsc{bes}}(K))$,
we have to show that $Y\in\mathsf{MaxB}(\ell(t))$ is such that
$Y\cap\overline{\mathsf{tr}(\sigma^{\prime})}\neq\emptyset$, but this is
clearly true as $Y\in\mathsf{MaxB}(\ell(t))$ and because the set of inhibition
has the same number of elements for each incarnation of $\ell(t)$. Conflicting
events cannot be added, hence the thesis. The other inclusion holds with the
same reasoning. ∎

Given a bes $\mathsf{B}$ define
$\mathcal{N}_{\textsc{bes}}^{\textsc{cn}}(\mathsf{B})$ as
$\mathcal{G}_{\textsc{un}}(\mathcal{N}_{\textsc{bes}}^{\textsc{un}}(\mathsf{B}))$.
Then also the following theorem holds.

######  Theorem .

Let $K$ be an plainly caused causal net and $\mathsf{B}$ be a bundle event
structure. Then
$K\cong\mathcal{N}_{\textsc{bes}}^{\textsc{cn}}(\mathcal{E}_{\textsc{cn}}^{\textsc{bes}}(K))$
and
$\mathsf{B}\equiv\mathcal{E}_{\textsc{cn}}^{\textsc{bes}}(\mathcal{N}_{\textsc{bes}}^{\textsc{cn}}(\mathsf{B}))$.

###### Proof.

By Propositions 5.3 and 5.3. ∎

##  6\. Context-dependent event structures and causal nets

We are now ready to relate Context-dependent event structures and causal nets.
We recall that in a Context-dependent event structure each event may happen in
different context and thus each happening has a different operational meaning.
Therefore we model each happening with a different transition and all the
transitions representing the same happening bear the same label. Dependencies
are inferred using inhibitor and read arcs, as it will be clear.

######  Definition .

Let $\mathsf{E}=(E,\\#,\gg)$ be an elementary cdes such that
$\forall\mathsf{Z}\gg e.\ \textsc{Cxt}(\mathsf{Z}\gg e)$ is finite. Define
$\mathcal{N}_{\textsc{cdes}}^{\textsc{cn}}(\mathsf{E})$ as the net $\langle
S,T,F,I,R,\mathsf{m},\ell\rangle$ where

  * •

$S=\\{{(\ast,e)}\mid{e\in E}\\}\cup\\{{(e,\ast)}\mid{e\in
E}\\}\cup\\{{(\\{e,e^{\prime}\\},\\#)}\mid{e\ \\#\ e^{\prime}}\\}$,

  * •

$T=\\{{(e,X,Y)}\mid{(X,Y)\in\mathsf{Z}\ \land\ \mathsf{Z}\gg e}\\}$,

  * •

$F=\\{{(s,(e,X,Y))}\mid{s=(\ast,e)\ \lor\ (s=(W,\\#)\ \land\ e\in W)}\\}\
\cup\ \\{{((e,X,Y),s)}\mid{s=(e,\ast)}\\}$,

  * •

$I=\\{{(s,(e,X,Y))}\mid{s=(\ast,e^{\prime})\ \land\ e^{\prime}\in X}\\}\ \cup$
$\\{{(s,(e,X,Y))}\mid{s=(e^{\prime},\ast)\ \land\
e^{\prime}\in\textsc{Cxt}(\mathsf{Z}\gg e)\setminus(X\cup Y)}\\}$,

  * •

$R=\\{{(s,(e,X,Y))}\mid{s=(e^{\prime},\ast)\ \land\ e^{\prime}\in Y}\\}$,

  * •

$\mathsf{m}=\\{{(\ast,e)}\mid{e\in
E}\\}\cup\\{{(\\{e,e^{\prime}\\},\\#)}\mid{e\ \\#\ e^{\prime}}\\}$, and

  * •

$\ell:T\to E$ is defined as $\ell((e,X,Y))=e$.

We introduce a transition $(e,X,Y)$ for each pair $(X,Y)$ of the entry
associated to the event $e$, and all these transitions are labeled with the
same event $e$. All these transitions consume the token present in the place
$(\ast,e)$ and put a token in the place $(e,\ast)$, thus just one transition
labeled with $e$ can be fired in each execution of the net. Recall that the
event $e$ is enabled at a configuration $C$ (here signaled by the places
$(e^{\prime},\ast)$ marked) if, for some $(X,Y)\in\mathsf{Z}$, it holds that
$\textsc{Cxt}(\mathsf{Z}\gg e)\cap C=X$ and $Y\subseteq C$. The inhibitor arcs
assure that some of the events in $\textsc{Cxt}(\mathsf{Z}\gg e)$ have
actually happened (namely the one in $X$) but the others (the ones in
$\textsc{Cxt}(\mathsf{Z}\gg e)\setminus(X\cup Y)$) have not, and the $Y$ are
other events that must have happened and this is signaled by read arcs. We
cannot require $\textsc{Cxt}(\mathsf{Z}\gg e)\setminus X$ as some of the
events there may be present in $Y$.

######  Example .

Consider the cdes in Example 4, the corresponding causal net is the one
depicted in Example 5. The event $\mathsf{c}$ has two incarnations as the
entry
$\\{(\emptyset,\\{\mathsf{a}\\}),(\\{\mathsf{b}\\},\emptyset)\\}\gg\mathsf{c}$
has two elements: $(\emptyset,\\{\mathsf{a}\\})$ and
$(\\{\mathsf{b}\\},\emptyset)$.

######  Example .

Consider the cdes of the Example 4, the event $\mathsf{c}$ has two
incarnations as the entry
$\\{(\emptyset,\emptyset),(\\{\mathsf{b}\\},\\{\mathsf{a}\\})\\}\gg\mathsf{c}$
has two elements, whereas $\mathsf{a}$ and $\mathsf{b}$ have one. The
associated causal net is

$t_{1}$$\mathsf{b}$$t_{2}$$\mathsf{c}$$t_{3}$$\mathsf{c}$$t_{4}$$\mathsf{a}$

######  Example .

Consider now the cdes in Example 4 (modeling the resolvable conflict of
[vGP04]).

$t_{1}$$\mathsf{a}$$t_{2}$$\mathsf{a}$$t_{3}$$\mathsf{c}$$t_{4}$$\mathsf{b}$$t_{5}$$\mathsf{b}$

the actual implementation of this cdes into the causal net depicted before,
where the events $\mathsf{a}$ and $\mathsf{b}$ have two incarnations each. The
transition $t_{1}$ is the one with $(X,Y)=(\emptyset,\emptyset)$ whereas
$t_{2}$ is $(\mathsf{a},\\{\mathsf{b}\\},\\{\mathsf{c}\\})$, $t_{4}$ is the
transition $(\mathsf{b},\\{\mathsf{a}\\},\\{\mathsf{c}\\})$ and finally
$t_{5}$ is $(\mathsf{b},\emptyset,\emptyset)$. The inhibitor and read arcs are
colored depending on event they are related to.

The net obtained from a cdes using Definition 6 is indeed a causal net, and
furthermore it is also conflict saturated.

######  Proposition .

Let $\mathsf{E}$ be an elementary cdes, and
$\mathcal{N}_{\textsc{cdes}}^{\textsc{cn}}(\mathsf{E})$ be the associated
contextual Petri net. Then
$\mathcal{N}_{\textsc{cdes}}^{\textsc{cn}}(\mathsf{E})$ is a causal net and
$\mathsf{Conf}_{\textsc{cdes}}(\mathsf{E})=\mathsf{Conf}_{\textsc{cn}}(\mathcal{N}_{\textsc{cdes}}^{\textsc{cn}}(\mathsf{E}))$.

###### Proof.

We proceed along the same line as in the proof of Proposition 5.3 and we check
the various conditions of Definitions 5 and 5. Conditions (1), (3) and (5) of
Definition 5 are again satisfied by construction. For the second condition,
take any transition $t=(e,X,Y)\in T$, with $e\in E$ and $X,Y\subseteq E$.
Consider $s\in\\!~{}^{\circ}{t}$. We have that $s$ is of the form
$(\ast,e^{\prime})$ for some $e^{\prime}\in e^{\prime}\in X$. Clearly
${s}{{}^{\bullet}}=\\{(e^{\prime},X_{1},Y^{\prime}_{1}),\dots(t^{\prime},Y^{\prime}_{k})\\}$
and $\ell({s}{{}^{\bullet}})=\\{e^{\prime}\\}$, thus
$|\ell({s}{{}^{\bullet}})|=1$. Given a $t\in T$, finiteness of
$\\!~{}^{\circ}{t}$ derives by the fact that in the cdes $\mathsf{Z}$ is
finite. The last condition follows by the fact that equally labeled transition
$t$ and $t^{\prime}$ in $T$ share a common input place: $(\ast,\ell(t))$.

$\mathsf{Conf}_{\textsc{cdes}}(\mathsf{E})=\mathsf{Conf}_{\textsc{cn}}(\mathcal{N}_{\textsc{cdes}}^{\textsc{cn}}(\mathsf{E}))$
depends on the fact that to each configuration
$C\in\mathsf{Conf}_{\textsc{cdes}}(\mathsf{E})$ a reachable marking $m_{C}$ in
the cn $\mathcal{N}_{\textsc{cdes}}^{\textsc{cn}}(\mathsf{E})$ correspond, and
vice versa.

First observe that the execution of a transition labeled with $e$ is signaled
by the fact that the place $(e,\ast)$ is marked (and $(\ast,e)$ not), and all
the places $(\\{e.e^{\prime}\\},\\#)$ are unmarked, thus given a configuration
$X$ the corresponding marking $m_{C}$ is such that $m((e,\ast))=1$ if $e\in
C$, $m((e,\ast))=1$ if $e\not\in C$, $m((W,\\#))=1$ if $W\cap C=\emptyset$ and
$m((W,\\#))=0$ if $W\cap C\neq\emptyset$.

If $C$ is the empty configuration then clearly the initial marking does the
job in $\mathcal{N}_{\textsc{cdes}}^{\textsc{cn}}(\mathsf{E})$. Consider a
configuration $C$ of size $n$, and the corresponding marking $m_{C}$, assume
that $C[\/{e}\/\rangle$ for some $e\in E$. Recall that this means that in
$\mathsf{Z}\gg e$ there is a pair $(X,Y)$ such that
$(\textsc{Cxt}{\mathsf{Z}\gg e})\cap C=X$ and $Y\subseteq C$. Take the
transition $(e,X,Y)$, it is clear that $m_{C}\,[\/{(e,X,Y)}\/\rangle\,$, as
the inhibitor and read arcs guarantee exactly this. The vice versa is along
the same line, and the equality between
$\mathsf{Conf}_{\textsc{cdes}}(\mathsf{E})$ and
$\mathsf{Conf}_{\textsc{cn}}(\mathcal{N}_{\textsc{cdes}}^{\textsc{cn}}(\mathsf{E}))$
follows. ∎

######  Proposition .

Let $\mathsf{E}$ be a cdes, and
$\mathcal{N}_{\textsc{cdes}}^{\textsc{cn}}(\mathsf{E})$ be the associated
contextual Petri net. Then
$\mathcal{N}_{\textsc{cdes}}^{\textsc{cn}}(\mathsf{E})$ is conflict saturated.

###### Proof.

Obvious as $\mathcal{N}_{\textsc{cdes}}^{\textsc{cn}}(\mathsf{E})$ is a cn. ∎

For the vice versa we do need to make a further assumption on the causal net.
The intuition is that equally labeled transitions are different incarnations
of the same activity, happening in different contexts. Henceforth one has to
make sure that the equally labeled transitions indeed represent the same
_event_ and each incarnation of an event should have the same _environment_ ,
meaning with environment the events related to it (which in the cdes is
calculated with Cxt). Given a causal net $K=\langle
S,T,F,I,R,\mathsf{m},\ell\rangle$ on a set of label $\mathsf{L}$ and a
transition $t\in T$, with $\overrightarrow{\\!~{}^{\circ}{t}}$ we denote the
set of labels $\\{{a\in\mathsf{L}}\mid{s\in\\!~{}^{\circ}{t}\ \land\
\ell({s}{{}^{\bullet}})=a}\\}$, with $\overleftarrow{\\!~{}^{\circ}{t}}$ the
set of labels $\\{{a\in\mathsf{L}}\mid{s\in\\!~{}^{\circ}{t}\ \land\ \ell({\rm
Phys.~{}Rev.~{}E}{s})=a}\\}$, and with $\widetilde{\underline{t}}$ the set of
labels $\\{{a\in\mathsf{L}}\mid{s\in\underline{t}\ \land\ \ell({\rm
Phys.~{}Rev.~{}E}{s})=a}\\}$.

######  Definition .

Let $K=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ be a causal net labeled over
$\mathsf{L}$, we say that $K$ is _well behaved_ if

  1. (1)

$\forall a\in\mathsf{L}$. $\forall t,t^{\prime}\in\ell^{-1}(a)$ it holds that
${\rm Phys.~{}Rev.~{}E}{t}\cup{\rm Phys.~{}Rev.~{}E}{t^{\prime}}=\\{s\\}$ and
${t}{{}^{\bullet}}\cup{t^{\prime}}{{}^{\bullet}}=\\{s^{\prime}\\}$, and

  2. (2)

$\forall a\in\mathsf{L}$. $\forall t,t^{\prime}\in\ell^{-1}(a)$ it holds that
$\overrightarrow{\\!~{}^{\circ}{t}}\cup\widetilde{\underline{t}}\cup\overleftarrow{\\!~{}^{\circ}{t}}=\overrightarrow{\\!~{}^{\circ}{t^{\prime}}}\cup\widetilde{\underline{t^{\prime}}}\cup\overleftarrow{\\!~{}^{\circ}{t^{\prime}}}$.

In a well behaved causal net all the transitions equally labeled have a common
input place and also a common output place (condition 1). The equally labeled
transitions in the causal net are the various incarnations of the _event_ they
represent, thus they have the same context, though the various kind of
involved arcs are different (condition 2).

######  Example .

Consider the net below:

$t_{1}$$\mathsf{b}$$t_{2}$$\mathsf{c}$$t_{3}$$\mathsf{c}$$t_{4}$$\mathsf{a}$

The transitions labeled with $\mathsf{c}$ have the same environment, namely
the set of labels $\\{\mathsf{a},\mathsf{b}\\}$.

It is worth to observe that when associating a causal net to a cdes we obtain
a well behaved one.

######  Proposition .

Let $\mathsf{E}$ be a cdes, and
$\mathcal{N}_{\textsc{cdes}}^{\textsc{cn}}(\mathsf{E})$ be the associated
contextual Petri net. Then
$\mathcal{N}_{\textsc{cdes}}^{\textsc{cn}}(\mathsf{E})$ is a well behaved
causal net.

###### Proof.

By construction of $\mathcal{N}_{\textsc{cdes}}^{\textsc{cn}}(\mathsf{E})$ the
requirements of Definition 6 hold. ∎

To a causal net we can associate a triple where the relations will turn out to
be, under some further requirements, those of a cdes. Here the events are the
labels of the transitions, conflicts between events are inferred using the
presets of the transitions and the entries are calculated using inhibitor and
read arcs.

######  Definition .

Let $K=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ be a causal net labeled over
$\mathsf{L}=E$. Define
$\mathcal{E}_{\textsc{cn}}^{\textsc{cdes}}(K)=(E,\gg,\\#)$ as the triple where

  * •

$E=\ell(T)$,

  * •

$\forall e\in E$. $\mathsf{Z}\gg e$ where $\mathsf{Z}=\\{{(X,Y)}\mid{t\in T.\
\ell(t)=e\ \land\ X=\overrightarrow{\\!~{}^{\circ}{t}}\ \land\
Y=\widetilde{\underline{t}}}\\}$, and

  * •

$\forall e,e^{\prime}\in E$. $e\ \\#\ e$ is there exists $t,t^{\prime}\in T$.
$\ell(t)\neq\ell(t^{\prime})$ and ${\rm Phys.~{}Rev.~{}E}{t}\cap{\rm
Phys.~{}Rev.~{}E}{t^{\prime}}\neq\emptyset$.

The construction above gives the proper cdes, provided that the cn is well
behaved.

######  Proposition .

Let $K=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ be a well behaved causal net
and $\mathcal{E}_{\textsc{cn}}^{\textsc{cdes}}(K)=(E,\gg,\\#)$ the associated
triple, then $\mathcal{E}_{\textsc{cn}}^{\textsc{cdes}}(K)$ is a cdes and
$\mathsf{Conf}_{\textsc{cn}}(K)=\mathsf{Conf}_{\textsc{cdes}}(\mathcal{E}_{\textsc{cn}}^{\textsc{cdes}}(K))$.

###### Proof.

$\mathcal{E}_{\textsc{cn}}^{\textsc{cdes}}(K)$ is clearly a cdes. It remains
to prove that
$\mathsf{Conf}_{\textsc{cn}}(K)=\mathsf{Conf}_{\textsc{cdes}}(\mathcal{E}_{\textsc{cn}}^{\textsc{cdes}}(K))$
but this follows the same argument of Proposition 6. ∎

The following theorem assure that the notion of (well behaved) causal net is
adequate in the relationship with context-dependent event structure.

######  Theorem .

Let $K=\langle S,T,F,I,R,\mathsf{m},\ell\rangle$ be a well behaved causal net,
and let $\mathsf{E}$ be a cdes. Then
$K\cong\mathcal{N}_{\textsc{cdes}}^{\textsc{cn}}(\mathcal{E}_{\textsc{cn}}^{\textsc{cdes}}(K))$
and
$\mathsf{E}\equiv\mathcal{E}_{\textsc{cn}}^{\textsc{cdes}}(\mathcal{N}_{\textsc{cdes}}^{\textsc{cn}}(\mathsf{E}))$.

###### Proof.

By Propositions 6 and 6. ∎

##  7\. Conclusions

In this paper we have proposed the notion of causal net as the net counterpart
of the context-dependent event structure, and shown that the notion is
adequate. A causal net is a Petri net where the dependencies are represented
using inhibitor and read arcs and not usual flow ones: the dependencies are
not any longer inferred by the production of a token to be consumed but they
are described by the presence or absence of tokens in places whose meaning is
that a particular activity has been executed or not. Another feature of the
causal net is that an activity, identified by a label, may have several
different implementations, but this is not surprising as usually unfoldings
have this peculiarity.

Like context-dependent event structure subsumes other kinds of event
structures, also the new notion comprises other kinds of nets, and we have
given a direct translation of occurrence nets and unravel nets into causal
one, and also the usual constructions associating event structures to nets can
be rewritten in this setting. Like context-dependent event structures, also
causal nets have a similar drawback, namely the difficulty in understanding
easily the dependencies among events, which in some of the event structures is
much more immediate.

Recently a notion of unfolding representing reversibility has been pointed out
([MMU19]) and the issue of how find the appropriate notion of net relating
_reversible_ event structure has been tackled ([MMP+20]) and solved for a
subclass of reversible event structure. The notion of causal net is then a
promising one as it may be used as the basis to model reversible prime event
structures as it is done in [MMP21]whereas classical approaches fail
([MMP+20]), as already observed.

In this paper we have focussed on the objects and not on the relations among
them, hence we have not investigated the categorical part of the new kind of
net, which we intend to pursue in the future. A notion of morphism for cdes
could be a partial mapping $f$ on events such that if $f(e)$ is defined and
$\mathsf{Z}\gg e$ then $f$ is such that for all
$(X,Y),(X^{\prime},Y^{\prime})\in\mathsf{Z}$ then
$f(X)=f(X^{\prime})\Rightarrow\ f(Y)=f(Y^{\prime})$ and the mapping can
identify only conflicting events.

But when considering causal nets it should be observed that whereas read arcs
are treated similarly to flow arcs, inhibitor arcs are usually treated as
contra-variant, which contrast our usage. Thus a new different notion of
mapping on nets should be introduced taking into account the fact that causal
nets are flat ones with respect to the flow relation.

It should also be mentioned that _persistent_ nets have been connected to
event structures ([CW05] and [BBC+18]), and in these nets events may happen in
different contexts, hence it would be interesting to compare these approaches
to the one pursued here.

## Acknowlegments

The author would like to acknowledge that Hernán Melgratti and Claudio A.
Mezzina, through many fruitful discussions on the notion of causal net, have
contributed to it. The anonymous reviewers have to be thanked for their useful
criticisms and suggestions that have greatly contributed to improve the paper.

## References

  * [AKPN15] Youssef Arbach, David Karcher, Kirstin Peters, and Uwe Nestmann.  Dynamic causality in event structures.  In Susanne Graf and Mahesh Viswanathan, editors, Formal Techniques for Distributed Objects, Components, and Systems - 35th IFIP WG 6.1 International Conference, FORTE 2015, Held as Part of the 10th International Federated Conference on Distributed Computing Techniques, DisCoTec 2015, Grenoble, France, June 2-4, 2015, Proceedings, volume 9039 of Lecture Notes in Computer Science, pages 83–97. Springer, 2015.
  * [AKPN18] Youssef Arbach, David S. Karcher, Kirstin Peters, and Uwe Nestmann.  Dynamic causality in event structures.  Logical Methods in Computer Science, 14(1), 2018.
  * [BBC+18] Paolo Baldan, Roberto Bruni, Andrea Corradini, Fabio Gadducci, Hernán C. Melgratti, and Ugo Montanari.  Event structures for Petri nets with persistence.  Logical Methods in Computer Science, 14(3), 2018.
  * [BBCP04] Paolo Baldan, Nadia Busi, Andrea Corradini, and G. Michele Pinna.  Domain and event structure semantics for Petri nets with read and inhibitor arcs.  Theoretical Computer Science, 323(1-3):129–189, 2004.
  * [BCM01] Paolo Baldan, Andrea Corradini, and Ugo Montanari.  Contextual Petri nets, asymmetric event structures and processes.  Information and Computation, 171(1):1–49, 2001.
  * [BCP15] Massimo Bartoletti, Tiziana Cimoli, and G. Michele Pinna.  Lending Petri nets.  Science of Computer Programming, 112:75–101, 2015.
  * [Bou90] Gérard Boudol.  Flow event structures and flow nets.  In Irène Guessarian, editor, Semantics of Systems of Concurrent Processes, LITP Spring School on Theoretical Computer Science, La Roche Posay, France, April 23-27, 1990, Proceedings, volume 469 of Lecture Notes in Computer Science, pages 62–95. Springer, 1990.
  * [CP14] Giovanni Casu and G. Michele Pinna.  Flow unfolding of multi-clock nets.  In Gianfranco Ciardo and Ekkart Kindler, editors, Application and Theory of Petri Nets and Concurrency - 35th International Conference, PETRI NETS 2014, Tunis, Tunisia, June 23-27, 2014. Proceedings, volume 8489 of Lecture Notes in Computer Science, pages 170–189. Springer, 2014\.
  * [CP17a] Giovanni Casu and G. Michele Pinna.  Merging relations: A way to compact petri nets’ behaviors uniformly.  In Frank Drewes, Carlos Martín-Vide, and Bianca Truthe, editors, Language and Automata Theory and Applications - 11th International Conference, LATA 2017, Umeå, Sweden, March 6-9, 2017, Proceedings, volume 10168 of Lecture Notes in Computer Science, pages 325–337, 2017.
  * [CP17b] Giovanni Casu and G. Michele Pinna.  Petri nets and dynamic causality for service-oriented computations.  In Ahmed Seffah, Birgit Penzenstadler, Carina Alves, and Xin Peng, editors, Proceedings of the Symposium on Applied Computing, SAC 2017, Marrakech, Morocco, April 3-7, 2017, pages 1326–1333. ACM, 2017.
  * [CW05] Federico Crazzolara and Glynn Winskel.  Petri nets with persistence.  Electronic Notes in Theoretical Computer Science, 121:143–155, 2005\.
  * [Fab07] Eric Fabre.  Trellis processes : A compact representation for runs of concurrent systems.  Discrete Event Dynamic Systems, 17(3):267–306, 2007.
  * [FP18] Eric Fabre and G. Michele Pinna.  Toward a uniform approach to the unfolding of nets.  In Massimo Bartoletti and Sophia Knight, editors, Proceedings 11th Interaction and Concurrency Experience, ICE 2018, Madrid, Spain, June 20-21, 2018, volume 279 of EPTCS, pages 21–36, 2018.
  * [GR83] Ursula Goltz and Wolfgang Reisig.  The non-sequential behavior of Petri nets.  Information and Control, 57(2/3):125–147, 1983.
  * [JK95] Ryszard Janicki and Maciej Koutny.  Semantics of inhibitor nets.  Information and Computation, 123:1–16, 1995.
  * [KKKV06] Victor Khomenko, Alex Kondratyev, Maciej Koutny, and Walter Vogler.  Merged Processes: a new condensed representation of Petri net behaviour.  Acta Informatica, 43(5):307–330, 2006.
  * [Lan93] Rom Langerak.  Bundle event structures: A non-interleaving semantics for lotos.  In Michel Diaz and Roland Groz, editors, FORTE ’92 Conference Proceedings, volume C-10 of IFIP Transactions, pages 331–346. North-Holland, 1993.
  * [MMP+20] Hernán C. Melgratti, Claudio Antares Mezzina, Iain Phillips, G. Michele Pinna, and Irek Ulidowski.  Reversible occurrence nets and causal reversible prime event structures.  In Ivan Lanese and Mariusz Rawski, editors, Reversible Computation - 12th International Conference, RC 2020, Oslo, Norway, July 9-10, 2020, Proceedings, volume 12227 of Lecture Notes in Computer Science, pages 35–53. Springer, 2020.
  * [MMP21] Hernán C. Melgratti, Claudio Antares Mezzina, and G. Michele Pinna.  A distributed operational view of reversible prime event structures.  In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1–13. IEEE, 2021.
  * [MMU19] Hernán C. Melgratti, Claudio Antares Mezzina, and Irek Ulidowski.  Reversing P/T nets.  In Hanne Riis Nielson and Emilio Tuosto, editors, Coordination Models and Languages - 21st IFIP WG 6.1 International Conference, COORDINATION 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Kongens Lyngby, Denmark, June 17-21, 2019, Proceedings, volume 11533 of Lecture Notes in Computer Science, pages 19–36. Springer, 2019.
  * [MR95] Ugo Montanari and Francesca Rossi.  Contextual nets.  Acta Informatica, 32(6):545–596, 1995.
  * [NPW81] Mogens Nielsen, Gordon Plotkin, and Glynn Winskel.  Petri Nets, Event Structures and Domains, Part 1.  Theoretical Computer Science, 13:85–108, 1981.
  * [PF20] G. Michele Pinna and Eric Fabre.  Spreading nets: A uniform approach to unfoldings.  Journal of Logical and Algebraic Methods in Programming, 112:100526, 2020.
  * [Pin11] G. Michele Pinna.  How much is worth to remember? a taxonomy based on Petri Nets Unfoldings.  In Lars Michael Kristensen and Laure Petrucci, editors, Applications and Theory of Petri Nets - 32nd International Conference, PETRI NETS 2011, Newcastle, UK, June 20-24, 2011. Proceedings, volume 6709 of Lecture Notes in Computer Science, pages 109–128. Springer, 2011\.
  * [Pin19] G. Michele Pinna.  Representing dependencies in event structures.  In Hanne Riis Nielson and Emilio Tuosto, editors, Coordination Models and Languages - 21st IFIP WG 6.1 International Conference, COORDINATION 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Kongens Lyngby, Denmark, June 17-21, 2019, Proceedings, volume 11533 of Lecture Notes in Computer Science, pages 3–18. Springer, 2019.
  * [Pin20a] G. Michele Pinna.  Operational Representation of Dependencies in Context-Dependent Event Structures.  In Simon Bliudze and Laura Bocchi, editors, Coordination Models and Languages - 22nd IFIP WG 6.1 International Conference, COORDINATION 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15-19, 2020, Proceedings, volume 12134 of Lecture Notes in Computer Science, pages 320–338. Springer, 2020.
  * [Pin20b] G. Michele Pinna.  Representing dependencies in event structures.  Logical Methods in Computer Science, 16(2), 2020.
  * [PP95] G. Michele Pinna and Axel Poigné.  On the nature of events: another perspective in concurrency.  Theoretical Computer Science, 138(2):425–454, 1995.
  * [PU15] Iain Phillips and Irek Ulidowski.  Reversibility and asymmetric conflict in event structures.  Journal of Logic and Algebraic Methods in Programming, 84(6):781–805, 2015.
  * [Rei85] Wolfgang Reisig.  Petri Nets: An Introduction.  EACTS Monographs on Theoretical Computer Science. Springer, 1985.
  * [Rei13] Wolfgang Reisig.  Understanding Petri Nets - Modeling Techniques, Analysis Methods, Case Studies.  Springer, 2013.
  * [vGP95] Rob J. van Glabbeek and Gordon D. Plotkin.  Configuration structures.  In Proceedings, 10th Annual IEEE Symposium on Logic in Computer Science, San Diego, California, USA, June 26-29, 1995, pages 199–209. IEEE Computer Society, 1995.
  * [vGP04] Rob J. van Glabbeek and Gordon D. Plotkin.  Event structures for resolvable conflict.  In Jirí Fiala, Václav Koubek, and Jan Kratochvíl, editors, Mathematical Foundations of Computer Science 2004, 29th International Symposium, MFCS 2004, Prague, Czech Republic, August 22-27, 2004, Proceedings, volume 3153 of Lecture Notes in Computer Science, pages 550–561. Springer, 2004.
  * [vGP09] Rob J. van Glabbeek and Gordon D. Plotkin.  Configuration structures, event structures and Petri nets.  Theoretical Computer Science, 410(41):4111–4159, 2009.
  * [Win86] Glynn Winskel.  Event Structures.  In Wilfried Brauer, Wolfgang Reisig, and Grzegorz Rozenberg, editors, Petri Nets: Applications and Relationships to Other Models of Concurrency, volume 255 of Lecture Notes in Computer Science, pages 325–392. Springer, 1986.