# Place Bisimilarity is Decidable, Indeed!

Roberto Gorrieri
Dipartimento di Informatica — Scienza e Ingegneria
Università di Bologna,
Mura A. Zamboni, 7, 40127 Bologna, Italy<EMAIL_ADDRESS>
###### Abstract

Place bisimilarity $\sim_{p}$ is a behavioral equivalence for finite Petri
nets, originally proposed in [2], that, differently from all the other
behavioral relations proposed so far, is not defined over the markings of a
finite net, rather over its places, which are finitely many. Place
bisimilarity $\sim_{p}$ was claimed decidable in [2], but its decidability was
not really proved. We show that it is possible to decide $\sim_{p}$ with a
simple algorithm, which essentially scans all the place relations (which are
finitely many) to check whether they are place bisimulations. We also show
that $\sim_{p}$ does respect the intended causal semantics of Petri nets, as
it is finer than causal-net bisimilarity [19]. Moreover, we propose a slightly
coarser variant, we call d-place bisimilarity $\sim_{d}$, that we conjecture
to be the coarsest equivalence, fully respecting causality and branching time
(as it is finer than fully-concurrent bisimilarity [5]), to be decidable on
finite Petri nets. Finally, two even coarser variants are discussed, namely
i-place and i-d-place bisimilarities, which are still decidable, do preserve
the concurrent behavior of Petri nets, but do not respect causality. These
results open the way towards formal verification (by equivalence checking) of
distributed systems modeled by finite Petri nets.

##  1 Introduction

There is widespread agreement that a very natural equivalence relation for
sequential, nondeterministic systems is bisimulation equivalence [34, 30],
defined over the semantic model of labeled transition systems [26] (LTSs, for
short). Bisimulation equivalence, which fully respects the branching structure
of systems, is defined coinductively, has a nice fixpoint characterization, is
easily decidable for finite-state LTSs, even decidable on some classes of
infinite state systems.

When considering distributed systems, one very natural semantic model is given
by finite Petri nets (see, e.g., [35, 37, 16]), in particular finite
Place/Transition Petri nets [9] (P/T nets, for short), a distributed model of
computation that can represent a class of distributed systems where the number
of sequential components can grow unboundedly. Petri nets have been
extensively used for the modeling and analysis of real distributed systems
(see, e.g., [39, 38] and the references therein). However, (almost) all the
behavioral equivalence relations that were defined on finite P/T nets (e.g.,
in the spectrum ranging from interleaving bisimilarity to fully concurrent
bisimilarity [5]) are relations over the global states of the net, called
markings (possibly decorated with some history information), which are usually
infinitely many, and so, not surprisingly, these equivalence relations are all
undecidable, as observed by Janc̆ar [23] and Esparza [10]. Indeed, by these
observations, it seems impossible to algorithmically compare the behavior of
finite P/T nets, in order to verify the correctness of a distributed system by
computing a behavioral equivalence relation between its specification net and
its implementation net, i.e., by means of equivalence checking, a well-known
formal verification technique. We want to contradict this idea by showing that
this is possible, at least in principle.

As a matter of fact, one relevant exception exists: place bisimilarity,
originating from an idea by Olderog [32] (under the name of strong
bisimilarity) and then refined by Autant, Belmesk and Schnoebelen [2], which
is an equivalence over markings, based on relations over the finite set of net
places, rather than over the (possibly infinite) set of net markings. This
equivalence is very natural and intuitive: as a place can be interpreted as a
sequential process type (and each token in this place as an instance of a
sequential process of that type), a place bisimulation essentially states
which kinds of sequential processes (composing the distributed system
represented by the Petri net) are to be considered as equivalent.

Informally, a binary relation $R$ over the set $S$ of places is a place
bisimulation if for all markings $m_{1}$ and $m_{2}$ which are bijectively
related via $R$ (denoted by $(m_{1},m_{2})\in R^{\oplus}$, where $R^{\oplus}$
is called the additive closure of $R$), if $m_{1}$ can perform transition
$t_{1}$, reaching marking $m_{1}^{\prime}$, then $m_{2}$ can perform a
transition $t_{2}$, reaching marking $m_{2}^{\prime}$, such that the pre-sets
of $t_{1}$ and $t_{2}$ are related by $R^{\oplus}$ (i.e.,
$(\mbox{${}^{\bullet}t_{1}$},\mbox{${}^{\bullet}t_{2}$})\in R^{\oplus})$, the
label of $t_{1}$ and $t_{2}$ is the same, the post-sets of $t_{1}$ and $t_{2}$
are related by $R^{\oplus}$ (i.e.,
$(\mbox{$t_{1}^{\bullet}$},\mbox{$t_{2}^{\bullet}$})\in R^{\oplus})$, and also
for the reached markings we have $(m_{1}^{\prime},m_{2}^{\prime})\in
R^{\oplus}$; and symmetrically if $m_{2}$ moves first. Two markings $m_{1}$
and $m_{2}$ are place bisimilar, denoted by $m_{1}\sim_{p}m_{2}$, if a place
bisimulation $R$ exists such that $(m_{1},m_{2})\in R^{\oplus}$. Place
bisimilarity does respect the expected causal behavior of Petri nets; as a
matter of fact, we show that place bisimilarity is slightly finer than causal-
net bisimilarity [14, 19] (or, equivalently, structure preserving bisimilarity
[14]), in turn slightly finer than fully-concurrent bisimilarity [5] (or,
equivalently, history-preserving bisimilarity [36, 12, 8]).

Place bisimilarity is an equivalence relation, but its definition is not
coinductive because the union of place bisimulations may be not a place
bisimulation; so, in general, there is not one single largest place
bisimulation, rather many maximal place bisimulations. In fact, place
bisimilarity is the relation on markings obtained by the union of the additive
closure of each maximal place bisimulation. As a consequence, the classic
algorithms for computing the coinductive bisimulation equivalence on LTSs [24,
33] cannot be adapted to compute place bisimilarity.

Place bisimilarity $\sim_{p}$ was claimed decidable in [2] and a polynomial-
time algorithm was presented in [3] to this aim. To be precise, the algorithm
in [3] is tailored for i-place bisimilarity $\sim_{i}$ (cf. Section 7), even
if it is argued that this algorithm can be easily adapted for deciding also
place bisimilarity $\sim_{p}$. However, (the variant of) the algorithm in [3]
does not characterize $\sim_{p}$, rather the subequivalence
$\sim_{p_{eq}}\subseteq\sim_{p}$ corresponding to the only maximal place
bisimulation which is also an equivalence relation (which is unique, indeed
[2]); hence, the decidability of place bisimilarity was not proved.

The main contribution of this paper is to show that $\sim_{p}$ is decidable
for finite P/T nets, indeed. The proof idea is as follows. Note that a place
relation $R\subseteq S\times S$ is finite if the set $S$ of places is finite;
hence, there are finitely many place relations for a finite net. We can list
all these place relations, say $R_{1},R_{2},\ldots R_{n}$. It is possible to
decide whether a place relation $R_{i}$ in this list is a place bisimulation
by checking two finite conditions over a finite number of marking pairs: this
is a non-obvious observation, as a place bisimulation requires that the place
bisimulation game holds for the infinitely many pairs $(m_{1},m_{2})$
belonging to $R_{i}^{\oplus}$. Hence, to decide whether $m_{1}\sim_{p}m_{2}$,
it is enough to check, for $i=$ $1,\ldots n$, whether $R_{i}$ is a place
bisimulation and, in such a case, whether $(m_{1},m_{2})\in R_{i}^{\oplus}$.

Moreover, we propose a novel, slightly coarser variant, we call d-place
bisimilarity and denote by $\sim_{d}$, that we conjecture to be the coarsest,
sensible (i.e., fully respecting causality and branching time) equivalence to
be decidable on finite P/T Petri nets (without silent moves). Essentially, a
d-place bisimulation is a relation on the set whose elements are the places
and the empty marking, which is considered as an additional dummy place. This
weaker variant is still finer than fully-concurrent bisimilarity [5]. The
decidability proof of d-place bisimilarity $\sim_{d}$ is very similar to that
of place bisimilarity $\sim_{p}$.

Finally, we recall the coarsest variant of place bisimilarity proposed in [3],
namely i-place bisimilarity $\sim_{i}$. An i-place bisimulation $R$ is a
relation such that $R^{\oplus}$ is an interleaving bisimulation. We argue that
i-place bisimilarity $\sim_{i}$ is still decidable, by adapting the same proof
technique we provided for deciding place bisimilarity $\sim_{p}$. However,
$\sim_{i}$ is not fully satisfactory: even if it respects the branching time,
it does not respect causality. As a last minor contribution, we propose an
even coarser decidable variant, called i-d-place bisimilarity $\sim_{id}$,
that is finer than step bisimilarity $\sim_{s}$ (originally proposed in [31])
and so it preserves the concurrent behavior of nets (but not causality).
Indeed, $\sim_{id}$ is the coarsest decidable equivalence defined so far on
finite P/T Petri nets respecting concurrency and the branching time.

$\sim_{p}$$\sim_{cn}$$\sim_{d}$$\sim_{i}$$\sim_{id}$$\sim_{fc}$$\sim_{s}$$\sim_{int}$
Figure 1: The diagram with the 8 behavioral equivalences studied in this paper

Figure 1 summarizes the relations among the eight different behavioral
equivalences we are studying in this paper, where the top element is the most
discriminating one (namely, place bisimilarity $\sim_{p}$) and the bottom
element is the coarsest one (namely, interleaving bisimilarity $\sim_{int}$).
Note that the equivalences based on place relations (namely, place
bisimilarity $\sim_{p}$, d-place bisimilarity $\sim_{d}$, i-place bisimilarity
$\sim_{i}$ and i-d-place bisimilarity $\sim_{id}$) are all decidable, while
fully-concurrent bisimilarity $\sim_{fc}$, step bisimilarity $\sim_{s}$ and
interleaving bisimilarity $\sim_{int}$ are not; to complete the picture, the
decidability of causal-net bisimilarity $\sim_{cn}$ is an open problem.

The paper is organized as follows. Section 2 recalls the basic definitions
about Petri nets, including their interleaving, concurrent and causal
semantics. Section 3 deals with place bisimilarity, shows that it is an
equivalence relation, that it is not coinductive, and, by means of examples,
shows that $\sim_{p}$ is different from $\sim_{p_{eq}}$, i.e., the only
maximal place bisimulation which is also an equivalence relation
(algorithmically characterized in [3]). Section 4 proves that place
bisimilarity implies causal-net bisimilarity. Section 5 proves that $\sim_{p}$
is decidable. Section 6 introduces the coarser d-place bisimilarity $\sim_{d}$
and proves that it implies fully-concurrent bisimilarity and that it is still
decidable. Section 7 recalls i-place bisimilarity from [3], introduces the
newly proposed coarser variant i-d-place bisimilarity, shows that the latter
implies step bisimilarity and hints that they are both decidable, too.
Finally, Section 8 discusses the pros and cons of place bisimilarity,
overviews related literature and hints some possible future research.

##  2 Petri Nets

###### Definition 1

(Multiset) Let ${\mathbb{N}}$ be the set of natural numbers. A multiset over a
finite set $S$ is a function $m:S\rightarrow{\mathbb{N}}$. The support set
$dom(m)$ of $m$ is $\\{s\in S\;\;\big{|}\;\;m(s)\neq 0\\}$. The set of all
multisets over $S$, denoted by ${\mathcal{M}}(S)$, is ranged over by $m$. We
write $s\in m$ if $m(s)>0$. The multiplicity of $s$ in $m$ is given by the
number $m(s)$. The size of $m$, denoted by $|m|$, is the number $\sum_{s\in
S}m(s)$, i.e., the total number of its elements. A multiset $m$ such that
$dom(m)=\emptyset$ is called empty and is denoted by $\theta$. We write
$m\subseteq m^{\prime}$ if $m(s)\leq m^{\prime}(s)$ for all $s\in S$.

Multiset union $\\_\oplus\\_$ is defined as follows: $(m\oplus m^{\prime})(s)$
$=m(s)+m^{\prime}(s)$; it is commutative, associative and has $\theta$ as
neutral element. Multiset difference $\\_\ominus\\_$ is defined as follows:
$(m_{1}\ominus m_{2})(s)=max\\{m_{1}(s)-m_{2}(s),0\\}$. The scalar product of
a number $j$ with $m$ is the multiset $j\cdot m$ defined as $(j\cdot
m)(s)=j\cdot(m(s))$. By $s_{i}$ we also denote the multiset with $s_{i}$ as
its only element. Hence, a multiset $m$ over $S=\\{s_{1},\ldots,s_{n}\\}$ can
be represented as $k_{1}\cdot s_{1}\oplus k_{2}\cdot s_{2}\oplus\ldots\oplus
k_{n}\cdot s_{n}$, where $k_{j}=m(s_{j})\geq 0$ for $j=1,\ldots,n$.  $\Box$

###### Definition 2

(Place/Transition Petri net) A labeled Place/Tran-sition Petri net (P/T net
for short) is a tuple $N=(S,A,T)$, where

  * $\bullet$

$S$ is the finite set of places, ranged over by $s$ (possibly indexed),

  * $\bullet$

$A$ is the finite set of labels, ranged over by $\ell$ (possibly indexed), and

  * $\bullet$

$T\subseteq{(\mathcal{M}}(S)\setminus\\{\theta\\})\times
A\times{\mathcal{M}}(S)$ is the finite set of transitions, ranged over by $t$
(possibly indexed).

Given a transition $t=(m,\ell,m^{\prime})$, we use the notation:

  * $\bullet$

${}^{\bullet}t$ to denote its pre-set $m$ (which cannot be an empty multiset)
of tokens to be consumed;

  * $\bullet$

$l(t)$ for its label $\ell$, and

  * $\bullet$

$t^{\bullet}$ to denote its post-set $m^{\prime}$ of tokens to be produced.

Hence, transition $t$ can be represented as
${}^{\bullet}t$${\>\stackrel{{\scriptstyle
l(t)}}{{\longrightarrow}}\>}$$t^{\bullet}$. We also define the flow function
flow$:(S\times T)\cup(T\times S)\rightarrow{\mathbb{N}}$ as follows: for all
$s\in S$, for all $t\in T$, flow$(s,t)=\mbox{${}^{\bullet}t$}(s)$ and
flow$(t,s)=\mbox{$t^{\bullet}$}(s)$. We will use $F$ to denote the flow
relation $\\{(x,y)\;\;\big{|}\;\;x,y\in S\cup T\,\wedge\,$flow$(x,y)>0\\}$.
Finally, we define pre-sets and post-sets also for places as follows:
$\mbox{${}^{\bullet}s$}=\\{t\in T\;\;\big{|}\;\;s\in\mbox{$t^{\bullet}$}\\}$
and $\mbox{$s^{\bullet}$}=\\{t\in
T\;\;\big{|}\;\;s\in\mbox{${}^{\bullet}t$}\\}$.  $\Box$

Graphically, a place is represented by a little circle and a transition by a
little box. These are connected by directed arcs, which may be labeled by a
positive integer, called the weight, to denote the number of tokens consumed
(when the arc goes from a place to the transition) or produced (when the arc
goes form the transition to a place) by the execution of the transition; if
the number is omitted, then the weight default value of the arc is $1$.

###### Definition 3

(Marking, P/T net system) A multiset over $S$ is called a marking. Given a
marking $m$ and a place $s$, we say that the place $s$ contains $m(s)$ tokens,
graphically represented by $m(s)$ bullets inside place $s$. A P/T net system
$N(m_{0})$ is a tuple $(S,A,T,m_{0})$, where $(S,A,T)$ is a P/T net and
$m_{0}$ is a marking over $S$, called the initial marking. We also say that
$N(m_{0})$ is a marked net.  $\Box$

###  2.1 Sequential Semantics

###### Definition 4

(Enabling, firing sequence, transition sequence, reachable marking, safe net)
Given a P/T net $N=(S,A,T)$, a transition $t$ is enabled at $m$, denoted by
$m[t\rangle$, if $\mbox{${}^{\bullet}t$}\subseteq m$. The execution (or
firing) of $t$ enabled at $m$ produces the marking
$m^{\prime}=(m\ominus\mbox{${}^{\bullet}t$})\oplus\mbox{$t^{\bullet}$}$. This
is written $m[t\rangle m^{\prime}$. A firing sequence starting at $m$ is
defined inductively as follows:

  * $\bullet$

$m[\epsilon\rangle m$ is a firing sequence (where $\epsilon$ denotes an empty
sequence of transitions) and

  * $\bullet$

if $m[\sigma\rangle m^{\prime}$ is a firing sequence and $m^{\prime}[t\rangle
m^{\prime\prime}$, then $m[\sigma t\rangle m^{\prime\prime}$ is a firing
sequence.

The set of reachable markings from $m$ is
$[m\rangle=\\{m^{\prime}\;\;\big{|}\;\;\exists\sigma.$ $m[\sigma\rangle
m^{\prime}\\}$. The P/T net system $N=$ $(S,A,T,m_{0})$ is safe if for each
$m\in[m_{0}\rangle$ and for all $s\in S$, we have that $m(s)\leq 1$.  $\Box$

Note that the reachable markings of a P/T net can be countably infinitely many
when the net is not bounded, i.e., when the number of tokens on some places
can grow unboundedly.

Now we recall a simple behavioral equivalence on P/T nets, defined directly
over the markings of the net, which compares two markings with respect to
their sequential behavior.

###### Definition 5

(Interleaving Bisimulation) Let $N=(S,A,T)$ be a P/T net. An interleaving
bisimulation is a relation $R\subseteq{\mathcal{M}}(S)\times{\mathcal{M}}(S)$
such that if $(m_{1},m_{2})\in R$ then

  * $\bullet$

$\forall t_{1}$ such that $m_{1}[t_{1}\rangle m^{\prime}_{1}$, $\exists t_{2}$
such that $m_{2}[t_{2}\rangle m^{\prime}_{2}$ with $l(t_{1})=l(t_{2})$ and
$(m^{\prime}_{1},m^{\prime}_{2})\in R$,

  * $\bullet$

$\forall t_{2}$ such that $m_{2}[t_{2}\rangle m^{\prime}_{2}$, $\exists t_{1}$
such that $m_{1}[t_{1}\rangle m^{\prime}_{1}$ with $l(t_{1})=l(t_{2})$ and
$(m^{\prime}_{1},m^{\prime}_{2})\in R$.

Two markings $m_{1}$ and $m_{2}$ are interleaving bisimilar, denoted by
$m_{1}\sim_{int}m_{2}$, if there exists an interleaving bisimulation $R$ such
that $(m_{1},m_{2})\in R$.  $\Box$

Interleaving bisimilarity was proved undecidable in [23] for P/T nets having
at least two unbounded places, with a proof based on the comparison of two
sequential P/T nets, where a P/T net is sequential if it does not offer any
concurrent behavior. Hence, interleaving bisimulation equivalence is
undecidable even for the subclass of sequential finite P/T nets. Esparza
observed in [10] that all the non-interleaving bisimulation-based equivalences
(in the spectrum ranging from interleaving bisimilarity to fully-concurrent
bisimilarity [5]) collapse to interleaving bisimilarity over sequential P/T
nets. Hence, the proof in [23] applies to all these non-interleaving
bisimulation equivalences as well.

###  2.2 Concurrent Semantics

Given a P/T net $N=(S,A,T)$ and a marking $m$, we say that two transitions
$t_{1},t_{2}\in T$ are concurrently enabled at $m$ if
$\mbox{${}^{\bullet}t$}_{1}\oplus\mbox{${}^{\bullet}t$}_{2}\subseteq m$. The
concurrent firing of these two transitions produces the marking
$m^{\prime}=(m\ominus(\mbox{${}^{\bullet}t$}_{1}\oplus\mbox{${}^{\bullet}t$}_{2}))\oplus(\mbox{$t_{1}^{\bullet}$}\oplus\mbox{$t_{2}^{\bullet}$})$.
We denote this fact by $m[\\{t_{1},t_{2}\\}\rangle m^{\prime}$. It is also
possible that the same transition is self-concurrent at some marking $m$,
meaning that two or more occurrences of it are concurrently enabled at $m$.

We can generalize the definition of concurrently enabled transitions to a
finite, nonempty multiset $G$ over the set $T$, called a step. A step
$G:T\rightarrow{\mathbb{N}}$ is enabled at marking $m$ if
$\mbox{${}^{\bullet}G$}\subseteq m$, where
$\mbox{${}^{\bullet}G$}=\bigoplus_{t\in T}G(t)\cdot\mbox{${}^{\bullet}t$}$ and
$G(t)$ denotes the number of occurrences of transition $t$ in the step $G$.
The execution of a step $G$ enabled at $m$ produces the marking
$m^{\prime}=(m\ominus\mbox{${}^{\bullet}G$})\oplus\mbox{$G^{\bullet}$}$, where
$\mbox{$G^{\bullet}$}=\bigoplus_{t\in T}G(t)\cdot\mbox{$t^{\bullet}$}$. This
is written $m[G\rangle m^{\prime}$. We sometimes refer to this as the
concurrent token game, in opposition to the sequential token game of
Definition 4. The label $l(G)$ of a step $G$ is the multiset
$l(G):A\rightarrow{\mathbb{N}}$ defined as follows:
$l(G)(a)=\sum_{t_{i}\in\mathit{dom}(G).l(t_{i})=a}G(t_{i})$.

Now we define a notion of bisimulation based on the firing of steps, rather
than of single transitions (as for interleaving bisimulation), originally
proposed in [31].

###### Definition 6

(Step Bisimulation) Let $N=(S,A,T)$ be a P/T net. A step bisimulation is a
relation $R\subseteq{\mathcal{M}}(S)\times{\mathcal{M}}(S)$ such that if
$(m_{1},m_{2})\in R$ then

  * $\bullet$

$\forall G_{1}$ such that $m_{1}[G_{1}\rangle m^{\prime}_{1}$, $\exists G_{2}$
s.t. $m_{2}[G_{2}\rangle m^{\prime}_{2}$ with $l(G_{1})=l(G_{2})$ and
$(m^{\prime}_{1},m^{\prime}_{2})\in R$,

  * $\bullet$

$\forall G_{2}$ such that $m_{2}[G_{2}\rangle m^{\prime}_{2}$, $\exists G_{1}$
s.t. $m_{1}[G_{1}\rangle m^{\prime}_{1}$ with $l(G_{1})=l(G_{2})$ and
$(m^{\prime}_{1},m^{\prime}_{2})\in R$.

Two markings $m_{1}$ and $m_{2}$ are step bisimilar (or step bisimulation
equivalent), denoted by $m_{1}\sim_{s}m_{2}$, if there exists a step
bisimulation $R$ such that $(m_{1},m_{2})\in R$.  $\Box$

Of course, $\sim_{s}$ is finer than $\sim_{int}$; moreover, also step
bisimilarity is undecidable for P/T nets having at least two unbounded places
[10].

###  2.3 Causality-based Semantics

We outline some definitions, adapted from the literature (cf., e.g., [15, 4,
32, 14, 19]).

###### Definition 7

(Acyclic net) A P/T net $N=(S,A,T)$ is acyclic if its flow relation $F$ is
acyclic (i.e., $\not\exists x$ such that $xF^{+}x$, where $F^{+}$ is the
transitive closure of $F$).  $\Box$

The causal semantics of a marked P/T net is defined by a class of particular
acyclic safe nets, where places are not branched (hence they represent a
single run) and all arcs have weight 1. This kind of net is called causal net.
We use the name $C$ (possibly indexed) to denote a causal net, the set $B$ to
denote its places (called conditions), the set $E$ to denote its transitions
(called events), and $L$ to denote its labels.

###### Definition 8

(Causal net) A causal net is a finite marked net
$C(\mathsf{m}_{0})=(B,L,E,\mathsf{m}_{0})$ satisfying the following
conditions:

  1. 1.

$C$ is acyclic;

  2. 2.

$\forall b\in B\;\;|\mbox{${}^{\bullet}b$}|\leq
1\,\wedge\,|\mbox{$b^{\bullet}$}|\leq 1$ (i.e., the places are not branched);

  3. 3.

$\forall b\in B\;\;\mathsf{m}_{0}(b)=\begin{cases}1&\mbox{if
$\;\mbox{${}^{\bullet}b$}=\emptyset$}\\\ 0&\mbox{otherwise;}\end{cases}$

  4. 4.

$\forall e\in E\;\;\mbox{${}^{\bullet}e$}(b)\leq
1\,\wedge\,\mbox{$e^{\bullet}$}(b)\leq 1$ for all $b\in B$ (i.e., all the arcs
have weight $1$).

We denote by $Min(C)$ the set $\mathsf{m}_{0}$, and by $Max(C)$ the set
$\\{b\in B\;\;\big{|}\;\;\mbox{$b^{\bullet}$}=\emptyset\\}$.  $\Box$

Note that any reachable marking of a causal net is a set, i.e., this net is
safe; in fact, the initial marking is a set and, assuming by induction that a
reachable marking $\mathsf{m}$ is a set and enables $e$, i.e.,
$\mathsf{m}[e\rangle\mathsf{m}^{\prime}$, then also
$\mathsf{m}^{\prime}=(\mathsf{m}\ominus\mbox{${}^{\bullet}e$})\oplus\mbox{$e^{\bullet}$}$
is a set, as the net is acyclic and because of the condition on the shape of
the post-set of $e$ (weights can only be $1$).

As the initial marking of a causal net is fixed by its shape (according to
item $3$ of Definition 8), in the following, in order to make the notation
lighter, we often omit the indication of the initial marking, so that the
causal net $C(\mathsf{m}_{0})$ is denoted by $C$.

###### Definition 9

(Moves of a causal net) Given two causal nets $C=(B,L,E,\mathsf{m}_{0})$ and
$C^{\prime}=(B^{\prime},L,E^{\prime},\mathsf{m}_{0})$, we say that $C$ moves
in one step to $C^{\prime}$ through $e$, denoted by $C[e\rangle C^{\prime}$,
if $\;\mbox{${}^{\bullet}e$}\subseteq Max(C)$, $E^{\prime}=E\cup\\{e\\}$ and
$B^{\prime}=B\cup\mbox{$e^{\bullet}$}$.  $\Box$

###### Definition 10

(Folding and Process) A folding from a causal net $C=(B,L,E,\mathsf{m}_{0})$
into a net system $N(m_{0})=(S,A,T,m_{0})$ is a function $\rho:B\cup E\to
S\cup T$, which is type-preserving, i.e., such that $\rho(B)\subseteq S$ and
$\rho(E)\subseteq T$, satisfying the following:

  * $\bullet$

$L=A$ and $\mathsf{l}(e)=l(\rho(e))$ for all $e\in E$;

  * $\bullet$

$\rho(\mathsf{m}_{0})=m_{0}$, i.e.,
$m_{0}(s)=|\rho^{-1}(s)\cap\mathsf{m}_{0}|$;

  * $\bullet$

$\forall e\in E,\rho(\mbox{${}^{\bullet}e$})=\mbox{${}^{\bullet}\rho(e)$}$,
i.e.,
$\rho(\mbox{${}^{\bullet}e$})(s)=|\rho^{-1}(s)\cap\mbox{${}^{\bullet}e$}|$ for
all $s\in S$;

  * $\bullet$

$\forall e\in E,\,\rho(\mbox{$e^{\bullet}$})=\mbox{$\rho(e)^{\bullet}$}$,
i.e., $\rho(\mbox{$e^{\bullet}$})(s)=|\rho^{-1}(s)\cap\mbox{$e^{\bullet}$}|$
for all $s\in S$.

A pair $(C,\rho)$, where $C$ is a causal net and $\rho$ a folding from $C$ to
a net system $N(m_{0})$, is a process of $N(m_{0})$.  $\Box$

###### Definition 11

(Moves of a process) Let $N(m_{0})=(S,A,T,m_{0})$ be a net system and let
$(C_{i},\rho_{i})$, for $i=1,2$, be two processes of $N(m_{0})$. We say that
$(C_{1},\rho_{1})$ moves in one step to $(C_{2},\rho_{2})$ through $e$,
denoted by $(C_{1},\rho_{1}){\mbox{${\>\stackrel{{\scriptstyle
e}}{{\longrightarrow}}\>}$}}(C_{2},\rho_{2})$, if $C_{1}[e\rangle C_{2}$ and
$\rho_{1}\subseteq\rho_{2}$. If $\pi_{1}=(C_{1},\rho_{1})$ and
$\pi_{2}=(C_{2},\rho_{2})$, we denote the move as
$\pi_{1}{\mbox{${\>\stackrel{{\scriptstyle
e}}{{\longrightarrow}}\>}$}}\pi_{2}$.  $\Box$

###### Definition 12

(Causal-net bisimulation) Let $N=(S,A,T)$ be a finite P/T net. A causal-net
bisimulation is a relation $R$, composed of triples of the form
$(\rho_{1},C,\rho_{2})$, where, for $i=1,2$, $(C,\rho_{i})$ is a process of
$N(m_{0_{i}})$ for some $m_{0_{i}}$, such that if $(\rho_{1},C,\rho_{2})\in R$
then

  * $i)$

$\forall t_{1},C^{\prime},\rho_{1}^{\prime}$ s.t.
$(C,\rho_{1}){\mbox{${\>\stackrel{{\scriptstyle
e}}{{\longrightarrow}}\>}$}}(C^{\prime},\rho_{1}^{\prime})$, where
$\rho_{1}^{\prime}(e)=t_{1}$, $\exists t_{2},\rho_{2}^{\prime}$ s.t.
$(C,\rho_{2}){\mbox{${\>\stackrel{{\scriptstyle
e}}{{\longrightarrow}}\>}$}}(C^{\prime},\rho_{2}^{\prime})$, where
$\rho_{2}^{\prime}(e)=t_{2}$, and
$(\rho^{\prime}_{1},C^{\prime},\rho^{\prime}_{2})\in R$;

  * $ii)$

and $\forall t_{2},C^{\prime},\rho_{2}^{\prime}$ such that
$(C,\rho_{2}){\mbox{${\>\stackrel{{\scriptstyle
e}}{{\longrightarrow}}\>}$}}(C^{\prime},\rho_{2}^{\prime})$, where
$\rho_{2}^{\prime}(e)=t_{2}$, $\exists t_{1},\rho_{1}^{\prime}$ such that
$(C,\rho_{1}){\mbox{${\>\stackrel{{\scriptstyle
e}}{{\longrightarrow}}\>}$}}(C^{\prime},\rho_{1}^{\prime})$, where
$\rho_{1}^{\prime}(e)=t_{1}$, and
$(\rho^{\prime}_{1},C^{\prime},\rho^{\prime}_{2})\in R$.

Two markings $m_{1}$ and $m_{2}$ of $N$ are cn-bisimilar (or cn-bisimulation
equivalent), denoted by $m_{1}\sim_{cn}m_{2}$, if there exists a causal-net
bisimulation $R$ containing a triple $(\rho^{0}_{1},C^{0},\rho^{0}_{2})$,
where $C^{0}$ contains no events and
$\rho^{0}_{i}(Min(C^{0}))=\rho^{0}_{i}(Max(C^{0}))=m_{i}\;$ for $i=1,2$.
$\Box$

Causal-net bisimilarity, which coincides with structure-preserving
bisimilarity [14], observes not only the events, but also the structure of the
distributed state. The problem of deciding causal-net bisimilarity over
general P/T nets is open, as the observation of Esparza [10] does not apply to
causal-net bisimilarity. It is slightly stronger than fully-concurrent
bisimulation (fc-bisimulation, for short) [5] (as this equivalence observes
only the events), whose definition was inspired by previous notions of
equivalence on other models of concurrency: history-preserving bisimulation,
originally defined in [36] under the name of behavior-structure bisimulation,
and then elaborated on in [12] (who called it by this name) and also
independently defined in [8] (who called it by mixed ordering bisimulation).
Its definition follows.

###### Definition 13

(Partial orders of events from a process) From a causal net
$C=(B,L,E,\mathsf{m}_{0})$, we can extract the partial order of its events
$\mathsf{E}_{\mathsf{C}}=(E,\preceq)$, where $e_{1}\preceq e_{2}$ if there is
a path in the net from $e_{1}$ to $e_{2}$, i.e., if
$e_{1}\mathsf{F}^{*}e_{2}$, where $\mathsf{F}^{*}$ is the reflexive and
transitive closure of $\mathsf{F}$, which is the flow relation for $C$.

Given a process $\pi=(C,\rho)$, we denote $\preceq$ as $\leq_{\pi}$, i.e.
given $e_{1},e_{2}\in E$, $e_{1}\leq_{\pi}e_{2}$ if and only if $e_{1}\preceq
e_{2}$.

Two partial orders $(E_{1},\preceq_{1})$ and $(E_{2},\preceq_{2})$ are
isomorphic if there is a label-preserving, order-preserving map $g:E_{1}\to
E_{2}$, i.e., a bijection such that $\mathsf{l}_{1}(e)=\mathsf{l}_{2}(g(e))$
and $e\preceq_{1}e^{\prime}$ if and only if $g(e)\preceq_{2}g(e^{\prime})$. We
also say that $g$ is an event isomorphism between the causal nets $C_{1}$ and
$C_{2}$ if it is an isomorphism between their associated partial orders
$\mathsf{E}_{C_{1}}$ and $\mathsf{E}_{C_{2}}$.  $\Box$

###### Definition 14

(Fully-concurrent bisimulation) Given a finite P/T net $N=(S,A,T)$, a fully-
concurrent bisimulation is a relation $R$, composed of triples of the form
$(\pi_{1},g,\pi_{2})$, where, for $i=1,2$, $\pi_{i}=(C_{i},\rho_{i})$ is a
process of $N(m_{0i})$ for some $m_{0i}$ and $g$ is an event isomorphism
between $\mathsf{E}_{C_{1}}$ and $\mathsf{E}_{C_{2}}$, such that if
$(\pi_{1},g,\pi_{2})\in R$ then

  * $i)$

$\forall t_{1},\pi_{1}^{\prime}$ such that
$\pi_{1}{\mbox{${\>\stackrel{{\scriptstyle
e_{1}}}{{\longrightarrow}}\>}$}}\pi_{1}^{\prime}$ with
$\rho_{1}^{\prime}(e_{1})=t_{1}$, $\exists t_{2},\pi_{2}^{\prime},g^{\prime}$
such that

    1. 1.

$\pi_{2}{\mbox{${\>\stackrel{{\scriptstyle
e_{2}}}{{\longrightarrow}}\>}$}}\pi_{2}^{\prime}$ with
$\rho_{2}^{\prime}(e_{2})=t_{2}$;

    2. 2.

$g^{\prime}=g\cup\\{(e_{1},e_{2})\\}$, and finally,

    3. 3.

$(\pi_{1}^{\prime},g^{\prime},\pi_{2}^{\prime})\in R$;

  * $ii)$

and symmetrically, if $\pi_{2}$ moves first.

Two markings $m_{1},m_{2}$ are fc-bisimilar, denoted by $m_{1}\sim_{fc}m_{2}$,
if a fully-concurrent bisimulation R exists, containing a triple
$(\pi^{0}_{1},\emptyset,\pi^{0}_{2})$ where
$\pi^{0}_{i}=(C^{0}_{i},\rho^{0}_{i})$ such that $C^{0}_{i}$ contains no
events and $\rho^{0}_{i}(Min(C^{0}_{i}))=\rho^{0}_{i}(Max(C^{0}_{i}))$
$=m_{i}\;$ for $i=1,2$.  $\Box$

##  3 Place Bisimilarity

We now present the place bisimulation idea, introduced in [2] as an
improvement of a behavioral relation proposed by Olderog in [32] on safe nets
(called strong bisimulation), which fails to induce an equivalence relation.
First, an auxiliary definition.

###  3.1 Additive Closure and its Properties

###### Definition 15

(Additive closure) Given a P/T net $N=(S,A,T)$ and a place relation
$R\subseteq S\times S$, we define a marking relation
$R^{\oplus}\,\subseteq\,{\mathcal{M}}(S)\times{\mathcal{M}}(S)$, called the
additive closure of $R$, as the least relation induced by the following axiom
and rule.

$\begin{array}[]{lllllllllll}\begin{array}[]{c}\\\ \hline\cr(\theta,\theta)\in
R^{\oplus}\end{array}&&\;\begin{array}[]{c}(s_{1},s_{2})\in
R\;(m_{1},m_{2})\in R^{\oplus}\\\ \hline\cr(s_{1}\oplus m_{1},s_{2}\oplus
m_{2})\in R^{\oplus}\end{array}\\\ \end{array}$
$\Box$

Note that, by definition, two markings are related by $R^{\oplus}$ only if
they have the same size; in fact, the axiom states that the empty marking is
related to itself, while the rule, assuming by induction that $m_{1}$ and
$m_{2}$ have the same size, ensures that $s_{1}\oplus m_{1}$ and $s_{2}\oplus
m_{2}$ have the same size.

###### Proposition 1

For each relation $R\subseteq S\times S$, if $(m_{1},m_{2})\in R^{\oplus}$,
then $|m_{1}|=|m_{2}|$.  $\Box$

Note also that the membership $(m_{1},m_{2})\in R^{\oplus}$ may be proved in
several different ways, depending on the chosen order of the elements of the
two markings and on the definition of $R$. For instance, if
$R=\\{(s_{1},s_{3}),$ $(s_{1},s_{4}),$ $(s_{2},s_{3}),(s_{2},s_{4})\\}$, then
$(s_{1}\oplus s_{2},s_{3}\oplus s_{4})\in R^{\oplus}$ can be proved by means
of the pairs $(s_{1},s_{3})$ and $(s_{2},s_{4})$, as well as by means of
$(s_{1},s_{4}),(s_{2},s_{3})$.

An alternative way to define that two markings $m_{1}$ and $m_{2}$ are related
by $R^{\oplus}$ is to state that $m_{1}$ can be represented as $s_{1}\oplus
s_{2}\oplus\ldots\oplus s_{k}$, $m_{2}$ can be represented as
$s_{1}^{\prime}\oplus s_{2}^{\prime}\oplus\ldots\oplus s_{k}^{\prime}$ and
$(s_{i},s_{i}^{\prime})\in R$ for $i=1,\ldots,k$. Therefore, it is easy to
observe that if $(m_{1},m_{2})\in R^{\oplus}$ and $m_{1}^{\prime}\subseteq
m_{1}$, then there exists $m_{2}^{\prime}\subseteq m_{2}$ such that
$(m_{1}^{\prime},m_{2}^{\prime})\in R^{\oplus}$ and $(m_{1}\ominus
m_{1}^{\prime},m_{2}\ominus m_{2}^{\prime})\in R^{\oplus}$.

###### Proposition 2

[17] For each place relation $R\subseteq S\times S$, the following hold:

  1. 1.

If $R$ is an equivalence relation, then $R^{\oplus}$ is an equivalence
relation.

  2. 2.

If $R_{1}\subseteq R_{2}$, then $R_{1}^{\oplus}\subseteq R_{2}^{\oplus}$,
i.e., the additive closure is monotone.

  3. 3.

If $(m_{1},m_{2})\in R^{\oplus}$ and $(m_{1}^{\prime},m_{2}^{\prime})\in
R^{\oplus}$, then $(m_{1}\oplus m_{1}^{\prime},m_{2}\oplus m_{2}^{\prime})\in
R^{\oplus}$, i.e., the additive closure is additive.

  4. 4.

If $R$ is an equivalence, $(m_{1}\oplus m_{1}^{\prime},$ $m_{2}\oplus
m_{2}^{\prime})\in R^{\oplus}$ and $(m_{1},m_{2})\in R^{\oplus}$, then
$(m_{1}^{\prime},m_{2}^{\prime})\in R^{\oplus}$, i.e., the additive closure of
an equivalence place relation is subtractive.

$\Box$

When $R$ is an equivalence relation, it is rather easy to check whether two
markings are related by $R^{\oplus}$. An algorithm, described in [17],
establishes whether an $R$-preserving bijection exists between the two
markings $m_{1}$ and $m_{2}$ of equal size $k$ in $O(k^{2})$ time. Another
algorithm, described in [18], checks whether $(m_{1},m_{2})\in R^{\oplus}$ in
$O(n)$ time, where $n$ is the size of $S$. However, these performant
algorithms heavily rely on the fact that $R$ is an equivalence relation, hence
also subtractive (case 4 of Proposition 2). If $R$ is not an equivalence
relation, which is typical for place bisimulations, the naive algorithm for
checking whether $(m_{1},m_{2})\in R^{\oplus}$ would simply consider $m_{1}$
represented as $s_{1}\oplus s_{2}\oplus\ldots\oplus s_{k}$, and then would
scan all the possible permutations of $m_{2}$, each represented as
$s^{\prime}_{1}\oplus s^{\prime}_{2}\oplus\ldots\oplus s^{\prime}_{k}$, to
check that $(s_{i},s_{i}^{\prime})\in R$ for $i=1,\ldots,k$. Of course, this
naive algorithm has worst-case complexity $O(k!)$.

###### Example 1

Consider $R=\\{(s_{1},s_{3}),$ $(s_{1},s_{4}),(s_{2},s_{4})\\}$, which is not
an equivalence relation. Suppose we want to check whether $(s_{1}\oplus
s_{2},s_{4}\oplus s_{3})\in R^{\oplus}$. If we start by matching
$(s_{1},s_{4})\in R$, then we would fail because the residual $(s_{2},s_{3})$
does not belong to $R$. However, if we permute the second marking to
$s_{3}\oplus s_{4}$, then we succeed because the required pairs
$(s_{1},s_{3})$ and $(s_{2},s_{4})$ are both in $R$.  $\Box$

Nonetheless, the problem of checking if $(m_{1},m_{2})\in R^{\oplus}$ has
polynomial time complexity because it can be considered an instance of the
problem of finding a perfect matching in a bipartite graph, where the nodes
are the tokens in the two markings and the edges are defined by the relation
$R$. In fact, the definition of the bipartite graph takes $O(k^{2})$ time
(where $k=|m_{1}|=|m_{2}|$) and, then, the Hopcroft-Karp-Karzanov algorithm
[22, 25] for computing the maximum matching has worst-case time complexity
$O(h\sqrt{k})$, where $h$ is the number of the edges in the bipartire graph
($h\leq k^{2}$) and to check whether the maximum matching is perfect can be
done simply by checking that the size of the matching equals the number of
nodes in each partition, i.e., $k$. Hence, in evaluating the complexity of the
algorithm in Section 5, we assume that the complexity of checking whether
$(m_{1},m_{2})\in R^{\oplus}$ is in $O(k^{2}\sqrt{k})$.

A related problem is that of computing, given a marking $m_{1}$ of size $k$,
the set of all the markings $m_{2}$ such that $(m_{1},m_{2})\in R^{\oplus}$.
This problem can be solved with a worst-case time complexity of $O(n^{k})$
because each of the $k$ tokens in $m_{1}$ can be related via $R$ to $n$ places
at most.

###### Proposition 3

[17] For each place relations $R,R_{1},R_{2}\subseteq S\times S$, the
following hold:

  1. 1.

$\emptyset^{\oplus}=\\{(\theta,\theta)\\}$, i.e., the additive closure of the
empty place relation yields a singleton marking relation, relating the empty
marking to itself.

  2. 2.

$(\mathcal{I}_{S})^{\oplus}=\mathcal{I}_{M}$, i.e., the additive closure of
the identity relation on places $\mathcal{I}_{S}=\\{(s,s)\;\;\big{|}\;\;s\in
S\\}$ yields the identity relation on markings
$\mathcal{I}_{M}=\\{(m,m)\;\;\big{|}\;\;$ $m\in{\mathcal{M}}(S)\\}$.

  3. 3.

$(R^{\oplus})^{-1}=(R^{-1})^{\oplus}$, i.e., the inverse of an additively
closed relation $R$ equals the additive closure of its inverse $R^{-1}$.

  4. 4.

$(R_{1}\circ R_{2})^{\oplus}=(R_{1}^{\oplus})\circ(R_{2}^{\oplus})$, i.e., the
additive closure of the composition of two place relations equals the
compositions of their additive closures.

$\Box$

###  3.2 Place Bisimulation and its Properties

We are now ready to introduce place bisimulation, which is a non-interleaving
behavioral relation defined over the net places.

###### Definition 16

(Place Bisimulation) Let $N=(S,A,T)$ be a P/T net. A place bisimulation is a
relation $R\subseteq S\times S$ such that if $(m_{1},m_{2})\in R^{\oplus}$
then

  * $\bullet$

$\forall t_{1}$ such that $m_{1}[t_{1}\rangle m^{\prime}_{1}$, $\exists t_{2}$
such that $m_{2}[t_{2}\rangle m^{\prime}_{2}$ with
$(\mbox{${}^{\bullet}t_{1}$},\mbox{${}^{\bullet}t_{2}$})\in R^{\oplus}$,
$l(t_{1})=l(t_{2})$, $(\mbox{$t_{1}^{\bullet}$},\mbox{$t_{2}^{\bullet}$})\in
R^{\oplus}$ and, moreover, $(m_{1}^{\prime},m_{2}^{\prime})\in R^{\oplus}$;
and symmetrically,

  * $\bullet$

$\forall t_{2}$ such that $m_{2}[t_{2}\rangle m^{\prime}_{2}$, $\exists t_{1}$
such that $m_{1}[t_{1}\rangle m^{\prime}_{1}$ with
$(\mbox{${}^{\bullet}t_{1}$},\mbox{${}^{\bullet}t_{2}$})\in R^{\oplus}$,
$l(t_{1})=l(t_{2})$, $(\mbox{$t_{1}^{\bullet}$},\mbox{$t_{2}^{\bullet}$})\in
R^{\oplus}$ and, moreover, $(m_{1}^{\prime},m_{2}^{\prime})\in R^{\oplus}$.

Two markings $m_{1}$ and $m_{2}$ are place bisimilar, denoted by
$m_{1}\sim_{p}m_{2}$, if there exists a place bisimulation $R$ such that
$(m_{1},m_{2})\in R^{\oplus}$.  $\Box$

Note that a place relation $R\subseteq S\times S$ is a place bisimulation if
for all $(m_{1},m_{2})\in R^{\oplus}$ the two place bisimulation conditions
above hold. So, it seems that infinitely many verifications are necessary to
establish whether $R$ is a place bisimulation. In Section 5 we prove that,
actually, only finitely many verifications are necessary.

In order to prove that $\sim_{p}$ is an equivalence relation, we now list some
useful properties of place bisimulation relations.

###### Proposition 4

For each P/T net $N=(S,A,T)$, the following hold:

  1. 1.

The identity relation ${\mathcal{I}}_{S}=\\{(s,s)\;\;\big{|}\;\;s\in S\\}$ is
a place bisimulation;

  2. 2.

the inverse relation $R^{-1}=\\{(s^{\prime},s)\;\;\big{|}\;\;(s,s^{\prime})\in
R\\}$ of a place bisimulation $R$ is a place bisimulation;

  3. 3.

the relational composition $R_{1}\circ
R_{2}=\\{(s,s^{\prime\prime})\;\;\big{|}\;\;$ $\exists
s^{\prime}.(s,s^{\prime})\in R_{1}\wedge(s^{\prime},s^{\prime\prime})\in
R_{2}\\}$ of two place bisimulations $R_{1}$ and $R_{2}$ is a place
bisimulation.

###### Proposition 5

For each P/T net $N=(S,A,T)$, relation
$\sim_{p}\;\subseteq\mathcal{M}(S)\times\mathcal{M}(S)$ is an equivalence
relation.

###### Proposition 6

(Place bisimilarity is finer than interleaving bisimilarity) Given a P/T net
$N=(S,A,T)$ and two markings $m_{1},m_{2}$, if $m_{1}\sim_{p}m_{2}$, then
$m_{1}\sim_{int}m_{2}$.

The implication above is strict, i.e., it is possible to find a P/T net and
two markings that are interleaving bisimilar but not place bisimilar. For
instance, in the CCS [30] terminology, the marking for $a.b.\mbox{\bf
0}+b.a.\mbox{\bf 0}$ and that for $a.\mbox{\bf 0}|b.\mbox{\bf 0}$ (see, e.g.,
[16]). It is also possible to show that place bisimilarity implies step
bisimilarity [31] (cf. the subsequent Example 10 and Theorem 7.1). As a matter
of fact, place bisimilarity is a truly concurrent behavioral equivalence,
which is slightly finer than causal-net bisimilarity [14, 19] (or,
equivalently, structure preserving bisimilarity [14]), in turn slightly finer
than fully-concurrent bisimilarity [5]. The following examples illustrate
these relationships.

$a)\qquad$$s_{1}$$a\;$$s_{2}\;$$b\;$22$b)\quad$$s_{3}$$a\;$$s_{4}\;$$b\;$
Figure 2: Two fully-concurrent bisimilar markings, which are not place
bisimilar
$s_{1}$$a\;$$s_{2}\;$$\;s_{3}$$b\;$$s_{4}\;$$s_{5}$$a\;$$s_{6}\;$$b\;$$s_{7}\;$22
Figure 3: Two causal-net bisimilar markings, which are not place bisimilar

###### Example 2

Consider the net in Figure 2. Note that it is not possible to build a place
bisimulation relating $s_{1}$ and $s_{3}$ because the post-sets of the
$a$-labeled transitions from $s_{1}$ and $s_{3}$ (i.e., $2\cdot s_{2}$ and
$s_{4}$, respectively) have different size. Of course, the two markings
$s_{1}$ and $s_{3}$ are not causal-net bisimilar, as they generate different
causal nets. However, $s_{1}$ and $s_{3}$ are fully-concurrent bisimilar [5],
because both can perform the same partial order of events (i.e., $b$ caused by
$a$).  $\Box$

###### Example 3

An intriguing example showing the difference between place bisimilarity and
causal-net bisimilarity is about the nets in Figure 3. Of course, $s_{1}$ and
$s_{5}$ are causal-net bisimilar, because both generate the same causal nets.
However, no place bisimulation relating $s_{1}$ and $s_{5}$ exists, as this
place relation would require the pair $(s_{2},s_{6})$, but $s_{2}$ and $s_{6}$
are not place bisimilar; in fact, $2\cdot s_{2}$ is stuck, while $2\cdot
s_{6}$ can perform $b$.  $\Box$

By Definition 16, place bisimilarity $\sim_{p}$ can be defined as follows:

$\sim_{p}=\bigcup\\{R^{\oplus}\;\;\big{|}\;\;R\mbox{ is a place
bisimulation}\\}.$

By monotonicity of the additive closure (Proposition 2(2)), if $R_{1}\subseteq
R_{2}$, then $R_{1}^{\oplus}\subseteq R_{2}^{\oplus}$. Hence, we can restrict
our attention to maximal place bisimulations only:

$\sim_{p}=\bigcup\\{R^{\oplus}\;\;\big{|}\;\;R\mbox{ is a {\em maximal} place
bisimulation}\\}.$

However, it is not true that

$\sim_{p}=(\bigcup\\{R\;\;\big{|}\;\;R\mbox{ is a {\em maximal} place
bisimulation}\\})^{\oplus}$

because the union of place bisimulations may be not a place bisimulation (as
already observed in [2]), so that its definition is not coinductive. We
illustrate this fact by means of the following tiny example.

$s_{1}\;$$a\;$$\;s_{2}$$s_{3}\;$ Figure 4: A simple net

###### Example 4

Consider the simple P/T net in Figure 4, with $S=\\{s_{1},s_{2},s_{3}\\}$. It
is rather easy to realize that there are only two interesting (i.e., useful to
relate non-deadlocked markings) maximal place bisimulations, namely:

$\begin{array}[]{lclll}R_{1}&=&\mathcal{I}_{S}=\\{(s_{1},s_{1}),(s_{2},s_{2}),(s_{3},s_{3})\\}\mbox{
and}\\\
R_{2}&=&(R_{1}\setminus\mathcal{I}_{\\{s_{1},s_{2}\\}})\cup\\{(s_{1},s_{2}),(s_{2},s_{1})\\}=\\{(s_{1},s_{2}),(s_{2},s_{1}),(s_{3},s_{3})\\},\\\
\end{array}$

only one of which is an equivalence relation. However, note that their union
$R=R_{1}\cup R_{2}$ is not a place bisimulation. In fact, on the one hand
$(s_{1}\oplus s_{1},s_{1}\oplus s_{2})\in R^{\oplus}$, but, on the other hand,
these two markings do not satisfy the place bisimulation game, because
$s_{1}\oplus s_{1}$ is stuck, while $s_{1}\oplus s_{2}$ can fire the
$a$-labeled transition, reaching $s_{3}$.

As $R_{1}$ and $R_{2}$ are two maximal place bisimulations, then we can prove
that $m\sim_{p}m$ for each marking $m\in\mathcal{M}(S)$ because $(m,m)\in
R_{1}^{\oplus}$, as well as that, e.g., $2\cdot s_{1}\oplus
s_{2}\sim_{p}s_{1}\oplus 2\cdot s_{2}$ as $(2\cdot s_{1}\oplus
s_{2},s_{1}\oplus 2\cdot s_{2})\in R_{2}^{\oplus}$.

There are also other four maximal place bisimulations, which however may be
used to relate deadlocked markings only:

$\begin{array}[]{lclll}R_{3}&=&\\{(s_{1},s_{3}),(s_{3},s_{2}),(s_{3},s_{3}),(s_{1},s_{2})\\}\\\
R_{4}&=&\\{(s_{3},s_{1}),(s_{2},s_{3}),(s_{3},s_{3}),(s_{2},s_{1})\\}\\\
R_{5}&=&\\{(s_{1},s_{1}),(s_{3},s_{3}),(s_{3},s_{1}),(s_{1},s_{3})\\}\mbox{
and}\\\
R_{6}&=&\\{(s_{2},s_{2}),(s_{3},s_{3}),(s_{3},s_{2}),(s_{2},s_{3})\\},\\\
\end{array}$

so that, e.g., $(2\cdot s_{1}\oplus s_{3},s_{2}\oplus 2\cdot s_{3})\in
R_{3}^{\oplus}$. Note that the equivalence relation $\sim_{p_{eq}}$
characterized in [3] is $R_{1}^{\oplus}$, which is an equivalence relation
indeed, because $R_{1}$ is an equivalence and, by Proposition 2(1), also
$R_{1}^{\oplus}$ is an equivalence. Instead $\sim_{p}=R_{1}^{\oplus}\cup
R_{2}^{\oplus}\cup R_{3}^{\oplus}\cup R_{4}^{\oplus}\cup R_{5}^{\oplus}\cup
R_{6}^{\oplus}$, so that these two equivalences are very different. Note that
$\sim_{p}$ is an equivalence relation, indeed, as it is reflexive
($\mathcal{I}_{M}=(\mathcal{I}_{S})^{\oplus}=R_{1}^{\oplus}\subseteq\sim_{p}$),
symmetric (because the inverse relation of a maximal place bisimulation is a
maximal place bisimulation; e.g., $R_{3}^{-1}=R_{4}$) and transitive (maximal
place relations are closed by relational composition; e.g., $R_{2}\circ
R_{2}=R_{1}$ and $R_{6}\circ R_{5}=R_{4}$).  $\Box$

$s_{1}$$a\;$$s_{2}\;$$\;s_{3}$$b\;$$s_{4}\;$$c\;$$s_{5}$$a\;$$s_{6}\;$$\;s_{7}$$b\;$$s_{8}\;$$c\;$
Figure 5: A more complex net

###### Example 5

Consider the net in Figure 5, where $S=\\{s_{1},s_{2},$ $s_{3},s_{4},$
$s_{5},s_{6},s_{7},s_{8}\\}$. It is not too difficult to realize that the six
interesting maximal place bisimulations are the following:

$\begin{array}[]{lclll}R_{1}&=&\mathcal{I}_{S}\cup\\{(s_{4},s_{8}),(s_{8},s_{4})\\},\mbox{
which is an equivalence relation,}\\\
R_{2}&=&(R_{1}\setminus\mathcal{I}_{\\{s_{2},s_{3}\\}})\cup\\{(s_{2},s_{3}),(s_{3},s_{2})\\},\\\
R_{3}&=&(R_{1}\setminus\mathcal{I}_{\\{s_{6},s_{7}\\}})\cup\\{(s_{6},s_{7}),(s_{7},s_{6})\\},\\\
\end{array}$

$\begin{array}[]{lclll}R_{4}&=&(R_{1}\setminus\mathcal{I}_{\\{s_{2},s_{3},s_{6},s_{7}\\}})\cup\\{(s_{2},s_{3}),(s_{3},s_{2}),(s_{6},s_{7}),(s_{7},s_{6})\\},\\\
\end{array}$

$\begin{array}[]{lclll}R_{5}&=&(R_{1}\setminus\mathcal{I}_{\\{s_{1},s_{2},s_{3},s_{5},s_{6},s_{7}\\}})\cup\\{(s_{2},s_{6}),(s_{3},s_{7}),(s_{6},s_{2}),(s_{7},s_{3})\\}\cup\\{(s_{1},s_{5}),(s_{5},s_{1})\\},\\\
R_{6}&=&(R_{1}\setminus\mathcal{I}_{\\{s_{1},s_{2},s_{3},s_{5},s_{6},s_{7}\\}})\cup\\{(s_{2},s_{7}),(s_{3},s_{6}),(s_{6},s_{3}),(s_{7},s_{2})\\}\cup\\{(s_{1},s_{5}),(s_{5},s_{1})\\}.\\\\[8.5359pt]
\end{array}$

However, there are also other, less interesting, maximal place bisimulations,
which may be used to relate deadlocked markings. For instance,
$R_{7}=\\{(s_{2},s_{3}),(s_{2},s_{6}),$ $(s_{6},s_{7}),$ $(s_{6},s_{2}),$
$(s_{4},s_{8}),(s_{8},s_{4})\\}$, so that $(2\cdot s_{2},s_{3}\oplus s_{6})\in
R_{7}^{\oplus}$. The equivalence relation $\sim_{p_{eq}}$ characterized in [3]
is $R_{1}^{\oplus}$, while $\sim_{p}\supseteq R_{1}^{\oplus}\cup
R_{2}^{\oplus}$ $\cup R_{3}^{\oplus}\cup R_{4}^{\oplus}\cup R_{5}^{\oplus}\cup
R_{6}^{\oplus}\cup R_{7}^{\oplus}$.  $\Box$

###### Example 6

As a tiny case study, let us consider the two unbounded producer-consumer
systems in Figure 6, where prod is the action of producing an item, del of
delivering an item, cons of consuming an item. Note that if a token is present
in the producer place $P_{1}^{\prime}$ (or $P_{2}$), then the transition
labeled by $prod$ can be performed at will, with the effect that the number of
tokens accumulated into place $D_{1}$ (or $D_{2}^{\prime}$,
$D_{2}^{\prime\prime}$) can grow unboundedly; hence, the reachable markings
from $P_{1}\oplus C_{1}$ (or $P_{2}\oplus C_{2}$) are infinitely many, so that
the state space of these two systems is infinite. In order to prove that
$P_{1}\oplus C_{1}\sim_{p}P_{2}\oplus C_{2}$, we can try to build a place
bisimulation $R$ which must contain at least the pairs
$(P_{1},P_{2}),(C_{1},C_{2})$; then, in order to match the $prod$-labeled
transitions, we see that also the pairs $(P_{1}^{\prime},P_{2}),$
$(D_{1},D_{2}^{\prime}),$ $(D_{1},D_{2}^{\prime\prime})$ are needed, and then,
in order to match the $del$-labeled transitions, also the pair
$(C_{1}^{\prime},C_{2}^{\prime})$ must be considered. The resulting relation
is

$R=\\{(P_{1},P_{2}),(P_{1}^{\prime},P_{2}),(D_{1},D_{2}^{\prime}),(D_{1},D_{2}^{\prime\prime}),(C_{1},C_{2}),(C_{1}^{\prime},C_{2}^{\prime})\\}$,

which is a place bisimulation, indeed (formally provable as explained in the
subsequent Lemma 1), justifying that $P_{1}\oplus C_{1}\sim_{p}P_{2}\oplus
C_{2}$. From $R$ we can also derive that, e.g., $P_{1}\oplus
P_{1}^{\prime}\oplus 2\cdot D_{1}\oplus C_{1}^{\prime}$ is place bisimilar to
$2\cdot P_{2}\oplus D_{2}^{\prime}\oplus D_{2}^{\prime\prime}\oplus
C_{2}^{\prime}$.  $\Box$

$P_{1}$$C_{1}$prod$P_{1}^{\prime}$$D_{1}$proddel$C_{1}^{\prime}$cons$P_{2}$$C_{2}$prodprod$D_{2}^{\prime}$$D_{2}^{\prime\prime}$deldel$C_{2}^{\prime}$cons
Figure 6: Two unbounded producer-consumer systems

###### Example 7

As a further example, consider the nets in Figure 7, that model a simple
system with two types of sequential processes: those that can perform $b$ and,
in doing so, generate two instances of the same process type (i.e., $s_{4},$
$s_{5},$ $s_{6},s_{7},s_{9}$); and those that can perform $a$ and, by doing
so, become a process of the first type (i.e., $s_{1},s_{2},$ $s_{3},$$s_{8}$).
It is easy to see that $R=\\{(s_{1},s_{8}),(s_{2},s_{8}),$ $(s_{3},s_{8}),$
$(s_{4},s_{9}),(s_{5},s_{9}),(s_{6},s_{9}),(s_{7},s_{9})\\}$ is a place
bisimulation. Hence, e.g., $s_{1}\oplus 2\cdot s_{3}\oplus s_{4}\oplus s_{7}$
is place bisimilar to $3\cdot s_{8}\oplus 2\cdot s_{9}$.  $\Box$

$a)\quad$$s_{1}$$a\;$$s_{2}\;$$\;a$$a\;$$\;s_{3}$$\;a$$\;a$$\;s_{4}$$\;s_{5}$$\;b$$\;b$$\;s_{6}$$b\;$$\;s_{7}$$b\;$22$b)\;\;$$s_{8}$$a\;$$s_{9}$$b\;$2
Figure 7: Two place bisimilar nets

##  4 Place Bisimilarity Implies Causal-net Bisimilarity

Now we want to prove that our definition of place bisimulation does respect
the intended causal semantics of Petri nets, by proving that place
bisimilarity $\sim_{p}$ implies causal-net bisimilarity $\sim_{cn}$. The
reverse implication does not hold, as illustrated in Example 3.

###### Theorem 4.1

For each P/T net $N=(S,A,T)$, if $m_{1}\sim_{p}m_{2}$ then
$m_{1}\sim_{cn}m_{2}$.

##  5 Place Bisimilarity is Decidable

Since the union of place bisimulations may be not a place bisimulation, its
definition is not coinductive and, therefore, the well-known polynomial
algorithms [24, 33] for computing the largest bisimulation on LTSs cannot be
adapted to compute place bisimilarity.

In order to prove that $\sim_{p}$ is decidable, we first need a technical
lemma which states that it is decidable to check whether a place relation
$R\subseteq S\times S$ is a place bisimulation.

###### Lemma 1

Given a P/T net $N=(S,A,T)$ and a place relation $R\subseteq S\times S$, it is
decidable if $R$ is a place bisimulation.

###### Theorem 5.1

(Place bisimilarity is decidable) Given a P/T net $N=(S,A,T)$, for each pair
of markings $m_{1}$ and $m_{2}$, it is decidable whether $m_{1}\sim_{p}m_{2}$.

About the complexity of this decision procedure, we note that if $|S|=n$, then
the set of all the place relations over $S$ has cardinality $2^{n^{2}}$.
Moreover, the procedure for checking whether a place relation $R_{i}$ in this
set is a place bisimulation has worst-case time complexity $O(q\cdot
n^{p_{1}}\cdot q\cdot(p_{2}^{2}\sqrt{p_{2}}))$. Finally, if $R_{i}$ is a place
bisimulation, the cost of checking whether $(m_{1},m_{2})\in R_{i}^{\oplus}$
is $O(k^{2}\sqrt{k})$ if the two markings have size $k$. Summing up, the
procedure is exponential in the size of the net.

##  6 A Coarser Variant: D-place Bisimilarity

Now we want to define a slightly weaker variant of place bisimulation, we call
d-place bisimulation, which may relate a place $s$ also to the empty marking
$\theta$. In order to provide the definition of d-place bisimulation, we need
first to extend the domain of a place relation: the empty marking $\theta$ is
considered as an additional place, so that a place relation is defined not on
$S$, rather on $S\cup\\{\theta\\}$. Hence, the symbols $r_{1}$ and $r_{2}$
that occur in the following definitions, can only denote either the empty
marking $\theta$ or a single place $s$. Now we extend the idea of additive
closure to these more general place relations, yielding d-additive closure.

###### Definition 17

(D-additive closure) Given a P/T net $N=(S,A,T)$ and a place relation
$R\subseteq(S\cup\\{\theta\\})\times(S\cup\\{\theta\\})$, we define a marking
relation $R^{\odot}\,\subseteq\,{\mathcal{M}}(S)\times{\mathcal{M}}(S)$,
called the d-additive closure of $R$, as the least relation induced by the
following axiom and rule.

$\begin{array}[]{lllllllllll}\begin{array}[]{c}\\\ \hline\cr(\theta,\theta)\in
R^{\odot}\end{array}&&\;\begin{array}[]{c}(r_{1},r_{2})\in
R\;\;(m_{1},m_{2})\in R^{\odot}\\\ \hline\cr(r_{1}\oplus m_{1},r_{2}\oplus
m_{2})\in R^{\odot}\end{array}\\\ \end{array}$
$\Box$

Note that if two markings are related by $R^{\odot}$, then they may have
different size; in fact, even if the axiom relates the empty marking to itself
(so two markings with the same size), as
$R\subseteq(S\cup\\{\theta\\})\times(S\cup\\{\theta\\})$, it may be the case
that $(\theta,s)\in R$, so that, assuming $(m_{1}^{\prime},m_{2}^{\prime})\in
R^{\odot}$ with $|m_{1}^{\prime}|=|m_{2}^{\prime}|$, we get that the pair
$(m_{1}^{\prime},s\oplus m_{2}^{\prime})$ belongs to $R^{\odot}$, as $\theta$
is the identity for the operator of multiset union. Hence, Proposition 1,
which is valid for place relations defined over $S$, is not valid for place
relations defined over $S\cup\\{\theta\\}$. However, the properties in
Propositions 2 and 3 hold also for these more general place relations. Note
that checking whether $(m_{1},m_{2})\in R^{\odot}$ has complexity
$O(k^{2}\sqrt{k})$, where $k$ is the size of the largest marking.

###### Definition 18

(D-place bisimulation) Let $N=(S,A,T)$ be a P/T net. A d-place bisimulation is
a relation $R\subseteq(S\cup\\{\theta\\})\times(S\cup\\{\theta\\})$ such that
if $(m_{1},m_{2})\in R^{\odot}$ then

  * $\bullet$

$\forall t_{1}$ such that $m_{1}[t_{1}\rangle m^{\prime}_{1}$, $\exists t_{2}$
such that $m_{2}[t_{2}\rangle m^{\prime}_{2}$ with
$(\mbox{${}^{\bullet}t_{1}$},\mbox{${}^{\bullet}t_{2}$})\in R^{\odot}$,
$l(t_{1})=l(t_{2})$, $(\mbox{$t_{1}^{\bullet}$},\mbox{$t_{2}^{\bullet}$})\in
R^{\odot}$ and, moreover, $(m_{1}^{\prime},m_{2}^{\prime})\in R^{\odot}$,

  * $\bullet$

$\forall t_{2}$ such that $m_{2}[t_{2}\rangle m^{\prime}_{2}$, $\exists t_{1}$
such that $m_{1}[t_{1}\rangle m^{\prime}_{1}$ with
$(\mbox{${}^{\bullet}t_{1}$},\mbox{${}^{\bullet}t_{2}$})\in R^{\odot}$,
$l(t_{1})=l(t_{2})$, $(\mbox{$t_{1}^{\bullet}$},\mbox{$t_{2}^{\bullet}$})\in
R^{\odot}$ and, moreover, $(m_{1}^{\prime},m_{2}^{\prime})\in R^{\odot}$.

Two markings $m_{1}$ and $m_{2}$ are d-place bisimilar, denoted by
$m_{1}\sim_{d}m_{2}$, if there exists a d-place bisimulation $R$ such that
$(m_{1},m_{2})\in R^{\odot}$.  $\Box$

$a)\qquad$$s_{1}$$a\;$$s_{2}\;$$b\;$$s_{3}\;$$b)\quad$$s_{4}$$a\;$$s_{5}\;$$\;s_{6}$$b\;$
Figure 8: Two d-place bisimilar nets

###### Example 8

Consider the net in Figure 8. It is easy to realize that
$R=\\{(s_{1},s_{4}),(\theta,s_{5}),$ $(s_{2},s_{6}),$ $(s_{3},\theta)\\}$ is a
d-place bisimulation. Hence, this example shows that d-place bisimilarity is
strictly coarser than place bisimilarity, and not finer than causal-net
bisimilarity, because $s_{1}$ and $s_{4}$ generate different causal nets.

The places that are related to $\theta$ (i.e., $s_{3}$ and $s_{5}$) are
deadlocks, i.e., they have empty post-set. However, it may happen that a
d-place bisimulation can also relate a place with non-empty post-set to
$\theta$. In fact, consider the net in Figure 9. It is easy to observe that
the relation $R=\\{(s_{1},s_{2}),(\theta,s_{3})\\}$ is a d-place bisimulation,
as for all the pairs $(m_{1},m_{2})\in R^{\odot}$, both markings are stuck, so
that the d-place bisimulation game is vacuously satisfied.

Nonetheless, it is easy to observe that if a d-place bisimulation $R$ relates
a place $s$ with non-empty post-set to $\theta$, then it is not possible to
find two transitions $t_{1}$ and $t_{2}$ such that for the proof of
$(\mbox{${}^{\bullet}t_{1}$},\mbox{${}^{\bullet}t_{2}$})\in R^{\odot}$ it is
necessary to use the pair $(s,\theta)$ (cf. the subsequent Example 9). In
other words, the condition
$(\mbox{${}^{\bullet}t_{1}$},\mbox{${}^{\bullet}t_{2}$})\in R^{\odot}$ in
Definition 18 is actually
$(\mbox{${}^{\bullet}t_{1}$},\mbox{${}^{\bullet}t_{2}$})\in R^{\oplus}$.
$\Box$

###### Example 9

Consider Figure 10. Even if $s_{1}$ and $s_{3}\oplus s_{4}$ are fc-bisimilar,
we cannot find any d-place bisimulation relating these two markings. If we
include the necessary pairs $(s_{1},s_{3})$ and $(\theta,s_{4})$, then we
would fail immediately, because the pair $(s_{1},s_{3})$ does not satisfy the
d-place bisimulation game, as $s_{1}$ can move, while $s_{3}$ cannot.  $\Box$

$a)\quad$$s_{1}$$b)\quad$$s_{2}$$s_{3}$$s_{4}$$a\;$ Figure 9: Relation
$\\{(s_{1},s_{2}),(\theta,s_{3})\\}$ is a d-place bisimulation

In order to prove that $\sim_{d}$ is an equivalence relation, we now list some
useful properties of d-place bisimulation relations, whose proof is omitted
because very similar to that of the analogous Proposition 4.

###### Proposition 7

For each P/T net $N=(S,A,T)$, the following hold:

  1. 1.

The identity relation ${\mathcal{I}}_{S}=\\{(r,r)\;\;\big{|}\;\;r\in
S\cup\\{\theta\\}\\}$ is a d-place bisimulation;

  2. 2.

the inverse relation $R^{-1}=\\{(r^{\prime},r)\;\;\big{|}\;\;(r,r^{\prime})\in
R\\}$ of a d-place bisimulation $R$ is a d-place bisimulation;

  3. 3.

the relational composition $R_{1}\circ
R_{2}=\\{(r,r^{\prime\prime})\;\;\big{|}\;\;$ $\exists
r^{\prime}.(r,r^{\prime})\in R_{1}\wedge(r^{\prime},r^{\prime\prime})\in
R_{2}\\}$ of two d-place bisimulations $R_{1}$ and $R_{2}$ is a d-place
bisimulation.

Hence, in a standard way, we can prove that d-place bisimilarity $\sim_{d}$ is
an equivalence relation, too.

$a)\qquad$$s_{1}$$a\;$$s_{2}\;$$b)\quad$$s_{3}$$s_{4}$$a\;$ Figure 10: Two fc-
bisimilar nets, but not d-place bisimilar

###  6.1 D-place Bisimilarity Implies Fully-concurrent Bisimilarity

D-place bisimilarity $\sim_{d}$ is incomparable w.r.t. causal-net bisimilarity
(cf. Example 3 and 8). However, we now show that $\sim_{d}$ does fully respect
causality and branching time, by proving that $\sim_{d}$ implies fully-
concurrent bisimilarity $\sim_{fc}$. Example 2 and Example 9 show that the
implication is strict.

###### Theorem 6.1

For each P/T net $N=(S,A,T)$, if $m_{1}\sim_{d}m_{2}$ then
$m_{1}\sim_{fc}m_{2}$.

###  6.2 D-place bisimilarity is decidable

Now, we follow the same steps of the decidability proof of $\sim_{p}$ to prove
that also d-place bisimilarity is decidable. Since the proof is very similar,
we simply sketch it.

###### Lemma 2

Given a P/T net $N=(S,A,T)$ and a relation
$R\subseteq(S\cup\\{\theta\\})\times(S\cup\\{\theta\\})$, it is decidable if
$R$ is a d-place bisimulation.

###### Theorem 6.2

(D-place bisimilarity is decidable) Given a P/T net $N=(S,A,T)$, for each pair
of markings $m_{1}$ and $m_{2}$, it is decidable whether $m_{1}\sim_{d}m_{2}$.

Of course, also this procedure is exponential in the size of the net.

##  7 A Coarser Decidable Equivalence, not Respecting Causality

Place bisimilarity is not the coarsest equivalence proposed in [3]. In fact,
the coarsest equivalence relation proposed in that paper, called i-place
bisimilarity, is as follows.

###### Definition 19

(I-place bisimulation) Let $N=(S,A,T)$ be a P/T net. An i-place bisimulation
is a relation $R\subseteq S\times S$ such that if $(m_{1},m_{2})\in
R^{\oplus}$ then

  * $\bullet$

$\forall t_{1}$ such that $m_{1}[t_{1}\rangle m^{\prime}_{1}$, $\exists t_{2}$
such that $m_{2}[t_{2}\rangle m^{\prime}_{2}$, $l(t_{1})=l(t_{2})$ and
$(m^{\prime}_{1},m^{\prime}_{2})\in R^{\oplus}$,

  * $\bullet$

$\forall t_{2}$ such that $m_{2}[t_{2}\rangle m^{\prime}_{2}$, $\exists t_{1}$
such that $m_{1}[t_{1}\rangle m^{\prime}_{1}$, $l(t_{1})=l(t_{2})$, and
$(m^{\prime}_{1},m^{\prime}_{2})\in R^{\oplus}$.

Two markings $m_{1}$ and $m_{2}$ are i-place bisimilar, denoted by
$m_{1}\sim_{i}m_{2}$, if there exists an i-place bisimulation $R$ such that
$(m_{1},m_{2})\in R^{\oplus}$.  $\Box$

In other words, $R\subseteq S\times S$ is an i-place bisimulation if
$R^{\oplus}$ is an interleaving bisimulation. Also $\sim_{i}$ is an
equivalence relation and can be proved decidable with a variation of the proof
technique of Section 5. In fact, it is easy to prove that $R$ is an i-place
bisimulation if and only if the following two finite conditions are satisfied:

  1. 1.

$\forall t_{1}\in T$, $\forall m$ such that $(\mbox{${}^{\bullet}t_{1}$},m)\in
R^{\oplus}$

     * $(a)$

$\exists t_{2}$ such that $m[t_{2}\rangle m^{\prime}$, with
$l(t_{1})=l(t_{2})$ and $(\mbox{$t_{1}^{\bullet}$},m^{\prime})\in R^{\oplus}$.

  2. 2.

$\forall t_{2}\in T$, $\forall m$ such that $(m,\mbox{${}^{\bullet}t_{2}$})\in
R^{\oplus}$

     * $(b)$

$\exists t_{1}$ such that $m[t_{1}\rangle m^{\prime}$, with
$l(t_{1})=l(t_{2})$ and $(m^{\prime},\mbox{$t_{2}^{\bullet}$})\in R^{\oplus}$.

However, i-place bisimilarity is not very satisfactory, because, even if it
respects the branching time, it does not respect causality.

###### Example 10

Let us consider the net in Figure 11, whose transitions are
$t_{1}=(s_{1},a,\theta),$ $t_{2}=(s_{2},b,\theta),t_{3}=(s_{3},a,\theta),$
$t_{4}=(s_{4},b,\theta)$ and $t_{5}=(s_{3}\oplus s_{4},a,s_{4})$. Let us
consider relation $R=\\{(s_{1},s_{3}),(s_{2},s_{4})\\}$, which is clearly an
i-place bisimulation (but not a place bisimulation). In particular,
$(s_{1}\oplus s_{2},s_{3}\oplus s_{4})\in R^{\oplus}$, transition $s_{3}\oplus
s_{4}[t_{5}\rangle s_{4}$ is matched by $s_{1}\oplus s_{2}[t_{1}\rangle
s_{2}$, and transition $s_{4}[t_{4}\rangle\theta$ is matched by
$s_{2}[t_{2}\rangle\theta$. However, in these computations $s_{1}\oplus s_{2}$
generates the partial order where $a$ and $b$ are independent, while
$s_{3}\oplus s_{4}$ generates the partial order where $b$ is caused by $a$.
$\Box$

$a)\qquad$$s_{1}$$a\;$$s_{2}\;$$b\;$$b)\quad$$s_{3}$$a\;$$s_{4}\;$$b\;$$a\;$
Figure 11: Two i-place bisimilar nets with different causal semantics

Nonetheless, $\sim_{i}$ implies step bisimilarity $\sim_{s}$ [31], so that
i-place bisimilar markings exhibit the same potential parallelism (cf. the
subsequent Theorem 7.1). In fact, markings $s_{1}\oplus s_{2}$ and
$s_{3}\oplus s_{4}$ of the nets in Figure 11 are the typical example of two
markings that are step bisimilar, but not ST bisimilar [11, 21, 6], a finer
behavioral equivalence which, as discussed in [14], is the coarsest
equivalence to be real-time consistent, meaning that for every association of
execution times to actions, assuming that actions happen as soon as they can,
the running times associated with computations from equivalent markings should
be the same. So, i-place bisimilarity, besides not respecting causality, it is
not even real-time consistent, as it does not imply ST bisimilarity. (On the
contrary, [14] argues that place bisimilarity is real-time consistent, and the
same can be argued for d-place bisimilarity.)

Note that i-place bisimilarity is incomparable w.r.t. d-place bisimilarity. On
the one hand, Example 8, discussing the net in Figure 8, shows that
$s_{1}\sim_{d}s_{4}$, but $s_{1}\nsim_{i}s_{4}$ because transition
$s_{1}{\mbox{${\>\stackrel{{\scriptstyle a}}{{\longrightarrow}}\>}$}}s_{2}$
cannot be matched by $s_{4}$ as the post-sets $s_{2}$ and $s_{5}\oplus s_{6}$
have different size. On the other hand, Example 10, discussing the net in
Figure 11, shows that $s_{1}\oplus s_{2}\sim_{i}s_{3}\oplus s_{4}$, but
$s_{1}\oplus s_{2}\nsim_{d}s_{3}\oplus s_{4}$ because transition $s_{3}\oplus
s_{4}{\mbox{${\>\stackrel{{\scriptstyle a}}{{\longrightarrow}}\>}$}}s_{4}$
cannot be matched by $s_{1}\oplus s_{2}$ by preserving the size of the pre-
sets.

Of course, it is possible to define an even coarser decidable equivalence by
allowing for a place to be related to the empty marking $\theta$, as for
d-place bisimilarity, yielding i-d-place bisimilarity.

###### Definition 20

(I-d-place bisimulation) Let $N=(S,A,T)$ be a P/T net. An i-d-place
bisimulation is a relation
$R\subseteq(S\cup\\{\theta\\})\times(S\cup\\{\theta\\})$ such that if
$(m_{1},m_{2})\in R^{\odot}$ then

  * $\bullet$

$\forall t_{1}$ such that $m_{1}[t_{1}\rangle m^{\prime}_{1}$, $\exists t_{2}$
such that $m_{2}[t_{2}\rangle m^{\prime}_{2}$, $l(t_{1})=l(t_{2})$ and
$(m^{\prime}_{1},m^{\prime}_{2})\in R^{\odot}$,

  * $\bullet$

$\forall t_{2}$ such that $m_{2}[t_{2}\rangle m^{\prime}_{2}$, $\exists t_{1}$
such that $m_{1}[t_{1}\rangle m^{\prime}_{1}$, $l(t_{1})=l(t_{2})$ and
$(m^{\prime}_{1},m^{\prime}_{2})\in R^{\odot}$.

Two markings $m_{1}$ and $m_{2}$ are i-d-place bisimilar, denoted by
$m_{1}\sim_{id}m_{2}$, if there exists an i-d-place bisimulation $R$ such that
$(m_{1},m_{2})\in R^{\odot}$.  $\Box$

In other words, $R\subseteq(S\cup\\{\theta\\})\times(S\cup\\{\theta\\})$ is an
i-d-place bisimulation if $R^{\odot}$ is an interleaving bisimulation. Of
course, also i-d-place bisimilarity $\sim_{id}$ is an equivalence relation,
slightly coarser than $\sim_{i}$, and can be proved decidable with yet another
variant of the proof technique in Sections 5 and 6.2. Indeed, it is easy to
see that a relation $R$ is an i-d-place bisimulation if and only if the
following two finite conditions are satisfied:

  1. 1.

$\forall t_{1}\in T$, $\forall m$ such that $(\mbox{${}^{\bullet}t_{1}$},m)\in
R^{\odot}$

     * $(a)$

$\exists t_{2}$ such that $m[t_{2}\rangle m^{\prime}$, with
$l(t_{1})=l(t_{2})$ and $(\mbox{$t_{1}^{\bullet}$},m^{\prime})\in R^{\odot}$.

  2. 2.

$\forall t_{2}\in T$, $\forall m$ such that $(m,\mbox{${}^{\bullet}t_{2}$})\in
R^{\odot}$

     * $(b)$

$\exists t_{1}$ such that $m[t_{1}\rangle m^{\prime}$, with
$l(t_{1})=l(t_{2})$ and $(m^{\prime},\mbox{$t_{2}^{\bullet}$})\in R^{\odot}$.

To conclude, we prove that $\sim_{id}$ implies step bisimilarity $\sim_{s}$,
so that, even if causality is not respected, at least the concurrent behavior
is preserved.

###### Theorem 7.1

For each P/T net $N=(S,A,T)$, if $m_{1}\sim_{id}m_{2}$ then
$m_{1}\sim_{s}m_{2}$.

##  8 Conclusion and Future Research

Place bisimilarity seems a very natural behavioral equivalence for finite P/T
Petri nets, which respects the expected causal behavior, as it is slightly
finer than causal-net bisimilarity [14, 19], (or, equivalently, structure
preserving bisimilarity [14]), in turn slightly finer than fully-concurrent
bisimilarity [5]. Significantly, to date, it is the first sensible (i.e.,
fully respecting causality and branching time) behavioral equivalence which
has been proved decidable for finite P/T nets (with the relevant exception of
net isomorphism), even if its complexity is exponential in the size of the
net. Thus, it is the only equivalence for which it is possible (at least, in
principle) to verify algorithmically the (causality-preserving) correctness of
a distributed system by exhibiting a place bisimulation between its
specification Petri net and its implementation Petri net.

It is sometimes argued that place bisimilarity is too discriminating. In
particular, [2] and [14] argue that a sensible equivalence should not
distinguish markings whose behaviors are patently the same, such as marked
Petri nets that differ only in their unreachable parts. As an example,
consider the net in Figure 12, originally presented in [2]. Clearly, markings
$s_{1}$ and $s_{4}$ are equivalent, also according to all the behavioral
equivalences discussed in [14], except for place bisimilarity. As a matter of
fact, a place bisimulation $R$ containing the pair $(s_{1},s_{4})$ would
require also the pairs $(s_{2},s_{5})$ and $(s_{3},s_{6})$, but then this
place relation $R$ cannot be a place bisimulation because $(s_{2}\oplus
s_{3},s_{5}\oplus s_{6})\in R^{\oplus}$, but $s_{2}\oplus s_{3}$ can perform
$c$, while this is not possible for $s_{5}\oplus s_{6}$. Nonetheless, we would
like to argue in favor of place bisimilarity, despite this apparent
paradoxical example.

$a)\quad$$s_{1}$$a$$b$$s_{2}$$s_{3}$$c$$b)\;\;$$s_{4}$$a$$b$$s_{5}$$s_{6}$
Figure 12: Two non-place bisimilar nets

As a matter of fact, our interpretation of place bisimilarity is that this
equivalence is an attempt of giving semantics to unmarked nets, rather than to
marked nets, so that the focus shifts from the common (but usually
undecidable) question When are two markings equivalent? to the more
restrictive (but decidable) question When are two places equivalent? A
possible (preliminary, but not accurate enough) answer to the latter question
may be: two places are equivalent if, whenever the same number of tokens are
put on these two places, the behavior of the marked nets is the same. If we
reinterpret the example of Figure 12 in this perspective, we clearly see that
place $s_{1}$ and place $s_{4}$ cannot be considered as equivalent because,
even if the markings $s_{1}$ and $s_{4}$ are equivalent, nonetheless the
marking $2\cdot s_{1}$ is not equivalent to the marking $2\cdot s_{4}$, as
only the former can perform the trace $abc$.

A place bisimulation $R$ considers two places $s_{1}$ and $s_{2}$ as
equivalent if $(s_{1},s_{2})\in R$, as, by definition of place bisimulation,
they must behave the same in any $R$-related context. Back to our example in
Figure 12, if $(s_{1},s_{4})$ would belong to $R$, then also $(2\cdot
s_{1},2\cdot s_{4})$ should belong to $R^{\oplus}$, but then we discover that
the place bisimulation game does not hold for this pair of markings, so that
$R$ cannot be a place bisimulation.

Moreover, there are at least the following three important technical
differences between place bisimilarity and other coarser, causality-respecting
equivalences, such as fully-concurrent bisimilarity [5].

  1. 1.

A fully-concurrent bisimulation is a complex relation – composed of cumbersome
triples of the form (process, bijection, process) – that must contain
infinitely many triples if the net system offers never-ending behavior.
(Indeed, not even one single case study of a system with never-ending behavior
has been developed for this equivalence.) On the contrary, a place
bisimulation is always a very simple finite relation over the set of places.
(And a tiny case study is outlined in Example 6.)

  2. 2.

A fully-concurrent bisimulation proving that $m_{1}$ and $m_{2}$ are
equivalent is a relation specifically designed for the initial markings
$m_{1}$ and $m_{2}$. If we want to prove that, e.g., $n\cdot m_{1}$ and
$n\cdot m_{2}$ are fully-concurrent bisimilar (which may not hold!), we have
to construct a new fully-concurrent bisimulation to this aim. Instead, a place
bisimulation $R$ relates those places which are considered equivalent under
all the possible $R$-related contexts. Hence, if $R$ justifies that
$m_{1}\sim_{p}m_{2}$ as $(m_{1},m_{2})\in R^{\oplus}$, then for sure the same
$R$ justifies that $n\cdot m_{1}$ and $n\cdot m_{2}$ are place bisimilar, as
also $(n\cdot m_{1},n\cdot m_{2})\in R^{\oplus}$.

  3. 3.

Finally, while place bisimilarity is decidable, fully-concurrent bisimilarity
is undecidable on finite P/T nets with at least two unbounded places [10].

Incidentally, note that place bisimilarity $\sim_{p}$ is not additive (i.e.,
it is not a congruence w.r.t. multiset union), despite the fact that each
place bisimulation is so (as mentioned above in item 2). In fact, consider the
simple net in Figure 4 discussed in Example 4. As $(s_{1},s_{3})\in R_{3}$, we
have that $s_{1}\sim_{p}s_{3}$; similarly, as $(s_{2},s_{3})\in R_{4}$, we
have $s_{2}\sim_{p}s_{3}$; however, $s_{1}\oplus s_{2}\nsim_{p}2\cdot s_{3}$
because $s_{1}\oplus s_{2}$ can move, while $2\cdot s_{3}$ is stuck.
Additivity (i.e., congruence w.r.t. multiset union) is a very strong property
that does not hold for any of the behavioral equivalences discussed in this
paper. However, [28] studies the problem of characterizing the largest
congruence w.r.t. multiset union refining interleaving bisimulation
$\sim_{int}$ such that it is also a bisimulation; the resulting behavioral
relation, called resource bisimilarity, is proved decidable, even if its
complexity is not studied.

One further criticism against place bisimilarity $\sim_{p}$ may be that its
complexity is too high to be useful in practice. However, on the one hand, we
would like to observe that essentially all the decidable properties over
unbounded finite P/T nets are at least exponential; for instance, about the
reachability problem (i.e., deciding whether a given marking is reachable from
the initial marking), Lipton proved an exponential space lower bound
(EXPSPACE-hard) [27], and none of the algorithms known so far is primitive
recursive (cf., e.g., [29]). On the other hand, we conjecture that our
decision procedure can be improved. In fact, future work will be devoted to
find more efficient algorithms for checking place bisimilarity. One idea could
be to build directly the set of maximal place bisimulations – starting from
the unique maximal equivalence place bisimulation (that can be easily computed
[3]) and then elaborating on it, as we did in Example 4 and 5 – rather than to
scan all the place relations to check whether they are place bisimulations, as
we did in the proof of Theorem 5.1. Moreover, if the goal is not that of
computing the equivalence relation $\sim_{p}$, but simply to prove that two
specific markings, say $m_{1}$ and $m_{2}$, are place bisimilar, one can
simply try to build one particular place bisimulation $R$ such that
$(m_{1},m_{2})\in R^{\oplus}$ (as we did for the tiny case studies of Example
6 and 7), which seems a much simpler task.

We have proposed a slight weakening of place bisimilarity $\sim_{p}$, called
d-place bisimilarity $\sim_{d}$, which may relate places to the empty marking
$\theta$ and which is still decidable. Actually, we conjecture that d-place
bisimilarity is the coarsest, sensible equivalence relation which is decidable
on finite P/T nets (without silent moves). D-place bisimilarity is still
slightly finer than fully-concurrent bisimilarity.

On the subclass of BPP nets (i.e., nets whose transitions have singleton pre-
set), place bisimilarity coincides with team bisimilarity [17], which is
actually coinductive and, for this reason, efficiently decidable (in
polynomial time, by using a generalization of, e.g., the Kanellakis-Smolka’s
algorithm [24]), characterized by a simple modal logic, and even axiomatizable
over the process algebra BPP with guarded summation and guarded recursion
[16]. Team bisimilarity is unquestionably the most appropriate behavioral
equivalence for BPP nets, as it coincides with structure-preserving
bisimilarity [14], hence matching all the relevant criteria expressed in [14]
for a sensible behavioral equivalence. Moreover, d-place bisimilarity
specializes to h-team bisimilarity [19], which coincides with fully-concurrent
bisimilarity on this subclass of P/T nets.

We have also discussed that place bisimilarity is not the coarsest decidable
equivalence for Petri nets proposed in [3]. In fact, we have proved that
i-place bisimilarity $\sim_{i}$ is still decidable, even if not satisfactory
as it does not respect causality. For the sake of exposition completeness, we
have observed that the newly proposed variant i-d-place bisimilarity
$\sim_{id}$ is an even coarser decidable equivalence relation, that is the
coarsest decidable equivalence defined so far on finite Petri nets respecting
the branching time and the concurrent behavior (as it is finer than step
bisimilarity $\sim_{s}$), but not respecting causality.

Extensions of the theory presented in this paper have been sketched in [20],
where the decidable branching place bisimilarity has been proposed for finite
P/T nets with silent moves (taking inspiration from branching bisimilarity on
LTSs [13]), and also in [7], where the decidable pti-place bisimilarity has
been proposed for the Turing-complete model of finite Petri nets with
inhibitor arcs [1, 35]. Future work will be devoted to deepen the study of
these extensions and to experimentally show the usefulness of the place
bisimulation framework over some complex case studies.

## References

  * [1] T. Agerwala, M. Flynn,  Comments on capabilities, limitations and correctness of Petri nets,  SIGARCH Comput. Archit. News, 2(4):81-86, 1973.
  * [2] C. Autant, Z. Belmesk, Ph. Schnoebelen,  Strong bisimilarity on nets revisited,  in Procs. PARLE’91, LNCS 506, 295-312, Springer, 1991.
  * [3] C. Autant, Ph. Schnoebelen,  Place bisimulations in Petri nets,  in Procs. Application and Theory of Petri Nets 1992, LNCS 616, 45-61, Springer, 1992.
  * [4] E. Best, R. Devillers,  Sequential and concurrent behavior in Petri net theory,  Theoretical Computer Science 55(1):87-136, 1987.
  * [5] E. Best, R. Devillers, A. Kiehn, L. Pomello,  Concurrent bisimulations in Petri nets,  Acta Inf. 28(3): 231-264, 1991.
  * [6] M. Bravetti, R. Gorrieri,  Deciding and axiomatizing weak ST bisimulation for a process algebra with recursion and action refinement,  ACM Trans. Comput. Log. 3(4): 465-520, 2002.
  * [7] A. Cesco, R. Gorrieri,  A decidable equivalence for a Turing-complete, distributed model of computation,  in Procs. 46th International Symposium on Mathematical Foundations of Computer Science (MFCS’21), 28:1-28:18, LIPIcs 202, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.
  * [8] P. Degano, R. De Nicola, U. Montanari,  Partial ordering descriptions and observations of nondeterministic concurrent systems,  in (J. W. de Bakker, W. P. de Roever, G. Rozenberg, Eds.)  Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, LNCS 354, 438-466, Springer, 1989.
  * [9] J. Desel, W. Reisig,  Place/Transition Petri nets,  in Lectures on Petri Nets I: Basic Models, LNCS 1491, 122-173, Springer, 1998.
  * [10] J. Esparza,  Decidability and complexity of Petri net problems: An introduction,  Lectures on Petri Nets I: Basic Models,  LNCS 1491, 374-428, Springer, 1998.
  * [11] R.J. van Glabbeek, F. Vaandrager,  Petri Net models for algebraic theories of concurrency,  in Proc. PARLE’87, LNCS 259, 224-242, Springer-Verlag, 1987.
  * [12] R.J. van Glabbeek, U. Goltz,  Equivalence notions for concurrent systems and refinement of actions,  in Procs. MFCS’89, LNCS 379, 237-248, Springer, 1989.
  * [13] R.J. van Glabbeek, W.P. Weijland,  Branching time and abstraction in bisimulation semantics,  Journal of the ACM 43(3):555-600, 1996.
  * [14] R.J. van Glabbeek,  Structure preserving bisimilarity - Supporting an operational Petri net semantics of CCSP,  in (R. Meyer, A. Platzer, H. Wehrheim, Eds.)  Correct System Design — Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, LNCS 9360, 99-130, Springer, 2015.
  * [15] U. Goltz, W. Reisig,  The non-sequential behaviour of Petri nets,  Information and Control 57(2-3):125-147, 1983.
  * [16] R. Gorrieri,  Process Algebras for Petri Nets: The Alphabetization of Distributed Systems,  EATCS Monographs in Computer Science, Springer, 2017.
  * [17] R. Gorrieri,  Team bisimilarity, and its associated modal logic, for BPP nets,  Acta Informatica 58(5):529-569, 2021.
  * [18] R. Gorrieri,  Causal semantics for BPP nets with silent moves,  Fundamenta Informaticae, 180(3):179-249, 2021.
  * [19] R. Gorrieri,  A study on team bisimulation and h-team bisimulation for BPP nets, Theoretical Computer Science 897:83-113, 2022.
  * [20] R. Gorrieri,  Branching place bisimilarity: A decidable behavioral equivalence for finite Petri nets with silent moves,  in Procs. 41st Formal Techniques for Distributed Objects, Components, and Systems (FORTE’21), LNCS 12719, 80-99, Springer, 2021.
  * [21] R. Gorrieri, C. Laneve, Split and ST bisimulation semantics, Inf. Comput. 118(2): 272-288, 1995.
  * [22] J.E. Hopcroft, R.M. Karp,  An $n^{5/2}$ algorithm for maximum matchings in bipartite graphs,  SIAM Journal on Computing, 2 (4): 225-231,1973.
  * [23] P. Janc̆ar,  Undecidability of bisimilarity for Petri nets and some related problems,  Theoretical Computer Science 148(2):281-301, 1995.
  * [24] P. Kanellakis, S. Smolka,  CCS expressions, finite state processes, and three problems of equivalence,  in Procs. 2nd Annual ACM Symposium on Principles of Distributed Computing, 228-240, ACM Press, 1983.
  * [25] A. V. Karzanov, An exact estimate of an algorithm for finding a maximum flow, applied to the problem on representatives, Problems in Cybernetics 5: 66-70, 1973.
  * [26] R. Keller,  Formal verification of parallel programs,  Comm. of the ACM 19(7):561-572, 1976.
  * [27] R. Lipton,  The reachability problem requires exponential space,  Tech. Rep. 63, Yale University, 1976.
  * [28] I.A. Lomazova, V.A. Bashkin, P. Janc̆ar,  Resource bisimilarity in Petri nets is decidable,  Fundamenta Informaticae, 186(1-4):175-194, 2022.
  * [29] E.W. Mayr,  An algorithm for the general Petri net reachability problem,  SIAM J. Comput. 13:441-460, 1984.
  * [30] R. Milner. Communication and Concurrency, Prentice-Hall, 1989.
  * [31] M. Nielsen, P.S. Thiagarajan,  Degrees of non-determinism and concurrency: A Petri net view,  in Procs. of the Fourth Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’84), LNCS 181, 89-117, Springer-Verlag, 1984.
  * [32] E.R. Olderog,  Nets, Terms and Formulas,  Cambridge Tracts in Theoretical Computer Science 23, Cambridge University Press, 1991.
  * [33] R. Paige, R.E. Tarjan,  Three partition refinement algorithms,  SIAM Journal of Computing 16(6):973-989, 1987.
  * [34] D.M.R. Park,  Concurrency and automata on infinite sequences,  In Proc. 5th GI-Conference on Theoretical Computer Science, LNCS 104, 167-183, Springer, 1981.
  * [35] J.L. Peterson,  Petri Net Theory and the Modeling of Systems, Prentice-Hall, 1981.
  * [36] A. Rabinovich, B.A. Trakhtenbrot,  Behavior structures and nets,  Fundamenta Informaticae 11(4):357-404, 1988.
  * [37] W. Reisig,  Petri Nets: An Introduction,  EATCS Monographs in Theor. Comp. Science,  Springer, 1985.
  * [38] W. Reisig,  Elements of Distributed Algorithms: Modeling and Analysis with Petri Nets,  Springer-Verlag, 1998.
  * [39] W. Reisig, G. Rozenberg (eds.),  Lectures on Petri Nets II: Applications,  Lecture Notes in Computer Science 1492,  Springer-Verlag, 1998.