# Compositional Semantics of Finite Petri Nets

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

Structure-preserving bisimilarity [11] is a truly concurrent behavioral
equivalence for finite Petri nets, which relates markings (of the same size
only) generating the same causal nets, hence also the same partial orders of
events. The process algebra FNM [14] truly represents all (and only) the
finite Petri nets, up to isomorphism. We prove that structure-preserving
bisimilarity is a congruence w.r.t. the FMN operators, In this way, we have
defined a compositional semantics, fully respecting causality and the
branching structure of systems, for the class of all the finite Petri nets.
Moreover, we study some algebraic properties of structure-preserving
bisimilarity, that are at the base of a sound (but incomplete) axiomatization
over FNM process terms.

##  1 Introduction

Structure-preserving bisimilarity [11] (sp-bisimilarity, for short) is a truly
concurrent, bisimulation-based, behavioral equivalence for finite P/T Petri
nets [27, 7], such that if two markings are related, then they generate the
same causal nets [10, 2, 24, 11], hence ensuring that they have the same size
and generate the same partial orders of events. As discussed in [11], sp-
bisimilarity $\sim_{sp}$ is the coarsest behavioral equivalence that respects
the following three aspects: $(i)$ the branching structure (being based on the
concept of bisimulation), $(ii)$ causality (being slightly finer than fully-
concurrent bisimilarity [3]) and $(iii)$ inevitability [22], meaning that if
two systems are equivalent, and in one the occurrence of a certain action is
inevitable, then so is it in the other one. Moreover, $\sim_{sp}$ is decidable
on bounded finite Petri nets [4], while its decidability for unbounded nets is
an open problem.

Finite P/T Petri nets can be represented, up to isomorphism, by means of the
process algebra FNM [14], which is a CCS-like sub-calculus extended with an
additional operator, called strong prefixing. This operator allows for atomic
execution of action sequences, so that a multi-party interaction can be
modeled as an atomic execution of a sequence of binary interactions.

The main aim of this paper is to show that sp-bisimilarity is a congruence for
the operators of FNM, thus yielding a compositional semantics, up to sp-
bisimilarity, for the class of all the finite P/T Petri nets. Moreover, we
study some algebraic properties of sp-bisimilarity and, based on these, we
introduce a sound (but incomplete) axiomatization over FNM process terms.

The paper is organized as follows. Section 2 introduces the basic definitions
about Petri nets, some novel definitions (notably, the distinction between
dynamically vs statically reachable subnet) and the definition of structure-
preserving bisimilarity. Section 3 recalls from [14] the process algebra FNM,
its (operational) semantics in terms of finite P/T Petri nets, and also the
representability theorem stating that each finite (statically reachable)
marked Petri net can be represented by a suitable FNM term, up to isomorphism.
Section 4 shows that sp-bisimilarity is a congruence for the FNM operators.
Section 5 presents a set of algebraic properties of sp-bisimilarity, some of
which are conditional, and hints that these do not cover all the possible
equalities that can be singled out. Based on this set of algebraic properties,
Section 6 shows a sound, but incomplete, axiomatization of sp-bisimilarity
over FNM process terms. Finally, Section 7 is devoted to some conclusions.

##  2 Basic Definitions

###### Definition 1

(Multiset) Let ${\mathbb{N}}$ be the set of natural numbers. Given a countable
set $S$, a finite multiset over $S$ is a function $m:S\rightarrow{\mathbb{N}}$
such that the support set $dom(m)=\\{s\in S\;\;\big{|}\;\;m(s)\neq 0\\}$ is
finite. The set of all finite multisets over $S$, denoted by
${\mathcal{M}}_{fin}(S)$, is ranged over by $m$, possibly indexed. (The set of
all finite subsets of $S$ is denoted by $\mathcal{P}_{fin}(S)$.) 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$. We also
write $m\subset m^{\prime}$ if $m\subseteq m^{\prime}$ and
$m(s)<m^{\prime}(s)$ for some $s\in S$.

Multiset union $\\_\oplus\\_$ is defined as: $(m\oplus m^{\prime})(s)$
$=m(s)+m^{\prime}(s)$. This operation is commutative, associative and has
$\theta$ as neutral element. Multiset difference $\\_\ominus\\_$ is defined
as: $(m_{1}\ominus m_{2})(s)=max\\{m_{1}(s)-m_{2}(s),0\\}$. The scalar product
of a natural $j$ with $m$ is the multiset $j\cdot m$ defined as $(j\cdot
m)(s)=j\cdot(m(s))$. By $s_{i}$ we 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/Transition Petri net (P/T net, or
Petri net, for short) is a tuple $N=(S,A,T)$, where

  * $\bullet$

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

  * $\bullet$

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

  * $\bullet$

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

A Petri net $N=(S,A,T)$ is finite when $S$ and $T$ are finite sets. Given a
transition $t=(m,a,m^{\prime})$, we use the notation ${}^{\bullet}t$ to denote
its pre-set $m$ (which cannot be an empty multiset) of tokens to be consumed;
$\ell(t)$ for its label $a$, and $t^{\bullet}$ to denote its post-set
$m^{\prime}$ of tokens to be produced. Hence, transition $t$ can be also
represented as
${}^{\bullet}t$${\>\stackrel{{\scriptstyle\ell(t)}}{{\longrightarrow}}\>}$$t^{\bullet}$.
$\Box$

In the graphical description of P/T nets, places (represented as circles) and
transitions (represented as boxes) are connected by directed arcs. The arcs
may be labeled with the number representing how many tokens are to be removed
from (or produced into) that place; no label on the arc is interpreted as the
number one, i.e., one token flowing on the arc. This numerical label of the
arc is called its weight.

###### Definition 3

(Marking, P/T net system) Given a P/T net $N=(S,A,T)$, a finite 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$

###### Definition 4

(Enabling, firing sequence, reachable marking) 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$, denoted by $[m\rangle$, is
$[m\rangle=\\{m^{\prime}\;\;\big{|}\;\;\exists\sigma.m[\sigma\rangle
m^{\prime}\\}$.  $\Box$

The reachable markings of a finite net can be countably infinitely many when
the net is not bounded, i.e., when the number of tokens in some places can
grow unboundedly.

###### Definition 5

(Classes of finite P/T Nets) A finite marked P/T net $N=(S,A,T,m_{0})$ is:

  * $\bullet$

safe if each place contains at most one token in each reachable marking, i.e.,
$\forall m\in[m_{0}\rangle,\forall s\in S,$ $m(s)\leq 1$.

  * $\bullet$

bounded if the number of tokens in each place is bounded by some $k$ for each
reachable marking, i.e., $\exists k\in{\mathbb{N}}$ such that $\forall
m\in[m_{0}\rangle,\forall s\in S$ we have that $m(s)\leq k$. If this is the
case, we say that the net is $k$-bounded (hence, a safe net is just a
1-bounded net).

A finite P/T net $N=(S,A,T)$ is a BPP net if $\forall t\in T$ we have
$|\mbox{${}^{\bullet}t$}|=1$.  $\Box$

We now recall a basic behavioral equivalence on P/T nets, derived from
standard bisimilarity on labeled transition systems [21, 13].

###### Definition 6

(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 [18] for finite 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 [8] 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 [18] applies to all these non-interleaving
bisimulation equivalences as well.

Given a P/T net $N=(S,A,T)$ and a marking $m$, we say that two transitions
$t_{1},t_{2}$ 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 [23].

###### Definition 7

(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}$. $m_{1}[G_{1}\rangle m^{\prime}_{1}$, $\exists G_{2}$ such
that $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}$. $m_{2}[G_{2}\rangle m^{\prime}_{2}$, $\exists G_{1}$ such
that $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
[8].

###  2.1 Dynamically Reachable and Statically Reachable Subnets

Now we introduce two different notions of reachable subnet, following [14]:

  * $\bullet$

dynamically reachable subnet, which refers to the set of places and
transitions dynamically reachable from the initial marking $m_{0}$ by the
token game (as described in Definition 4), and

  * $\bullet$

statically reachable subnet, which refers to the places and transitions which
are reachable by a weaker token game, stating that a transition $t$ is
statically enabled at $S^{\prime}$ (i.e., the current set of the statically
reached places (initiallly $dom(m_{0})$)), when $dom(\mbox{${}^{\bullet}t$})$
is a subset of $S^{\prime}$.

Based on the latter, we introduce the notion of statically reduced net, i.e.,
a net where all of its places and transitions are statically reachable from
$dom(m_{0})$. This notion is important in Section 3, because we will show that
the net semantics $Net(p)$ of an FNM term $p$ is a finite, statically reduced
P/T net.

$a)\qquad\qquad$$a.\mbox{\bf 0}+\overline{a}.\mbox{\bf
0}$$a\;$$\;\overline{a}$$b)\;\;$$a.\mbox{\bf 0}+\overline{a}.\mbox{\bf
0}$$a\;$$\;\overline{a}$$\;\tau$2 Figure 1: The dynamically reachable subnet
(a) and the statically reachable subnet (b) for $a.\mbox{\bf
0}+\overline{a}.\mbox{\bf 0}$

In fact, the semantics of a term $p$ is not simply the net that can be
dynamically reached from the initial marking $\mbox{$dec$}(p)$ corresponding
to $p$, rather it is the net describing all the potential behaviors of $p$, as
if the number of tokens in $\mbox{$dec$}(p)$ can be increased at will. For
instance, consider the FNM sequential process $p=a.\mbox{\bf
0}+\overline{a}.\mbox{\bf 0}$; its dynamically reachable subnet, outlined in
Figure 1(a), shows the expected behavior that $p$ can perform either $a$ or
its complementary action $\overline{a}$. On the contrary, its statically
reachable subnet in (b) describes additionally the potential self-
synchronization of $p$ with another copy of itself; in this way, the net
semantics for $p$ and for the parallel term $p\mbox{$\,|\,$}p$ differ only for
the form of the initial marking (one token for $p$ and two tokens for
$p\mbox{$\,|\,$}p$), but the underlying net is the same. The statically
reachable subnet of a finite P/T net is always algorithmically computable,
also for Nonpermissive nets [14], even though they are a Turing-complete model
of computation, and so for them, as the reachability problem is undecidable,
it is not always possible to compute the dynamically reachable subnet.

Now we provide the formal definitions for these two different forms of
reachable subnet.

###### Definition 8

(Dynamically reachable subnet, dynamically reduced net) Given a P/T Petri net
system $N(m_{0})=$ $(S,A,T,m_{0})$, the dynamically reachable subnet
$Net_{d}(N(m_{0}))$ is $(S^{\prime},A^{\prime},T^{\prime},m_{0})$, where

$\begin{array}[]{rcl}S^{\prime}&=&\\{s\in S\;\;\big{|}\;\;\exists
m\in[m_{0}\rangle\mbox{ such that }m(s)\geq 1\\},\\\ T^{\prime}&=&\\{t\in
T\;\;\big{|}\;\;\exists m\in[m_{0}\rangle\mbox{ such that }m[t\rangle\\},\\\
A^{\prime}&=&\\{a\;\;\big{|}\;\;\exists t\in T^{\prime}\mbox{ such that
}\ell(t)=a\\}.\end{array}$

A P/T net system $N(m_{0})=(S,A,T,m_{0})$ is dynamically reduced if
$N(m_{0})=Net_{d}(N(m_{0}))$, i.e., the net system is equal to its dynamically
reachable subnet.  $\Box$

The dynamically reachable subnet of the net in Figure 2(a) is outlined in
Figure 2(b). Given a finite net $N(m_{0})$, it is algorithmically derivable
$Net_{d}(N(m_{0}))$ by means of its coverability tree [19], but its complexity
is exponential in the size of the net.

$s_{1}$$s_{2}$$s_{3}$$a\;$$\;b$$\;c$$\;d$$s_{4}$$s_{5}$$a)\quad\qquad$2$s_{1}$$s_{2}$$a\;$$\;b$$s_{4}$$b)\;\;$
Figure 2: A net system in (a) and its dynamically reachable subnet in (b)

###### Definition 9

(Statically reachable subnet and statically reduced net) Given a P/T net
$N=(S,A,T)$, we say that a transition $t$ is statically enabled by a set of
places $S^{\prime}\subseteq S$, denoted by $S^{\prime}\llbracket t\rangle$, if
$dom(\mbox{${}^{\bullet}t$})\subseteq S^{\prime}$.

Given two sets of places $S_{1},S_{2}\subseteq S$, we say that $S_{2}$ is
statically reachable in one step from $S_{1}$ if there exists a transition
$t\in T$, such that $S_{1}\llbracket t\rangle$,
$dom(\mbox{$t^{\bullet}$})\not\subseteq S_{1}$ and $S_{2}=S_{1}\cup
dom(\mbox{$t^{\bullet}$})$; this is denoted by
$S_{1}{\mbox{${\>\stackrel{{\scriptstyle t}}{{\Longrightarrow}}\>}$}}S_{2}$.
The static reachability relation
${\mbox{${\>\stackrel{{\scriptstyle}}{{\Longrightarrow}}\\!\\!\\!\phantom{}^{*}\>}$}}\subseteq\mathcal{P}_{fin}(S)\times\mathcal{P}_{fin}(S)$
is the least relation such that

  * $\bullet$

$S_{1}{\mbox{${\>\stackrel{{\scriptstyle}}{{\Longrightarrow}}\\!\\!\\!\phantom{}^{*}\>}$}}S_{1}$
and

  * $\bullet$

if
$S_{1}{\mbox{${\>\stackrel{{\scriptstyle}}{{\Longrightarrow}}\\!\\!\\!\phantom{}^{*}\>}$}}S_{2}$
and $S_{2}{\mbox{${\>\stackrel{{\scriptstyle
t}}{{\Longrightarrow}}\>}$}}S_{3}$, then
$S_{1}{\mbox{${\>\stackrel{{\scriptstyle}}{{\Longrightarrow}}\\!\\!\\!\phantom{}^{*}\>}$}}S_{3}$.

A set of places $S_{k}\subseteq S$ is the largest set statically reachable
from $S_{1}$ if
$S_{1}{\mbox{${\>\stackrel{{\scriptstyle}}{{\Longrightarrow}}\\!\\!\\!\phantom{}^{*}\>}$}}S_{k}$
and for all $t\in T$ such that $S_{k}\llbracket t\rangle$, we have that
$dom(\mbox{$t^{\bullet}$})\subseteq S_{k}$. Given a P/T net system
$N(m_{0})=(S,A,T,m_{0})$, we denote by $\llbracket dom(m_{0})\rangle$ the
largest set of places statically reachable from $dom(m_{0})$, i.e., the
largest $S_{k}$ such that
$dom(m_{0}){\mbox{${\>\stackrel{{\scriptstyle}}{{\Longrightarrow}}\\!\\!\\!\phantom{}^{*}\>}$}}S_{k}$.

The statically reachable subnet $Net_{s}(N(m_{0}))$ is the net
$(S^{\prime},A^{\prime},T^{\prime},m_{0})$, where

$\begin{array}[]{rcl}S^{\prime}&=&\llbracket dom(m_{0})\rangle,\\\
T^{\prime}&=&\\{t\in T\;\;\big{|}\;\;S^{\prime}\llbracket t\rangle\\},\\\
A^{\prime}&=&\\{a\;\;\big{|}\;\;\exists t\in T^{\prime}\mbox{ such that
}\ell(t)=a\\}.\end{array}$

A P/T net system $N(m_{0})=(S,A,T,m_{0})$ is statically reduced if
$Net_{s}(N(m_{0}))$ $=N(m_{0})$, i.e., the net system is equal to its
statically reachable subnet.  $\Box$

The statically reachable subnet $Net_{s}(N(m_{0}))$ of a finite Petri net
$N(m_{0})$ can be computed with an easy polynomial algorithm [14]. We will
show in Section 3 that, given an FNM process $p$, its net semantics is the
statically reachable subnet from its initial marking $\mbox{$dec$}(p)$,
extracted from the infinite net describing the semantics of the whole FNM
process algebra.

Finally, we outline some useful properties relating statically reduced nets
and dynamically reduced ones.

###### Proposition 1

Given a P/T net system $N(m_{0})=(S,A,T,m_{0})$, if $N(m_{0})$ is dynamically
reduced, then it is also statically reduced.  $\Box$

However, the converse implication is not true: there are statically reduced
P/T systems that are not dynamically reduced. E.g., the statically reduced P/T
system $N(s_{1})=$ $(\\{s_{1},s_{2},s_{3}\\},$
$\\{a,b\\},\\{(s_{1},a,s_{2}),(2\cdot s_{1},b,s_{3})\\},s_{1})$ cannot
dynamically reach place $s_{3}$. Consider the net system in Figure 2(a); its
statically reachable subnet is outlined in Figure 3. If we compare it with its
dynamically reachable subnet in Figure 2(b), we note that the statically
reachable subnet contains the dynamically reachable subnet. This holds in
general.

$s_{1}$$s_{2}$$a\;$$\;b$$\;c$$s_{4}$$s_{5}$2 Figure 3: The statically
reachable subnet of Figure 2(a)

###### Proposition 2

Given a P/T system $N(m_{0})=(S,A,T,m_{0})$, if its dynamically reachable
subnet $Net_{d}(N(m_{0}))$ is $(S^{\prime},A^{\prime},T^{\prime},m_{0})$ and
its statically reachable subnet $Net_{s}(N(m_{0}))$ is
$(S^{\prime\prime},A^{\prime\prime},T^{\prime\prime},m_{0})$, then
$S^{\prime}\subseteq S^{\prime\prime}$, $T^{\prime}\subseteq T^{\prime\prime}$
and $A^{\prime}\subseteq A^{\prime\prime}$.  $\Box$

For some classes of nets, however, the two notions coincide, in particular for
BPP nets, i.e., those nets whose transitions have singleton preset.

###  2.2 Structure Preserving Bisimilarity

We recall from [11] the definition of this behavioral equivalence, adapting
some auxiliary notations to our aims.

###### Definition 10

(Linking) Let $N=(S,A,T)$ be a P/T net. A link is a pair $(s_{1},s_{2})\in
S\times S$. A linking $l$ is a finite multiset of links, i.e., $l:S\times
S\rightarrow{\mathbb{N}}$ where $dom(l)$ is finite. With abuse of notation, we
denote by $\theta$ the empty linking, i.e., the empty multiset of links. Given
a set $L$ of links, we denote by $L^{+}$ the set of all the linkings over $L$,
i.e., of all the multisets over $L$.

Given a linking $l$, the two projected markings $m_{1}$ and $m_{2}$ can be
defined as $m_{1}(s_{1})=\pi_{1}(l)(s_{1})=\sum_{s_{2}\in S}l(s_{1},s_{2})$
and $m_{2}(s_{2})=\pi_{2}(l)(s_{2})=\sum_{s_{1}\in S}l(s_{1},s_{2})$. For
instance, if $l=\\{(s_{1},s_{2}),(s_{1}^{\prime},s_{2}^{\prime})\\}$, then
$\pi_{1}(l)=s_{1}\oplus s_{1}^{\prime}$ and $\pi_{2}(l)=s_{2}\oplus
s_{2}^{\prime}$; instead, if $l=\theta$, then $\pi_{1}(l)=\theta$ and
$\pi_{2}(l)=\theta$, i.e., $l$ is projected on the empty marking.

Given a linking $l$, its inverse $l^{-1}$ is defined as:
$l^{-1}(s_{2},s_{1})=l(s_{1},s_{2})$. Given two linkings $l_{1}$ and $l_{2}$,
their relational composition $l_{1}\circ l_{2}$ defines a set of linkings,
that can be empty (so the operation is not defined) in case
$\pi_{2}(l_{1})\neq\pi_{1}(l_{2})$. A linking $h\in l_{1}\circ l_{2}$ if there
exists a multiset $k:S\times S\times S\rightarrow{\mathbb{N}}$ of triples of
places, such that $l_{1}(s_{1},s_{2})=\sum_{s_{3}\in S}k(s_{1},s_{2},s_{3})$,
$l_{2}(s_{2},s_{3})=\sum_{s_{1}\in S}k(s_{1},s_{2},s_{3})$ and
$h(s_{1},s_{3})=\sum_{s_{2}\in S}k(s_{1},s_{2},s_{3})$. For instance, if
$l_{1}=\\{(s_{1},s_{2}),(s_{1}^{\prime},s_{2})\\}$ and
$l_{2}=\\{(s_{2},s_{3}),(s_{2},s_{3}^{\prime})\\}$, then $l_{1}\circ
l_{2}=\\{h_{1},h_{2}\\}$, where
$h_{1}=\\{(s_{1},s_{3}),(s_{1}^{\prime},s_{3}^{\prime})\\}$ and
$h_{2}=\\{(s_{1},s_{3}^{\prime}),(s_{1}^{\prime},s_{3})\\}$.

We will use $l$, $\overline{l}$, $h$, $\overline{h}$, $c$ and $\overline{c}$,
possibly indexed, to range over linkings. As linkings are multisets, we can
use the operations defined over multisets, such as union $\oplus$ and
difference $\ominus$. For instance, $(l\oplus
c)(s_{1},s_{2})=l(s_{1},s_{2})+c(s_{1},s_{2})$.  $\Box$

###### Definition 11

(Structure Preserving Bisimulation) Let $N=(S,A,T)$ be a P/T net. A structure-
preserving bisimulation (sp-bisimulation, for short) is a set $R$ of linkings
such that if $l\in R$, then $\forall c\subseteq l$,

  1. 1.

$\forall t_{1}$ such that $\mbox{${}^{\bullet}t_{1}$}=\pi_{1}(c)$, there exist
a transition $t_{2}$ such that $\ell(t_{1})=\ell(t_{2})$,
$\mbox{${}^{\bullet}t_{2}$}=\pi_{2}(c)$, and a linking $\overline{c}$ such
that $\mbox{$t_{1}^{\bullet}$}=\pi_{1}(\overline{c})$,
$\mbox{$t_{2}^{\bullet}$}=\pi_{2}(\overline{c})$ and $\overline{l}=(l\ominus
c)\oplus\overline{c}\in R$;

  2. 2.

$\forall t_{2}$ such that $\mbox{${}^{\bullet}t_{2}$}=\pi_{2}(c)$, there exist
a transition $t_{1}$ such that $\ell(t_{1})=\ell(t_{2})$,
$\mbox{${}^{\bullet}t_{1}$}=\pi_{1}(c)$, and a linking $\overline{c}$ such
that $\mbox{$t_{1}^{\bullet}$}=\pi_{1}(\overline{c})$,
$\mbox{$t_{2}^{\bullet}$}=\pi_{2}(\overline{c})$ and $\overline{l}=(l\ominus
c)\oplus\overline{c}\in R$.

Two markings $m_{1}$ and $m_{2}$ are structure-preserving bisimilar, denoted
by $m_{1}\sim_{sp}m_{2}$, if there exists a linking $l$ in a structure
preserving bisimulation $R$ such that $m_{1}=\pi_{1}(l)$ and
$m_{2}=\pi_{2}(l)$.  $\Box$

Note that the two matching transitions $t_{1}$ and $t_{2}$ in the structure-
preserving bisimulation game must have the same shape because $(i)$
$\mbox{${}^{\bullet}t_{1}$}=\pi_{1}(c)$ and
$\mbox{${}^{\bullet}t_{2}$}=\pi_{2}(c)$ implies that
$|\mbox{${}^{\bullet}t_{1}$}|=|\mbox{${}^{\bullet}t_{2}$}|$, then $(ii)$
$\ell(t_{1})=\ell(t_{2})$ and, finally, $(iii)$ from
$\mbox{$t_{1}^{\bullet}$}=\pi_{1}(\overline{c})$ and
$\mbox{$t_{2}^{\bullet}$}=\pi_{2}(\overline{c})$ we derive that
$|\mbox{$t_{1}^{\bullet}$}|=|\mbox{$t_{2}^{\bullet}$}|$.

###### Remark 1

(Structure-preserving bisimilarity implies interleaving bisimilarity) It is
easy to observe that if $R_{1}$ is an sp-bisimulation, then

$R_{2}=\\{(\pi_{1}(l),\pi_{2}(l))\;\;\big{|}\;\;l\in R_{1}\\}$

is an interleaving bisimulation such that the matching transitions in the
bisimulation game have the same shape. Therefore, if $m_{1}\sim_{sp}m_{2}$,
then

  1. 1.

$\forall t_{1}$ such that $m_{1}[t_{1}\rangle m_{1}^{\prime}$, there exists
$t_{2}$ such that $m_{2}[t_{2}\rangle m_{2}^{\prime}$,
$|\mbox{${}^{\bullet}t_{1}$}|=|\mbox{${}^{\bullet}t_{2}$}|$,
$\ell(t_{1})=\ell(t_{2})$,
$|\mbox{$t_{1}^{\bullet}$}|=|\mbox{$t_{2}^{\bullet}$}|$ and
$m_{1}^{\prime}\sim_{sp}m_{2}^{\prime}$;

  2. 2.

$\forall t_{2}$ such that $m_{2}[t_{2}\rangle m_{2}^{\prime}$, there exists
$t_{1}$ such that $m_{1}[t_{1}\rangle m_{1}^{\prime}$,
$|\mbox{${}^{\bullet}t_{1}$}|=|\mbox{${}^{\bullet}t_{2}$}|$,
$\ell(t_{1})=\ell(t_{2})$,
$|\mbox{$t_{1}^{\bullet}$}|=|\mbox{$t_{2}^{\bullet}$}|$ and
$m_{1}^{\prime}\sim_{sp}m_{2}^{\prime}$.

$\Box$

###### Remark 2

(Structure-preserving bisimilarity implies step bisimilarity) It is easy to
observe that if $R$ is an sp-bisimulation, then it is also able to match steps
rather than single transitions. In fact, we want to prove that if $l\in R$,
then $\forall c\subseteq l$

  1. 1.

$\forall G_{1}$ such that $\mbox{${}^{\bullet}G_{1}$}=\pi_{1}(c)$, there exist
a step $G_{2}$ such that $\ell(G_{1})=\ell(G_{2})$,
$\mbox{${}^{\bullet}G_{2}$}=\pi_{2}(c)$, and a linking $\overline{c}$ such
that $\mbox{$G_{1}^{\bullet}$}=\pi_{1}(\overline{c})$,
$\mbox{$G_{2}^{\bullet}$}=\pi_{2}(\overline{c})$ and $\overline{l}=(l\ominus
c)\oplus\overline{c}\in R$;

  2. 2.

$\forall G_{2}$ such that $\mbox{${}^{\bullet}G_{2}$}=\pi_{2}(c)$, there exist
a step $G_{1}$ such that $\ell(G_{1})=\ell(G_{2})$,
$\mbox{${}^{\bullet}G_{1}$}=\pi_{1}(c)$, and a linking $\overline{c}$ such
that $\mbox{$G_{1}^{\bullet}$}=\pi_{1}(\overline{c})$,
$\mbox{$G_{2}^{\bullet}$}=\pi_{2}(\overline{c})$ and $\overline{l}=(l\ominus
c)\oplus\overline{c}\in R$.

This can be proved as follows. For simplicity’ sake, we consider a step
$G_{1}=\\{t_{1},t_{2}\\}$ composed of two transitions only; the general proof
is only notationally more complex. By symmetry we consider only the first
item.

If $\mbox{${}^{\bullet}G_{1}$}=\pi_{1}(c)$, this means that $c=c_{1}\oplus
c_{2}$ such that $\pi_{1}(c_{i})=\mbox{${}^{\bullet}t_{i}$}$ for $i=1,2$.
Since $l\in R$ and $R$ is an sp-bisimulation, for transition $t_{1}$, there
exist a transition $t_{1}^{\prime}$ such that
$\ell(t_{1})=\ell(t_{1}^{\prime})$,
$\pi_{2}(c_{1})=\mbox{${}^{\bullet}t_{1}^{\prime}$}$, and $\overline{c_{1}}$
such that $\pi_{1}(\overline{c_{1}})=\mbox{$t_{1}^{\bullet}$}$,
$\pi_{2}(\overline{c_{1}})=\mbox{$t_{1}^{\prime\bullet}$}$ and, moreover,
$(l\ominus c_{1})\oplus\overline{c_{1}}\in R$. Hence, for transition $t_{2}$,
there exist a transition $t_{2}^{\prime}$ such that
$\ell(t_{2})=\ell(t_{2}^{\prime})$,
$\pi_{2}(c_{2})=\mbox{${}^{\bullet}t_{2}^{\prime}$}$, and $\overline{c_{2}}$
such that $\pi_{1}(\overline{c_{2}})=\mbox{$t_{2}^{\bullet}$}$,
$\pi_{2}(\overline{c_{2}})=\mbox{$t_{2}^{\prime\bullet}$}$ and $(((l\ominus
c_{1})\oplus\overline{c_{1}})\ominus c_{2})\oplus\overline{c_{2}}$
$=(l\ominus(c_{1}\oplus c_{2}))\oplus(\overline{c_{1}}\oplus\overline{c_{2}})$
$=(l\ominus c)\oplus\overline{c}\in R$, by taking
$\overline{c_{1}}\oplus\overline{c_{2}}=\overline{c}$. Therefore, If
$\mbox{${}^{\bullet}G_{1}$}=\pi_{1}(c)$, then a step
$G_{2}=\\{t_{1}^{\prime},t_{2}^{\prime}\\}$ exists such that
$\ell(G_{1})=\ell(G_{2})$, $\mbox{${}^{\bullet}G_{2}$}=\pi_{2}(c)$, and a
linking $\overline{c}$ such that
$\mbox{$G_{1}^{\bullet}$}=\pi_{1}(\overline{c})$,
$\mbox{$G_{2}^{\bullet}$}=\pi_{2}(\overline{c})$ and $\overline{l}=(l\ominus
c)\oplus\overline{c}\in R$, as required.

As a consequence of this observation, it follows that if $R_{1}$ is an sp-
bisimulation, then $R_{2}=\\{(\pi_{1}(l),\pi_{2}(l))\;\;\big{|}\;\;l\in
R_{1}\\}$ is a step bisimulation.  $\Box$

Actually, it can be proved [11] that if two markings are sp-bisimilar, then
they generate the same causal nets (also called occurrence nets) [10, 2, 24],
so that this behavioral semantics is very concrete and slightly finer than
fully-concurrent bisimilarity [3], an adaptation to Petri nets of history-
preserving bisimilarity [28, 9, 6].

Interestingly enough, sp-bisimilarity is resource-aware: as a token is an
instance of a sequential process to be executed over one processor, if two
markings have different size, then a different number of processors is
necessary. Hence, a behavioral semantics, such as sp-bisimilarity, equates
distributed systems only if they require the same amount of execution
resources. Van Glabbeek [11] argued that structure-preserving bisimilarity
(hence, also its alternative process-oriented characterization, called causal-
net bisimilarity [11, 17]) is the most appropriate behavioral equivalence for
Petri nets, as it is the only one respecting a list of 9 desirable
requirements he proposed, among which there is the observation that it is the
coarsest equivalence respecting inevitability [22], meaning that if two
systems are equivalent, and in one the occurrence of a certain action is
inevitable, then so is it in the other one.

Finally, note that structure-preserving bisimilarity $\sim_{sp}$ is such that
it relates (dynamically) reachable markings only, i.e., it is a relation
actually defined over $Net_{d}(N(m_{0}))$.

$P_{1}$$C_{1}$prod$D_{1}$del$C_{1}^{\prime}$cons$P_{2}$$C_{2}$prodprod$D_{2}^{\prime}$$D_{2}^{\prime\prime}$deldel$C_{2}^{\prime}$cons
Figure 4: Two net bisimilar unbounded producer-consumer systems

###### Example 1

Consider the two nets in Figure 4, representing two unbounded producer-
consumer systems, where prod is the action of producing an item, del of
delivering an item, cons of consuming an item. We want to prove that
$P_{1}\oplus C_{1}\sim_{sp}P_{2}\oplus C_{2}$. This can be easily achieved by
defining the following set of links
$L=\\{(P_{1},P_{2}),(C_{1},C_{2}),(C_{1}^{\prime},C_{2}^{\prime}),$
$(D_{1},D_{2}^{\prime}),(D_{1},D_{2}^{\prime\prime})\\}$, and then by
considering the set $L^{+}$ of all the multisets over $L$: it is easy to
realize that $L^{+}$ is a structure-preserving bisimulation, that can be used
to prove not only that $P_{1}\oplus C_{1}\sim_{sp}P_{2}\oplus C_{2}$ but also
that, e.g., $2\cdot P_{1}\oplus 3\cdot C_{1}\oplus D_{1}\sim_{sp}2\cdot
P_{2}\oplus 3\cdot C_{2}\oplus D_{2}^{\prime\prime}$ as well as $D_{1}\oplus
C_{1}^{\prime}\sim_{sp}D_{2}^{\prime}\oplus C_{2}^{\prime}$. As a matter of
fact, $L$ is a place bisimulation [1, 16], a behavioral relation slightly
finer than structure-preserving bisimilarity (see [16] for examples
distinguishing place bisimilarity from sp-bisimilarity).  $\Box$

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

###### Proposition 3

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

  1. 1.

Given the set $Id=\\{(s,s)\;\;\big{|}\;\;s\in S\\}$, the set $Id^{+}$ is an
sp-bisimulation;

  2. 2.

the inverse $R^{-1}=\\{l^{-1}\;\;\big{|}\;\;l\in R\\}$ of an sp bisimulation
$R$ is an sp-bisimulation;

  3. 3.

the relational composition $R_{1}\circ R_{2}=\bigcup_{l_{1}\in R_{1},l_{2}\in
R_{2}}l_{1}\circ l_{2}$ of two sp-bisimulations $R_{1}$ and $R_{2}$ is an sp-
bisimulation;

  4. 4.

given a family $\\{R_{i}\\}_{i\in I}$ of structure-preserving bisimulations,
their union $\cup_{i\in I}R_{i}$ is an sp-bisimulation.

###### Proposition 4

For each P/T net $N=(S,A,T)$, $\sim_{sp}\;=\;\bigcup\\{R\;\;\big{|}\;\;$
$R\mbox{ is an sp-bisimulation}\\}$ is an equivalence relation and the largest
sp-bisimulation.

##  3 FNM: Syntax and Net Semantics

In this section we briefly recall some definitions and theorems from [14],
where the reader can find more details.

Let ${\mathcal{L}}$ be a finite set of names, ranged over by $a,b,c,\ldots$,
also called the input actions. Let $\overline{\mathcal{L}}$ be the set of co-
names, ranged over by $\overline{a},\overline{b},\overline{c},\ldots$, also
called the output actions. The set ${\mathcal{L}}\cup\overline{\mathcal{L}}$,
ranged over by $\alpha,\beta,\ldots$, is the set of observable actions. Let
$Act={\mathcal{L}}\cup\overline{\mathcal{L}}\cup\\{\tau\\}$, such that
$\tau\not\in{\mathcal{L}}\cup\overline{\mathcal{L}}$, be the finite set of
actions (or labels), ranged over by $\mu$. Action $\tau$ denotes an invisible,
internal activity. Let $\mathcal{C}$ be a finite set of process constants,
disjoint from $Act$, ranged over by $A,B,C,\ldots$, possibly indexed.

Finite-Net Multi-CCS (FNM for short) is the calculus whose terms are generated
from actions and constants as described by the following abstract syntax:

$\begin{array}[]{lclccccccccllcl}s&::=&\mbox{\bf
0}&|&\mu.t&|&\;\underline{a}.s&|&\;s+s&\hskip 42.67912pt\mbox{{\em guarded
terms}}\\\ q&::=&s&|&C&&&&&\hskip 42.67912pt\mbox{{\em sequential terms}}\\\
t&::=&q&|&t\mbox{$\,|\,$}t&&&&&\hskip 36.98866pt\mbox{{\em restriction-free
terms}}\\\ p&::=&t&|&\mbox{$({\bf\nu}a)$}p&&&&&\hskip 36.98866pt\mbox{{\em
general terms}}\\\ \\\ \end{array}$

where we assume that a constant $C$ is defined by a guarded process, i.e., a
process in syntactic category $s$ (i.e., $C\doteq s$). An FNM term $p$ is an
FNM process if the set Const$(p)$ of constants used by $p$ is finite and each
constant in Const$(p)$ is equipped with a defining equation. The set of FNM
processes is denoted by $\mathcal{P}_{FNM}$, the set of its sequential
processes, i.e., of the processes in syntactic category $q$, by
$\mathcal{P}_{FNM}^{seq}$, and the set of its guarded processes, i.e., of the
processes in syntactic category $s$, by $\mathcal{P}_{FNM}^{grd}$.

The FNM operators are those of CCS [21, 13], used in constrained manner, with
the addition of the strong prefixing operator: $\underline{a}.s$ is a strongly
prefixed process, where the strong prefix $a$ is the first input action of a
transaction that continues with the sequential process $s$ (provided that $s$
can complete the transaction). Hence, the strong prefixing operator allows for
the creation of transitions labeled by an atomic sequence $\sigma$, which is a
sequence of visible actions, composed of inputs only, but possibly ending with
an output, that are executed atomically; more precisely, $\sigma$ ranges over
the set of labels
${\mathcal{A}}=\\{\tau\\}\cup\mathcal{L}^{*}\cdot(\mathcal{L}\cup\overline{\mathcal{L}})$.
E.g., $\underline{a}.(b.\mbox{\bf 0}+\overline{c}.\mbox{\bf 0})$ can perform
two transitions reaching 0: one labeled by the atomic sequence $ab$, the other
one by the atomic sequence $a\overline{c}$.

A consequence of the fact that transitions may be labeled by atomic sequences
is the need for a new, more general, discipline of synchronization, which
extends the basic CCS rule [21, 13] for synchronizing two complementary
actions. Two sequences $\sigma_{1}$ and $\sigma_{2}$ can be synchronized, and
the result is $\sigma$, if relation
$\mathit{Sync}(\sigma_{1},\sigma_{2},\sigma)$ holds. This relation, formally
defined in Table 1, holds if at least one of the two sequences is a single
output action, say $\sigma_{1}=\overline{a}$, and the other one is either the
complementary input action $a$ or an atomic sequence starting with $a$. Hence,
it is not possible to synchronize two atomic sequences.

A well-formed FNM process [14] $p$ is an FNM process satisfying a simple
syntactic condition, denoted by wf(p), ensuring that its executable atomic
sequences are composed of input actions only. This ensures that a multi-party
synchronization can take place only among one leader, i.e., the process
performing the atomic sequence of inputs, and as many other components (the
servants), as the length of the atomic sequence, where each servant executes
one output action. We will show that the Petri net associated with a well-
formed FNM process $p$ is finite. In the following we restrict our attention
to well-formed processes only.

$\begin{array}[]{lclclclclcl}\begin{array}[]{c}\\\
\hline\cr\mathit{Sync}(\alpha,\overline{\alpha},\tau)\end{array}&\quad\begin{array}[]{c}\sigma\neq\epsilon\\\
\hline\cr\mathit{Sync}(a\sigma,\overline{a},\sigma)\end{array}&\quad\begin{array}[]{c}\sigma\neq\epsilon\\\
\hline\cr\mathit{Sync}(\overline{a},a\sigma,\sigma)\end{array}\\\\[-5.69046pt]
\end{array}$

Table 1: Synchronization relation $\mathit{Sync}$

###  3.1 Extended Terms

The FNM processes are built upon the set
${\mathcal{L}}\cup\overline{\mathcal{L}}$, ranged over by $\alpha$, of visible
actions. We assume we also have sets
${\mathcal{L}}^{\prime}=\\{a^{\prime}\,|\,a\in\mathcal{L}\\}$ and
$\overline{{\mathcal{L}}^{\prime}}=$ $\\{\overline{a^{\prime}}\,|\,$
$\overline{a}\in\overline{\mathcal{L}}\\}$, where
${\mathcal{L}}^{\prime}\cup\overline{\mathcal{L}^{\prime}}$, ranged over by
$\alpha^{\prime}$, is the set of auxiliary restricted actions, i.e., actions
that are only allowed to synchronize. By definition, each restricted action
$\alpha^{\prime}$ corresponds to exactly one visible action $\alpha$. Let
$\mathcal{G}=$ ${\mathcal{L}}\cup{\mathcal{L}}^{\prime}$, ranged over by
$\gamma$, be the set of input actions and their restricted counterparts.
$\overline{\mathcal{G}}=\overline{\mathcal{L}}\cup\overline{{\mathcal{L}}^{\prime}}$
is the set of output actions and their restricted counterparts. The set
$Act_{\gamma}={\mathcal{G}}\cup\overline{\mathcal{G}}\cup\\{\tau\\}$, ranged
over by $\mu$ (with abuse of notation), is used to build the set of extended
terms, whose syntax is defined as for FNM, where the prefixes are taken from
the set $Act_{\gamma}$, the strong prefixes from the set $\mathcal{G}$ and the
bound action $a$ is in $\mathcal{L}$. An extended general FNM term
$p=\mbox{$({\bf\nu}L)$}t$ is an extended process if Const$(p)$ is finite, each
constant in Const$(p)$ is defined and $t$ is admissible, i.e.,

$\hskip 113.81102pt\forall a\in\mathcal{L},\,\\{a,a^{\prime}\\}\not\subseteq
fn(t)$,

where the function $fn(-)$, computing the free names, is defined on extended
terms in the obvious way. The admissibility condition expresses a sort of
sanity check on any restriction-free, extended term $t$: it is not possible
that, for each action $a\in\mathcal{L}$, there are occurrences in $t$ of both
$a$ and its associated restricted action $a^{\prime}$; this because each
action type can occur in $t$ only in one of the two modalities: either
restricted or unrestricted (i.e., normally visible). For instance,
$a.a^{\prime}.\mbox{\bf 0}$ is not admissible, while $a.\mbox{\bf
0}\mbox{$\,|\,$}b^{\prime}.\mbox{\bf 0}$ is admissible. By the notation
$ad(t)$ we mean that $t$ is admissible.

By ${\mathcal{P}}_{FNM}^{\gamma}$ we denote the set of all extended FNM
processes. By ${\mathcal{P}}_{FNM}^{\gamma,par}$ we denote the set of all
restriction-free, extended FNM processes, i.e., those extended processes in
syntactic category $t$. By ${\mathcal{P}}_{FNM}^{\gamma,seq}$ we denote the
set of all sequential, extended FNM processes, i.e., those extended processes
in syntactic category $q$. By ${\mathcal{P}}_{FNM}^{\gamma,grd}$ we denote the
set of all guarded, extended FNM processes, i.e., those extended processes in
syntactic category $s$.

###  3.2 Net Semantics

In this section, we summarize a technique (operational in style), proposed in
[14], for building an infinite P/T net for the whole of FNM, starting from a
description of its places and its net transitions. The resulting net
$N_{FNM}=(S_{FNM},\mathcal{A},T_{FNM})$ is such that, for each
$p\in{\mathcal{P}}_{FNM}$, the net system $N_{FNM}(\mbox{$dec$}(p))$
statically reachable from the initial marking $\mbox{$dec$}(p)$ is a
statically reduced P/T net, which is finite if $p$ is well-formed; such a net
system is denoted by $Net(p)$.

$\begin{array}[]{rclrclllll}\mbox{$dec$}(\mbox{\bf
0})&=&\theta&\qquad\mbox{$dec$}(p+q)&=&\\{p+q\\}&\mbox{$dec$}(\mu.p)&=&\\{\mu.p\\}\\\
\mbox{$dec$}(\underline{\gamma}.p,I)&=&\\{\underline{\gamma}.p\\}&\qquad\mbox{$dec$}(p\mbox{$\,|\,$}q)&=&\mbox{$dec$}(p)\oplus
dec(q)\\\
\mbox{$dec$}(C)&=&\\{C\\}&\qquad\mbox{$dec$}(\mbox{$({\bf\nu}a)$}p)&=&\mbox{$dec$}(p)\mbox{$\\{a^{\prime}/a\\}$}\quad
a^{\prime}\in{\mathcal{L}}^{\prime}\\\\[-8.5359pt] \end{array}$

Table 2: Decomposition function

The set of FNM places, ranged over by $s$, is
$S_{FNM}={\mathcal{P}}_{FNM}^{\gamma,seq}\setminus\\{\mbox{\bf 0}\\}$, i.e.,
the set of all sequential, extended FNM processes, except 0.

Function
$\mbox{$dec$}:{\mathcal{P}}_{FNM}^{\gamma}\rightarrow{\mathcal{M}}_{fin}(S_{FNM})$,
which maps extended processes into markings, is outlined in Table 2. Process 0
is mapped to the empty marking $\theta$. A sequential process $p$ is mapped to
one place with name $p$. This is the case of $\mu.p$ (where $\mu$ can be any
action in $Act_{\gamma}$), a constant $C$, $p+q$ and $\underline{\gamma}.p$
(where $\gamma\in\mathcal{G}=\mathcal{L}\cup\mathcal{L}^{\prime}$). Note that
when $C\doteq\mbox{\bf 0}$, we have that $\mbox{$dec$}(\mbox{\bf
0})=\theta\neq\\{C\\}=\mbox{$dec$}(C)$. Note also that $\mbox{$dec$}(\mbox{\bf
0})=\theta\neq\\{\mbox{\bf 0}+\mbox{\bf 0}\\}=\mbox{$dec$}(\mbox{\bf
0}+\mbox{\bf 0})$.

Parallel composition is interpreted as multiset union; e.g., the decomposition
of $a.\mbox{\bf 0}\mbox{$\,|\,$}a.\mbox{\bf 0}$ produces the marking
$a.\mbox{\bf 0}\oplus a.\mbox{\bf 0}=2\cdot a.\mbox{\bf 0}$. The decomposition
of a general process $\mbox{$({\bf\nu}a)$}p$ – where $a\in\mathcal{L}$ –
generates the multiset obtained from the decomposition of $p$, to which the
substitution $\\{a^{\prime}/a\\}$ is applied; the application of the
substitution $\\{a^{\prime}/a\\}$ to a multiset is performed element-wise. We
assume that, in decomposing $\mbox{$({\bf\nu}a)$}p$, the choice of the
restricted name is fixed by the rule that associates with a visible action $a$
its unique corresponding restricted action $a^{\prime}$.

###### Proposition 5

For each $p\in{\mathcal{P}}_{FNM}^{\gamma}$, $\mbox{$dec$}(p)$ is a finite
multiset of places.  $\Box$

A marking $m\in{\mathcal{M}}_{fin}(S_{FNM})$ is admissible, denoted by
$ad(m)$, if for all $a\in\mathcal{L}$, $\\{a,a^{\prime}\\}\not\subseteq
fn(m)$, where $fn(m)=\bigcup_{s\in dom(m)}fn(s)$, with $fn(\theta)=\emptyset$.

A marking $m\in{\mathcal{M}}_{fin}(S_{FNM})$ is complete if an FNM process
$p\in\mathcal{P}_{FNM}$ exists such that $\mbox{$dec$}(p)=m$.

###### Theorem 3.1

A marking $m\in{\mathcal{M}}_{fin}(S_{FNM})$ is admissible iff it is complete.
$\Box$

Hence, this theorem states not only that function $dec$ maps FNM processes to
admissible markings over $S_{FNM}$, but also that $dec$ is surjective over
this set.

###### Definition 12

(Well-behaved) A set of places $S\subseteq S_{FNM}$ is well behaved if for all
$s\in S$ we have that wf$(s)$ holds, i.e., the sequential FNM extended term
$s$ is well-formed.  $\Box$

In order to define the set $T_{FNM}$ of all the FNM net transitions, we need
some auxiliary definitions. Let
${\mathcal{A}}^{\gamma}=\\{\tau\\}\cup\mathcal{G}^{*}\cdot(\mathcal{G}\cup\overline{\mathcal{G}})$,
ranged over by $\sigma$ with abuse of notation, be the set of labels; hence, a
label $\sigma$ can be the invisible action $\tau$, or a (possibly empty)
sequence of inputs (or restricted inputs) followed by an input or an output
(or its restricted counterpart). Let
$\rightarrow\;\subseteq{\mathcal{M}}_{fin}(S_{FNM})\times{\mathcal{A}}^{\gamma}\times{\mathcal{M}}_{fin}(S_{FNM})$
be the least set of transitions generated by the axiom and rules in Table 3.

$\begin{array}[]{lcllcl}\mbox{(pref)}&\begin{array}[]{c}\\\
\hline\cr\\{\mu.p\\}{\mbox{${\>\stackrel{{\scriptstyle\mu}}{{\longrightarrow}}\>}$}}\mbox{$dec$}(p)\end{array}&&\;\;\;\mbox{(cons)}&\begin{array}[]{c}\mbox{$dec$}(p){\mbox{${\>\stackrel{{\scriptstyle\sigma}}{{\longrightarrow}}\>}$}}m\\\
\hline\cr\\{C\\}{\mbox{${\>\stackrel{{\scriptstyle\sigma}}{{\longrightarrow}}\>}$}}m\end{array}&C\doteq
p\\\
\mbox{(sum${}_{1}$)}&\begin{array}[]{c}\mbox{$dec$}(p){\mbox{${\>\stackrel{{\scriptstyle\sigma}}{{\longrightarrow}}\>}$}}m\\\
\hline\cr\\{p+q\\}{\mbox{${\>\stackrel{{\scriptstyle\sigma}}{{\longrightarrow}}\>}$}}m\end{array}&&\;\;\;\mbox{(s-pref)}&\begin{array}[]{c}\mbox{$dec$}(p){\mbox{${\>\stackrel{{\scriptstyle\sigma}}{{\longrightarrow}}\>}$}}m\\\
\hline\cr\\{\underline{\gamma}.p\\}{\mbox{${\>\stackrel{{\scriptstyle\gamma\diamond\sigma}}{{\longrightarrow}}\>}$}}m\end{array}\\\
\end{array}$

$\begin{array}[]{lcllcl}\mbox{(s-com)}&\begin{array}[]{c}m_{1}{\mbox{${\>\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}\>}$}}m_{1}^{\prime}\;\;m_{2}{\mbox{${\>\stackrel{{\scriptstyle\sigma_{2}}}{{\longrightarrow}}\>}$}}m_{2}^{\prime}\\\
\hline\cr m_{1}\oplus
m_{2}{\mbox{${\>\stackrel{{\scriptstyle\sigma}}{{\longrightarrow}}\>}$}}m_{1}^{\prime}\oplus
m_{2}^{\prime}\end{array}&ad(m_{1}\oplus m_{2})\wedge
Sync(\sigma_{1},\sigma_{2},\sigma)\\\ \end{array}$

Table 3: Rules for net transitions (symmetric rule (sum2) omitted)

Let us comment on the rules of Table 3. Axiom (pref) states that if one token
is present in the place $\mu.p$, then a $\mu$-labeled transition is derivable
from marking $\\{\mu.p\\}$, producing the marking $\mbox{$dec$}(p)$. This
holds for each $\mu$, i.e., for the invisible action $\tau$, for each visible
action $\alpha$ as well as for each restricted action $\alpha^{\prime}$. By
rule (sum1), the transitions from the place $p+q$ are those from the marking
$\mbox{$dec$}(p)$; as $p$ is sequential, $\mbox{$dec$}(p)$ is $\\{p\\}$ if
$p\neq\mbox{\bf 0}$, while, if $p=\mbox{\bf 0}$, $\mbox{$dec$}(p)=\theta$, but
no transition is derivable from the empty marking, so that the rule is really
applicable only when $\mbox{$dec$}(p)=\\{p\\}$. Similarly, rule (cons) states
that the transitions derivable from $\\{C\\}$ are those derivable from the
place $\\{p\\}$, if $C\doteq p$ with $p\neq\mbox{\bf 0}$. In rule (s-pref),
$\gamma$ may be any input action $a$ or any restricted action $a^{\prime}$,
and the auxiliary function $\gamma\diamond\sigma$ returns $\gamma$ if
$\sigma=\tau$, or $\gamma\sigma$ otherwise. This rule requires that the
premise transition
$\mbox{$dec$}(p){\mbox{${\>\stackrel{{\scriptstyle\sigma}}{{\longrightarrow}}\>}$}}m$
be derivable by the rules, which is really possible only when
$\mbox{$dec$}(p)=\\{p\\}$. Rule (s-com) requires that the transition pre-set
be admissible in order to avoid producing transitions that have no counterpart
in the LTS semantics of FNM, described in [14]. Rule (s-com) explains how a
synchronization takes place: it is required that $m_{1}$ and $m_{2}$ perform
synchronizable sequences $\sigma_{1}$ and $\sigma_{2}$, producing $\sigma$;
here we assume that relation $\mathit{Sync}$ has been extended also to
restricted actions in the obvious way, i.e., a restricted output action
$\overline{a^{\prime}}$ can be synchronized only with its complementary
restricted input action $a^{\prime}$ or with an atomic sequence beginning with
$a^{\prime}$. As an example, the net transition
$\\{\underline{a}.b^{\prime}.p,\overline{a}.q,\overline{b^{\prime}}.r\\}{\mbox{${\>\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}\>}$}}\mbox{$dec$}(p)\oplus\mbox{$dec$}(q)\oplus\mbox{$dec$}(r)$
is derivable by the rules, as shown in Table 4.

(pref) $\\{b^{\prime}.p\\}{\mbox{${\>\stackrel{{\scriptstyle
b^{\prime}}}{{\longrightarrow}}\>}$}}\mbox{$dec$}(p)$ (s-pref)
$\\{\underline{a}.b^{\prime}.p\\}{\mbox{${\>\stackrel{{\scriptstyle
ab^{\prime}}}{{\longrightarrow}}\>}$}}\mbox{$dec$}(p)$ (pref)
$\\{\overline{a}.q\\}{\mbox{${\>\stackrel{{\scriptstyle\overline{a}}}{{\longrightarrow}}\>}$}}\mbox{$dec$}(q)$
(s-com)
$\\{\underline{a}.b^{\prime}.p,\overline{a}.q\\}{\mbox{${\>\stackrel{{\scriptstyle
b^{\prime}}}{{\longrightarrow}}\>}$}}\mbox{$dec$}(p)\oplus\mbox{$dec$}(q)$
(pref)
$\\{\overline{b^{\prime}}.r\\}{\mbox{${\>\stackrel{{\scriptstyle\overline{b^{\prime}}}}{{\longrightarrow}}\>}$}}\mbox{$dec$}(r)$
(s-com)
$\\{\underline{a}.b^{\prime}.p,\overline{a}.q,\overline{b^{\prime}}.r\\}{\mbox{${\>\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}\>}$}}\mbox{$dec$}(p)\oplus\mbox{$dec$}(q)\oplus\mbox{$dec$}(r)$

Table 4: The proof of a net transition

Transitions with labels containing restricted actions must not be taken in the
resulting net, as we accept only transitions labeled over
${\mathcal{A}}=\\{\tau\\}\cup\mathcal{L}^{*}\cdot(\mathcal{L}\cup\overline{\mathcal{L}})$.
However, they are useful in producing acceptable transitions, as two
complementary restricted actions can synchronize, producing a $\tau$-labeled
transition or shortening the synchronized sequence. For instance, in the
example above, the derivable transition
$\\{b^{\prime}.p\\}{\mbox{${\>\stackrel{{\scriptstyle
b^{\prime}}}{{\longrightarrow}}\>}$}}\mbox{$dec$}(p)$ is not an acceptable
transition because its label is not in ${\mathcal{A}}$, while
$\\{\underline{a}.b^{\prime}.p,\overline{a}.q,\overline{b^{\prime}}.r\\}{\mbox{${\>\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}\>}$}}\mbox{$dec$}(p)\oplus\mbox{$dec$}(q)\oplus\mbox{$dec$}(r)$
is so. Hence, the P/T net for FNM is the triple
$N_{FNM}=(S_{FNM},{\mathcal{A}},$ $T_{FNM})$, where the set

$T_{FNM}=\\{(m_{1},\sigma,m_{2})\;\;\big{|}\;\;m_{1}{\mbox{${\>\stackrel{{\scriptstyle\sigma}}{{\longrightarrow}}\>}$}}m_{2}$
$\mbox{ is derivable by the rules and }\sigma\in{\mathcal{A}}\\}$

is obtained by filtering out those transitions derivable by the rules whose
label $\sigma$ contains some restricted name $a^{\prime}$ or
$\overline{a^{\prime}}$.

We now want to show that for each finite, well-behaved set of places
$S\subseteq S_{FNM}$, the set of transitions statically enabled at $S$ is
finite. Given a place $s\in S$, by $s\vdash t$ we mean that transition
$t=(\\{s\\},\sigma,m)$ is derivable by the rules in Table 3, hence with
$\sigma\in\mathcal{A}^{\gamma}$.

###### Lemma 1

The set $T_{s}=\\{t\;\;\big{|}\;\;s\vdash t\\}$ is finite, for each $s\in
S_{FNM}$.

Given a finite, well-behaved set of places $S\subseteq S_{FNM}$, let
$T^{S}_{1}$ be $\bigcup_{s\in S}T_{s}$, i.e., the set of all transitions, with
a singleton pre-set in $S$, derivable by the rules with labeling in
$\mathcal{A}^{\gamma}$. The set $T^{S}_{1}$ is finite, being the finite union
(as $S$ is finite) of finite sets (as $T_{s}$ is finite for each $s\in S$, by
Lemma 1).

Let $k\in{\mathbb{N}}$ be the length of the longest label of the transitions
in $T^{S}_{1}$. It is possible to argue (details in [14]) that if a multi-
party transition $t$ is derivable by the rules from the well-behaved set $S$,
then its proof contains $k$ synchronizations at most, each one between a
transition (labeled with a sequence of inputs) and a singleton-pre-set
transition (labeled with a single output action); hence, at most $k+1$
participants can take part in a multi-party synchronization. Therefore, the
set of all the transitions statically enabled at a finite, well-behaved set
$S$ can be defined by means of a sequence of sets $T^{S}_{i}$ of transitions,
for $2\leq i\leq k+1$, where each transition $t\in T^{S}_{i}$ has a pre-set
${}^{\bullet}t$ of size $i$, as follows:

$\begin{array}[]{rclll}T^{S}_{i}&=&\\{(m_{1}\oplus
m_{2},\sigma,m_{1}^{\prime}\oplus m_{2}^{\prime})\;\;\big{|}\;\;ad(m_{1}\oplus
m_{2}),\\\
&&\qquad\qquad\exists\sigma_{1}\exists\gamma.(m_{1},\sigma_{1},m_{1}^{\prime})\in
T^{S}_{i-1},(m_{2},\overline{\gamma},m_{2}^{\prime})\in
T^{S}_{1},\mathit{Sync}(\sigma_{1},\overline{\gamma},\sigma)\\}.\end{array}$

Note that $T^{S}_{2}$ is finite, because $T^{S}_{1}$ is finite; inductively,
$T^{S}_{i+1}$, for $2\leq i\leq k$ is finite, because $T^{S}_{i}$ and $T_{1}$
are finite. So, the set $T_{S}$ of all the transitions statically enabled at
$S$ is

$T_{S}=\\{t\;\;\big{|}\;\;t\in\bigcup_{i=1}^{k+1}T^{S}_{i}\wedge\ell(t)\in\mathcal{A}\\},$

where only transitions labeled over $\mathcal{A}$ are considered. $T_{S}$ is
finite, being a finite union of finite sets; therefore, we have the following
result.

###### Theorem 3.2

If $S\subseteq S_{FNM}$ is a finite, well-behaved set of places, then set
$T_{S}\subseteq T_{FNM}$ of all the transitions statically enabled at $S$ is
finite.  $\Box$

(pref) $\\{dec.\mbox{\bf 0}\\}{\mbox{${\>\stackrel{{\scriptstyle
dec}}{{\longrightarrow}}\>}$}}\theta$ (s-pref)
$\\{\underline{c^{\prime}}.dec.\mbox{\bf
0}\\}{\mbox{${\>\stackrel{{\scriptstyle
c^{\prime}dec}}{{\longrightarrow}}\>}$}}\theta$ (s-pref)
$\\{\underline{c^{\prime}}.\underline{c^{\prime}}.dec.\mbox{\bf
0}\\}{\mbox{${\>\stackrel{{\scriptstyle
c^{\prime}c^{\prime}dec}}{{\longrightarrow}}\>}$}}\theta$ (sum1)
$\\{s_{2}\\}{\mbox{${\>\stackrel{{\scriptstyle
c^{\prime}c^{\prime}dec}}{{\longrightarrow}}\>}$}}\theta$ (pref)
$\\{\overline{c^{\prime}}.\mbox{\bf
0}\\}{\mbox{${\>\stackrel{{\scriptstyle\overline{c^{\prime}}}}{{\longrightarrow}}\>}$}}\theta$
(sum2)
$\\{s_{2}\\}{\mbox{${\>\stackrel{{\scriptstyle\overline{c^{\prime}}}}{{\longrightarrow}}\>}$}}\theta$
(s-com) $\\{s_{2},s_{2}\\}{\mbox{${\>\stackrel{{\scriptstyle
c^{\prime}dec}}{{\longrightarrow}}\>}$}}\theta$ (pref)
$\\{\overline{c^{\prime}}.\mbox{\bf
0}\\}{\mbox{${\>\stackrel{{\scriptstyle\overline{c^{\prime}}}}{{\longrightarrow}}\>}$}}\theta$
(sum2)
$\\{s_{2}\\}{\mbox{${\>\stackrel{{\scriptstyle\overline{c^{\prime}}}}{{\longrightarrow}}\>}$}}\theta$
(s-com) $\\{s_{2},s_{2},s_{2}\\}{\mbox{${\>\stackrel{{\scriptstyle
dec}}{{\longrightarrow}}\>}$}}\theta$

Table 5: The proof of a net transition, where
$s_{2}=\underline{c^{\prime}}.\underline{c^{\prime}}.dec.\mbox{\bf
0}+\overline{c}^{\prime}.\mbox{\bf 0}$

###### Example 2

(1/3 Semi-counter) Let us consider a semi-counter such that three occurrences
of $inc$ are needed to enable one $dec$, whence the name 1/3 semi-counter. The
well-formed process $p=\mbox{$({\bf\nu}c)$}A$, where

$A\doteq inc.(A\mbox{$\,|\,$}(\underline{c}.\underline{c}.dec.\mbox{\bf
0}+\overline{c}.\mbox{\bf 0}))$

is a 1/3 semi-counter. The initial marking $m_{0}$ is
$\mbox{$dec$}(p)=\mbox{$dec$}(\mbox{$({\bf\nu}c)$}A)=$
$\mbox{$dec$}(A)\mbox{$\\{c^{\prime}/c\\}$}=\\{A\\}\mbox{$\\{c^{\prime}/c\\}$}=\\{s_{1}\\}$;
place $s_{1}$ is the extended, sequential process
$A_{\mbox{$\\{c^{\prime}/c\\}$}}$, where the constant
$A_{\mbox{$\\{c^{\prime}/c\\}$}}$ is obtained by applying the substitution
$\\{c^{\prime}/c\\}$ to the body of $A$:

$A_{\mbox{$\\{c^{\prime}/c\\}$}}\doteq
inc.(A_{\mbox{$\\{c^{\prime}/c\\}$}}\mbox{$\,|\,$}(\underline{c^{\prime}}.\underline{c^{\prime}}.dec.\mbox{\bf
0}+\overline{c^{\prime}}.\mbox{\bf 0}))$.

Then, let $S_{0}=dom(m_{0})=\\{s_{1}\\}$. The set of transitions statically
enabled at $S_{0}$ is $T^{S_{0}}_{1}=T_{s_{1}}=\\{t_{1}\\}$, where the only
transition is $t_{1}=\\{s_{1}\\}{\mbox{${\>\stackrel{{\scriptstyle
inc}}{{\longrightarrow}}\>}$}}\\{s_{1},s_{2}\\}$, with
$s_{2}=\underline{c^{\prime}}.\underline{c^{\prime}}.dec.\mbox{\bf
0}+\overline{c}^{\prime}.\mbox{\bf 0}$. Therefore, the new set of statically
reachable places is $S_{1}=\\{s_{1},s_{2}\\}$. Note that $s_{2}$ can produce
two transitions in $T_{s_{2}}$, namely
$t^{\prime}=\\{s_{2}\\}{\mbox{${\>\stackrel{{\scriptstyle
c^{\prime}c^{\prime}dec}}{{\longrightarrow}}\>}$}}\theta$ and
$t^{\prime\prime}=\\{s_{2}\\}{\mbox{${\>\stackrel{{\scriptstyle\overline{c^{\prime}}}}{{\longrightarrow}}\>}$}}\theta$,
but neither is labeled over $\mathcal{A}$. Since the longest label has length
$3$, we have to compute the sets $T^{S_{1}}_{i}$ for $i=1,\ldots,4$:

$T^{S_{1}}_{1}=\\{t_{1},t^{\prime},t^{\prime\prime}\\}$,

$T^{S_{1}}_{2}=\\{t^{\prime\prime\prime}\\}$, where
$t^{\prime\prime\prime}=(\\{s_{2},s_{2}\\},c^{\prime}dec,\theta)$,

$T^{S_{1}}_{3}=\\{t_{2}\\}$, where
$t_{2}=(\\{s_{2},s_{2},s_{2}\\},dec,\theta)$, whose proof is shown in Table 5,

$T^{S_{1}}_{4}=\emptyset$.

Hence, $T_{S_{1}}=\\{t_{1},t_{2}\\}$, as these two are the only transitions
labeled over $\mathcal{A}$. As $t_{2}$ does not add any new reachable place,
we have that $S_{1}$ is the set of places statically reachable from the
initial marking, and $T_{S_{1}}$ is the set of transitions statically enabled
at $S_{1}$. This net is depicted in Figure 5.  $\Box$

$\;s_{1}$$inc\;$$\;s_{2}$$dec\;$3 Figure 5: The P/T net for the $1/3$ semi-
counter

The P/T net system associated with a process $p\in\mathcal{P}_{FNM}$ is the
subnet of $N_{FNM}$ statically reachable from the initial marking
$\mbox{$dec$}(p)$, denoted by $Net(p)$.

###### Definition 13

Let $p$ be a process in $\mathcal{P}_{FNM}$. The P/T net system statically
associated with $p$ is $Net(p)=(S_{p},A_{p},T_{p},m_{0})$, where
$m_{0}=\mbox{$dec$}(p)$ and

$\begin{array}[]{rcl}S_{p}&=&\llbracket dom(m_{0})\rangle\quad\mbox{computed
in $N_{FNM}$,}\\\ T_{p}&=&\\{t\in T_{FNM}\;\;\big{|}\;\;S_{p}\llbracket
t\rangle\\},\\\ A_{p}&=&\\{\sigma\in{\mathcal{A}}\;\;\big{|}\;\;\exists t\in
T_{p}\mbox{ such that }\ell(t)=\sigma\\}.\\\\[-8.5359pt] \end{array}$

$\Box$

The following propositions present three facts that are obviously true by
construction of the net $Net(p)$ associated with an FNM process $p$.

###### Proposition 6

For each $p\in{\mathcal{P}}_{FNM}$, $Net(p)$ is a statically reduced P/T net.
$\Box$

###### Proposition 7

If $\mbox{$dec$}(p)=\mbox{$dec$}(q)$, then $Net(p)=Net(q)$.  $\Box$

###### Proposition 8

For each restriction-free $t\in\mathcal{P}_{FNM}$ and for each
$L\subseteq\mathcal{L}$:

  * $i)$

If $Net(t)=(S,A,T,m_{0})$, then, for each $n\geq 1$, $Net(t^{n})=(S,A,T,n\cdot
m_{0})$, where $t^{1}=t$ and $t^{n+1}=t\mbox{$\,|\,$}t^{n}$.

  * $ii)$

If $Net(\mbox{$({\bf\nu}L)$}t)=(S,A,T,m_{0})$, then
$Net(\mbox{$({\bf\nu}L)$}(t^{n}))=(S,A,T,n\cdot m_{0})$, for $n\geq 1$.
$\Box$

Definition 13 suggests a way of generating $Net(p)$ with an algorithm based on
the inductive definition of the static reachability relation (see Definition
9): Start with the initial set of places $S_{0}=dom(\mbox{$dec$}(p))$, and
then apply the rules in Table 3 in order to produce the set $T_{S_{0}}$ of
transitions (labeled over $\mathcal{A}$) statically enabled at $S_{0}$, as
well as the additional places statically reachable by means of such
transitions. Then repeat this procedure from the set of places statically
reached so far. An instance of this procedure was given in Example 2. There
are two problems with this algorithm:

  * $\bullet$

the obvious halting condition is “until no new places are statically
reachable”; of course, the algorithm terminates if we know that the set
$S_{p}$ of places statically reachable from $dom(\mbox{$dec$}(p))$ is finite;
additionally,

  * $\bullet$

at each step of the algorithm, we have to be sure that the set of transitions
derivable from the current set of statically reachable places is finite.

We are going to prove only the first requirement — $S_{p}$ is finite for each
$p\in\mathcal{P}_{FNM}$ — because it implies also the second one for well-
formed processes. As a matter of fact, if $p$ is well formed, then
$dom(\mbox{$dec$}(p))$ is well behaved, and so is each set $S$ of places
statically reachable from $dom(\mbox{$dec$}(p))$ (as proved in [14]); since
$S\subseteq S_{p}$, $S$ is also finite, and so, by Theorem 3.2, the set
$T_{S}$ of transitions statically enabled at the finite, well-behaved set $S$
is finite, too.

###### Theorem 3.3

For each $p\in\mathcal{P}_{FNM}$, let $Net(p)=(S_{p},A_{p},T_{p},m_{0})$ be
defined as in Definition 13. Then, the set $S_{p}$ is finite.

###### Theorem 3.4

[14] For each well-formed FNM process $p$,
$Net(p)=(S_{p},A_{p},T_{p},\mbox{$dec$}(p))$ is a finite P/T net.  $\Box$

###  3.3 Representing All Finite P/T Net

Theorem 3.4 ensures that only finite P/T nets can be represented by FNM
processes. It is not completely obvious that all finite P/T nets can be
represented by FNM processes. However, we now hints (details in [14]), that
this is the case, indeed. As illustrated in Figure 6, given a P/T net
$N(m_{0})$, we define a translation to an FNM term
$\mathcal{T}_{FNM}(N(m_{0}))=p$, such that its associated net $Net(p)$,
according to the net semantics described in the previous section, is a P/T net
(rooted) isomorphic [14] to $N(m_{0})$, i.e., $N(m_{0})\cong_{r}Net(p)$.

Finite P/T
nets$N(m_{0})$$Net(p)$$\cong_{r}$FNM$p=\mathcal{T}_{FNM}(N(m_{0}))$translation
functionnet semantics Figure 6: Graphical description of the representability
theorem, up to isomorphism

The translation from nets to processes defines a constant $C_{i}$ in
correspondence with each place $s_{i}$; the constant $C_{i}$ has a summand
$c^{j}_{i}$ for each transition $t_{j}$, which is 0 when $s_{i}$ is not in the
pre-set of $t_{j}$. The FNM process $\mathcal{T}_{FNM}(N(m_{0}))$ associated
with the finite net system $N(m_{0})$, labeled over
$\mathcal{L}\cup\\{\tau\\}$, has a bound name $x^{j}_{i}$ for each pair
$(s_{i},t_{j})$, where $s_{i}$ is a place and $t_{j}$ is a transition; such
bound names are used to force synchronization among the components
participating in transition $t_{j}$ with pre-set of cardinality two or more.
Among the many places in the pre-set of $t_{j}$, the one with least index $i$
(as we assume that places are indexed) plays the role of leader of the
synchronization; the corresponding leader constant $C_{i}$ has a summand
$c_{i}^{j}$ containing the atomic input sequence needed for the multi-party
synchronization, such that each strong input prefix $x_{h}^{j}$ (for $h>i$) is
synchronized with the corresponding output $\overline{x}_{h}^{j}$ performed by
the servant participant of index $h$; in case
$\mbox{${}^{\bullet}t_{j}$}(s_{i})\geq 2$, then the summand $c_{i}^{j}$ is
actually a sum of $\overline{x}^{j}_{i}.\mbox{\bf 0}$ with the atomic input
sequence, so that one instance of $C_{i}$ acts as the leader, while the others
are servants.

###### Definition 14

(Translating finite P/T nets into well-formed FNM processes) Given
$A\subseteq\mathcal{L}\cup\\{\tau\\}$, let $N(m_{0})=(S,A,T,m_{0})$ — with
$S=\\{s_{1},\ldots,s_{n}\\}$, $T=\\{t_{1},\ldots,t_{k}\\}$, and
$\ell(t_{j})=\mu_{j}$ — be a finite P/T net. Function $\mathcal{T}_{FNM}(-)$,
from finite P/T nets to well-formed FNM processes, is defined as

$\mathcal{T}_{FNM}(N(m_{0}))=\mbox{$({\bf\nu}L)$}(\underbrace{C_{1}|\cdots|C_{1}}_{m_{0}(s_{1})}|\cdots|\underbrace{C_{n}|\cdots|C_{n}}_{m_{0}(s_{n})})$

where
$L=\\{x^{1}_{1},\ldots,x^{1}_{n},x^{2}_{1},\ldots,x^{2}_{n},\ldots,x^{k}_{1},\ldots,x^{k}_{n}\\}$
is such that $L\cap A=\emptyset$, each $C_{i}$ is equipped with a defining
equation $C_{i}\;\doteq{}\;c_{i}^{1}+\cdots+c_{i}^{k}$ (with
$C_{i}\doteq\mbox{\bf 0}$ if $k=0$), and each summand $c_{i}^{j}$, for
$j=1,\ldots,k$, is equal to

  * $\bullet$

0, if $s_{i}\not\in\mbox{${}^{\bullet}t$}_{j}$;

  * $\bullet$

$\mu_{j}.\Pi_{j}$, if $\mbox{${}^{\bullet}t$}_{j}=\\{s_{i}\\}$;

  * $\bullet$

$\overline{x}^{j}_{i}.\mbox{\bf 0}$, if $\mbox{${}^{\bullet}t$}_{j}(s_{i})>0$
and $\mbox{${}^{\bullet}t$}_{j}(s_{i^{\prime}})>0$ for some $i^{\prime}<i$
(i.e., $s_{i}$ is not the leader for the synchronization on $t_{j}$);

  * $\bullet$

$\underbrace{\underline{x}^{j}_{i+1}.\cdots.\underline{x}^{j}_{i+1}}_{\mbox{${}^{\bullet}t$}_{j}(s_{i+1})}.\ldots.\underbrace{\underline{x}^{j}_{n}.\cdots.\underline{x}^{j}_{n}}_{\mbox{${}^{\bullet}t$}_{j}(s_{n})}.\mu_{j}.\Pi_{j}$,
if $\mbox{${}^{\bullet}t$}_{j}(s_{i})=1$ and $s_{i}$ is the leader of the
synchronization (i.e., $\mbox{${}^{\bullet}t$}_{j}(s_{i^{\prime}})>0$ for no
$i^{\prime}<i$, while $\mbox{${}^{\bullet}t$}_{j}(s_{i^{\prime}})>0$ for some
$i^{\prime}>i$);

  * $\bullet$

$\overline{x}^{j}_{i}.\mbox{\bf
0}+\underbrace{\underline{x}^{j}_{i}.\cdots.\underline{x}^{j}_{i}}_{\mbox{${}^{\bullet}t$}_{j}(s_{i})-1}.\underbrace{\underline{x}^{j}_{i+1}.\cdots.\underline{x}^{j}_{i+1}}_{\mbox{${}^{\bullet}t$}_{j}(s_{i+1})}.\ldots.\underbrace{\underline{x}^{j}_{n}.\cdots.\underline{x}^{j}_{n}}_{\mbox{${}^{\bullet}t$}_{j}(s_{n})}.\mu_{j}.\Pi_{j}$,
otherwise (i.e., $s_{i}$ is the leader and
$\mbox{${}^{\bullet}t$}_{j}(s_{i})\geq 2$).

Finally, process $\Pi_{j}$ is
$\underbrace{C_{1}|\cdots|C_{1}}_{\mbox{$t_{j}^{\bullet}$}(s_{1})}|\cdots|\underbrace{C_{n}|\cdots|C_{n}}_{\mbox{$t_{j}^{\bullet}$}(s_{n})}$,
meaning that $\Pi_{j}=\mbox{\bf 0}$ if $\mbox{$t_{j}^{\bullet}$}=\theta$.
$\Box$

Note that $\mathcal{T}_{FNM}(N(m_{0}))$ is an FNM process: in fact, the
restriction operator occurs only at the top level, applied to the parallel
composition of a finite number of constants; each constant has a body that is
sequential and restriction-free. Note also that $\mathcal{T}_{FNM}(N(m_{0}))$
is a well-formed process: in fact, each strong prefix is a bound input
$x^{j}_{i}$, and each sequence ends with an action $\mu_{j}\in A$, which is
either an input or $\tau$; hence, no atomic sequence ends with an output.
Therefore, the following proposition holds by Theorem 3.4 and Proposition 6.

###### Proposition 9

For each finite P/T Petri net $N(m_{0})$, the net
$Net(\mathcal{T}_{FNM}(N(m_{0})))$ is a finite, statically reduced P/T net.
$\Box$

###### Theorem 3.5

(Representability Theorem)[14] Let $N(m_{0})=(S,A,T,m_{0})$ be a finite,
statically reduced P/T net system such that
$A\subseteq\mathcal{L}\cup\\{\tau\\}$, and let
$p=\mathcal{T}_{FNM}(N(m_{0}))$. Then, $Net(p)$ is isomorphic to $N(m_{0})$.
$\Box$

###### Example 3

Consider Figure 4(a). After clean-up (i.e., removing all the unnecessary 0
summands and all the unused restricted actions), its FNM representation is
$p=\mbox{$({\bf\nu}a)$}(P_{1}\mbox{$\,|\,$}C_{1})$, where $P_{1}\doteq
prod.(P_{1}\mbox{$\,|\,$}D_{1})$, $D_{1}\doteq\overline{a}.\mbox{\bf 0}$,
$C_{1}\doteq\underline{a}.del.C_{1}^{\prime}$ and $C_{1}^{\prime}\doteq
cons.C_{1}$. Indeed, $Net(p)$ is isomorphic to the net in Figure 4(a), where
place $P_{1}$ corresponds to the term $P_{1}\mbox{$\\{a^{\prime}/a\\}$}$
(i.e., the constant $P_{1\mbox{$\\{a^{\prime}/a\\}$}}\doteq
prod.(P_{1\mbox{$\\{a^{\prime}/a\\}$}}\mbox{$\,|\,$}D_{1\mbox{$\\{a^{\prime}/a\\}$}})$),
place $D_{1}$ to the term $D_{1}\mbox{$\\{a^{\prime}/a\\}$}$ (i.e., the
constant
$D_{1\mbox{$\\{a^{\prime}/a\\}$}}\doteq\overline{a}^{\prime}.\mbox{\bf 0}$),
and so on.  $\Box$

##  4 Structure Preserving Bisimilarity is a Congruence

Now we prove that structure-preserving bisimilarity $\sim_{sp}$ is a
congruence for the FNM operators, or, in other words, that the FNM operators
are compositional up to $\sim_{sp}$. We extend the definition of sp-
bisimilarity to FNM terms, i.e., we write $p\sim_{sp}q$, meaning that there
exists an sp-bisimulation $R$ in the net obtained by the union of $Net(p)$ and
$Net(q)$, that contains a linking $l$ such that $\mbox{$dec$}(p)=\pi_{1}(l)$
and $\mbox{$dec$}(q)=\pi_{2}(l)$. In the following, given an FNM term $r$, by
$Id_{r}$ we denote the set of links

$Id_{r}=\\{(s,s)\;\;\big{|}\;\;\exists m\in[\mbox{$dec$}(r)\rangle\text{ and
}s\in m\\}$

so that $Id_{r}^{+}$ is clearly a structure-preserving bisimulation justifying
$\mbox{$dec$}(r)\sim_{sp}\mbox{$dec$}(r)$.

###### Proposition 10

(Congruence for strong prefixing and choice) Let $p$ and $q$ be FNM guarded
processes, i.e., processes in syntactic category $s$. If $p\sim_{sp}q$, then

$\begin{array}[]{lrcll}(i)&\underline{a}.p&\sim_{sp}&\underline{a}.q,&\mbox{
for all $a\in\mathcal{L}$},\\\ (ii)&p+r&\sim_{sp}&q+r,&\mbox{ for each process
$r$ in syntactic category $s$.}\\\ \end{array}$

###### Proposition 11

(Congruence for prefixing) Let $p$ and $q$ be restriction-free FNM processes.
If $p\sim_{sp}q$, then $\mu.p\sim_{sp}\mu.q$, for all $\mu\in Act$.

In order to prove the congruence property for parallel composition on
restriction-free FNM process terms, we have to recall that a transition $t$
may be the result of a synchronization of many parallel transitions, say a
step $G=\\{t_{1},\ldots,t_{k}\\}$ (where each transition has preset of size
1), such that one transition is the leader of the synchronization, performing
a sequence of inputs, and all the others are servant transitions, performing
one output action only. Note that if $t$, derivable by repeated application of
rule (s-com), is enabled, then also all the transitions in the step $G$ are
derivable by the rules and enabled, as the process terms are restriction-free,
so that no restricted action may occur in the label of such transitions. We
now introduce an auxiliary relation, called $\mathit{MSync}$ and outlined in
Table 6, that explains how the synchronization of such a step $G$ takes place.

$\begin{array}[]{lcr}\begin{array}[]{c}\\\
\hline\cr\mathit{MSync}(\\{\sigma\\},\\{\sigma\\})\end{array}&&\begin{array}[]{c}\mathit{Sync}(\sigma_{1},\sigma_{2},\sigma)\;\;\;\mathit{MSync}(M\oplus\\{\sigma\\},M^{\prime})\\\
\hline\cr\mathit{MSync}(M\oplus\\{\sigma_{1},\sigma_{2}\\},M^{\prime})\end{array}\end{array}$

Table 6: Multiset synchronization relation $\mathit{MSync}$

###### Proposition 12

(Congruence for parallel composition) Let $p$ and $q$ be restriction-free FNM
processes. If $p\sim_{sp}q$, then $p\mbox{$\,|\,$}r\sim_{sp}q\mbox{$\,|\,$}r$,
for each restriction-free $r\in\mathcal{P}_{FNM}$.

Note that it is easy to generalize the congruence property for parallel
composition as follows: If $p_{i}\sim_{sp}q_{i}$ for $i=1,2$, then
$p_{1}\mbox{$\,|\,$}p_{2}\sim_{sp}q_{1}\mbox{$\,|\,$}q_{2}$. In fact, if
$R_{i}$ is an sp-bisimulation for $p_{i}\sim_{sp}q_{i}$, for $i=1,2$, then it
is easy to see that $R=\\{l_{1}\oplus l_{2}\;\;\big{|}\;\;l_{1}\in
R_{1},l_{2}\in R_{2}\\}$ is an sp-bisimulation.

###### Proposition 13

(Congruence for restriction)

Let $p$ and $q$ be general FNM processes. If $p\sim_{sp}q$, then
$\mbox{$({\bf\nu}a)$}p\sim_{sp}\mbox{$({\bf\nu}a)$}q$ for all
$a\in\mathcal{L}$.

Still there is one construct missing: recursion, defined over guarded terms
only. Consider an extension of FNM where terms can be constructed using
variables, such as $x,y,\ldots$: this defines an “open” FNM.

###### Definition 15

(Open FNM) Let $Var=\\{x,y,z,\ldots\\}$ be a finite set of variables. The FNM
open terms are generated from actions, constants and variables by the
following abstract syntax (using three syntactic categories):

$\begin{array}[]{lclccccccccllcl}s&::=&\mbox{\bf
0}&|&\mu.t&|&\;\underline{a}.s&|&\;s+s&\hskip 36.98866pt\mbox{{\em guarded
open terms}}\\\ q&::=&s&|&C&|&x&&&\hskip 39.83368pt\mbox{{\em sequential open
terms}}\\\ t&::=&q&|&t\mbox{$\,|\,$}t&&&&&\hskip 36.98866pt\mbox{{\em
restriction-free open terms}}\\\ p&::=&t&|&\mbox{$({\bf\nu}a)$}p&&&&&\hskip
36.98866pt\mbox{{\em general open terms}}\\\ \end{array}$

where $x$ is any variable taken from $Var$. The open net semantics for open
FNM extends the net semantics in Section 3 with
$Net(x)=(\\{x\\},\emptyset,\emptyset,x)$, so that, e.g., the semantics of
$a.x$ is the net $(\\{a.x,x\\},\\{a\\},$ $\\{(a.x,a,x)\\},a.x)$.  $\Box$

Sometimes we use the notation $p(x_{1},\ldots,x_{n})$ to state explicitly that
term $p$ is open on the tuple of variables $(x_{1},\ldots,x_{n})$. For
instance, $p_{1}(x)=a.(b.\mbox{\bf 0}+c.x)+d.x$ and
$p_{2}(x)=d.x+a.(c.x+b.\mbox{\bf 0})$ are open guarded FNM terms.

Structure-preserving bisimulation equivalence can be extended to open terms as
follows. An open term $p(x_{1},\ldots,x_{n})$ can be closed by means of a
substitution

$p(x_{1},\ldots,x_{n})\\{r_{1}/x_{1},\ldots,r_{n}/x_{n}\\}$

with the effect that each occurrence of the variable $x_{i}$ (within $p$ and
the body of each constant in Const$(p)$) is replaced by the closed FNM
sequential process $r_{i}$, for $i=1,\ldots,n$. For instance,
$p_{1}(x)\\{d.\mbox{\bf 0}/x\\}=a.(b.\mbox{\bf 0}+c.d.\mbox{\bf
0})+d.d.\mbox{\bf 0}$.

A natural extension of structure-preserving bisimilarity $\sim_{sp}$ over open
sequential terms is as follows:
$p(x_{1},\ldots,x_{n})\sim_{sp}q(x_{1},\ldots,x_{n})$ if for all tuples of
(closed) FNM terms $(r_{1},\ldots,r_{n})$, we have that

$p(x_{1},\ldots,x_{n})\\{r_{1}/x_{1},\ldots,r_{n}/x_{n}\\}$ $\sim_{sp}$
$q(x_{1},\ldots,x_{n})\\{r_{1}/x_{1},\ldots,r_{n}/x_{n}\\}$.

E.g., it is easy to see that $p_{1}(x)\sim_{sp}p_{2}(x)$. As a matter of fact,
for all $r$,

$p_{1}(x)\\{r/x\\}=a.(b.\mbox{\bf 0}+c.r)+d.r$ $\sim_{sp}$
$d.r+a.(c.r+b.\mbox{\bf 0})$ = $p_{2}(x)\\{r/x\\}$,

which can be easily proved.

This definition can be extended to open markings (which are multisets of
(open) sequential terms). If
$m(x_{1},\ldots,x_{n})=s_{1}(x_{1},\ldots,x_{n})\oplus\ldots\oplus
s_{k}(x_{1},\ldots,x_{n})$, then

$m(x_{1},\ldots,x_{n})\\{r_{1}/x_{1},\ldots,r_{n}/x_{n}\\}=$

$\hskip
42.67912pts_{1}(x_{1},\ldots,x_{n})\\{r_{1}/x_{1},\ldots,r_{n}/x_{n}\\}\oplus\ldots\oplus
s_{k}(x_{1},\ldots,x_{n})\\{r_{1}/x_{1},\ldots,r_{n}/x_{n}\\}$.

Therefore, we state
$m_{1}(x_{1},\ldots,x_{n})\sim_{sp}m_{2}(x_{1},\ldots,x_{n})$ if for all
tuples of (closed) FNM terms $(r_{1},\ldots,r_{n})$, we have that

$m_{1}(x_{1},\ldots,x_{n})\\{r_{1}/x_{1},\ldots,r_{n}/x_{n}\\}$ $\sim_{sp}$
$m_{2}(x_{1},\ldots,x_{n})\\{r_{1}/x_{1},\ldots,r_{n}/x_{n}\\}$.

For simplicity’s sake, let us now restrict our attention to open guarded terms
using a single undefined variable. We can recursively close an open term
$p(x)$ by means of a recursively defined constant. For instance, $A\doteq
p(x)\\{A/x\\}$. The resulting process constant $A$ is a closed FNM sequential
process. By saying that net bisimilarity is a congruence for recursion we mean
what is stated in the following. For simplicity’s sake, in the following a
term $p$ open on a variable $x$ is no longer annotated as $p(x)$.

###### Theorem 4.1

Let $p$ and $q$ be two open guarded FNM terms, with one variable $x$ at most.
Let $A\doteq p\\{A/x\\}$, $B\doteq q\\{B/x\\}$ and $p\sim_{sp}q$. Then
$A\sim_{sp}B$.

The extension to the case of open terms with multiple undefined constants,
e.g., $p(x_{1},\ldots,x_{n})$ can be obtained in a standard way [21, 13].

##  5 Algebraic Properties

Now we propose a set of algebraic properties that hold for structure-
preserving bisimilarity. For some of these, we take inspiration from similar
laws for standard bisimulation equivalence on the labeled transition system
semantics of CCS-like process algebras (see, e.g., [21, 13, 30]).

###### Proposition 14

(Laws of the choice operator) For all $p,q,r\in\mathcal{P}_{FNM}^{grd}$, the
following hold:

$\begin{array}[]{lrcllllll}&p+(q+r)&\sim_{sp}&(p+q)+r&&\;\mbox{(associativity)}\\\
&p+q&\sim_{sp}&q+p&&\;\mbox{(commutativity)}\\\ &p+\mbox{\bf
0}&\sim_{sp}&p&\mbox{if $p\neq\mbox{\bf 0}$\; }&\;\mbox{(identity)}\\\
&p+p&\sim_{sp}&p&\mbox{if $p\neq\mbox{\bf 0}$\; }&\;\mbox{(idempotency)}\\\
\end{array}$

Note that the identity law and the idempotency law have the side condition
$p\neq\mbox{\bf 0}$. This is strictly necessary because $\mbox{\bf
0}+\mbox{\bf 0}$ and 0 have a completely different semantics: the former
originates a stuck place, while the latter the empty marking. Of course, these
are not sp-bisimilar as $|\mbox{$dec$}(\mbox{\bf 0}+\mbox{\bf 0})|=1$ while
$|\mbox{$dec$}(\mbox{\bf 0})|=0$.

As we have shown that the choice operator $+$ is associative (and commutative)
w.r.t. $\sim_{sp}$, we sometimes use the $n$-ary version of this operator.
Hence, we shorten the term $(\ldots(p_{1}+p_{2})+\ldots+p_{n})$ as
$\sum_{i=1}^{n}p_{i}$.

###### Proposition 15

(Laws of the strong prefixing operator) For all
$p,q\in\mathcal{P}_{FNM}^{grd}$ and for each $a\in\mathcal{L}$, the following
hold:

$\begin{array}[]{lrcllllll}&\underline{a}.(p+q)&\sim_{sp}&\underline{a}.p+\underline{a}.q&&\;\mbox{(distribution)}\\\
&\underline{a}.\tau.p&\sim_{sp}&a.p&&\;\mbox{(absorption)}\\\ \mbox{if
$p\sim_{sp}\mbox{\bf 0}+\mbox{\bf 0}$ or $p=\mbox{\bf 0}$,
then}&\quad\underline{a}.p&\sim_{sp}&\mbox{\bf 0}+\mbox{\bf
0}&&\;\mbox{(annihilation)}\\\ \end{array}$

Note that in the annihilation law we have equated $\underline{a}.p$ to
$\mbox{\bf 0}+\mbox{\bf 0}$, as both are stuck places, and not to 0, whose
semantics is the empty marking.

###### Proposition 16

(Laws of the constant) For each $p\in\mathcal{P}_{FNM}^{grd}$, and each
$C\in\mathcal{C}$, the following hold:

$\begin{array}[]{lrcllllll}\mbox{if $C\doteq\mbox{\bf 0}$, then}&\quad
C&\sim_{sp}&\mbox{\bf 0}+\mbox{\bf 0}&&\;\mbox{(stuck)}\\\ \mbox{if $C\doteq
p$ and $p\neq\mbox{\bf 0}$, then}&\quad C&\sim_{sp}&p&&\;\mbox{(unfolding)}\\\
\mbox{if $C\doteq p\\{C/x\\}$ and $q\sim_{sp}p\\{q/x\\}$ then}&\quad
C&\sim_{sp}&q&&\;\mbox{(folding)}\\\ \end{array}$

where, in the third law, $p$ is actually open on $x$ (while $q$ is closed).

###### Remark 3

Note that the stuck property and the unfolding property can be summarized by
one single unfolding law as follows:

if $C\doteq p$, then $C\sim_{sp}p+\mbox{\bf 0}$

because in case $p=\mbox{\bf 0}$, we have that $C$ is sp-bisimilar to
$\mbox{\bf 0}+\mbox{\bf 0}$, while in case $p\neq\mbox{\bf 0}$, the addition
of the summand 0 is irrelevant, as it can be absorbed (by the identity law in
Proposition 14).  $\Box$

###### Proposition 17

(Laws of the parallel operator) For all restriction-free FNM processes
$p,q,r$, the following hold:

$\begin{array}[]{lrclllll}&\quad
p\mbox{$\,|\,$}(q\mbox{$\,|\,$}r)&\;\sim_{sp}&(p\mbox{$\,|\,$}q)\mbox{$\,|\,$}r&&\mbox{(associativity)}\\\
&\quad
p\mbox{$\,|\,$}q&\;\sim_{sp}&q\mbox{$\,|\,$}p&&\mbox{(commutativity)}\\\
&\quad p\mbox{$\,|\,$}\mbox{\bf 0}&\;\sim_{sp}&p&&\mbox{(identity)}\\\
\end{array}$

As we have shown that parallel composition is associative (and commutative)
w.r.t. $\sim_{sp}$, we sometimes use the $n$-ary version of this operator.
Hence, we shorten the term
$(\ldots(p_{1}\mbox{$\,|\,$}p_{2})\mbox{$\,|\,$}\ldots\mbox{$\,|\,$}p_{n})$ as
$\Pi_{i=1}^{n}p_{i}$.

In order to define some algebraic properties for the restriction operator, we
assume the reader familiar with the notion of free names of a process $p$
(denoted by ${\it fn}(p)$), bound names (denoted by ${\it bn}(p)$) and
syntactic substitution of action $b$ in place of $a$ within $p$, denoted by
$p\mbox{$\\{b/a\\}$}$ (see, e.g., [13, 30] for introductory books on these
topics).

###### Proposition 18

(Laws of the restriction operator) For each process $p\in\mathcal{P}_{FNM}$
and for all $a,b\in\mathcal{L}$, the following hold:

$\begin{array}[]{lrclllll}&\mbox{$({\bf\nu}a)$}p&\sim_{sp}&p&\mbox{if
$a\not\in\mbox{{\it fn}}(p)$}&\mbox{(remove)}\\\
&\mbox{$({\bf\nu}a)$}(\mbox{$({\bf\nu}b)$}p)&\sim_{sp}&\mbox{$({\bf\nu}b)$}(\mbox{$({\bf\nu}a)$}p)&\mbox{if
$a\neq b$}&\mbox{(reorder)}\\\
&\mbox{$({\bf\nu}a)$}p&\sim_{sp}&\mbox{$({\bf\nu}b)$}(p\mbox{$\\{b/a\\}$})&\mbox{if
$b\not\in\mbox{{\it fn}}(p)\cup bn(p)$ }&\mbox{(alpha-conversion)}\\\
\end{array}$

Note that the remove law above implies also the following law:

$\quad\mbox{$({\bf\nu}a)$}(\mbox{$({\bf\nu}a)$}p)\sim_{sp}\mbox{$({\bf\nu}a)$}p$

stating that duplicated application of the restriction operator are
inessential. This law, together with the reorder law, justifies the notational
convention, that we often adopt, of using the restriction operator over a set
of names; e.g., for
$\mbox{$({\bf\nu}a)$}(\mbox{$({\bf\nu}b)$}(\mbox{$({\bf\nu}a)$}p))$, we can
use the notation $\mbox{$({\bf\nu}\\{a,b\\})$}p$.

Now we introduce some laws about the interplay between some operators, related
to manipulation of the preset or of the postset of net transitions. However,
we anticipate that these laws are rather specific, less general and less
elegant than those above. The following example illustrates the issue for the
presets.

###### Example 4

Consider the term
$p=\mbox{$({\bf\nu}a)$}(\mbox{$({\bf\nu}b)$}((\underline{a}.\underline{b}.c.p_{1}\mbox{$\,|\,$}\overline{a}.p_{2})\mbox{$\,|\,$}\overline{b}.p_{3}))$.
The only initial transition performable by $\mbox{$dec$}(p)$ is a three-way
synchronization, labeled $c$, reaching the marking
$((\mbox{$dec$}(p_{1})\oplus\mbox{$dec$}(p_{2})\oplus\mbox{$dec$}(p_{3}))\mbox{$\\{b^{\prime}/b\\}$})\mbox{$\\{a^{\prime}/a\\}$}$.
The same behavior is also possible by the term
$q=\mbox{$({\bf\nu}a)$}(\mbox{$({\bf\nu}b)$}((\underline{b}.\underline{a}.c.p_{1}\mbox{$\,|\,$}\overline{a}.p_{2})\mbox{$\,|\,$}\overline{b}.p_{3}))$,
where the leader process has permuted the two strong prefixes. As a matter of
fact, the restricted actions that occur in the input sequence of the leader
process, that is able to perform a multi-party synchronization in full, are to
be considered as a multiset of inputs rather than a sequence of inputs.
Moreover, also the term
$r=\mbox{$({\bf\nu}a)$}(\mbox{$({\bf\nu}b)$}((\underline{a}.\underline{b}.c.p_{1}\mbox{$\,|\,$}\overline{b}.p_{2})\mbox{$\,|\,$}\overline{a}.p_{3}))$,
where the output guards have been exchanged, is sp-bisimilar to both $p$ and
$q$. The following laws focus on these aspects.  $\Box$

###### Proposition 19

(Laws of the preset) For each $n\geq 2$, for each restriction-free process
$p\in\mathcal{P}_{FNM}$, for each $a_{0},\ldots a_{n}\in\mathcal{L}$, for each
$A\subseteq\mathcal{L}$ such that $\\{a_{1},\ldots a_{n}\\}\subseteq A$
($a_{0}\not\in A$), for each $r\in\mathcal{P}^{grd}_{FNM}$ such that
$fn(r)\cap\\{a_{1},\ldots,a_{n}\\}=\emptyset$, for each restriction-free
process $q\in\mathcal{P}_{FNM}$ such that
$fn(q)\cap\\{a_{1},\ldots,a_{n}\\}=\emptyset$, for each $\delta$ permutation
on $\\{1,\ldots,n\\}$, the following holds:

$\begin{array}[]{lrcrllll}(i)&\mbox{$({\bf\nu}A)$}(((\underline{a}_{n}.\ldots\underline{a}_{1}.a_{0}.p+r)\mbox{$\,|\,$}\Pi_{i=1}^{n}\overline{a}_{i}.p_{i})\mbox{$\,|\,$}q)&\sim_{sp}\\\
&\mbox{$({\bf\nu}A)$}(((\underline{a}_{\delta(n)}.\ldots\underline{a}_{\delta(1)}.a_{0}.p+r)\mbox{$\,|\,$}\Pi_{i=1}^{n}\overline{a}_{i}.p_{i})\mbox{$\,|\,$}q)\\\
\\\
(ii)&\mbox{$({\bf\nu}A)$}(((\underline{a}_{n}.\ldots\underline{a}_{1}.a_{0}.p+r)\mbox{$\,|\,$}\Pi_{i=1}^{n}\overline{a}_{i}.p_{i})\mbox{$\,|\,$}q)&\sim_{sp}\\\
&\mbox{$({\bf\nu}A)$}(((\underline{a}_{n}.\ldots\underline{a}_{1}.a_{0}.p+r)\mbox{$\,|\,$}\Pi_{i=1}^{n}\overline{a}_{\delta(i)}.p_{i})\mbox{$\,|\,$}q)\\\
\end{array}$

For each $n\geq 1$, for each restriction-free process $p\in\mathcal{P}_{FNM}$,
for each $a_{0},\ldots a_{n}\in\mathcal{L}$, for each $A\subseteq\mathcal{L}$
such that $\\{a_{0},\ldots a_{n}\\}\subseteq A$, for each
$r\in\mathcal{P}^{grd}_{FNM}$ such that
$fn(r)\cap\\{a_{0},\ldots,a_{n}\\}=\emptyset$, for each restriction-free
process $q$ such that $fn(q)\cap\\{a_{0},\ldots,a_{n}\\}=\emptyset$, for each
$\delta$ permutation on $\\{0,\ldots,n\\}$ the following holds:

$\begin{array}[]{lrcrllll}(iii)&\mbox{$({\bf\nu}A)$}(((\underline{a}_{n}.\ldots\underline{a}_{1}.a_{0}.p+r)\mbox{$\,|\,$}\Pi_{i=0}^{n}\overline{a}_{i}.p_{i})\mbox{$\,|\,$}q)&\sim_{sp}\\\
&\mbox{$({\bf\nu}A)$}(((\underline{a}_{\delta(n)}.\ldots\underline{a}_{\delta(1)}.a_{\delta(0)}.p+r)\mbox{$\,|\,$}\Pi_{i=0}^{n}\overline{a}_{i}.p_{i})\mbox{$\,|\,$}q)\\\
\\\
(iv)&\mbox{$({\bf\nu}A)$}(((\underline{a}_{n}.\ldots\underline{a}_{1}.a_{0}.p+r)\mbox{$\,|\,$}\Pi_{i=0}^{n}\overline{a}_{i}.p_{i})\mbox{$\,|\,$}q)&\sim_{sp}\\\
&\mbox{$({\bf\nu}A)$}(((\underline{a}_{n}.\ldots\underline{a}_{1}.a_{0}.p+r)\mbox{$\,|\,$}\Pi_{i=0}^{n}\overline{a}_{\delta(i)}.p_{i})\mbox{$\,|\,$}q)\\\
\end{array}$

Note that in these laws some of the $a_{i}$’s can be the same action. For
instance, the third law above (together with the identity laws for the choice
operator and parallel one), allows us to prove that

$\mbox{$({\bf\nu}\\{a,b\\})$}(((\underline{a}.\underline{b}.a.p\mbox{$\,|\,$}\overline{a}.p_{1})\mbox{$\,|\,$}\overline{b}.p_{2})\mbox{$\,|\,$}\overline{a}.p_{3})\sim_{sp}\mbox{$({\bf\nu}\\{a,b\\})$}(((\underline{a}.\underline{a}.b.p\mbox{$\,|\,$}\overline{a}.p_{1})\mbox{$\,|\,$}\overline{b}.p_{2})\mbox{$\,|\,$}\overline{a}.p_{3}).$

However, these laws of the preset do not ensure that all the possible
equalities of this sort (i.e., related to the preset of a multi-party
transition) can be derived. For instance, considering Example 4, if we assume
that $b$ is not free in $p_{1},p_{2}$ and $p_{3}$, then also
$t=\mbox{$({\bf\nu}a)$}((\underline{a}.\underline{a}.c.p_{1}\mbox{$\,|\,$}\overline{a}.p_{2})\mbox{$\,|\,$}\overline{a}.p_{3})$
is sp-bisimilar to $p$, $q$ and $r$. But a specific law should be added to
those in Proposition 19 to this aim.

In order to show which kind of laws we may single out about the postset of
synchronized transitions, we discuss some simple examples.

###### Example 5

Let us consider the term
$q_{1}=\mbox{$({\bf\nu}a)$}(a.p_{1}\mbox{$\,|\,$}\overline{a}.p_{2})$. The
only initial transition performable by $\mbox{$dec$}(q_{1})$ is a binary,
$\tau$-labeled synchronization, reaching the marking
$((\mbox{$dec$}(p_{1})\oplus\mbox{$dec$}(p_{2}))\mbox{$\\{a^{\prime}/a\\}$}$.
The same behavior is also possible, among many others, by the following terms:

$q_{2}=\mbox{$({\bf\nu}a)$}(a.(p_{1}\mbox{$\,|\,$}p_{2})\mbox{$\,|\,$}\overline{a}.\mbox{\bf
0})$,

$q_{3}=\mbox{$({\bf\nu}a)$}(a.\mbox{\bf
0}\mbox{$\,|\,$}\overline{a}.(p_{1}\mbox{$\,|\,$}p_{2}))$,

$q_{4}=\mbox{$({\bf\nu}a)$}(a.p_{2}\mbox{$\,|\,$}\overline{a}.p_{1})$,

where the continuations of the two synchronizing components of $q_{1}$ can be
mixed up at will. In general, we can state that for each
$p_{1}^{\prime},p_{2}^{\prime}$ such that
$p_{1}^{\prime}\mbox{$\,|\,$}p_{2}^{\prime}\sim_{sp}p_{1}\mbox{$\,|\,$}p_{2}$,
also
$q=\mbox{$({\bf\nu}a)$}(a.p_{1}^{\prime}\mbox{$\,|\,$}\overline{a}.p_{2}^{\prime})$
is sp-bisimilar to $q_{1}$. This idea can be generalized by the following
laws.  $\Box$

###### Proposition 20

(Laws of the postset-1) For each $n\geq 1$, for all restriction-free processes
$p,p_{i}\in\mathcal{P}_{FNM}$ for $i=1,\ldots,n$, for all $a_{0},\ldots
a_{n}\in\mathcal{L}$, for each $A\subseteq\mathcal{L}$ such that
$\\{a_{1},\ldots a_{n}\\}\subseteq A$ ($a_{0}\not\in A$), for each
$r\in\mathcal{P}^{grd}_{FNM}$ such that
$fn(r)\cap\\{a_{1},\ldots,a_{n}\\}=\emptyset$, for each restriction-free
process $q\in\mathcal{P}_{FNM}$ such that
$fn(q)\cap\\{a_{1},\ldots,a_{n}\\}=\emptyset$, for all restriction-free
$p^{\prime},p^{\prime}_{i}\in\mathcal{P}_{FNM}$ for $i=1,\ldots,n$, such that
$p\mbox{$\,|\,$}\Pi_{i=1}^{n}p_{i}\sim_{sp}p^{\prime}\mbox{$\,|\,$}\Pi_{i=1}^{n}p^{\prime}_{i}$,
the following holds:

$\begin{array}[]{lrcrllll}(i)&\mbox{$({\bf\nu}A)$}(((\underline{a}_{n}.\ldots\underline{a}_{1}.a_{0}.p+r)\mbox{$\,|\,$}\Pi_{i=1}^{n}\overline{a}_{i}.p_{i})\mbox{$\,|\,$}q)&\sim_{sp}\\\
&\mbox{$({\bf\nu}A)$}(((\underline{a}_{n}.\ldots\underline{a}_{1}.a_{0}.p^{\prime}+r)\mbox{$\,|\,$}\Pi_{i=1}^{n}\overline{a}_{i}.p^{\prime}_{i})\mbox{$\,|\,$}q)\\\
\end{array}$

For each $n\geq 0$, for all restriction-free processes
$p,p_{i}\in\mathcal{P}_{FNM}$ for $i=0,\ldots,n$, for all $a_{0},\ldots
a_{n}\in\mathcal{L}$, for each $A\subseteq\mathcal{L}$ such that
$\\{a_{0},\ldots a_{n}\\}\subseteq A$, for each $r\in\mathcal{P}^{grd}_{FNM}$
such that $fn(r)\cap\\{a_{0},\ldots,a_{n}\\}=\emptyset$, for each restriction-
free process $q\in\mathcal{P}_{FNM}$ such that
$fn(q)\cap\\{a_{0},\ldots,a_{n}\\}=\emptyset$, for all restriction-free
processes $p^{\prime},p^{\prime}_{i}\in\mathcal{P}_{FNM}$ for $i=0,\ldots,n$,
such that
$p\mbox{$\,|\,$}\Pi_{i=0}^{n}p_{i}\sim_{sp}p^{\prime}\mbox{$\,|\,$}\Pi_{i=0}^{n}p^{\prime}_{i}$,
the following holds:

$\begin{array}[]{lrcrllll}(ii)&\mbox{$({\bf\nu}A)$}(((\underline{a}_{n}.\ldots\underline{a}_{1}.a_{0}.p+r)\mbox{$\,|\,$}\Pi_{i=0}^{n}\overline{a}_{i}.p_{i})\mbox{$\,|\,$}q)&\sim_{sp}\\\
&\mbox{$({\bf\nu}A)$}(((\underline{a}_{n}.\ldots\underline{a}_{1}.a_{0}.p^{\prime}+r)\mbox{$\,|\,$}\Pi_{i=0}^{n}\overline{a}_{i}.p^{\prime}_{i})\mbox{$\,|\,$}q)\\\
\end{array}$

###### Remark 4

Note that the laws (ii) and (iv) of Proposition 19 are a special case of the
above laws (i) and (ii), respectively. As a matter of fact, when
$p=p^{\prime}$ and the sequence $p_{1}^{\prime},\ldots,p_{n}^{\prime}$ is just
a permutation of the sequence $p_{1},\ldots,p_{n}$, we have that law (i) above
is the same as law (ii) of Proposition 19. Similarly, one can argue that law
(iv) of Proposition 19 is a special case of law (ii) above.  $\Box$

###### Example 6

The free mix up operation discussed in the previous example can be done only
if the initial synchronization is unique, so that the system is deterministic
w.r.t. the synchronizations. In general, this is not the case. For instance,
consider the term
$q_{1}=\mbox{$({\bf\nu}a)$}((a.p_{1}+a.p_{2})\mbox{$\,|\,$}\overline{a}.p_{3})$.
There are two initial $\tau$-labeled synchronizations performable by
$\mbox{$dec$}(q_{1})$, reaching either the marking
$((\mbox{$dec$}(p_{1})\oplus\mbox{$dec$}(p_{3}))\mbox{$\\{a^{\prime}/a\\}$}$
or the marking
$((\mbox{$dec$}(p_{2})\oplus\mbox{$dec$}(p_{3}))\mbox{$\\{a^{\prime}/a\\}$}$.
The same behavior is also possible by the following term:

$q_{2}=\mbox{$({\bf\nu}a)$}((a.(p_{1}\mbox{$\,|\,$}p_{3})+a.(p_{2}\mbox{$\,|\,$}p_{3}))\mbox{$\,|\,$}\overline{a}.\mbox{\bf
0})$

where the continuations of the unique output subprocess is moved to the
continuation of the two, alternative input subprocesses. In general, we can
state that for each $r_{1},r_{2}$ such that
$p_{3}\sim_{sp}r_{1}\mbox{$\,|\,$}r_{2}$, also
$q_{2}=\mbox{$({\bf\nu}a)$}((a.(r_{1}\mbox{$\,|\,$}p_{1})+a.(r_{1}\mbox{$\,|\,$}p_{2}))\mbox{$\,|\,$}\overline{a}.r_{2})$
is structure-preserving bisimilar to $q_{1}$. This idea can be generalized by
the following laws.  $\Box$

###### Proposition 21

(Laws of the postset-2) For each $n\geq 1$, for all $a_{0},\ldots
a_{n}\in\mathcal{L}$, for each $A\subseteq\mathcal{L}$ such that
$\\{a_{1},\ldots a_{n}\\}\subseteq A$ ($a_{0}\not\in A$), for each guarded
process $v\in\mathcal{P}^{grd}_{FNM}$ such that
$fn(v)\cap\\{a_{1},\ldots,a_{n}\\}=\emptyset$, for each restriction-free
process $q\in\mathcal{P}_{FNM}$ such that
$fn(q)\cap\\{a_{1},\ldots,a_{n}\\}=\emptyset$, for each $k\geq 1$, for all
restriction-free processes $v_{i}\in\mathcal{P}_{FNM}$ for $i=1,\ldots,k$, for
all restriction-free processes $p_{i}\in\mathcal{P}_{FNM}$ for $i=1,\ldots,n$,
for all restriction-free processes $r,r_{i}\in\mathcal{P}_{FNM}$ for
$i=1,\ldots,n$ such that
$\Pi_{i=1}^{n}p_{i}\sim_{sp}r\mbox{$\,|\,$}\Pi_{i=1}^{n}r_{i}$, the following
holds:

$\begin{array}[]{lrcrllll}(i)&\mbox{$({\bf\nu}A)$}(((\sum_{i=1}^{k}\underline{a}_{n}.\ldots\underline{a}_{1}.a_{0}.v_{i}+v)\mbox{$\,|\,$}\Pi_{i=1}^{n}\overline{a}_{i}.p_{i})\mbox{$\,|\,$}q)&\sim_{sp}\\\
&\mbox{$({\bf\nu}A)$}(((\sum_{i=1}^{k}\underline{a}_{n}.\ldots\underline{a}_{1}.a_{0}.(v_{i}\mbox{$\,|\,$}r)+v)\mbox{$\,|\,$}\Pi_{i=1}^{n}\overline{a}_{i}.r_{i})\mbox{$\,|\,$}q)\\\
\end{array}$

For each $n\geq 0$, for all $a_{0},\ldots a_{n}\in\mathcal{L}$, for each
$A\subseteq\mathcal{L}$ such that $\\{a_{0},\ldots a_{n}\\}\subseteq A$, for
each guarded process $v\in\mathcal{P}^{grd}_{FNM}$ such that
$fn(v)\cap\\{a_{0},\ldots,a_{n}\\}=\emptyset$, for each restriction-free
process $q\in\mathcal{P}_{FNM}$ such that
$fn(q)\cap\\{a_{0},\ldots,a_{n}\\}=\emptyset$, for each $k\geq 1$, for all
restriction-free processes $v_{i}\in\mathcal{P}_{FNM}$ for $i=1,\ldots,k$, for
all restriction-free processes $p_{i}\in\mathcal{P}_{FNM}$ for $i=0,\ldots,n$,
for each restriction-free processes $r,r_{i}\in\mathcal{P}_{FNM}$ for
$i=0,\ldots,n$, such that
$\Pi_{i=0}^{n}p_{i}\sim_{sp}r\mbox{$\,|\,$}\Pi_{i=0}^{n}r_{i}$, the following
holds:

$\begin{array}[]{lrcrllll}(ii)&\mbox{$({\bf\nu}A)$}(((\sum_{i=1}^{k}\underline{a}_{n}.\ldots\underline{a}_{1}.a_{0}.v_{i}+v)\mbox{$\,|\,$}\Pi_{i=0}^{n}\overline{a}_{i}.p_{i})\mbox{$\,|\,$}q)&\sim_{sp}\\\
&\mbox{$({\bf\nu}A)$}(((\sum_{i=1}^{k}\underline{a}_{n}.\ldots\underline{a}_{1}.a_{0}.(v_{i}\mbox{$\,|\,$}r)+v)\mbox{$\,|\,$}\Pi_{i=0}^{n}\overline{a}_{i}.r_{i})\mbox{$\,|\,$}q)\\\
\end{array}$

###### Example 7

The partial mix up operation discussed in the previous example can be easily
done only if the output is unique. In general, no easy mix up can be
performed. For instance, consider the term
$q_{1}=\mbox{$({\bf\nu}a)$}((a.p_{1}+a.p_{2})\mbox{$\,|\,$}(\overline{a}.p_{3}+\overline{a}.p_{4}))$.
Note that there are four initial synchronizations performable by
$\mbox{$dec$}(q_{1})$. However, in this case, as both occurrences of the input
action $a$ can be synchronized with both occurrences of the output action
$\overline{a}$, there is no easy mix up of the continuations: it is necessary
that $p_{1}$ and $p_{2}$ (or $p_{3}$ and $p_{4}$) share some behaviorally
equivalent subcomponent. E.g., if $p_{1}\sim_{sp}r\mbox{$\,|\,$}r_{1}$ and
$p_{2}\sim_{sp}r\mbox{$\,|\,$}r_{2}$, then
$q_{2}=\mbox{$({\bf\nu}a)$}((a.r_{1}+a.r_{2})\mbox{$\,|\,$}(\overline{a}.(r\mbox{$\,|\,$}p_{3})+\overline{a}.(r\mbox{$\,|\,$}p_{4})))$
is sp-bisimilar to $q_{1}$. Similarly, if $p_{3}\sim_{sp}r\mbox{$\,|\,$}r_{3}$
and $p_{4}\sim_{sp}r\mbox{$\,|\,$}r_{4}$, then it is not difficult to see that
also
$q_{3}=\mbox{$({\bf\nu}a)$}((a.(p_{1}\mbox{$\,|\,$}r)+a.(p_{2}\mbox{$\,|\,$}r))\mbox{$\,|\,$}(\overline{a}.r_{3}+\overline{a}.r_{4}))$
is sp-bisimilar to $q_{1}$. Specific laws should be added to deal with such
situations.  $\Box$

The examples above give evidence that in order to capture more and more
equalities, more and more (rather cumbersome) laws must be added. In fact, we
think that it is not possible to capture all the algebraic laws that hold for
sp-bisimilarity.

##  6 Sound Axiomatization

In this section we provide a sound, but incomplete, axiomatization of
structure-preserv-ing bisimulation equivalence over FNM. For simplicity’s
sake, the syntactic definition of open FNM (cf. Definition 15) is assumed here
flattened, with only one syntactic category, but we require that each ground
instantiation of an axiom must respect the syntactic definition of (closed)
FNM given in Section 3. This means that we can write the axiom
$x+(y+z)=(x+y)+z$ (these terms cannot be written in open FNM according to
Definition 15), but it is invalid to instantiate it to $C+(a.\mbox{\bf
0}+b.\mbox{\bf 0}\mbox{$\,|\,$}\mbox{\bf 0})=(C+a.\mbox{\bf 0})+(b.\mbox{\bf
0}\mbox{$\,|\,$}\mbox{\bf 0})$ because these are not legal FNM processes (the
constant $C$ and the parallel process $b.\mbox{\bf 0}\mbox{$\,|\,$}\mbox{\bf
0}$ cannot be used as summands).

The set of axioms are outlined in Tables 7 and 8. We call $E$ the set of
axioms $\\{$A1, A2, A3, A4, S1, S2, S3, C1, C2, P1, P2, P3, R1, R2, R3, Pr1,
Pr2, Ps1, Ps2, Ps3, Ps4$\\}$. By the notation $E\vdash p=q$ we mean that there
exists an equational deduction proof of the equality $p=q$, by using the
axioms in $E$. Besides the usual equational deduction rules of reflexivity,
symmetry, transitivity, substitutivity and instantiation (see, e.g., [13] for
an introductory book on the subject), in order to deal with constants we need
also the following recursion congruence rule:

$\frac{p=q\;\wedge\;A\doteq p\\{A/x\\}\;\wedge\;B\doteq q\\{B/x\\}}{A=B}$

Let us first comment on the axioms in Table 7, which are more standard and
also already appeared in the literature in some form.

The axioms A1-A4 are the usual axioms for choice [29, 20] where, however,
A3-A4 have the side condition $x\neq\mbox{\bf 0}$; hence, it is not possible
to prove $E\vdash\mbox{\bf 0}+\mbox{\bf 0}=\mbox{\bf 0}$, as expected, because
these two terms have a completely different semantics; in fact, no other
sequential process $p$ can be equated to 0.

The axioms S1-S3 are the axioms for strong prefixing, similar to those
originally proposed in [12]. Note that the annihilation axiom S3 requires that
$x$ is 0 or can be proved equal to a stuck place, such as $\mbox{\bf
0}+\mbox{\bf 0}$. Note also that these axioms are actually a finite collection
of axioms, one for each input prefix $a$: since the set $\mathcal{L}$ is
finite, the instances of S1-S3 are finitely many.

The conditional axioms (or inference rules) C1-C2 are about process constants,
originally introduced in [15] and inspired to those for the fixpoint operator
of finite-state CCS [20]. Note that axiom C1 summarizes the algebraic laws
stuck and unfolding of Proposition 16 (cf. Remark 3). Note also that these
conditional axioms are actually a finite collection of axioms, one for each
constant definition: since the set $\mathcal{C}$ of process constants is
finite, the instances of C1-C2 are finitely many.

The axioms P1-P3 are the usual ones for parallel composition. They are typical
for non-interleaving behavioral congruences (see, e.g., [15, 17]), while they
are not used for standard bisimilarity, in favor of the so-called expansion
theorem (or interleaving law) [21, 13], according to which parallel
composition can be seen as a derived operator expressible by a suitable
combination of the operators of action prefixing and choice.

Finally, we have axioms R1-R3 for the restriction operator. These axioms occur
in many contexts as ingredients of suitable structural congruences for the
operational interleaving semantics (defined on labeled transitions systems) of
some process algebras, notably the $\pi$-calculus (see, e.g., [26, 30]) or
Multi-CCS [13].

$\begin{array}[]{llrcll}{\bf
A1}&\;\;\mbox{Associativity}&\;\;x+(y+z)&=&(x+y)+z&\\\ {\bf
A2}&\;\;\mbox{Commutativity}&\;\;x+y&=&y+x&\\\ {\bf
A3}&\;\;\mbox{Identity}&\;\;x+\mbox{\bf 0}&=&x&\quad\mbox{ if $x\neq\mbox{\bf
0}$}\\\ {\bf A4}&\;\;\mbox{Idempotence}&\;\;x+x&=&x&\quad\mbox{ if
$x\neq\mbox{\bf 0}$}\\\ \end{array}$

$\begin{array}[]{llrcll}{\bf
S1}&\;\;\mbox{Distribution}&\;\;\underline{a}.(x+y)&=&\underline{a}.x+\underline{a}.y&\\\
{\bf S2}&\;\;\mbox{Absorption}&\;\;\underline{a}.\tau.x&=&a.x&\\\ {\bf
S3}&\;\;\mbox{Annihilation}&\;\;\underline{a}.x&=&\mbox{\bf 0}+\mbox{\bf
0}&\quad\mbox{ if $x=\mbox{\bf 0}$ or $x=\mbox{\bf 0}+\mbox{\bf 0}$}\\\
\end{array}$

$\begin{array}[]{llrcllll}{\bf C1}&\;\;\mbox{Unfolding}&\;\;\mbox{if $C\doteq
p$,}&\mbox{then}&\mbox{$C=p+\mbox{\bf 0}$}&\\\ {\bf
C2}&\;\;\mbox{Folding}&\;\;\mbox{if $C\doteq
p\\{C/x\\}\;\wedge\;q=p\\{q/x\\}$,}&\mbox{then}&\mbox{$C=q$}&\\\ \end{array}$

$\begin{array}[]{llrcll}{\bf
P1}&\;\;\mbox{Associativity}&\;\;x\mbox{$\,|\,$}(y\mbox{$\,|\,$}z)&=&(x\mbox{$\,|\,$}y)\mbox{$\,|\,$}z&\\\
{\bf P2}&\;\;\mbox{Commutativity}&\;\;x\mbox{$\,|\,$}y&=&y\mbox{$\,|\,$}x&\\\
{\bf P3}&\;\;\mbox{Identity}&\;\;x\mbox{$\,|\,$}\mbox{\bf 0}&=&x&\\\
\end{array}$

$\begin{array}[]{llrcll}{\bf
R1}&\;\;\mbox{Remove}&\;\;\mbox{$({\bf\nu}a)$}x&=&x&\quad\mbox{ if $a\not\in
fn(x)$}\\\ {\bf
R2}&\;\;\mbox{Reorder}&\;\;\mbox{$({\bf\nu}a)$}(\mbox{$({\bf\nu}b)$}x)&=&\mbox{$({\bf\nu}b)$}(\mbox{$({\bf\nu}a)$}x)&\quad\mbox{
if $a\neq b$}\\\ {\bf
R3}&\;\;\mbox{$\alpha$-conversion}&\;\;\mbox{$({\bf\nu}a)$}x&=&\mbox{$({\bf\nu}b)$}(x\mbox{$\\{b/a\\}$})&\quad\mbox{
if $b\not\in fn(x)\cup bn(x)$}\\\ \end{array}$

Table 7: Some axioms for structure-preserving bisimulation equivalence

Let us now comment on the axioms in Table 8, which are new, to the best of our
knowledge. These axioms are all conditional and, moreover, are actually
infinitary schemata due to the potentially unbounded number of participants to
the multi-party synchronization they model. In fact, they are parametric in
$n$.

Axioms Pr1-Pr2 are related to the laws of the preset, discussed in Proposition
19, while Ps1-Ps4 are the axiomatic counterpart of the laws in Proposition 20
and 21. Note that we have omitted the axioms related to laws (ii) and (iv) in
Proposition 19 because these axioms would have been redundant (cf. Remark 4).

$\begin{array}[]{llrcll}{\bf Pr1}&\mbox{if $\\{a_{1},\ldots,a_{n}\\}\subseteq
A$, $a_{0}\not\in A$, $fn(y)\cap\\{a_{1},\ldots,a_{n}\\}=\emptyset$,
$fn(z)\cap\\{a_{1},\ldots,a_{n}\\}=\emptyset$ and}&\\\ &\mbox{$\delta$ a
permutation on $\\{1,\ldots,n\\}$, then}\\\
&\quad\mbox{$({\bf\nu}A)$}(((\underline{a}_{n}.\ldots\underline{a}_{1}.a_{0}.x+y)\mbox{$\,|\,$}\Pi_{i=1}^{n}\overline{a}_{i}.x_{i})\mbox{$\,|\,$}z)=\\\
&\qquad\qquad\mbox{$({\bf\nu}A)$}(((\underline{a}_{\delta(n)}.\ldots\underline{a}_{\delta(1)}.a_{0}.x+y)\mbox{$\,|\,$}\Pi_{i=1}^{n}\overline{a}_{i}.x_{i})\mbox{$\,|\,$}z)\\\
{\bf Pr2}&\mbox{if $\\{a_{0},\ldots,a_{n}\\}\subseteq A$,
$fn(y)\cap\\{a_{0},\ldots,a_{n}\\}=\emptyset$,
$fn(z)\cap\\{a_{0},\ldots,a_{n}\\}=\emptyset$ and}&\\\ &\mbox{$\delta$ a
permutation on $\\{0,\ldots,n\\}$, then}\\\
&\quad\mbox{$({\bf\nu}A)$}(((\underline{a}_{n}.\ldots\underline{a}_{1}.a_{0}.x+y)\mbox{$\,|\,$}\Pi_{i=0}^{n}\overline{a}_{i}.x_{i})\mbox{$\,|\,$}z)=\\\
&\qquad\qquad\mbox{$({\bf\nu}A)$}(((\underline{a}_{\delta(n)}.\ldots\underline{a}_{\delta(1)}.a_{\delta(0)}.x+y)\mbox{$\,|\,$}\Pi_{i=0}^{n}\overline{a}_{i}.x_{i})\mbox{$\,|\,$}z)\\\
\end{array}$

$\begin{array}[]{llrcllll}{\bf Ps1}&\mbox{if
$\\{a_{1},\ldots,a_{n}\\}\subseteq A$, $a_{0}\not\in A$,
$fn(y)\cap\\{a_{1},\ldots,a_{n}\\}=\emptyset$,
$fn(z)\cap\\{a_{1},\ldots,a_{n}\\}=\emptyset$ and}&\\\
&\mbox{$x\mbox{$\,|\,$}\Pi_{i=1}^{n}x_{i}=x^{\prime}\mbox{$\,|\,$}\Pi_{i=1}^{n}x^{\prime}_{i}$,
then}\\\
&\quad\mbox{$({\bf\nu}A)$}(((\underline{a}_{n}.\ldots\underline{a}_{1}.a_{0}.x+y)\mbox{$\,|\,$}\Pi_{i=1}^{n}\overline{a}_{i}.x_{i})\mbox{$\,|\,$}z)=\\\
&\qquad\qquad\mbox{$({\bf\nu}A)$}(((\underline{a}_{n}.\ldots\underline{a}_{1}.a_{0}.x^{\prime}+y)\mbox{$\,|\,$}\Pi_{i=1}^{n}\overline{a}_{i}.x^{\prime}_{i})\mbox{$\,|\,$}z)\\\
{\bf Ps2}&\mbox{if $\\{a_{0},\ldots,a_{n}\\}\subseteq A$,
$fn(y)\cap\\{a_{0},\ldots,a_{n}\\}=\emptyset$,
$fn(z)\cap\\{a_{0},\ldots,a_{n}\\}=\emptyset$ and}&\\\
&\mbox{$x\mbox{$\,|\,$}\Pi_{i=0}^{n}x_{i}=x^{\prime}\mbox{$\,|\,$}\Pi_{i=0}^{n}x^{\prime}_{i}$,
then}\\\
&\quad\mbox{$({\bf\nu}A)$}(((\underline{a}_{n}.\ldots\underline{a}_{1}.a_{0}.x+y)\mbox{$\,|\,$}\Pi_{i=0}^{n}\overline{a}_{i}.x_{i})\mbox{$\,|\,$}z)=\\\
&\qquad\qquad\mbox{$({\bf\nu}A)$}(((\underline{a}_{n}.\ldots\underline{a}_{1}.a_{0}.x^{\prime}+y)\mbox{$\,|\,$}\Pi_{i=0}^{n}\overline{a}_{i}.x^{\prime}_{i})\mbox{$\,|\,$}z)\\\
{\bf Ps3}&\mbox{if $\\{a_{1},\ldots,a_{n}\\}\subseteq A$, $a_{0}\not\in A$,
$fn(y)\cap\\{a_{1},\ldots,a_{n}\\}=\emptyset$,
$fn(z)\cap\\{a_{1},\ldots,a_{n}\\}=\emptyset$ and}&\\\
&\mbox{$\Pi_{i=1}^{n}x_{i}=w\mbox{$\,|\,$}\Pi_{i=1}^{n}w_{i}$, then}\\\
&\quad\mbox{$({\bf\nu}A)$}(((\sum_{j=1}^{k}\underline{a}_{n}.\ldots\underline{a}_{1}.a_{0}.y_{j}+y)\mbox{$\,|\,$}\Pi_{i=1}^{n}\overline{a}_{i}.x_{i})\mbox{$\,|\,$}z)=\\\
&\qquad\qquad\mbox{$({\bf\nu}A)$}(((\sum_{j=1}^{k}\underline{a}_{n}.\ldots\underline{a}_{1}.a_{0}.(y_{j}\mbox{$\,|\,$}w)+y)\mbox{$\,|\,$}\Pi_{i=1}^{n}\overline{a}_{i}.w_{i})\mbox{$\,|\,$}z)\\\
{\bf Ps4}&\mbox{if $\\{a_{0},\ldots,a_{n}\\}\subseteq A$,
$fn(y)\cap\\{a_{0},\ldots,a_{n}\\}=\emptyset$,
$fn(z)\cap\\{a_{0},\ldots,a_{n}\\}=\emptyset$ and}&\\\
&\mbox{$\Pi_{i=0}^{n}x_{i}=w\mbox{$\,|\,$}\Pi_{i=0}^{n}w_{i}$, then}\\\
&\quad\mbox{$({\bf\nu}A)$}(((\sum_{j=1}^{k}\underline{a}_{n}.\ldots\underline{a}_{1}.a_{0}.y_{j}+y)\mbox{$\,|\,$}\Pi_{i=0}^{n}\overline{a}_{i}.x_{i})\mbox{$\,|\,$}z)=\\\
&\qquad\qquad\mbox{$({\bf\nu}A)$}(((\sum_{j=1}^{k}\underline{a}_{n}.\ldots\underline{a}_{1}.a_{0}.(y_{j}\mbox{$\,|\,$}w)+y)\mbox{$\,|\,$}\Pi_{i=0}^{n}\overline{a}_{i}.w_{i})\mbox{$\,|\,$}z)\\\
\end{array}$

Table 8: Some further conditional axiom schemata for structure-preserving
bisimilarity

###### Theorem 6.1

(Soundness) For every $p,q\in\mathcal{P}_{FNM}$, if $E\vdash p=q$, then
$p\sim_{sp}q$.

Of course, this axiomatization is incomplete, as illustrated, e.g., in Example
7.

###### Example 8

Let us consider the two unbounded producer/consumer systems in Figure 4. It is
easy to see that the net semantics of
$\mbox{$({\bf\nu}a)$}(P_{1}\mbox{$\,|\,$}C_{1})$, with $P_{1}\doteq
prod.(P_{1}\mbox{$\,|\,$}D_{1})$, $D_{1}\doteq\overline{a}.\mbox{\bf 0}$,
$C_{1}\doteq\underline{a}.del.C_{1}^{\prime}$ and $C_{1}^{\prime}\doteq
cons.C_{1}$, is a net isomorphic to that on the left, while the net semantics
of $\mbox{$({\bf\nu}b)$}(P_{2}\mbox{$\,|\,$}C_{2})$, with $P_{2}\doteq
prod.(P_{2}\mbox{$\,|\,$}D_{2}^{\prime})+prod.(P_{2}\mbox{$\,|\,$}D_{2}^{\prime\prime})$,
$D_{2}^{\prime}\doteq\overline{b}.\mbox{\bf 0}$,
$D_{2}^{\prime\prime}\doteq\overline{b}.\mbox{\bf 0}$,
$C_{2}\doteq\underline{b}.del.C_{2}^{\prime}$ and $C_{2}^{\prime}\doteq
cons.C_{2}$, is a net isomorphic to that on the right.

By using the axioms in $E$, it is possible to equate these two terms. First of
all, by axiom R3, we get that $\mbox{$({\bf\nu}a)$}(P_{1}\mbox{$\,|\,$}C_{1})$
is equal to
$\mbox{$({\bf\nu}b)$}((P_{1}\mbox{$\,|\,$}C_{1})\mbox{$\\{b/a\\}$})$, so that,
by applying the substitution, the resulting term is
$\mbox{$({\bf\nu}b)$}(P_{1_{\mbox{$\\{b/a\\}$}}}\mbox{$\,|\,$}C_{1_{\mbox{$\\{b/a\\}$}}})$,
with

$\begin{array}[]{rcllll}P_{1_{\mbox{$\\{b/a\\}$}}}&\doteq&prod.(P_{1_{\mbox{$\\{b/a\\}$}}}\mbox{$\,|\,$}D_{1_{\mbox{$\\{b/a\\}$}}})&\quad
D_{1_{\mbox{$\\{b/a\\}$}}}&\doteq&\overline{b}.\mbox{\bf 0}\\\
C_{1_{\mbox{$\\{b/a\\}$}}}&\doteq&\underline{b}.del.C_{1_{\mbox{$\\{b/a\\}$}}}^{\prime}&\quad
C_{1_{\mbox{$\\{b/a\\}$}}}^{\prime}&\doteq&cons.C_{1_{\mbox{$\\{b/a\\}$}}}.\\\
\end{array}$

Now, by recursion congruence, we get that
$D_{2}^{\prime}=D_{2}^{\prime\prime}$, so that, by substitutivity, we get
$prod.(P_{2}\mbox{$\,|\,$}D_{2}^{\prime})=prod.(P_{2}\mbox{$\,|\,$}D_{2}^{\prime\prime})$,
and so, by axiom A4, we get
$prod.(P_{2}\mbox{$\,|\,$}D_{2}^{\prime})+prod.(P_{2}\mbox{$\,|\,$}D_{2}^{\prime})=prod.(P_{2}\mbox{$\,|\,$}D_{2}^{\prime})$.
Let us define a new constant $P_{2}^{\prime}\doteq
prod.(P_{2}^{\prime}\mbox{$\,|\,$}D_{2}^{\prime})$; clearly, by recursion
congruence, $P_{2}=P_{2}^{\prime}$. Again, by recursion congruence, we also
have that $D_{1_{\mbox{$\\{b/a\\}$}}}=D_{2}^{\prime}$, so that
$prod.(x\mbox{$\,|\,$}D_{1_{\mbox{$\\{b/a\\}$}}})=prod.(x\mbox{$\,|\,$}D_{2}^{\prime})$
holds by substitutivity. Hence, by recursion congruence, we get
$P_{1_{\mbox{$\\{b/a\\}$}}}=P_{2}^{\prime}$. By axiom C1, we get
$C_{1_{\mbox{$\\{b/a\\}$}}}=\underline{b}.del.cons.C_{1_{\mbox{$\\{b/a\\}$}}}$
as well as $C_{2}=\underline{b}.del.cons.C_{2}$, so that, by recursion
congruence, we get $C_{1_{\mbox{$\\{b/a\\}$}}}=C_{2}$. Then, by
substitutivity,
$\mbox{$({\bf\nu}b)$}(P_{1_{\mbox{$\\{b/a\\}$}}}\mbox{$\,|\,$}C_{1_{\mbox{$\\{b/a\\}$}}})=\mbox{$({\bf\nu}b)$}(P_{2}\mbox{$\,|\,$}C_{2})$,
so that, by transitivity, we get
$\mbox{$({\bf\nu}a)$}(P_{1}\mbox{$\,|\,$}C_{1})=\mbox{$({\bf\nu}b)$}(P_{2}\mbox{$\,|\,$}C_{2})$.
$\Box$

##  7 Conclusion

Structure-preserving bisimulation [11] is a very intuitive, rather manageable,
truly concurrent behavioral relation, whose process-oriented characterization
is causal-net bisimilarity [11, 17], a behavioral equivalence fully respecting
causality and the branching structure of systems.

The decidability of sp-bisimilarity over finite (unbounded) P/T nets is an
open problem, because the negative observation in [8] does not apply to it.
Nonetheless, structure-preserving bisimilarity is decidable on bounded nets in
exponential time [4]. In fact, the set of reachable markings are finitely many
for a bounded net, and the set of linkings definable on a pair of markings of
equal size $k$ has size $k!$. Hence, there are finitely many relations (that
are all finite) composed of linkings, and it is enough to exhaustively check
whether each of them is a structure-preserving bisimulation and, in the
positive case, to check whether it contains a linking projected on the two
initial markings of interest.

Note that the class of bounded finite P/T nets (i.e., the class onto which sp-
bisimilarity is decidable) is much larger than the class of nets that is used
to give semantics to regular CCS [21, 13] (also called RCS in [14]), because
these process terms give origin to finite P/T nets whose transitions have
preset of size 1 or 2, and if the preset size is 1, then its postset size is 1
at most, while if the preset size is 2, then its label is $\tau$ and the
postset size is 2 at most.

Structure-preserving bisimilarity is decidable on BPP nets (i.e., nets whose
transitions have preset of size 1), because on this class of nets it coincides
with team bisimilarity [15, 17], which is decidable in polynomial time.

Van Glabbeek [11] argued that structure-preserving bisimilarity is the most
appropriate behavioral equivalence for Petri nets, as it is the only one
respecting a list of desirable requirements he proposed. Among these, there is
‘compositionality’, up to structure-preserving bisimilarity, of the operators
(recursion not considered) of the process algebra CCSP, that Olderog proposed
in his monograph [24] and equipped with a safe net (i.e., in each reachable
marking each place may contain one token at most) semantics. In this paper we
have complemented his result by proving that structure-preserving bisimilarity
can be used to give a compositional semantics of the process algebra FNM [14],
which truly represents all (and only) the finite P/T nets, up to isomorphism.
In this way, we have obtained for the first time a compositional semantics,
fully respecting causality and the branching structure of systems, for the
class of all the finite P/T Petri nets.

It is interesting to observe [14] that also the coarser step bisimilarity [23]
is a congruence for all the FNM operators, while interleaving bisimilarity is
not a congruence for the FNM operator of parallel composition, so that, in
order to give a satisfactory account of this process algebra, a non-
interleaving behavioral semantics is strictly necessary. Since structure-
preserving bisimilarity may appear even too concrete, as it may fail to equate
markings generating the same causal nets (cf. the definition of i-causal net
bisimilarity in [4]), a challenging open problem is to see whether it is
possible to define a compositional semantics for some other behavioral
equivalence in between step bisimilarity (a bit too abstract) and structure-
preserving bisimilarity (a bit too concrete).

To the best of our knowledge, algebraic properties of a truly concurrent
behavioral equivalence for a calculus semantically richer than BPP444BPP is
the acronym of Basic Parallel Processes [5], a simple CCS [21, 13] subcalculus
(without the restriction operator) whose processes cannot communicate. In [14]
a variant of BPP, which requires guarded summation (as in BPPg [5]) and also
that the body of each process constant is guarded (i.e., guarded recursion),
is actually shown to represent all and only the BPP nets, up to net
isomorphism. BPP is a subcalculus of FNM. have never been investigated before.
Here we have shown that for sp-bisimilarity, besides the usual laws for
choice, parallel composition and restriction, we have also less standard laws
related to strong prefixing and process constants, as well as a number of
additional original laws about the interplay between parallel composition and
restriction.

An interesting open problem is to find a complete axiomatization of sp-
bisimilarity over FNM. However, note that such a complete set of axioms might
be available only if sp-bisimilarity is decidable (that is not known yet), and
in such a case, since we use infinitary axiom schemata, it seems that such a
hypothetical set would be infinite.

It is interesting to observe that in the special subcase of BPP [5, 14] the
situation is much better. In fact, [15] describes a finite, sound and
complete, axiomatization of team bisimilarity (which is an alternative
formulation of sp-bisimilarity for BPP nets), while [17] describes a finite,
sound and complete, axiomatization of h-team bisimilarity (which is an
alternative characterization of fully-concurrent bisimilarity [3] for BPP
nets).

## 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] E. Best, R. Devillers,  Sequential and concurrent behavior in Petri net theory,  Theoretical Computer Science 55(1):87-136, 1987.
  * [3] E. Best, R. Devillers, A. Kiehn, L. Pomello,  Concurrent bisimulations in Petri nets,  Acta Inf. 28(3): 231-264, 1991.
  * [4] A. Cesco, R. Gorrieri,  Decidability of two truly concurrent equivalences for finite bounded Petri nets,  CoRR, abs/2104.14856, 2021, https://arxiv.org/abs/2104.14856
  * [5] S. Christensen,  Decidability and Decomposition in Process Algebra,  Ph.D. Thesis, University of Edinburgh (1993)
  * [6] 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.
  * [7] J. Desel, W. Reisig,  Place/Transition Petri nets,  in Lectures on Petri Nets I: Basic Models, LNCS 1491, 122-173, Springer, 1998.
  * [8] J. Esparza,  Decidability and complexity of Petri net problems: An introduction,  Lectures on Petri Nets I: Basic Models,  LNCS 1491, 374-428, Springer, 1998.
  * [9] 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.
  * [10] U. Goltz, W. Reisig,  The non-sequential behaviour of Petri nets,  Information and Control 57(2-3):125-147, 1983.
  * [11] 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.
  * [12] R. Gorrieri, U. Montanari,  Towards hierarchical specification of systems: A proof system for strong prefixing,  Int. J. of Foundations of Computer Science 1(3): 277-293, 1990.
  * [13] R. Gorrieri, C. Versari, Introduction to Concurrency Theory: Transition Systems and CCS, EATCS Texts in Theoretical Computer Science, Springer-Verlag, 2015.
  * [14] R. Gorrieri,  Process Algebras for Petri Nets: The Alphabetization of Distributed Systems,  EATCS Monographs in Computer Science, Springer, 2017.
  * [15] R. Gorrieri,  Team bisimilarity, and its associated modal logic, for BPP nets,  Acta Informatica 58(5):529-569, 2021.
  * [16] R. Gorrieri,  Place bisimilarity is decidable, indeed!,  CoRR, abs/2104.01392, 2021, https://arxiv.org/abs/2104.01392
  * [17] R. Gorrieri,  A study on team bisimulation and h-team bisimulation for BPP nets, Theoretical Computer Science 897:83-113, 2022.
  * [18] P. Janc̆ar,  Undecidability of bisimilarity for Petri nets and some related problems,  Theoretical Computer Science 148(2):281-301, 1995.
  * [19] R.M. Karp, R.E. Miller,  Parallel program schemata,  Journal of Computer and System Sciences 3(2):147-195, 1969.
  * [20] R. Milner.  A complete inference systems for a class of regular behaviors,  J. Comput. System Sci. 28: 439-466, 1984.
  * [21] R. Milner,  Communication and Concurrency,  Prentice-Hall, 1989.
  * [22] A.W. Mazurkiewicz, E. Ochmanski, W. Penczek.  Concurrent systems and inevitability.  Theoretical Computer Science, 64:281–304, 1989.
  * [23] 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.
  * [24] E.R. Olderog,  Nets, Terms and Formulas,  Cambridge Tracts in Theoretical Computer Science 23, Cambridge University Press, 1991.
  * [25] 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.
  * [26] J. Parrow,  An introduction to the $\pi$-calculus,  Chapter 8 of Handbook of Process Algebra (J.A. Bergstra, A. Ponse, S.A. Smolka, eds.), 479-543, Elsevier, 2001.
  * [27] J.L. Peterson,  Petri Net Theory and the Modeling of Systems, Prentice-Hall, 1981.
  * [28] A. Rabinovich, B.A. Trakhtenbrot,  Behavior structures and nets,  Fundamenta Informaticae 11(4):357-404, 1988.
  * [29] A. Salomaa,  Two complete axiom systems for the algebra of regular events,  Journal of the ACM 13(1): 58-169, 1966. doi:10.1145/321312.321326
  * [30] D. Sangiorgi, D. Walker,  The $\pi$-calculus: A Theory of Mobile Processes,  Cambridge University Press, 2001.