definitionthm propositionthm lemmathm corollarythm conjecturethm remarkthm
examplethm proposition lemma corollary conjecture remark definition example

# Concurrency and Probability: Removing Confusion, Compositionally

Roberto Bruni  University of Pisa, Italy<EMAIL_ADDRESS>,  Hernán
Melgratti  ICC - Universidad de Buenos Aires - Conicet, Argentina
<EMAIL_ADDRESS>and  Ugo Montanari  University of Pisa, Italy
<EMAIL_ADDRESS>
###### Abstract.

Assigning a satisfactory truly concurrent semantics to Petri nets with
confusion and distributed decisions is a long standing problem, especially if
one wants to resolve decisions by drawing from some probability distribution.
Here we propose a general solution to this problem based on a recursive,
static decomposition of (occurrence) nets in loci of decision, called
_structural branching cells_ (_s-cells_). Each s-cell exposes a set of
alternatives, called _transactions_. Our solution transforms a given Petri
net, possibly with confusion, into another net whose transitions are the
transactions of the s-cells and whose places are those of the original net,
with some auxiliary nodes for bookkeeping. The resulting net is confusion-free
by construction, and thus conflicting alternatives can be equipped with
probabilistic choices, while nonintersecting alternatives are purely
concurrent and their probability distributions are independent. The validity
of the construction is witnessed by a tight correspondence with the
recursively stopped configurations of Abbes and Benveniste. Some advantages of
our approach are that: i) s-cells are defined statically and locally in a
compositional way; ii) our resulting nets faithfully account for concurrency.

###### Key words and phrases:

Petri nets, confusion, dynamic nets, persistent places, OR causality,
concurrency, probabilistic computation

##  1\. Introduction

Concurrency theory and practice provide a useful abstraction for the design
and use of a variety of systems. Concurrent computations (also _processes_),
as defined in many models, are equivalence classes of executions, called
_traces_ , where the order of concurrent (i.e., independent) events is
inessential. A key notion in concurrent models is _conflict_ (also known as
choices or decisions). Basically, two events are in conflict when they cannot
occur in the same execution. The interplay between concurrency and conflicts
introduces a phenomenon in which the execution of an event can be influenced
by the occurrence of another concurrent (and hence independent) event. Such
situation, known as _confusion_ , naturally arises in concurrent and
distributed systems and is intrinsic to problems involving mutual exclusion
[26]. When interleaving semantics is considered, the problem is less
compelling, however it has been recognised and studied from the beginning of
net research [25], and to address it in a general and acceptable way can be
considered as a long-standing open problem for concurrency theory.

To illustrate confusion, we rely on Petri nets [23, 24], which are a basic,
well understood model of concurrency.

$\textstyle{\bullet}$$\textstyle{\scriptstyle{1}}$$\textstyle{a}$$\textstyle{d}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{2}}$
$\textstyle{\scriptstyle{3}}$
$\textstyle{\scriptstyle{6}}$$\textstyle{b}$$\textstyle{c}$
$\textstyle{\scriptstyle{4}}$ $\textstyle{\scriptstyle{5}}$

$\textstyle{a\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{d}$$\textstyle{b\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{c}$

(a) Asymmetric confusion

$\textstyle{\bullet}$$\textstyle{\scriptstyle{1}}$$\textstyle{a}$$\textstyle{d}$
$\textstyle{\scriptstyle{3}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{2}}$
$\textstyle{\scriptstyle{6}}$ $\textstyle{\scriptstyle{\neg
c}}$$\textstyle{c}$$\textstyle{b_{1}}$$\textstyle{b_{2}}$
$\textstyle{\scriptstyle{5}}$ $\textstyle{\scriptstyle{4}}$

$\textstyle{a\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{d\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{b_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{c}$$\textstyle{b_{2}}$

(b) Removing confusion

Figure 1. Some nets (top) and their event structures (bottom)

The simplest example of (asymmetric) confusion is the net in Fig. 1(a). We
assume the reader is familiar with the firing semantics of Petri nets,
otherwise see the short summary in Section 2.2. The net has two traces
involving the concurrent events $a$ and $b$, namely $\sigma_{1}=a;b$ and
$\sigma_{2}=b;a$. Both traces define the same concurrent execution.
Contrastingly, $\sigma_{1}$ and $\sigma_{2}$ are associated with completely
different behaviours of the system as far as the resolution of choices is
concerned. In fact, the system makes two choices while executing $\sigma_{1}$:
firstly, it chooses $a$ over $d$, enabling $c$ as an alternative to $b$;
secondly, $b$ is selected over $c$. Differently, the system makes just one
choice in $\sigma_{2}$: since initially $c$ is not enabled, $b$ is executed
without any choice; after that, the system chooses $a$ over $d$. As
illustrated by this example, the choices made by two different traces of the
same concurrent computation may differ depending on the order in which
concurrent events occur.

The fundamental problem behind confusion relates to the description of
distributed, global choices. Such problem becomes essential when choices are
driven by probabilistic distributions and one wants to assign probabilities to
executions, as it is the case with probabilistic, concurrent models. Consider
again Fig. 1(a) and assume that $a$ is chosen over $d$ with probability
$p_{a}$ while $b$ is chosen over $c$ with probability $p_{b}$. When driven by
independent choices, the trace $\sigma_{1}$ has probability $p_{a}\cdot
p_{b}$, while $\sigma_{2}$ has probability $1\cdot p_{a}=p_{a}$. Hence, two
linear representations of the same concurrent computation, which are deemed
equivalent, would be assigned different probabilities.

Different solutions have been proposed in the literature for adding
probabilities to Petri nets [11, 19, 20, 12, 17, 14, 6, 15]. To avoid
confusion, most of them replace nondeterminism with probability only in part,
or disregard concurrency, or introduce time dependent stochastic
distributions, thus giving up the time and speed independence features typical
of truly concurrent models. Confusion-free probabilistic models have been
studied in [28], but this class, which subsumes free-choice nets, is usually
considered quite restrictive. More generally, the distributability of
decisions has been studied, e.g., in [27, 16], but while the results in [27]
apply to some restricted classes of nets, the approach in [16] requires nets
to be decorated with agents and produces distributed models with both
nondeterminism and probability, where concurrency depends on the scheduling of
agents.

$\textstyle{a\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathbb{C}_{1}}$$\textstyle{d}$$\textstyle{b\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{c}$
(a) Initial configuration

$\textstyle{a\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{b\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathbb{C}_{2}}$$\textstyle{c}$
(b) $a$ is chosen

$\textstyle{d}$$\textstyle{b\ignorespaces}$$\textstyle{\mathbb{C}_{3}}$ (c)
$d$ is chosen

Figure 2. AB’s dynamic branching cells for the example in Fig. 1(a)

A substantial advance has been contributed by Abbes and Benveniste (AB) [1, 2,
3]. They consider prime event structures and provide a branching cell
decomposition that establishes the order in which choices are resolved (see
Section 4.2). Intuitively, the event structure in Fig. 1(a) has the three
branching cells outlined in Fig. 2. First a decision between $a$ and $d$ must
be taken (Fig. 2(a)): if $a$ is executed, then a subsequent branching cell
$\\{b,c\\}$ is enabled (Fig. 2(b)); otherwise (i.e., if $d$ is chosen) the
trivial branching cell $\\{b\\}$ is enabled (Fig. 2(c)). In this approach, the
trace $\sigma_{2}=b;a$ is not admissible, because the branching cell $\\{b\\}$
does not exist in the original decomposition (Fig. 2(a)): it appears after the
choice of $d$ over $a$ has been resolved. Branching cells are equipped with
independent probability distributions and the probability assigned to a
concurrent execution is given by the product of the probabilities assigned by
its branching cells. Notably, the sum of the probabilities of maximal
configurations is 1. Every decomposition of a configuration yields an
execution sequence compatible with that configuration. Unfortunately, certain
sequences of events, legal w.r.t. the configuration, are not executable
according to AB.

### Problem statement

The question addressed in this paper is a foundational one: _can concurrency
and general probabilistic distributions coexist in Petri nets? If so, under
which circumstances?_ By _coexistence_ we mean that all the following issues
must be addressed:

  1. (1)

_Speed independence_ : Truly concurrent semantics usually requires computation
to be time-independent and also independent from the relative speed of
processes. In this sense, while attaching rates of stochastic distributions to
transitions is perfectly fine with interleaving semantics, they are not suited
when truly concurrent semantics is considered.

  2. (2)

_Schedule independence_ : Concurrent events must be driven by independent
probability distributions. This item is tightly related to the confusion
problem, where the set of alternatives, and thus their probability
distribution, can be changed by the execution of some concurrent event.

  3. (3)

_Probabilistic computation_ : Nondeterministic choices must be replaceable by
probabilistic choices. This means that whenever two transitions are enabled,
the choice to fire one instead of the other is either inessential (because
they are concurrent) or is driven by some probability distribution.

  4. (4)

_Complete concurrency_ : It must be possible to establish a bijective
correspondence between equivalence classes of firing sequences and a suitable
set of concurrent processes. In particular, given a concurrent process it must
be possible to recover all its underlying firing sequences.

  5. (5)

_Sanity check #1_ : All firing sequences of the same process carry the same
probability, i.e., the probability of a concurrent computation is independent
from the order of execution.

  6. (6)

_Sanity check #2_ : The sum of the probabilities assigned to all possible
maximal processes must be $1$.

In this paper we provide a positive answer for finite occurrence nets: given
any such net we show how to define loci of decisions, called _structural
branching cells_ (_s-cells_), and construct another net where independent
probability distributions can be assigned to concurrent events. This means
that each s-cell can be assigned to a distributed random agent and that any
concurrent computation is independent from the scheduling of agents.

### Overview of the approach

$\textstyle{\bullet}$$\textstyle{\scriptstyle{1}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{7}}$$\textstyle{a}$$\textstyle{d}$$\textstyle{e}$$\textstyle{f}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{2}}$
$\textstyle{\scriptstyle{3}}$ $\textstyle{\scriptstyle{6}}$
$\textstyle{\scriptstyle{8}}$
$\textstyle{\scriptstyle{9}}$$\textstyle{b}$$\textstyle{c}$$\textstyle{g}$
$\textstyle{\scriptstyle{4}}$ $\textstyle{\scriptstyle{5}}$
$\textstyle{\scriptstyle{10}}$

$\textstyle{a\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{d}$$\textstyle{e\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{f}$$\textstyle{b\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{c\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{g}$

(a) Confusion with OR-causes

$\textstyle{\bullet}$$\textstyle{\scriptstyle{1}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{7}}$$\textstyle{a}$$\textstyle{d}$$\textstyle{e}$$\textstyle{f}$
$\textstyle{\scriptstyle{3}}$ $\textstyle{\scriptstyle{6}}$
$\textstyle{\scriptstyle{\neg c}}$ $\textstyle{\scriptstyle{8}}$
$\textstyle{\scriptstyle{9}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{2}}$$\textstyle{b}$$\textstyle{c}$$\textstyle{bg}$$\textstyle{g}$
$\textstyle{\scriptstyle{4}}$ $\textstyle{\scriptstyle{5}}$
$\textstyle{\scriptstyle{10}}$ (b) An attempt

$\textstyle{\bullet}$$\textstyle{\scriptstyle{1}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{7}}$$\textstyle{a}$$\textstyle{d}$$\textstyle{e}$$\textstyle{f}$
$\textstyle{\scriptstyle{3}}$ $\textstyle{\scriptstyle{6}}$
$\textstyle{\scriptstyle{\neg c}}$ $\textstyle{\scriptstyle{8}}$
$\textstyle{\scriptstyle{9}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{2}}$$\textstyle{b}$$\textstyle{c}$$\textstyle{bg}$$\textstyle{g}$
$\textstyle{\scriptstyle{4}}$ $\textstyle{\scriptstyle{5}}$
$\textstyle{\scriptstyle{10}}$ (c) A solution with persistent places

Figure 3. Running example

Following the rationale behind AB’s approach, a net is transformed into
another one that postpones the execution of choices that can be affected by
pending decisions. According to this intuition, the net in Fig. 1(a) is
transformed into another one that delays the execution of $b$ until all its
potential alternatives (i.e., $c$) are enabled or definitively excluded. In
this sense, $b$ should never be executed before the decision between $a$ and
$d$ is taken, because $c$ could still be enabled (if $a$ is chosen). As a
practical situation, imagine that $a$ and $d$ are the choices of your partner
to either come to town ($a$) or go to the sea ($d$) and that you can go to the
theatre alone ($b$), which is always an option, or go together with him/her
($c$), which is possible only when he/she is in town and accepts the
invitation. Of course you better postpone the decision until you know if your
partner is in town or not. This behaviour is faithfully represented, e.g., by
the confusion-free net in Fig. 1(b), where two variants of $b$ are made
explicit: $b_{1}$ (your partner is in town) and $b_{2}$ (your partner is not
in town). The new place $\neg c$ represents the fact that $c$ will never be
enabled. Now, from the concurrency point of view, there is a single process
that comprises both $a$ and $b_{1}$ (with $a$ a cause of $b_{1}$), whose
overall probability is the product of the probability of choosing $a$ over $d$
by the probability of choosing $b_{1}$ over $c$. The other two processes
comprise, respectively, $d$ and $b_{2}$ (with $d$ a cause of $b_{2}$) and $a$
and $c$ (with $a$ a cause of $c$). As the net is confusion-free all criteria
in the desiderata are met.

The general situation is more involved because: i) there can be several ways
to disable the same transition; ii) resolving a choice may require to execute
several transitions at once. Consider the net in Fig. 3(a): i) $c$ is
discarded as soon as $d$ _or_ $f$ fires; and ii) when both $a$ and $e$ are
fired we can choose to execute $c$ alone or _both_ $b$ and $g$. Likewise the
previous example, we may expect to transform the net as in Fig. 3(b). Again,
the place $\neg c$ represents the permanent disabling of $c$. This way a
probability distribution can drive the choice between $c$ and (the joint
execution of) $bg$, whereas $b$ and $g$ (if enabled) can fire concurrently
when $\neg c$ is marked.

A few things are worth remarking: i) a token in $\neg c$ can be needed several
times (e.g., to fire $b$ and $g$), hence tokens should be read but not
consumed from $\neg c$ (whence the double headed arcs from $\neg c$ to $b$ and
$g$, called _self-loops_); ii) several tokens can appear in the place $\neg c$
(by firing both $d$ and $f$). These facts have severe repercussions on the
concurrent semantics of the net. Suppose the trace $d;f;b$ is observed. The
firings of $d$ and $f$ produce two tokens in the place $\neg c$: Does $b$
causally depend on the token generated from $d$ or from $f$ (or from both)?
Moreover, consider the trace $d;e;b;g$, in which $b$ takes and releases a
token in $\neg c$. Does $g$ causally depend on $b$ (due to such self-loop)?
This last question can be solved by replacing self-loops with _read arcs_
[21], so that the firing of $b$ does not alter the content of $\neg c$ and
thus no causal dependency arises between $b$ and $g$. Nevertheless, if process
semantics or event semantics is considered, then we should explode all
possible combinations of causal dependencies, thus introducing a new,
undesired kind of nondeterminism. In reality, we should not expect any causal
dependency between $b$ and $g$, while both have OR dependencies on $d$ and
$f$.

To account for OR dependencies, we exploit the notion of _persistence_ :
tokens in a persistent place have infinite weight and are collective. Namely,
once a token reaches a persistent place, it cannot be removed and if two
tokens reach the same persistent place they are indistinguishable. Such
networks are a variant of ordinary P/T nets and have been studied in [10]. In
the example, we can declare $\neg c$ to be a persistent place and replace
self-loops/read arcs on $\neg c$ with ordinary outgoing arcs (see Fig. 3(c)).
Nicely we are able to introduce a process semantics for nets with persistent
places that satisfies complete concurrency.

The place $\neg c$ in the examples above is just used to sketch the general
idea: our transformation introduces persistent places like
$\mathbf{\overline{3}}$ to express that a token will never appear in the
regular place $3$.

### Contribution.

In this paper we show how to systematically derive confusion-free nets (with
persistency) from any (finite, occurrence) Petri net and equip them with
probabilistic distributions and concurrent semantics in the vein of AB’s
construction.

Technically, our approach is based on a structurally recursive decomposition
of the original net in s-cells. A simple kind of Asperti-Busi’s dynamic nets
is used as an intermediate model to structure the coding. While not strictly
necessary, the intermediate step emphasises the hierarchical nature of the
construction. The second part is a general flattening step independent of our
special case. Our definition is purely local (to s-cells), static and
compositional, whereas AB’s is dynamic and global (i.e., it requires the
entire PES). Using nets with persistency, we compile the execution strategy of
nets with confusion in a statically defined, confusion-free, operational
model. The advantage is that the concurrency within a process of the obtained
p-net is consistent with execution, i.e., all linearizations of a persistent
process are executable.

### Structure of the paper

After fixing notation in Section 2, our solution to the confusion problem
consists of the following steps: (i) we define s-cells in a compositional way
(Section 3.1); (ii) from s-cells decomposition and the use of dynamic nets, we
derive a confusion-free net with persistency (Section 3.2); (iii) we prove the
correspondence with AB’s approach (Section 4); (iv) we define a new notion of
process that accounts for OR causal dependencies and satisfies complete
concurrency (Section 5); and (v) we show how to assign probabilistic
distributions to s-cells (Section 6). For the sake of readability, all proofs
of main results can be found in Appendix.

##  2\. Preliminaries

###  2.1. Notation

We let $\mathbb{N}$ be the set of natural numbers,
$\mathbb{N}_{\infty}=\mathbb{N}\cup\\{\infty\\}$ and $\mathbb{2}=\\{0,1\\}$.
We write $U^{S}$ for the set of functions from $S$ to $U$: hence a subset of
$S$ is an element of $\mathbb{2}^{S}$, a multiset $m$ over $S$ is an element
of $\mathbb{N}^{S}$, and a bag $b$ over $S$ is an element of
$\mathbb{N}_{\infty}^{S}$. By overloading the notation, union, difference and
inclusion of sets, multisets and bags are all denoted by the same symbols:
$\cup$, $\setminus$ and $\subseteq$, respectively. In the case of bags, the
difference $b\setminus m$ is defined only when the second argument is a
multiset, with the convention that $(b\setminus m)(s)=\infty$ if
$b(s)=\infty$. Similarly, $(b\cup b^{\prime})(s)=\infty$ if $b(s)=\infty$ or
$b^{\prime}(s)=\infty$. A set can be seen as a multiset or a bag whose
elements have unary multiplicity. Membership is denoted by $\in$: for a
multiset $m$ (or a bag $b$), we write $s\in m$ for $m(s)\neq 0$ ($b(s)\neq
0$). Given a relation $R\subseteq S\times S$, we let $R^{+}$ be its transitive
closure and $R^{*}$ be its reflexive and transitive closure. We say that $R$
is _acyclic_ if $\forall s\in S.~{}(s,s)\not\in R^{+}$.

###  2.2. Petri Nets, confusion and free-choiceness

A _net structure_ $N$ (also _Petri net_) [23, 24] is a tuple $(P,T,F)$ where:
$P$ is the set of places, $T$ is the set of transitions, and
$F\subseteq(P\times T)\cup(T\times P)$ is the flow relation. For $x\in P\cup
T$, we denote by ${}^{\bullet}{x}=\\{y\mid(y,x)\in F\\}$ and
$x^{\bullet}=\\{z\mid(x,z)\in F\\}$ its _pre-set_ and _post-set_ ,
respectively. We assume that $P$ and $T$ are disjoint and non-empty and that
${}^{\bullet}{t}$ and $t^{\bullet}$ are non empty for every $t\in T$. We write
$t:X\to Y$ for $t\in T$ with $X={}^{\bullet}{t}$ and $Y=t^{\bullet}$.

A _marking_ is a multiset $m\in\mathbb{N}^{P}$. We say that $p$ is _marked_ at
$m$ if $p\in m$. We write $(N,m)$ for the net $N$ _marked_ by $m$. We write
$m_{0}$ for the initial marking of the net, if any.

Graphically, a Petri net is a directed graph whose nodes are the places and
transitions and whose set of arcs is $F$. Places are drawn as circles and
transitions as rectangles. The marking $m$ is represented by inserting $m(p)$
tokens in each place $p\in m$ (see Fig. 1).

A transition $t$ is _enabled_ at the marking $m$, written $m\xrightarrow{t}$,
if ${}^{\bullet}{t}\subseteq m$. The execution of a transition $t$ enabled at
$m$, called _firing_ , is written $m\xrightarrow{t}m^{\prime}$ with
$m^{\prime}=(m\setminus{}^{\bullet}{t})\cup t^{\bullet}$. A firing sequence
from $m$ to $m^{\prime}$ is a finite sequence of firings
$m=m_{0}\xrightarrow{t_{1}}\cdots\xrightarrow{t_{n}}m_{n}=m^{\prime}$,
abbreviated to $m\xrightarrow{t_{1}\cdots t_{n}}m^{\prime}$ or just
$m\rightarrow^{*}m^{\prime}$. Moreover, it is _maximal_ if no transition is
enabled at $m^{\prime}$. We write $m\xrightarrow{t_{1}\cdots t_{n}}$ if there
is $m^{\prime}$ such that $m\xrightarrow{t_{1}\cdots t_{n}}m^{\prime}$. We say
that $m^{\prime}$ is _reachable_ from $m$ if $m\rightarrow^{*}m^{\prime}$. The
set of markings reachable from $m$ is written $[m\rangle$. A marked net
$(N,m)$ is _safe_ if each $m^{\prime}\in[m\rangle$ is a set.

Two transition $t,u$ are in _direct conflict_ if
${}^{\bullet}{t}\cap{}^{\bullet}{u}\neq\emptyset$. A net is called _free-
choice_ if for all transitions $t,u$ we have either
${}^{\bullet}{t}={}^{\bullet}{u}$ or
${}^{\bullet}{t}\cap{}^{\bullet}{u}=\emptyset$, i.e., if a transition $t$ is
enabled then all its conflicting alternatives are also enabled. Note that
free-choiceness is purely structural. Confusion-freeness considers instead the
dynamics of the net. A safe marked net $(N,m_{0})$ has confusion iff there
exists a reachable marking $m$ and transitions $t,u,v$ such that:

  1. (1)

(i) $t,u,v$ are enabled at $m$, (ii)
${}^{\bullet}{t}\cap{}^{\bullet}{u}\neq\emptyset\neq{}^{\bullet}{u}\cap{}^{\bullet}{v}$,
(iii) ${}^{\bullet}{t}\cap{}^{\bullet}{v}=\emptyset$ (symmetric case); or

  2. (2)

(i) $t$ and $v$ are enabled at $m$, (ii) $u$ is not enabled at $m$ but it
becomes enabled after the firing of $t$, and (iii)
${}^{\bullet}{t}\cap{}^{\bullet}{v}=\emptyset$ and
${}^{\bullet}{v}\cap{}^{\bullet}{u}\neq\emptyset$ (asymmetric case).

In case 1, $t$ and $v$ are concurrently enabled but the firing of one disables
an alternative ($u$) to the other. In case 2, the firing of $t$ enables an
alternative to $u$. An example of symmetric confusion is given by
$m=\\{2,3,8\\}$, $t=b$, $u=c$ and $v=g$ in Fig. 3(a), while for the asymmetric
case take $m=\\{1,2\\}$, $t=a$, $v=b$ and $u=c$ in Fig. 1(a). A net is
_confusion-free_ when it has no confusion.

###  2.3. Deterministic Nonsequential Processes

A _deterministic nonsequential process_ (or just _process_) [13] represents
the equivalence class of all firing sequences of a net that only differ in the
order in which concurrent firings are executed. It is given as a mapping
$\pi:\mathcal{D}\to N$ from a _deterministic occurrence net_ $\mathcal{D}$ to
$N$ (preserving pre- and post-sets), where a deterministic occurrence net is
such that: (1) the flow relation is acyclic, (2) there are no backward
conflicts ($\forall p\in P.~{}|{}^{\bullet}{p}|\leq 1$), and (3) there are no
forward conflicts ($\forall p\in P.~{}|p^{\bullet}|\leq 1$). We let
${}^{\circ}{\mathcal{D}}=\\{p\,\mid\,{}^{\bullet}{p}=\emptyset\\}$ and
$\mathcal{D}^{\circ}=\\{p\,\mid\,p^{\bullet}=\emptyset\\}$ be the sets of
_initial_ and _final places_ of $\mathcal{D}$, respectively (with
$\pi({}^{\circ}{\mathcal{D}})$ be the initial marking of $N$). When $N$ is an
acyclic safe net, the mapping $\pi:\mathcal{D}\to N$ is just an injective
graph homomorphism: without loss of generality, we name the nodes in
$\mathcal{D}$ as their images in $N$ and let $\pi$ be the identity. The firing
sequences of a processes $\mathcal{D}$ are its maximal firing sequences
starting from the marking ${}^{\circ}{\mathcal{D}}$. A process of $N$ is
_maximal_ if its firing sequences are maximal in $N$.

$\textstyle{\bullet}$$\textstyle{\scriptstyle{1}}$$\textstyle{a}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{2}}$
$\textstyle{\scriptstyle{3}}$$\textstyle{b}$ $\textstyle{\scriptstyle{4}}$ (a)
Concurrent run ($a$ and $b$)

$\textstyle{\bullet}$$\textstyle{\scriptstyle{1}}$$\textstyle{d}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{2}}$
$\textstyle{\scriptstyle{6}}$$\textstyle{b}$ $\textstyle{\scriptstyle{4}}$ (b)
Concurrent run ($b$ and $d$)

$\textstyle{\bullet}$$\textstyle{\scriptstyle{1}}$$\textstyle{a}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{2}}$
$\textstyle{\scriptstyle{3}}$$\textstyle{c}$ $\textstyle{\scriptstyle{5}}$ (c)
Sequential run ($a$ before $c$)

Figure 4. Maximal processes for the net in Fig. 1(a)

For example, take the net in Fig. 1(a). It has three maximal processes that
are reported in Fig. 4. The equivalence class of the firing sequences
$m_{0}\xrightarrow{a\,b}$ and $m_{0}\xrightarrow{b\,a}$ is the maximal process
$\mathcal{D}$ in Fig. 4(a) with places $\\{1,2,3,4\\}$ and transitions
$\\{a:1\to 3,b:2\to 4\\}$, where ${}^{\circ}{\mathcal{D}}=\\{1,2\\}$ and
$\mathcal{D}^{\circ}=\\{3,4\\}$. Likewise, the equivalence class of the firing
sequences $m_{0}\xrightarrow{b\,d}$ and $m_{0}\xrightarrow{d\,b}$ is the
maximal process in Fig. 4(b). As $c$ can only be executed after $a$, the
corresponding process is in Fig.4(c).

Given an acyclic net we let $\preceq=F^{*}$ be the (reflexive) _causality_
relation and say that two transitions $t_{1}$ and $t_{2}$ are in _immediate
conflict_ , written $t_{1}\\#_{0}t_{2}$ if $t_{1}\neq
t_{2}\;\wedge\;{}^{\bullet}{t_{1}}\cap{}^{\bullet}{t_{2}}\neq\emptyset$. The
_conflict relation_ $\\#$ is defined by letting $x\\#y$ if there are
$t_{1},t_{2}\in T$ such that $(t_{1},x),(t_{2},y)\in F^{+}$ and
$t_{1}\\#_{0}t_{2}$. Then, a _nondeterministic occurrence net_ (or just
_occurrence net_) is a net $\mathcal{O}=(P,T,F)$ such that: (1) the flow
relation is acyclic, (2) there are no backward conflicts ($\forall p\in
P.~{}|{}^{\bullet}{p}|\leq 1$), and (3) there are no self-conflicts ($\forall
t\in T.~{}\neg(t\\#t)$). The _unfolding_ $\mathcal{U}(N)$ of a safe Petri net
$N$ is an occurrence net that accounts for all (finite and infinite) runs of
$N$: its transitions model all the possible instances of transitions in $N$
and its places model all the tokens that can be created in any run. Our
construction takes a finite occurrence net as input, which can be, e.g., the
(truncated) unfolding of any safe net.

###  2.4. Nets With Persistency

Nets with persistency (_p-nets_) [10] partition the set of places into regular
places $P$ (ranged by $p,q,...$) and persistent places $\mathbf{P}$ (ranged by
$\mathbf{p},\mathbf{q},...$). We use $s$ to range over
$\mathbb{S}=P\cup\mathbf{P}$ and write a p-net as a tuple $(\mathbb{S},T,F)$.
Intuitively, persistent places guarantee some sort of monotonicity about the
knowledge of the system. Technically, this is realised by letting states be
bags of places $b\in\mathbb{N}_{\infty}^{\mathbb{S}}$ instead of multisets,
with the constraint that $b(p)\in\mathbb{N}$ for any regular place $p\in P$
and $b(\mathbf{p})\in\\{0,\infty\\}$ for any persistent place
$\mathbf{p}\in\mathbf{P}$. To guarantee that this property is preserved by
firing sequences, we assume that the post-set $t^{\bullet}$ of a transition
$t$ is the bag such that: $(t^{\bullet})(p)=1$ if $(t,p)\in F$ (as usual);
$(t^{\bullet})(\mathbf{p})=\infty$ if $(t,\mathbf{p})\in F$; and
$(t^{\bullet})(s)=0$ if $(t,s)\not\in F$. We say that a transition $t$ is
_persistent_ if it is attached to persistent places only (i.e. if
${}^{\bullet}{t}\cup t^{\bullet}\subseteq\mathbf{P}$).

The notions of enabling, firing, firing sequence and reachability extend in
the obvious way to p-nets (when markings are replaced by bags). For example, a
transition $t$ is _enabled_ at the bag $b$, written $b\xrightarrow{t}$, if
${}^{\bullet}{t}\subseteq b$, and the firing of an enabled transitions is
written $b\xrightarrow{t}b^{\prime}$ with
$b^{\prime}=(b\setminus{}^{\bullet}{t})\cup t^{\bullet}$.

A firing sequence is _stuttering_ if it has multiple occurrences of a
persistent transition. Since firing a persistent transition $t$ multiple times
is inessential, we consider non-stuttering firing sequences. (Alternatively,
we can add a marked regular place $p_{t}$ to the preset of each persistent
transition $t$, so $t$ fires at most once.)

A marked p-net $(N,b_{0})$ is _$1$ -$\infty$-safe_ if each reachable bag
$b\in[b_{0}\rangle$ is such that $b(p)\in\mathbb{2}$ for all $p\in P$ and
$b(\mathbf{p})\in\\{0,\infty\\}$ for all $\mathbf{p}\in\mathbf{P}$. Note that
in $1$-$\infty$-safe nets the amount of information conveyed by any reachable
bag is finite, as each place is associated with one bit of information (marked
or unmarked). Graphically, persistent places are represented by circles with
double border (and they are either empty or contain a single token).

The notion of confusion extends to p-nets, by checking direct conflicts w.r.t.
regular places only.

$\textstyle{\bullet}$$\textstyle{\scriptstyle{1}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{2}}$$\textstyle{a}$$\textstyle{b}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{3}}$
$\textstyle{\scriptstyle{{\scriptstyle{\bf
4}}}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{5}}$$\textstyle{c}$$\textstyle{d}$
$\textstyle{\scriptstyle{6}}$ $\textstyle{\scriptstyle{7}}$ Figure 5. A marked
p-net

As an example, consider the $1$-$\infty$-safe, confusion-free p-net in Fig. 5.
After firing $a$ and $c$, the firing of $b$ is inessential to enable $d$,
because the persistent place ${\bf 4}$ is marked by $\infty$.

###  2.5. Dynamic Nets

Dynamic nets [4] are Petri nets whose sets of places and transitions may
increase dynamically. We focus on a subclass of persistent dynamic nets that
only allows for changes in the set of transitions, which is defined as
follows.

######  Definition  (Dynamic p-nets).

The set _$\textsc{dn}(\mathbb{S})$_ is the least set satisfying the recursive
equation:

$\textsc{dn}(\mathbb{S})=\\{(T,b)\;\;|\;\;T\subseteq
2^{\mathbb{S}}\times\textsc{dn}(\mathbb{S})\;\;\wedge\;\;T\mbox{ finite
}\wedge\;\;b\in\mathbb{N}_{\infty}^{\mathbb{S}}\\}$

The definition above is a domain equation for the set of dynamic p-nets over
the set of places $\mathbb{S}$: the set $\textsc{dn}(\mathbb{S})$ is the least
fixed point of the equation. The simplest elements in
$\textsc{dn}(\mathbb{S})$ are pairs $(\emptyset,b)$ with bag
$b\in\mathbb{N}_{\infty}^{\mathbb{S}}$ (with $b(p)\in\mathbb{N}$ for any $p\in
P$ and $b(\mathbf{p})\in\\{0,\infty\\}$ for any $\mathbf{p}\in\mathbf{P}$).
Nets $(T,b)$ are defined recursively; indeed any element $t=(S,N)\in T$ stands
for a transition with preset $S$ and postset $N$, which is another element of
$\textsc{dn}(\mathbb{S})$. An ordinary transition from $b$ to $b^{\prime}$ has
thus the form $(b,(\emptyset,b^{\prime}))$. We write $S\to N$ for the
transition $t=(S,N)$, ${}^{\bullet}{t}=S$ for its preset, and
$t^{\bullet}=N\in\textsc{dn}(\mathbb{S})$ for its postset. For $N=(T,b)$ we
say that $T$ is the set of _top transitions_ of $N$. All the other transitions
are called dynamic.

The firing rule rewrites a dynamic p-net $(T,b)$ to another one. The firing of
a transition $t=S\to(T^{\prime},b^{\prime})\in T$ consumes the preset $S$ and
releases both the transitions $T^{\prime}$ and the tokens in $b^{\prime}$.
Formally, if $t=S\to(T^{\prime},b^{\prime})\in T$ with $S\subseteq b$ then
$(T,b)\xlongrightarrow{t}(T\cup T^{\prime},(b\setminus S)\cup b^{\prime})$.

The notion of $1$-$\infty$-safe dynamic p-net is defined analogously to p-nets
by considering the bags $b$ of reachable states $(T,b)$.

$\textstyle{\color[rgb]{120,120,120}\bullet}$$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf
3}}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{2}}$
$\textstyle{\scriptstyle{3}}$$\textstyle{{t_{3}}}$$\textstyle{t_{b}}$$\textstyle{t_{c}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 5}}}$
$\textstyle{\scriptstyle{4}}$ $\textstyle{\scriptstyle{5}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 4}}}$ (a) A
dynamic p-net $N$

$\textstyle{\color[rgb]{120,120,120}\bullet}$$\textstyle{\color[rgb]{120,120,120}\bullet}$$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf
3}}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{2}}$$\textstyle{\color[rgb]{120,120,120}\bullet}$
$\textstyle{\scriptstyle{3}}$$\textstyle{\color[rgb]{120,120,120}t_{3}}$
$\textstyle{\scriptstyle{\color[rgb]{120,120,120}p_{b}}}$$\textstyle{t_{b}}$$\textstyle{t_{c}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 5}}}$
$\textstyle{\scriptstyle{4}}$ $\textstyle{\scriptstyle{5}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 4}}}$ (b) The
corresponding p-net $\llparenthesis N\rrparenthesis$

Figure 6. A dynamic p-net encoded as a p-net

A sample of a dynamic net is shown in Fig. 6(a), whose only dynamic
transition, which is activated by $t_{3}$, is depicted with dashed border. The
arrow between $t_{3}$ and $t_{b}$ denotes the fact that $t_{b}$ is activated
dynamically by the firing of $t_{3}:\overline{\bf 3}\to(\\{b:2\to
4\\},\\{\overline{\bf 5}\\})$.

We show that any dynamic p-net can be encoded as a (flat) p-net. Our encoding
resembles the one in [4], but it is simpler because we do not need to handle
place creation. Intuitively, we release any transition $t$ immediately but we
add a persistent place $\mathbf{p}_{t}$ to its preset, to enable $t$
dynamically ($\mathbf{p}_{t}$ is initially empty iff $t$ is not a top
transition). Given a set $T$ of transitions, $b_{T}$ is the bag such that
$b_{T}({\bf p}_{t})=\infty$ if $t\in T$ and $b_{T}(s)=0$ otherwise.

For $N=(T,b)\in\textsc{dn}(\mathbb{S})$, we let
$\mathbb{T}(N)=T\cup\bigcup_{t\in T}\mathbb{T}(t^{\bullet})$ be the set of all
(possibly nested) transitions appearing in $N$. From Definition 2.5 it follows
that $\mathbb{T}(N)$ is finite and well-defined.

######  Definition  (From dynamic to static).

Given $N=(T,b)\in\textsc{dn}(\mathbb{S})$, the corresponding p-net
$\llparenthesis N\rrparenthesis$ is defined as $\llparenthesis
N\rrparenthesis=(\mathbb{S}\cup{\bf P}_{\mathbb{T}(N)},\mathbb{T}(N),F,b\cup
b_{T})$, where

  * •

${\bf P}_{\mathbb{T}(N)}=\\{{\bf p}_{t}\ |\ t\in\mathbb{T}(N)\\}$; and

  * •

$F$ is such that for any $t=S\to(T^{\prime},b^{\prime})\in\mathbb{T}(N)$ then
$t:{}^{\bullet}{t}\cup\\{{\bf p}_{t}\\}\to b^{\prime}\cup b_{T^{\prime}}$.

The transitions of $\llparenthesis N\rrparenthesis$ are those from $N$ (set
$\mathbb{T}(N)$). Any place of $N$ is also a place of $\llparenthesis
N\rrparenthesis$ (set $\mathbb{S}$). In addition, there is one persistent
place ${\bf p}_{t}$ for each $t\in\mathbb{T}(N)$ (set ${\bf
P}_{\mathbb{T}(N)}$). The initial marking of $\llparenthesis N\rrparenthesis$
is that of $N$ (i.e., $b$) together with the persistent tokens that enable the
top transitions of $N$ (i.e., $b_{T}$). Adding $b_{T}$ is convenient for the
statement in Proposition 2.5, but we could safely remove ${\bf
P}_{T}\subseteq{\bf P}_{\mathbb{T}(N)}$ (and $b_{T}$) from the flat p-net
without any consequence.

######  Example .

The dynamic p-net $N$ in Fig. 6(a) is encoded as the p-net $\llparenthesis
N\rrparenthesis$ in Fig. 6(b), which has as many transitions as $N$, but the
preset of every transition contains an additional persistent place (depicted
in grey) to indicate transition’s availability. All the new places but $p_{b}$
are marked because the corresponding transitions are initially available.
Contrastingly, $p_{b}$ is unmarked because the corresponding transition
becomes available after the firing of $t_{3}$.

The following result shows that all computations of a dynamic p-net can be
mimicked by the corresponding p-net and vice versa. Hence, the encoding
preserves also 1-safety over regular places.

######  Proposition .

Let $N=(T,b)\in\textsc{dn}(\mathbb{S})$. Then,

  1. (1)

$N\xlongrightarrow{t}N^{\prime}$ implies $\llparenthesis
N\rrparenthesis\xlongrightarrow{t}\llparenthesis N^{\prime}\rrparenthesis$;

  2. (2)

Moreover, $\llparenthesis N\rrparenthesis\xlongrightarrow{t}N^{\prime}$
implies there exists $N^{\prime\prime}$ such that
$N\xlongrightarrow{t}N^{\prime\prime}$ and $N^{\prime}=\llparenthesis
N^{\prime\prime}\rrparenthesis$.

######  Corollary .

$\llparenthesis N\rrparenthesis$ is $1$-$\infty$-safe iff $N$ is 1-safe.

##  3\. From Petri Nets to Dynamic P-Nets

In this section we show that any (finite, acyclic) net $N$ can be associated
with a confusion-free, dynamic p-net $\llbracket N\rrbracket$ by suitably
encoding loci of decision. The mapping builds on the structural cell
decomposition introduced below.

###  3.1. Structural Branching Cells

A structural branching cell represents a statically determined locus of
choice, where the firing of some transitions is considered against all the
possible conflicting alternatives. To each transition $t$ we assign an s-cell
$[t]$. This is achieved by taking the equivalence class of $t$ w.r.t. the
equivalence relation $\leftrightarrow$ induced by the least preorder
$\sqsubseteq$ that includes immediate conflict $\\#_{0}$ and causality
$\preceq$. For convenience, each s-cell $[t]$ also includes the places in the
pre-sets of the transitions in $[t]$, i.e., we let the relation
$\mathsf{Pre}^{-1}$ be also included in $\sqsubseteq$, with
$\mathsf{Pre}=F\cap(P\times T)$. This way, if $(p,t)\in F$ then $p\sqsubseteq
t$ because $p\preceq t$ and $t\sqsubseteq p$ because
$(t,p)\in\mathsf{Pre}^{-1}$. Formally, we let $\sqsubseteq$ be the transitive
closure of the relation $\\#_{0}\ \cup\preceq\cup\ \mathsf{Pre}^{-1}$. Since
$\\#_{0}$ is subsumed by the transitive closure of the relation $\preceq\cup\
\mathsf{Pre}^{-1}$, we equivalently set $\sqsubseteq\ =(\preceq\cup\
\mathsf{Pre}^{-1})^{*}$. Then, we let $\leftrightarrow\ =\\{(x,y)\mid
x\sqsubseteq y\wedge y\sqsubseteq x\\}$. Intuitively, the choices available in
the equivalence class $[t]_{|\leftrightarrow}$ of a transition $t$ must be
resolved atomically.

######  Definition  (S-cells).

Let $N=(P,T,F)$ be a finite, nondeterministic occurrence net. The set
$\textsc{bc}(N)$ of _s-cells_ is the set of equivalence classes of
$\leftrightarrow$, i.e., $\textsc{bc}(N)=\\{[t]_{|\leftrightarrow}\mid t\in
T\\}$.

######  Remark .

Exploiting the algebraic structure of monoidal categories, in [8] we have
given an alternative characterization of s-cells as those nets that can be
decomposed neither in parallel nor in sequence. The alternative definition is
maybe more intuitive, but its formalization requires some technical machinery
which we prefer to leave out of the scope of the present paper.

We let $\mathbb{C}$ range over s-cells. By definition it follows that for all
$\mathbb{C},\mathbb{C}^{\prime}\in\textsc{bc}(N)$, if
$\mathbb{C}\cap\mathbb{C}^{\prime}\neq\emptyset$ then
$\mathbb{C}=\mathbb{C}^{\prime}$. For any s-cell $\mathbb{C}$, we denote by
$N_{\mathbb{C}}$ the subnet of $N$ whose elements are in
$\mathbb{C}\cup\bigcup_{t\in\mathbb{C}}t^{\bullet}$. Abusing the notation, we
denote by ${}^{\circ}{\mathbb{C}}$ the set of all the initial places in
$N_{\mathbb{C}}$ and by $\mathbb{C}^{\circ}$ the set of all the final places
in $N_{\mathbb{C}}$.

######  Definition  (Transactions).

Let $\mathbb{C}\in\textsc{bc}(N)$. Then, a _transaction_ $\theta$ of
$\mathbb{C}$, written $\theta:\mathbb{C}$, is a maximal (deterministic)
process of $N_{\mathbb{C}}$.

Since the set of transitions in a transaction $\theta$ uniquely determines the
corresponding process in $N_{\mathbb{C}}$, we write a transaction $\theta$
simply as the set of its transitions.

$\textstyle{\bullet}$$\textstyle{\scriptstyle{1}}$$\textstyle{\mathbb{C}_{1}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{7}}$$\textstyle{\mathbb{C}_{2}}$$\textstyle{a}$$\textstyle{d}$$\textstyle{e}$$\textstyle{f}$
$\textstyle{\scriptstyle{6}}$
$\textstyle{\scriptstyle{9}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{2}}$
$\textstyle{\scriptstyle{3}}$$\textstyle{\mathbb{C}_{3}}$
$\textstyle{\scriptstyle{8}}$$\textstyle{b}$$\textstyle{c}$$\textstyle{g}$
$\textstyle{\scriptstyle{4}}$ $\textstyle{\scriptstyle{5}}$
$\textstyle{\scriptstyle{\ 10}}$ (a) Structural branching cells

$\begin{array}[]{ll@{ = } l}\lx@intercol\mathbb{C}_{1}:\hfil\lx@intercol\\\
&\theta_{a}&\\{a\\}\\\ &\theta_{d}&\\{d\\}\\\\[5.0pt]
\lx@intercol\mathbb{C}_{2}:\hfil\lx@intercol\\\ &\theta_{e}&\\{e\\}\\\
&\theta_{f}&\\{f\\}\\\\[5.0pt] \lx@intercol\mathbb{C}_{3}:\hfil\lx@intercol\\\
&\theta_{c}&\\{c\\}\\\ &\theta_{bg}&\\{b,g\\}\end{array}$ (b) Transactions

$\textstyle{\scriptstyle{3}}$ $\textstyle{\scriptstyle{8}}$$\textstyle{g}$
$\textstyle{\scriptstyle{\ 10}}$ (c) $N_{\mathbb{C}_{3}}\ominus 2$

$\textstyle{\scriptstyle{2}}$
$\textstyle{\scriptstyle{8}}$$\textstyle{b}$$\textstyle{\mathbb{C}_{b}}$$\textstyle{g}$$\textstyle{\mathbb{C}_{g}}$
$\textstyle{\scriptstyle{4}}$ $\textstyle{\scriptstyle{\ 10}}$ (d)
$N_{\mathbb{C}_{3}}\ominus 3$

$\textstyle{\scriptstyle{2}}$ $\textstyle{\scriptstyle{3}}$$\textstyle{b}$
$\textstyle{\scriptstyle{4}}$ (e) $N_{\mathbb{C}_{3}}\ominus 8$

Figure 7. Structural branching cells (running example)

######  Example .

The net $N$ in Fig. 3(a) has the three s-cells shown in Fig. 7(a), whose
transactions are listed in Fig. 7(b). For $\mathbb{C}_{1}$ and
$\mathbb{C}_{2}$, each transition defines a transaction; $\mathbb{C}_{3}$ has
one transaction associated with $c$ and one with (the concurrent firing of)
$b$ and $g$.

The following operation $\ominus$ is instrumental for the definition of our
encoding and stands for the removal of a minimal place of a net and all the
elements that causally depend on it. Formally, $N\ominus p$ is the least set
that satisfies the rules (where ${}^{\circ}{\\_}$ has higher precedence over
set difference):

$q\in N\ominus pq\in{}^{\circ}{N}\setminus\\{p\\}\qquad t\in N\ominus pt\in
N\qquad{}^{\bullet}{t}\subseteq N\ominus p\qquad q\in N\ominus pt\in N\ominus
p\qquad q\in t^{\bullet}$

$\textstyle{\bullet}$$\textstyle{\scriptstyle{1}}$$\textstyle{\mathbb{C}_{1}}$$\textstyle{a}$$\textstyle{d}$
$\textstyle{\scriptstyle{3}}$
$\textstyle{\scriptstyle{6}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{2}}$$\textstyle{\mathbb{C}_{2}}$$\textstyle{\mathbb{C}_{3}}$$\textstyle{b}$$\textstyle{c}$
$\textstyle{\scriptstyle{4}}$ $\textstyle{\scriptstyle{5}}$ Figure 8. S-cells
for the net in Fig. 1(a)

######  Example .

Consider the net in Fig. 1(a). There are two main s-cells: $\mathbb{C}_{1}$
associated with $\\{a,d\\}$, and $\mathbb{C}_{2}$ with $\\{b,c\\}$. There is
also a nested s-cell $\mathbb{C}_{3}$ that arises from the decomposition of
the subnet $N_{\mathbb{C}_{2}}\ominus 3$. All the above s-cells are shown in
Fig. 8.

######  Example .

Consider the s-cells in Fig. 7(a). The net $N_{\mathbb{C}_{1}}\ominus 1$ is
empty because every node in $N_{\mathbb{C}_{1}}$ causally depends on $1$.
Similarly, $N_{\mathbb{C}_{2}}\ominus 7$ is empty. The cases for
$\mathbb{C}_{3}$ are in Figs. 7(c)–7(e).

###  3.2. Encoding s-cells as confusion-free dynamic nets

Intuitively, the proposed encoding works by explicitly representing the fact
that a place will not be marked in a computation. We denote with
$\overline{\bf p}$ the place that models such “negative” information about the
regular place $p$ and let $\overline{\bf P}=\\{{\bf\overline{p}}\ |\ p\in
P\\}$.111The notation $\overline{P}$ denotes just a set of places whose names
are decorated with a bar; it should not be confused with usual set complement.
The encoding uses negative information to recursively decompose s-cells under
the assumption that some of their minimal places will stay empty.

######  Definition  (From s-cells to dynamic p-nets).

Let $N=(P,T,F,m)$ be a marked occurrence net. Its dynamic p-net $\llbracket
N\rrbracket\in\textsc{dn}(P\cup\overline{\bf P})$ is defined as $\llbracket
N\rrbracket=(T_{\rm pos}\cup T_{\rm neg},m)$, where:

$\begin{array}[]{l@{\ }l@{\ }l}T_{\rm pos}&=&\\{\
{}^{\circ}{\mathbb{C}}\to(\emptyset,\theta^{\circ}\cup\overline{\mathbb{C}^{\circ}\setminus\theta^{\circ}})\
\mid\ \mathbb{C}\in\textsc{bc}(N)\ \mbox{and }\theta:\mathbb{C}\ \\}\\\ T_{\rm
neg}&=&\\{\ \overline{\bf
p}\to(T^{\prime},\overline{\mathbb{C}^{\circ}\setminus(N_{\mathbb{C}}\ominus
p)^{\circ}})\ \mid\;\mathbb{C}\in\textsc{bc}(N)\ \mbox{and
}p\in{}^{\circ}{\mathbb{C}}\\\ &&\phantom{\\{\ \overline{\bf
p}\to(T^{\prime},\overline{\mathbb{C}^{\circ}\setminus(N_{\mathbb{C}}\ominus
p)^{\circ}})\ \mid\;}\;\mbox{and }(T^{\prime},b)=\llbracket
N_{\mathbb{C}}\ominus p\rrbracket\ \\}\end{array}$

For any s-cell $\mathbb{C}$ of $N$ and transaction $\theta:\mathbb{C}$, the
encoding generates a transition
$t_{\theta,\mathbb{C}}=({}^{\circ}{\mathbb{C}}\to(\emptyset,\theta^{\circ}\cup\overline{\mathbb{C}^{\circ}\setminus\theta^{\circ}}))\in
T_{\rm pos}$ to mimic the atomic execution of $\theta$. Despite
${}^{\circ}{\theta}$ may be strictly included in ${}^{\circ}{\mathbb{C}}$, we
define ${}^{\circ}{\mathbb{C}}$ as the preset of $t_{\theta,\mathbb{C}}$ to
ensure that the execution of $\theta$ only starts when the whole s-cell
$\mathbb{C}$ is enabled. Each transition $t_{\theta,\mathbb{C}}\in T_{\rm
pos}$ is a transition of an ordinary Petri net because its postset consists of
(i) the final places of $\theta$ and (ii) the negative versions of the places
in $\mathbb{C}^{\circ}\setminus\theta^{\circ}$. A token in
$\overline{\bf{p}}\in\overline{\mathbb{C}^{\circ}\setminus\theta^{\circ}}$
represents the fact that the corresponding ordinary place
$p\in\mathbb{C}^{\circ}$ will not be marked because it depends on discarded
transitions (not in $\theta$).

Negative information is propagated by the transitions in $T_{\rm neg}$. For
each cell $\mathbb{C}$ and place $p\in{}^{\circ}{\mathbb{C}}$, there exists
one dynamic transition $t_{p,\mathbb{C}}=\overline{\bf
p}\to(T^{\prime},\overline{\mathbb{C}^{\circ}\setminus(N_{\mathbb{C}}\ominus
p)^{\circ}})$ whose preset is just $\overline{\bf p}$ and whose postset is
defined in terms of the subnet $N_{\mathbb{C}}\ominus p$. The postset of
$t_{p,\mathbb{C}}$ accounts for two effects of propagation: (i) the generation
of the negative tokens for all maximal places of $\mathbb{C}$ that causally
depend on $p$, i.e., for the negative places associated with the ones in
$\mathbb{C}^{\circ}$ that are not in $(N_{\mathbb{C}}\ominus p)^{\circ}$; and
(ii) the activation of all transitions $T^{\prime}$ obtained by encoding
$N_{\mathbb{C}}\ominus p$, i.e., the behaviour of the branching cell
$\mathbb{C}$ after the token in the minimal place $p$ is excluded. We remark
that the bag $b$ in $(T^{\prime},b)=\llbracket N_{\mathbb{C}}\ominus
p\rrbracket$ is always empty, because i) $N_{\mathbb{C}}$ is unmarked and,
consequently, $N_{\mathbb{C}}\ominus p$ is unmarked, and ii) the initial
marking of $\llbracket N\rrbracket$ corresponds to the initial marking of $N$.

$\textstyle{\bullet}$$\textstyle{\scriptstyle{1}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf
1}}}$$\textstyle{t_{a}}$$\textstyle{t_{d}}$ $\textstyle{\scriptstyle{3}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 6}}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 3}}}$
$\textstyle{\scriptstyle{6}}$ (a) S-cell $\mathbb{C}_{1}$

$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 2}}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf
3}}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{2}}$
$\textstyle{\scriptstyle{3}}$$\textstyle{t_{b}}$$\textstyle{t^{\prime}_{b}}$$\textstyle{t_{c}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 5}}}$
$\textstyle{\scriptstyle{4}}$ $\textstyle{\scriptstyle{5}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 4}}}$ (b)
S-cell $\mathbb{C}_{2}$ and its sub s-cell $\mathbb{C}_{3}$

$\textstyle{\bullet}$$\textstyle{\scriptstyle{1}}$$\textstyle{t_{d}}$$\textstyle{t_{a}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 3}}}$
$\textstyle{\scriptstyle{6}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf
6}}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{2}}$
$\textstyle{\scriptstyle{3}}$
$\textstyle{\scriptstyle{\color[rgb]{120,120,120}p_{b}}}$$\textstyle{t_{b}}$$\textstyle{t^{\prime}_{b}}$$\textstyle{t_{c}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 5}}}$
$\textstyle{\scriptstyle{4}}$ $\textstyle{\scriptstyle{5}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 4}}}$ (c) Flat
net (pruned)

Figure 9. S-cells as dynamic nets and their composed, flattened version (for
the net in Fig. 1(a))

######  Example .

We sketch the main ideas over the net in Fig. 1(a). We recall that it has two
main s-cells ($\mathbb{C}_{1}$ associated with $\\{a,d\\}$, and
$\mathbb{C}_{2}$ with $\\{b,c\\}$) and a nested one ($\mathbb{C}_{3}$): see
Fig. 8. Their dynamic nets are in Figs. 9(a)–9(b), where auxiliary transitions
are in grey and unlabeled. Places $\mathbf{\overline{1}}$ and
$\mathbf{\overline{2}}$ (and their transitions) are irrelevant, because the
places $1$ and $2$ are already marked. However, our cells being static, we
need to introduce auxiliary places in all cases. Note that in Fig. 9(b) there
is an arc between two transitions. As explained before, this is because the
target transition is dynamically created when the other is executed (hence the
dashed border). Also note that there are two transitions with the same
subscript $b$: one ($t^{\prime}_{b}$) is associated with the s-cell
$\mathbb{C}_{2}$, the other ($t_{b}$) with the unique s-cell $\mathbb{C}_{3}$
of $N_{\mathbb{C}_{2}}\ominus 3$ and is released when the place
$\mathbf{\overline{3}}$ becomes marked.

After the s-cells are assembled and flattened we get the p-net in Fig. 9(c)
(where irrelevant nodes are pruned). Initially, $t_{a}$ and $t_{d}$ are
enabled. Firing $t_{a}$ leads to the marking $\\{2,3,\mathbf{\overline{6}}\\}$
where $t^{\prime}_{b}:\\{2,3\\}\to\\{4,\mathbf{\overline{5}}\\}$ and
$t_{c}:\\{2,3\\}\to\\{\mathbf{\overline{4}},5\\}$ are enabled (and in
conflict). Firing $t_{d}$ instead leads to the marking
$\\{2,\mathbf{\overline{3}},6\\}$ where only the auxiliary transition can be
fired, enabling $t_{b}:\\{2,\mathbf{p}_{b}\\}\to 4$. The net is confusion-
free, as every conflict involves transitions with the same preset. For
example, as the places $3$ and $\mathbf{\overline{3}}$ (and thus
$\mathbf{\overline{p}}_{b}$) are never marked in a same run, the transitions
$t^{\prime}_{b}:\\{2,3\\}\to\\{4,\mathbf{\overline{5}}\\}$ and
$t_{b}:\\{2,\mathbf{p}_{b}\\}\to 4$ will never compete for the token in $2$.

######  Example .

$\begin{array}[]{l@{}l}\begin{array}[]{l@{\ : \ }l@{}l@{\
}l}t_{a}&1\to(\emptyset,\\{3,\overline{\bf 6}\\})&&\mbox{for}\ \theta_{a}\\\
t_{d}&1\to(\emptyset,\\{6,\overline{\bf 3}\\})&&\mbox{for}\
\theta_{d}\\\\[3.0pt] t_{1}&\overline{\bf 1}\to(\emptyset,\\{\overline{\bf
3},\overline{\bf 6}\\})\\\\[2.0pt] t_{e}&7\to(\emptyset,\\{8,\overline{\bf
9}\\})&&\mbox{for}\ \theta_{e}\\\ t_{f}&7\to(\emptyset,\\{9,\overline{\bf
8}\\})&&\mbox{for}\ \theta_{f}\\\\[3.0pt] t_{7}&\overline{\bf
7}\to(\emptyset,\\{\overline{\bf 8},\overline{\bf 9}\\})\\\\[2.0pt]
t_{bg}&2,3,8\to(\emptyset,\\{4,10,\overline{\bf 5}\\})&&\mbox{for}\
\theta_{bg}\\\ t_{c}&2,3,8\to(\emptyset,\\{5,\overline{\bf 4},\overline{\bf
10}\\})&&\mbox{for}\ \theta_{c}\end{array}&\begin{array}[]{l@{\ : \
}l@{}l@{}l}t_{2}&\overline{\bf
2}\to(\\{t_{g},t^{\prime}_{8}\\},\\{\overline{\bf 4},\overline{\bf 5}\\})\\\
t_{3}&\overline{\bf
3}\to(\\{t_{b},t^{\prime}_{2},t_{g},t^{\prime}_{8}\\},\\{\overline{\bf
5}\\})&\\\ t_{8}&\overline{\bf
8}\to(\\{t_{b},t^{\prime}_{2}\\}\\{\overline{\bf 5},\overline{\bf
10}\\})&\\\\[10.0pt] \lx@intercol\it where\hfil\lx@intercol\\\
\lx@intercol\hfil\hfil\lx@intercol&t_{b}:2\to(\emptyset,\\{4\\})\\\
\lx@intercol\hfil\hfil\lx@intercol&t^{\prime}_{2}:\overline{\bf
2}\to(\emptyset,\\{\overline{\bf 4}\\})\\\
\lx@intercol\hfil\hfil\lx@intercol&t_{g}:8\to(\emptyset,\\{10\\})\\\
\lx@intercol\hfil\hfil\lx@intercol&t^{\prime}_{8}:\overline{\bf
8}\to(\emptyset,\\{\overline{\bf 10}\\})\end{array}\end{array}$
Figure 10. Encoding of branching cells (running example)

Consider the net $N$ and its s-cells in Fig. 7(a). Then, $\llbracket
N\rrbracket=(T,b)$ is defined such that $b$ is the initial marking of $N$,
i.e., $b=\\{1,2,7\\}$, and $T$ has the transitions shown in Fig. 10.

First consider the s-cell $\mathbb{C}_{1}$. $T_{\rm pos}$ contains one
transition for each transaction in $\mathbb{C}_{1}$, namely $t_{a}$ (for
$\theta_{a}:\mathbb{C}_{1}$) and $t_{d}$ (for $\theta_{d}:\mathbb{C}_{1}$).
Both $t_{a}$ and $t_{d}$ have ${}^{\circ}{\mathbb{C}_{1}}=\\{1\\}$ as preset.
By definition of $T_{\rm pos}$, both transitions have empty sets of
transitions in their postsets. Additionally, $t_{a}^{\bullet}$ produces tokens
in $\theta_{a}^{\circ}=\\{3\\}$ (positive) and
$\overline{\mathbb{C}^{\circ}_{1}\setminus\theta_{a}^{\circ}}=\overline{\\{3,6\\}\setminus\\{3\\}}=\\{\overline{\bf
6}\\}$ (negative), while $t_{d}^{\bullet}$ produces tokens in
$\theta_{d}^{\circ}=\\{6\\}$ and
$\overline{\mathbb{C}^{\circ}_{1}\setminus\theta^{\circ}_{d}}=\\{\overline{\bf
3}\\}$. Finally, $t_{1}\in T_{\rm neg}$ propagates negative tokens for the
unique place in ${}^{\circ}{\mathbb{C}_{1}}=\\{1\\}$. Since
$N_{\mathbb{C}_{1}}\ominus 1$ is the empty net, $\llbracket
N_{\mathbb{C}_{1}}\ominus 1\rrbracket=(\emptyset,\emptyset)$. Hence, $t_{1}$
produces negative tokens for all maximal places of $\mathbb{C}_{1}$, i.e.,
$\\{\overline{\bf 3},\overline{\bf 6}\\}$. For the s-cell $\mathbb{C}_{2}$ we
analogously obtain the transitions $t_{e}$, $t_{f}$ and $t_{7}$.

The s-cell $\mathbb{C}_{3}$ has two transactions $\theta_{bg}$ and
$\theta_{c}$. Hence, $\llbracket N\rrbracket$ has two transitions
$t_{bg},t_{c}\in T_{\rm pos}$. Despite $\theta_{bg}$ mimics the firing of $b$
and $g$, which are disconnected from the place $3$, it is included in the
preset of $t_{bg}$ to postpone the firing of $t_{bg}$ until $\mathbb{C}_{1}$
is executed. Transitions $t_{2},t_{3},t_{8}\in T_{\rm neg}$ propagate the
negative information for the places in
${}^{\circ}{\mathbb{C}}_{3}=\\{2,3,8\\}$. The transition $t_{3}$ has
${}^{\bullet}{t_{3}}=\\{\overline{\bf 3}\\}$ as its preset and its postset is
obtained from $N_{\mathbb{C}_{3}}\ominus 3$, which has two (sub) s-cells
${\mathbb{C}_{b}}$ and ${\mathbb{C}_{g}}$ (see Fig. 7(d)). The transitions
$t_{b}$ and $t^{\prime}_{2}$ arise from ${\mathbb{C}_{b}}$, and $t_{g}$ and
$t^{\prime}_{8}$ from ${\mathbb{C}_{g}}$. Hence,
${t_{3}^{\bullet}}=(\\{t_{b},t^{\prime}_{2},t_{g},t^{\prime}_{8}\\},\\{\overline{\bf
5}\\})$ because $\llbracket N_{\mathbb{C}_{3}}\ominus
3\rrbracket=(\\{t_{b},t^{\prime}_{2},t_{g},t^{\prime}_{8}\\},\emptyset)$ and
$\overline{\mathbb{C}_{3}^{\circ}\setminus(N_{\mathbb{C}_{3}}\ominus
3)^{\circ}}=\\{\overline{\bf 5}\\}$. Similarly, we derive $t_{2}$ from
$N_{\mathbb{C}_{3}}\ominus 2$ and $t_{8}$ from $N_{\mathbb{C}_{3}}\ominus 8$.

We now highlight some features of the encoded net. First, the set of top
transitions is free-choice: positive and negative transitions have disjoint
presets and the presets of any two positive transitions either coincide (if
they arise from the same s-cell) or are disjoint. Recursively, this property
holds at any level of nesting. Hence, the only source of potential confusion
is due to the combination of top transitions and those activated dynamically,
e.g., $t_{b}$ and either $t_{bg}$ or $t_{c}$. However, $t_{b}$ is activated
only when either $\overline{\bf 3}$ or $\overline{\bf 8}$ are marked, while
${}^{\bullet}{t_{bg}}={}^{\bullet}{t_{c}}=\\{2,3,8\\}$. Then, confusion is
avoided if $p$ and $\overline{\bf p}$ can never be marked in the same
execution (Lemma 3.2).

$\textstyle{\bullet}$$\textstyle{\scriptstyle{1}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{7}}$$\textstyle{t_{d}}$$\textstyle{t_{a}}$$\textstyle{t_{e}}$$\textstyle{t_{f}}$
$\textstyle{\scriptstyle{6}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 3}}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 6}}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 9}}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 8}}}$
$\textstyle{\scriptstyle{9}}$$\textstyle{\color[rgb]{120,120,120}t_{3}}$$\textstyle{\color[rgb]{120,120,120}t_{8}}$
$\textstyle{\scriptstyle{8}}$
$\textstyle{\scriptstyle{3}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{2}}$$\textstyle{\color[rgb]{120,120,120}t^{\prime}_{8}}$$\textstyle{t_{g}}$$\textstyle{t_{bg}}$$\textstyle{t_{c}}$$\textstyle{t_{b}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 5}}}$
$\textstyle{\scriptstyle{10}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 4}}}$
$\textstyle{\scriptstyle{5}}$ $\textstyle{\scriptstyle{4}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 10}}}$
Figure 11. Dynamic net $\llbracket N\rrbracket$ (running example)

The net $\llbracket N\rrbracket$ is shown in Fig. 11, where the places
$\\{\overline{\bf 1},\overline{\bf 2},\overline{\bf 7}\\}$ and the transitions
$\\{t_{1},t_{7},t_{2},t^{\prime}_{2}\\}$ are omitted because superseded by the
initial marking $\\{1,2,7\\}$.

We remark that the same dynamic transition can be released by the firing of
different transitions (e.g., $t_{b}$ by $t_{3}$ and $t_{8}$) and possibly
several times in the same computation. Similarly, the same negative
information can be generated multiple times. However this duplication has no
effect, since we handle persistent tokens. For instance, the firing sequence
$t_{d};t_{f};t_{3};t_{8}$ releases two copies of $t_{b}$ and marks
$\overline{\bf 5}$ twice. This is inessential for reachability, but has
interesting consequences w.r.t. causal dependencies (see Section 5).

We now show that the encoding generates confusion-free nets. We start by
stating a useful property of the encoding that ensures that an execution
cannot generate tokens in both $p$ and $\overline{\bf p}$.

######  Lemma  (Negative and positive tokens are in exclusion).

If $\llbracket N\rrbracket\rightarrow^{*}(T,b)$ and $\overline{\bf p}\in b$
then $(T,b)\rightarrow^{*}(T^{\prime},b^{\prime})$ implies that $p\not\in
b^{\prime}$.

We now observe from Def. 3.2 that for any transition $t\in\llbracket
N\rrbracket\in\textsc{dn}(P\cup\overline{\bf P})$ it holds that either
${}^{\bullet}{t}\subseteq P$ or ${}^{\bullet}{t}\subseteq\overline{\bf P}$.
The next result says that whenever there exist two transitions $t$ and
$t^{\prime}$ that have different but overlapping presets, at least one of them
is disabled by the presence of a negative token in the marking $b$.

######  Lemma  (Nested rules do not collide).

Let $\llbracket N\rrbracket\in\textsc{dn}(P\cup\overline{\bf P})$. If
$\llbracket N\rrbracket\rightarrow^{*}(T,b)$ then for all $t,t^{\prime}\in T$
s.t. ${}^{\bullet}{t}\neq{}^{\bullet}{t^{\prime}}$ and
${}^{\bullet}{t}\cap{}^{\bullet}{t^{\prime}}\cap P\neq\emptyset$ it holds that
there is $p\in P\cap({}^{\bullet}{t}\cup{}^{\bullet}{t^{\prime}})$ such that
$\overline{\bf p}\in b$.

The main result states that $\llbracket\cdot\rrbracket$ generates confusion-
free nets.

######  Theorem .

Let $\llbracket N\rrbracket\in\textsc{dn}(P\cup\overline{\bf P})$. If
$\llbracket N\rrbracket\rightarrow^{*}(T,b)\xlongrightarrow{t}$ and
$(T,b)\xlongrightarrow{t^{\prime}}$ then either
${}^{\bullet}{t}={}^{\bullet}{t^{\prime}}$ or
${}^{\bullet}{t}\cap{}^{\bullet}{t^{\prime}}=\emptyset$.

######  Corollary .

Any net $\llbracket N\rrbracket\in\textsc{dn}(P\cup\overline{\bf P})$ is
confusion-free.

Finally, we can combine the encoding $\llbracket\cdot\rrbracket$ with
$\llparenthesis\cdot\rrparenthesis$ (from Section 2.5) to obtain a (flat)
$1$-$\infty$-safe, confusion-free, p-net $\llparenthesis\llbracket
N\rrbracket\rrparenthesis$, that we call the _uniformed net_ of $N$. By
Proposition 2.5 we get that the uniformed net $\llparenthesis\llbracket
N\rrbracket\rrparenthesis$ is also confusion-free by construction.

######  Corollary .

Any p-net $\llparenthesis\llbracket N\rrbracket\rrparenthesis$ is confusion-
free.

##  4\. Static vs Dynamic cell decomposition

As mentioned in the Introduction, Abbes and Benveniste proposed a way to
remove confusion by dynamically decomposing prime event structures. In
Sections 4.1 and 4.2 we recall the basics of the AB’s approach as introduced
in [1, 2, 3]. Then, we show that there is an operational correspondence
between AB decomposition and s-cells introduced in Section 3.1.

###  4.1. Prime Event Structures

A _prime event structure_ (also _PES_) [22, 30] is a triple
$\mathcal{E}=(E,\preceq,\\#)$ where: $E$ is the set of _events_ ; the
_causality relation_ $\preceq$ is a partial order on events; the _conflict
relation_ $\\#$ is a symmetric, irreflexive relation on events such that
conflicts are inherited by causality, i.e., $\forall e_{1},e_{2},e_{3}\in
E.~{}e_{1}\\#e_{2}\preceq e_{3}\Rightarrow e_{1}\\#e_{3}$.

The PES $\mathcal{E}_{N}$ associated with a net $N$ can be formalised using
category theory as a chain of universal constructions, called coreflections.
Hence, for each PES $\mathcal{E}$, there is a standard, unique (up to
isomorphism) nondeterministic occurrence net $N_{\mathcal{E}}$ that yields
$\mathcal{E}$ and thus we can freely move from one setting to the other.

Consider the nets in Figs. 1(a) and 3(a). The corresponding PESs are shown
below each net. Events are in bijective correspondence with the transitions of
the nets. Strict causality is depicted by arrows and immediate conflict by
curly lines.

Given an event $e$, its _downward closure_ $\lfloor e\rfloor=\\{e^{\prime}\in
E\mid e^{\prime}\preceq e\\}$ is the set of causes of $e$. As usual, we assume
that $\lfloor e\rfloor$ is finite for any $e$. Given $B\subseteq E$, we say
that $B$ is _downward closed_ if $\forall e\in B.~{}\lfloor e\rfloor\subseteq
B$ and that $B$ is _conflict-free_ if $\forall e,e^{\prime}\in
B.~{}\neg(e\\#e^{\prime})$. We let the _immediate conflict_ relation $\\#_{0}$
be defined on events by letting $e\\#_{0}e^{\prime}$ iff $(\lfloor
e\rfloor\times\lfloor e^{\prime}\rfloor)\cap\\#=\\{(e,e^{\prime})\\}$, i.e.,
two events are in immediate conflict if they are in conflict but their causes
are compatible.

###  4.2. Abbes and Benveniste’s Branching Cells

In the following we assume that a (finite) PES $\mathcal{E}=(E,\preceq,\\#)$
is given. A _prefix_ $B\subseteq E$ is any downward-closed set of events
(possibly with conflicts). Any prefix $B$ induces an event structure
$\mathcal{E}_{B}=(B,\preceq_{B},\\#_{B})$ where $\preceq_{B}$ and $\\#_{B}$
are the restrictions of $\preceq$ and $\\#$ to the events in $B$. A _stopping
prefix_ is a prefix $B$ that is closed under immediate conflicts, i.e.,
$\forall e\in B,e^{\prime}\in E.~{}e\\#_{0}e^{\prime}\Rightarrow e^{\prime}\in
B$. Intuitively, a stopping prefix is a prefix whose (immediate) choices are
all available. It is _initial_ if the only stopping prefix strictly included
in $B$ is $\emptyset$. We assume that any $e\in E$ is contained in a finite
stopping prefix.

A _configuration_ $v\subseteq\mathcal{E}$ is any set of events that is
downward closed and conflict-free. Intuitively, a configuration represents
(the state reached after executing) a concurrent but deterministic computation
of $\mathcal{E}$. Configurations are ordered by inclusion and we denote by
$\mathcal{V}_{\mathcal{E}}$ the poset of finite configurations of
$\mathcal{E}$ and by $\Omega_{\mathcal{E}}$ the poset of maximal
configurations of $\mathcal{E}$.

The _future_ of a configuration $v$, written $E^{v}$, is the set of events
that can be executed after $v$, i.e., $E^{v}=\\{e\in E\setminus v\ \mid\
\forall e^{\prime}\in v.\neg(e\\#e^{\prime})\\}$. We write $\mathcal{E}^{v}$
for the event structure induced by $E^{v}$. We assume that any finite
configuration enables only finitely many events, i.e., the set of minimal
elements in $E^{v}$ w.r.t. $\preceq$ is finite for any
$v\in\mathcal{V}_{\mathcal{E}}$.

A configuration $v$ is _stopped_ if there is a stopping prefix $B$ with
$v\in\Omega_{B}$. and $v$ is _recursively stopped_ if there is a finite
sequence of configurations $\emptyset=v_{0}\subset\ldots\subset v_{n}=v$ such
that for any $i\in[0,n)$ the set $v_{i+1}\setminus v_{i}$ is a finite stopped
configuration of $\mathcal{E}^{v_{i}}$ for $v_{i}$ in $\mathcal{E}$.

A _branching cell_ is any initial stopping prefix of the future
$\mathcal{E}^{v}$ of a finite recursively stopped configuration $v$.
Intuitively, a branching cell is a minimal subset of events closed under
immediate conflict. We remark that branching cells are determined by
considering the whole (future of the) event structure $\mathcal{E}$ and they
are recursively computed as $\mathcal{E}$ is executed. Remarkably, every
maximal configuration has a branching cell decomposition.

######  Example .

$\textstyle{d\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{a\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{e\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{f}$$\textstyle{b\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{c\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{g}$
(a) $\mathcal{E}_{N}$

$\textstyle{e\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{f}$$\textstyle{b\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{c\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{g}$
(b) $\mathcal{E}_{N}^{\\{a\\}}$

$\textstyle{b\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{c\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{g}$
(c) $\mathcal{E}_{N}^{\\{a,e\\}}$

$\textstyle{e\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{f}$$\textstyle{b}$$\textstyle{g}$
(d) $\mathcal{E}_{N}^{\\{d\\}}$

Figure 12. AB’s branching cell decomposition (running example)

Consider the PES $\mathcal{E}_{N}$ in Fig. 3(a) and its maximal configuration
$v=\\{a,e,b,g\\}$. We show that $v$ is recursively stopped by exhibiting a
branching cell decomposition. The initial stopping prefixes of
$\mathcal{E}_{N}=\mathcal{E}_{N}^{\emptyset}$ are shown in Fig. 12(a). There
are two possibilities for choosing $v_{1}\subseteq v$ and $v_{1}$ recursively
stopped: either $v_{1}=\\{a\\}$ or $v_{1}=\\{e\\}$. When $v_{1}=\\{a\\}$, the
choices for $v_{2}$ are determined by the stopping prefixes of
$\mathcal{E}_{N}^{\\{a\\}}$ (see Fig. 12(b)) and the only possibility is
$v_{2}=\\{a,e\\}$. From $\mathcal{E}_{N}^{\\{a,e\\}}$ in Fig. 12(c), we take
$v_{3}=v$. Note that $\\{a,e,b\\}$ is not recursively stopped because
$\\{b\\}$ is not maximal in the stopping prefix of
$\mathcal{E}_{N}^{\\{a,e\\}}$ (see Fig. 12(c)). Finally, note that the
branching cells $\mathcal{E}_{N}^{\\{a\\}}$ (Fig. 12(b)) and
$\mathcal{E}_{N}^{\\{d\\}}$ (Fig. 12(d)) correspond to different choices in
$\mathcal{E}_{N}^{\emptyset}$ and thus have different stopping prefixes.

###  4.3. Relating s-cells and AB’s decomposition

The recursively stopped configurations of a net $N$ characterise all the
allowed executions of $N$. Hence, we formally link the recursively stopped
configurations of $\mathcal{E}_{N}$ with the computations of the uniformed net
$\llparenthesis\llbracket N\rrbracket\rrparenthesis$. For technical
convenience, we first show that the recursively stopped configurations of
$\mathcal{E}_{N}$ are in one-to-one correspondence with the computations of
the dynamic net $\llbracket N\rrbracket$. Then, the desired correspondence is
obtained by using Proposition 2.5 to relate the computations of a dynamic net
and its associated p-net.

We rely on the auxiliary map $\lVert-\rVert$ that links transitions in
$\llbracket N\rrbracket$ with events in $\mathcal{E}_{N}$. Specifically,
$\lVert-\rVert$ associates each transition $t$ of $\llbracket N\rrbracket$
with the set $\lVert t\rVert$ of transitions of $N$ (also events in
$\mathcal{E}_{N}$) that are encoded by $t$. Formally,

$\lVert t\rVert=\begin{cases}{\it ev}(\theta)&\mbox{if
}t=t_{\theta,\mathbb{C}}\in T_{\rm pos}\\\ \emptyset&\mbox{if }t\in T_{\rm
neg}\end{cases}$

where ${\it ev}(\theta)$ is the set of transitions in $\theta$.

######  Example .

Consider the net $N$ in Fig. 7(a) which is encoded as the dynamic p-net in
Fig. 10. The auxiliary mapping $\lVert\\_\rVert$ is as follows

$\begin{array}[]{l@{\qquad}l@{\qquad}l@{\qquad}l}\lVert
t_{a}\rVert=\\{a\\}&\lVert t_{d}\rVert=\\{d\\}&\lVert
t_{e}\rVert=\\{e\\}&\lVert t_{f}\rVert=\\{f\\}\\\ \lVert
t_{bg}\rVert=\\{b,g\\}&\lVert t_{c}\rVert=\\{c\\}&\lVert
t_{b}\rVert=\\{b\\}&\lVert t_{g}\rVert=\\{g\\}\\\ \lx@intercol\lVert
t\rVert=\emptyset\ \mbox{if}\
t\in\\{t_{1},t_{7},t_{2},t_{3},t_{8},t^{\prime}_{2},t^{\prime}_{8}\\}\hfil\lx@intercol\end{array}$

A transition $t_{\theta,\mathbb{C}}$ of $\llparenthesis N\rrparenthesis$
associated with a transaction $\theta:\mathbb{C}$ of $N$ is mapped to the
transitions of $\theta$. For instance, $t_{a}$ is mapped to $\\{a\\}$, which
is the only transition in $\theta_{a}$. Differently, transitions that
propagate negative information, i.e.,
$t\in\\{t_{1},t_{7},t_{2},t_{3},t_{8},t^{\prime}_{2},t^{\prime}_{8}\\}$, are
mapped to $\emptyset$ because they do not encode any transition of $N$.

In what follows we write $M\xLongrightarrow{}M^{\prime}$ for a possibly empty
firing sequence $M\xlongrightarrow{t_{1}\cdots t_{n}}M^{\prime}$ such that
$\lVert t_{i}\rVert=\emptyset$ for all $i\in[1,n]$. If $\lVert
t\rVert\neq\emptyset$, we write $M\xLongrightarrow{t}M^{\prime}$ if
$M\xLongrightarrow{}M_{0}\xLongrightarrow{t}M_{1}\xLongrightarrow{}M^{\prime}$
for some $M_{0},M_{1}$. Moreover, we write $M\xLongrightarrow{t_{1}\cdots
t_{n}}$ if there exist $M_{1},...,M_{n}$ such that
$M\xLongrightarrow{t_{1}}M_{1}\xLongrightarrow{t_{2}}\cdots\xLongrightarrow{t_{n}}M_{n}$.

The following result states that the computations of any dynamic p-net
produced by $\llbracket\\_\rrbracket$ are in one-to-one correspondence with
the recursively stopped configurations of Abbes and Benveniste.

######  Lemma .

Let $N$ be an occurrence net.

  1. (1)

If $\llbracket N\rrbracket\xLongrightarrow{t_{1}\cdots t_{n}}$, then
$v=\bigcup_{1\leq i\leq n}\lVert t_{i}\rVert$ is recursively stopped in
$\mathcal{E}_{N}$ and $(\lVert t_{i}\rVert)_{1\leq i\leq n}$ is a valid
decomposition of $v$.

  2. (2)

If $v$ is recursively stopped in $\mathcal{E}_{N}$, then for any valid
decomposition $(v_{i})_{1\leq i\leq n}$ there exists $\llbracket
N\rrbracket\xLongrightarrow{t_{1}\cdots t_{n}}$ such that $\lVert
t_{i}\rVert=v_{i}$.

######  Example .

Consider the branching cell decomposition for
$v=\\{a,e,b,g\\}\in\mathcal{E}_{v}$ discussed in Ex. 4.2. Then, the net
$\llbracket N\rrbracket$ in Ex. 3.2 can mimic that decomposition with the
following computation

$\begin{array}[]{l}(T,\\{1,2,7\\})\xlongrightarrow{t_{a}}(T,\\{2,3,7,\overline{\bf
6}\\})\xlongrightarrow{t_{e}}(T,\\{2,3,8,\overline{\bf 6},\overline{\bf
9}\\})\xlongrightarrow{t_{bg}}(T,\\{4,10,\overline{\bf 5},\overline{\bf
6},\overline{\bf 9}\\})\end{array}$

with $v_{1}=\lVert t_{a}\rVert=\\{a\\}$, $v_{2}=\lVert t_{e}\rVert=\\{e\\}$,
and $v_{3}=\lVert t_{bg}\rVert=\\{b,g\\}$.

From Lemma 4.3 and Proposition 2.5 we obtain the next result.

######  Theorem  (Correspondence).

Let $N$ be an occurrence net.

  1. (1)

If $\llparenthesis\llbracket
N\rrbracket\rrparenthesis\xLongrightarrow{t_{1}\cdots t_{n}}$, then
$v=\bigcup_{1\leq i\leq n}\lVert t_{i}\rVert$ is recursively stopped in
$\mathcal{E}_{N}$ and $(\lVert t_{i}\rVert)_{1\leq i\leq n}$ is a valid
decomposition of $v$.

  2. (2)

If $v$ is recursively stopped in $\mathcal{E}_{N}$, then for any valid
decomposition $(v_{i})_{1\leq i\leq n}$ there exists $\llparenthesis\llbracket
N\rrbracket\rrparenthesis\xLongrightarrow{t_{1}\cdots t_{n}}$ such that
$\lVert t_{i}\rVert=v_{i}$.

By (1) above, any computation of $\llparenthesis\llbracket
N\rrbracket\rrparenthesis$ corresponds to a (recursively stopped)
configuration of $\mathcal{E}_{N}$, i.e., a process of $N$. By (2), every
execution of $N$ that can be decomposed in terms of AB’s branching cells is
preserved by $\llparenthesis\llbracket N\rrbracket\rrparenthesis$, because any
recursively stopped configuration of $\mathcal{E}_{N}$ is mimicked by
$\llparenthesis\llbracket N\rrbracket\rrparenthesis$.

##  5\. Concurrency of the Uniformed Net

In this section we study the amount of concurrency still present in the
uniformed net $\llparenthesis\llbracket N\rrbracket\rrparenthesis$. Here, we
extend the notion of a process to the case of $1$-$\infty$-safe p-nets and we
show that all the _legal_ firing sequences of a process of the uniformed net
$\llparenthesis\llbracket N\rrbracket\rrparenthesis$ are executable.

The notion of deterministic occurrence net is extended to p-nets by slightly
changing the definitions of conflict and causal dependency: (i) two
transitions are not in conflict when all shared places are persistent, (ii) a
persistent place can have more than one immediate cause in its preset, which
introduces OR-dependencies.

######  Definition  (Persistent process).

An occurrence p-net $O=(P\cup\mathbf{P},T,F)$ is an acyclic p-net such that
$|p^{\bullet}|\leq 1$ and $|{}^{\bullet}{p}|\leq 1$ for any $p\in P$ (but not
necessarily for those in $\mathbf{P}$).

A persistent process for $N$ is an occurrence p-net $O$ together with a net
morphism $\pi:O\rightarrow N$ that preserves presets and postsets and the
distinction between regular and persistent places. Without loss of generality,
when $N$ is acyclic, we assume that $O$ is a subnet of $N$ (with the same
initial marking) and $\pi$ is the identity.

In an ordinary occurrence net, the causes of an item $x$ are all its
predecessors. In p-nets, the alternative sets of causes of an item $x$ are
given by a formula $\Phi(x)$ of the propositional calculus without negation,
where the basic propositions are the transitions of the occurrence net. If we
represent such a formula as a sum of products, it corresponds to a set of
collections, i.e. a set of sets of transitions. Different collections
correspond to alternative causal dependencies, while transitions within a
collection are all the causes of that alternative and $true$ represents the
empty collection. Such a formula $\Phi(x)$ represents a monotone boolean
function, which expresses, as a function of the occurrences of past
transitions, if $x$ has enough causes. It is known that such formulas, based
on positive literals only, have a unique DNF (sum of products) form, given by
the set of prime implicants. In fact, every prime implicant is also essential
[29]. We define $\Phi(x)$ by well-founded recursion:

$\Phi(x)=\left\\{\begin{array}[]{ll}\mathit{true}&\mbox{if $x\in
P\cup\mathbf{P}\wedge{}^{\bullet}{x}=\emptyset$}\\\
\bigvee_{t\in{}^{\bullet}{x}}(t\wedge\Phi(t))&\mbox{if $x\in
P\cup\mathbf{P}\wedge{}^{\bullet}{x}\neq\emptyset$}\\\
\bigwedge_{s\in{}^{\bullet}{x}}\Phi(s)&\mbox{if $x\in T$}\end{array}\right.$

Ordinary deterministic processes satisfy complete concurrency: each process
determines a partial ordering of its transitions, such that the executable
sequences of transitions are exactly the linearizations of the partial order.
More formally, after executing any firing sequence $\sigma$ of the process, a
transition $t$ is enabled if and only if all its predecessors in the partial
order (namely its causes) already appear in $\sigma$. In the present setting a
similar property holds.

######  Definition  (Legal firing sequence).

A sequence of transitions $t_{1};\cdots;t_{n}$ of a persistent process is
_legal_ if for all $k\in[1,n]$ we have that $\bigwedge_{i=1}^{k-1}t_{i}$
implies $\Phi(t_{k})$.

It is immediate to notice that if the set of persistent places is empty
($\mathbf{P}=\emptyset$) then the notion of persistent process is the ordinary
one, $\Phi(x)$ is just the conjunction of the causes of $x$ and a sequence is
legal iff it is a linearization of the process.

######  Theorem  (Complete Concurrency).

Let $\sigma=t_{1};\cdots;t_{n}$ with $n\geq 0$ be a, possibly empty, firing
sequence of a persistent process, and $t$ a transition not in $\sigma$. The
following conditions are all equivalent: (i) $t$ is enabled after $\sigma$;
(ii) there is a collection of causes of $t$ which appears in $\sigma$; (iii)
$\bigwedge_{i=1}^{n}t_{i}$ implies $\Phi(t)$.

######  Corollary .

Given a persistent process, a sequence is legal iff it is a firing sequence.

$\textstyle{\bullet}$$\textstyle{\scriptstyle{1}}$$\textstyle{\color[rgb]{120,120,120}\bullet}$
$\textstyle{t_{a}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf
6}}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{2}}$
$\textstyle{\scriptstyle{3}}$$\textstyle{\color[rgb]{120,120,120}\bullet}$$\textstyle{t^{\prime}_{b}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 5}}}$
$\textstyle{\scriptstyle{4}}$ (a) $a\preceq b$

$\textstyle{\bullet}$$\textstyle{\scriptstyle{1}}$$\textstyle{\color[rgb]{120,120,120}\bullet}$
$\textstyle{t_{a}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf
6}}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{2}}$
$\textstyle{\scriptstyle{3}}$$\textstyle{\color[rgb]{120,120,120}\bullet}$
$\textstyle{t_{c}}$ $\textstyle{\scriptstyle{5}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 4}}}$ (b)
$a\preceq c$

$\textstyle{\color[rgb]{120,120,120}\bullet}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{1}}$$\textstyle{t_{d}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 3}}}$
$\textstyle{\scriptstyle{6}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{2}}$
$\textstyle{\scriptstyle{\color[rgb]{120,120,120}p_{b}}}$$\textstyle{t_{b}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 5}}}$
$\textstyle{\scriptstyle{4}}$ (c) $d\preceq b$

Figure 13. Processes for the net in Fig. 9(c)

######  Example .

Figs. 13(a)–13(c) show the maximal processes of the net in Fig. 9(c). It is
evident that all executions are serialized.

######  Example .

$\textstyle{\color[rgb]{120,120,120}\bullet}$$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf
p_{t_{d}}}}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{1}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{7}}$$\textstyle{\color[rgb]{120,120,120}\bullet}$$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf
p_{t_{f}}}}}$$\textstyle{t_{d}}$$\textstyle{t_{f}}$
$\textstyle{\scriptstyle{6}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 3}}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 8}}}$
$\textstyle{\scriptstyle{9}}$$\textstyle{\color[rgb]{120,120,120}t_{3}}$$\textstyle{\color[rgb]{120,120,120}t_{8}}$
$\textstyle{\color[rgb]{120,120,120}{\scriptstyle{\bf p_{t_{g}}\
}}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{2}}$
$\textstyle{\color[rgb]{120,120,120}{\scriptstyle{\bf p_{t_{b}}}}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf
p_{t^{\prime}_{8}}}}}$$\textstyle{t_{b}}$$\textstyle{\color[rgb]{120,120,120}t^{\prime}_{8}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 5}}}$
$\textstyle{\scriptstyle{4}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 10}}}$
Figure 14. A process for $\llparenthesis\llbracket N\rrbracket\rrparenthesis$
(running example)

Fig. 14 shows a process for the net $\llparenthesis\llbracket
N\rrbracket\rrparenthesis$ of our running example (see $N$ in Fig. 3(a) and
$\llbracket N\rrbracket$ in Fig. 11). The process accounts for the firing of
the transitions $d$, $f$, $b$ in $N$. Despite they look as concurrent events
in $N$, the persistent place $\bf p_{t_{b}}$ introduces some causal
dependencies. In fact, we have: $\Phi(t_{d})=\Phi(t_{f})=\mathit{true}$,
$\Phi(t_{3})=t_{d}$, $\Phi(t_{8})=t_{f}$ and $\Phi(t_{b})=(t_{3}\wedge
t_{d})\vee(t_{8}\wedge t_{f})$, thus $t_{b}$ can be fired only after either
$t_{d}$ or $t_{f}$ (or both). The other maximal processes are reported in
Appendix E.

$\textstyle{\bullet}$$\textstyle{\scriptstyle{1}}$$\textstyle{\color[rgb]{120,120,120}\bullet}$$\textstyle{\color[rgb]{120,120,120}\bullet}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{7}}$$\textstyle{t_{a}}$$\textstyle{t_{e}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 6}}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 9}}}$
$\textstyle{\scriptstyle{8}}$$\textstyle{\color[rgb]{120,120,120}\bullet}$
$\textstyle{\scriptstyle{3}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{2}}$$\textstyle{t_{bg}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 5}}}$
$\textstyle{\scriptstyle{10}}$ $\textstyle{\scriptstyle{4}}$ (a)

$\textstyle{\bullet}$$\textstyle{\scriptstyle{1}}$$\textstyle{\color[rgb]{120,120,120}\bullet}$$\textstyle{\color[rgb]{120,120,120}\bullet}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{7}}$$\textstyle{t_{a}}$$\textstyle{t_{e}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 6}}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 9}}}$
$\textstyle{\scriptstyle{8}}$$\textstyle{\color[rgb]{120,120,120}\bullet}$
$\textstyle{\scriptstyle{3}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{2}}$$\textstyle{t_{bg}}$
$\textstyle{\scriptstyle{8_{t_{bg}}}}$
$\textstyle{\scriptstyle{2_{t_{bg}}}}$$\textstyle{g_{t_{bg}}}$$\textstyle{b_{t_{bg}}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 5}}}$
$\textstyle{\scriptstyle{10}}$ $\textstyle{\scriptstyle{4}}$ (b)

Figure 15. Expanding transactions I

Still referring to the net $\llparenthesis\llbracket
N\rrbracket\rrparenthesis$ of our running example, a more interesting case to
consider is the process in Fig. 15(a) whose transition $t_{bg}$ stands for the
transaction where $b$ and $g$ are executed simultaneously. One may argue that
having $t_{bg}$ as an atomic action can reduce the overall concurrency of the
system. However, $t_{bg}$ can be expanded with (a fresh copy of) its
underlying process as shown in Fig. 15(b). We use $t_{bg}$ as a subscript for
the new nodes of the process to guarantee they are fresh. The preset of the
transition $t_{bg}$ is left unchanged. Its postset takes care of the
propagation of negative information and of enabling the initial places of the
underlying process. The final places of the underlying process are the
(positive) places in the postset of the original transition $t_{bg}$. This
transformation has the side effect to separate the choice of the transaction
from its execution, but it increases the amount of concurrency, as
$b_{t_{bg}}$ and $g_{t_{bg}}$ can now be executed in any order. While it might
be possible in some cases to avoid the additional choice event, the general
construction would look cumbersome.

The improvement is even more evident if we consider the net $N$ in Fig. 16(a).
There are two s-cells $\mathbb{C}_{1}$ and $\mathbb{C}_{2}$: the former has
two transactions $\theta_{a}=\\{a\\}$ and $\theta_{bc}=\\{b,c\\}$, the latter
is trivial as it has only one transaction $\theta_{d}=\\{d\\}$. One process of
$\llparenthesis\llbracket N\rrbracket\rrparenthesis$ is in Fig. 16(b), where
$t_{bc}$ and $t_{d}$ are executed concurrently. However it does not take into
account the fact that the execution of $b$ and $c$ can be interleaved with
that of $d$. If we expand $t_{bc}$ as discussed in the previous example, we
get the process in Fig. 16(c), where $d$ can be executed after $b$ and before
$c$.

$\textstyle{\bullet}$$\textstyle{\scriptstyle{1}}$$\textstyle{\mathbb{C}_{1}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{2}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{3}}$$\textstyle{\mathbb{C}_{2}}$$\textstyle{a}$$\textstyle{b}$$\textstyle{d}$
$\textstyle{\scriptstyle{4}}$ $\textstyle{\scriptstyle{5}}$$\textstyle{c}$
$\textstyle{\scriptstyle{6}}$ $\textstyle{\scriptstyle{7}}$ (a)

$\textstyle{\bullet}$$\textstyle{\scriptstyle{1}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{2}}$$\textstyle{\color[rgb]{120,120,120}\bullet}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{3}}$$\textstyle{\color[rgb]{120,120,120}\bullet}$$\textstyle{t_{bc}}$$\textstyle{t_{d}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 6}}}$
$\textstyle{\scriptstyle{7}}$ $\textstyle{\scriptstyle{5}}$ (b)

$\textstyle{\bullet}$$\textstyle{\scriptstyle{1}}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{2}}$$\textstyle{\color[rgb]{120,120,120}\bullet}$$\textstyle{\bullet}$$\textstyle{\scriptstyle{3}}$$\textstyle{\color[rgb]{120,120,120}\bullet}$$\textstyle{t_{bc}}$$\textstyle{t_{d}}$
$\textstyle{\scriptstyle{1_{t_{bc}}}}$ $\textstyle{\scriptstyle{2_{t_{bc}}}}$
$\textstyle{\scriptstyle{5}}$$\textstyle{b_{t_{bc}}}$
$\textstyle{\scriptstyle{4_{t_{bc}}}}$$\textstyle{c_{t_{bc}}}$
$\textstyle{\color[rgb]{120,120,120}\overline{\scriptstyle{\bf 6}}}$
$\textstyle{\scriptstyle{7}}$ (c)

Figure 16. Expanding transactions II

Formally, given a process $\theta$ and a transition name $t$, let $\theta_{t}$
be the process where any non final place/transition $n$ is renamed to $n_{t}$
and any final place is left unchanged. We say a positive transition
$t_{\theta,\mathbb{C}}$ of $\llparenthesis\llbracket
N\rrbracket\rrparenthesis$ is _non-atomic_ if the process $\theta$ involves
more than one transition. Given a net $N$ and its uniformed net
$\llparenthesis\llbracket N\rrbracket\rrparenthesis$ we let
$\llparenthesis{\llbracket N\rrbracket}\rrparenthesis_{\mathit{conc}}$ denote
the persistent net obtained from $\llparenthesis\llbracket
N\rrbracket\rrparenthesis$ by removing each non-atomic transition
$t_{\theta,\mathbb{C}}$ and by adding, for each such transition, the places
and transitions in $\theta_{t_{\theta,\mathbb{C}}}$ together with a transition
$t^{\prime}_{\theta,\mathbb{C}}$ such that
${}^{\bullet}{t}^{\prime}_{\theta,\mathbb{C}}={}^{\bullet}{t}_{\theta,\mathbb{C}}$
but whose postset consists of ${}^{\circ}{\theta}_{t_{\theta,\mathbb{C}}}$
together with the negative places in the postset of $t_{\theta,\mathbb{C}}$.

##  6\. Probabilistic Nets

We can now outline our methodology to assign probabilities to the concurrent
runs of a Petri net, also in the presence of confusion. Given a net $N$, we
apply s-cell decomposition from Section 3.1, and then we assign probability
distributions to the transactions available in each cell $\mathbb{C}$ (and
recursively to the s-cell decomposition of $N_{\mathbb{C}}$). Let
$\mathcal{P}_{\mathbb{C}}:\\{\theta\mid\theta:\mathbb{C}\\}\to[0,1]$ denote
the probability distribution function of the s-cell $\mathbb{C}$ (such that
$\sum_{\theta:\mathbb{C}}\mathcal{P}_{\mathbb{C}}(\theta)=1$). Such
probability distributions are defined locally and transferred automatically to
the transitions in $T_{\rm pos}$ of the dynamic p-net $\llbracket N\rrbracket$
defined in Section 3, in such a way that
$\mathcal{P}(t_{\theta,\mathbb{C}})=\mathcal{P}_{\mathbb{C}}(\theta)$. Each
negative transitions in $T_{\rm neg}$ has probability 1 because no choice is
associated with it. Since the uniformed net $\llparenthesis\llbracket
N\rrbracket\rrparenthesis$ has the same transitions of $\llbracket
N\rrbracket$, the probability distribution can be carried over
$\llparenthesis\llbracket N\rrbracket\rrparenthesis$ (thanks to Proposition
2.5).

#### AB’s probability distribution

Building on the bijective correspondence in Theorem 4.3, the distribution
$\mathcal{P}_{\mathbb{C}}$ can be chosen in such a way that it is consistent
with the one attached to the transitions of Abbes and Benveniste’s branching
cells (if any).

#### Purely local distribution

Another simple way to define $\mathcal{P}_{\mathbb{C}}$ is by assigning
probability distributions to the arcs leaving the same place of the original
net, as if each place were able to decide autonomously which transition to
fire. Then, given a transaction $\theta:\mathbb{C}$, we can set
$\mathcal{Q}_{\mathbb{C}}(\theta)$ be the product of the probability
associated with the arcs of $N$ entering the transitions in $\theta$. Of
course, in general it can happen that
$\sum_{\theta:\mathbb{C}}\mathcal{Q}_{\mathbb{C}}(\theta)<1$, as not all
combinations are feasible. However, it is always possible to normalise the
quantities of feasible assignments by setting
$\mathcal{P}_{\mathbb{C}}(\theta)=\frac{\mathcal{Q}_{\mathbb{C}}(\theta)}{\sum_{\theta^{\prime}:\mathbb{C}}\mathcal{Q}_{\mathbb{C}}(\theta^{\prime})}$
for any transaction $\theta:\mathbb{C}$.

######  Example .

$\textstyle{\bullet}$$\scriptstyle{\frac{1}{3}}$$\scriptstyle{\frac{2}{3}}$$\textstyle{\scriptstyle{1}}$$\textstyle{\bullet}$$\scriptstyle{\frac{2}{3}}$$\scriptstyle{\frac{1}{3}}$$\textstyle{\scriptstyle{2}}$$\textstyle{a}$$\textstyle{b}$
$\textstyle{\scriptstyle{3}}$ $\textstyle{\scriptstyle{4}}$ Figure 17. A free-
choice net

Take the free-choice net in Fig. 17 and assume that decisions are local to
each place. Thus, place $1$ lends its token to $a$ with probability
$p_{1}=\frac{1}{3}$ and to $b$ with $q_{1}=\frac{2}{3}$. Similarly, place $2$
lends its token to $a$ with probability $p_{2}=\frac{1}{3}$ and to $b$ with
$q_{2}=\frac{2}{3}$. Then one can set $p_{a}=p_{1}\cdot p_{2}=\frac{1}{9}$ and
$p_{b}=q_{1}\cdot q_{2}=\frac{4}{9}$. However their sum is $\frac{5}{9}\neq
1$. This anomaly is due to the existence of deadlocked choices with nonzero
probabilities which disappear in the process semantics of nets. To some
extent, the probabilities assigned to $a$ and $b$ should be conditional w.r.t.
the fact that the local choices performed at places $1$ and $2$ are
compatible, i.e., all non compatible choices are disregarded. This means that
we need to normalize the values of $p_{a}$ and $p_{b}$ over their sum. Of
course, normalisation is possible only if there is at least one admissible
alternative. In this simple example we get $\mathcal{Q}(a)=\frac{1}{9}$,
$\mathcal{Q}(b)=\frac{4}{9}$,
$\mathcal{P}(a)=\frac{1}{9}/\frac{5}{9}=\frac{1}{5}$ and
$\mathcal{P}(b)=\frac{4}{9}/\frac{5}{9}=\frac{4}{5}$.

######  Example .

Suppose that in our running example we assign uniform distributions to all
arcs leaving a place. From simple calculation we have
$\mathcal{P}_{\mathbb{C}_{1}}(\theta_{a})=\mathcal{P}_{\mathbb{C}_{1}}(\theta_{d})=\frac{1}{2}$
for the first cell,
$\mathcal{P}_{\mathbb{C}_{2}}(\theta_{e})=\mathcal{P}_{\mathbb{C}_{2}}(\theta_{f})=\frac{1}{2}$
for the second cell,
$\mathcal{P}_{\mathbb{C}_{3}}(\theta_{c})=\mathcal{P}_{\mathbb{C}_{{3}}}(\theta_{bg})=\frac{1}{2}$
for the third cell. The transactions of nested cells are uniquely defined and
thus have all probability $1$.

Given a firing sequence $t_{1};\cdots;t_{n}$ we can set
$\mathcal{P}(t_{1};\cdots;t_{n})=\prod_{i=1}^{n}\mathcal{P}(t_{i})$. Hence
firing sequences that differ in the order in which transitions are fired are
assigned the same probability. Thanks to Theorem 5, we can consider maximal
persistent processes instead of firing sequences and set
$\mathcal{P}(O)=\prod_{t\in O}\mathcal{P}(t)$. In fact any maximal firing
sequence in $O$ includes all transitions of $O$ and its probability is
independent from the order of firing. It follows from Theorem 4.3 that any
maximal configuration has a corresponding maximal process (and viceversa) and
since Abbes and Benveniste proved that the sum of the probabilities assigned
to maximal configurations is $1$, the same holds for maximal persistent
processes.

######  Example .

Suppose the distributions are assigned as in Example 6. Then, the persistent
process in Fig. 14 has probability:
$\mathcal{P}(O)=\mathcal{P}(t_{d})\cdot\mathcal{P}(t_{f})\cdot\mathcal{P}(t_{3})\cdot\mathcal{P}(t_{8})\cdot\mathcal{P}(t_{b})\cdot\mathcal{P}(t^{\prime}_{8})=\frac{1}{2}\cdot\frac{1}{2}\cdot
1\cdot 1\cdot 1\cdot 1=\frac{1}{4}$. There are other four maximal processes
shown in Appendix E together with their probabilities. We note that the sum of
all probabilities assigned to maximal processes is indeed $1$.

##  7\. Conclusion and Future Work

AB’s branching cells are a sort of interpreter (or scheduler) for executing
PESs in the presence of confusion. Our main results develop along two
orthogonal axis. Firstly, our approach is an innovative construction with the
following advantages:

  1. (1)

Compositionality: s-cells are defined statically and locally, while AB’s
branching cells are defined dynamically and globally (by executing the whole
event structure).

  2. (2)

Compilation vs interpretation: AB’s construction gives an interpreter that
rules out some executions of an event structure. We instead compile a net into
another one (with persistency) whose execution is driven by ordinary firing
rules.

  3. (3)

Complete concurrency: AB’s recursively stopped configurations may include
traces that cannot be executed by the interpreter. Differently, our notion of
process captures all and only those executable traces of a concurrent
computation.

  4. (4)

Simplicity: s-cells definition in terms of a closure relation takes a couple
of lines (see Definition 3.1), while AB’s branching cell definition is more
involved.

  5. (5)

Full matching: we define a behavioural correspondence that relates AB’s
maximal configurations with our maximal deterministic processes, preserving
their probability assignment.

Secondly, we provide the following fully original perspectives:

  1. (1)

Confusion removal: our target model is confusion-free.

  2. (2)

Locally executable model: probabilistic choices are confined to transitions
with the same pre-set, and hence can be resolved locally and concurrently.
Besides, our target model relies on ordinary firing rules (with persistent
places).

  3. (3)

Processes: we define a novel notion of process for nets with persistency that
conservatively extends the ordinary notion of process and captures the right
amount of concurrency.

  4. (4)

Goal satisfaction: our construction meets all requirements in the list of
desiderata.

This paper has extended the conference version [7] by including more examples
and all detailed proofs of main results. The idea of expanding transactions
into the underlying processes is also original to this contribution.

Moreover, the construction presented here has opened the way to other
interesting research directions. First, it has led to the implementation of a
tool, called RemConf [18] after “removal of confusion”, that takes in input an
acyclic net $N$ in the standard format .pnml and returns the net
$\llparenthesis\llbracket N\rrbracket\rrparenthesis$. As persistent places
cannot be modeled in .pnml, they are implemented using self-loops instead of
input arcs when they are part of the preset of a transition. This makes it
possible to simulate the execution of $\llparenthesis\llbracket
N\rrbracket\rrparenthesis$ using any .pnml compatible tool. The tool is
available at http://remconf.di.unipi.it.

Regarding OR causality, it can be accounted for by general event structures,
where events can be enabled by distinct minimal sets of events. In [5] we have
extended the connection between p-nets and event structures in order to deal
with OR causes. Generalising the work on ordinary nets, Petri nets with
persistent places are related to a new subclass of general event structures,
called locally connected, by means of a chain of coreflections relying on an
unfolding construction, as for the original construction by Winskel. The fact
that a whole body of theory can be extended from Petri nets to p-nets
witnesses that p-nets can be chosen as a general computational model and not
just a convenient variant of an existing model. The causal AND/OR-dependencies
share some similarities also with the work on connectors and Petri nets with
boundaries [9] that we would like to formalize.

We also want to investigate the connection between our s-cell structure and
Bayesian networks, so to make forward and backward reasoning techniques
available in our setting. Some results in this direction can be found in [8].

Our construction is potentially complex: given a s-cell $\mathbb{C}$ we
recursively consider the nested s-cells in $N_{\mathbb{C}}\ominus p$, for any
initial place $p\in N_{\mathbb{C}}$. In the worst case, the number of nested
s-cells can be exponential on the number of their initial places. However
s-cells are typically much smaller than the whole net and it can be the case
that the size of all s-cells is bound by some fixed $k$. In this case, the
number of s-cells in our construction can still become exponential on the
constant $k$, but linear w.r.t. the number of places of the net.

A limitation of our approach is that it applies to finite occurrence nets only
(or, equivalently, to finite PESs). As a future work, we plan to deal with
cycles and unfolding semantics. This requires some efforts and we conjecture
it is feasible only if the net is safe and its behaviour has some regularity:
the same s-cell can be executed several times in a computation but every
instance is restarted without tokens left from previous rounds.

#### Acknowledgments

The idea of structural cells emerged, with a different goal, in collaboration
with Lorenzo Galeotti after his MSc thesis. The tool RemConf has been
developed as part of the MSc thesis of Gianluca Maraschio. We thank Glynn
Winskel, Holger Hermanns, Joost-Pieter Katoen for giving us insightful
references. The research has been supported by CONICET grant PIP
11220130100148CO and by Università di Pisa projects PRA_2016_64 _Through the
fog_ and PRA_2018_66 _DECLWARE: Metodologie dichiarative per la progettazione
e il deployment di applicazioni_. The third author carried on part of the work
while attending a Program on Logical Structures in Computation at Simons
Institute, Berkeley, 2016.

## References

  * [1] Samy Abbes and Albert Benveniste.  Branching cells as local states for event structures and nets: Probabilistic applications.  In FOSSACS’05, volume 3441 of Lect. Notes in Comp. Sci., pages 95–109. Springer, 2005.
  * [2] Samy Abbes and Albert Benveniste.  True-concurrency probabilistic models: Branching cells and distributed probabilities for event structures.  Inf. Comput., 204(2):231–274, 2006.
  * [3] Samy Abbes and Albert Benveniste.  True-concurrency probabilistic models: Markov nets and a law of large numbers.  Theor. Comput. Sci., 390(2-3):129–170, 2008.
  * [4] Andrea Asperti and Nadia Busi.  Mobile Petri nets.  Mathematical Structures in Computer Science, 19(6):1265–1278, 2009\.
  * [5] 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.
  * [6] Anne Bouillard, Stefan Haar, and Sidney Rosario.  Critical paths in the partial order unfolding of a stochastic petri net.  In International Conference on Formal Modeling and Analysis of Timed Systems, pages 43–57. Springer, 2009.
  * [7] Roberto Bruni, Hernán C. Melgratti, and Ugo Montanari.  Concurrency and probability: Removing confusion, compositionally.  In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 195–204. ACM, 2018.
  * [8] Roberto Bruni, Hernán C. Melgratti, and Ugo Montanari.  Unifying inference for Bayesian and Petri nets.  CoRR, abs/1807.06305, 2018.
  * [9] Roberto Bruni, Hernán C. Melgratti, Ugo Montanari, and Pawel Sobocinski.  Connector algebras for C/E and P/T nets’ interactions.  Logical Methods in Computer Science, 9(3), 2013.
  * [10] Federico Crazzolara and Glynn Winskel.  Petri nets with persistence.  Electr. Notes Theor. Comput. Sci., 121:143–155, 2005.
  * [11] Joanne Bechta Dugan, Kishor S. Trivedi, Robert Geist, and Victor F. Nicola.  Extended stochastic Petri nets: Applications and analysis.  In Performance’84, pages 507–519. North-Holland, 1984.
  * [12] Christian Eisentraut, Holger Hermanns, Joost-Pieter Katoen, and Lijun Zhang.  A semantics for every GSPN.  In Petri Nets 2013, volume 7927 of Lect. Notes in Comp. Sci., pages 90–109. Springer, 2013.
  * [13] Ursula Goltz and Wolfgang Reisig.  The non-sequential behavior of Petri nets.  Information and Control, 57(2/3):125–147, 1983.
  * [14] Stefan Haar.  Probabilistic cluster unfoldings.  Fundamenta Informaticae, 53(3-4):281–314, 2002.
  * [15] Joost-Pieter Katoen, Rom Langerak, and Diego Latella.  Modeling systems by probabilistic process algebra: An event structures approach.  1993\.
  * [16] Joost-Pieter Katoen and Doron A. Peled.  Taming confusion for modeling and implementing probabilistic concurrent systems.  In ESOP’13, volume 7792 of Lect. Notes in Comp. Sci., pages 411–430. Springer, 2013.
  * [17] Manfred Kudlek.  Probability in petri nets.  Fundamenta Informaticae, 67(1-3):121–130, 2005.
  * [18] Gianluca Maraschio.  A tool for confusion removal in probabilistic concurrent models, 2018\.  MSc thesis, Università degli Studi di Pisa.
  * [19] Marco Ajmone Marsan, Gianni Conte, and Gianfranco Balbo.  A class of generalized stochastic Petri nets for the performance evaluation of multiprocessor systems.  ACM Trans. Comput. Syst., 2(2):93–122, 1984.
  * [20] Michael K. Molloy.  Discrete time stochastic Petri nets.  IEEE Trans. Softw. Eng., 11(4):417–423, April 1985.
  * [21] Ugo Montanari and Francesca Rossi.  Contextual nets.  Acta Inf., 32(6):545–596, 1995.
  * [22] Mogens Nielsen, Gordon D. Plotkin, and Glynn Winskel.  Petri nets, event structures and domains, part I.  Theor. Comput. Sci., 13:85–108, 1981.
  * [23] C.A. Petri.  Kommunikation mit Automaten.  PhD thesis, Institut für Instrumentelle Mathematik, Bonn, 1962.
  * [24] Wolfgang Reisig.  Understanding Petri Nets - Modeling Techniques, Analysis Methods, Case Studies.  Springer, 2013.
  * [25] Grzegorz Rozenberg and Joost Engelfriet.  Elementary net systems.  In Advances in Petri Nets 1996, Part I, volume 1491 of Lect. Notes in Comp. Sci., pages 12–121. Springer, 1998.
  * [26] Einar Smith.  On the border of causality: Contact and confusion.  Theor. Comput. Sci., 153(1&2):245–270, 1996.
  * [27] Rob J. van Glabbeek, Ursula Goltz, and Jens-Wolfhard Schicke-Uffmann.  On characterising distributability.  Logical Methods in Computer Science, 9(3), 2013.
  * [28] Daniele Varacca, Hagen Völzer, and Glynn Winskel.  Probabilistic event structures and domains.  Theor. Comput. Sci., 358(2-3):173–199, 2006.
  * [29] Ingo Wegener.  The complexity of Boolean functions.  Wiley-Teubner series in computer science. John Wiley & Sons, Inc., New York, NY, USA, 1987.
  * [30] Glynn Winskel.  Event structures.  In Advances in Petri Nets 1986, Part II, volume 255 of Lect. Notes in Comp. Sci., pages 325–392. Springer, 1987.

##  Appendix A Detailed proofs of results in Section 2.4

######  Proposition 2.5.

Let $N=(T,b)\in\textsc{dn}(\mathbb{S})$. Then,

  1. (1)

$N\xlongrightarrow{t}N^{\prime}$ implies $\llparenthesis
N\rrparenthesis\xlongrightarrow{t}\llparenthesis N^{\prime}\rrparenthesis$;

  2. (2)

Moreover, $\llparenthesis N\rrparenthesis\xlongrightarrow{t}N^{\prime}$
implies there exists $N^{\prime\prime}$ such that
$N\xlongrightarrow{t}N^{\prime\prime}$ and $N^{\prime}=\llparenthesis
N^{\prime\prime}\rrparenthesis$.

###### Proof.

We start by showing that $N\xlongrightarrow{t}N^{\prime}$ implies
$\llparenthesis N\rrparenthesis\xlongrightarrow{t}\llparenthesis
N^{\prime}\rrparenthesis$. If $N\xlongrightarrow{t}N^{\prime}$ then
$t=S\to(T^{\prime},b^{\prime})\in T$, $S\subseteq b$ and $N^{\prime}=(T\cup
T^{\prime},(b\setminus S)\cup b^{\prime})$. By definition of
$\llparenthesis\\_\rrparenthesis$, it holds that $\llparenthesis
N\rrparenthesis=(\mathbb{S}\cup{\bf P}_{\mathbb{T}(N)},\mathbb{T}(N),F,b\cup
b_{T})$ where ${\bf P}_{\mathbb{T}(N)}=\\{{\bf p}_{t^{\prime}}\ |\
{t^{\prime}}\in\mathbb{T}(N)\\}$. Note that

$\begin{array}[]{l@{\ =\ }ll}\mathbb{T}(N)&T\cup\bigcup_{t^{\prime}\in
T}\mathbb{T}(t^{\prime\bullet})&\mbox{by def. of }\mathbb{T}(\\_)\\\
&T\cup\bigcup_{t^{\prime}\in
T}\mathbb{T}(t^{\prime\bullet})\cup\mathbb{T}(t^{\bullet})&t\in T\\\
&T\cup\bigcup_{t^{\prime}\in T}\mathbb{T}(t^{\prime\bullet})\cup
T^{\prime}\cup\bigcup_{t^{\prime}\in
T^{\prime}}\mathbb{T}(t^{\prime\bullet})&\mbox{by def. of }\mathbb{T}(\\_)\\\
&(T\cup T^{\prime})\cup\bigcup_{t^{\prime}\in T\cup
T^{\prime}}\mathbb{T}(t^{\prime\bullet})&\mbox{by assoc. and}\\\
\lx@intercol\hfil\mbox{comm. of }\cup\lx@intercol\\\
&\mathbb{T}(N^{\prime})&\mbox{by def. of }\mathbb{T}(\\_)\end{array}$

Hence, $\llparenthesis N^{\prime}\rrparenthesis=(\mathbb{S}\cup{\bf
P}_{\mathbb{T}(N)},\mathbb{T}(N),F,(b\setminus S)\cup b^{\prime}\cup b_{T\cup
T^{\prime}})$. By the definition of $\llparenthesis\\_\rrparenthesis$,
$t\in\mathbb{T}(N)$ and $F$ is such that $t:S\cup\\{{\bf p}_{t}\\}\to
b^{\prime}\cup b_{T^{\prime}}$. Hence, $t$ is enabled in $b\cup b_{T}$ because
$S\subseteq b$ and ${\bf p}_{t}\in b_{T}$. Consequently, $b\cup
b_{T}\xlongrightarrow{t}((b\cup b_{T})\setminus(S\cup\\{{\bf p}_{t}\\}))\cup
b^{\prime}\cup b_{T^{\prime}}=(b\setminus S)\cup b_{T}\cup b^{\prime}\cup
b_{T^{\prime}}=(b\setminus S)\cup b^{\prime}\cup b_{T\cup T^{\prime}}$.

The proof for $\llparenthesis N\rrparenthesis\xlongrightarrow{t}N^{\prime}$
implies there exists $N^{\prime\prime}$ such that
$N\xlongrightarrow{t}N^{\prime\prime}$ and $N^{\prime}=\llparenthesis
N^{\prime\prime}\rrparenthesis$ follows by analogous arguments. ∎

##  Appendix B Proofs of results in Section 3

This section presents the proofs of the results in Section 3. Note that we
need some auxiliary lemmas that are not present in the main text of the paper.
They are marked by the keyword “Aux” to avoid ambiguities. For reviewer’s
convenience, the high-level proof sketches are separated from the proofs in
full detail, that are included in a separate section.

We start by showing that the encoding of a net into a dynamic net does not add
computations. We show that each reachable marking $b$ of the dynamic net can
be associated with a reachable marking $m$ of the original net, when
disregarding negative information. We remark that in general the relation
between such $b$ and $m$ is that $b\cap P\subseteq m$ and not necessarily
$b\cap P=m$ (see, e.g., Lemma B). This is because the transitions
$t_{\theta,\mathbb{C}}$ generated by the encoding ($T_{\rm pos}$) always
consume the tokens in all minimal places of the branching cell $\mathbb{C}$.
This choice is immaterial for the behaviour of the encoded net, as made
explicit by the main results in the paper.

######  Lemma  (Aux.).

Let $N=(P,T,F,m)$. If $\llbracket N\rrbracket\rightarrow^{*}(T,b)$ then
$m\rightarrow^{*}m^{\prime}$ and $b\cap P\subseteq m^{\prime}$.

###### Proof.

The proof follows by induction on the length of the reduction $\llbracket
N\rrbracket\rightarrow^{n}(T,b)$.

  * •

Base case (n=0). It follows immediately because $b=m$.

  * •

Inductive case (n = k+1). Then, $\llbracket
N\rrbracket\rightarrow^{k}(T^{\prime},b^{\prime})\xlongrightarrow{t}(T,b)$. By
inductive hypothesis, $m\rightarrow^{*}m^{\prime\prime}$ and $b^{\prime}\cap
P\subseteq m^{\prime\prime}$. We now proceed by case analysis on the shape of
$t$.

    * –

$t={}^{\circ}{\mathbb{C}}\to(\emptyset,\theta^{\circ}\cup\overline{\mathbb{C}^{\circ}\setminus\theta^{\circ}})$.
Then, ${}^{\circ}{\mathbb{C}}\subseteq b^{\prime}$, $T=T^{\prime}$ and
$b=(b^{\prime}\setminus{}^{\circ}{\mathbb{C}})\cup\theta^{\circ}\cup\overline{\mathbb{C}^{\circ}\setminus\theta^{\circ}}$.
Since ${}^{\circ}{\mathbb{C}}\subseteq P$, we have
${}^{\circ}{\mathbb{C}}\subseteq m^{\prime\prime}$. Moreover,
$\theta:\mathbb{C}$ implies
${}^{\circ}{\theta}\subseteq{}^{\circ}{\mathbb{C}}\subseteq m^{\prime\prime}$.
Since $\theta$ is a deterministic process,
$m^{\prime\prime}\rightarrow^{*}(m^{\prime\prime}\setminus{}^{\circ}{\theta})\cup\theta^{\circ}$.
Then, take
$m^{\prime}=(m^{\prime\prime}\setminus{}^{\circ}{\theta})\cup\theta^{\circ}$.

Note that $b\cap P=((b^{\prime}\cap
P)\setminus{}^{\circ}{\mathbb{C}})\cup\theta^{\circ}$. We use $(b^{\prime}\cap
P)\subseteq m^{\prime\prime}$ and
${}^{\circ}{\theta}\subseteq{}^{\circ}{\mathbb{C}}$ to conclude that $b\cap
P\subseteq m^{\prime}$.

    * –

$t=\overline{\bf
p}\to(T^{\prime},\overline{\mathbb{C}^{\circ}\setminus(N_{\mathbb{C}}\ominus
p)^{\circ}})$. It follows immediately because $b^{\prime}\cap P=b\cap P$.

∎

######  Corollary  (Aux.).

If $N$ is 1-safe then $\llbracket N\rrbracket$ is $1$-$\infty$-safe.

######  Lemma 3.2.

Let $\llbracket N\rrbracket\in\textsc{dn}(P\cup\overline{\bf P})$. If
$\llbracket N\rrbracket\rightarrow^{*}(T,b)$ then for all $t,t^{\prime}\in T$
such that ${}^{\bullet}{t}\neq{}^{\bullet}{t^{\prime}}$ and
${}^{\bullet}{t}\cap{}^{\bullet}{t^{\prime}}\cap P\neq\emptyset$ it holds that
there is $p\in P\cap({}^{\bullet}{t}\cup{}^{\bullet}{t^{\prime}})$ such that
$\overline{\bf p}\in b$.

###### Proof.

The proof follows by induction on the length of the firing sequence
$\llbracket N\rrbracket\xrightarrow{t_{1}\cdots t_{n}}(T,b)$.

  * •

Base Case $n=0$. It holds trivially because any pair of different transitions
in $T$ have either the same preset (i.e., if they are taken from $T_{\rm pos}$
and originate from the same s-cell) or disjoint presets (i.e., if they are
taken both from $T_{\rm pos}$ but originate from different s-cells, or both
from $T_{\rm neg}$, or one from $T_{\rm neg}$ and the other from $T_{\rm
pos}$).

  * •

Inductive step $n=k+1$. Hence, $\llbracket N\rrbracket\xrightarrow{t_{1}\cdots
t_{k}}(T^{\prime},b^{\prime})\xlongrightarrow{t_{k+1}}(T,b)$. By inductive
hypothesis, for all $t,t^{\prime}\in T^{\prime}$ such that and
${}^{\bullet}{t}\cap{}^{\bullet}{t^{\prime}}\cap P\neq\emptyset$, it holds
that there is $p\in P\cap({}^{\bullet}{t}\cup{}^{\bullet}{t^{\prime}})$ such
that $\overline{\bf p}\in b^{\prime}$. Then, we proceed by case analysis on
$t_{k+1}$.

    * –

$t_{k+1}={}^{\circ}{\mathbb{C}}\to(\emptyset,\theta^{\circ}\cup\overline{\mathbb{C}^{\circ}\setminus\theta^{\circ}})$.
It holds trivially because $T=T^{\prime}$ and $b^{\prime}\cap\ \overline{\bf
P}\subseteq b$.

    * –

$t_{k+1}=\overline{\bf
p}\to(T^{\prime\prime},\overline{\mathbb{C}^{\circ}\setminus(N_{\mathbb{C}}\ominus
p)^{\circ}})$ for some $\mathbb{C}$, $p\in{}^{\circ}{\mathbb{C}}$, and
$(T^{\prime\prime},\emptyset)=\llbracket N_{\mathbb{C}}\ominus p\rrbracket$.
Then $T=T^{\prime}\cup T^{\prime\prime}$. By the definition of
$\llbracket\\_\rrbracket$, we have that for all $t,t^{\prime}\in
T^{\prime\prime}$ either (i) ${}^{\bullet}{t}={}^{\bullet}{t^{\prime}}$ or
(ii) ${}^{\bullet}{t}\cap{}^{\bullet}{t^{\prime}}=\emptyset$ (reasoning
analogously to the Base Case). It remains to consider the cases in which $t$
and $t^{\prime}$ are taken one from $T^{\prime}$ and the other from
$T^{\prime\prime}$. W.l.o.g., we consider $t\in T^{\prime\prime}$ and
$t^{\prime}\in T^{\prime}$ and proceed as follows. By the definition of
$\llbracket\\_\rrbracket$, $t\in T^{\prime\prime}$ implies either (i)
${}^{\bullet}{t}\subseteq\overline{\bf P}$ or (ii)
${}^{\bullet}{t}={}^{\circ}{\mathbb{C}_{1}}$ for
$\mathbb{C}_{1}\in\textsc{bc}(N_{\mathbb{C}}\ominus p)$. Case (i), follows
immediately because there does not exist $t^{\prime}$ s.t.
${}^{\bullet}{t}\cap{}^{\bullet}{t^{\prime}}\cap P\neq\emptyset$. For (ii), we
note that ${}^{\bullet}{t}^{\prime}={}^{\circ}{\mathbb{C}_{2}}$ with
$\mathbb{C}_{1}\neq\mathbb{C}_{2}$,
${}^{\circ}{\mathbb{C}_{1}}\cap{}^{\circ}{\mathbb{C}_{2}}\neq\emptyset$ and
${}^{\bullet}{t}\cup{}^{\bullet}{t^{\prime}}\subseteq P$. We proceed by
contradiction and assume
$\overline{({}^{\bullet}{t}\cup{}^{\bullet}{t^{\prime}})}\cap b=\emptyset$.
There must exist an s-cell $\mathbb{C}_{3}$ such that
$\mathbb{C}_{1}\cup\mathbb{C}_{2}\subseteq\mathbb{C}_{3}$ (because
$\mathbb{C}_{1}$ and $\mathbb{C}_{2}$ are closed under immediate conflict and
their union introduces immediate conflict between the transitions consuming
from the shared places in
${}^{\circ}{\mathbb{C}_{1}}\cap{}^{\circ}{\mathbb{C}_{2}}$). If
$\mathbb{C}_{2}=\mathbb{C}_{3}$, then $\mathbb{C}_{1}\subset\mathbb{C}_{2}$.
Hence $p\in{}^{\circ}{\mathbb{C}_{2}}$ and $p\in{}^{\bullet}{t^{\prime}}$,
which contradicts
$\overline{({}^{\bullet}{t}\cup{}^{\bullet}{t^{\prime}})}\cap b=\emptyset$
because $t_{k+1}$ enabled at $b$ implies $\overline{\bf p}\in b$. Otherwise,
$\mathbb{C}_{2}\subset\mathbb{C}_{3}$. Consequently, there exists (at least) a
transition $t^{\prime\prime}\in T^{\prime}$ such that
${}^{\bullet}{t^{\prime\prime}}={}^{\circ}{\mathbb{C}_{3}}$ and
${}^{\bullet}{t^{\prime}}\neq{}^{\bullet}{t^{\prime\prime}}$. Since
$t^{\prime}\in T^{\prime}$ and $t^{\prime\prime}\in T^{\prime}$, we can use
inductive hypothesis to conclude that
$\overline{({}^{\bullet}{t^{\prime}}\cup{}^{\bullet}{t^{\prime\prime}})}\cap
b\neq\emptyset$. The proof is completed by noting that this is in
contradiction with the assumption
$\overline{({}^{\bullet}{t}\cup{}^{\bullet}{t^{\prime}})}\cap b=\emptyset$
because
${}^{\bullet}{t^{\prime\prime}}\supseteq{}^{\bullet}{t}\cup{}^{\bullet}{t^{\prime}}$.

∎

In what follows we write $p\prec q$ if $p\preceq q$ and $p\neq q$. The
following auxiliary result provides some invariants about the configurations
that can be reached by an encoded dynamic net.

######  Lemma  (Aux.).

If $\llbracket N\rrbracket\rightarrow^{*}(T,b)$ then

  1. (1)

${p}\in b$ implies $\overline{\bf p}\not\in b$;

  2. (2)

if $\overline{\bf p}\in b$ and $p\preceq q$ then $q\not\in b$;

  3. (3)

if $p\preceq q$, $p\in b$ and $\overline{\bf q}\in b$ then there exists
$r\prec q$ and $\overline{\bf r}\in b$; and

  4. (4)

if $(T,b)\xlongrightarrow{t}$ and ${}^{\bullet}{t}={}^{\circ}{\mathbb{C}}$ for
some $\mathbb{C}$ then
$(\mathbb{C}^{\circ}\cup\overline{\mathbb{C}^{\circ}})\cap b=\emptyset$.

###### Proof.

The proof follows by induction on the length of the firing sequence
$\llbracket N\rrbracket\xrightarrow{t_{1}\cdots t_{n}}(T,b)$.

  * •

Base Case $n=0$. Hence $(T,b)=\llbracket N\rrbracket$.

    1. (1)

It follows from $b\subseteq P$.

    2. (2)

Since $b\subseteq P$ there is no $\overline{\bf p}\in b$.

    3. (3)

Since $b\subseteq P$ there is no $\overline{\bf q}\in b$.

    4. (4)

It follows from the fact that $N$ is an occurrence net,
$b\subseteq{}^{\circ}{N}$, and hence there does not exist any
$\mathbb{C}\in\textsc{bc}(N)$ such that
$(\mathbb{C}^{\circ}\cup\overline{\mathbb{C}^{\circ}})\cap b\neq\emptyset$.

  * •

Inductive step $n=k+1$. Hence, $\llbracket N\rrbracket\xrightarrow{t_{1}\cdots
t_{k}}(T^{\prime},b^{\prime})\xlongrightarrow{t_{k+1}}(T,b)$. By inductive
hypothesis, (1) ${p}\in b^{\prime}$ implies $\overline{\bf p}\not\in
b^{\prime}$; (2) if $\overline{\bf p}\in b^{\prime}$ and $p\preceq q$ then
$q\not\in b^{\prime}$; (3) if $p\preceq q$, $p\in b^{\prime}$ and
$\overline{\bf q}\in b^{\prime}$ then there exists $r\prec q$ and
$\overline{\bf r}\in b^{\prime}$; and (4) if
$(T^{\prime},b^{\prime})\xlongrightarrow{t}$ and
${}^{\bullet}{t}={}^{\circ}{\mathbb{C}}$ for some ${\mathbb{C}}$ then
$(\mathbb{C}^{\circ}\cup\overline{\mathbb{C}^{\circ}})\cap
b^{\prime}=\emptyset$. We now proceed by case analysis on $t_{k+1}$.

    * –

$t_{k+1}={}^{\circ}{\mathbb{C}_{k+1}}\to(\emptyset,\theta^{\circ}\cup\overline{\mathbb{C}_{k+1}^{\circ}\setminus\theta^{\circ}})$
for some s-cell $\mathbb{C}_{k+1}$ and transaction $\theta:\mathbb{C}_{k+1}$.
Hence,
$b=(b^{\prime}\setminus{}^{\circ}{\mathbb{C}_{k+1}})\cup(\theta^{\circ}\cup\overline{\mathbb{C}_{k+1}^{\circ}\setminus\theta^{\circ}})$.

      1. (1)

We proceed by contradiction. Assume that there exists $p$ such that $p\in b$
and $\overline{\bf p}\in b$. Since $p\in b$ we have that either $p\in
b^{\prime}\setminus{}^{\circ}{\mathbb{C}_{k+1}}$ or $p\in\theta^{\circ}$.
First, assume $p\in b^{\prime}\setminus{}^{\circ}{\mathbb{C}_{k+1}}$. By
inductive hypothesis (1), $\overline{\bf p}\not\in b^{\prime}$ and, hence,
$\overline{\bf p}\not\in b^{\prime}\setminus{}^{\circ}{\mathbb{C}_{k+1}}$.
Therefore, it should be the case that $\overline{\bf
p}\in(\theta^{\circ}\cup\overline{\mathbb{C}_{k+1}^{\circ}\setminus\theta^{\circ}})$.
Hence, $\overline{\bf p}\in\overline{\mathbb{C}_{k+1}^{\circ}}$ and
${p}\in{\mathbb{C}_{k+1}^{\circ}}$. Since $t_{k+1}$ is enabled at
$(T^{\prime},b^{\prime})$, we can use inductive hypothesis (4) on ${t_{k+1}}$
to conclude
$(\mathbb{C}_{k+1}^{\circ}\cup\overline{\mathbb{C}_{k+1}^{\circ}})\cap
b^{\prime}=\emptyset$. Consequently, ${p}\in{\mathbb{C}_{k+1}^{\circ}}$
implies $p\not\in b^{\prime}$. But this is in contradiction with the
assumption that $p\in b^{\prime}\setminus{}^{\circ}{\mathbb{C}_{k+1}}$. Assume
instead $p\in\theta^{\circ}$. Then $\overline{\bf
p}\not\in\overline{\mathbb{C}_{k+1}^{\circ}\setminus\theta^{\circ}}$. Hence,
it should be the case that $\overline{\bf p}\in
b^{\prime}\setminus{}^{\circ}{\mathbb{C}_{k+1}}$. But this is also in
contradiction with the hypothesis (4)
$(\mathbb{C}_{k+1}^{\circ}\cup\overline{\mathbb{C}_{k+1}^{\circ}})\cap
b^{\prime}=\emptyset$.

      2. (2)

We proceed by contradiction. Assume there exist $p$ and $q$ such that
$\overline{\bf p}\in b$, $p\preceq q$ and $q\in b$.

         * *

Firstly, consider $\overline{\bf p}\in
b^{\prime}\setminus{}^{\circ}{\mathbb{C}_{k+1}}$, which implies $\overline{\bf
p}\in b^{\prime}$. By inductive hypothesis (2), for all $q$ s.t. $p\preceq q$
it holds that $q\not\in b^{\prime}$.Hence, it should be the case that
$q\in(\theta^{\circ}\cup\overline{\mathbb{C}_{k+1}^{\circ}\setminus\theta^{\circ}})$.
Hence either (i) $p=q$, (ii) $p\in{}^{\circ}{\mathbb{C}_{k+1}}$ or (iii)
$p\prec p^{\prime}$ and $p^{\prime}\prec q$ for some
$p^{\prime}\in{}^{\circ}{\mathbb{C}_{k+1}}$. For (i), note that
$q=p\in(\theta^{\circ}\cup\overline{\mathbb{C}_{k+1}^{\circ}\setminus\theta^{\circ}})$.
Hence, $q\in\mathbb{C}_{k+1}^{\circ}$, which is in contradiction with the
assumption $\overline{\bf p}\in b^{\prime}$ and the inductive hypothesis (4).
For (ii), note that it implies $p\in b^{\prime}$, which is in contradiction
with the assumption $\overline{\bf p}\in b^{\prime}$ and inductive hypothesis
(1). For (iii), note that $\overline{\bf p}\in b^{\prime}$ and $p\prec
p^{\prime}$ imply $p^{\prime}\not\in b^{\prime}$ by inductive hypothesis (2),
which is in contradiction with the fact that
$p^{\prime}\in{}^{\circ}{\mathbb{C}_{k+1}}$ and $t_{k+1}$ is enabled.

         * *

Assume instead $\overline{\bf
p}\in\theta^{\circ}\cup\overline{\mathbb{C}_{k+1}^{\circ}\setminus\theta^{\circ}}$.
Hence, $p\in\mathbb{C}_{k+1}^{\circ}\setminus\theta^{\circ}$ and therefore
$p\in{\mathbb{C}_{k+1}^{\circ}}$. Suppose there is $q\in b^{\prime}$ and
$p\preceq q$. Note that $p^{\prime}\preceq p$ for all
$p^{\prime}\in{}^{\circ}{\mathbb{C}_{k+1}}$ by definition of branching cells.
By transitivity of $\preceq$, $p^{\prime}\preceq q$ for all
$p^{\prime}\in{}^{\circ}{\mathbb{C}_{k+1}}$. Since $t_{k+1}$ is enabled at
$b^{\prime}$, ${}^{\circ}{\mathbb{C}_{k+1}}\subseteq b^{\prime}$. By using
Lemma B, we can conclude that $q\not\in b^{\prime}$ for all $q$ s.t. $p\preceq
q$, which contradicts the hypothesis $q\in b^{\prime}$ and $p\preceq q$.
Assume instead
$q\in\theta^{\circ}\cup\overline{\mathbb{C}_{k+1}^{\circ}\setminus\theta^{\circ}}$.
Hence, $q\in\theta^{\circ}$. Hence, $p\neq q$. Moreover,
$p\in\mathbb{C}_{k+1}^{\circ}$ and $q\in\mathbb{C}_{k+1}^{\circ}$ contradict
the assumption $p\preceq q$.

      3. (3)

We proceed by case analysis. If $p\in b^{\prime}$ and $\overline{\bf q}\in
b^{\prime}$ then the proof follows by inductive hypothesis. If $p\in
b^{\prime}$ and $\overline{\bf q}\not\in b^{\prime}$, then $\overline{\bf
q}\in\theta^{\circ}\cup\overline{\mathbb{C}_{k+1}^{\circ}\setminus\theta^{\circ}}$.
Therefore, $p\preceq q$ implies $p\in{}^{\circ}{\mathbb{C}}$, which
contradicts the assumption $p\in b$. If $p\not\in b^{\prime}$ and
$\overline{\bf q}\in b^{\prime}$, then $p\in\theta^{\circ}$, which contradicts
$p\preceq q$.

      4. (4)

Let $t\in T$ such that ${}^{\bullet}{t}={}^{\circ}{\mathbb{C}}\subseteq b$ for
some $\mathbb{C}$. Since $t$ is enabled at $b$ and $\llbracket N\rrbracket$ is
$1$-$\infty$-safe by Corollary B, then
$\mathbb{C}_{k+1}\cap\mathbb{C}=\emptyset$. If $t$ is enabled at
$(b^{\prime}\setminus{}^{\circ}{\mathbb{C}_{k+1}})$ then $t$ is enabled at
$b^{\prime}$. By inductive hypothesis (4), we conclude that
$(\mathbb{C}^{\circ}\cup\overline{\mathbb{C}^{\circ}})\cap(b^{\prime}\setminus{}^{\circ}{\mathbb{C}_{k+1}})=\emptyset$.
If $t$ is not enabled at $(T^{\prime},b^{\prime})$, then it holds that for
$x\in{}^{\circ}{\mathbb{C}}$ exists
$y\in(\mathbb{C}_{k+1}^{\circ}\cup\overline{\mathbb{C}_{k+1}^{\circ}})$ such
that $y\preceq x$. By inductive hypothesis
$(\mathbb{C}_{k+1}^{\circ}\cup\overline{\mathbb{C}_{k+1}^{\circ}})\cap
b^{\prime}=\emptyset$, hence
$(\mathbb{C}^{\circ}\cup\overline{\mathbb{C}^{\circ}})\cap
b^{\prime}=\emptyset$. Therefore,
$(\mathbb{C}^{\circ}\cup\overline{\mathbb{C}^{\circ}})\cap b=\emptyset$.

    * –

$t_{k+1}=\overline{\bf
r}\to(T^{\prime\prime},\overline{\mathbb{C}_{k+1}^{\circ}\setminus(N_{{\mathbb{C}_{k+1}}}\ominus
r)^{\circ}})$ for some s-cell $\mathbb{C}_{k+1}$ and place
$r\in{}^{\circ}{\mathbb{C}_{k+1}}$. Then, $T=T^{\prime}\cup T^{\prime\prime}$
with $\llbracket N_{{\mathbb{C}_{k+1}}}\ominus
r\rrbracket=(T^{\prime\prime},\\_)$ and
$b=b^{\prime}\cup\overline{\mathbb{C}_{k+1}^{\circ}\setminus(N_{{\mathbb{C}_{k+1}}}\ominus
r)^{\circ}}$.

      1. (1)

We proceed by contradiction. Assume that there exists $p$ such that $p\in b$
and $\overline{\bf p}\in b$. Note that $p\in b$ implies $p\in b^{\prime}$. By
inductive hypothesis (1), $\overline{\bf p}\not\in b^{\prime}$. Therefore, it
should be the case that $\overline{\bf
p}\in\overline{\mathbb{C}_{k+1}^{\circ}\setminus(N_{{\mathbb{C}_{k+1}}}\ominus
r)^{\circ}}$. Consequently $p\in\mathbb{C}_{k+1}^{\circ}$ and
$p\not\in(N_{{\mathbb{C}_{k+1}}}\ominus r)^{\circ}$. Hence, $r\preceq p$.
Since $t$ is enabled at $b^{\prime}$, $\overline{\bf r}\in b^{\prime}$. By
inductive hypothesis (2), $p\not\in b^{\prime}$ which contradicts the
hypothesis $p\not\in b$.

      2. (2)

We proceed by contradiction. Assume there exist $p$ and $q$ such that
$\overline{\bf p}\in b$, $p\preceq q$ and $q\in b$. Note that $q\in b$ implies
$q\in b^{\prime}$. Assume $\overline{\bf p}\in b^{\prime}$. By inductive
hypothesis, for all $q$ s.t. $p\preceq q$ then $q\not\in b^{\prime}$ and,
hence it is in contradiction with assumption $q\in b$. Assume instead
$\overline{\bf
p}\in\overline{\mathbb{C}_{k+1}^{\circ}\setminus(N_{{\mathbb{C}_{k+1}}}\ominus
r)^{\circ}}$. As before, we conclude that $r\preceq p$. By transitivity of
$\preceq$, we have $r\preceq q$. By inductive hypothesis (2), $q\not\in
b^{\prime}$, which is in contradiction with assumption $q\in b$.

      3. (3)

For $\overline{\bf q}\in b^{\prime}$, it follows immediately by inductive
hypothesis. For $\overline{\bf
q}\in\overline{\mathbb{C}_{k+1}^{\circ}\setminus(N_{{\mathbb{C}_{k+1}}}\ominus
r)^{\circ}}$, it follows straightforwardly because $r\preceq q$ and
$\overline{\bf r}\in b$.

      4. (4)

Assume ${}^{\bullet}{t}={}^{\circ}{\mathbb{C}}\subseteq b$ for some
$\mathbb{C}$. Hence, ${}^{\bullet}{t}={}^{\circ}{\mathbb{C}}\subseteq
b^{\prime}$. There are two cases:

         * *

Suppose $t\in T^{\prime}$. By inductive hypothesis (4),
$(\mathbb{C}^{\circ}\cup\overline{\mathbb{C}^{\circ}})\cap
b^{\prime}=\emptyset$. We show that the following holds

$(\mathbb{C}^{\circ}\cup\overline{\mathbb{C}^{\circ}})\cap\overline{\mathbb{C}_{k+1}^{\circ}\setminus(N_{{\mathbb{C}_{k+1}}}\ominus
r)^{\circ}}=\emptyset$

It is enough to show that

$\overline{\mathbb{C}^{\circ}}\cap\overline{\mathbb{C}_{k+1}^{\circ}\setminus(N_{{\mathbb{C}_{k+1}}}\ominus
r)^{\circ}}=\emptyset$

We proceed by contradiction and assume there exists $q$ such that
$q\in\mathbb{C}^{\circ}$ and
$q\in(\mathbb{C}_{k+1}^{\circ}\setminus(N_{{\mathbb{C}_{k+1}}}\ominus
r)^{\circ})$. Because
$q\in(\mathbb{C}_{k+1}^{\circ}\setminus(N_{{\mathbb{C}_{k+1}}}\ominus
r)^{\circ})$, $r\preceq q$. Since $q\in\mathbb{C}^{\circ}$,
$r\in{}^{\circ}{\mathbb{C}}$ (because $\mathbb{C}$ is closed under causality).
Hence $r\in b^{\prime}$ because $t$ is enabled at $b^{\prime}$. By the
contrapositive of inductive hypothesis (1), $\overline{\bf r}\not\in
b^{\prime}$, but this is in contradiction with the hypothesis that $t_{k+1}$
is enabled at $b^{\prime}$.

         * *

Suppose $t\in T^{\prime\prime}$. Then,
${}^{\bullet}{t}\cap{}^{\circ}{(N_{{\mathbb{C}_{k+1}}}\ominus r)}=\emptyset$.
Hence, for all $q\in\mathbb{C}^{\circ}$ there exists
$s\in{}^{\circ}{\mathbb{C}}$ s.t. $s\preceq q$. Since $t$ is enabled at $b$,
${}^{\circ}{\mathbb{C}}\subseteq b$ holds. By Lemma B, $\mathbb{C}^{\circ}\cap
b=\emptyset$. We show by contradiction that $\overline{\mathbb{C}^{\circ}}\cap
b=\emptyset$ does not hold either. Assume that there exists $\overline{\bf
q}\in\overline{\mathbb{C}^{\circ}}$ and $\overline{\bf q}\in b$. Since there
exists $s\in{}^{\circ}{\mathbb{C}}\subseteq b$ and $s\preceq q$, we can use
inductive hypothesis (3) to conclude that there exist $o\preceq q$ s.t.
$\overline{\bf o}\in b$. By the inductive hypothesis (2) $q\not\in b$, and
this is in contradiction with the assumption of $t$ enabled at $b$.

∎

######  Lemma 3.2.

If $\llbracket N\rrbracket\rightarrow^{*}(T,b)$ and $\overline{\bf p}\in b$
then $(T,b)\rightarrow^{*}(T^{\prime},b^{\prime})$ implies that $p\not\in
b^{\prime}$.

###### Proof.

If $\overline{\bf p}\in b$ then $\overline{\bf p}\in b^{\prime}$ because
$\overline{\bf p}$ is persistent. Moreover, $\llbracket
N\rrbracket\rightarrow^{*}(T^{\prime},b^{\prime})$. By the contrapositive of