# On Distributability of Petri Nets††thanks: This work was partially supported
by the DFG (German Research Foundation).
An extended abstract of this paper appeared in L. Birkedal, ed.: Proc. 15th
Int. Conf. on Foundations of Software Science and Computation Structures
(FoSSaCS 2012), LNCS 7213, Springer, 2012, pp. 331–345,
doi:http://dx.doi.org/10.1007/978-3-642-28729-9˙22.

Rob van Glabbeek NICTA, Sydney, AustraliaSchool of Computer Science and
Engineering
Univ. of New South Wales, Sydney, Australia<EMAIL_ADDRESS>Institute for
Programming and Reactive Systems
TU Braunschweig, Germany Ursula Goltz Jens-Wolfhard Schicke-Uffmann Institute
for Programming and Reactive Systems
TU Braunschweig, Germany<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract

We formalise a general concept of distributed systems as sequential components
interacting asynchronously. We define a corresponding class of Petri nets,
called LSGA nets, and precisely characterise those system specifications which
can be implemented as LSGA nets up to branching ST-bisimilarity with explicit
divergence.

##  1 Introduction

The aim of this paper is to contribute to a fundamental understanding of the
concept of a distributed reactive system and the paradigms of synchronous and
asynchronous interaction. We start by giving an intuitive characterisation of
the basic features of distributed systems. In particular we assume that
distributed systems consist of components that reside on different locations,
and that any signal from one component to another takes time to travel. Hence
the only interaction mechanism between components is asynchronous
communication.

Our aim is to characterise which system specifications may be implemented as
distributed systems. In many formalisms for system specification or design,
synchronous communication is provided as a basic notion; this happens for
example in process algebras. Hence a particular challenge is that it may be
necessary to simulate synchronous communication by asynchronous communication.

Trivially, any system specification may be implemented distributedly by
locating the whole system on one single component. Hence we need to pose some
additional requirements. One option would be to specify locations for system
activities and then to ask for implementations satisfying this distribution
and still preserving the behaviour of the original specification. This is done
in [2]. Here we pursue a different approach. We add another requirement to our
notion of a distributed system, namely that its components only allow
sequential behaviour. We then ask whether an arbitrary system specification
may be implemented as a distributed system consisting of sequential components
in an optimal way, that is without restricting the concurrency of the original
specification. This is a particular challenge when synchronous communication
interacts with concurrency in the specification of the original system. We
will give a precise characterisation of the class of distributable systems,
which answers in particular under which conditions synchronous communication
may be implemented in a distributed setting.

For our investigations we need a model which is expressive enough to represent
concurrency. It is also useful to have an explicit representation of the
distributed state space of a distributed system, showing in particular the
local control states of components. We choose Petri nets, which offer these
possibilities and additionally allow finite representations of infinite
behaviours. We work within the class of _structural conflict nets_ [8]—a
proper generalisation of the class of one-safe place/transition systems, where
conflict and concurrency are clearly separated.

For comparing the behaviour of systems with their distributed implementation
we need a suitable equivalence notion. Since we think of open systems
interacting with an environment, and since we do not want to restrict
concurrency in applications, we need an equivalence that respects branching
time and concurrency to some degree. Our implementations use transitions which
are invisible to the environment, and this should be reflected in the
equivalence by abstracting from such transitions. However, we do not want
implementations to introduce divergence. In the light of these requirements we
work with two semantic equivalences. _Step readiness equivalence_ is one of
the weakest equivalences that captures branching time, concurrency and
divergence to some degree; whereas _branching ST-bisimilarity with explicit
divergence_ fully captures branching time, divergence, and those aspects of
concurrency that can be represented by concurrent actions overlapping in time.
We obtain the same characterisation for both notions of equivalence, and thus
implicitly for all notions in between these extremes.

We model distributed systems consisting of sequential components as an
appropriate class of Petri nets, called _LSGA nets_. These are obtained by
composing nets with sequential behaviour by means of an asynchronous parallel
composition. We show that this class corresponds exactly to a more abstract
notion of distributed systems, formalised as _distributed nets_ [7].

We then consider distributability of system specifications which are
represented as structural conflict nets. A net $N$ is _distributable_ if there
exists a distributed implementation of $N$, that is a distributed net which is
semantically equivalent to $N$. In the implementation we allow unobservable
transitions, and labellings of transitions, so that single actions of the
original system may be implemented by multiple transitions. However, the
system specifications for which we search distributed implementations are
_plain_ nets without these features.

We give a precise characterisation of distributable nets in terms of a semi-
structural property. This characterisation provides a formal proof that the
interplay between choice and synchronous communication is a key issue for
distributability.

To establish the correctness of our characterisation we develop a new method
for rigorously proving the equivalence of two Petri nets, one of which known
to be plain, up to branching ST-bisimilarity with explicit divergence.

##  2 Basic Notions

In this paper we employ _signed multisets_ , which generalise multisets by
allowing elements to occur in it with a negative multiplicity.

######  Definition 2.1.

multiset Let $X$ be a set.

  * –

A signed multiset over $X$ is a function $A\\!:X\rightarrow\mbox{\bbb Z}$,
i.e. $A\in\mbox{\bbb Z}^{X}$.
It is a _multiset_ iff $A\in{\rm Nature}^{X}$, i.e. iff $A(x)\geq 0$ for all
$x\in X$.

  * –

$x\in X$ is an _element of_ a signed multiset $A\in{\rm Nature}^{X}$, notation
$x\in A$, iff $A(x)\neq 0$.

  * –

For signed multisets $A$ and $B$ over $X$ we write $A\leq B$ iff $A(x)\leq
B(x)$ for all $x\mathbin{\in}X$;
$A\cup B$ denotes the signed multiset over $X$ with $(A\cup
B)(x):=\textrm{max}(A(x),B(x))$,
$A\cap B$ denotes the signed multiset over $X$ with $(A\cap
B)(x):=\textrm{min}(A(x),B(x))$,
$A+B$ denotes the signed multiset over $X$ with $(A+B)(x):=A(x)+B(x)$,
$A-B$ denotes the signed multiset over $X$ with $(A-B)(x):=A(x)-B(x)$, and
for $k\mathbin{\in}{\rm Nature}$ the signed multiset $k\cdot A$ is given by
$(k\cdot A)(x):=k\cdot A(x)$.

  * –

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

  * –

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

  * –

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

  * –

A signed multiset $A$ over $X$ is _finite_ iff $|A|<\infty$, i.e., iff the set
$\\{x\mid x\mathbin{\in}A\\}$ is finite.
We write $A\in_{f}\mbox{\bbb Z}^{X}$ or $A\in_{f}{\rm Nature}^{X}$ to indicate
that $A$ is a finite (signed) multiset over $X$.

  * –

Any function $f:X\rightarrow\mbox{\bbb Z}$ or $f:X\rightarrow\mbox{\bbb
Z}^{Y}$ from $X$ to either the integers or the signed multisets over some set
$Y$ extends to the finite signed multisets $A$ over $X$ by $f(A)=\sum_{x\in
X}A(x)\cdot f(x)$.

Two signed multisets $A\\!:X\rightarrow\mbox{\bbb Z}$ and
$B\\!:Y\rightarrow\mbox{\bbb Z}$ 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 signed multisets. This enables us,
for instance, to use $A+B$ even when $A$ and $B$ have different underlying
domains. A multiset $A$ with $A(x)\in\\{0,1\\}$ for all $x$ is identified with
the set $\\{x\mid A(x)=1\\}$. A signed multiset with elements $x$ and $y$,
having multiplicities $-2$ and $3$, is denoted as
$-2\cdot\\{x\\}+3\cdot\\{y\\}$.

We consider here general labelled place/transition systems with arc weights.
Arc weights are not necessary for the results of the paper, but are included
for the sake of generality.

######  Definition 2.2.

Petri net Let Act be a set of _visible actions_ and $\tau\mathbin{\not\in}{\rm
Act}$ be an _invisible action_. Let ${\rm Act}_{\tau}:={\rm
Act}\stackrel{{\scriptstyle\mbox{\huge.}}}{{\cup}}\\{\tau\\}$. A (_labelled_)
_Petri net_ (_over ${\rm Act}_{\tau}$_) is a tuple $N=(S,T,F,M_{0},\ell)$
where

  * –

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

  * –

$F:(S\times T\cup T\times S)\rightarrow{\rm Nature}$ (the _flow relation_
including _arc weights_),

  * –

$M_{0}:S\rightarrow{\rm Nature}$ (the _initial marking_), and

  * –

$\ell:T\rightarrow{\rm Act}_{\tau}$ (the _labelling function_).

Petri nets are depicted by drawing the places as circles and the transitions
as boxes, containing their label. Identities of places and transitions are
displayed next to the net element. When $F(x,y)>0$ for $x,y\mathbin{\in}S\cup
T$ there is an arrow (_arc_) from $x$ to $y$, labelled with the _arc weight_
$F(x,y)$. Weights 1 are elided. When a Petri net represents a concurrent
system, a global state of this system is given as a _marking_ , a multiset $M$
of places, depicted by placing $M(s)$ dots (_tokens_) in each place $s$. The
initial state is $M_{0}$.

To compress the graphical notation, we also allow universal quantifiers of the
form $\forall x.\phi(x)$ to appear in the drawing (cf. Figure 3). A quantifier
replaces occurrences of $x$ in element identities with all concrete values for
which $\phi(x)$ holds, possibly creating a set of elements instead of the
depicted single one. An arc of which only one end is replicated by a given
quantifier results in a fan of arcs, one for each replicated element. If both
ends of an arc are affected by the same quantifier, an arc is created between
pairs of elements corresponding to the same $x$, but not between elements
created due to differing values of $x$.

The behaviour of a Petri net is defined by the possible moves between markings
$M$ and $M^{\prime}$, which take place when a finite multiset $G$ of
transitions _fires_. In that case, each occurrence of a transition $t$ in $G$
consumes $F(s,t)$ tokens from each place $s$. Naturally, this can happen only
if $M$ makes all these tokens available in the first place. Next, each $t$
produces $F(t,s)$ tokens in each $s$. Definition LABEL:df-firing formalises
this notion of behaviour.

######  Definition 2.3.

preset Let $N=(S,T,F,M_{0},\ell)$ be a Petri net and $x\mathbin{\in}S\cup T$.
The multisets ${\vphantom{x}}^{\bullet}x,~{}{x}^{\bullet}:S\cup
T\rightarrow{\rm Nature}$ 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, and if $x\in S$ we speak of
_pre-_ and _posttransitions_. The _token replacement function_
$\llbracket\\_\\!\\_\rrbracket:T\rightarrow\mbox{\bbb Z}^{S}$ is given by
$\llbracket t\rrbracket={t}^{\bullet}-{\vphantom{t}}^{\bullet}t$ for all $t\in
T$. These functions extend to finite signed multisets as usual (see Definition
LABEL:df-multiset).

######  Definition 2.4.

firing Let $N\mathbin{=}(S,T,F,M_{0},\ell)$ be a Petri net,
$G\mathbin{\in}{\rm Nature}^{T}\\!$, $G$ non-empty and finite, and
$M,M^{\prime}\in{\rm Nature}^{S}$.
$G$ is a _step_ from $M$ to $M^{\prime}$, written
$M~{}[G\rangle_{N}~{}M^{\prime}$, iff

  * –

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

  * –

$M^{\prime}=(M-{\vphantom{G}}^{\bullet}G)+{G}^{\bullet}=M+\llbracket
G\rrbracket$.

Note that steps are (finite) multisets, thus allowing self-concurrency, i.e.
the same transition can occur multiple times in a single step. We write
$M~{}[t\rangle_{N}~{}M^{\prime}$ for
$M\mathrel{[\\{t\\}\rangle_{N}}M^{\prime}$, whereas $M[G\rangle_{N}$
abbreviates $\exists M^{\prime}.~{}M\mathrel{[G\rangle_{N}}M^{\prime}$. We may
omit the subscript $N$ if clear from context.

In our nets transitions are labelled with _actions_ drawn from a set ${\rm
Act}\stackrel{{\scriptstyle\mbox{\huge.}}}{{\cup}}\\{\tau\\}$. This makes it
possible to see these nets as models of _reactive systems_ that interact with
their environment. A transition $t$ can be thought of as the occurrence of the
action $\ell(t)$. If $\ell(t)\mathbin{\in}{\rm Act}$, this occurrence can be
observed and influenced by the environment, but if $\ell(t)\mathbin{=}\tau$,
it cannot and $t$ is an _internal_ or _silent_ transition. Transitions whose
occurrences cannot be distinguished by the environment carry the same label.
In particular, since the environment cannot observe the occurrence of internal
transitions at all, they are all labelled $\tau$.

The labelling function $\ell$ extends to finite multisets of transitions
$G\in\mbox{\bbb Z}^{T}$ by $\ell(G):=\sum_{t\in T}G(t)\cdot\\{\ell(t)\\}$. For
$A,B\in\mbox{\bbb Z}^{{\rm Act}_{\tau}}$ we write $A\equiv B$ iff
$\ell(A)(a)=\ell(B)(a)$ for all $a\in{\rm Act}$, i.e. iff $A$ and $B$ contain
the same (numbers of) visible actions, allowing
$\ell(A)(\tau)\neq\ell(B)(\tau)$. Hence $\ell(G)\equiv\emptyset$ indicates
that $\ell(t)=\tau$ for all transitions $t\in T$ with $G(t)\neq 0$.

######  Definition 2.5.

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

  * –

The set $[M_{0}\rangle_{N}$ of _reachable markings of $N$_ is defined as the
smallest set containing $M_{0}$ that is closed under $[G\rangle_{N}$, meaning
that if $M\in[M_{0}\rangle_{N}$ and $M\mathrel{[G\rangle_{N}}M^{\prime}$ then
$M^{\prime}\in[M_{0}\rangle_{N}$.

  * –

$N$ is _one-safe_ iff $M\in[M_{0}\rangle_{N}\Rightarrow\forall s\in
S.~{}M(s)\leq 1$.

  * –

The _concurrency relation_ $\mathord{\smile}\subseteq T^{2}$ is given by
$t\smile u\Leftrightarrow\exists
M\mathbin{\in}[M_{0}\rangle.~{}M[\\{t\\}\mathord{+}\\{u\\}\rangle$.

  * –

$N$ is a _structural conflict net_ iff for all $t,u\in T$ with $t\smile u$ we
have ${\vphantom{t}}^{\bullet}t\cap{\vphantom{u}}^{\bullet}u=\emptyset$.

We use the term _plain nets_ for Petri nets where $\ell$ is injective and no
transition has the label $\tau$, i.e. essentially unlabelled nets.

This paper first of all aims at studying finite Petri nets: nets with finitely
many places and transitions. However, our work also applies to infinite nets
with the properties that ${\vphantom{t}}^{\bullet}t\neq\emptyset$ for all
transitions $t\in T$, and any reachable marking (a) is finite, and (b) enables
only finitely many transitions. Henceforth, we call such nets _finitary_.
Finitariness can be ensured by requiring
$|M_{0}|\mathbin{<}\infty\wedge\forall t\in
T.\,{\vphantom{t}}^{\bullet}t\neq\emptyset\wedge\forall x\in S\cup
T.\,|{x}^{\bullet}|<\infty$, i.e. that the initial marking is finite, no
transition has an empty set of preplaces, and each place and transition has
only finitely many outgoing arcs.

##  3 Semantic Equivalences

In this section, we give an overview on some semantic equivalences for
reactive systems. Most of these may be defined formally for Petri nets in a
uniform way, by first defining equivalences for transition systems and then
associating different transition systems with a Petri net. This yields in
particular different non-interleaving equivalences for Petri nets.

######  Definition 3.1.

LTS Let $\mathfrak{Act}$ be a set of _visible actions_ and
$\tau\mathbin{\not\in}\mathfrak{Act}$ be an _invisible action_. Let
$\mathfrak{Act}_{\tau}:=\mathfrak{Act}\stackrel{{\scriptstyle\mbox{\huge.}}}{{\cup}}\\{\tau\\}$.
A _labelled transition system_ (LTS) (_over $\mathfrak{Act}_{\tau}$_) is a
triple $\mathfrak{L}=(\mathfrak{S},\mathfrak{T},\mathfrak{M_{0}})$ with

  * –

$\mathfrak{S}$ a set of _states_ ,

  * –

$\mathfrak{T}\subseteq\mathfrak{S}\times\mathfrak{Act}_{\tau}\times\mathfrak{S}$
a _transition relation_

  * –

and $\mathfrak{M_{0}}\in\mathfrak{S}$ the _initial state_.

Given an LTS $(\mathfrak{S},\mathfrak{T},\mathfrak{M_{0}})$ with
$\mathfrak{M},\mathfrak{M}^{\prime}\in\mathfrak{S}$ and
$\alpha\in\mathfrak{Act}_{\tau}$, we write
$\mathfrak{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\alpha$\hskip 2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}$ for
$(\mathfrak{M},\alpha,\mathfrak{M}^{\prime})\in\mathfrak{T}$. We write
$\mathfrak{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\alpha$\hskip 2.5pt}\hfil}}$}}$ for
$\exists\mathfrak{M}^{\prime}.~{}\mathfrak{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\alpha$\hskip 2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}$ and
$\mathfrak{M}\arrownot\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\alpha$\hskip 2.5pt}\hfil}}$}}$ for
$\nexists\mathfrak{M}^{\prime}.~{}\mathfrak{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\alpha$\hskip 2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}$.
Furthermore, $\mathfrak{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\mbox{\tiny\rm(}\alpha\mbox{\tiny\rm)}$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}$ denotes
$\mathfrak{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\alpha$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}\vee(\alpha\mathbin{=}\tau\wedge\mathfrak{M}\mathbin{=}\mathfrak{M}^{\prime})$,
meaning that in case $\alpha\mathbin{=}\tau$ performing a $\tau$-transition is
optional. For $\,a_{1}a_{2}\cdots a_{n}\in\mathfrak{Act}^{*}$ we write
$\mathfrak{M}\mathrel{\hbox{$\mathop{\hbox
to31.74887pt{$\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_{1}a_{2}\cdots a_{n}~{}$\hskip
2.5pt}}$}}\mathfrak{M}^{\prime}$ when

$\mathfrak{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$\hskip
2.5pt}\hfil}}$}}\stackrel{{\scriptstyle
a_{1}}}{{\longrightarrow}}\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}}$}}\stackrel{{\scriptstyle
a_{2}}}{{\longrightarrow}}\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}}$}}\cdots\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}}$}}\stackrel{{\scriptstyle
a_{n}}}{{\longrightarrow}}\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}}$}}\mathfrak{M}^{\prime}\vspace{-4pt}$

where $\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}}$}}$ denotes the reflexive and transitive closure of
$\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\tau$\hskip 2.5pt}\hfil}}$}}$. A state
$\mathfrak{M}\in\mathfrak{S}$ is said to be _reachable_ iff there is a
$\sigma\in\mathfrak{Act}^{*}$ such that
$\mathfrak{M_{0}}\stackrel{{\scriptstyle\sigma}}{{\Longrightarrow}}\mathfrak{M}$.
The set of all reachable states is denoted by $[\mathfrak{M_{0}}\rangle$. In
case there are $\mathfrak{M}_{i}\in[\mathfrak{M_{0}}\rangle$ for all $i\geq 1$
with $\mathfrak{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\tau$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}_{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\tau$\hskip 2.5pt}\hfil}}$}}\cdots$ the LTS is said to
display _divergence_.

Many semantic equivalences on LTSs that in some way abstract from internal
transitions are defined in the literature; an overview can be found in [5]. On
divergence-free LTSs, the most discriminating semantics in the spectrum of
equivalences of [5], and the only one that fully respects the branching
structure of related systems, is _branching bisimilarity_ , proposed in [11].

######  Definition 3.2.

branching LTS Two LTSs
$(\mathfrak{S}_{1},\mathfrak{T}_{1},\mathfrak{M_{0}}_{1})$ and
$(\mathfrak{S}_{2},\mathfrak{T}_{2},\mathfrak{M_{0}}_{2})$ are _branching
bisimilar_ iff there exists a relation
$\mathcal{B}\,\subseteq\mathfrak{S}_{1}\times\mathfrak{S}_{2}$—a _branching
bisimulation_ —such that, for all $\alpha\mathbin{\in}\mathfrak{Act}_{\tau}$:

  1. 1.

$\mathfrak{M_{0}}_{1}\mathcal{B}\,\mathfrak{M_{0}}_{2}$;

  2. 2.

if $\mathfrak{M}_{1}\mathcal{B}\,\mathfrak{M}_{2}$ and
$\mathfrak{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\alpha$\hskip 2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}_{1}$
then $\exists\mathfrak{M}^{\dagger}_{2},\mathfrak{M}^{\prime}_{2}$ such that
$\mathfrak{M}_{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$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\dagger}_{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\mbox{\tiny\rm(}\alpha\mbox{\tiny\rm)}$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}_{2}$,
$\mathfrak{M}_{1}\mathcal{B}\,\mathfrak{M}^{\dagger}_{2}$ and
$\mathfrak{M}^{\prime}_{1}\mathcal{B}\,\mathfrak{M}^{\prime}_{2}$;

  3. 3.

if $\mathfrak{M}_{1}\mathcal{B}\,\mathfrak{M}_{2}$ and
$\mathfrak{M}_{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\alpha$\hskip 2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}_{2}$
then $\exists\mathfrak{M}^{\dagger}_{1},\mathfrak{M}^{\prime}_{1}$ such that
$\mathfrak{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$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\dagger}_{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\mbox{\tiny\rm(}\alpha\mbox{\tiny\rm)}$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}_{1}$,
$\mathfrak{M}^{\dagger}_{1}\mathcal{B}\,\mathfrak{M}_{2}$ and
$\mathfrak{M}^{\prime}_{1}\mathcal{B}\,\mathfrak{M}^{\prime}_{2}$.

Branching bisimilarity _with explicit divergence_ [11, 9], is a variant of
branching bisimilarity that fully respects the diverging behaviour of related
systems. Since in this paper we mainly compare systems of which one admits no
divergence at all, the definition simplifies to the requirement that the other
system may not diverge either.

One of the semantics reviewed in [5] that respects branching time and
divergence only to a small extent, is _readiness equivalence_ , proposed in
[14].

######  Definition 3.3.

readiness Let $\mathfrak{L}=(\mathfrak{S},\mathfrak{T},\mathfrak{M_{0}})$ be
an LTS, $\sigma\in\mathfrak{Act}^{*}$ and $X\subseteq\mathfrak{Act}$.
$\langle\sigma,X\rangle$ is a _ready pair_ of $\mathfrak{L}$ iff

$\exists\mathfrak{M}.~{}\mathfrak{M_{0}}\stackrel{{\scriptstyle\sigma}}{{\Longrightarrow}}\mathfrak{M}\wedge\mathfrak{M}\arrownot\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}\wedge\,X=\\{a\mathbin{\in}\mathfrak{Act}\mid\mathfrak{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 a$\hskip
2.5pt}\hfil}}$}}\\}.$

We write $\mathfrak{R}(\mathfrak{L})$ for the set of all ready pairs of
$\mathfrak{L}$.
Two LTSs $\mathfrak{L}_{1}$ and $\mathfrak{L}_{2}$ are _readiness equivalent_
iff $\mathfrak{R}(\mathfrak{L}_{1})=\mathfrak{R}(\mathfrak{L}_{2})$.

As indicated in [6], see in particular the diagram on Page 317 (or 88),
equivalences on LTSs have been ported to Petri nets and other causality
respecting models of concurrency chiefly in five ways: we distinguish
_interleaving semantics_ , _step semantics_ , _split semantics_ , _ST-
semantics_ and _causal semantics_. Causal semantics fully respect the causal
relationships between the actions of related systems, whereas interleaving
semantics fully abstract from this information. Step semantics differ from
interleaving semantics by taking into account the possibility of multiple
actions to occur simultaneously (in _one step_); this carries a minimal amount
of causal information. ST-semantics respect causality to the extent that it
can be expressed in terms of the possibility of durational actions to overlap
in time. They are formalised by executing a visible action $a$ in two phases:
its start $a^{+}$ and its termination $a^{-}$. Moreover, terminating actions
are properly matched with their starts. Split semantics are a simplification
of ST-semantics in which the matching of starts and terminations is dropped.

Interleaving semantics on Petri nets can be formalised by associating to each
net $N=(S,T,F,M_{0},\ell)$ the LTS $(\mathfrak{S},\mathfrak{T},M_{0})$ with
$\mathfrak{S}$ the set of markings of $N$ and $\mathfrak{T}$ given by

$M_{1}\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}M_{2}:\Leftrightarrow\exists\,t\mathbin{\in}T.~{}\alpha\mathbin{=}\ell(t)\wedge
M_{1}~{}[t\rangle~{}M_{2}.$

Here we take $\mathfrak{Act}:={\rm Act}$. Now each equivalence on LTSs from
[5] induces a corresponding interleaving equivalence on nets by declaring two
nets equivalent iff the associated LTSs are. For example, _interleaving
branching bisimilarity_ is the relation of Definition LABEL:df-branching_LTS
with the $\mathfrak{M}$’s denoting markings, and the $\alpha$’s actions from
${\rm Act}_{\tau}$.

Step semantics on Petri nets can be formalised by associating another LTS to
each net. Again we take $\mathfrak{S}$ to be the markings of the net, and
$\mathfrak{M_{0}}$ the initial marking, but this time $\mathfrak{Act}$
consists of the _steps_ over ${\rm Act}$, the non-empty, finite multisets $A$
of visible actions from ${\rm Act}$, and the transition relation
$\mathfrak{T}$ is given by

$M_{1}\stackrel{{\scriptstyle
A}}{{\longrightarrow}}M_{2}:\Leftrightarrow\exists\,G\in_{f}{\rm
Nature}^{T}.~{}A=\ell(G)\wedge M_{1}~{}[G\rangle~{}M_{2}$

with $\tau$-transitions defined just as in the interleaving case. In
particular, the step version of readiness equivalence would be the relation of
Definition LABEL:df-readiness with the $\mathfrak{M}$’s denoting markings, the
$a$’s steps over ${\rm Act}$, and the $\sigma$’s sequences of steps. However,
variations in this type of definition are possible. In this paper, following
[7], we employ a form of step readiness semantics that is a bit closer to
interleaving semantics: $\sigma$ is a sequence of single actions, whereas the
menu $X$ of possible continuations after $\sigma$ is a set of steps.

######  Definition 3.4.

step readiness Let $N=(S,T,F,M_{0},\ell)$ be a Petri net, $\sigma\in{\rm
Act}^{*}$ and $X\subseteq{\rm Nature}^{{\rm Act}}$. $\langle\sigma,X\rangle$
is a _step ready pair_ of $N$ iff

$\exists M.M_{0}\stackrel{{\scriptstyle\sigma}}{{\Longrightarrow}}M\wedge
M\arrownot\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}\wedge\,X=\\{A\mathbin{\in}{\rm
Nature}^{\rm Act}\mid 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 A$\hskip
2.5pt}\hfil}}$}}\\}.$

We write $\mathcal{R}(N)$ for the set of all step ready pairs of $N$.
Two Petri nets $N_{1}$ and $N_{2}$ are _step readiness equivalent_ ,
$N_{1}\approx_{\mathscr{R}}N_{2}$, iff
$\mathcal{R}(N_{1})=\mathcal{R}(N_{2})$.

Next we propose a general definition on Petri nets of ST-versions of each of
the semantics of [5]. Again we do this through a mapping from nets to a
suitable LTS. An _ST-marking_ of a net $(S,T,F,M_{0},\ell)$ is a pair
$(M,U)\mathbin{\in}{\rm Nature}^{S}\mathord{\times}T^{*}$ of a normal marking,
together with a sequence of transitions _currently firing_. The _initial_ ST-
marking is $\mathfrak{M_{0}}:=(M_{0},\varepsilon)$. The elements of ${\rm
Act}^{\pm}:=\\{a^{+},\,a^{-n}\mid a\mathbin{\in}{\rm Act},~{}n\mathbin{>}0\\}$
are called _visible action phases_ , and $Act^{\pm}_{\tau}:={\rm
Act}^{\pm}\stackrel{{\scriptstyle\mbox{\huge.}}}{{\cup}}\\{\tau\\}$. For $U\in
T^{*}$, we write $t\in^{(n)}U$ if $t$ is the $n^{\it th}$ element of $U$.
Furthermore $U^{-n}$ denotes $U$ after removal of the $n^{\it th}$ transition.

######  Definition 3.5.

ST-marking Let $N=(S,T,F,M_{0},\ell)$ be a Petri net, labelled over ${\rm
Act}_{\tau}$.

The _ST-transition relations_ $\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\eta$\hskip 2.5pt}\hfil}}$}}$ for $\eta\mathbin{\in}{\rm
Act}^{\pm}_{\tau}$ between ST-markings are given by

$(M,U)\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}}$}}(M^{\prime},U^{\prime})$ iff $\exists
t\mathbin{\in}T.~{}\ell(t)=a\wedge M[t\rangle\wedge
M^{\prime}=M-{\vphantom{t}}^{\bullet}t\wedge U^{\prime}=Ut$.

$(M,U)\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}}$}}(M^{\prime},U^{\prime})$ iff $\exists
t\in^{(n)}U.~{}\ell(t)=a\wedge U^{\prime}=U^{-n}\wedge
M^{\prime}=M+{t}^{\bullet}$.

$(M,U)\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\tau$\hskip 2.5pt}\hfil}}$}}(M^{\prime},U^{\prime})$ iff
$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\tau$\hskip 2.5pt}\hfil}}$}}M^{\prime}\wedge U^{\prime}=U$.

Now the ST-LTS associated to a net $N$ is
$(\mathfrak{S},\mathfrak{T},\mathfrak{M_{0}})$ with $\mathfrak{S}$ the set of
ST-markings of $N$, $\mathfrak{Act}:={\rm Act}^{\pm}$, $\mathfrak{T}$ as
defined in Definition LABEL:df-ST-marking, and $\mathfrak{M_{0}}$ the initial
ST-marking. Again, each equivalence on LTSs from [5] induces a corresponding
ST-equivalence on nets by declaring two nets equivalent iff their associated
LTSs are. In particular, _branching ST-bisimilarity_ is the relation of
Definition LABEL:df-branching_LTS with the $\mathfrak{M}$’s denoting ST-
markings, and the $\alpha$’s action phases from ${\rm Act}^{\pm}_{\tau}$. We
write $N_{1}\approx^{\Delta}_{bSTb}N_{2}$ iff $N_{1}$ and $N_{2}$ are
branching ST-bisimilar with explicit divergence.

_ST-bisimilarity_ was originally proposed in [10]. It was extended to a
setting with internal actions in [18], based on the notion of _weak
bisimilarity_ of [13], which is a bit less discriminating than branching
bisimilarity. The above can be regarded as a reformulation of the same idea;
the notion of weak ST-bisimilarity defined according to the recipe above
agrees with the ST-bisimilarity of [18].

The next proposition says that branching ST-bisimilarity with explicit
divergence is more discriminating than (i.e.  _stronger_ than, _finer_ than,
or included in) step readiness equivalence.

######  Proposition 3.6.

step ready ST Let $N_{1}$ and $N_{2}$ be Petri nets. If
$N_{1}\approx^{\Delta}_{bSTb}N_{2}$ then $N_{1}\approx_{\mathscr{R}}N_{2}$.

######  Proof 3.7.

Suppose $N_{1}\approx^{\Delta}_{bSTb}N_{2}$ and
$\langle\sigma,X\rangle\in\mathcal{R}(N_{1})$. By symmetry it suffices to show
that $\langle\sigma,X\rangle\in\mathcal{R}(N_{2})$.

There must be a branching bisimulation $\mathcal{B}\,$ between the ST-markings
of $N_{1}=(S_{1},T_{1},F_{1},{M_{0}}_{1},\ell_{1})$ and
$N_{2}=(S_{2},T_{2},F_{2},{M_{0}}_{2},\ell_{2})$. In particular,
$({M_{0}}_{1},\epsilon)\mathcal{B}\,({M_{0}}_{2},\epsilon)$. Let
$\sigma:=a_{1}a_{2}\cdots a_{n}\in{\rm Act}^{*}$. Then
${M_{0}}_{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$\hskip
2.5pt}\hfil}}$}}\stackrel{{\scriptstyle
a_{1}}}{{\longrightarrow}}\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}}$}}\stackrel{{\scriptstyle
a_{2}}}{{\longrightarrow}}\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}}$}}\cdots\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}}$}}\stackrel{{\scriptstyle
a_{n}}}{{\longrightarrow}}\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^{\prime}_{1}$ for a marking $M^{\prime}_{1}\mathbin{\in}{\rm
Nature}^{S_{1}}$ with $X=\\{A\mathbin{\in}{\rm Nature}^{\rm Act}\mid
M^{\prime}_{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$\hskip
2.5pt}\hfil}}$}}\\}$ and
$M^{\prime}_{1}\arrownot\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}$.
Hence $({M_{0}}_{1},\epsilon)\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}}$}}\stackrel{{\scriptstyle
a_{1}^{+}}}{{\longrightarrow}}\stackrel{{\scriptstyle
a_{1}^{-1}}}{{\longrightarrow}}\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}}$}}\stackrel{{\scriptstyle
a_{2}^{+}}}{{\longrightarrow}}\stackrel{{\scriptstyle
a_{2}^{-1}}}{{\longrightarrow}}\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}}$}}\cdots\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}}$}}\stackrel{{\scriptstyle
a_{n}^{+}}}{{\longrightarrow}}\stackrel{{\scriptstyle
a_{n}^{-1}}}{{\longrightarrow}}\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^{\prime}_{1},\epsilon)$. Thus, using the properties of a
branching bisimulation on the ST-LTSs associated to $N_{1}$ and $N_{2}$, there
must be a marking $M^{\prime}_{2}\mathbin{\in}{\rm Nature}^{S_{2}}$ such that
$({M_{0}}_{2},\epsilon)\\!\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}}$}}\stackrel{{\scriptstyle
a_{1}^{+}}}{{\longrightarrow}}\stackrel{{\scriptstyle
a_{1}^{-1}}}{{\longrightarrow}}\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}}$}}\stackrel{{\scriptstyle
a_{2}^{+}}}{{\longrightarrow}}\stackrel{{\scriptstyle
a_{2}^{-1}}}{{\longrightarrow}}\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}}$}}\cdots\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}}$}}\stackrel{{\scriptstyle
a_{n}^{+}}}{{\longrightarrow}}\stackrel{{\scriptstyle
a_{n}^{-1}}}{{\longrightarrow}}\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^{\prime}_{2},\epsilon)$ and
$(M^{\prime}_{1},\epsilon)\mathcal{B}\,(M^{\prime}_{2},\epsilon)$. Since
$(M^{\prime}_{1},\epsilon)\arrownot\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}$,
the ST-marking $(M^{\prime}_{1},\epsilon)$ admits no divergence. As
$\approx^{\Delta}_{bSTb}$ respects this property, also
$(M^{\prime}_{2},\epsilon)$ admits no divergence, and there must be an
$M^{\prime\prime}_{2}\mathbin{\in}{\rm Nature}^{S_{2}}$ with
$M^{\prime\prime}_{2}\arrownot\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}$
and $(M^{\prime}_{2},\epsilon)\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^{\prime\prime}_{2},\epsilon)$. Clause 3. of a branching
bisimulation gives
$(M^{\prime}_{1},\epsilon)\mathcal{B}\,(M^{\prime\prime}_{2},\epsilon)$, and
Definition LABEL:df-ST-marking yields
${M_{0}}_{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\sigma$\hskip 2.5pt}\hfil}}$}}M^{\prime\prime}_{2}$.

Now let $B=\\{b_{1},\ldots,b_{n}\\}\in X$. Then
$M^{\prime}_{1}\stackrel{{\scriptstyle B}}{{\longrightarrow}}$, so
$(M^{\prime}_{1},\epsilon)\stackrel{{\scriptstyle
b_{1}^{+}}}{{\longrightarrow}}\stackrel{{\scriptstyle
b_{2}^{+}}}{{\longrightarrow}}\cdots\stackrel{{\scriptstyle
b_{m}^{+}}}{{\longrightarrow}}$. Property 2. of a branching bisimulation
implies $(M^{\prime\prime}_{2},\epsilon)\stackrel{{\scriptstyle
b_{1}^{+}}}{{\longrightarrow}}\stackrel{{\scriptstyle
b_{2}^{+}}}{{\longrightarrow}}\cdots\stackrel{{\scriptstyle
b_{m}^{+}}}{{\longrightarrow}}$ and hence
$M^{\prime\prime}_{2}\stackrel{{\scriptstyle B}}{{\longrightarrow}}$.
Likewise, with Property 3., $M^{\prime\prime}_{2}\stackrel{{\scriptstyle
B}}{{\longrightarrow}}$ implies $M^{\prime}_{1}\stackrel{{\scriptstyle
B}}{{\longrightarrow}}$ for all $B\in{\rm Nature}^{\rm Act}$. It follows that
$\langle\sigma,X\rangle\in\mathcal{R}(N_{2})$.

In this paper we employ both step readiness equivalence and branching ST-
bisimilarity with explicit divergence. Fortunately it will turn out that for
our purposes the latter equivalence coincides with its split version (since
always one of the compared nets is plain, see Proposition LABEL:pr-split).

A _split marking_ of a net $N=(S,T,F,M_{0},\ell)$ is a pair $(M,U)\in{\rm
Nature}^{S}\times{\rm Nature}^{T}$ of a normal marking $M$, together with a
multiset of transitions currently firing. The _initial_ split marking is
$\mathfrak{M_{o}}:=(M_{0},\emptyset)$. A split marking can be regarded as an
abstraction from an ST-marking, in which the total order on the (finite)
multiset of transitions that are currently firing has been dropped. Let ${\rm
Act}^{\pm}_{\rm split}:=\\{a^{+},\,a^{-}\mid a\in{\rm Act}\\}$.

######  Definition 3.8.

split marking Let $N=(S,T,F,M_{0},\ell)$ be a Petri net, labelled over ${\rm
Act}_{\tau}$.

The _split transition relations_ $\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\zeta$\hskip 2.5pt}\hfil}}$}}$ for $\zeta\mathbin{\in}{\rm
Act}^{\pm}_{\rm
split}\stackrel{{\scriptstyle\mbox{\huge.}}}{{\cup}}\\{\tau\\}$ between split
markings are given by

$(M,U)\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}}$}}(M^{\prime},U^{\prime})$ iff $\exists
t\mathbin{\in}T.~{}\ell(t)=a\wedge M[t\rangle\wedge
M^{\prime}=M-{\vphantom{t}}^{\bullet}t\wedge U^{\prime}=U+\\{t\\}$.

$(M,U)\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}}$}}(M^{\prime},U^{\prime})$ iff $\exists
t\mathbin{\in}U.~{}\ell(t)=a\wedge U^{\prime}=U-\\{t\\}\wedge
M^{\prime}=M+{t}^{\bullet}$.

$(M,U)\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\tau$\hskip 2.5pt}\hfil}}$}}(M^{\prime},U^{\prime})$ iff
$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\tau$\hskip 2.5pt}\hfil}}$}}M^{\prime}\wedge U^{\prime}=U$.

Note that $(M,U)\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}}$}}$ iff $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 a$\hskip
2.5pt}\hfil}}$}}$, whereas $(M,U)\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}}$}}$ iff $a\in\ell(U)$. With induction on
reachability of markings it is furthermore easy to check that
$(M,U)\in[\mathfrak{M_{0}}\rangle$ iff $\ell(U)\in{\rm Nature}^{\rm Act}$ and
$M+\\!{\vphantom{U}}^{\bullet}U\in[M_{0}\rangle$.

The split LTS associated to a net $N$ is
$(\mathfrak{S},\mathfrak{T},\mathfrak{M_{0}})$ with $\mathfrak{S}$ the set of
split markings of $N$, $\mathfrak{Act}:={\rm Act}^{\pm}$, $\mathfrak{T}$ as
defined in Definition LABEL:df-split_marking, and $\mathfrak{M_{0}}$ the
initial split marking. Again, each equivalence on LTSs from [5] induces a
corresponding split equivalence on nets by declaring two nets equivalent iff
their associated LTSs are. In particular, _branching split bisimilarity_ is
the relation of Definition LABEL:df-branching_LTS with the $\mathfrak{M}$’s
denoting split markings, and the $\alpha$’s action phases from ${\rm
Act}^{\pm}_{\rm
split}\stackrel{{\scriptstyle\mbox{\huge.}}}{{\cup}}\\{\tau\\}$.

For $\mathfrak{M}=(M,U)\in{\rm Nature}^{S}\times T^{*}$ an ST-marking, let
$\overline{\mathfrak{M}}=(M,\overline{U})\in{\rm Nature}^{S}\times{\rm
Nature}^{T}$ be the split marking obtained by converting the sequence $U$ into
the multiset $\overline{U}$, where $\overline{U}(t)$ is the number of
occurrences of the transition $t\in T$ in $U$. Moreover, define
$\ell(\mathfrak{M})$ by $\ell(M,U):=\ell(U)$ and $\ell(t_{1}t_{2}\cdots
t_{k}):=\ell(t_{1})\ell(t_{2})\cdots\ell(t_{k})$. Furthermore, for
$\eta\in{\rm Act}^{\pm}_{\tau}$, let $\overline{\eta}\in{\rm Act}^{\pm}_{\rm
split}\stackrel{{\scriptstyle\mbox{\huge.}}}{{\cup}}\\{\tau\\}$ be given by
$\overline{a^{+}}:=a^{+}$, $\overline{a^{-n}}:=a^{-}$ and
$\overline{\tau}:=\tau$.

###### Observation 1

Let $\mathfrak{M},\mathfrak{M}^{\prime}$ be ST-markings,
$\mathfrak{M}^{\dagger}$ a split marking, $\eta\mathbin{\in}{\rm
Act}^{\pm}_{\tau}$ and $\zeta\in{\rm Act}^{\pm}_{\rm split}\cup\\{\tau\\}$.
Then

  * –

$\mathfrak{M}\in{\rm Nature}^{S}\times T^{*}$ is the initial ST-marking of $N$
iff $\overline{\mathfrak{M}}\in{\rm Nature}^{S}\times{\rm Nature}^{T}$ is the
initial split marking of $N$;

  * –

if $\mathfrak{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\eta$\hskip 2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}$ then
$\overline{\mathfrak{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\overline{\eta}$\hskip
2.5pt}\hfil}}$}}\overline{\mathfrak{M}^{\prime}}$;

  * –

if $\overline{\mathfrak{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\zeta$\hskip 2.5pt}\hfil}}$}}\mathfrak{M}^{\dagger}$ then
there is a $\mathfrak{M}^{\prime}\in{\rm Nature}^{S}\times T^{*}$ and
$\eta\in{\rm Act}^{\pm}_{\tau}$ such that
$\mathfrak{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\eta$\hskip 2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}$,
$\overline{\eta}=\zeta$ and
$\overline{\mathfrak{M}^{\prime}}=\mathfrak{M}^{\dagger}$;

  * –

if $\mathfrak{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\mbox{\tiny\rm(}\eta\mbox{\tiny\rm)}$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}$ then
$\overline{\mathfrak{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\overline{\mbox{\tiny\rm(}\eta\mbox{\tiny\rm)}}$\hskip
2.5pt}\hfil}}$}}\overline{\mathfrak{M}^{\prime}}$;

  * –

if $\overline{\mathfrak{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\mbox{\tiny\rm(}\zeta\mbox{\tiny\rm)}$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\dagger}$ then there is a
$\mathfrak{M}^{\prime}\in{\rm Nature}^{S}\times T^{*}$ and $\eta\in{\rm
Act}^{\pm}_{\tau}$ such that $\mathfrak{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\mbox{\tiny\rm(}\eta\mbox{\tiny\rm)}$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}$, $\overline{\eta}=\zeta$ and
$\overline{\mathfrak{M}^{\prime}}=\mathfrak{M}^{\dagger}$;

  * –

if $\mathfrak{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$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}$ then
$\overline{\mathfrak{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$\hskip
2.5pt}\hfil}}$}}\overline{\mathfrak{M}^{\prime}}$;

  * –

if $\overline{\mathfrak{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$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\dagger}$ then there is a
$\mathfrak{M}^{\prime}\in{\rm Nature}^{S}\times T^{*}$ such that
$\mathfrak{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$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}$ and
$\overline{\mathfrak{M}^{\prime}}=\mathfrak{M}^{\dagger}$. $\Box$

######  Lemma 3.9.

label sequence Let $N_{1}=(S_{1},T_{1},F_{1},{M_{0}}_{1},\ell)$ and
$N_{2}=(S_{2},T_{2},F_{2},{M_{0}}_{2},\ell_{2})$ be two nets, $N_{2}$ being
plain; let $\mathfrak{M}_{1},\mathfrak{M}^{\prime}_{1}$ be ST-markings of
$N_{1}$, and $\mathfrak{M}_{2},\mathfrak{M}^{\prime}_{2}$ ST-markings of
$N_{2}$. If $\ell(\mathfrak{M}_{2})=\ell(\mathfrak{M}_{1})$,
$\mathfrak{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\eta$\hskip 2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}_{1}$ and
$\mathfrak{M}_{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\mbox{\tiny\rm(}\eta^{\prime}\mbox{\tiny\rm)}$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}_{2}$ with
$\overline{\eta^{\prime}}=\overline{\eta}$, then there is an
$\mathfrak{M}^{\prime\prime}_{2}$ with
$\mathfrak{M}_{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\mbox{\tiny\rm(}\eta\mbox{\tiny\rm)}$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\prime\prime}_{2}$,
$\ell(\mathfrak{M}^{\prime\prime}_{2})=\ell(\mathfrak{M}^{\prime}_{1})$, and
$\overline{\mathfrak{M}^{\prime\prime}_{2}}=\overline{\mathfrak{M}^{\prime}_{2}}$.

######  Proof 3.10.

If $\mathfrak{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\eta$\hskip 2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}$ or
$\mathfrak{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\mbox{\tiny\rm(}\eta\mbox{\tiny\rm)}$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}$ then $\ell(\mathfrak{M}^{\prime})$ is
completely determined by $\ell(\mathfrak{M})$ and $\eta$. For this reason the
requirement
$\ell(\mathfrak{M}^{\prime\prime}_{2})=\ell(\mathfrak{M}^{\prime}_{1})$ will
hold as soon as the other requirements are met.

First suppose $\eta$ is of the form $\tau$ or $a^{+}$. Then
$\overline{\eta}=\eta$ and moreover $\overline{\eta^{\prime}}=\overline{\eta}$
implies $\eta^{\prime}=\eta$. Thus we can take
$\mathfrak{M}^{\prime\prime}_{2}:=\mathfrak{M}^{\prime}_{2}$.

Now suppose $\eta:=a^{-n}$ for some $n>0$. Then $\eta^{\prime}=a^{-m}$ for
some $m>0$. As $\mathfrak{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\eta$\hskip 2.5pt}\hfil}}$}}$, the $n^{\it th}$ element of
$\ell(\mathfrak{M}_{1})$ must (exist and) be $a$. Since
$\ell(\mathfrak{M}_{2})=\ell(\mathfrak{M}_{1})$, also the $n^{\it th}$ element
of $\ell(\mathfrak{M}_{2})$ must be $a$, so there is an
$\mathfrak{M}^{\prime\prime}_{2}$ with
$\mathfrak{M}_{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\mbox{\tiny\rm(}\eta\mbox{\tiny\rm)}$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\prime\prime}_{2}$. Let
$\mathfrak{M}_{2}:=(M_{2},U_{2})$. Then $U_{2}$ is a sequence of transitions
of which the $n^{\it th}$ and the $m^{\it th}$ elements are both labelled $a$.
Since the net $N_{2}$ is plain, those two transitions must be equal. Let
$\mathfrak{M}^{\prime}_{2}:=(M^{\prime}_{2},U^{\prime}_{2})$ and
$\mathfrak{M^{\prime\prime}}_{2}:=(M^{\prime\prime}_{2},U^{\prime\prime}_{2})$.
We find that $M^{\prime\prime}_{2}\mathbin{=}M^{\prime}_{2}$ and
$\overline{U^{\prime\prime}_{2}}\mathbin{=}\overline{U^{\prime}_{2}}$. It
follows that
$\overline{\mathfrak{M}^{\prime\prime}_{2}}=\overline{\mathfrak{M}^{\prime}_{2}}$.

###### Observation 2

If $\mathfrak{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$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}$ for ST-markings
$\mathfrak{M},\mathfrak{M}^{\prime}$ then
$\ell(\mathfrak{M}^{\prime})=\ell(\mathfrak{M})$.

###### Observation 3

If $\ell(\mathfrak{M}_{1})=\ell(\mathfrak{M}_{2})$ and
$\mathfrak{M}_{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^{-n}$\hskip 2.5pt}\hfil}}$}}$ for some $a\in{\rm Act}$ and $n>0$, then
$\mathfrak{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
a^{-n}$\hskip 2.5pt}\hfil}}$}}$.

###### Observation 4

If $\mathfrak{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
a^{-n}$\hskip 2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}$ and
$\mathfrak{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
a^{-n}$\hskip 2.5pt}\hfil}}$}}\mathfrak{M}^{\prime\prime}$ for some $a\in{\rm
Act}$ and $n>0$, then $\mathfrak{M}^{\prime}_{1}=\mathfrak{M}^{\prime}_{2}$.

######  Proposition 3.11.

split Let $N_{1}=(S_{1},T_{1},F_{1},{M_{0}}_{1},\ell)$ and
$N_{2}=(S_{2},T_{2},F_{2},{M_{0}}_{2},\ell_{2})$ be two nets, $N_{2}$ being
plain. Then $N_{1}$ and $N_{2}$ are branching ST-bisimilar (with explicit
divergence) iff they are branching split bisimilar (with explicit divergence).

######  Proof 3.12.

Suppose $\mathcal{B}\,$ is a branching ST-bisimulation between $N_{1}$ and
$N_{2}$. Then, by Observation 1, the relation $\mathcal{B}\,_{\rm
split}:=\\{(\overline{\mathfrak{M}_{1}},\overline{\mathfrak{M}_{2}})\mid(\mathfrak{M}_{1},\mathfrak{M}_{2})\in\mathcal{B}\,\\}$
is a branching split bisimulation between $N_{1}$ and $N_{2}$.

Now let $\mathcal{B}\,$ be a branching split bisimulation between $N_{1}$ and
$N_{2}$. Then, using Observation 1, the relation $\mathcal{B}\,_{\rm
ST}:=\\{(\mathfrak{M}_{1},\mathfrak{M}_{2})\mid\ell_{1}(\mathfrak{M}_{1})=\ell_{2}(\mathfrak{M}_{2})\wedge(\overline{\mathfrak{M}_{1}},\overline{\mathfrak{M}_{2}})\in\mathcal{B}\,\\}$
turns out to be a branching ST-bisimulation between $N_{1}$ and $N_{2}$:

  1. 1.

$\mathfrak{M_{0}}_{1}\mathcal{B}\,_{\rm ST}\mathfrak{M_{0}}_{2}$ follows from
Observation 1, using that
$\overline{\mathfrak{M_{0}}_{1}}\mathcal{B}\,\overline{\mathfrak{M_{0}}_{2}}$
and
$\ell(\mathfrak{M_{0}}_{1})\mathbin{=}\ell(\mathfrak{M_{0}}_{2})\mathbin{=}\epsilon$.

  2. 2.

Suppose $\mathfrak{M}_{1}\mathcal{B}\,_{\rm ST}\mathfrak{M}_{2}$ and
$\mathfrak{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\eta$\hskip 2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}_{1}$. Then
$\overline{\mathfrak{M}_{1}}\mathcal{B}\,\overline{\mathfrak{M}_{2}}$ and
$\overline{\mathfrak{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\overline{\eta}$\hskip
2.5pt}\hfil}}$}}\overline{\mathfrak{M}^{\prime}_{1}}$. Hence
$\exists\mathfrak{M}^{\dagger}_{2},\mathfrak{M}^{\ddagger}_{2}$ such that
$\overline{\mathfrak{M}_{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$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\dagger}_{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\mbox{\tiny\rm(}\overline{\eta}\mbox{\tiny\rm)}$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\ddagger}_{2}$,
$\overline{\mathfrak{M}_{1}}\mathcal{B}\,\mathfrak{M}^{\dagger}_{2}$ and
$\overline{\mathfrak{M}^{\prime}_{1}}\mathcal{B}\,\mathfrak{M}^{\ddagger}_{2}$.
As $N_{2}$ is plain, $\mathfrak{M}^{\dagger}_{2}=\overline{\mathfrak{M}_{2}}$.
By Observation 1, using that
$\overline{\mathfrak{M}_{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\mbox{\tiny\rm(}\overline{\eta}\mbox{\tiny\rm)}$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\ddagger}_{2}$,
$\exists\mathfrak{M}^{\prime}_{2},\,\eta^{\prime}$ such that
$\mathfrak{M}_{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\mbox{\tiny\rm(}\eta^{\prime}\mbox{\tiny\rm)}$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}_{2}$,
$\overline{\eta^{\prime}}=\overline{\eta}$ and
$\overline{\mathfrak{M}^{\prime}_{2}}=\mathfrak{M}^{\ddagger}_{2}$. By Lemma
LABEL:lem-label_sequence, there is an ST-marking
$\mathfrak{M}^{\prime\prime}_{2}$ such that
$\mathfrak{M}_{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\mbox{\tiny\rm(}\eta\mbox{\tiny\rm)}$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\prime\prime}_{2}$,
$\ell(\mathfrak{M}^{\prime\prime}_{2})=\ell(\mathfrak{M}^{\prime}_{1})$, and
$\overline{\mathfrak{M}^{\prime\prime}_{2}}=\overline{\mathfrak{M}^{\prime}_{2}}=\mathfrak{M}^{\ddagger}_{2}$.
It follows that $\mathfrak{M}^{\prime}_{1}\mathcal{B}\,_{\rm
ST}\mathfrak{M}^{\prime\prime}_{2}$.

  3. 3.

Suppose $\mathfrak{M}_{1}\mathcal{B}\,_{\rm ST}\mathfrak{M}_{2}$ and
$\mathfrak{M}_{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\eta$\hskip 2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}_{2}$. Then
$\overline{\mathfrak{M}_{1}}\mathcal{B}\,\overline{\mathfrak{M}_{2}}$ and
$\overline{\mathfrak{M}_{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\overline{\eta}$\hskip
2.5pt}\hfil}}$}}\overline{\mathfrak{M}^{\prime}_{2}}$. Hence
$\exists\mathfrak{M}^{\dagger}_{1},\mathfrak{M}^{\ddagger}_{1}$ such that
$\overline{\mathfrak{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$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\dagger}_{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\mbox{\tiny\rm(}\overline{\eta}\mbox{\tiny\rm)}$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\ddagger}_{1}$,
$\mathfrak{M}^{\dagger}_{1}\mathcal{B}\,\overline{\mathfrak{M}_{2}}$ and
$\mathfrak{M}^{\ddagger}_{1}\mathcal{B}\,\overline{\mathfrak{M}^{\prime}_{2}}$.
By Observation 1, $\exists\mathfrak{M}^{*}_{1}$ such that
$\mathfrak{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$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{*}_{1}$ and
$\overline{\mathfrak{M}^{*}_{1}}=\mathfrak{M}^{\dagger}_{1}$. By Observation
2, $\ell(\mathfrak{M}^{*}_{1})=\ell(\mathfrak{M}_{1})=\ell(\mathfrak{M}_{2})$,
so $\mathfrak{M}^{*}_{1}\mathcal{B}\,_{\rm ST}\mathfrak{M}_{2}$. Since $N_{2}$
is plain, $\eta\neq\tau$.

     * •

Let $\eta=a^{+}$ for some $a\in{\rm Act}$. Using that
$\overline{\mathfrak{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\mbox{\tiny\rm(}\overline{\eta}\mbox{\tiny\rm)}$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\ddagger}_{1}$, by Observation 1
$\exists\mathfrak{M}^{\prime}_{1},\,\eta^{\prime}$ such that
$\mathfrak{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\mbox{\tiny\rm(}\eta^{\prime}\mbox{\tiny\rm)}$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}_{1}$,
$\overline{\eta^{\prime}}=\overline{\eta}$ and
$\overline{\mathfrak{M}^{\prime}_{1}}=\mathfrak{M}^{\ddagger}_{1}$. It must be
that $\eta^{\prime}=\eta=a^{+}$ and
$\ell(\mathfrak{M}^{\prime}_{1})=\ell(\mathfrak{M}^{*}_{1})a=\ell(\mathfrak{M}_{2})a=\ell(\mathfrak{M}^{\prime}_{2})$.
Hence $\mathfrak{M}^{\prime}_{1}\mathcal{B}\,_{\rm
ST}\mathfrak{M}^{\prime}_{2}$.

     * •

Let $\eta=a^{-n}$ for some $a\in{\rm Act}$ and $n>0$. By Observation 3,
$\exists\mathfrak{M}^{\prime}_{1}$ with
$\mathfrak{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\eta$\hskip 2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}_{1}$. By
Part 2. of this proof, $\exists\mathfrak{M}^{\prime\prime}_{2}$ such that
$\mathfrak{M}_{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\mbox{\tiny\rm(}\eta\mbox{\tiny\rm)}$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\prime\prime}_{2}$ and
$\mathfrak{M}^{\prime}_{1}\mathcal{B}\,_{\rm
ST}\mathfrak{M}^{\prime\prime}_{2}$. By Observation 4
$\mathfrak{M}^{\prime\prime}_{2}=\mathfrak{M}^{\prime}_{2}$.

Since the net $N_{2}$ is plain, it has no divergence. In such a case, the
requirement “with explicit divergence” requires $N_{1}$ to be free of
divergence as well, regardless of whether split or ST-semantics is in used.

In this paper we will not consider causal semantics. The reason is that our
distributed implementations will not fully preserve the causal behaviour of
nets. We will further comment on this in the conclusion.

##  4 Distributed Systems

In this section, we stipulate what we understand by a distributed system, and
subsequently formalise a model of distributed systems in terms of Petri nets.

  * –

A distributed system consists of components residing on different locations.

  * –

Components work concurrently.

  * –

Interactions between components are only possible by explicit communications.

  * –

Communication between components is time consuming and asynchronous.

Asynchronous communication is the only interaction mechanism in a distributed
system for exchanging signals or information.

  * –

The sending of a message happens always strictly before its receipt (there is
a causal relation between sending and receiving a message).

  * –

A sending component sends without regarding the state of the receiver; in
particular there is no need to synchronise with a receiving component. After
sending the sender continues its behaviour independently of receipt of the
message.

As explained in the introduction, we will add another requirement to our
notion of a distributed system, namely that its components only allow
sequential behaviour.

Formally, we model distributed systems as nets consisting of component nets
with sequential behaviour and interfaces in terms of input and output places.

######  Definition 4.1.

component Let $N\mathbin{=}(S,T,F,M_{0},\ell)$ be a Petri net,
$I,O\mathbin{\subseteq}S$, $I\mathop{\cap}O\mathbin{=}\emptyset$ and
${O}^{\bullet}=\emptyset$.

  * 1.

$(N,I,O)$ is a _component with interface $(I,O)$_.

  * 2.

$(N,I,O)$ is a _sequential_ component with interface $(I,O)$ iff
$\exists Q\mathbin{\subseteq}S\mathord{\setminus}(I\cup O)$ with $\forall t\in
T.|{\vphantom{t}}^{\bullet}t\mathop{\upharpoonright}Q|=1\wedge|{t}^{\bullet}\\!\mathop{\upharpoonright}Q|=1$
and $|M_{0}\mathop{\upharpoonright}Q|=1$.

An input place $i\mathbin{\in}I$ of a component
$\mathcal{C}\mathbin{=}(N,I,O)$ can be regarded as a mailbox of $\mathcal{C}$
for a specific type of messages. An output place $o\mathbin{\in}O$, on the
other hand, is an address outside $\mathcal{C}$ to which $\mathcal{C}$ can
send messages. Moving a token into $o$ is like posting a letter. The condition
${o}^{\bullet}=\emptyset$ says that a message, once posted, cannot be
retrieved by the component.

A set of places like $Q$ above is called an _$S$ -invariant_. The requirements
guarantee that the number of tokens in these places remains constant, in this
case $1$. It follows that no two transitions can ever fire concurrently (in
one step). Conversely, whenever a net is sequential, in the sense that no two
transitions can fire in one step, it is easily converted into a behaviourally
equivalent net with the required $S$-invariant, namely by adding a single
marked place with a self-loop to all transitions. This modification preserves
virtually all semantic equivalences on Petri nets from the literature,
including $\approx^{\Delta}_{bSTb}$.

Next we define an operator for combining components with asynchronous
communication by fusing input and output places.

######  Definition 4.2.

parcomp Let $\mathfrak{K}$ be an index set.
Let $((S_{k},T_{k},F_{k},{M_{0}}_{k},\ell_{k}),I_{k},O_{k})$ with
$k\in\mathfrak{K}$ be components with interface such that $(S_{k}\cup
T_{k})\cap(S_{l}\cup T_{l})=(I_{k}\cup O_{k})\cap(I_{l}\cup O_{l})$ for all
$k,l\in\mathfrak{K}$ with $k\neq l$ (components are disjoint except for
interface places) and $I_{k}\cap I_{l}=\emptyset$ for all $k,l\in\mathfrak{K}$
with $k\neq l$ (mailboxes cannot be shared; any message has a unique
recipient).

Then the _asynchronous parallel composition_ of these components is defined by

$\Big{\|}_{i\in\mathfrak{K}}((S_{k},T_{k},F_{k},{M_{0}}_{k},\ell_{k}),I_{k},O_{k})=((S,T,F,{M_{0}},\ell),I,O)\vspace{-.5ex}$

with
$S\mathord{=}\bigcup_{k\in\mathfrak{K}}S_{k},~{}T\mathord{=}\bigcup_{k\in\mathfrak{K}}\\!T_{k},~{}F\mathord{=}\bigcup_{k\in\mathfrak{K}}F_{k},~{}M_{0}\mathord{=}\sum_{k\in\mathfrak{K}}{M_{0}}_{k},~{}\ell\mathord{=}\bigcup_{k\in\mathfrak{K}}\ell_{k}$
(componentwise union of all nets),
$I\mathord{=}\bigcup_{k\in\mathfrak{K}}I_{k}$ (we accept additional inputs
from outside), and
$O\mathord{=}\bigcup_{k\in\mathfrak{K}}O_{k}\setminus\bigcup_{k\in\mathfrak{K}}I_{k}$
(once fused with an input, $o\mathbin{\in}O_{I}$ is no longer an output).

###### Observation 5

$\|$ is associative.

This follows directly from the associativity of the (multi)set union operator.
$\Box$

We are now ready to define the class of nets representing systems of
asynchronously communicating sequential components.

######  Definition 4.3.

LSGA A Petri net $N$ is an _LSGA net_ (a _locally sequential globally
asynchronous net_) iff there exists an index set $\mathfrak{K}$ and sequential
components with interface $\mathcal{C}_{k},~{}k\mathbin{\in}\mathfrak{K}$,
such that $(N,I,O)=\|_{k\in\mathfrak{K}}\mathcal{C}_{k}$ for some $I$ and $O$.

Up to $\approx^{\Delta}_{bSTb}$—or any reasonable equivalence preserving
causality and branching time but abstracting from internal activity—the same
class of LSGA systems would have been obtained if we had imposed, in
Definition LABEL:df-component, that $I$, $O$ and $Q$ form a partition of $S$
and that ${\vphantom{I}}^{\bullet}I=\emptyset$. However, it is essential that
our definition allows multiple transitions of a component to read from the
same input place.

In the remainder of this section we give a more abstract characterisation of
Petri nets representing distributed systems, namely as _distributed_ Petri
nets, which we introduced in [7]. This will be useful in Section 5, where we
investigate distributability using this more semantic characterisation. We
show below that the concrete characterisation of distributed systems as LSGA
nets and this abstract characterisation agree.

Following [2], to arrive at a class of nets representing distributed systems,
we associate _localities_ to the elements of a net $N=(S,T,F,M_{0},\ell)$. We
model this by a function $D:S\cup T\rightarrow\textrm{Loc}$, with Loc a set of
possible locations. We refer to such a function as a _distribution_ of $N$.
Since the identity of the locations is irrelevant for our purposes, we can
just as well abstract from Loc and represent $D$ by the equivalence relation
$\equiv_{D}$ on $S\cup T$ given by $x\equiv_{D}y$ iff $D(x)=D(y)$.

Following [7], we impose a fundamental restriction on distributions, namely
that when two transitions can occur in one step, they cannot be co-located.
This reflects our assumption that at a given location actions can only occur
sequentially.

In [7] we observed that Petri nets incorporate a notion of synchronous
interaction, in that a transition can fire only by synchronously taking the
tokens from all of its preplaces. In general the behaviour of a net would
change radically if a transition would take its input tokens one by one—in
particular deadlocks may be introduced. Therefore we insist that in a
distributed Petri net, a transition and all its input places reside on the
same location. There is no reason to require the same for the output places of
a transition, for the behaviour of a net would not change significantly if
transitions were to deposit their output tokens one by one [7].

This leads to the following definition of a distributed Petri net.

######  Definition 4.4.

distributed[7] A Petri net $N=(S,T,F,M_{0},\ell)$ is _distributed_ iff there
exists a distribution $D$ such that

  * (1)

$\forall s\in S,~{}t\in T.~{}\hskip
1.0pts\in{\vphantom{t}}^{\bullet}t\Rightarrow t\equiv_{D}s$,

  * (2)

$\forall t,u\in T.~{}t\smile u\Rightarrow t\not\equiv_{D}u$.

A typical example of a net which is not distributed is shown in Figure 2 on
Page 2. Transitions $t$ and $v$ are concurrently executable and hence should
be placed on different locations. However, both have preplaces in common with
$u$ which would enforce putting all three transitions on the same location. In
fact, distributed nets can be characterised in the following semi-structural
way.

###### Observation 6

A Petri net is distributed iff there is no sequence $t_{0},\ldots,t_{n}$ of
transitions with $t_{0}\smile t_{n}$ and
${\vphantom{t_{i-1}}}^{\bullet}t_{i-1}\cap{\vphantom{t_{i}}}^{\bullet}t_{i}\neq\emptyset$
for $i=1,\ldots,n$. $\Box$

We proceed to show that the classes of LSGA nets and distributable nets
essentially coincide. That every LSGA net is distributed follows because we
can place each sequential component on a separate location. The following two
lemmas constitute a formal argument. Here we call a component with interface
$(N,I,O)$ distributed iff $N$ is distributed.

######  Lemma 4.5.

sequential component distributed Any sequential component with interface is
distributed.

######  Proof 4.6.

As a sequential component displays no concurrency, it suffices to co-locate
all places and transitions.

Lemma LABEL:lem-parcompdistributed states that the class of distributed nets
is closed under asynchronous parallel composition.

######  Lemma 4.7.

parcompdistributed Let $\mathcal{C}_{k}=(N_{k},I_{k},O_{k})$,
$k\mathbin{\in}\mathfrak{K}$, be components with interface, satisfying the
requirements of Definition LABEL:df-parcomp, which are all distributed. Then
$\|_{k\in\mathfrak{K}}\mathcal{C}_{k}$ is distributed.

######  Proof 4.8.

We need to find a distribution $D$ satisfying the requirements of Definition
LABEL:df-distributed.

Every component $\mathcal{C}_{k}$ is distributed and hence comes with a
distribution $D_{k}$. Without loss of generality the codomains of all $D_{k}$
can be assumed disjoint.

Considering each $D_{k}$ as a function from net elements onto locations, a
partial function $D_{k}^{\prime}$ can be defined which does not map any places
in $O_{k}$, denoting that the element may be located arbitrarily, and behaves
as $D_{k}$ for all other elements. As an output place has no posttransitions
within a component, any total function larger than (i.e. a superset of)
$D_{k}^{\prime}$ is still a valid distribution for $N_{k}$.

Now $D^{\prime}=\bigcup_{k\in\mathfrak{K}}D_{k}^{\prime}$ is a (partial)
function, as every place shared between components is an input place of at
most one. The required distribution $D$ can be chosen as any total function
extending $D^{\prime}$; it satisfies the requirements of Definition LABEL:df-
distributed since the $D_{k}$’s do.

######  Corollary 4.9.

LSGA distributed Every LSGA net is distributed. $\Box$

Conversely, any distributed net $N$ can be transformed in an LSGA net by
choosing co-located transitions with their pre- and postplaces as sequential
components and declaring any place that belongs to multiple components to be
an input place of component $N_{k}$ if it is a preplace of a transition in
$N_{k}$, and an output place of component $N_{l}$ if it is a postplace of a
transition in $N_{l}$ and not an input place of $N_{l}$. Furthermore, in order
to guarantee that the components are sequential in the sense of Definition
LABEL:df-component, an explicit control place is added to each
component—without changing behaviour—as explained below Definition LABEL:df-
component. It is straightforward to check that the asynchronous parallel
composition of all so-obtained components is an LSGA net, and that it is
equivalent to $N$ (using $\approx_{\mathscr{R}}$, $\approx^{\Delta}_{bSTb}$,
or any other reasonable equivalence).

######  Theorem 4.10.

bothdistributedequal For any distributed net $N$ there is an LSGA net
$N^{\prime}$ with $N^{\prime}\approx^{\Delta}_{bSTb}N$.

######  Proof 4.11.

Let $N=(S,T,F,M_{0},\ell)$ be a distributed net with a distribution $D$. Then
an equivalent LSGA net $N^{\prime}$ can be constructed by composing sequential
components with interfaces as follows.

For each equivalence class $[x]$ of net elements according to $D$ a sequential
component $(N_{[x]},I_{[x]},O_{[x]})$ is created. Each such component contains
one new and initially marked place $p_{[x]}$ which is connected via self-loops
to all transitions in $[x]$. The interface of the component is formed by
$I_{[x]}:=(S\cap[x])$111Alternatively, we could take
$I_{[x]}:={(T\backslash[x])}^{\bullet}\cap[x]$. and $O_{[x]}:={([x]\cap
T)}^{\bullet}\setminus[x]$. Formally,
$N_{[x]}:=(S_{[x]},T_{[x]},F_{[x]},{M_{0}}_{[x]},\ell_{[x]})$ with

  * •

$S_{[x]}=((S\cap[x])\cup O_{[x]}\cup\\{p_{[x]}\\}$,

  * •

$T_{[x]}=T\cap[x]$,

  * •

$F_{[x]}=F\mathop{\upharpoonright}(S_{[x]}\cup
T_{[x]})^{2}\cup\\{(p_{[x]},t),(t,p_{[x]})\mid t\in T_{[x]}\\}$,

  * •

${M_{0}}_{[x]}=(M_{0}\mathop{\upharpoonright}[x])\cup\\{p_{[x]}\\}$, and

  * •

$\ell_{[x]}=\ell\mathop{\upharpoonright}[x]$.

All components overlap at interfaces only, as the sole places not in an
interface are the newly created $p_{[x]}$. The $I_{[x]}$ are disjoint as the
equivalence classes $[x]$ are, so
$(N^{\prime},I^{\prime},O^{\prime}):=\|_{[x]\in(S\cup
T)/D}(N_{[x]},O_{[x]},I_{[x]})$ is well-defined. It remains to be shown that
$N^{\prime}\approx^{\Delta}_{bSTb}N$. The elements of $N^{\prime}$ are exactly
those of $N$ plus the new places $p_{[x]}$, which stay marked continuously
except when a transition from $[x]$ is firing, and never connect two
concurrently enabled transitions. Hence there exists a bijection between the
ST-markings of $N^{\prime}$ and $N$ that preserves the ST-transition relations
between them, i.e. the associated ST-LTSs are isomorphic. From this it follows
that $N^{\prime}\approx^{\Delta}_{bSTb}N$.

###### Observation 7

Every distributed Petri net is a structural conflict net. $\Box$

######  Corollary 4.12.

LSGA-structuralconflict Every LSGA net is a structural conflict net. $\Box$

Further on, we use a more liberal definition of a distributed net, called
_essentially distributed_. We will show that up to $\approx^{\Delta}_{bSTb}$
any essentially distributed net can be converted into a distributed net. In
[7] we employed an even more liberal definition of a distributed net, which we
call here _externally distributed_. Although we showed that up to step
readiness equivalence any externally distributed net can be converted into a
distributed net, this does not hold for $\approx^{\Delta}_{bSTb}$.

######  Definition 4.13.

externally distributed A net $N=(S,T,F,M_{0},\ell)$ is _essentially
distributed_ iff there exists a distribution $D$ satisfying (1) of Definition
LABEL:df-distributed and

  * ($2^{\prime}$)

$\forall t,u\in T.~{}t\smile u\wedge\ell(t)\neq\tau\Rightarrow
t\not\equiv_{D}u$.

It is _externally distributed_ iff there exists a distribution $D$ satisfying
(1) and

  * ($2^{\prime\prime}$)

$\forall t,u\in T.~{}t\smile u\wedge\ell(t),\ell(u)\neq\tau\Rightarrow
t\not\equiv_{D}u$.

Instead of ruling out co-location of concurrent transitions in general,
essentially distributed nets permit concurrency of internal
transitions—labelled $\tau$—at the same location. Externally distributed nets
even allow concurrency between external and internal transitions at the same
location. If the transitions $t$ and $v$ in the net of Figure 2 would both be
labelled $\tau$, the net would be essentially distributed, although not
distributed; in case only $v$ would be labelled $\tau$ the net would be
externally distributed but not essentially distributed. Essentially
distributed nets need not be structural conflict nets; in fact, _any_ net
without external transitions is essentially distributed.

The following proposition says that up to $\approx^{\Delta}_{bSTb}$ any
essentially distributed net can be converted into a distributed net.

######  Proposition 4.14.

essentiallydistributedequal For any essentially distributed net $N$ there is a
distributed net $N^{\prime}$ with $N^{\prime}\approx^{\Delta}_{bSTb}N$.

######  Proof 4.15.

The same construction as in the proof of Theorem LABEL:thm-
bothdistributedequal applies: $N^{\prime}$ differs from $N$ by the addition,
for each location $[x]$, of a marked place $p_{[x]}$ that is connected through
self-loops to all transitions at that location. This time there exists a
bijection between the _reachable_ ST-markings of $N^{\prime}$ and $N$ that
preserves the ST-transition relations between them. This bijection exists
because a reachable ST-marking is a pair $(M,U)$ with $U$ a sequence of
_external_ transitions only; this follows by a straightforward induction on
reachability by ST-transitions. From this it follows that
$N^{\prime}\approx^{\Delta}_{bSTb}N$.

Likewise, up to $\approx_{\mathscr{R}}$ any externally distributed net can be
converted into a distributed net.

######  Proposition 4.16.

externallydistributedequal[7] For any externally distributed net $N$ there is
a distributed net $N^{\prime}$ with $N^{\prime}\approx_{\mathscr{R}}N$.

######  Proof 4.17.

Again the same construction applies. This time there exists a bijection
between the markings of $N^{\prime}$ and $N$ that preserves the step
transition relations between them, i.e. the associated step transition systems
are isomorphic. Here we use that the transitions in the associated LTS involve
either a multiset of concurrently firing _external_ transitions, or a single
internal one. From this, step readiness equivalence follows.

The counterexample in Figure 2 shows that up to
$N^{\prime}\approx^{\Delta}_{bSTb}N$ not any externally distributed net can be
converted into a distributed net. Sequentialising the component with actions
$a$, $b$ and $\tau$ would disable the execution $\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}}$}}\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
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
c^{+}$\hskip 2.5pt}\hfil}}$}}$.

0.8$p$$q$

$a$

$t$

$b$

$u$

$c$

$v$

Figure 1: A fully marked M.

0.8$p$$q$

$a$

$t$

$b$

$u$

$\tau$

$v$$r$

$c$

$w$

Figure 2: Externally distributed, but not distributable.

######  Definition 4.18.

canonical Given any Petri net $N$, the _canonical co-location relation_
$\equiv_{C}$ on $N$ is the equivalence relation on the places and transitions
of $N$ _generated_ by Condition (1) of Definition LABEL:df-distributed, i.e.
the smallest equivalence relation $\equiv_{D}$ satisfying (1). The _canonical
distribution_ of $N$ is the distribution $C$ that maps each place or
transition to its $\equiv_{C}$-equivalence class.

###### Observation 8

A Petri net that is distributed (resp. essentially or externally distributed)
w.r.t. any distribution $D$, is distributed (resp. essentially or externally
distributed) w.r.t. its canonical distribution.

Hence a net is distributed (resp. essentially or externally distributed) iff
its canonical distribution $D$ satisfies Condition (2) of Definition LABEL:df-
distributed (resp. Condition ($2^{\prime}$) or ($2^{\prime\prime}$) of
Definition LABEL:df-externally_distributed).

##  5 Distributable Systems

We now consider Petri nets as specifications of concurrent systems and ask the
question which of those specifications can be implemented as distributed
systems. This question can be formalised as

> Which Petri nets are semantically equivalent to distributed nets?

Of course the answer depends on the choice of a suitable semantic equivalence.
Here we will answer this question using the two equivalences discussed in the
introduction. We will give a precise characterisation of those nets for which
we can find semantically equivalent distributed nets. For the negative part of
this characterisation, stating that certain nets are not distributable, we
will use step readiness equivalence, which is one of the simplest and least
discriminating equivalences imaginable that abstracts from internal actions,
but preserves branching time, concurrency and divergence to some small degree.
As explained in [7], giving up on any of these latter three properties would
make any Petri net distributable, but in a rather trivial and unsatisfactory
way. For the positive part, namely that all other nets are indeed
distributable, we will use the most discriminating equivalence for which our
implementation works, namely branching ST-bisimilarity with explicit
divergence, which is finer than step readiness equivalence. Hence we will
obtain the strongest possible results for both directions and it turns out
that the concept of distributability is fairly robust w.r.t. the choice of a
suitable equivalence: any equivalence notion between step readiness
equivalence and branching ST-bisimilarity with explicit divergence will yield
the same characterisation.

######  Definition 5.1.

distributable A Petri net $N$ is _distributable_ up to an equivalence
$\approx$ iff there exists a distributed net $N^{\prime}$ with
$N^{\prime}\approx N$.

Formally we give our characterisation of distributability by classifying which
finitary plain structural conflict nets can be implemented as distributed
nets, and hence as LSGA nets. In such implementations, we use invisible
transitions. We study the concept “distributable” for plain nets only, but in
order to get the largest class possible we allow non-plain implementations,
where a given transition may be split into multiple transitions carrying the
same label.

It is well known that sometimes a global protocol is necessary to implement
synchronous interaction present in system specifications. In particular, this
may be needed for deciding choices in a coherent way, when these choices
require agreement of multiple components. The simple net in Figure 2 shows a
typical situation of this kind. Independent decisions of the two choices might
lead to a deadlock. As remarked in [7], for this particular net there exists
no satisfactory distributed implementation that fully respects the reactive
behaviour of the original system. Indeed such M-structures, representing
interference between concurrency and choice, turn out to play a crucial rôle
for characterising distributability.

######  Definition 5.2.

fullM Let $N=(S,T,F,M_{0},\ell)$ be a Petri net. $N$ has a _fully reachable
pure M_ iff
$\exists t,u,v\in
T.{\vphantom{t}}^{\bullet}t\cap{\vphantom{u}}^{\bullet}u\neq\emptyset\wedge{\vphantom{u}}^{\bullet}u\cap{\vphantom{v}}^{\bullet}v\neq\emptyset\wedge{\vphantom{t}}^{\bullet}t\cap{\vphantom{v}}^{\bullet}v=\emptyset\wedge\exists
M\in[M_{0}\rangle.{\vphantom{t}}^{\bullet}t\cup{\vphantom{u}}^{\bullet}u\cup{\vphantom{v}}^{\bullet}v\subseteq
M$.

Note that Definition LABEL:df-fullM implies that $t\neq u$, $u\neq v$ and
$t\neq v$.

We now give an upper bound on the class of distributable nets by adopting a
result from [7].

######  Theorem 5.3.

trulysyngltfullm Let $N$ be a plain structural conflict Petri net. If $N$ has
a fully reachable pure M, then $N$ is not distributable up to step readiness
equivalence.

######  Proof 5.4.

In [7] this theorem was obtained for plain one-safe nets.222In [7] the theorem
was claimed and proven only for plain nets with a fully reachable _visible_
pure M; however, for plain nets the requirement of visibility is irrelevant.
The proof applies verbatim to plain structural conflict nets as well.

Since $\approx^{\Delta}_{bSTb}$ is finer than $\approx_{\mathscr{R}}$, this
result holds also for distributability up to $\approx^{\Delta}_{bSTb}$ (and
any equivalence between $\approx_{\mathscr{R}}$ and
$\approx^{\Delta}_{bSTb}$).

In the following, we establish that this upper bound is tight, and hence a
finitary plain structural conflict net is distributable iff it has no fully
reachable pure M. For this, it is helpful to first introduce macros in Petri
nets for reversibility of transitions.

###  5.1 Petri nets with reversible transitions

A _Petri net with reversible transitions_ generalises the notion of a Petri
net; its semantics is given by a translation to an ordinary Petri net, thereby
interpreting the reversible transitions as syntactic sugar for certain net
fragments. It is defined as a tuple $(S,T,\Omega,\mbox{\it\i},F,M_{0},\ell)$
with $S$ a set of places, $T$ a set of (reversible) transitions, labelled by
$\ell:T\rightarrow{\rm
Act}\stackrel{{\scriptstyle\mbox{\huge.}}}{{\cup}}\\{\tau\\}$, $\Omega$ a set
of _undo interfaces_ with the relation $\mbox{\it\i}\subseteq\Omega\times T$
linking interfaces to transitions, $M_{0}\mathbin{\in}{\rm Nature}^{S}$ an
initial marking, and

$F\\!:(S\times T\times\\{{\scriptstyle\it
in,~{}early,~{}late,~{}out,~{}far}\\}\rightarrow{\rm Nature})$

the flow relation. When $F(s,t,{\scriptstyle\it type})>0$ for
${\scriptstyle\it type}\in\\{{\scriptstyle\it
in,~{}early,~{}late,~{}out,~{}far}\\}$, this is depicted by drawing an arc
from $s$ to $t$, labelled with its arc weight $F(s,t,{\scriptstyle\it type})$,
of the form 0.7, 0.7, 0.7, 0.7, 0.7, respectively. For $t\mathbin{\in}T$ and
${\scriptstyle\it type}\in\\{{\scriptstyle\it
in,~{}early,~{}late,~{}out,~{}far}\\}$, the multiset of places $t^{\it
type}\mathbin{\in}{\rm Nature}^{S}$ is given by $t^{\it
type}(s)=F(s,t,{\scriptstyle\it type})$. When $s\mathbin{\in}t^{\it type}$ for
${\scriptstyle\it type}\in\\{{\scriptstyle\it in,~{}early,~{}late}\\}$, the
place $s$ is called a _preplace_ of $t$ of type type; when
$s\mathbin{\in}t^{\it type}$ for ${\scriptstyle\it type}\in\\{{\scriptstyle\it
out,~{}far}\\}$, $s$ is called a _postplace_ of $t$ of type type. For each
undo interface $\omega\mathbin{\in}\Omega$ and transition $t$ with
$\mbox{\it\i}(\omega,t)$ there must be places $\textsf{undo}_{\omega}(t)$,
$\textsf{reset}_{\omega}(t)$ and $\textsf{ack}_{\omega}(t)$ in $S$. A
transition with a nonempty set of interfaces is called _reversible_ ; the
other (_standard_) transitions may have pre- and postplaces of types in and
out only—for these transitions $t^{\it
in}\mathbin{=}{\vphantom{t}}^{\bullet}t$ and $t^{\it
out}\mathbin{=}{t}^{\bullet}$. In case $\Omega=\emptyset$, the net is just a
normal Petri net.

A global state of a Petri net with reversible transitions is given by a
marking $M\mathbin{\in}{\rm Nature}^{S}$, together with the state of each
reversible transition “currently in progress”. Each transition in the net can
fire as usual. A reversible transition can moreover take back (some of) its
output tokens, and be _undone_ and _reset_. When a transition $t$ fires, it
consumes $\sum_{{\scriptstyle\it type}\in\\{{\scriptstyle\it
in,~{}early,~{}late}\\}}F(s,t,{\scriptstyle\it type})$ tokens from each of its
preplaces $s$ and produces $\sum_{{\scriptstyle\it type}\in\\{{\scriptstyle\it
out,~{}far}\\}}F(s,t,{\scriptstyle\it type})$ tokens in each of its postplaces
$s$. A reversible transition $t$ that has fired can start its reversal by
consuming a token from $\textsf{undo}_{\omega}(t)$ for one of its interfaces
$\omega$. Subsequently, it can take back one by one a token from its
postplaces of type far. After it has retrieved all its output of type far, the
transition is undone, thereby returning $F(s,t,{\scriptstyle\it early})$
tokens in each of its preplaces $s$ of type early. Afterwards, by consuming a
token from $\textsf{reset}_{\omega}(t)$, for the same interface $\omega$ that
started the undo-process, the transition terminates its chain of activities by
returning $F(s,t,{\scriptstyle\it late})$ tokens in each of its late preplaces
$s$. At that occasion it also produces a token in $\textsf{ack}_{\omega}(t)$.
Alternatively, two tokens in $\textsf{undo}_{\omega}(t)$ and
$\textsf{reset}_{\omega}(t)$ can annihilate each other without involving the
transition $t$; this also produces a token in $\textsf{ack}_{\omega}(t)$. The
latter mechanism comes in action when trying to undo a transition that has not
yet fired.

Figure LABEL:fig-reversible shows the translation of a reversible transition
$t$ with $\ell(t)\mathbin{=}a$ into an ordinary net fragment.

0.8$(in)$$(late)$$(early)$$\textsf{undo}_{\omega}(t)$$\textsf{reset}_{\omega}(t)$$\textsf{ack}_{\omega}(t)$$(far)$$(out)$

$a$

$t$

$\omega$

0.8$f$$o$$i$$l$$e$$\textsf{take}(f,t)$

$\tau$

$t\cdot\textsf{undo}(f)$$\textsf{took}(f,t)$

$\tau$

$t\cdot\textsf{undo}_{\omega}$

$\tau$

$t\cdot\textsf{undone}$$\textsf{fired}(t)$$\rho(t)\\!$

$a$

$t\cdot\textsf{fire}$

$\tau$

$t\cdot\textsf{reset}_{\omega}$$\textsf{undo}_{\omega}(t)$$\rho_{\omega}(t)$

$\tau$

$t\cdot\textsf{elide}_{\omega}$$\textsf{ack}_{\omega}(t)$$\textsf{reset}_{\omega}(t)$$\forall
f\in t^{\,\it far}$$\forall o\in t^{out}$$\forall i\in t^{in}$$\forall l\in
t^{late}$$\forall e\in
t^{early}$$\forall\omega.\,\mbox{\it\i}(\omega,t)$$withreversibletransitionstranslatesintothePetrinetcontainingallplaces$S$,initiallymarkedasindicatedby$M_0$,allstandardtransitionsin$T$,labelledaccordingto$ℓ$,alongwiththeirpre-
andpostplaces,andfurthermoreallnetelementsmentionedinTable~{}\ref{tab-
reversible}.Here\hypertarget{Tback}{}$T^←$denotesthesetofreversibletransitionsin$T.

###  5.2 The conflict replicating implementation

Now we establish that a finitary plain structural conflict net that has no
fully reachable pure M is distributable. We do this by proposing the _conflict
replicating implementation_ of any such net, and show that this implementation
is always (a) essentially distributed, and (b) equivalent to the original net.
In order to get the strongest possible result, for (b) we use branching ST-
bisimilarity with explicit divergence.

0.8$\begin{array}[]{l}\displaystyle\forall j\in T^{\prime}\\\ \forall
p\in{\vphantom{j}}^{\bullet}j\\\ \forall h<^{\\#}j\\\ \forall i\leq^{\\#}j\\\
\forall k\geq^{\\#}j\\\ \forall l>^{\\#}j\\\ \forall
q\in{\vphantom{i}}^{\bullet}i\\\ \forall c\in{q}^{\bullet}\\\ \forall
r\in{i\,}^{\bullet}\\\ \forall
t\in\Omega_{i}:=\begin{array}[t]{@{}l@{}}\\{\textsf{initialise}_{c}\mid
c\mathbin{\raisebox{0.0pt}[0.0pt][0.0pt]{$\stackrel{{\scriptstyle\\#}}{{=}}$}}i\\}+\mbox{}\\\
\\{\textsf{transfer}^{b}_{c}\mid
b<^{\\#}c\mathbin{\raisebox{0.0pt}[0.0pt][0.0pt]{$\stackrel{{\scriptstyle\\#}}{{=}}$}}i\\}\end{array}\\\
\forall
u\mathbin{\raisebox{0.0pt}[0.0pt][0.0pt]{$\stackrel{{\scriptstyle\\#}}{{=}}$}}j\\\
\end{array}$$F(p,j)$$F(i,r)$$F(q,i)$$p$

$\tau$

$\textsf{distribute}_{p}$$p_{j}$$\textsf{pre}^{j}_{k}$$\pi_{j}$

$\tau$

$\textsf{initialise}_{j}$

$u$$\textsf{undo}_{u}(\textsf{initialise}_{j})$$\textsf{reset}_{u}(\textsf{initialise}_{j})$$\textsf{ack}_{u}(\textsf{initialise}_{j})$$\textsf{trans}^{h}_{j}\textsf{-in}$$\pi_{h\\#j}$

$\tau$

$\textsf{transfer}^{h}_{j}$

$u$$\textsf{undo}_{u}(\textsf{transfer}^{h}_{j})$$\textsf{reset}_{u}(\textsf{transfer}^{h}_{j})$$\textsf{ack}_{u}(\textsf{transfer}^{h}_{j})$$\textsf{trans}^{h}_{j}\textsf{-out}$$\textsf{pre}^{i}_{j}$$\pi_{j\\#l}$

$\ell(i)$

$\textsf{execute}^{i}_{j}$$\textsf{undo}_{i}(t)$$\textsf{fetch}_{i,j}^{q,c}\textsf{-in}$$q_{c}$

$\tau$

$\textsf{fetch}_{i,j}^{q,c}$$\textsf{fetch}_{i,j}^{q,c}\textsf{-out}$

$\tau$

$\textsf{fetched}^{i}_{j}$$\textsf{ack}_{i}(t)$$\textsf{reset}_{i}(t)$

$\tau$

$\textsf{finalise}^{i}$$r$

Figure 3: The conflict replicating implementation

To define the conflict replicating implementation of a net
$N=(S,T,F,M_{0},\ell)$ we fix an arbitrary well-ordering $<$ on its
transitions. We let $b,c,g,h,i,j,k,l$ range over these ordered transitions,
and write

  * –

$i\mathbin{\\#}j$ iff $i\neq
j\wedge{\vphantom{i}}^{\bullet}i\cap{\vphantom{j}}^{\bullet}j\neq\emptyset$
(transitions $i$ and $j$ are _in conflict_), and
$i\mathbin{\raisebox{0.0pt}[0.0pt][0.0pt]{$\stackrel{{\scriptstyle\\#}}{{=}}$}}j$
iff $i\mathbin{\\#}j\vee i\mathbin{=}j$,

  * –

$i<^{\\#}\\!j$ iff $i<j\wedge i\mathbin{\\#}j$, and $i\leq^{\\#}\\!j$ iff
$i<^{\\#}\\!j\vee i=j$.

Figure 3 shows the conflict replicating implementation of $N$. It is presented
as a Petri net

$\mathcal{I}(N)=(S^{\prime},T^{\prime},F^{\prime},\Omega,\mbox{\it\i},M^{\prime}_{0},\ell^{\prime})$

with reversible transitions. The set $\Omega$ of undo interfaces is $T$, and
for $i\mathbin{\in}\Omega$ we have $\mbox{\it\i}(i,t)$ iff
$t\mathbin{\in}\Omega_{i}$, where the sets of transitions
$\Omega_{i}\mathbin{\in}{\rm Nature}^{T^{\prime}}$ are specified in Figure 3.
The implementation $\mathcal{I}(N)$ inherits the places of $N$ (i.e.
$S^{\prime}\supseteq S$), and we postulate that
$M^{\prime}_{0}\mathord{\upharpoonright}S=M_{0}$. Given this, Figure 3 is not
merely an illustration of $\mathcal{I}(N)$—it provides a complete and accurate
description of it, thereby defining the conflict replicating implementation of
any net. In interpreting this figure it is important to realise that net
elements are completely determined by their name (identity), and exist only
once, even if they show up multiple times in the figure. For instance, the
place $\pi_{h\\#j}$ with $h\mathord{=}2$ and $j\mathord{=}5$ (when using
natural numbers for the transitions in $T$) is the same as the place
$\pi_{j\\#l}$ with $j\mathord{=}2$ and $l\mathord{=}5$; it is a standard
preplace of $\textsf{execute}^{i}_{2}$ (for all $i\leq^{\\#}\\!2$), a standard
postplace of $\textsf{fetched}^{i}_{2}$, as well as a late preplace of
$\textsf{transfer}^{2}_{5}$. A description of this net after expanding the
macros for reversible transitions appears in Table 6 on Page 6. The rôle of
the transitions $\textsf{distribute}_{p}$ for $p\mathbin{\in}S$ is to
distribute a token in $p$ to copies $p_{j}$ of $p$ in the localities of all
transitions $j\mathbin{\in}T$ with $p\mathbin{\in}{\vphantom{j}}^{\bullet}j$.
In case $j$ is enabled in $N$, the transition $\textsf{initialise}_{j}$ will
become enabled in $\mathcal{I}(N)$. These transitions put tokens in the places
$\textsf{pre}^{j}_{k}$, which are preconditions for all transitions
$\textsf{execute}^{j}_{k}$, which model the execution of $j$ at the location
of $k$. When two conflicting transitions $h$ and $j$ are both enabled in $N$,
the first steps $\textsf{initialise}_{h}$ and $\textsf{initialise}_{j}$
towards their execution in $\mathcal{I}(N)$ can happen in parallel. To prevent
them from executing both, $\textsf{execute}^{j}_{j}$ (of $j$ at its own
location) is only possible after $\textsf{transfer}^{h}_{j}$, which disables
$\textsf{execute}^{h}_{h}$. The main idea behind the conflict replicating
implementation is that a transition $h\mathbin{\in}T$ is primarily executed by
a sequential component of its own, but when a conflicting transition $j$ gets
enabled, the sequential component implementing $j$ may “steal” the possibility
to execute $h$ from the home component of $h$, and keep the options to do $h$
and $j$ open until one of them occurs. To prevent $h$ and $j$ from stealing
each other’s initiative, which would result in deadlock, a global asymmetry is
built in by ordering the transitions. Transition $j$ can steal the initiative
from $h$ only when $h<j$. In case $j$ is also in conflict with a transition
$l$, with $j<l$, the initiative to perform $j$ may subsequently be stolen by
$l$. In that case either $h$ and $l$ are in conflict too—then $l$ takes
responsibility for the execution of $h$ as well—or $h$ and $l$ are
concurrent—in that case $h$ will not be enabled, due to the absence of fully
reachable pure Ms in $N$. The absence of fully reachable pure Ms also
guarantees that it cannot happen that two concurrent transitions $j$ and $k$
both steal the initiative from an enabled transition $h$. After the firing of
$\textsf{execute}^{i}_{j}$ all tokens that were left behind in the process of
carefully orchestrating this firing will have to be cleaned up, in order to
prepare the net for the next activity in the same neighbourhood. This is the
reason for the reversibility of the transitions preparing the firing of
$\textsf{execute}^{i}_{j}$. Hence there is an undo interface for each
transition $i\in T^{\prime}$, cleaning up the mess made in preparation of
firing $\textsf{execute}^{i}_{j}$ for some $j\geq^{\\#}i$. $\Omega_{i}$ is the
multiset of all transitions $t$ that could possibly have contributed to this.
For each of them the undo interface $i$ is activated, by
$\textsf{execute}^{i}_{j}$ depositing a token in $\textsf{undo}_{i}(t)$. After
all preparatory transitions that have fired are undone, tokens appear in the
places $p_{c}$ for all $p\mathbin{\in}{\vphantom{i}}^{\bullet}i$ and
$c\mathbin{\in}{p}^{\bullet}$. These are collected by
$\textsf{fetch}_{i,j}^{p,c}$, after which all transitions in $\Omega_{i}$ get
a reset signal. Those that have fired and were undone are reset, and those
that never fired perform $\textsf{elide}_{i}(t)$. In either case a token
appears in $\textsf{ack}_{i}(t)$. These are collected by
$\textsf{finalise}^{i}$, which finishes the process of executing $i$ by
depositing tokens in its postplaces.

0.8

$p$$q$$r$$s$$v$$x$$y$$z$

$a$

$1$

$b$

$2$

$c$

$3$

$d$

$4$

$e$

$5$and more powerful. By means of a simplification a similar method can be
obtained, also in three steps, for establishing the equivalence of two Petri
nets up to interleaving branching bisimilarity with explicit divergence. This
is elaborated at the end of this section.

######  Definition 5.5.

deterministic A labelled transition system
$(\mathfrak{S},\mathfrak{T},\mathfrak{M_{0}})$ is called _deterministic_ if
for all reachable states $\mathfrak{M}\in[\mathfrak{M_{0}}\rangle$ we have
$\mathfrak{M}\arrownot\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\tau$\hskip 2.5pt}\hfil}}$}}$ and if
$\mathfrak{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 a$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}$ and
$\mathfrak{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 a$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\prime\prime}$ for some $a\in\mathfrak{Act}$
then $\mathfrak{M}^{\prime}=\mathfrak{M}^{\prime\prime}$.

Deterministic systems may not have reachable $\tau$-transitions at all; this
way, if $\mathfrak{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\sigma$\hskip 2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}$ and
$\mathfrak{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\sigma$\hskip 2.5pt}\hfil}}$}}\mathfrak{M}^{\prime\prime}$
for some $\sigma\in\mathfrak{Act}^{*}$ then
$\mathfrak{M}^{\prime}=\mathfrak{M}^{\prime\prime}$. Note that the labelled
transition system associated to a plain Petri net is deterministic; the same
applies to the ST-LTS, the split LTS or the step LTS associated to such a net.

######  Lemma 5.6.

plain branching bisimilarity Let
$(\mathfrak{S}_{1},\mathfrak{T}_{1},\mathfrak{M_{0}}_{1})$ and
$(\mathfrak{S}_{2},\mathfrak{T}_{2},\mathfrak{M_{0}}_{2})$ be two labelled
transition systems, the latter being deterministic. Suppose there is a
relation $\mathcal{B}\,\subseteq\mathfrak{S}_{1}\times\mathfrak{S}_{2}$ such
that

  1. (a)

$\mathfrak{M_{0}}_{1}\mathcal{B}\,\mathfrak{M_{0}}_{2}$,

  2. (b)

if $\mathfrak{M}_{1}\mathcal{B}\,\mathfrak{M}_{2}$ and
$\mathfrak{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\tau$\hskip 2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}_{1}$ then
$\mathfrak{M}^{\prime}_{1}\mathcal{B}\,\mathfrak{M}_{2}$,

  3. (c)

if $\mathfrak{M}_{1}\mathcal{B}\,\mathfrak{M}_{2}$ and
$\mathfrak{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 a$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}_{1}$ for some $a\in\mathfrak{Act}$ then
$\exists\mathfrak{M}^{\prime}_{2}.~{}\mathfrak{M}_{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$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}_{2}\wedge\mathfrak{M}^{\prime}_{1}\mathcal{B}\,\mathfrak{M}^{\prime}_{2}$,

  4. (d)

if $\mathfrak{M}_{1}\mathcal{B}\,\mathfrak{M}_{2}$ and
$\mathfrak{M}_{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$\hskip
2.5pt}\hfil}}$}}$ for some $a\in\mathfrak{Act}$ then either
$\mathfrak{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 a$\hskip
2.5pt}\hfil}}$}}$ or $\mathfrak{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\tau$\hskip 2.5pt}\hfil}}$}}$

  5. (e)

and there is no infinite sequence
$\mathfrak{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\tau$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}_{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\tau$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\prime\prime}_{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\tau$\hskip 2.5pt}\hfil}}$}}\cdots$ with
$\mathfrak{M}_{1}\mathcal{B}\,\mathfrak{M}_{2}$ for some $\mathfrak{M}_{2}$.

Then $\mathcal{B}\,$ is a branching bisimulation, and the two LTSs are
branching bisimilar with explicit divergence.

  * Proof:

It suffices to show that $\mathcal{B}\,$ satisfies Conditions 1–3 of
Definition LABEL:df-branching_LTS; the condition on explicit divergence
follows immediately from (e), using that a deterministic LTS admits no
divergence at all.

    1. 1.

By (a).

    2. 2.

In case $\alpha=\tau$ this follows directly from (b), and otherwise from (c).
In both cases $\mathfrak{M}^{\dagger}_{2}:=\mathfrak{M}_{2}$ and when
$\alpha=\tau$ also $\mathfrak{M}^{\prime}_{2}:=\mathfrak{M}_{2}$.

    3. 3.

Suppose $\mathfrak{M}_{1}\mathcal{B}\,\mathfrak{M}_{2}$ and
$\mathfrak{M}_{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\alpha$\hskip 2.5pt}\hfil}}$}}\mathfrak{M}^{\prime}_{2}$.
Since $(\mathfrak{S}_{2},\mathfrak{T}_{2},\mathfrak{M_{0}}_{2})$ is
deterministic, $\alpha=a\in{\rm Act}$. By (d) we have either
$\mathfrak{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 a$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{1}_{1}$ or
$\mathfrak{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\tau$\hskip 2.5pt}\hfil}}$}}\mathfrak{M}^{1}_{1}$ for some
$\mathfrak{M}^{1}_{1}\in\mathfrak{S}_{1}$. In the latter case (b) yields
$\mathfrak{M}^{1}_{1}\mathcal{B}\,\mathfrak{M}_{2}$, and using (d) again,
either $\mathfrak{M}^{1}_{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$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{2}_{1}$ or
$\mathfrak{M}^{1}_{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\tau$\hskip 2.5pt}\hfil}}$}}\mathfrak{M}^{2}_{1}$ for some
$\mathfrak{M}^{2}_{1}\in\mathfrak{S}_{1}$. Repeating this argument, if the
choice between $a$ and $\tau$ is made $k$ times in favour of $\tau$ (with
$k\geq 0$), we obtain $\mathfrak{M}^{k}_{1}\mathcal{B}\,\mathfrak{M}_{2}$
(where $\mathfrak{M}^{0}_{1}:=\mathfrak{M}_{1}$) and either
$\mathfrak{M}^{k}_{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$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{k+1}_{1}$ or
$\mathfrak{M}^{k}_{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\tau$\hskip 2.5pt}\hfil}}$}}\mathfrak{M}^{k+1}_{1}$. By (e),
at some point the choice must be made in favour of $a$, say at
$\mathfrak{M}^{k}_{1}$. Thus $\mathfrak{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$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{k}_{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$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{k+1}_{1}$, with
$\mathfrak{M}^{k}_{1}\mathcal{B}\,\mathfrak{M}_{2}$. We take
$\mathfrak{M}^{\dagger}_{1}$ and $\mathfrak{M}^{\prime}_{1}$ from Definition
LABEL:df-branching_LTS to be $\mathfrak{M}^{k}_{1}$ and
$\mathfrak{M}^{k+1}_{1}$. It remains to show that
$\mathfrak{M}^{k+1}_{1}\mathcal{B}\,\mathfrak{M}^{\prime}_{2}$. By (c) there
is an $\mathfrak{M}^{\prime\prime}_{2}\in\mathfrak{S}_{2}$ with
$\mathfrak{M}_{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$\hskip
2.5pt}\hfil}}$}}\mathfrak{M}^{\prime\prime}_{2}$ and
$\mathfrak{M}^{k+1}_{1}\mathcal{B}\,\mathfrak{M}^{\prime\prime}_{2}$. Since
$(\mathfrak{S}_{2},\mathfrak{T}_{2},\mathfrak{M_{0}}_{2})$ is deterministic,
$\mathfrak{M}^{\prime}_{2}=\mathfrak{M}^{\prime\prime}_{2}$. $\Box$

######  Lemma 5.7.

1ST Let $N=(S,T,F,M_{0},\ell)$ and
$N^{\prime}=(S^{\prime},T^{\prime},F^{\prime},M^{\prime}_{0},\ell^{\prime})$
be two nets, $N^{\prime}$ being plain. Suppose there is a relation
$\mathcal{B}\,\subseteq({\rm Nature}^{S}\times{\rm Nature}^{T})\times({\rm
Nature}^{S^{\prime}}\times{\rm Nature}^{T^{\prime}})$ such that

  1. (a)

$(M_{0},\emptyset)\mathcal{B}\,(M^{\prime}_{0},\emptyset)$,

  2. (b)

if $(M_{1},U_{1})\mathcal{B}\,(M_{1}^{\prime},U^{\prime}_{1})$ and
$(M_{1},U_{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\tau$\hskip 2.5pt}\hfil}}$}}(M_{2},U_{2})$ then
$(M_{2},U_{2})\mathcal{B}\,(M_{1}^{\prime},U^{\prime}_{1})$,

  3. (c)

if $(M_{1},U_{1})\mathcal{B}\,(M_{1}^{\prime},U^{\prime}_{1})$ and
$(M_{1},U_{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\eta$\hskip 2.5pt}\hfil}}$}}(M_{2},U_{2})$ for some
$\eta\in{\rm Act}^{\pm}$
then
$\exists(M^{\prime}_{2},U^{\prime}_{2}).~{}(M^{\prime}_{1},U^{\prime}_{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\eta$\hskip
2.5pt}\hfil}}$}}(M^{\prime}_{2},U^{\prime}_{2})\wedge(M_{2},U_{2})\mathcal{B}\,(M_{2}^{\prime},U^{\prime}_{2})$,

  4. (d)

if $(M_{1},U_{1})\mathcal{B}\,(M_{1}^{\prime},U^{\prime}_{1})$ and
$(M^{\prime}_{1},U^{\prime}_{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\eta$\hskip 2.5pt}\hfil}}$}}$ with $\eta\in{\rm Act}^{\pm}$
then either $\mathord{(M_{1},U_{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\eta$\hskip 2.5pt}\hfil}}$}}}$ or
$\mathord{(M_{1},U_{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\tau$\hskip 2.5pt}\hfil}}$}}}$

  5. (e)

and there is no infinite sequence $(M,U)\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\tau$\hskip
2.5pt}\hfil}}$}}(M_{1},U_{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\tau$\hskip
2.5pt}\hfil}}$}}(M_{2},U_{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\tau$\hskip 2.5pt}\hfil}}$}}\cdots$ with
$(M,U)\mathcal{B}\,(M^{\prime},U^{\prime})$ for some
$(M^{\prime},U^{\prime})$.

Then $\mathcal{B}\,$ is a branching split bisimulation, and
$N\approx^{\Delta}_{bSTb}N^{\prime}$.

######  Proof 5.8.