<figure><img src="image_1.png" /></figure>

HAL
open science

# Branching Place Bisimilarity: A Decidable Behavioral Equivalence for Finite Petri Nets with Silent Moves

Roberto Gorrieri

<figure><img src="image_2.png" /></figure>

## To cite this version:

Roberto Gorrieri. Branching Place Bisimilarity: A Decidable Behavioral Equivalence for Finite Petri Nets with Silent Moves. 41th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2021, Valletta, Malta. pp.80-99, 10.1007/978-3-030-78089-0_5. hal-03740270

HAL Id: hal-03740270

https://inria.hal.science/hal-03740270v1

Submitted on 29 Jul 2022

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_3.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
<figure><img src="image_4.png" /></figure>

ifip

International Federation for Information Processing

This document is the original author manuscript of a paper submitted to an IFIP
conference proceedings or other IFIP publication by Springer Nature. As such, there
may be some differences in the official published version of the paper. Such
differences, if any, are usually due to reformatting during preparation for publication or
minor corrections made by the author(s) during final proofreading of the publication
manuscript.
Branching Place Bisimilarity:
A Decidable Behavioral Equivalence
for Finite Petri Nets with Silent Moves

Roberto Gorrieri

roberto.gorrieri@unibo.it

Dipartimento di Informatica — Scienza e Ingegneria
Università di Bologna,
Mura A. Zamboni 7, 40127 Bologna, Italy

**Abstract.** Place bisimilarity ~p is a behavioral equivalence for finite Petri nets, proposed in [1] and proved decidable in [13]. In this paper we propose an extension to finite Petri nets with silent moves of the place bisimulation idea, yielding branching place bisimilarity ≈p, following the intuition of branching bisimilarity [6] on labeled transition systems. We prove that ≈p is a decidable equivalence relation. Moreover, we argue that it is strictly finer than branching fully-concurrent bisimilarity [22, 12], essentially because ≈p does not consider as unobservable those τ-labeled net transitions with pre-set size larger than one, i.e., those resulting from multi-party interaction.

# 1 Introduction

Place bisimilarity, originating from an idea by Olderog [19] (under the name of strong bisimilarity) and then refined by Autant, Belmesk and Schnoebelen [1], is a behavioral equivalence over finite Place/Transition Petri nets (P/T nets, for short), based on relations over the *finite set of net places*, rather than over the (possibly infinite) set of net markings. This equivalence does respect the expected causal behavior of Petri nets; in fact, van Glabbeek proved in [7] that place bisimilarity is slightly finer than *structure preserving bisimilarity* [7], in turn slightly finer than *fully-concurrent bisimilarity* [3]. Place bisimilarity was proved decidable in [13] and, to date, it is the only sensible behavioral equivalence which was proved decidable over finite Petri nets (with the exception of net isomorphism).

This paper aims at extending the place bisimulation idea to Petri nets with silent transitions. To this aim, we take inspiration from *branching bisimilarity*, proposed in [6] over labeled transition systems [16, 8] (LTSs, for short), a behavioral relation more appropriate than weak bisimilarity [17], as it better respects the timing of choices.

The main problem we had to face was to properly understand if and when a silent net transition can be really considered as potentially unobservable. In fact, while in the theory of sequential, nondeterministic systems, modeled by means of LTSs, all the τ-labeled transitions can, to some extent, be abstracted away, in the theory of Petri nets (and of distributed systems, in general), it is rather questionable whether this is the case. For sure a silent net transition with pre-set and post-set of size 1 may be abstracted
away, as it represents some internal computation, local to a single sequential component of the distributed system. However, a τ-labeled net transition with pre-set of size 2 or more, which models a multi-party interaction, is really observable: since to establish the synchronization it is necessary to use some communication infrastructure, for sure one observer can see that such a synchronization takes place. This is, indeed, what happens over the Internet: a communication via IP is an observable event, even if the actual content of the message may be unobservable (in case it is encrypted).

For this reason, our definition of branching place bisimulation considers as potentially unobservable only the so-called τ-sequential transitions, i.e., those silent transitions whose pre-set and post-set have size 1. We prove that branching place bisimilarity $\approx_p$ is an equivalence relation, where the crucial step in this proof is to prove that the relational composition of two branching place bisimulations is a branching place bisimulation. Of course, $\approx_p$ is rather discriminating if compared to other behavioral semantics; in particular, we conjecture that it is strictly finer than branching fully-concurrent bisimilarity [22, 12], essentially because the latter may also abstract w.r.t. silent transitions that are not τ-sequential (and also may relate markings of different size).

The main contribution of this paper is to show that $\approx_p$ is decidable for finite P/T nets. The proof idea is as follows. As a place relation $R \subseteq S \times S$ is finite if the set $S$ of places is finite, there are finitely many place relations for a finite net. We can list all these relations, say $R_1, R_2, \dots, R_n$. It is decidable whether a place relation $R_i$ is a branching place bisimulation by checking two finite conditions over a finite number of marking pairs: this is a non-obvious observation, as a branching place bisimulation requires that the place bisimulation game holds for the infinitely many pairs $m_1$ and $m_2$ which are bijectively related via $R_i$ (denoted by $(m_1, m_2) \in R_i^\oplus$). Hence, to decide whether $m_1 \approx_p m_2$, it is enough to check, for $i=1, \dots, n$, whether $R_i$ is a branching place bisimulation and, in such a case, whether $(m_1, m_2) \in R_i^\oplus$.

The paper is organized as follows. Section 2 recalls the basic definitions about Petri nets. Section 3 recalls the main definitions and results about place bisimilarity. Section 4 introduces branching place bisimilarity and proves that it is an equivalence relation. Section 5 shows that $\approx_p$ is decidable. Finally, in Section 6 we discuss the pros and cons of branching place bisimilarity, and describe related literature and some future research.

## 2 Basic Definitions

**Definition 1. (Multiset)** Let $\mathbb{N}$ be the set of natural numbers. Given a finite set $S$, a multiset over $S$ is a function $m: S \to \mathbb{N}$. The support set $dom(m)$ of $m$ is $\{s \in S \mid 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 $\emptyset$. We write $m \subseteq m'$ if $m(s) \leq m'(s)$ for all $s \in S$. Multiset union $\oplus$ is defined as follows: $(m \oplus m')(s) = m(s) + m'(s)$. 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, \dots, s_n\}$ can be represented as $k_1 \cdot s_1 \oplus k_2 \cdot s_2 \oplus \dots \oplus k_n \cdot s_n$, where $k_j = m(s_j) \ge 0$ for $j = 1, \dots, n$. $\square$

**Definition 2. (Place/Transition net)** A labeled Place/Transition Petri net (P/T net for short) is a tuple $N = (S, A, T)$, where

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

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

* $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')$, we use the notation:

* $\bullet t$ to denote its pre-set $m$ (which cannot be empty) of tokens to be consumed;

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

* $t^\bullet$ to denote its post-set $m'$ of tokens to be produced.

Hence, transition $t$ can be also represented as $\bullet t \xrightarrow{l(t)} t^\bullet$.

<figure><img src="image_5.png" /></figure>

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 from the transition to a place) by the execution of the transition; if the number is omitted, then the weight default value 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. $\square$

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

* $m[\varepsilon]m$ is a firing sequence (where $\varepsilon$ denotes an empty sequence of transitions) and

* if $m[\sigma]m'$ is a firing sequence and $m'[t]m''$, then $m[\sigma t]m''$ is a firing sequence.

If $\sigma = t_1 \dots t_n$ (for $n \ge 0$) and $m[\sigma]m'$ is a firing sequence, then there exist $m_1, \dots, m_{n+1}$ such that $m = m_1[t_1]m_2[t_2]\dots m_n[t_n]m_{n+1} = m'$, and $\sigma = t_1 \dots t_n$ is called a transition sequence starting at $m$ and ending at $m'$.

The definition of pre-set and post-set can be extended to transition sequences as follows: $\bullet \varepsilon = \theta$, $\bullet (t\sigma) = \bullet t \oplus (\bullet \sigma \ominus t^\bullet)$, $\varepsilon^\bullet = \theta$, $(t\sigma)^\bullet = \sigma^\bullet \oplus (t^\bullet \ominus \bullet \sigma)$.

The set of reachable markings from $m$ is $[m] = \{m' \mid \exists \sigma.m[\sigma]m'\}$. Note that the reachable markings can be countably infinitely many. $\square$
**Definition 5. (P/T net with silent moves, τ-sequential)** A P/T net $N = (S,A,T)$ such that $\tau \in A$, where $\tau$ is the only invisible action that can be used to label transitions, is called a P/T net with silent moves.

A transition $t \in T$ is τ-sequential if $l(t) = \tau$ and $|t| = 1 = |\bullet t|$. A P/T net $N$ with silent moves is τ-sequential if $\forall t \in T$ if $l(t) = \tau$, then $t$ is τ-sequential. $\square$

**Definition 6. (Idling transitions, τ-sequential (acyclic) transition sequence)** Given a P/T net $N = (S,A,T)$ with silent moves, the set of idling transitions is $I(S) = \{i(s) \mid s \in S, i(s) = (s, \tau, s)\}$. In defining silent transition sequences, we take the liberty of using also the fictitious idling transitions, so that, e.g., if $\sigma = i(s_1)i(s_2)$, then $s_1 \oplus s_2[\sigma]s_1 \oplus s_2$. Given a transition sequence $\sigma$, its observable label $o(\sigma)$ is computed inductively as:

$$o(\varepsilon) = \varepsilon$$ 
$$o(t\sigma) = \begin{cases} l(t) o(\sigma) & \text{if } l(t) \neq \tau \\ o(\sigma) & \text{otherwise.} \end{cases}$$

A transition sequence $\sigma = t_1 t_2 \dots t_n$ (where $n \ge 1$ and some of the $t_i$ can be idling transitions) is τ-1-sequential if $l(t_i) = \tau$, $|t_i| = 1 = |\bullet t_i|$ for $i = 1, \dots, n$, and $t_i = \bullet t_{i+1}$ for $i = 1, \dots, n-1$, so that $o(\sigma) = \varepsilon$ and $|\sigma| = 1 = |\bullet \sigma|$.

A transition sequence $\sigma = \sigma_1 \sigma_2 \dots \sigma_k$ is τ-k-sequential if $\sigma_i$ is τ-1-sequential for $i = 1, \dots, k$, $\bullet \sigma = \bullet \sigma_1 \oplus \bullet \sigma_2 \oplus \dots \oplus \bullet \sigma_k$ and $\sigma^\bullet = \sigma_1^\bullet \oplus \sigma_2^\bullet \oplus \dots \oplus \sigma_k^\bullet$, so that $o(\sigma) = \varepsilon$ and $|\sigma^\bullet| = k = |\bullet \sigma|$. We say that $\sigma$ is τ-sequential if it is τ-k-sequential for some $k \ge 1$.

A τ-1-sequential $\sigma = t_1 t_2 \dots t_n$ is acyclic if $\bullet \sigma = m_0[t_1]m_1[t_2]m_2 \dots m_{n-1}[t_n]m_n = \sigma^\bullet$ and $m_i \neq m_j$ for all $i \neq j$, with $i, j \in \{1, 2, \dots, n\}$. A τ-k-sequential $\sigma = \sigma_1 \sigma_2 \dots \sigma_k$ is acyclic if $\sigma_i$ is acyclic and τ-1-sequential for $i = 1, \dots, k$. We say that $\sigma$ is an acyclic τ-sequential transition sequence if it is acyclic and τ-k-sequential for some $k \ge 1$. $\square$

**Remark 1. (Acyclic τ-sequential transition sequence)** The definition of acyclic τ-1-sequential transition sequence is a bit non-standard as it may allow for a cycle when the initial marking and the final one are the same. For instance, $\sigma = i(s)i(s)$ is cyclic, while the apparently cyclic subsequence $\sigma' = i(s)$ is actually acyclic, according to our definition. Note that, given a τ-1-sequential transition sequence $\sigma$, it is always possible to find an acyclic τ-1-sequential transition sequence $\sigma'$ such that $\bullet \sigma = \bullet \sigma'$ and $\sigma^\bullet = \sigma'^\bullet$. For instance, if $\bullet \sigma = m_0[t_1]m_1[t_2]m_2 \dots m_{n-1}[t_n]m_n = \sigma^\bullet$ and the only cycle is given by $m_i[t_{i+1}]m_{i+1} \dots m_{j-1}[t_j]m_j$ with $m_i = m_j$ and $i \ge 1$, then $\sigma' = t_1 t_2 \dots t_i t_{i+1} \dots t_n$ is acyclic and $\bullet \sigma = \bullet \sigma'$ and $\sigma^\bullet = \sigma'^\bullet$.

Note also that, given a τ-k-sequential transition sequence $\sigma = \sigma_1 \sigma_2 \dots \sigma_k$, it is always possible to find an acyclic τ-k-sequential transition sequence $\sigma' = \sigma'_1 \sigma'_2 \dots \sigma'_k$, where $\sigma'_i$ is the acyclic τ-1-sequential transition sequence corresponding to $\sigma_i$ for $i = 1, 2, \dots, k$, in such a way that $\bullet \sigma = \bullet \sigma'$ and $\sigma^\bullet = \sigma'^\bullet$. Finally, note that, given two markings $m_1$ and $m_2$ of equal size $k$, it is decidable whether there exists an acyclic τ-k-sequential transition $\sigma$ such that $\bullet \sigma = m_1$ and $\sigma^\bullet = m_2$. $\square$

**Definition 7. (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

* $\forall t_1$ such that $m_1[t_1]m_1^\prime, \exists t_2$ such that $m_2[t_2]m_2^\prime$ with $l(t_1) = l(t_2)$ and $(m_1^\prime, m_2^\prime) \in R$,

* $\forall t_2$ such that $m_2[t_2]m_2^\prime, \exists t_1$ such that $m_1[t_1]m_1^\prime$ with $l(t_1) = l(t_2)$ and $(m_1^\prime, m_2^\prime) \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$. $\square$

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

**Definition 8.** (Branching interleaving bisimulation) Let $N = (S, A, T)$ be a P/T net with silent moves. A branching interleaving bisimulation is a relation $R \subseteq \mathcal{M}(S) \times \mathcal{M}(S)$ such that if $(m_1, m_2) \in R$ then

* $\forall t_1$ such that $m_1[t_1]m'_1$,
  - either $l(t_1) = \tau$ and $\exists \sigma_2$ such that $o(\sigma_2) = \varepsilon, m_2[\sigma_2]m'_2$ with $(m_1, m'_2) \in R$ and $(m'_1, m'_2) \in R$,
  - or $\exists \sigma, t_2$ such that $o(\sigma) = \varepsilon, l(t_1) = l(t_2), m_2[\sigma]m[t_2]m'_2$ with $(m_1, m) \in R$ and $(m'_1, m'_2) \in R$,

* and, symmetrically, $\forall t_2$ such that $m_2[t_2]m'_2$.

Two markings $m_1$ and $m_2$ are branching interleaving bisimilar, denoted $m_1 \approx_{bri} m_2$, if there exists a branching interleaving bisimulation $R$ that relates them. $\square$

This definition is not a rephrasing on nets of the original definition on LTSs in [6], rather of a slight variant called semi-branching bisimulation [6, 2], which gives rise to the same equivalence relation as the original definition but has better mathematical properties. Branching interleaving bisimilarity $\approx_{bri}$ is the largest branching interleaving bisimulation and also an equivalence relation. Of course, also branching interleaving bisimilarity is undecidable for finite P/T nets.

## 3 Place Bisimilarity

We now present place bisimulation, introduced in [1] as an improvement of strong bisimulation, a behavioral relation proposed by Olderog in [19] on safe nets which fails to induce an equivalence relation. Our definition is formulated in a slightly different way, but it is coherent with the original one. First, an auxiliary definition.

**Definition 9.** (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.

$$ \frac{\frac{(s_1, s_2) \in R \quad (m_1, m_2) \in R^{\oplus}}{(\theta, \theta) \in R^{\oplus}}}{(s_1 \oplus m_1, s_2 \oplus m_2) \in R^{\oplus}} \quad \square $$
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|$. $\square$

Note also that there may be several proofs of $(m_1, m_2) \in R^{\oplus}$, 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 \dots \oplus s_k$, $m_2$ can be represented as $s'_1 \oplus s'_2 \oplus \dots \oplus s'_k$ and $(s_i, s'_i) \in R$ for $i = 1, \dots, k$. In fact, a 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 \dots \oplus s_k$ and then scan all the possible permutations of $m_2$, each represented as $s'_1 \oplus s'_2 \oplus \dots \oplus s'_k$, to check that $(s_i, s'_i) \in R$ for $i = 1, \dots, k$. Of course, this naive algorithm is in $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 that $(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 fail because the residual $(s_2, s_3)$ is not in $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$. $\square$

Nonetheless, the problem of checking whether $(m_1, m_2) \in R^{\oplus}$ has polynomial time complexity because it can be considered as an instance of the problem of finding a perfect matching in a bipartite graph, where the nodes of the two partitions 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 [14] for computing the maximum matching has worst-case time complexity $O(h\sqrt{k})$, where $h$ is the number of the edges in the bipartite graph ($h \le 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})$.

**Proposition 2.** [10] For each place relation $R \subseteq S \times S$, the following hold:

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

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

3. If $(m_1, m_2) \in R^{\oplus}$ and $(m'_1, m'_2) \in R^{\oplus}$, then $(m_1 \oplus m'_1, m_2 \oplus m'_2) \in R^{\oplus}$, i.e., the additive closure is additive. $\square$

**Proposition 3.** [10] For each family of place relations $R_i \subseteq S \times S$, the following hold:

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

2. $(\mathcal{I}_S)^{\oplus} = \mathcal{I}_M$, i.e., the additive closure of the identity relation on places $\mathcal{I}_S = \{(s, s) \mid s \in S\}$ is the identity relation on markings $\mathcal{I}_M = \{(m, m) \mid m \in \mathcal{M}(S)\}$.
<figure><img src="image_6.png" /><figcaption>Fig. 1. A simple net</figcaption></figure>

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

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 is the compositions of their additive closures. $\square$

**Definition 10. (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

* $\forall t_1$ such that $m_1[t_1\rangle m'_1, \exists t_2$ such that $m_2[t_2\rangle m'_2$ with $(\bullet t_1, \bullet t_2) \in R^\oplus$, $l(t_1) = l(t_2)$, $(t'_1, t'_2) \in R^\oplus$ and $(m'_1, m'_2) \in R^\oplus$,

* $\forall t_2$ such that $m_2[t_2\rangle m'_2, \exists t_1$ such that $m_1[t_1\rangle m'_1$ with $(\bullet t_1, \bullet t_2) \in R^\oplus$, $l(t_1) = l(t_2)$, $(t'_1, t'_2) \in R^\oplus$ and $(m'_1, m'_2) \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$. $\square$

**Proposition 4.** [1, 13] For each P/T net $N = (S, A, T)$, relation $\sim_p \subseteq \mathcal{M}(S) \times \mathcal{M}(S)$ is an equivalence relation. $\square$

By Definition 10, place bisimilarity can be defined as follows:

$$ \sim_p = \bigcup \{R^\oplus \mid R \text{ 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 \mid R \text{ is a maximal place bisimulation}\}. $$

However, it is not true that

$$ \sim_p = (\bigcup \{R \mid R \text{ is a maximal place bisimulation}\})^\oplus $$

because the union of place bisimulations may not be a place bisimulation, so that its definition is not coinductive. We illustrate this fact by means of the following example.

**Example 2.** Consider the simple P/T net in Figure 1, with $S = \{s_1, s_2, s_3\}$. It is rather easy to realize that there are only two maximal place bisimulations, namely:

$$ R_1 = \mathcal{I}_S = \{(s_1, s_1), (s_2, s_2), (s_3, s_3)\} \text{ 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)\}, $$

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$. $\square$
## 4 Branching Place Bisimilarity

Now we define a variant of place bisimulation, which is insensitive, to some extent, to τ-sequential transitions, i.e., τ-labeled transitions whose pre-set and post-set have size one. This relation is inspired to (semi-)branching bisimulation [6, 2], a behavioral relation defined over LTSs. In its definition, we use τ-sequential transition sequences, usually denoted by $\sigma$, which are sequences composed of τ-sequential transitions in $T \cup I(S)$, i.e., τ-sequential net transitions and also idling transitions.

**Definition 11. (Branching place bisimulation)** Given a P/T net $N = (S, A, T)$, a branching place bisimilarity is a relation $R \subseteq S \times S$ such that if $(m_1, m_2) \in R^\oplus$

1. $\forall t_1$ such that $m_1[t_1]m'_1$

(i) either $t_1$ is τ-sequential and $\exists \sigma, m'_2$ such that $\sigma$ is τ-sequential, $m_2[\sigma]m'_2$, and $(\bullet t_1, \bullet \sigma) \in R$, $(\bullet t_1, \sigma^\bullet) \in R$, $(t'_1, \sigma^\bullet) \in R$ and $(m_1 \ominus \bullet t_1, m_2 \ominus \bullet \sigma) \in R^\oplus$;

(ii) or there exist $\sigma, t_2, m, m'_2$ such that $\sigma$ is τ-sequential, $m_2[\sigma]m[t_2]m'_2$, $l(t_1) = l(t_2)$, $\sigma^\bullet = \bullet t_2$, $(\bullet t_1, \bullet \sigma) \in R^\oplus$, $(\bullet t_1, \bullet t_2) \in R^\oplus$ $(t'_1, t'_2) \in R^\oplus$, and moreover, $(m_1 \ominus \bullet t_1, m_2 \ominus \bullet \sigma) \in R^\oplus$;

2. and, symmetrically, $\forall t_2$ such that $m_2[t_2]m'_2$

(i) either $t_2$ is τ-sequential and $\exists \sigma, m'_1$ such that $\sigma$ is τ-sequential, $m_1[\sigma]m'_1$, and $(\bullet \sigma, \bullet t_2) \in R$, $(\sigma^\bullet, \bullet t_2) \in R$, $(\sigma^\bullet, t'_2) \in R$ and $(m_1 \ominus \bullet \sigma, m_2 \ominus \bullet t_2) \in R^\oplus$;

(ii) or there exist $\sigma, t_1, m, m'_1$ such that $\sigma$ is τ-sequential, $m_1[\sigma]m[t_1]m'_1$, $l(t_1) = l(t_2)$, $\sigma^\bullet = \bullet t_1$, $(\bullet \sigma, \bullet t_2) \in R^\oplus$, $(\bullet t_1, \bullet t_2) \in R^\oplus$ $(t'_1, t'_2) \in R^\oplus$, and moreover, $(m_1 \ominus \bullet \sigma, m_2 \ominus \bullet t_2) \in R^\oplus$.

Two markings $m_1$ and $m_2$ are branching place bisimulation equivalent, denoted by $m_1 \approx_p m_2$, if there exists a branching place bisimulation $R$ such that $(m_1, m_2) \in R^\oplus$. $\square$

Note that, in the either case, by additivity of $R^\oplus$ (cf. Proposition 2(3)), from $(m_1 \ominus \bullet t_1, m_2 \ominus \bullet \sigma) \in R^\oplus$ and $(\bullet t_1, \sigma^\bullet) \in R$, we get $(m_1, m'_2) \in R^\oplus$, as well as, from $(t'_1, \sigma^\bullet) \in R$ we get $(m'_1, m'_2) \in R^\oplus$. Similarly for the or case.

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

(i) The identity relation $\mathcal{I}_S$ is a branching place bisimulation.

(ii) The inverse relation $R^{-1}$ of a branching place bisimulation $R$ is a branching place bisimulation.

*Proof.* Case (i) is obvious. For case (ii), assume $(m_2, m_1) \in (R^{-1})^\oplus$ and $m_2[t_2]m'_2$. By Proposition 3(3), we have that $(m_2, m_1) \in (R^\oplus)^{-1}$ and so $(m_1, m_2) \in R^\oplus$. Since $R$ is a branching place bisimulation, we have that

(i) either $t_2$ is τ-sequential and $\exists \sigma, m'_1$ such that $\sigma$ is τ-sequential, $m_1[\sigma]m'_1$, and $(\bullet \sigma, \bullet t_2) \in R$, $(\sigma^\bullet, \bullet t_2) \in R$, $(\sigma^\bullet, t'_2) \in R$ and, moreover, $(m_1 \ominus \bullet \sigma, m_2 \ominus \bullet t_2) \in R^\oplus$;

(ii) or there exist $\sigma, t_1, m, m'_1$ such that $\sigma$ is τ-sequential, $m_1[\sigma]m[t_1]m'_1$, $l(t_1) = l(t_2)$, $\sigma^\bullet = \bullet t_1$, $(\bullet \sigma, \bullet t_2) \in R^\oplus$, $(\bullet t_1, \bullet t_2) \in R^\oplus$ $(t'_1, t'_2) \in R^\oplus$, and $(m_1 \ominus \bullet \sigma, m_2 \ominus \bullet t_2) \in R^\oplus$.

Summing up, if $(m_2, m_1) \in (R^{-1})^\oplus$ and $m_2[t_2]m'_2$ (the case when $m_1$ moves first is symmetric, and so omitted), then
(i) either $t_2$ is $\tau$-sequential and $\exists \sigma, m'_1$ such that $\sigma$ is $\tau$-sequential, $m_1[\sigma]m'_1$, and
    $(\cdot_{t_2}, \cdot_{\sigma}) \in R^{-1}$, $(\cdot_{t_2}, \cdot_{\sigma^*}) \in R^{-1}$, $(t'_2, \sigma^*) \in R^{-1}$ and $(m_2 \ominus \cdot_{t_2}, m_1 \ominus \cdot_{\sigma}) \in (R^{-1})^{\oplus}$;

(ii) or there exist $\sigma, t_1, m, m'_1$ such that $\sigma$ is $\tau$-sequential, $m_1[\sigma]m[t_1]m'_1$, $l(t_1) = l(t_2)$, $\sigma^* = \cdot_{t_1}$, $(\cdot_{t_2}, \cdot_{\sigma}) \in (R^{-1})^{\oplus}$, $(\cdot_{t_2}, \cdot_{t_1}) \in (R^{-1})^{\oplus}$, $(t'_2, t'_1) \in (R^{-1})^{\oplus}$, and, moreover, $(m_2 \ominus \cdot_{t_2}, m_1 \ominus \cdot_{\sigma}) \in (R^{-1})^{\oplus}$;

so that $R^{-1}$ is a branching place bisimulation, indeed. $\square$

Much more challenging is to prove that the relation composition of two branching
place bisimulations is a branching place bisimulation. We need a technical lemma first.

**Lemma 1.** Let $N = (S,A,T)$ be a P/T net, and $R$ be a place bisimulation.

1. For each $\tau$-sequential transition sequence $\sigma_1$, for all $m_2$ such that $(\cdot \sigma_1, m_2) \in R^{\oplus}$, a $\tau$-sequential transition sequence $\sigma_2$ exists such that $m_2 = \cdot \sigma_2$ and $(\sigma_1^*, \sigma_2^*) \in R^{\oplus}$;

2. and symmetrically, for each $\tau$-sequential transition sequence $\sigma_2$, for all $m_1$ such that $(m_1, \cdot \sigma_2) \in R^{\oplus}$, a $\tau$-sequential transition sequence $\sigma_1$ exists such that $m_1 = \cdot \sigma_1$ and $(\sigma_1^*, \sigma_2^*) \in R^{\oplus}$.

*Proof.* By symmetry, we prove only case 1, by induction on the length of $\sigma_1$.

Base case: $\sigma_1 = \varepsilon$. In this trivial case, $\cdot \sigma_1 = \theta$ and so the only possible $m_2$ is $\theta$ as
well. We just take $\sigma_2 = \varepsilon$ and all the required conditions are trivially satisfied.

Inductive case: $\sigma_1 = \delta_1 t_1$, where $t_1 \in T \cup I(S)$. Hence, by inductive hypothesis, for each $m_2$ such that $(\cdot \delta_1, m_2) \in R^{\oplus}$, we know that there exists a $\delta_2$ such that $m_2 = \cdot \delta_2$ and $(\delta_1^*, \delta_2^*) \in R^{\oplus}$.

If $t_1 = i(s)$, then we have to consider two subcases:

* if $s \in \delta_1^*$, then $\cdot \delta_1 t_1 = \cdot \delta_1$ and $\delta_1 t_1^* = \delta_1^*$. Hence, we can take $\sigma_2 = \delta_2$ and all the required conditions are trivially satisfied;

* if $s \notin \delta_1^*$, then $\cdot \delta_1 t_1 = \cdot \delta_1 \oplus s$ and $\delta_1 t_1^* = \delta_1^* \oplus s$. Then, $\forall s'$ such that $(s, s') \in R$, we can take $\sigma_2 = \delta_2 i(s')$, so that $(\cdot \delta_1 t_1, \cdot \delta_2 i(s')) \in R^{\oplus}$, $(\delta_1 t_1^*, \delta_2 i(s')^*) \in R^{\oplus}$, as required.

Also if $t_1 \in T$, we have consider two subcases:

* If $s_1 = \cdot t_1 \in \delta_1^*$, then, since $(\delta_1^*, \delta_2^*) \in R^{\oplus}$, there exists $s_2 \in \delta_2^*$ such that $(s_1, s_2) \in R$ and $(\delta_1^* \ominus s_1, \delta_2^* \ominus s_2) \in R^{\oplus}$. Then, by Definition 11, it follows that to the move $s_1 \xrightarrow{\tau} s_1'$:

(i) Either there exist $\sigma, s'_2$ such that $\sigma$ is $\tau$-sequential, $s_2[\sigma]s'_2$, $(s_1, s'_2) \in R$ and $(s'_1, s'_2) \in R$.

In this case, we take $\sigma_2 = \delta_2 \sigma$, so that $(\cdot \delta_1 t_1, \cdot \delta_2 \sigma) \in R^{\oplus}$ (because $\cdot \delta_1 t_1 = \cdot \delta_1$ and $\cdot \delta_2 \sigma = \cdot \delta_2$), and $(\delta_1 t_1^*, \delta_2 \sigma^*) \in R^{\oplus}$ (because $\delta_1 t_1^* = (\delta_1^* \ominus s_1) \oplus s'_1$ and $\delta_2 \sigma^* = (\delta_2^* \ominus s_2) \oplus s'_2$), as required.

(ii) Or there exist $\sigma, t_2, \bar{s}, s'_2$ such that $\sigma t_2$ is $\tau$-sequential, $\sigma^* = \cdot t_2$, $s_2[\sigma] \bar{s} [t_2] s'_2$, $(s_1, \bar{s}) \in R$ and $(s'_1, s'_2) \in R$.

In this case, we take $\sigma_2 = \delta_2 \sigma t_2$, so that $(\cdot \delta_1 t_1, \cdot \delta_2 \sigma t_2) \in R^{\oplus}$, and, moreover,
$(\delta_1 t_1^*, \delta_2 \sigma t_2^*) \in R^{\oplus}$, as required.

* If $s_1 = \cdot t_1 \notin \delta_1^*$, then, for each $s_2$ such that $(s_1, s_2) \in R$, we follow the same step as above (by Definition 11), and so we omit this part of the proof.
**Proposition 6.** For each P/T net $N = (S,A,T)$, the relational composition $R_1 \circ R_2$ of two branching place bisimulations $R_1$ and $R_2$ is a branching place bisimulation.

*Proof.* Assume $(m_1, m_3) \in (R_1 \circ R_2)^{\oplus}$ and $m_1[t_1]m_1'$. By Proposition 3(4), we have that $(m_1, m_3) \in (R_1)^{\oplus} \circ (R_2)^{\oplus}$, and so $m_2$ exists such that $(m_1, m_2) \in R_1^{\oplus}$ and $(m_2, m_3) \in R_2^{\oplus}$. As $(m_1, m_2) \in R_1^{\oplus}$ and $R_1$ is a branching place bisimulation, if $m_1[t_1]m_1'$, then

(i) either $t_1$ is $\tau$-sequential and $\exists \sigma, m_2' \text{ such that } \sigma \text{ is } \tau$-sequential, $m_2[\sigma]m_2'$, and $(\bullet t_1, \bullet \sigma) \in R_1$, $(\bullet t_1, \sigma') \in R_1$, $(t_1^*, \sigma') \in R_1$ and $(m_1 \ominus \bullet t_1, m_2 \ominus \bullet \sigma) \in R_1^{\oplus}$;

(ii) or there exist $\sigma, t_2, m, m_2'$ such that $\sigma$ is $\tau$-sequential, $m_2[\sigma]m[t_2]m_2'$, $l(t_1) = l(t_2)$, $\sigma^\bullet = \bullet t_2$, $(\bullet t_1, \bullet \sigma) \in R_1^{\oplus}, (\bullet t_1, \bullet t_2) \in R_1^{\oplus} (t_1^*, t_2') \in R_1^{\oplus}$, and moreover, $(m_1 \ominus \bullet t_1, m_2 \ominus \bullet \sigma) \in R_1^{\oplus}$.

Let us consider case (i), i.e., assume that to the move $m_1[t_1]m_1'$, $m_2$ replies with $m_2[\sigma]m_2'$ such that $(\bullet t_1, \bullet \sigma) \in R_1$, $(\bullet t_1, \sigma') \in R_1$, $(t_1^*, \sigma') \in R_1$ and, moreover, $(m_1 \ominus \bullet t_1, m_2 \ominus \bullet \sigma) \in R_1^{\oplus}$. Since $(m_2, m_3) \in R_2^{\oplus}$, there exists a submarking $\bar{m} \subseteq m_3$ such that $(\bullet \sigma, \bar{m}) \in R_2^{\oplus}$ and $(m_2 \ominus \bullet \sigma, m_3 \ominus \bar{m}) \in R_2^{\oplus}$. By Lemma 1, there exists a $\tau$-sequential transition sequence $\sigma'$ such that $\bar{m} = \bullet \sigma'$ and $(\sigma^\bullet, \sigma'^\bullet) \in R_2^{\oplus}$. Hence, $m_3[\sigma']m_3'$, where $m_3' = (m_3 \ominus \bullet \sigma') \oplus \sigma'^\bullet$.

Summing up, to the move $m_1[t_1]m_1'$, $m_3$ can reply with $m_3[\sigma']m_3'$, in such a way that $(\bullet t_1, \bullet \sigma') \in R_1 \circ R_2$, $(\bullet t_1, \sigma') \in R_1 \circ R_2$, $(t_1^*, \sigma') \in R_1 \circ R_2$ and, moreover, $(m_1 \ominus \bullet t_1, m_3 \ominus \bullet \sigma') \in (R_1 \circ R_2)^{\oplus}$, (by Proposition 3(4)), as required.

Let us consider case (ii), i.e., assume that to the move $m_1[t_1]m_1'$, $m_2$ replies with $m_2[\sigma]m[t_2]m_2'$, where $\sigma$ is $\tau$-sequential, $l(t_1) = l(t_2)$, $\sigma^\bullet = \bullet t_2$, and $(\bullet t_1, \bullet \sigma) \in R_1^{\oplus}$, $(\bullet t_1, \bullet t_2) \in R_1^{\oplus}, (t_1^*, t_2') \in R_1^{\oplus}$, and moreover, $(m_1 \ominus \bullet t_1, m_2 \ominus \bullet \sigma) \in R_1^{\oplus}$.

Since $(m_2, m_3) \in R_2^{\oplus}$, there exists a submarking $\bar{m} \subseteq m_3$ such that $(\bullet \sigma, \bar{m}) \in R_2^{\oplus}$ and $(m_2 \ominus \bullet \sigma, m_3 \ominus \bar{m}) \in R_2^{\oplus}$. By Lemma 1, there exists a $\tau$-sequential transition sequence $\sigma'$ such that $\bar{m} = \bullet \sigma'$ and $(\sigma^\bullet, \sigma'^\bullet) \in R_2^{\oplus}$. Hence, $m_3[\sigma']m'$, where $m' = (m_3 \ominus \bullet \sigma') \oplus \sigma'^\bullet$ and, moreover, $(m, m') \in R_2^{\oplus}$.

Since $(m, m') \in R_2^{\oplus}$, $\sigma^\bullet = \bullet t_2$ and $(\sigma^\bullet, \sigma'^\bullet) \in R_2^{\oplus}$, there exists $\underline{m} = \sigma'^\bullet \subseteq m'$ such that $(\bullet t_2, \underline{m}) \in R_2^{\oplus}$ and $(m \ominus \bullet t_2, m' \ominus \underline{m}) \in R_2^{\oplus}$. Hence, by Definition 11, to the move $\bullet t_2[t_2]t_2^*$, $\underline{m}$ can reply as follows:

(a) Either $t_2$ is $\tau$-sequential and $\exists \bar{\sigma}$ such that $\bar{\sigma}$ is $\tau$-sequential, $\underline{m} = \bullet \bar{\sigma}$, $\underline{m}[\bar{\sigma}]\bar{\sigma}^\bullet$, and $(\bullet t_2, \bullet \bar{\sigma}) \in R_2$, $(\bullet t_2, \bar{\sigma}^\bullet) \in R_2$, $(t_2^*, \bar{\sigma}^\bullet) \in R_2$ and $(m \ominus \bullet t_2, m' \ominus \bullet \bar{\sigma}) \in R_2^{\oplus}$.

In this case, to the move $m_1[t_1]m_1'$, $m_3$ can reply with $m_3[\sigma']m'[\bar{\sigma}]m_3'$, with $m_3' = (m' \ominus \bullet \bar{\sigma}) \oplus \bar{\sigma}^\bullet$, such that $(\bullet t_1, \bullet \sigma'\bar{\sigma}) \in (R_1 \circ R_2)^{\oplus}$ (because $(\bullet t_1, \bullet \sigma) \in R_1^{\oplus}$, $\sigma'^\bullet = \bullet \bar{\sigma}$ and $(\bullet \sigma, \bullet \sigma') \in R_2^{\oplus})$, $(\bullet t_1, \sigma'\bar{\sigma}^\bullet) \in (R_1 \circ R_2)^{\oplus}$ (because $(\bullet t_1, \bullet t_2) \in R_1$, $\sigma'^\bullet = \bullet \bar{\sigma}$ and $(\bullet t_2, \bar{\sigma}^\bullet) \in R_2$), $(t_1^*, \sigma'\bar{\sigma}^\bullet) \in (R_1 \circ R_2)^{\oplus}$ (as $(t_1^*, t_2^*) \in R_1$ and $(t_2^*, \bar{\sigma}^\bullet) \in R_2$), and, moreover, $(m_1 \ominus \bullet t_1, m_3 \ominus \bullet \sigma'\bar{\sigma}) \in (R_1 \circ R_2)^{\oplus}$.

(b) or $\exists \bar{\sigma}, t_3, \bar{m}$ such that $\bar{\sigma}$ is $\tau$-sequential, $\underline{m} = \bullet \bar{\sigma}$, $\underline{m}[\bar{\sigma}]\bar{m}[t_3]t_3^*$, $l(t_2) = l(t_3)$, $\bar{m} = \bar{\sigma}^\bullet = \bullet t_3$, $(\bullet t_2, \bullet \bar{\sigma}) \in R_2^{\oplus}, (\bullet t_2, \bullet t_3) \in R_2^{\oplus} (t_2^*, t_3^*) \in R_2^{\oplus}$, and $(m \ominus \bullet t_2, m' \ominus \bullet \bar{\sigma}) \in R_2^{\oplus}$.

In this case, to the move $m_2[\sigma]m[t_2]m_2'$, $m_3$ replies with $m_3[\sigma']m'[\bar{\sigma}]m''[t_3]m_3'$, with $m_3' = (m' \ominus \bullet \bar{\sigma}) \oplus t_3^*$, such that $\bar{\sigma}$ is $\tau$-sequential, $\bullet \bar{\sigma} = \sigma'^\bullet$, and therefore $(\bullet \sigma t_2, \bullet \sigma'\bar{\sigma}t_3) \in R_2^{\oplus}$ (because $\bullet \sigma t_2 = \bullet \sigma$, $\bullet \sigma'\bar{\sigma}t_3 = \bullet \sigma'$ and $(\bullet \sigma, \bullet \sigma') \in R_2^{\oplus}$), and $(\sigma t_2^*, \sigma'\bar{\sigma}t_3^*) \in R_2^{\oplus}$ (because $\sigma t_2^* = t_2^*$, $\sigma'\bar{\sigma}t_3^* = t_3^*$ and $(t_2^*, t_3^*) \in R_2^{\oplus}$).

Summing up, to the move $m_1[t_1]m_1'$, $m_3$ can reply with $m_3[\sigma']m'[\bar{\sigma}]m''[t_3]m_3'$, such that $(\bullet t_1, \bullet \sigma'\bar{\sigma}) \in (R_1 \circ R_2)^{\oplus}$ (as $(\bullet t_1, \bullet \sigma) \in R_1^{\oplus}$, $\bullet \sigma'\bar{\sigma} = \bullet \sigma'$ and $(\bullet \sigma, \bullet \sigma') \in R_2^{\oplus}$),
<figure><img src="image_7.png" /><figcaption>**Fig. 2.** Some simple nets with silent moves</figcaption></figure>

(•t₁, •t₃) ∈ (R₁ ○ R₂)⊕ (as (•t₁, •t₂) ∈ R₁⊕, and (•t₂, •t₃) ∈ R₂⊕), (t₁•, t₃•) ∈ (R₁ ○ R₂)⊕
(because (t₁•, t₂•) ∈ R₁⊕, and (t₂•, t₃•) ∈ R₂⊕), and (m₁ ⊖ •t₁, m₃ ⊖ •σ'σ) ∈ (R₁ ○ R₂)⊕
(because (m₁ ⊖ •t₁, m₂ ⊖ •σ) ∈ R₁⊕ and (m₂ ⊖ •σ, m₃ ⊖ •σ') ∈ R₂⊕).

The case when $m_2$ moves first is symmetric, and so omitted. Hence, $R_1 \circ R_2$ is a branch-
ing place bisimulation, indeed. $\square$

**Theorem 1.** For each P/T net $N = (S, A, T)$, relation $\approx_p \subseteq \mathcal{M}(S) \times \mathcal{M}(S)$ is an equivalence relation.

*Proof.* Direct consequence of Propositions 5 and 6. $\square$

**Proposition 7. (Branching place bisimilarity is finer than branching interleaving bisimilarity)** For each P/T net $N = (S, A, T)$, $m_1 \approx_p m_2$ implies $m_1 \approx_{\text{bri}} m_2$.

*Proof.* If $m_1 \approx_p m_2$, then $(m_1, m_2) \in R^{\oplus}$ for some branching place bisimulation $R$. Note that $R^{\oplus}$ is a branching interleaving bisimilarity, so that $m_1 \approx_{\text{bri}} m_2$. $\square$

**Example 3.** Consider the nets in Figure 2. Of course, $s_1 \approx_p s_2$, as well as $s_1 \approx_{\tau} s_4$. However, $s_2 \not\approx_p s_5$, because $s_2$ cannot respond to the non-$\tau$-sequential move $s_5 \xrightarrow{\tau} \theta$. For the same reason, $s_2 \not\approx_p s_6$. Note that silent transitions that are not $\tau$-sequential are not considered as unobservable. $\square$

By Definition 11, branching place bisimilarity can be defined as follows:

$$
\approx_p = \bigcup \{ \mathcal{R}^{\oplus} \mid R \text{ is a branching 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 branching place bisimulations only:

$$
\sim_p = \bigcup \{ \mathcal{R}^{\oplus} \mid R \text{ is a maximal branching place bisimulation} \}.
$$

However, it is not true that

$\sim_p = (\bigcup\{R \mid R \text{ is a maximal place bisimulation}\})^{\oplus},$ because the union of branching
place bisimulations may be not a branching place bisimulation.

**Example 4.** Consider the nets in Figure 3. It is easy to realize that $s_1 \oplus s_2 \approx_p s_3 \oplus s_5$, because $R_1 = \{(s_1, s_3), (s_2, s_5), (s_1, s_4)\}$ is a branching place bisimulation. In fact, to the move $t_1 = s_1 \oplus s_2 \xrightarrow{a} s_1 \oplus s_2$, $s_3 \oplus s_5$ replies with $s_3 \oplus s_5[\sigma]s_4 \oplus s_5[t_2]s_3 \oplus s_5$, where $\sigma = t_i(s_5)$ (with $t = (s_3, \tau, s_4)$ and $i(s_5) = (s_5, \tau, s_5)$) and $t_2 = (s_4 \oplus s_5, a, s_3 \oplus s_5)$, such that $(\bullet t_1, \bullet t_2) \in R_1^{\oplus}$ and $(t_1^{\bullet}, t_2^{\bullet}) \in R_1^{\oplus}$. Then, to the move $s_3 \oplus s_5[t]s_4 \oplus s_5$, $s_1 \oplus s_2$ can reply
<figure><img src="image_8.png" /><figcaption>**Fig. 3.** Some branching place bisimilar nets</figcaption></figure>

by idling with $s_1 \oplus s_2[\sigma']s_1 \oplus s_2$, where $\sigma' = i(s_1)$, and $(\bullet\sigma', \bullet t) \in R_1^{\oplus}$, $(\sigma'\bullet, \bullet t) \in R_1^{\oplus}$ and $(\sigma'\bullet, t\bullet) \in R_1^{\oplus}$.

Note that also the identity relation $\mathcal{I}_S$, where $S = \{s_1, s_2, s_3, s_4, s_5\}$ is a branching place bisimulation. However, $R = R_1 \cup \mathcal{I}_S$ is not a branching place bisimulation, because, for instance, $(s_1 \oplus s_2, s_3 \oplus s_2) \in R^{\oplus}$, but these two markings are clearly not equivalent, as $s_1 \oplus s_2$ can do $a$, while $s_3 \oplus s_2$ cannot.

Similarly, one can prove that $s_1 \oplus s_2 \stackrel{\approx_p}{\sim} s_6 \oplus s_8$ because $R_2 = \{(s_1, s_6), (s_2, s_8), (s_1, s_7), (s_2, s_9)\}$ is a branching place bisimulation. $\square$

# 5 Branching Place Bisimilarity is Decidable

In order to prove that $\approx_p$ is decidable, we first need a technical lemma which states that it is decidable to check if a place relation $R \subseteq S \times S$ is a branching place bisimulation.

**Lemma 2.** 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 branching place bisimulation.

*Proof.* We want to prove that $R$ is a branching place bisimulation if and only if the following two conditions are satisfied:

1. $\forall t_1 \in T, \forall m \text{ such that } (\bullet t_1, m) \in R^{\oplus}$

(a) either $t_1$ is $\tau$-sequential and there exists an acyclic $\tau$-sequential $\sigma$ such that $m = \bullet\sigma$, $(\bullet t_1, \sigma\bullet) \in R$ and $(t_1^\bullet, \sigma^\bullet) \in R$;

(b) or there exist an acyclic $\tau$-sequential $\sigma$ and $t_2 \in T$, with $\sigma^\bullet = \bullet t_2$, such that $m = \bullet\sigma$, $l(t_1) = l(t_2)$, $(\bullet t_1, \bullet t_2) \in R^{\oplus}$ and $(t_1^\bullet, t_2^\bullet) \in R^{\oplus}$.

2. $\forall t_2 \in T, \forall m \text{ such that } (m, \bullet t_2) \in R^{\oplus}$

(a) either $t_2$ is $\tau$-sequential and there exists an acyclic $\tau$-sequential $\sigma$ such that $m = \bullet\sigma$, $(\sigma^\bullet, \bullet t_2) \in R$ and $(\sigma^\bullet, t_2^\bullet) \in R$;

(b) or there exist an acyclic $\tau$-sequential $\sigma$ and $t_1 \in T$, with $\sigma^\bullet = \bullet t_1$, such that $m = \bullet\sigma$, $l(t_1) = l(t_2)$, $(\bullet t_1, \bullet t_2) \in R^{\oplus}$ and $(t_1^\bullet, t_2^\bullet) \in R^{\oplus}$.

The implication from left to right is obvious: if $R$ is a branching place bisimulation, then for sure conditions 1 and 2 are satisfied, because, as observed in Remark 1, if there exists a suitable $\tau$-sequential transition sequence $\sigma$, then there exists also a suitable
acyclic τ-sequential $\sigma'$ such that $\bullet\sigma = \bullet\sigma'$ and $\sigma' = \sigma'^{\bullet}$. For the converse implication, assume that conditions 1 and 2 are satisfied; then we have to prove that the branching place bisimulation game for $R$ holds for all pairs $(m_1, m_2) \in R^{\oplus}$.

Let $q = \{(s_1, s'_1), (s_2, s'_2), \dots, (s_k, s'_k)\}$ be any multiset of associations that can be used to prove that $(m_1, m_2) \in R^{\oplus}$. So this means that $m_1 = s_1 \oplus s_2 \oplus \dots \oplus s_k$, $m_2 = s'_1 \oplus s'_2 \oplus \dots \oplus s'_k$ and that $(s_i, s'_i) \in R$ for $i=1, \dots, k$. If $m_1[t_1]m'_1$, then $m'_1 = m_1 \ominus \bullet t_1 \oplus t_1^{\bullet}$. Consider the multiset of associations $p = \{(\bar{s}_1, \bar{s}'_1), \dots, (\bar{s}_h, \bar{s}'_h)\} \subseteq q$, with $\bar{s}_1 \oplus \dots \oplus \bar{s}_h = \bullet t_1$. Note that $(\bullet t_1, \bar{s}'_1 \oplus \dots \oplus \bar{s}'_h) \in R^{\oplus}$. Therefore, by condition 1,

(a) either $t_1$ is $\tau$-sequential and there exists an acyclic $\tau$-sequential $\sigma$ such that $m = \bullet\sigma$, $(\bullet t_1, \sigma^\bullet) \in R$ and $(t_1^\bullet, \sigma^\bullet) \in R$;

(b) or there exist an acyclic $\tau$-sequential $\sigma$ and $t_2 \in T$, with $\sigma^\bullet = \bullet t_2$, such that $m = \bullet\sigma$, $l(t_1) = l(t_2)$, $(\bullet t_1, \bullet t_2) \in R^{\oplus}$ and $(t_1^\bullet, t_2^\bullet) \in R^{\oplus}$.

In case (a), since $\bullet\sigma \subseteq m_2$, also $m_2[\sigma]m_2^\bullet$ is firable, where $m_2^\bullet = m_2 \ominus \bullet\sigma \oplus \sigma^\bullet$, so that $(\bullet t_1, \sigma^\bullet) \in R$, $(t_1^\bullet, \sigma^\bullet) \in R$ and, finally, $(m_1 \ominus \bullet t_1, m_2 \ominus \bullet \sigma) \in R^{\oplus}$, as required. Note that the last condition holds because, from the multiset $q$ of matching pairs for $m_1$ and $m_2$, we have removed those in $p$. In case (b), since $\bullet\sigma \subseteq m_2$, also $m_2[\sigma]m[t_2]m_2^\bullet$ is firable, where $m_2^\bullet = m_2 \ominus \bullet\sigma \oplus t_2^\bullet$, so that $l(t_1) = l(t_2)$, $(\bullet t_1, \bullet t_2) \in R^{\oplus}$, $(t_1^\bullet, t_2^\bullet) \in R^{\oplus}$ and, finally, $(m_1 \ominus \bullet t_1, m_2 \ominus \bullet \sigma) \in R^{\oplus}$, as required.

If $m_2[t_2]m_2^\bullet$, then we have to use an argument symmetric to the above, where condition 2 is used instead. Hence, we have proved that conditions 1 and 2 are enough to prove that $R$ is a branching place bisimulation.

Finally, observe that the set $T$ is finite and, for each $t_1 \in T$, the number of markings $m$ such that $(\bullet t_1, m) \in R^{\oplus}$ and $(m, \bullet t_1) \in R^{\oplus}$ is finite as well. More precisely, this part of the procedure takes $O(q \cdot \frac{(n+p-1)!}{(n-1)! \cdot p!} \cdot (p^2\sqrt{p}))$ time where $q = |T|$, $n = |S|$ and $p$ is the least number such that $|\bullet t| \le p$ for all $t \in T$, because the distribution of $p$ tokens over $n$ places is given by the binomial coefficient $\binom{n+p-1}{p} = \frac{(n+p-1)!}{(n-1)! \cdot p!}$ and checking if such a marking of size $p$ is related to $\bullet t_1$ takes $O(p^2\sqrt{p})$ time.

Moreover, for each pair $(t_1, m)$ satisfying the condition $(\bullet t_1, m) \in R^{\oplus}$, we have to check conditions (a) and (b), each checkable in a finite amount of time. In fact, for case (a), we have to check if there exists a place $s$ such that $(\bullet t_1, s) \in R$ and $(t_1^\bullet, s) \in R$, which is reachable from $m$ by means of an acyclic $\tau$-1-sequential transition sequence $\sigma$; this condition is decidable because we have at most $n$ places to examine and for each candidate place $s$, we can check whether a suitable acyclic $\tau$-1-sequential $\sigma$ exists. Similarly, in case (b) we have to consider all the transitions $t_2$ such that $(\bullet t_1, \bullet t_2) \in R^{\oplus}$ and $(t_1^\bullet, t_2^\bullet) \in R^{\oplus}$ and check if at least one of these is reachable from $m$ by means of an acyclic $\tau$-sequential transition sequence $\sigma$ such that $\bullet\sigma = m$ and $\sigma^\bullet = \bullet t_2$ and the existence of such a $\sigma$ is decidable. Therefore, in a finite amount of time we can decide if a given place relation $R$ is actually a branching place bisimulation. $\square$

**Theorem 2. (Branching 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 \approx_p m_2$.

*Proof.* If $|m_1| \neq |m_2|$, then $m_1 \not\approx_p m_2$ by Proposition 1. Otherwise, let $|m_1| = k = |m_2|$. As $|S| = n$, the set of all the place relations over $S$ is of size $2^n$. Let us list such relations
<figure><img src="image_9.png" /><figcaption>**Fig. 4.** Two non-place bisimilar nets</figcaption></figure>

as: $R_1, R_2, \dots, R_{2^n}$. Hence, for $i = 1, \dots, 2^n$, by Lemma 2 we can decide whether $R_i$ is a branching place bisimulation and, in such a case, we can check whether $(m_1, m_2) \in R_i^{\oplus}$ in $O(k^2\sqrt{k})$ time. As soon as we found a branching place bisimulation $R_i$ such that $(m_1, m_2) \in R_i^{\oplus}$, we stop concluding that $m_1 \approx_p m_2$. If none of the $R_i$ is a branching place bisimulation such that $(m_1, m_2) \in R_i^{\oplus}$, then we can conclude that $m_1 \not\approx_p m_2$. $\square$

# 6 Conclusion and Future Research

Place bisimilarity [1] is the only decidable [13] behavioral equivalence for P/T nets which respects the expected causal behavior, as it is slightly finer than structure preserving bisimilarity [7], in turn slightly finer than fully-concurrent bisimilarity [3]. Thus, it is the only equivalence for which it is possible (at least, in principle) to verify algorithmically the (causality-preserving) correctness of an implementation by exhibiting a place bisimulation between its specification and implementation.

It is sometimes argued that place bisimilarity is too discriminating. In particular, [1] and [7] 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 4, discussed in [1]. Clearly, markings $s_1$ and $s_4$ are equivalent, also according to all the behavioral equivalences discussed in [7], 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.

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

Moreover, if we consider the duality between the process algebra FNM (a dialect of CCS, extended with multi-party interaction) and P/T nets, proposed in [9], we may find further arguments supporting this more restrictive interpretation of net behavior. In fact, an *unmarked* P/T net $\mathcal{N}$ can be described by an FNM system of equations, where each equation defines a constant $C_i$ (whose body is a sequential process term $t_i$), representing place $s_i$. Going back to the nets in Figure 4, according to this duality, the constant $C_1$ for place $s_1$ is not equivalent (in any reasonable sense) to the constant $C_4$ for place $s_4$ because these two constants describe all the potential behaviors of these two places, which are clearly different! Then, the marked net $\mathcal{N}(m_0)$ is described by a parallel term composed of as many instances of $C_i$ as the tokens that are present in $s_i$ for $m_0$, encapsulated by a suitably defined restriction operator $(vL)^{-}$. Continuing the example, it turns out that $(vL)C_1$ is equivalent to $(vL)C_4$ because the markings $s_1$ and $s_4$ are equivalent, but $(vL)(C_1|C_1)$ is not equivalent to $(vL)(C_4|C_4)$ because the markings $2 \cdot s_1$ is not equivalent to the marking $2 \cdot s_4$, as discussed above.

Furthermore, on the subclass of BPP nets (i.e., nets whose transitions have singleton pre-set), place bisimilarity specializes to *team bisimilarity* [10], which is unquestionably the most appropriate behavioral equivalence for BPP nets, as it coincides with *structure-preserving bisimilarity* [7], hence matching all the relevant criteria expressed in [7] for a sensible behavioral equivalence.

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

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 finite set of places. (And a simple case study is described in [13].)

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 $\mathcal{R}$ relates those places which are considered equivalent under all the possible $\mathcal{R}$-related contexts. Hence, if $\mathcal{R}$ justifies that $m_1 \sim_p m_2$ as $(m_1, m_2) \in \mathcal{R}^{\oplus}$, then for sure the same $\mathcal{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 \mathcal{R}^{\oplus}$.

3. Finally, while place bisimilarity is decidable [13], fully-concurrent bisimilarity is undecidable on finite P/T nets [5].
<figure><img src="image_10.png" /><figcaption>**Fig. 5.** Two branching fully-concurrent P/T nets</figcaption></figure>

The newly defined *branching place bisimilarity* is the only extension of the place bisimilarity idea to P/T nets with silent moves that has been proved decidable, even if the time complexity of the decision procedure we have proposed is exponential in the size of the net.

Of course, this behavioral relation may be subject to the same criticisms raised to place bisimilarity and also its restrictive assumption that only τ-sequential transitions can be abstracted away can be criticized, as its applicability to real case studies may appear rather limited. In the following, we try to defend our point of view.

First, on the subclass of BPP nets, branching place bisimilarity coincides with *branching team bisimilarity* [12], a very satisfactory equivalence which is actually coin-
ductive and, for this reason, also very efficiently decidable in polynomial time. More-
over, on the subclass of *finite-state machines* (i.e., nets whose transitions have singleton
pre-set and singleton, or empty, post-set), branching team bisimilarity has been axiom-
atized [11] on the process algebra CFM [9], which can represent all (and only) the
finite-state machines, up to net isomorphism.

Second, we conjecture that branching place bisimilarity does respect the causal be-
havior of P/T nets. In particular, we conjecture that *branching fully-concurrent bisimi-
larity* [22, 12] (which is undecidable) is strictly coarser than $\approx_p$, because it may equate
nets whose silent transitions are not $\tau$-sequential (and also may relate markings of dif-
ferent size). For instance, consider the net in Figure 5. Of course, the markings $s_1 \oplus s_3$
and $s_5 \oplus s_6$ are branching fully-concurrent bisimilar: to the move $s_1 \oplus s_3[t_1]s_2 \oplus s_3$,
where $t_1 = (s_1, \tau, s_2)$, $s_5 \oplus s_6$ can reply with $s_5 \oplus s_6[t_2]s_7 \oplus s_8$, where $t_2 = (s_5 \oplus s_6, \tau, s_7 \oplus
s_8)$ and the reached markings are clearly equivalent. However, $s_1 \oplus s_3 \not\cong_p s_5 \oplus s_6$ because
$s_1 \oplus s_3$ cannot reply to the move $s_5 \oplus s_6[t_2]s_7 \oplus s_8$, as $t_2$ is not $\tau$-sequential (i.e., it can
be seen as the result of a synchronization), while $t_1$ is $\tau$-sequential.

We already argued in the introduction that it is very much questionable whether a
synchronization can be considered as unobservable, even if this idea is rooted in the
theory of concurrency from the very beginning. As a matter of fact, in CCS [17] and
in the $\pi$-calculus [18, 24], the result of a synchronization is a silent, $\tau$-labeled (hence
unobservable) transition. However, the silent label $\tau$ is used in these process algebras for two different purposes:

* First, to ensure that a synchronization is strictly binary: since the label $\tau$ cannot be used for synchronization, by labeling a synchronization transition by $\tau$ any further synchronization of the two partners with other parallel components is prevented (i.e., multi-party synchronization is disabled).

* Second, to describe that the visible effect of the transition is null: a $\tau$-labeled transition can be considered unobservable and can be abstracted away, to some extent.

Nonetheless, it is possible to modify slightly these process algebras by introducing two different actions for these different purposes. In fact, the result of a binary synchronization can be some *observable* label, say $\lambda$ (or even $\lambda(a)$, if the name of the channel $a$ is considered as visible), for which no co-label exists, so that further synchronization is impossible. While the action $\tau$, that can be used as a prefix, is used to denote some local, internal (hence unobservable) computation. In this way, a net semantics for these process algebras (in the style of, e.g., [9]) would generate $\tau$-sequential P/T nets, that are amenable to be compared by means of branching place bisimilarity.

As a final comment, we want to discuss an apparently insurmountable limitation of our approach. In fact, the extension of the place bisimulation idea to nets with silent transitions that are not $\tau$-sequential seems very hard, or even impossible. Consider again the two P/T nets in Figure 5. If we want that $s_1 \oplus s_3$ be related to $s_5 \oplus s_6$, we need to include the pairs $(s_1, s_5)$ and $(s_3, s_6)$. If the marking $s_5 \oplus s_6$ silently reaches $s_7 \oplus s_8$, then $s_1 \oplus s_3$ can respond by idling (and in such a case we have to include the pairs $(s_1, s_7)$ and $(s_3, s_8)$) or by performing the transition $s_1 \xrightarrow{\tau} s_2$ (and in such a case we have to include the pairs $(s_2, s_7)$ and $(s_3, s_8)$). In any case, the candidate place relation $R$ should be of the form $\{(s_1, s_5), (s_3, s_6), (s_3, s_8), \dots\}$. However, this place relation cannot be a place bisimulation of any sort because, on the one hand, $(s_1 \oplus s_3, s_5 \oplus s_8) \in R^{\oplus}$ but, on the other hand, $s_1 \oplus s_3$ can eventually perform $a$, while $s_5 \oplus s_8$ is stuck.

Nonetheless, this negative observation is coherent with our intuitive interpretation of (branching) place bisimilarity as a way to give semantics to *unmarked* nets. In the light of the duality between P/T nets and the FNM process algebra discussed above [9], a place is interpreted as a sequential process type (and each token in this place as an instance of a sequential process of that type, subject to some restriction); hence, a (branching) place bisimulation essentially states which kinds of sequential processes (composing the distributed system represented by the Petri net) are to be considered equivalent. In our example above, it makes no sense to consider place $s_1$ and place $s_5$ as equivalent, because the corresponding FNM constants $C_1$ and $C_5$ have completely different behavior: $C_5$ can interact (with $C_6$), while $C_1$ can only perform some internal, local transition.

Future work will be devoted to find more efficient algorithms for checking branching place bisimilarity. One idea could be to build directly the set of maximal branching place bisimulations, rather than to scan all the place relations to check whether they are branching place bisimulations, as we did in the proof of Theorem 2.

**Acknowledgements:** The anonymous referees are thanked for their useful comments and suggestions.
References

1. C. Autant, Z. Belmesk, Ph. Schnoebelen, Strong bisimilarity on nets revisited, in Procs. PARLE'91, vol. II: Parallel Languages, LNCS 506, 295-312, Springer, 1991.

2. T. Basten, Branching bisimilarity is an equivalence indeed!, *Information Processing Letters* 58(3): 141-147, 1996.

3. E. Best, R. Devillers, A. Kiehn, L. Pomello, Concurrent bisimulations in Petri nets, *Acta Inf.* 28(3): 231-264, 1991.

4. J. Desel, W. Reisig, Place/Transition Petri nets, in *Lectures on Petri Nets I: Basic Models*, LNCS 1491, 122-173, Springer, 1998.

5. J. Esparza, Decidability and complexity of Petri net problems: An introduction, *Lectures on Petri Nets I: Basic Models*, LNCS 1491, 374-428, Springer, 1998.

6. R.J. van Glabbeek, W.P. Weijland, Branching time and abstraction in bisimulation semantics, *Journal of the ACM* 43(3):555-600, 1996.

7. 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.

8. R. Gorrieri, C. Versari, *Introduction to Concurrency Theory: Transition Systems and CCS*, EATCS Texts in Theoretical Computer Science, Springer-Verlag (2015)

9. R. Gorrieri, *Process Algebras for Petri Nets: The Alphabetization of Distributed Systems*, EATCS Monographs in Computer Science, Springer, 2017.

10. R. Gorrieri, Team bisimilarity, and its associated modal logic, for BPP nets, *Acta Informatica*, 2020. DOI: 10.1007/s00236-020-00377-4

11. R. Gorrieri, Team equivalences for finite-state machines with silent moves, *Information and Computation* 275:104603, 2020. DOI:10.1016/j.ic.2020.104603

12. R. Gorrieri, Causal semantics for BPP nets with silent moves, submitted, 2020.

13. R. Gorrieri, Place bisimilarity is decidable, indeed!, arXiv:2104.01392, april 2021.

14. 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.

15. P. Jančar, Undecidability of bisimilarity for Petri nets and some related problems, *Theoretical Computer Science* 148(2):281-301, 1995.

16. R. Keller, Formal verification of parallel programs, *Comm. of the ACM* 19(7):561-572, 1976.

17. R. Milner, *Communication and Concurrency*, Prentice-Hall, 1989.

18. R. Milner, J. Parrow, D. Walker, A calculus of mobile processes, *Information and Computation* 100(1), 1-77, 1992.

19. E.R. Olderog, *Nets, Terms and Formulas*, Cambridge Tracts in Theoretical Computer Science 23, Cambridge University Press, 1991.

20. 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.

21. J.L. Peterson, *Petri Net Theory and the Modeling of Systems*, Prentice-Hall, 1981.

22. S. Pinchinat. *Des bisimulations pour la sémantique des systèmes réactifs*, Génie logiciel [cs.SE], Ph.D. thesis, Institut National Polytechnique de Grenoble - INPG, 1993.

23. W. Reisig, *Petri Nets: An Introduction*, EATCS Monographs in Theoretical Computer Science, Springer-Verlag, 1985.

24. D. Sangiorgi, D. Walker, *The π-calculus: A Theory of Mobile Processes*, Cambridge University Press, 2001.