TR CONCUR 11institutetext:  NICTA, Sydney, Australia 22institutetext: School
of Comp. Sc. and Engineering, Univ. of New South Wales, Sydney, Australia
33institutetext: Institute for Programming and Reactive Systems, TU
Braunschweig, Germany
33email<EMAIL_ADDRESS>33email<EMAIL_ADDRESS>33email:
<EMAIL_ADDRESS>
#  On Causal Semantics of Petri Nets
(extended abstract)††thanks: This work was partially supported by the DFG
(German Research Foundation).

Rob van Glabbeek 1122 Ursula Goltz 33 Jens-Wolfhard Schicke 33

# On Causal Semantics of Petri Nets††thanks: This work was partially supported
by the DFG (German Research Foundation).

Rob van Glabbeek 1122 Ursula Goltz 33 Jens-Wolfhard Schicke 33

###### Abstract

We consider approaches for causal semantics of Petri nets, explicitly
representing dependencies between transition occurrences. For one-safe nets or
condition/event-systems, the notion of process as defined by Carl Adam Petri
provides a notion of a run of a system where causal dependencies are reflected
in terms of a partial order. A well-known problem is how to generalise this
notion for nets where places may carry several tokens. Goltz and Reisig have
defined such a generalisation by distinguishing tokens according to their
causal history. However, this so-called _individual token interpretation_ is
often considered too detailed. A number of approaches have tackled the problem
of defining a more abstract notion of process, thereby obtaining a so-called
_collective token interpretation_. Here we give a short overview on these
attempts and then identify a subclass of Petri nets, called _structural
conflict nets_ , where the interplay between conflict and concurrency due to
token multiplicity does not occur. For this subclass, we define abstract
processes as equivalence classes of Goltz-Reisig processes. We justify this
approach by showing that we obtain exactly one maximal abstract process if and
only if the underlying net is conflict-free with respect to a canonical notion
of conflict.

##  1 Introduction

In this paper we address a well-known problem in Petri net theory, namely how
to generalise Petri’s concept of non-sequential processes to nets where places
may carry multiple tokens.

One of the most interesting features of Petri nets is that they allow the
explicit representation of causal dependencies between action occurrences when
modelling reactive systems. This is a key difference with models of reactive
systems (like standard transition systems) with an inherent so-called
interleaving semantics, modelling concurrency by non-deterministic choice
between sequential executions. In [GG01] it has been shown, using the model of
event structures or configuration structures, that causal semantics are
superior to interleaving semantics when giving up the assumption that actions
are atomic entities.

In the following, we give a concise overview on existing approaches on
semantics of Petri nets that give an account of their runs, without claiming
completeness, and following closely a similar presentation in [GGS11].

Initially, Petri introduced the concept of a net together with a definition of
its dynamic behaviour in terms of the firing rule for single transitions or
for finite sets (_steps_) of transitions firing in parallel. Sequences of
transition firings or of steps are the usual way to define the behaviour of a
Petri net. When considering only single transition firings, the set of all
firing sequences yields a linear time interleaving semantics (no choices
between alternative behaviours are represented). Otherwise we obtain a linear
time step semantics, with information on possible parallelism, but without
explicit representation of causal dependencies between transition occurrences.

Petri then defined _condition/event systems_ , where — amongst other
restrictions — places (there called conditions) may carry at most one token.
For this class of nets, he proposed what is now the classical notion of a
_process_ , given as a mapping from an _occurrence net_ (acyclic net with
unbranched places) to the original net [Pet77, GSW80]. A process models a run
of the represented system, obtained by choosing one of the alternatives in
case of conflict. It records all occurrences of the transitions and places
visited during such a run, together with the causal dependencies between them,
which are given by the flow relation of the net. A linear-time causal
semantics of a condition/event system is thus obtained by associating with a
net the set of its processes. Depending on the desired level of abstraction,
it may suffice to extract from each process just the partial order of
transition occurrences in it. The firing sequences of transitions or steps can
in turn be extracted from these partial orders. Nielsen, Plotkin and Winskel
extended this to a branching-time semantics by using occurrence nets with
forward branched places [NPW81]. These capture all runs of the represented
system, together with the branching structure of choices between them.

However, the most frequently used class of Petri nets are nets where places
may carry arbitrary many tokens, or a certain maximal number of tokens when
adding place capacities. This type of nets is often called _place/transition
systems_ (P/T systems). Here tokens are usually assumed to be
indistinguishable entities, for example representing a number of available
resources in a system. Unfortunately, it is not straightforward to generalise
the notion of process, as defined by Petri for condition/event systems, to P/T
systems. In fact, it has now for more than 20 years been a well-known problem
in Petri net theory how to formalise an appropriate causality-based concept of
process or run for general P/T systems. In the following we give an
introduction to the problem and a short overview on existing approaches.

As a first approach, Goltz and Reisig generalised Petri’s notion of process to
general P/T systems [GR83]. We call this notion of a process _GR-process_. It
is based on a canonical unfolding of a P/T systems into a condition/event
system, representing places that may carry several tokens by a corresponding
number of conditions (see [Gol87]). Figure 1 shows a P/T system with two of
its GR-processes.

0.9 0.712

a

b43

c512

a

b

44

c

3512

a

b

44

c

35

Figure 1: A net $N$ with its two maximal GR-processes. The correspondence
between elements of the net and their occurrences in the processes is
indicated by labels.

Engelfriet adapted GR-processes by additionally representing choices between
alternative behaviours [Eng91], thereby adopting the approach of [NPW81] to
P/T systems, although without arc weights. Meseguer, Sassone and Montanari
extended this to cover also arc weights [MMS97].

However, if one wishes to interpret P/T systems with a causal semantics, there
are alternative interpretations of what “causal semantics” should actually
mean. Goltz already argued that when abstracting from the identity of multiple
tokens residing in the same place, GR-processes do not accurately reflect runs
of nets, because if a Petri net is conflict-free it should intuitively have
only one complete run (for there are no choices to resolve), yet it may have
multiple maximal GR-processes [Gol86]. This phenomenon already occurs in
Figure 1, since the choice between alternative behaviours is here only due to
the possibility to choose between two tokens which can or even should be seen
as indistinguishable entities. A similar argument is made, e.g., in [HKT95].

At the heart of this issue is the question whether multiple tokens residing in
the same place should be seen as individual entities, so that a transition
consuming just one of them constitutes a conflict, as in the interpretation
underlying GR-processes and the approach of [Eng91, MMS97], or whether such
tokens are indistinguishable, so that taking one is equivalent to taking the
other. Van Glabbeek and Plotkin call the former viewpoint the _individual
token interpretation_ of P/T systems. For an alternative interpretation, they
use the term _collective token interpretation_ [GP95]. A possible
formalisation of these interpretations occurs in [Gla05]. In the following we
call process notions for P/T systems which are adherent to a collective token
philosophy _abstract processes_. Another option, proposed by Vogler, regards
tokens only as notation for a natural number stored in each place; these
numbers are incremented or decremented when firing transitions, thereby
introducing explicit causality between any transitions removing tokens from
the same place [Vog91].

Mazurkiewicz applies again a different approach in [Maz89]. He proposes
_multitrees_ , which record possible multisets of fired transitions, and then
takes confluent subsets of multitrees as abstract processes of P/T systems.
This approach does not explicitly represent dependencies between transition
occurrences and hence does not apply to nets with self-loops, where such
information may not always be retrieved.

Yet another approach has been proposed by Best and Devillers in [BD87]. Here
an equivalence relation is generated by a transformation for changing
causalities in GR-processes, called _swapping_ , that identifies GR-processes
which differ only in the choice which token was removed from a place. In this
paper, we adopt this approach and we show that it yields a fully satisfying
solution for a subclass of P/T systems. We call the resulting notion of a more
abstract process _BD-process_. In the special case of one-safe P/T systems
(where places carry at most one token), or for condition/event systems, no
swapping is possible, and a BD-process is just an isomorphism class of GR-
processes.

Meseguer and Montanari formalise runs in a net $N$ as morphisms in a category
$\mathcal{T}(N)$ [MM88]. In [DMM89] it has been established that these
morphisms “coincide with the commutative processes defined by Best and
Devillers” (their terminology for BD-processes). Likewise, Hoogers, Kleijn and
Thiagarajan represent an abstract run of a net by a _trace_ , thereby
generalising the trace theory of Mazurkiewicz [Maz95], and remark that “it is
straightforward but laborious to set up a 1-1 correspondence between our
traces and the equivalence classes of finite processes generated by the swap
operation in [Best and Devillers, 1987]”.

To explain why it can be argued that BD-processes are not fully satisfying as
abstract processes for general P/T systems, we recall in Figure 2 an example
due to Ochmański [Och89, BMO09], see also [DMM89, GGS11]. In the initial
situation only two of the three enabled transitions can fire, which
constitutes a conflict. However, the equivalence obtained from the swapping
transformation (formally defined in Section 3) identifies all possible maximal
GR-processes and hence yields only one complete abstract run of the system. We
are not aware of a solution, i.e. any formalisation of the concept of a run of
a net that correctly represents both causality and parallelism of nets, and
meets the requirement that for this net there is more than one possible
complete run.

0.9 0.7

a

b

c

d-¿[270]d; 0.1

Figure 2: A net with only a single process up to swapping equivalence.

In [GGS11] and in the present paper, we continue the line of research of
[MM88, DMM89, Maz89, HKT95] to formalise a causality-based notion of an
abstract process of a P/T system that fits a collective token interpretation.
As remarked already in [Gol86], ‘what we need is some notion of an “abstract
process”’ and ‘a notion of maximality for abstract processes’, such that ‘a
P/T-system is conflict-free iff it has exactly one maximal abstract process
starting at the initial marking’. The example from Figure 2 shows that BD-
processes are in general not suited. We defined in [GGS11] a subclass of P/T
systems where conflict and concurrency are clearly separated. We called these
nets _structural conflict nets_. Using the formalisation of conflict for P/T
systems from [Gol86], we have shown that, for this subclass of P/T systems, we
obtain more than one maximal BD-process whenever the net contains a
conflict.111The notion of maximality for BD-processes is not trivial. However,
with the results from Section 6, Corollary 1 from [GGS11] may be rephrased in
this way. The proof of this result is quite involved; it was achieved by using
an alternative characterisation of BD-processes via firing sequences from
[BD87].

In this paper, we will show the reverse direction of this result, namely that
we obtain exactly one maximal BD-process of a structural conflict net if the
net is conflict-free. Depending on the precise formalisation of a suitable
notion of maximality of BD-processes, this holds even for arbitrary nets.
Summarising, we then have established that we obtain exactly one maximal
abstract process in terms of BD-processes for structural conflict nets _if and
only if_ the net is conflict-free with respect to a canonical notion of
conflict.

We proceed by defining basic notions for P/T systems in Section 2. In Section
3, we define GR-processes and introduce the swapping equivalence. Section 4
recalls the concept of conflict in P/T systems and defines structural conflict
nets.222The material in Sections 2 to 4 follows closely the presentation in
[GGS11], but needs to be included to make the paper self-contained. In Section
5, we recapitulate the alternative characterisation of BD-processes from
[BD87] in terms of an equivalence notion on firing sequences [BD87] and prove
in this setting that a conflict-free net has exactly one maximal run. Finally,
in Section 6, we investigate notions of maximality for BD-processes and then
transfer the result from Section 5 to BD-processes. Due to lack of space, the
proofs of Lemma’s 2, 3, 9, 11 and 12, some quite involved, are omitted; these
can be found in [glabbeek11causaltr].

##  2 Place/transition Systems

We will employ the following notations for multisets.

###### Definition 1

Let $X$ be a set.

  * $\bullet$

A multiset over $X$ is a function $A\\!:X\rightarrow\bbbn$, i.e.
$A\in\bbbn^{X}\\!\\!$.

  * $\bullet$

$x\in X$ is an _element of_ $A$, notation $x\in A$, iff $A(x)>0$.

  * $\bullet$

For multisets $A$ and $B$ over $X$ we write $A\subseteq B$ iff $A(x)\leq B(x)$
for all $x\mathbin{\in}X$;
$A\cup B$ denotes the multiset over $X$ with $(A\cup
B)(x):=\text{max}(A(x),B(x))$,
$A\cap B$ denotes the multiset over $X$ with $(A\cap
B)(x):=\text{min}(A(x),B(x))$,
$A+B$ denotes the multiset over $X$ with $(A+B)(x):=A(x)+B(x)$,
$A-B$ is given by
$(A-B)(x):=A(x)\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{$\stackrel{{\scriptstyle\raisebox{-5.0pt}[0.0pt][0.0pt]{\huge$\cdot$}}}{{\raisebox{0.0pt}[0.0pt][0.0pt]{$-$}}}$}}B(x)=\mbox{max}(A(x)-B(x),0)$,
and for $k\mathbin{\in}\bbbn$ the multiset $k\cdot A$ is given by $(k\cdot
A)(x):=k\cdot A(x)$.

  * $\bullet$

The function $\emptyset\\!:X\rightarrow\bbbn$, given by $\emptyset(x):=0$ for
all $x\mathbin{\in}X$, is the _empty_ multiset over $X$.

  * $\bullet$

If $A$ is a multiset over $X$ and $Y\subseteq X$ then
$A\mathop{\upharpoonright}Y$ denotes the multiset over $Y$ defined by
$(A\mathop{\upharpoonright}Y)(x):=A(x)$ for all $x\mathbin{\in}Y$.

  * $\bullet$

The cardinality $|A|$ of a multiset $A$ over $X$ is given by $|A|:=\sum_{x\in
X}A(x)$.

  * $\bullet$

A multiset $A$ over $X$ is _finite_ iff $|A|<\infty$, i.e., iff the set
$\\{x\mid x\mathbin{\in}A\\}$ is finite.

Two multisets $A\\!:X\rightarrow\bbbn$ and $B\\!:Y\rightarrow\bbbn$ are
_extensionally equivalent_ iff $A\mathop{\upharpoonright}(X\cap
Y)=B\mathop{\upharpoonright}(X\cap Y)$, $A\mathop{\upharpoonright}(X\setminus
Y)=\emptyset$, and $B\mathop{\upharpoonright}(Y\setminus X)=\emptyset$. In
this paper we often do not distinguish extensionally equivalent multisets.
This enables us, for instance, to use $A\cup B$ even when $A$ and $B$ have
different underlying domains. With $\\{x,x,y\\}$ we will denote the multiset
over $\\{x,y\\}$ with $A(x)\mathbin{=}2$ and $A(y)\mathbin{=}1$, rather than
the set $\\{x,y\\}$ itself. A multiset $A$ with $A(x)\leq 1$ for all $x$ is
identified with the set $\\{x\mid A(x)=1\\}$.

Below we define place/transition systems as net structures with an initial
marking. In the literature we find slight variations in the definition of P/T
systems concerning the requirements for pre- and postsets of places and
transitions. In our case, we do allow isolated places. For transitions we
allow empty postsets, but require at least one preplace, thus avoiding
problems with infinite self-concurrency. Moreover, following [BD87], we
restrict attention to nets of _finite synchronisation_ , meaning that each
transition has only finitely many pre- and postplaces. Arc weights are
included by defining the flow relation as a function to the natural numbers.
For succinctness, we will refer to our version of a P/T system as a _net_.

###### Definition 2

  * A _net_ is a tuple $N=(S,T,F,M_{0})$ where

    * $\bullet$

$S$ and $T$ are disjoint sets (of _places_ and _transitions_),

    * $\bullet$

$F:(S\mathord{\times}T\mathrel{\cup}T\mathord{\times}S)\rightarrow\bbbn$ (the
_flow relation_ including _arc weights_), and

    * $\bullet$

$M_{0}:S\rightarrow\bbbn$ (the _initial marking_)

such that for all $t\mathbin{\in}T$ the set $\\{s\mid F(s,t)>0\\}$ is finite
and non-empty, and the set $\\{s\mid F(t,s)>0\\}$ is finite.

Graphically, nets are depicted by drawing the places as circles and the
transitions as boxes. For $x,y\mathbin{\in}S\cup T$ there are $F(x,y)$ arrows
(_arcs_) from $x$ to $y$. When a net represents a concurrent system, a global
state of this system is given as a _marking_ , a multiset of places, depicted
by placing $M(s)$ dots (_tokens_) in each place $s$. The initial state is
$M_{0}$. The system behaviour is defined by the possible moves between
markings $M$ and $M^{\prime}$, which take place when a finite multiset $G$ of
transitions _fires_. When firing a transition, tokens on preplaces are
consumed and tokens on postplaces are created, one for every incoming or
outgoing arc of $t$, respectively. Obviously, a transition can only fire if
all necessary tokens are available in $M$ in the first place. Definition 4
formalises this notion of behaviour.

###### Definition 3

Let $N\\!=\\!(S,T,F,M_{0})$ be a net and $x\mathbin{\in}S\cup T$.

  * The multisets ${\vphantom{x}}^{\bullet}x,~{}{x}^{\bullet}:S\cup T\rightarrow\bbbn$ are given by ${\vphantom{x}}^{\bullet}x(y)=F(y,x)$ and ${x}^{\bullet}(y)=F(x,y)$ for all $y\mathbin{\in}S\cup T$. If $x\in T$, the elements of ${\vphantom{x}}^{\bullet}x$ and ${x}^{\bullet}$ are called _pre-_ and _postplaces_ of $x$, respectively. These functions extend to multisets $X:S\cup T\rightarrow\bbbn$ as usual, by ${\vphantom{X}}^{\bullet}X:=\Sigma_{x\in S\cup T}X(x)\cdot{\vphantom{x}}^{\bullet}x$ and ${X}^{\bullet}:=\Sigma_{x\in S\cup T}X(x)\cdot{x}^{\bullet}$.

###### Definition 4

Let $N\mathbin{=}(S,T,F,M_{0})$ be a net, $G\in\bbbn^{T}\\!$, $G$ non-empty
and finite, and $M,M^{\prime}\in\bbbn^{S}\\!$.

  * $G$ is a _step_ from $M$ to $M^{\prime}$, written $M\stackrel{{\scriptstyle G}}{{\longrightarrow}}_{N}M^{\prime}$, iff

    * $\bullet$

${}^{\bullet}G\subseteq M$ ($G$ is _enabled_) and

    * $\bullet$

$M^{\prime}=(M-\mbox{${}^{\bullet}G$})+G^{\bullet}$.

We may leave out the subscript $N$ if clear from context. Extending the notion
to words $\sigma=t_{1}t_{2}\ldots t_{n}\in T^{*}$ we write
$M\stackrel{{\scriptstyle\sigma}}{{\longrightarrow}}M^{\prime}$ for

$\exists
M_{1},M_{2},\ldots,M_{n-1}.~{}M\\!\stackrel{{\scriptstyle\\{t_{1}\\}}}{{\longrightarrow}}\\!M_{1}\\!\stackrel{{\scriptstyle\\{t_{2}\\}}}{{\longrightarrow}}\\!M_{2}\cdots
M_{n-1}\\!\stackrel{{\scriptstyle\\{t_{n}\\}}}{{\longrightarrow}}\\!M^{\prime}\\!\\!.$

When omitting $\sigma$ or $M^{\prime}$ we always mean it to be existentially
quantified. When
$M_{0}\stackrel{{\scriptstyle\sigma}}{{\longrightarrow}}_{N}$, the word
$\sigma$ is called a _firing sequence_ of $N$. The set of all firing sequences
of $N$ is denoted by $\text{FS}(N)$.

Note that steps are (finite) multisets, thus allowing self-concurrency. Also
note that $M\mathrel{\hbox{$\mathop{\hbox
to25.14609pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip
2.5pt$\scriptstyle\\{t,u\\}$\hskip 2.5pt}}$}}$ implies
$M\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle
tu$\hskip 2.5pt}\hfil}}$}}$ and $M\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle
ut$\hskip 2.5pt}\hfil}}$}}$. We use the notation $t\in\sigma$ to indicate that
the transition $t$ occurs in the sequence $\sigma$, and $\sigma\leq\rho$ to
indicate that $\sigma$ is a prefix of the sequence $\rho$, i.e.
$\exists\mu.~{}\rho=\sigma\mu$.

##  3 Processes of place/transition systems

We now define processes of nets. A (GR-)process is essentially a conflict-
free, acyclic net together with a mapping function to the original net. It can
be obtained by unwinding the original net, choosing one of the alternatives in
case of conflict. The acyclic nature of the process gives rise to a notion of
causality for transition firings in the original net via the mapping function.
Conflicts present in the original net are represented by one net yielding
multiple processes, each representing one possible way to decide the
conflicts.

###### Definition 5

  * A pair $P=(\text{\fsc N},\pi)$ is a _(GR-)process_ of a net $N=(S,T,F,M_{0})$ iff

    * $\bullet$

$\text{\fsc N}=(\SS,\text{\fsc T},\text{\fsc F},\text{\fsc M}_{0})$ is a net,
satisfying

      * $-$

$\forall
s\in\SS.~{}|{\vphantom{s}}^{\bullet}s|\leq\\!1\\!\geq|{s}^{\bullet}|\wedge\,\text{\fsc
M}_{0}(s)=\left\\{\begin{array}[]{@{}l@{\quad}l@{}}1&\mbox{if
${\vphantom{s}}^{\bullet}s=\emptyset$}\\\
0&\mbox{otherwise,}\end{array}\right.$

      * $-$

F is acyclic, i.e. $\forall x\mathbin{\in}\SS\cup\text{\fsc
T}.~{}(x,x)\mathbin{\not\in}\text{\fsc F}^{+}$, where $\text{\fsc F}^{+}$ is
the transitive closure of $\\{(t,u)\mid F(t,u)>0\\}$,

      * $-$

and $\\{t\mid(t,u)\in\text{\fsc F}^{+}\\}$ is finite for all $u\in\text{\fsc
T}$.

    * $\bullet$

$\pi:\SS\cup\text{\fsc T}\rightarrow S\cup T$ is a function with
$\pi(\SS)\subseteq S$ and $\pi(\text{\fsc T})\subseteq T$, satisfying

      * $-$

$\pi(\text{\fsc M}_{0})=M_{0}$, i.e. $M_{0}(s)=|\pi^{-1}(s)\cap\text{\fsc
M}_{0}|$ for all $s\in S$, and

      * $-$

$\forall t\in\text{\fsc T},s\in
S.~{}F(s,\pi(t))=|\pi^{-1}(s)\cap{\vphantom{t}}^{\bullet}t|\wedge
F(\pi(t),s)=|\pi^{-1}(s)\cap{t}^{\bullet}|$.

$P$ is called _finite_ if T is finite.

The conditions for N ensure that a process is indeed a mapping from an
occurrence net as defined in [Pet77, GSW80] to the net $N$; hence we define
processes here in the classical way as in [GR83, BD87] (even though not
introducing occurrence nets explicitly).

A process is not required to represent a completed run of the original net. It
might just as well stop early. In those cases, some set of transitions can be
added to the process such that another (larger) process is obtained. This
corresponds to the system taking some more steps and gives rise to a natural
order between processes.

###### Definition 6

Let $P=((\SS,\text{\fsc T},\text{\fsc F},\text{\fsc M}_{0}),\pi)$ and
$P^{\prime}=((\SS^{\prime},\text{\fsc T}\,^{\prime},\text{\fsc
F}\,^{\prime},\text{\fsc M}_{0}^{\prime}),\pi^{\prime})$ be two processes of
the same net.

  * $\bullet$

$P^{\prime}$ is a _prefix_ of $P$, notation $P^{\prime}\leq P$, and $P$ an
_extension_ of $P^{\prime}$, iff $\SS^{\prime}\subseteq\SS$, $\text{\fsc
T}\,^{\prime}\subseteq\text{\fsc T}$, $\text{\fsc M}_{0}^{\prime}=\text{\fsc
M}_{0}$, $\text{\fsc F}\,^{\prime}=\text{\fsc
F}\mathop{\upharpoonright}(\SS^{\prime}\mathord{\times}\text{\fsc
T}\,^{\prime}\mathrel{\cup}\text{\fsc
T}\,^{\prime}\mathord{\times}\SS^{\prime})$ and
$\pi^{\prime}=\pi\mathop{\upharpoonright}(\SS^{\prime}\times\text{\fsc
T}\,^{\prime})$.

  * $\bullet$

A process of a net is said to be _maximal_ if it has no proper extension.

The requirements above imply that if $P^{\prime}\leq P$, $(x,y)\in\text{\fsc
F}^{+}$ and $y\in\SS^{\prime}\cup\text{\fsc T}\,^{\prime}$ then
$x\in\SS^{\prime}\cup\text{\fsc T}\,^{\prime}$. Conversely, any subset
$\text{\fsc T}\,^{\prime}\subseteq\text{\fsc T}$ satisfying
$(t,u)\in\text{\fsc F}^{+}\wedge u\in\text{\fsc T}\,^{\prime}\Rightarrow
t\in\text{\fsc T}\,^{\prime}$ uniquely determines a prefix of $P$.

Henceforth, we will write $P^{\prime}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle G$\hskip
2.5pt}\hfil}}$}}P$ with $G\mathbin{\in}\bbbn^{T}$ a finite and non-empty
multiset of transitions of the underlying net, if $P^{\prime}\mathbin{\leq}P$,
all transitions in $K:=\text{\fsc T}\setminus\text{\fsc T}\,^{\prime}$ are
maximal in T w.r.t. $\text{\fsc F}^{+}$, and $\pi(K)=G$, i.e.
$G(t)=|\pi^{-1}(t)\cap K|$ for all $t\in T$. As usual, we write
$P^{\prime}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip
2.5pt}\hfil}}$}}P$ instead of $P^{\prime}\mathrel{\hbox{$\mathop{\hbox
to18.70015pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip
2.5pt$\scriptstyle\\{a\\}$\hskip 2.5pt}}$}}P$ for singleton steps. Let
$\mathcal{P}_{0}(N)$ be the set of _initial processes_ of a net $N$: those
with an empty set of transitions. Now for each finite process $P$ of $N$,
having $n$ transitions, there is a sequence
$P_{0}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle
a_{1}$\hskip 2.5pt}\hfil}}$}}P_{1}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle
a_{2}$\hskip 2.5pt}\hfil}}$}}\ldots\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle
a_{n}$\hskip 2.5pt}\hfil}}$}}P_{n}$ with $P_{0}\in\mathcal{P}_{0}(N)$ and
$P_{n}=P$.

For $P=((\SS,\text{\fsc T},\text{\fsc F},\text{\fsc M}_{0}),\pi)$ a finite GR-
process of a net $N=(S,T,F,M_{0})$, we write $P^{\circ}$ for
$\\{s\mathbin{\in}\SS\mid\forall t\mathbin{\in}\text{\fsc T}.~{}\text{\fsc
F}(s,t)\mathbin{=}0\\}$, and $\widehat{P}$ for the marking
$\pi(P^{\circ})\in\bbbn^{S}$. The following observations describe a _step
bisimulation_ [GG01] between the above transition relation on the processes of
a net, and the one on its markings.

###### Observation 1

Let $N=(S,T,F,M_{0})$ be a net, $G\mathbin{\in}\bbbn^{T}$ non-empty and
finite, and $P,Q$ be finite GR-processes of $N$.

  * (a)

$\mathcal{P}_{0}(N)\neq\emptyset$ and if $P\mathbin{\in}\mathcal{P}_{0}$ then
$\widehat{P}=M_{0}$.

  * (b)

If $P\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle G$\hskip
2.5pt}\hfil}}$}}Q$ then $\widehat{P}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle G$\hskip
2.5pt}\hfil}}$}}\widehat{Q}$.

  * (c)

If $\widehat{P}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle G$\hskip
2.5pt}\hfil}}$}}M$ then there is a $Q$ with $P\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle G$\hskip
2.5pt}\hfil}}$}}Q$ and $\widehat{Q}=M$.

  * (d)

$\widehat{P}$ is _reachable_ in the sense that
$M_{0}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle$\hskip
2.5pt}\hfil}}$}}\widehat{P}$. (This follows from (a) and (b).)

Two processes $(\text{\fsc N},\pi)$ and $(\text{\fsc
N}\,^{\prime},\pi^{\prime})$ are _isomorphic_ iff there exists an isomorphism
$\phi$ from N to $\text{\fsc N}\,^{\prime}$ which respects the process
mapping, i.e. $\pi=\pi^{\prime}\circ\phi$. Here an isomorphism $\phi$ between
two nets $\text{\fsc N}=(\SS,\text{\fsc T},\text{\fsc F},\text{\fsc M}_{0})$
and $\text{\fsc N}\,^{\prime}=(\SS^{\prime},\text{\fsc
T}\,^{\prime},\text{\fsc F}\,^{\prime},\text{\fsc M}^{\prime}_{0})$ is a
bijection between their places and transitions such that $\text{\fsc
M}^{\prime}_{0}(\phi(s))=\text{\fsc M}_{0}(s)$ for all $s\in\SS$ and
$\text{\fsc F}\,^{\prime}(\phi(x),\phi(y))=\text{\fsc F}(x,y)$ for all
$x,y\in\SS\cup\text{\fsc T}$.

Next we formally introduce the swapping transformation and the resulting
equivalence notion on GR-processes from [BD87].

###### Definition 7

Let $P=((\SS,\text{\fsc T},\text{\fsc F},\text{\fsc M}_{0}),\pi)$ be a process
and let $p,q\in\SS$ with $(p,q)\notin\text{\fsc F}^{+}\cup(\text{\fsc
F}^{+})^{-1}$ and $\pi(p)=\pi(q)$.

  * Then $\mbox{swap}(P,p,q)$ is defined as $((\SS,\text{\fsc T},\text{\fsc F}\,^{\prime},\text{\fsc M}_{0}),\pi)$ with

$\text{\fsc F}\,^{\prime}(x,y)=\begin{cases}\text{\fsc F}(q,y)&\text{ iff
}x=p,\,y\in\text{\fsc T}\\\ \text{\fsc F}(p,y)&\text{ iff
}x=q,\,y\in\text{\fsc T}\\\ \text{\fsc F}(x,y)&\text{ otherwise. }\end{cases}$

###### Definition 8

  * $\bullet$

Two processes $P$ and $Q$ of the same net are _one step swapping equivalent_
($P\approx_{\mbox{s}}Q$) iff $\mbox{swap}(P,p,q)$ is isomorphic to $Q$ for
some places $p$ and $q$.

  * $\bullet$

We write $\approx_{\mbox{s}}^{*}$ for the reflexive and transitive closure of
$\approx_{\mbox{s}}$, and
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$
for the $\approx_{\mbox{s}}^{*}$-equivalence class of a finite process $P$.
The prefix relation $\leq$ between processes is lifted to such equivalence
classes by
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P^{\prime}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\leq\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$
iff $P^{\prime}\approx_{\mbox{s}}^{*}Q^{\prime}\leq Q\approx_{\mbox{s}}^{*}P$
for some $Q^{\prime},Q$.

  * $\bullet$

Two processes $P$ and $Q$ are _swapping equivalent_
($P\approx_{\mbox{s}}^{\infty}Q$) iff

$\begin{split}&{\downarrow(\\{\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P^{\prime}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\mid
P^{\prime}\leq P,~{}P^{\prime}~{}\mbox{finite}\\})}=\\\
&{\downarrow(\\{\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q^{\prime}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\mid
Q^{\prime}\leq Q,~{}Q^{\prime}~{}\mbox{finite}\\})}\end{split}$

where $\downarrow$ denotes prefix-closure under $\leq$.

  * $\bullet$

We call a $\approx_{\mbox{s}}^{\infty}$-equivalence class of processes a _BD-
process_, and write
${{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}_{\psscalebox{0.8}{\scriptscriptstyle\infty}}}$.

It is not hard to verify that if $P\approx_{\mbox{s}}^{*}Q\leq Q^{\prime}$
then $P\leq P^{\prime}\approx_{\mbox{s}}^{*}Q^{\prime}$ for some process
$P^{\prime}$. This implies that $\leq$ is a partial order on
$\approx_{\mbox{s}}^{*}$-equivalence classes of finite processes.
Alternatively, this conclusion follows from Theorem 4 in [GGS11].

Our definition of $\approx_{\mbox{s}}^{\infty}$ deviates from the definition
of $\equiv_{1}^{\infty}$ from [BD87] to make proofs easier later on. We
conjecture however that the two notions coincide.

Note that if $P\approx_{\mbox{s}}^{\infty}Q$ and $P$ is finite, then also $Q$
is finite. Moreover, for finite GR-processes $P$ and $Q$ we have
$P\approx_{\mbox{s}}^{\infty}Q$ iff $P\approx_{\mbox{s}}^{*}Q$. Thus, for a
finite GR-process $P$, we have
${{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}_{\psscalebox{0.8}{\scriptscriptstyle\infty}}}=\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$.
In that case we call
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$
a _finite_ BD-process.

The following observations are easy to check.

###### Observation 2

Let $P,Q,P^{\prime},Q^{\prime}$ be finite GR-processes of a net $N$.

  * (a)

If $P\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip
2.5pt}\hfil}}$}}Q$ and $P\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip
2.5pt}\hfil}}$}}Q^{\prime}$ then $Q\approx_{\mbox{s}}^{*}Q^{\prime}$.

  * (b)

If $P\approx_{\mbox{s}}^{*}Q$ and $P\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip
2.5pt}\hfil}}$}}P^{\prime}$ then $Q\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip
2.5pt}\hfil}}$}}Q^{\prime}$ for some $Q^{\prime}$ with
$P^{\prime}\approx_{\mbox{s}}^{*}Q^{\prime}$.

For GR-processes $P$ and $Q$ we write
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip
2.5pt}\hfil}}$}}\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$
if $P\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip
2.5pt}\hfil}}$}}Q^{\prime}$ for some
$Q^{\prime}\mathbin{\in}\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$.
By Observation 2(b) this implies that for any
$P^{\prime}\mathbin{\in}\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$
there is a
$Q^{\prime}\mathbin{\in}\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$
with $P^{\prime}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip
2.5pt}\hfil}}$}}Q^{\prime}$. By Observation 2(a), for any BD-process
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$
of a $N$ and any transition $a$ of $N$ there is at most one BD-process
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$
with
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip
2.5pt}\hfil}}$}}\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$.

We define a _BD-run_ as a more abstract and more general form of BD-process.
Like a BD-process, a BD-run is completely determined by its finite
approximations, which are finite BD-processes; however, a BD-run does not
require that these finite approximations are generated by a given GR-process.

###### Definition 9

Let $N$ be a net.

  * A _BD-run_ $\mathcal{R}$ of $N$ is a non-empty set of finite BD-processes of $N$ such that

    * $\bullet$

$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\leq\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\in\mathcal{R}\Rightarrow\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\in\mathcal{R}$
($\mathcal{R}$ is prefix-closed), and

    * $\bullet$

$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}},\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\in\mathcal{R}\Rightarrow\exists\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}U{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\in\mathcal{R}.~{}\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\leq\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}U{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\wedge\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\leq\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}U{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$
($\mathcal{R}$ is directed).

The class of finite BD-processes and the finite elements (in the set
theoretical sense) in the class of BD-runs are in bijective correspondence.
Every finite BD-run $\mathcal{R}$ must have a largest element, say
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$,
and the set of all prefixes of
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$
is $\mathcal{R}$. Conversely, the set of prefixes of a finite BD-process
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$
is a finite BD-run of which the largest element is again
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$.

We now define a canonical mapping from GR-processes to BD-runs.

###### Definition 10

Let $N$ be a net and $P$ a process thereof.

  * Then ${\it BD}(P):=\mathord{\downarrow}\\{\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P^{\prime}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\mid P^{\prime}\leq P,~{}P^{\prime}\text{ finite}\\}$.

###### Lemma 1

Let $N$ be a net and $P$ a process thereof.

Then ${\it BD}(P)$ is a BD-run.

###### Proof

See [GGS11, Lemma 1]. ∎

This immediately yields an injective function from BD-processes to BD-runs,
since by Definition 8, $P\approx_{\mbox{s}}^{\infty}Q$ iff ${\it BD}(P)={\it
BD}(Q)$. For countable nets (i.e. nets with countably many places and
transitions), this function is even a bijection.

###### Lemma 2

Let $N=(S,T,F,M_{0})$$N$ be a countable net and $\mathcal{R}$ a BD-run of $N$.

Then $\mathcal{R}$ is countable and there exists a process $P$ of $N$ such
that $\mathcal{R}={\it BD}(P)$.

###### Proof

Up to isomorphism there is only one GR-process $((\SS,\text{\fsc T},\text{\fsc
F},\text{\fsc M}_{0}),\pi)$ of $N$ with $|\text{\fsc T}|=0$. Furthermore, as
$N$ is countable, up to isomorphism there are only countably many with
$|\text{\fsc T}|=1$, countably many with $|\text{\fsc T}|=2$ and so on. Given
that isomorphic GR-processes are swapping equivalent, there are only countably
many BD-processes with any given finite number of transitions. Hence we can
enumerate all finite BD-processes of $N$. As $\mathcal{R}$ contains only
finite BD-processes of $N$, it, too, must be countable.

We construct a sequence of processes $P_{i}=((\SS_{i},\text{\fsc
T}_{i},\text{\fsc F}_{i},{\text{\fsc M}_{0}}),\pi_{i})$. We start with
$P_{0}=((\SS_{0},\emptyset,\emptyset,\text{\fsc M}_{0}),\pi_{0})$ where
$\SS_{0}:=\\{(s,i)\in S\times\bbbn\mid i<M_{0}(s)\\}$, $\text{\fsc
M}_{0}(s,i)=1$ and $\pi_{0}(s,i)=s$. As
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P_{0}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$
is a prefix of every finite BD-process of $N$,
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P_{0}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\in\mathcal{R}$.

We can enumerate the elements of $\mathcal{R}$ as $Q_{1},Q_{2},\ldots$. Now
given a process $P_{i}$ with
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P_{i}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\in\mathcal{R}$,
consider
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q_{i}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\in\mathcal{R}$.
As $\mathcal{R}$ is directed, there exists a
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P^{\prime}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\in\mathcal{R}$
with
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P_{i}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\leq\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P^{\prime}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\wedge\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q_{i}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\leq\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P^{\prime}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$
which is to say there exists some $P_{i+1}$ with $P_{i}\leq
P_{i+1}\approx_{\mbox{s}}^{*}P^{\prime}$, and some $Q^{\prime}$ with
$Q_{i}\leq Q^{\prime}\approx_{\mbox{s}}^{*}P^{\prime}$. We have
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P_{i+1}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}=\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P^{\prime}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\in\mathcal{R}$.

The limit $((\bigcup_{i=0}^{\infty}\SS_{i},\bigcup_{i=0}^{\infty}\text{\fsc
T}_{i},\bigcup_{i=0}^{\infty}\text{\fsc F}_{i},\text{\fsc
M}_{0}),\bigcup_{i=0}^{\infty}\pi_{i})$ of the $P_{i}$ is the $P$ we had to
find. We need to show that $\mathcal{R}={\it BD}(P)$.

Take any element
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q_{i}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$
of $\mathcal{R}$. Per construction,
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q_{i}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\leq\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P_{i+1}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$
and $P_{i+1}\leq P$, so
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q_{i}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\in{\it
BD}(P_{i})$. Hence $\mathcal{R}\subseteq{\it BD}(P)$.

Now take any
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\in{\it
BD}(P)=\mathord{\downarrow}\\{\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P^{\prime}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\mid
P^{\prime}\leq P,P^{\prime}\text{ finite}\\}$. Then there exist some finite
$Q^{\prime}$ such that
${\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\leq\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q^{\prime}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}}\wedge{Q^{\prime}\leq
P}$. The process $Q^{\prime}$ has finitely many transitions. Hence there
exists some $i$ such that all of these transitions occur in $P_{i}$ and as
$Q^{\prime}\leq P$ then also $Q^{\prime}\leq P_{i}$. Since
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P_{i}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\in\mathcal{R}$
and $\mathcal{R}$ is prefix closed, we have
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q^{\prime}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\in\mathcal{R}$
and
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\in\mathcal{R}$.
∎

Lemma 2 does not hold for uncountable nets, as witnessed by the counterexample
in Figure 3. This net $N$ has a transition $t$ for each real number
$t\mathbin{\in}\bbbr$. Each such transition has a private preplace $s_{t}$
with $M_{0}(s_{t})=1$ and $F(s_{t},t)=1$, which ensures that $t$ can fire only
once. Furthermore there is one shared place $s$ with $M_{0}(s)=2$ and a loop
$F(s,t)=F(t,s)=1$ for each transition $t$. There are no other places,
transitions or arcs besides the ones mentioned above.

Each GR-process of $N$, and hence also each BD-process, has only countably
many transitions. Yet, any two GR-processes firing the same finite set of
transitions of $N$ are swapping equivalent, and the set of all finite BD-
processes of $N$ constitutes a single BD-run involving all transitions.

0.9 0.7

$0$

$1$

2$\cdots$2$\cdots$2$\cdots$2$\cdots$2$\cdots$2$\cdots$

Figure 3: A net with no maximal GR-process, but with a maximal BD-run.

We now show that the mapping BD respects the ordering of processes.

###### Lemma 3

Let $N$ be a net, and $P$ and $P^{\prime}$ two GR-processes of $N$.

If $P\leq P^{\prime}$ then ${\it BD}(P)\subseteq{\it BD}(P^{\prime})$.

$\begin{array}[]{@{}l@{\hspace{23pt}}l<EMAIL_ADDRESS>23.0&P\leq P^{\prime}\Rightarrow\hfil\hskip 23.0\\\ \hfil\hskip 23.0&\\{Q\mid
Q\leq P,\,Q\text{ finite}\\}\subseteq\\{Q^{\prime}\mid Q^{\prime}\leq
P^{\prime},\,Q^{\prime}\text{ finite}\\}\Rightarrow\hfil\hskip 23.0\\\
\hfil\hskip
23.0&\\{\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\mid
Q\leq P,\,Q\text{
finite}\\}\subseteq\\{\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q^{\prime}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\mid
Q^{\prime}\leq P^{\prime},\,Q^{\prime}\text{ finite}\\}\Rightarrow\hfil\hskip
23.0\\\ \hfil\hskip
23.0&\mathord{\downarrow}\\{\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\mid
Q\leq P,\,Q\text{
finite}\\}\subseteq\mathord{\downarrow}\\{\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q^{\prime}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\mid
Q^{\prime}\leq P^{\prime},\,Q^{\prime}\text{ finite}\\}\Rightarrow\hfil\hskip
23.0\\\ \hfil\hskip 23.0&{\it BD}(P)\subseteq{\it BD}(P^{\prime}).\hfil\hskip
23.0&\mbox{\squareforqed}\end{array}$

##  4 Conflicts in place/transition systems

We recall the canonical notion of conflict introduced in [Gol86].

###### Definition 11

Let $N\mathbin{=}(S,T,F,M_{0})$ be a net and $M\in\bbbn^{S}\\!$.

  * $\bullet$

A finite, non-empty multiset $G\in\bbbn^{T}$ is in _(semantic) conflict_ in
$M$ iff
$(\forall t\in G.~{}M\mathrel{\hbox{$\mathop{\hbox
to25.94823pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle
G\mathop{\upharpoonright}\\{t\\}$\hskip 2.5pt}}$}})\wedge\neg
M\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle G$\hskip
2.5pt}\hfil}}$}}$.

  * $\bullet$

$N$ is _(semantic) conflict-free_ iff no finite, non-empty multiset
$G\in\bbbn^{T}$ is in semantic conflict in any $M$ with
$M_{0}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle$\hskip
2.5pt}\hfil}}$}}M$.

  * $\bullet$

$N$ is _binary-conflict--free_ iff no multiset $G\in\bbbn^{T}$ with $|G|=2$
is in semantic conflict in any $M$ with $M_{0}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle$\hskip
2.5pt}\hfil}}$}}M$.

  * Remark:

In a net $(S,T,F,M_{0})$ with $S=\\{s\\}$, $T=\\{t,u\\}$, $M_{0}(s)=1$ and
$F(s,t)=F(s,u)=1$, the multiset $\\{t,t\\}$ is not enabled in $M_{0}$. For
this reason the multiset $\\{t,t,u\\}$ does not count as being in conflict in
$M_{0}$, even though it is not enabled. However, its subset $\\{t,u\\}$ is in
conflict.

###### Lemma 4

Let $N\mathbin{=}(S,T,F,M_{0})$ be a binary-conflict--free net,
$a,b\mathbin{\in}T$ with $a\mathbin{\neq}b$, and $P,P^{\prime},Q$ be finite
GR-processes of $N$.

If $P\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip
2.5pt}\hfil}}$}}P^{\prime}$ and $P\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle b$\hskip
2.5pt}\hfil}}$}}Q$ then $\widehat{P}\mathrel{\hbox{$\mathop{\hbox
to25.31538pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip
2.5pt$\scriptstyle\\{a,b\\}$\hskip 2.5pt}}$}}$ and $\exists
Q^{\prime}.~{}P^{\prime}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle b$\hskip
2.5pt}\hfil}}$}}Q^{\prime}\wedge\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip
2.5pt}\hfil}}$}}\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q^{\prime}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$.

###### Proof

Suppose $P\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip
2.5pt}\hfil}}$}}P^{\prime}$ and $P\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle b$\hskip
2.5pt}\hfil}}$}}Q$ with $a\neq b$. Then $M_{0}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle$\hskip
2.5pt}\hfil}}$}}\widehat{P}$ by Observation 1(d). Moreover,
$\widehat{P}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip
2.5pt}\hfil}}$}}\widehat{P}^{\prime}$ and
$\widehat{P}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle b$\hskip
2.5pt}\hfil}}$}}\widehat{Q}$ by Observation 1(b). Hence, as $N$ is binary-
conflict--free, $\widehat{P}\mathrel{\hbox{$\mathop{\hbox
to25.31538pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip
2.5pt$\scriptstyle\\{a,b\\}$\hskip 2.5pt}}$}}$. Therefore
$\widehat{P}^{\prime}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle b$\hskip
2.5pt}\hfil}}$}}M$ for some $M$. Using Observation 1(c), there exists a GR-
process $Q^{\prime}$ with $P^{\prime}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle b$\hskip
2.5pt}\hfil}}$}}Q^{\prime}$ and $\widehat{Q}^{\prime}=M$. This $Q^{\prime}$
can be chosen in such a way that the $b$-transition uses no tokens that are
produced by the preceding $a$ transition. We then obtain that
$P\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle b$\hskip
2.5pt}\hfil}}$}}Q^{\prime\prime}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip
2.5pt}\hfil}}$}}Q^{\prime}$ for some $Q^{\prime\prime}$. By Observation 2(a),
$Q\approx_{\mbox{s}}^{*}Q^{\prime\prime}$, and hence
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip
2.5pt}\hfil}}$}}\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q^{\prime}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$.
∎

We proposed in [GGS11] a class of P/T systems where the structural definition
of conflict in terms of shared preplaces, as often used in Petri net theory,
matches the semantic definition of conflict as given above. We called this
class of nets _structural conflict nets_. For a net to be a structural
conflict net, we require that two transitions sharing a preplace will never
occur both in one step.

###### Definition 12

Let $N\mathbin{=}(S,T,F,M_{0})$ be a net.

  * $N$ is a _structural conflict net_ iff $\forall t,u.~{}(M_{0}\mathrel{\hbox{$\mathop{\hbox to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle$\hskip 2.5pt}\hfil}}$}}\;\mathrel{\hbox{$\mathop{\hbox to25.14609pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox{\vrule height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle\\{t,u\\}$\hskip 2.5pt}}$}})\Rightarrow{\vphantom{t}}^{\bullet}t\cap{\vphantom{u}}^{\bullet}u=\emptyset$.

Note that this excludes self-concurrency from the possible behaviours in a
structural conflict net: as in our setting every transition has at least one
preplace, $t=u$ implies
${\vphantom{t}}^{\bullet}t\cap{\vphantom{u}}^{\bullet}u\neq\emptyset$. Also
note that in a structural conflict net a non-empty, finite multiset $G$ is in
conflict in a marking $M$ iff $G$ is a set and two distinct transitions in $G$
are in conflict in $M$. Hence a structural conflict net is conflict-free if
and only if it is binary-conflict--free. Moreover, two transitions enabled in
$M$ are in (semantic) conflict iff they share a preplace.

##  5 A conflict-free net has exactly one maximal run

In this section, we recapitulate results from [BD87], giving an alternative
characterisation of runs of a net in terms of firing sequences. We use an
adapted notation and terminology and a different treatment of infinite runs,
as in [GGS11]. As a main result of the present paper, we then prove in this
setting that a conflict-free net has exactly one maximal run. In the following
section, this result will be transferred to BD-processes.

The behaviour of a net can be described not only by its processes, but also by
its firing sequences. The imposed total order on transition firings abstracts
from information on causal dependence, or concurrency, between transition
firings. To retrieve this information we introduce an _adjacency_ relation on
firing sequences, recording which interchanges of transition occurrences are
due to semantic independence of transitions. Hence adjacent firing sequences
represent the same run of the net. We then define _FS-runs_ in terms of the
resulting equivalence classes of firing sequences.

###### Definition 13

Let $N=(S,T,F,M_{0})$ be a net, and $\sigma,\rho\in\text{FS}(N)$.

  * $\bullet$

$\sigma$ and $\rho$ are _adjacent_ , $\sigma\leftrightarrow\rho$, iff
$\sigma=\sigma_{1}tu\sigma_{2}$, $\rho=\sigma_{1}ut\sigma_{2}$ and
$M_{0}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip
2.5pt$\scriptstyle\sigma_{1}$\hskip
2.5pt}\hfil}}$}}\mathrel{\hbox{$\mathop{\hbox
to25.14609pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip
2.5pt$\scriptstyle\\{t,u\\}$\hskip 2.5pt}}$}}$.

  * $\bullet$

We write
$\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}$
for the reflexive and transitive closure of
$\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}$,
and $[\sigma]$ for the
$\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}$-equivalence
class of a firing sequence $\sigma$.

Note that
$\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}$-related
firing sequences contain the same (finite) multiset of transition occurrences.
When writing
$\sigma\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\rho$
we implicitly claim that $\sigma,\rho\in\text{FS}(N)$. Furthermore
$\sigma\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\rho\wedge\sigma\mu\in\text{FS}(N)$
implies
$\sigma\mu\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\rho\mu$
for all $\mu\in T^{*}$.

The following definition introduces the notion of _partial_ FS-run which is a
formalisation of the intuitive concept of a finite, partial run of a net.

###### Definition 14

Let $N$ be a net and $\sigma,\rho\in\text{FS}(N)$.

  * $\bullet$

A _partial FS-run_ of $N$ is an
$\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}$-equivalence
class of firing sequences.

  * $\bullet$

A partial FS-run $[\sigma]$ is a _prefix_ of another partial FS-run $[\rho]$,
notation $[\sigma]\leq[\rho]$, iff
$\exists\mu.~{}\sigma\leq\mu\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\\!\rho$.

Note that
$\sigma^{\prime}\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\\!\sigma\leq\mu$
implies
$\exists\mu^{\prime}.~{}\sigma^{\prime}\leq\mu^{\prime}\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\mu$;
thus the notion of prefix is well-defined, and a partial order.

Similar to the construction of BD-runs out of finite BD-processes, the
following concept of an FS-run extends the notion of a partial FS-run to
possibly infinite runs, in such a way that an FS-run is completely determined
by its finite approximations.

###### Definition 15

Let $N$ be a net.

  * An _FS-run_ of $N$ is a non-empty, prefix-closed and directed set of partial FS-runs of $N$.

There is a bijective correspondence between partial FS-runs and the finite
elements in the class of FS-runs, just as in the case of BD-runs in Section 3.
Much more interesting however is the following bijective correspondence
between BD-runs and FS-runs.

###### Theorem 5.1

There exists a bijective function $\Pi$ from FS-runs to BD-runs such that
$\Pi(\mathcal{R})\subseteq\Pi(\mathcal{R}^{\prime})$ iff
$\mathcal{R}\subseteq\mathcal{R}^{\prime}$.

###### Proof

See [GGS11], in particular the remarks at the end of Section 5. ∎

We use the relations between firing sequences up to
$\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}$
and finite GR-processes up to $\approx_{\mbox{s}}^{*}$, as examined in [BD87],
to establish the following variant of Lemma 4, which we will need in the next
section.

###### Lemma 5

Let $N\mathbin{=}(S,T,F,M_{0})$ be a structural conflict net,
$a,b\mathbin{\in}T$ with $a\mathbin{\neq}b$, $\mathcal{R}$ be a BD-run of $N$,
and $P,P^{\prime},Q\in^{2}\mathcal{R}$. (Here $X\mathbin{\in^{2}}Z$ stands for
$\exists Y.~{}X\mathbin{\in}Y\mathbin{\in}Z$.)

If $P\\!\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip
2.5pt}\hfil}}$}}\\!P^{\prime}$ and $P\\!\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle b$\hskip
2.5pt}\hfil}}$}}\\!Q$ then $\widehat{P}\\!\mathrel{\hbox{$\mathop{\hbox
to25.31538pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip
2.5pt$\scriptstyle\\{a,b\\}$\hskip 2.5pt}}$}}$ and $\exists
Q^{\prime}\\!\in^{2}\\!\mathcal{R}.~{}P^{\prime}\\!\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle b$\hskip
2.5pt}\hfil}}$}}\\!Q^{\prime}\wedge\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\\!\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip
2.5pt}\hfil}}$}}\\!\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q^{\prime}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$.

###### Proof

Suppose $P\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip
2.5pt}\hfil}}$}}P^{\prime}$ and $P\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle b$\hskip
2.5pt}\hfil}}$}}Q$ with $a\neq b$. Then $M_{0}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle$\hskip
2.5pt}\hfil}}$}}\widehat{P}$ by Observation 1(d). Let $\sigma\in T^{*}$ be
such that $M_{0}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip
2.5pt$\scriptstyle\sigma$\hskip 2.5pt}\hfil}}$}}\widehat{P}$. As runs are
directed, there is a finite BD-process
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}U{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\in\mathcal{R}$
with
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P^{\prime}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\leq\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}U{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$
and
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\leq\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}U^{\prime}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$.
Hence there must be a sequence $P^{\prime}=P_{1}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle
a_{1}$\hskip 2.5pt}\hfil}}$}}P_{2}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle
a_{2}$\hskip 2.5pt}\hfil}}$}}\ldots\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle
a_{k}$\hskip 2.5pt}\hfil}}$}}P_{k+1}$ with
$P_{k+1}\in\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}U{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$,
and, similarly, a sequence $Q=Q_{1}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle
b_{1}$\hskip 2.5pt}\hfil}}$}}Q_{2}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle
b_{2}$\hskip 2.5pt}\hfil}}$}}\ldots\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle
b_{\ell}$\hskip 2.5pt}\hfil}}$}}Q_{\ell+1}$ with
$Q_{\ell+1}\in\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}U{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$.
Let $a_{0}:=a$ and $\rho:=a_{0}a_{1}\cdots a_{k}$; likewise let $b_{0}:=b$ and
$\mu:=b_{0}b_{1}\cdots b_{\ell}$. By Theorem 3 in [GGS11] it follows that
$\sigma\rho,\sigma\mu\in\text{FS}(N)$ and
$\sigma\rho\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\sigma\mu$.
By Definition 13, $\sigma\rho$ and $\sigma\mu$ must contain the same multiset
of transitions. So $b=a_{h}$ for some $1\leq h\leq k$; we take $h$ minimal, so
that $b\neq a_{j}$ for $0\leq j<h$.

Let $Q^{\prime}_{h}:=P_{h+1}$. Since $P_{h+1}\leq P_{k+1}\in^{2}\mathcal{R}$
and $\mathcal{R}$ is prefix-closed, we have
$Q^{\prime}_{h}\in^{2}\mathcal{R}$. Working our way down from $h\mathord{-}1$
to $0$, we construct for any $j$ with $0\leq j<h$ a
$Q^{\prime}_{j}\in^{2}\mathcal{R}$ with $P_{j}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle b$\hskip
2.5pt}\hfil}}$}}Q^{\prime}_{j}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle
a_{j}$\hskip 2.5pt}\hfil}}$}}Q^{\prime}_{j+1}$. Suppose we already have
$Q^{\prime}_{j+1}$. Then $P_{j}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle
a_{j}$\hskip 2.5pt}\hfil}}$}}P_{j+1}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle b$\hskip
2.5pt}\hfil}}$}}Q^{\prime}_{j+1}$.

Somewhere in the sequence
$\sigma\rho=\nu_{1}\leftrightarrow\nu_{2}\leftrightarrow\cdots\leftrightarrow\nu_{n}=\sigma\mu$
the transitions $a_{j}$ and $b$ must be exchanged, i.e.
$\nu_{i}=\nu^{\prime}a_{j}b\nu^{\prime\prime}\leftrightarrow\nu^{\prime}ba_{j}\nu^{\prime\prime}=\nu_{i+1}$.
Thus there is a marking $M$ with $M_{0}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip
2.5pt$\scriptstyle\nu^{\prime}$\hskip
2.5pt}\hfil}}$}}M\mathrel{\hbox{$\mathop{\hbox
to27.19157pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip
2.5pt$\scriptstyle\\{a_{j},b\\}$\hskip 2.5pt}}$}}$. Since $N$ is a structural
conflict net,
${\vphantom{a_{j}}}^{\bullet}a_{j}\cap{\vphantom{b}}^{\bullet}b=\emptyset$.
This immediately yields a $Q^{\prime}_{j}$ with
$P_{j}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle b$\hskip
2.5pt}\hfil}}$}}Q^{\prime}_{j}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle
a_{j}$\hskip 2.5pt}\hfil}}$}}Q^{\prime}_{j+1}$. Since
$Q^{\prime}_{j+1}\in^{2}\mathcal{R}$ and $\mathcal{R}$ is prefix-closed, we
have $Q^{\prime}_{j}\in^{2}\mathcal{R}$.

Finally, let $Q^{\prime}:=Q^{\prime}_{1}$. Then
$P^{\prime}\mathop{=}P_{1}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle b$\hskip
2.5pt}\hfil}}$}}Q^{\prime}_{1}\mathop{=}Q^{\prime}$ and
$P\mathop{=}P_{0}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle b$\hskip
2.5pt}\hfil}}$}}Q^{\prime}_{0}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip
2.5pt}\hfil}}$}}Q^{\prime}_{1}$. Observation 2(a) yields
$Q\approx_{\mbox{s}}^{*}Q^{\prime}_{0}$. Hence
$\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip
2.5pt}\hfil}}$}}\mathop{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q^{\prime}{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}}$.
∎

We now show that a conflict-free net has exactly one maximal run. As we have a
bijective correspondence, it does not matter which notion of run we use here
(FS-run or BD-run). We prove an even stronger result, using binary-
conflict--free instead of conflict-free. In preparation we need the following
lemmas.

###### Lemma 6

Let $N=(S,T,F,M_{0})$ be a binary-conflict--free net, $\sigma t,\sigma
u\mathbin{\in}\text{FS}(N)$ with $t,u\mathbin{\in}T$, and $t\mathbin{\neq}u$.

Then $\sigma tu,\sigma ut\in\text{FS}(N)$ and $\sigma
tu\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\sigma
ut$.

###### Proof

As we have unlabelled transitions, $\sigma$ leads to a unique marking. From
$M_{0}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle\sigma
t$\hskip 2.5pt}\hfil}}$}}{}\wedge M_{0}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle\sigma
u$\hskip 2.5pt}\hfil}}$}}$ we thus have that an $M_{1}$ exists with
$M_{0}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip
2.5pt$\scriptstyle\sigma$\hskip 2.5pt}\hfil}}$}}{}M_{1}\wedge
M_{1}{\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle t$\hskip
2.5pt}\hfil}}$}}}\wedge M_{1}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip 2.5pt$\scriptstyle u$\hskip
2.5pt}\hfil}}$}}$. Due to binary-conflict--freeness then also
$M_{1}\mathrel{\hbox{$\mathop{\hbox
to25.14609pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip
2.5pt$\scriptstyle\\{t,u\\}$\hskip 2.5pt}}$}}$. Hence
$M_{0}\mathrel{\hbox{$\mathop{\hbox
to15.00002pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox
to15.00002pt{\hfil\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip
2.5pt$\scriptstyle\sigma$\hskip 2.5pt}\hfil}}$}}\mathrel{\hbox{$\mathop{\hbox
to25.14609pt{$\mathord{-}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{-}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}\limits^{\hbox{\vrule
height=6.45831pt,depth=4.30554pt,width=0.0pt\hskip
2.5pt$\scriptstyle\\{t,u\\}$\hskip 2.5pt}}$}}$, so $\sigma tu,\sigma
ut\in\text{FS}(N)$ and $\sigma
tu\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\sigma
ut$. ∎

###### Lemma 7

Let $N=(S,T,F,M_{0})$ be a binary-conflict--free net, $\sigma
t,\sigma\rho\mathbin{\in}\text{FS}(N)$ with $t\mathbin{\in}T$, $\sigma,\rho\in
T^{*}$, and $t\mathbin{\notin}\rho$.

Then $\sigma t\rho,\sigma\rho t\in\text{FS}(N)$ and $\sigma
t\rho\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\sigma\rho
t$.

###### Proof

Via induction on the length of $\rho$.

If $\rho\mathbin{=}\epsilon$, $\sigma t\in\text{FS}(N)$ trivially implies
$\sigma\epsilon t,\sigma t\epsilon\in\text{FS}(N)$ and $\sigma\epsilon
t\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\sigma
t\epsilon$.

For the induction step take $\rho\mathbin{:=}u\mu$ (with $u\neq t$). With
$\sigma t,\sigma u\in\text{FS}(N)$ and Lemma 6 also $\sigma ut\in\text{FS}(N)$
and $\sigma
tu\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\sigma
ut$. Together with $\sigma u\mu\in\text{FS}(N)$, the induction assumption then
gives us $\sigma ut\mu\in\text{FS}(N)$ and $\sigma
ut\mu\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\sigma
u\mu t=\sigma\rho t$. With $\sigma
ut\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\sigma
tu$ also $\sigma
ut\mu\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\sigma
tu\mu=\sigma t\rho$ and $\sigma\rho t,\,\sigma t\rho\in\text{FS}(N)$. ∎

###### Lemma 8

Let $N=(S,T,F,M_{0})$ be a binary-conflict--free net,
$\sigma,\rho_{1},\rho_{2}\in T^{*}$, $t\in T$, $t\notin\rho_{1}$.

If $\sigma t\in\text{FS}(N)\wedge\sigma\rho_{1}t\rho_{2}\in\text{FS}(N)$ then
$\sigma t\rho_{1}\rho_{2}\in\text{FS}(N)\wedge\sigma
t\rho_{1}\rho_{2}\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\sigma\rho_{1}t\rho_{2}$.

###### Proof

Applying Lemma 7 with $\sigma
t\mathbin{\in}\text{FS}(N)\wedge\sigma\rho_{1}\mathbin{\in}\text{FS}(N)$ we
get $\sigma t\rho_{1}\mathbin{\in}\text{FS}(N)\wedge\sigma
t\rho_{1}\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\sigma\rho_{1}t$.
Since $\sigma\rho_{1}t\rho_{2}\in\text{FS}(N)$ the latter yields $\sigma
t\rho_{1}\rho_{2}\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\sigma\rho_{1}t\rho_{2}$
and thus $\sigma t\rho_{1}\rho_{2}\in\text{FS}(N)$. ∎

###### Lemma 9

Let $N$ be a binary-conflict--free net.

If $\sigma,\sigma^{\prime}\mathbin{\in}\text{FS}(N)$ then
$\exists\mu,\mu^{\prime}.~{}\sigma\mu\mathbin{\in}\text{FS}(N)\wedge\sigma^{\prime}\mu^{\prime}\in\text{FS}(N)\wedge\sigma\mu\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\sigma^{\prime}\mu^{\prime}$.

###### Proof

Via induction on the length of $\sigma$.

If $\sigma=\epsilon$ we take $\mu=\sigma^{\prime}$ and
$\mu^{\prime}=\epsilon$.

For the induction step we start with

$\sigma,\sigma^{\prime}\in\text{FS}(N)\Rightarrow\exists\mu,\mu^{\prime}.~{}\sigma\mu\in\text{FS}(N)\wedge\sigma^{\prime}\mu^{\prime}\in\text{FS}(N)\wedge\sigma\mu\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\sigma^{\prime}\mu^{\prime}$

and need to show that

$\sigma
t,\sigma^{\prime}\in\text{FS}(N)\Rightarrow\exists\bar{\mu},\bar{\mu}^{\prime}.~{}\sigma
t\bar{\mu}\in\text{FS}(N)\wedge\sigma^{\prime}\bar{\mu}^{\prime}\in\text{FS}(N)\wedge\sigma
t\bar{\mu}\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\sigma^{\prime}\bar{\mu}^{\prime}\text{~{}.}$

If $t\mathbin{\in}\mu$, $\mu$ must be of the form $\mu_{1}t\mu_{2}$ with
$t\notin\mu_{1}$. We then take $\bar{\mu}:=\mu_{1}\mu_{2}$ and
$\bar{\mu}^{\prime}:=\mu^{\prime}$. By Lemma 8 we find $\sigma
t\mu_{1}\mu_{2}\in\text{FS}(N)$, i.e. $\sigma t\bar{\mu}\in\text{FS}(N)$.
$\sigma^{\prime}\bar{\mu}^{\prime}\in\text{FS}(N)$ is already contained in the
induction assumption. Per Lemma 8 $\sigma t\bar{\mu}=\sigma
t\mu_{1}\mu_{2}\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\sigma\mu_{1}t\mu_{2}=\sigma\mu$.
From the induction assumption we obtain
$\sigma\mu\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\sigma^{\prime}\mu^{\prime}=\sigma^{\prime}\bar{\mu}^{\prime}$.

If $t\mathbin{\notin}\mu$, we take $\bar{\mu}:=\mu$ and
$\bar{\mu}^{\prime}:=\mu^{\prime}t$. By Lemma 7 we find that $\sigma
t\mu,\sigma\mu t\in\text{FS}(N)$, i.e. also $\sigma
t\bar{\mu}\in\text{FS}(N)$. From $\sigma\mu t\in\text{FS}(N)$ and
$\sigma\mu\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\sigma^{\prime}\mu^{\prime}$
follows that $\sigma^{\prime}\mu^{\prime}t\in\text{FS}(N)$, i.e.
$\sigma^{\prime}\bar{\mu}^{\prime}\in\text{FS}(N)$. Also by Lemma 7 we find
$\sigma t\bar{\mu}=\sigma
t\mu\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\sigma\mu
t$. From the induction assumption we obtain $\sigma\mu
t\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\sigma^{\prime}\mu^{\prime}t=\sigma^{\prime}\bar{\mu}^{\prime}$.
∎

###### Theorem 5.2

Let $N$ be a binary-conflict--free net.

There is exactly one maximal FS-run of $N$.

###### Proof

Let $\mathcal{R}=\\{[\sigma]\mid\sigma\text{ is a finite firing sequence of
}N\\}$. We claim that $\mathcal{R}$ is said maximal FS-run of $N$.

First we show that $\mathcal{R}$ is prefix closed and directed, and thus
indeed an FS-run.

Take any $[\rho]\leq[\sigma]\in\mathcal{R}$. Then by definition of $\leq$,
$\exists\nu.~{}\rho\leq\nu\wedge\nu\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\sigma$.
We need to show that $[\rho]\in\mathcal{R}$, i.e. that $\rho$ is a firing
sequence of $N$. Since $\sigma$ is a firing sequence of $N$ and
$\nu\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\sigma$,
$\nu$ is also a firing sequence of $N$. Together with $\rho\leq\nu$ follows
that $\rho$, too, is a firing sequence of $N$. Thus $\mathcal{R}$ is prefix
closed.

To show directedness, let $[\sigma],[\rho]\in\mathcal{R}$. We need to show
that
$\exists[\nu]\mathbin{\in}\mathcal{R}.~{}[\sigma]\leq[\nu]\linebreak[3]\wedge[\rho]\leq[\nu]$,
or with the definitions of $\leq$ and $[~{}]$ expanded,
$\exists\nu.~{}(\,\exists\alpha.~{}\sigma\leq\alpha\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\nu\linebreak[3]\wedge\,\exists\beta.~{}\rho\leq\beta\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\nu)$.
We now apply Lemma 9 to $\sigma,\rho\in\text{FS}(N)$, obtaining $\mu$ and
$\mu^{\prime}$ as mentioned in that lemma, and take $\alpha=\sigma\mu$ and
$\beta=\rho\mu^{\prime}$. Then Lemma 9 gives us
$\alpha\mathrel{\,\,\rput(0.0pt,2.84526pt){\psscalebox{-0.8}{\leftrightarrow}}\,\,}^{*}\beta$
and we take $\nu=\alpha$. Thus $\mathcal{R}$ is directed.

Finally we show that $\mathcal{R}$ is maximal. Take any run
$\mathcal{R}^{\prime}$ of $N$. Then $\mathcal{R}^{\prime}\subseteq\mathcal{R}$
by definition of $\mathcal{R}$, hence $\mathcal{R}$ is maximal. ∎

##  6 BD-processes fit structural conflict nets

In this section we show that BD-processes are adequate as abstract processes
for the subclass of structural conflict nets.

In [GGS11] we have shown that a semantic conflict in a structural conflict net
always gives rise to multiple maximal GR-processes even up to swapping
equivalence.

###### Theorem 6.1

Let $N$ be a structural conflict net.

If $N$ has only one maximal GR-process up to $\approx_{\mbox{s}}^{\infty}$
then $N$ is conflict-free.

###### Proof

Corollary 1 from [GGS11]. ∎

We conjectured in [GGS11] that, for countable nets, also the reverse direction
holds, namely that a countable conflict-free structural conflict net has
exactly one maximal GR-process up to $\approx_{\mbox{s}}^{\infty}$.

In Section 5 we have already shown that a corresponding result holds for runs
instead of processes. We will now transfer this result to BD-processes, and
hence prove the conjecture.

We proceed by investigating three notions of maximality for BD-processes; they
will turn out to coincide for structural conflict nets.

###### Definition 16

  * •

A BD-process
${{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}_{\psscalebox{0.8}{\scriptscriptstyle\infty}}}$
is _weakly maximal_ (or a maximal GR-process up to
$\approx_{\mbox{s}}^{\infty}$), iff some
$P^{\prime}\mathbin{\in}{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}_{\psscalebox{0.8}{\scriptscriptstyle\infty}}}$
is maximal (in the GR-process sense).

  * •

A BD-process
${{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}_{\psscalebox{0.8}{\scriptscriptstyle\infty}}}$
is _maximal_ iff $\forall
P^{\prime}\in{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}_{\psscalebox{0.8}{\scriptscriptstyle\infty}}}\,\,\forall
Q.~{}(P^{\prime}\leq Q\Rightarrow P^{\prime}\approx_{\mbox{s}}^{\infty}Q)$.

  * •

A BD-process
${{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}_{\psscalebox{0.8}{\scriptscriptstyle\infty}}}$
is _run-maximal_ iff the BD-run ${\it BD}(P)$ is maximal.

The first notion is the simplest way of inheriting the notion of maximality of
GR-process by BD-processes, whereas the last one inherits the notion of
maximality from BD-runs. The middle notion is the canonical notion of
maximality with respect to a natural order on BD-process, defined below.

###### Definition 17

Let $N$ be a net.

We define a relation $\preceq$ between BD-processes, via

${{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}_{\psscalebox{0.8}{\scriptscriptstyle\infty}}}\preceq{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}_{\psscalebox{0.8}{\scriptscriptstyle\infty}}}:\Leftrightarrow\exists
P^{\prime}\approx_{\mbox{s}}^{\infty}P\;\,\exists
Q^{\prime}\approx_{\mbox{s}}^{\infty}Q.~{}P^{\prime}\leq Q^{\prime}~{},$

and construct an order between BD-processes via

${{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}_{\psscalebox{0.8}{\scriptscriptstyle\infty}}}\leq{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}_{\psscalebox{0.8}{\scriptscriptstyle\infty}}}:\Leftrightarrow{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}_{\psscalebox{0.8}{\scriptscriptstyle\infty}}}\preceq^{+}{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}_{\psscalebox{0.8}{\scriptscriptstyle\infty}}}~{}.$

By construction, the relation $\leq$ is reflexive and transitive (even though
$\preceq$ in general is not transitive). Lemma 3 yields that it also is
antisymmetric, and hence a partial order. Namely, if
${{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}_{\psscalebox{0.8}{\scriptscriptstyle\infty}}}\leq{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}_{\psscalebox{0.8}{\scriptscriptstyle\infty}}}$
and
${{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}_{\psscalebox{0.8}{\scriptscriptstyle\infty}}}\leq{{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}_{\psscalebox{0.8}{\scriptscriptstyle\infty}}}$,
then ${\it BD}(P)={\it BD}(Q)$, so $P\approx_{\mbox{s}}^{\infty}Q$, implying
${{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}_{\psscalebox{0.8}{\scriptscriptstyle\infty}}}={{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}Q{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}_{\psscalebox{0.8}{\scriptscriptstyle\infty}}}$.

Now maximality according to Definition 16 is simply maximality w.r.t. $\leq$:

${{\psset{linewidth=0.1pt}\psline{-}(4.2679pt,-1.42262pt)(1.42262pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(1.42262pt,-1.42262pt)(1.42262pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(1.42262pt,7.11317pt)(4.2679pt,7.11317pt)}\phantom{[\,}P{\psset{linewidth=0.1pt}\psline{-}(0.0pt,-1.42262pt)(2.84526pt,-1.42262pt)}{\psset{linewidth=1.5pt}\psline{-}(2.84526pt,-1.42262pt)(2.84526pt,7.11317pt)}{\psset{linewidth=0.1pt}\psline{-}(2.84526pt,7.11317pt)(0.0pt,7.11317pt)}\phantom{]\,}_{\psscalebox{0.8}{\scriptscriptstyle\infty}}}$
is maximal iff