=Paper=
{{Paper
|id=Vol-3072/paper12
|storemode=property
|title=Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets (11)
|pdfUrl=https://ceur-ws.org/Vol-3072/paper12.pdf
|volume=Vol-3072
|authors=Arnaldo Cesco,Roberto Gorrieri
|dblpUrl=https://dblp.org/rec/conf/ictcs/CescoG21
}}
==Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets (11) ==
https://ceur-ws.org/Vol-3072/paper12.pdf
Decidability of Two Truly Concurrent Equivalences for
Finite Bounded Petri Nets
Arnaldo Cesco[0000−0002−3417−1890] and Roberto Gorrieri[0000−0001−5502−0584]
arnaldo.cesco@studio.unibo.it roberto.gorrieri@unibo.it ∗
Dipartimento di Informatica — Scienza e Ingegneria
Università di Bologna, Mura A. Zamboni 7, 40127 Bologna, Italy
Abstract. We prove that (strong) fully-concurrent bisimilarity and causal-net
bisimilarity are decidable for finite bounded Petri nets. The proofs are based
on a generalization of the ordered marking proof technique that Vogler used to
demonstrate that (strong) fully-concurrent bisimilarity (or, equivalently, history-
preserving bisimilarity) is decidable on finite safe nets.
Keywords: Behavioral equivalences · True concurrency · Fully-concurrent bisim-
ilarity · Causal-net bisimilarity · Decidability.
1 Introduction
Truly concurrent equivalences, such as fully-concurrent bisimilarity [2] or causal-net
bisimilarity [9,12], have been advocated as very suitable equivalences to compare the
behavior of Petri nets. However, most results about their decidability [19,14,20] are
limited to the class of finite safe nets, i.e., nets whose places can hold one token at most.
Our main aim is to extend some of these decidability proofs to the case of bounded nets.
In his seminal paper [19], Vogler demonstrated that (strong) fully-concurrent bisim-
ilarity is decidable on finite safe nets. His proof is based on an alternative characteriza-
tion of fully-concurrent bisimulation, called ordered marking bisimulation (OM bisimu-
lation, for short), which represents the current global state of the net system as a marking
equipped with a pre-ordering on its tokens, reflecting the causal ordering of the tran-
sitions that produced the tokens. However, the ordered marking idea works well if the
marking is a set (as it is the case for safe nets), and so it is not immediate to generalize
it to bounded nets, whose markings are, in general, multisets. The first contribution of
this paper is the definition of an alternative token game semantics for Petri nets which
is defined according to the individual token philosophy, rather than the collective to-
ken philosophy, as it is customary for Petri nets. This is obtained by representing each
token as a pair (s, i), where s is the name of the place where the token is on, and i is
a natural number (an index) assigned to the token in such a way that different tokens
on the same place have different indexes. In this way, a multiset over the set of places
(i.e., a marking) is turned into a set of indexed places. The main advantage of hav-
ing turned multisets into sets is that Vogler’s ordered marking idea can be used also in
∗ Copyright 2021 for this paper by its authors. Use permitted under Creative Commons Li-
cense Attribution 4.0 International (CC BY 4.0).
2 A. Cesco and R. Gorrieri
this richer context, yielding ordered indexed markings. The second contribution of the
paper is to show that (strong) fully-concurrent bisimulation can be equivalently charac-
terized as a suitable bisimulation over ordered indexed markings, called OIM bisimu-
lation, generalizing the approach by Vogler [19]. An OIM bisimulation is formed by a
set of triples, each composed of two ordered indexed markings and a relation between
these two ordered indexed markings that respects the pre-orders. The decidability of
(strong) fully-concurrent bisimilarity on finite bounded nets follows by observing that
the reachable indexed markings are finitely many, so the ordered indexed markings of
interest are finitely many as well, so that there can only be finitely many candidate rela-
tions (which are all finite) to be OIM-bisimulations. The third contribution of the paper
is to show that our generalization of Vogler’s proof technique can be adapted to prove
the decidability also of another truly concurrent behavioral equivalence, namely causal-
net bisimilarity [12], a behavioral equivalence that coincides with structure-preserving
bisimilarity [9], and which is slightly finer than (strong) fully-concurrent bisimilarity.
The paper is organized as follows. Section 2 recalls the basic definitions about Petri
nets. Section 3 recalls the causal semantics, including the definition of causal-net bisim-
ilarity and (strong) fully-concurrent bisimilarity. Section 4 introduces indexed markings
and the alternative, individual, token game semantics. Section 5 describes indexed or-
dered markings and their properties. Section 6 introduces OIM-bisimulation, proves
that its equivalence coincides with (strong) fully-concurrent bisimilarity and, moreover,
shows that it is decidable. Section 7 hints that also causal-net bisimilarity is decidable.
Finally, Section 8 discusses related literature and some future research. For lack of
space, longer proofs are to be found in the preliminary full version of this article [5].
2 Basic Definitions
Definition 1. (Multiset) Let N be the set of natural numbers. Given a finite set S, a
multiset over S is a function m : S → N. The support set dom(m) of m is {s ∈ S m(s) 6=
0}. The set of all multisets over S, denoted by M (S), is ranged over by m. We write
s ∈ 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 ∑s∈S m(s), i.e., the total number of its elements. A multiset
m such that dom(m) = 0/ is called empty and is denoted by θ . We write m ⊆ m0 if m(s) ≤
m0 (s) for all s ∈ S. Multiset union ⊕ is defined as follows: (m⊕m0 )(s) = m(s)+m0 (s).
Multiset difference is defined as follows: (m1 m2 )(s) = max{m1 (s) − m2 (s), 0}.
The scalar product of a number j with m is the multiset j · m defined as ( j · m)(s) =
j · (m(s)). By si we also denote the multiset with si as its only element. Hence, a multiset
m over S = {s1 , . . . , sn } can be represented as k1 · s1 ⊕ k2 · s2 ⊕ . . . ⊕ kn · sn , where k j =
m(s j ) ≥ 0 for j = 1, . . . , n. 2
Definition 2. (Place/Transition net) A labeled Place/Transition Petri net (P/T net for
short) is a tuple N = (S, A, T ), where
• S is the finite set of places, ranged over by s (possibly indexed),
• A is the finite set of labels, ranged over by ` (possibly indexed), and
• T ⊆ (M (S) \ {θ }) × A × M (S) is the finite set of transitions, ranged over by t
(possibly indexed).
Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets 3
Given a transition t = (m, `, m0 ), we use the notation:
• •t to denote its pre-set m (which cannot be an empty multiset) of tokens to be con-
sumed;
• l(t) for its label `, and
• t • to denote its post-set m0 of tokens to be produced.
l(t)
Hence, transition t can be also represented as •t −→ t • . We also define the flow function
flow : (S × T ) ∪ (T × S) → N as follows: for all s ∈ S, for all t ∈ T , flow(s,t) = •t(s)
and flow(t, s) = t • (s). We will use F to denote the flow relation {(x, y) ∈ (S × T ) ∪ (T ×
S) flow(x, y) > 0}. Finally, we define pre-sets and post-sets also for places as follows:
• s = {t ∈ T s ∈ t • } and s• = {t ∈ T s ∈ •t}. 2
In the graphical description of finite P/T nets, places (represented as circles) and
transitions (represented as boxes) are connected by directed arcs. The arcs may be la-
beled with the number representing how many tokens of that type 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) A multiset over S is called a marking. Given
a marking m and a place s, we say that the place s contains m(s) tokens, graphi-
cally represented by m(s) bullets inside place s. A P/T net system N(m0 ) is a tuple
(S, A, T, m0 ), where (S, A, T ) is a P/T net and m0 is a marking over S, called the initial
marking. We also say that N(m0 ) is a marked net. 2
The sequential semantics of a marked net is defined by the so-called token game,
describing the flow of tokens through it. There are several possible variants (see, e.g.,
[8]) of the token game; below we present the so-called collective interpretation, accord-
ing to which multiple tokens on the same place are indistinguishable, while in Section 4
we introduce a novel variant following the so-called individual interpretation.
Definition 4. (Token game) A transition t is enabled at m, denoted m[ti, if •t ⊆ m. The
firing of t enabled at m produces the marking m0 = (m •t) ⊕ t • , written m[tim0 . 2
Definition 5. (Firing sequence, reachable marking) A firing sequence starting at m
is defined inductively as follows:
• m[εim is a firing sequence (where ε denotes an empty sequence of transitions) and
• if m[σ im0 is a firing sequence and m0 [tim00 , then m[σtim00 is a firing sequence.
If σ = t1 . . .tn (for n ≥ 0) and m[σ im0 is a firing sequence, then there exist m1 , . . . , mn+1
such that m = m1 [t1 im2 [t2 i . . . . . . mn [tn imn+1 = m0 , and σ = t1 . . .tn is called a transition
sequence starting at m and ending at m0 . The set of reachable markings from m is [mi =
{m0 ∃σ .m[σ im0 }. Note that the set of reachable markings may be countably infinite
for finite P/T nets. 2
Definition 6. (Classes of finite P/T Nets) A finite marked P/T net N = (S, A, T, m0 ) is:
• safe if every place contains at most one token under every reachable marking, i.e.
∀s ∈ S , m(s) ≤ 1 for all m ∈ [m0 i.
• bounded if the number of token in any place is bounded by some k for any reachable
marking, i.e. ∃k ∈ N, ∀s ∈ S such that m(s) ≤ k for all m ∈ [m0 i. If this is the case,
we say that the net is k-bounded (hence, a safe net is just a 1-bounded net). 2
4 A. Cesco and R. Gorrieri
3 Causality-based Semantics
We outline some definitions adapted from literature (cf., e.g., [11,1,16,19,9,12]).
Definition 7. (Acyclic net) A P/T net N = (S, A, T ) is acyclic if its flow relation F is
acyclic (i.e., 6 ∃x such that x F + x, where F + is the transitive closure of F).
The concurrent semantics of a marked P/T net is defined by a class of particular
acyclic safe nets, where places are not branched (hence they represent a single run) and
all arcs have weight 1. This kind of net is called causal net. We use the name C (possibly
indexed) to denote a causal net, the set B to denote its places (called conditions), the set
E to denote its transitions (called events), and L to denote its labels.
Definition 8. (Causal net) A causal net is a finite marked net C(m0 ) = (B, L, E, m0 )
satisfying the following conditions:
1. C is acyclic;
2. ∀b ∈ B |• b| ≤ 1 ∧(|b• | ≤ 1 (i.e., the places are not branched);
1 if • b = 0/
3. ∀b ∈ B m0 (b) =
0 otherwise;
4. ∀e ∈ E • e(b) ≤ 1 ∧ e• (b) ≤ 1 for all b ∈ B (i.e., all the arcs have weight 1).
We denote by Min(C) the set m0 , and by Max(C) the set {b ∈ B b• = 0}./
A sequence of events σ ∈ E ∗ is maximal (or complete) if it contains all events in E,
each taken once only. 2
Note that any reachable marking of a causal net is a set, i.e., this net is safe. As the
initial marking of a causal net is fixed by its shape, in the following, in order to make
the notation lighter, we often omit the indication of the initial marking (also in their
graphical representation), so that the causal net C(m0 ) is denoted by C.
Definition 9. (Moves of a causal net) Given two causal nets C = (B, L, E, m0 ) and
C0 = (B0 , L, E 0 , m0 ), we say that C moves in one step to C0 through e, denoted by C[eiC0 ,
if • e ⊆ Max(C), E 0 = E ∪ {e} and B0 = B ∪ e• . 2
Definition 10. (Folding and Process) A folding from a causal net C = (B, L, E, m0 )
into a net system N(m0 ) = (S, A, T, m0 ) is a function ρ : B ∪ E → S ∪ T , which is type-
preserving, i.e., such that ρ(B) ⊆ S and ρ(E) ⊆ T , satisfying the following:
• L = A and l(e) = l(ρ(e)) for all e ∈ E;
• ρ(m0 ) = m0 , i.e., m0 (s) = |ρ −1 (s) ∩ m0 |;
• ∀e ∈ E, ρ(• e) = • ρ(e), i.e., ρ(• e)(s) = |ρ −1 (s) ∩ • e| for all s ∈ S;
• ∀e ∈ E, ρ(e• ) = ρ(e)• , i.e., ρ(e• )(s) = |ρ −1 (s) ∩ e• | for all s ∈ S.
A pair (C, ρ), where C is a causal net and ρ a folding from C to a net system N(m0 ), is
a process of N(m0 ), written also as π. 2
Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets 5
Definition 11. (Partial orders of events from a process) From a causal net C =
(B, L, E, m0 ), we can extract the partial order of its events EC = (E, ), where e1 e2
if there is a path in the net from e1 to e2 , i.e., if e1 F∗ e2 , where F∗ is the reflexive and
transitive closure of F, which is the flow relation for C. Given a process π = (C, ρ), we
denote as ≤π , i.e. given e1 , e2 ∈ E, e1 ≤π e2 if and only if e1 e2 . 2
Definition 12. (Moves of a process) Let N(m0 ) = (S, A, T, m0 ) be a net system and let
(Ci , ρi ), for i = 1, 2, be two processes of N(m0 ). We say that (C1 , ρ1 ) moves in one step
e
to (C2 , ρ2 ) through e, denoted by (C1 , ρ1 ) −→ (C2 , ρ2 ), if C1 [eiC2 and ρ1 ⊆ ρ2 .
e
If π1 = (C1 , ρ1 ) and π2 = (C2 , ρ2 ), we denote the move as π1 −→ π2 . 2
Definition 13. (Causal-net bisimulation) Let N = (S, A, T ) be a finite P/T net. A causal-
net bisimulation is a relation R, composed of triples of the form (ρ1 ,C, ρ2 ), where, for
i = 1, 2, (C, ρi ) is a process of N(m0i ) for some m0i , such that if (ρ1 ,C, ρ2 ) ∈ R then
e
i) ∀t1 ,C0 , ρ10 such that (C, ρ1 ) −→ (C0 , ρ10 ), where ρ10 (e) = t1 , ∃t2 , ρ20 such that
e
(C, ρ2 ) −→ (C0 , ρ20 ), where ρ20 (e) = t2 , and (ρ10 ,C0 , ρ20 ) ∈ R;
e
ii) symmetrically, ∀t2 ,C0 , ρ20 such that (C, ρ2 ) −→ (C0 , ρ20 ), where ρ20 (e) = t2 , ∃t1 , ρ10
e
such that (C, ρ1 ) −→ (C0 , ρ10 ), where ρ10 (e) = t1 , and (ρ10 ,C0 , ρ20 ) ∈ R.
Two markings m1 and m2 of N are cn-bisimilar (or cn-bisimulation equivalent),
denoted by m1 ∼cn m2 , if there exists a causal-net bisimulation R containing a triple
(ρ10 ,C0 , ρ20 ), where C0 contains no events and ρi0 (Min(C0 )) = ρi0 (Max(C0 )) = mi for
i = 1, 2. 2
Causal-net bisimilarity, which coincides with structure-preserving bisimilarity [9],
observes not only the events, but also the structure of the distributed state. A weaker
equivalence, observing only the events performed, is fully-concurrent bisimulation (fc-
bisimulation, for short) [2] , whose definition was inspired by previous notions of equiv-
alence on other models of concurrency [17,6,10].
Definition 14. (Fully-concurrent bisimilarity) Given a finite P/T net N = (S, A, T ), a
fully-concurrent bisimulation is a relation R, composed of triples of the form (π1 , f , π2 )
where, for i = 1, 2, πi = (Ci , ρi ) is a process of N(m0i ) for some m0i and f is an isomor-
phism between EC1 and EC2 , such that if (π1 , f , π2 ) ∈ R then:
e
i) ∀t1 , π10 such that π1 −→
1
π10 , where ρ10 (e1 ) = t1 , there exist e2 ,t2 , π20 , f 0 such that
e
1. π2 −→ 2
π20 where ρ20 (e2 ) = t2 ,
2. f 0 = f ∪· {e1 7→ e2 },
3. (π10 , f 0 , π20 ) ∈ R;
ii) symmetrically, if π2 moves first.
Two markings m1 , m2 of N are fc-bisimilar, denoted by m1 ∼ f c m2 if a fully-concurrent
bisimulation R exists, containing a triple (π10 , 0,
/ π20 ) where πi0 = (Ci0 , ρi0 ) such that Ci0
contains no events and ρi (Min(Ci )) = ρi (Max(Ci0 )) = mi for i = 1, 2.
0 0 0 2
6 A. Cesco and R. Gorrieri
4 Indexed Marking Semantics
We define an alternative, novel token game semantics for Petri nets according to the
individual token philosophy. A token is represented as an indexed place, i.e. a pair
(s, i), where s is the name of the place where the token is on, and i is an index assigned
to the token such that different tokens on the same place have different indexes. In this
way, a standard marking is turned into an indexed marking, i.e. a set of indexed places.
Definition 15. (Indexed marking) Given a finite net N = (S, A, T ), an indexed mark-
ing is a function k : S → − P f in (N) associating to each place a finite set of natural num-
bers, such that the associated (de-indexed) marking m is obtained as m(s) = | k(s) | for
each s ∈ S. In this case, we write α(k) = m. The support set dom(k) is {s ∈ S k(s) 6= 0}. /
The set of the indexed markings with support set S is denoted by K(S).
An indexed place is a pair (s, i) such that s ∈ S and i ∈ N. A set of indexed places
{(s1 , i1 ), . . . , (sn , in )} ∈ P(S × N) is also another way of describing an indexed mark-
ing.1 Hence, K(S) ⊆ P(S × N). Each element of an indexed marking, i.e. each indexed
place, is a token.
An indexed marking k ∈ K(S) is closed if k(s) = {1, . . . , | k(s) |} for all s ∈ dom(k). If
there exists a marked net N(m0 ) and a closed indexed marking k0 such that α(k0 ) = m0 ,
we say that k0 is an initial indexed marking of N, and we write N(k0 ). 2
We define the difference between an indexed marking k and a marking m (such that
− M (S) →
m(s) ≤ |k(s)| for all s ∈ S) as : K(S) → − P(K(S))
k θ ={k}
k (s ⊕ m) =(k s) m
{k1 , . . . kn } m =k1 m ∪ . . . ∪ kn m
0 0 0 0 0
k s = {k k (s ) = k(s ) if s 6= s , or
= k(s) \ {n} if s0 = s and n ∈ k(s)}
− M (S) →
and the union of an indexed marking k and a marking m as : K(S) → − K(S)
kθ = k
k (s ⊕ m) = (k s) m
k s = k0
where for all s0 ∈ S , k0 (s0 ) is defined as:
(
0 0 k(s0 ) if s0 6= s
k (s ) =
k(s) ∪ {n} if s0 = s, n = min(k(s)) where k(s) = N \ k(s)
where we use min(H), with H ∈ P(N), to denote the least element of H. Note that
the difference between an indexed marking and a marking is a set of indexed markings:
1 Being a set, we are sure that 6 ∃ j , j such that s = s ∧ i = i , i.e., each token on a
1 2 j1 j2 j1 j2
place s has an index different from the index of any other token on s.
Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets 7
since it makes no sense to prefer a single possible execution over another, all possible
choices for n ∈ k(s) are to be considered. The token game is modified accordingly,
taking into account the individual token interpretation.
Definition 16. (Token game with indexed markings) Given a net N = (S, A, T ) and
an indexed marking k ∈ K(S) such that m = α(k), we say that a transition t ∈ T is
enabled at k if •t ⊆ m, denoted kJti. If t occurs, the firing of t enabled at k produces the
indexed marking k0 , denoted kJtik0 , if
- ∃k00 ∈ k •t and
- k0 = k00 t • . 2
Note that there can be more than one indexed marking produced by the firing of t,
but for all k0 such that kJtik0 , it is true that α(k0 ) = m •t ⊕ t • .
From now on, indexed markings will be always represented as sets of indexed
places, i.e., we denote an indexed marking k by {(s1 , n1 ) . . . (si , ni )} where | k | = i.
s1 s1 s1
a) 1 b) 1 c)
u u u
2 2 2
1
s2 2 3 s2 1 3 s2 1 2
3 4
v v v
s3 s3 1 s3 1
Fig. 1. Execution of the transition labeled by v, then of the transition labeled by u, on a bounded
net with initial marking m0 = s1 ⊕ 3s2 . Tokens to be consumed are in red, generated ones in blue.
Example 1. In Figure 1(a) a simple net N is given. The initial marking is m0 = s1 ⊕ 3s2 ,
therefore the marked net N(m0 ) is 5-bounded. The initial indexed marking is k0 =
{(s1 , 1), (s2 , 1), (s2 , 2), (s2 , 3)}. Let us suppose that transition t2 , labeled by v, occurs.
There are three possible ways to remove a token from s2 : removing (s2 , 1), or removing
(s2 , 2), or removing (s2 , 3). Indeed, the operation k0 •t2 yields a set of three possible
indexed markings, each one a possible result of the difference: {{(s1 , 1), (s2 , 2), (s2 , 3)},
{(s1 , 1), (s2 , 1), (s2 , 3)}, {(s1 , 1), (s2 , 1), (s2 , 2)}}. Let us choose, for the sake of the ar-
gument, that the token deleted by t2 is (s2 , 2), i.e. choose k0 = {(s1 , 1), (s2 , 1), (s2 , 3)}.
The union k0 t2• easily yields the indexed marking k1 = {(s1 , 1), (s2 , 1), (s2 , 3), (s3 , 1)},
as depicted in Figure 1(b). Note that this choice was arbitrary and two other values
of k1 are possible. Indeed, from Definition 16, we know that the transition relation
8 A. Cesco and R. Gorrieri
generated deleted untouched
m[tim0 t• •t m •t
kJtik0 k0 \ k00 k \ k00 k00
Table 1. Different notation for tokens in the token game. On the first line, the collective case. On
the last one, the individual case.
on indexed markings is nondeterministic. However, the resulting marked net is the
same for all three cases, that is, the same of Figure 1(b) without indexes. Now we
suppose that (given the indexed marking k1 from above) transition t1 , labeled by u,
occurs. In that case, k1 •t1 yields the singleton set {{(s2 , 1), (s2 , 3), (s3 , 1)}}, there-
fore we choose k00 = {(s2 , 1), (s2 , 3), (s3 , 1)}. Since t1• = s2 ⊕ s2 , we show in detail how
k00 t1• is computed. First, we apply the definition for union with non-singleton mul-
tisets: k00 (s2 ⊕ s2 ) = (k00 s2 ) s2 . Then, we compute k00 s2 : since the least free
index for the place s2 is 2, k00 s2 = {(s2 , 1), (s2 , 2)(s2 , 3), (s3 , 1)}. Now we apply again
the definition: note that this time the least free index for s2 is 4, and the final result
is k2 = {(s2 , 1), (s2 , 2)(s2 , 3), (s2 , 4), (s3 , 1)}. The resulting marked net is depicted in
Figure 1(c). 2
The notation for tokens in the token game has become slightly more unintuitive,
so in Table 1 we provide a comparison between the one used in the previous sections
and the one we will use in the following part of this work. Given a transition t such
that kJtik0 and m[tim0 , assume k00 ∈ k •t such that k0 = k00 t • , where α(k) = m and
α(k0 ) = m0 .
Definition 17. (Firing sequence with IM) Given a finite net N = (S, A, T ) and an in-
dexed marking k, a firing sequence starting at k is defined inductively as follows:
• kJεik is a firing sequence (where ε denotes an empty sequence of transitions) and
• if kJσ ik0 is a firing sequence and k0 Jtik00 , then kJσtik00 is a firing sequence.
The set of reachable indexed markings from k is Jki = {k0 ∃σ . kJσ ik0 }. Given a net
N(k0 ), we call Jk0 i the set of reachable indexed marking of N, denoted by IM(N). 2
Proposition 1. Given a finite bounded net N = (S, A, T, m0 ), the set IM(N) ⊆ K(S) of
reachable indexed markings is finite.
Proof. Full detail in the preliminary full version of this article [5].
5 Ordered Indexed Marking Semantics
Vogler [19] introduces ordered markings (OM for short) to describe the state of a safe
marked net. They consist of a safe marking together with a preorder which reflects
precedences in the generation of tokens. This is reflected in the token game for OM: if
s precedes some s00 in the old OM and s00 is used to produce a new token s0 , then s must
precede s0 in the new OM.
Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets 9
The key idea of Vogler’s decidability proof for safe nets is that the OM obtained by
a sequence of transitions of a net is the same as the one induced by a process, whose
events correspond to that sequence of transitions, on the net itself. Since ordered mark-
ings are finite objects, Vogler defines OM-bisimulation and shows that it coincides with
fully-concurrent bisimulation. He himself hinted at a possibility [19] of extending the
result to bounded nets, but suggested that it would have been technically quite involved.
We adapt his approach by defining a semantics based on ordered indexed mark-
ings, taking into account the individual token interpretation of nets, and proving that an
extension to bounded nets is indeed possible.
Definition 18. (Ordered indexed marking) Given a P/T net N = (S, A, T ) and an in-
dexed marking k ∈ K(S), the pair (k, ≤) is an ordered indexed marking if ≤⊆ k × k is a
preorder, i.e. a reflexive and transitive relation. The set of all possible ordered indexed
markings of N is denoted by OIM(N).
If k0 is the initial indexed marking of N, we define the initial ordered indexed mark-
ing init(N) as (k0 , k0 × k0 ). If the initial indexed marking is not clear from the context,
we write init(N(k0 )) to denote the initial ordered indexed marking. 2
Definition 19. (Token game with ordered indexed markings) Given a P/T net N =
(S, A, T ) and an ordered indexed marking (k, ≤), we say that a transition t ∈ T is en-
abled at (k, ≤) if kJti; this is denoted by (k, ≤)Jti.
The firing of t enabled at (k, ≤) may produce an ordered indexed marking (k0 , ≤0 )
– and we denote this by (k, ≤)Jti(k0 , ≤0 ) – where:
• k00 ∈ k •t such that k0 = k00 t •
• for all (sh , ih ), (s j , i j ) ∈ k0 , (sh , ih ) ≤0 (s j , i j ) if and only if:
1. (sh , ih ), (s j , i j ) ∈ k00 and (sh , ih ) ≤ (s j , i j ), or
2. (sh , ih ), (s j , i j ) ∈ k0 \ k00 , or
3. (sh , ih ) ∈ k00 , (s j , i j ) ∈ k0 \ k00 and ∃(sl , il ) ∈ k \ k00 such that (sh , ih ) ≤ (sl , il ). 2
Note that, as for indexed markings, many different ordered indexed markings are
produced from the firing of t. This means that also the transition relation for ordered
indexed markings is nondeterministic. Moreover, in the same fashion as Vogler’s work
[19], the preorder reflects the precedence in the generation of tokens, which is not strict,
i.e. if tokens (s1 , n1 ) and (s2 , n2 ) are generated together we have both (s1 , n1 ) ≤ (s2 , n2 )
and (s2 , n2 ) ≤ (s1 , n1 ).
Example 2. Consider again the net in Figure 1 and the first part of the execution of
Example 1, i.e. k0 Jt2 ik1 . According to Definition 18, the initial ordered indexed marking
is (k0 , ≤0 ), where ≤0 = k0 × k0 . When t2 fires, token (s2 , 2) is removed and token (s3 , 1)
is generated, while all other tokens are untouched. Let us denote the preorder induced
by the firing of t2 as ≤1 . According to item 2 of Definition 19, since (s3 , 1) is generated
by the firing of t2 , we have (s3 , 1) ≤1 (s3 , 1). According to item 1 of Definition 19,
the preorder on all tokens untouched by t2 remains the same, therefore e.g. (s2 , 3) ≤1
(s1 , 1) and viceversa. Furthermore, consider (s1 , 1) and (s3 , 1): we have that t2 generates
(s3 , 1), deletes (s2 , 2) and leaves (s1 , 1) untouched. Since (s1 , 1) ≤0 (s2 , 2), by item 3 of
Definition 19 we have (s1 , 1) ≤1 (s3 , 1). The same reasoning applies to all untouched
10 A. Cesco and R. Gorrieri
tokens. Summing up, we have (k0 , ≤0 )Jt2 i(k1 , ≤1 ) where
≤1 =≤0 \{((si , ni ), (s j , n j )) ∈ k0 (si , ni ) = (s2 , 2) ∨ (s j , n j ) = (s2 , 2)} ∪
{((s1 , 1), (s3 , 1)), ((s2 , 1), (s3 , 1)), ((s2 , 3), (s3 , 1)), ((s3 , 1), (s3 , 1))}. 2
Definition 20. (Firing sequence with OIM) A firing sequence starting at (k, ≤) is
defined inductively as follows:
• (k, ≤)Jεi(k, ≤) is a firing sequence (where ε denotes an empty sequence of transi-
tions) and
• if (k, ≤)Jσ i(k0 , ≤0 ) is a firing sequence and (k0 , ≤0 )0 Jti(k00 , ≤00 ), then
(k, ≤)Jσti(k00 , ≤00 ) is a firing sequence.
The set of reachable ordered indexed markings from (k, ≤) is
J(k, ≤)i = {(k0 , ≤0 ) ∃σ . (k, ≤)Jσ i(k0 , ≤0 )}.
Given an initial indexed marking k0 , the set of all the reachable ordered indexed mark-
ings of N(k0 ) is denoted by Jinit(N)i. 2
Proposition 2. Given a bounded net N = (S, A, T, m0 ), Jinit(N)i is finite.
Proof. The set IM(N) of reachable indexed markings is finite by Proposition 1. The
set of possible preorders for an indexed marking k = {(s1 , n1 ) . . . (s j , n j )} ∈ IM(N) is
finite, because ≤⊆ k × k. Therefore, Jinit(N)i is finite.
5.1 Ordered indexed marking and causality-based semantics
Given a transition sequence σ , there is an operational preorder on tokens obtained by
Definition 20, and a preorder derived from the process ≤π obtained from the causal
net C corresponding to the transition sequence σ . In the following, we introduce some
notation for processes and ordered indexed markings, and relate the two. If π = (C, ρ)
is a process of a marked net N(m0 ) and k0 is the initial indexed marking for N(m0 ) (i.e.
α(k0 ) = m0 and k0 is closed), we also say that π is a process of N(k0 ). Moreover, given
a process π = (C, ρ) of a net N(k0 ) and σ a complete transition sequence of C, we write
init(N)Jπi(k, ≤) if init(N)Jρ(σ )i(k, ≤).
Theorem 1. Let π = (C, ρ) a process of N(k0 ) such that init(N)Jπi(k, ≤).
e
Then (k, ≤)Jti(k0 , ≤0 ) if and only if π −→ π 0 where ρ 0 (e) = t and init(N)Jπ 0 i(k0 , ≤0 ).
Proof. By induction on the sequence σ .e where σ is a complete transition sequence of
C. Complete proof in the preliminary full version of this article [5].
Example 3. In Figure 2(a), the same 5-bounded P/T net N as Figure 1 is depicted, to-
gether with its empty process (we omit the representation of its initial marking). Fig-
ure 2(b,c) shows how the process corresponding to the transition sequence t2 t1 grows.
We consider the same execution as in Example 1, i.e. k0 Jt2 ik1 Jt1 ik2 . For simplicity’s
sake, in the following each condition will be mapped to the place having same subscript
and each event will be mapped to the transition having same label. We will denote each
process πi as the one thus corresponding to causal net Ci . Before any transition fires, we
have init(N) = (k0 , ≤0 ) where ≤0 = k0 × k0 by Definition 18. Not surprisingly, all
Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets 11
s1 b1 b12 b22 b32
a) 1 (C0
u
2
1
s2 2 3
v
s3
[e2 i
Jt2 i
s1 b1 b12 b22 b32
b) 1 (C1
u v
2
s2 1 3 b3
v
s3
[e1 i
1
Jt1 i
s1 b1 b12 b22 b32
c) (C2
u u v
2
s2 1 2
3 4
b42 b52
b3
v
s3 1
Fig. 2. Execution of the transition labeled by v, then u, on the net of Figure 1 and corresponding
process (only the mapping of maximal conditions to tokens is displayed). Tokens to be consumed
are red, generated ones blue.
12 A. Cesco and R. Gorrieri
conditions bij are minimal in the causal net C0 and mapped to tokens in the initial in-
dexed ordered marking. The firing of t2 deletes token (s2 , 2) and generates token (s3 , 1);
moreover, since (s2 , 1) ≤0 (s2 , 2) we have (s2 , 1) ≤1 (s3 , 1). Note that b12 ∈ Min(C1 ) but
b3 6∈ Min(C1 ). After the firing of t1 , there are four tokens in place s2 . However, since
(s2 , 2) and (s2 , 4) are generated by t1 , they are greater in ≤2 than (s2 , 1) and (s2 , 3). This
can also be seen at the process level: b12 and b32 are minimal conditions of C2 , while b42
and b52 are not. On the other hand, note that, just as b42 and b3 are not minimal in C2 but
also not related by ≤π2 , also (s2 , 2) and (s3 , 1) are not related by ≤2 . 2
6 Fully-concurrent Bisimilarity is Decidable
We now define a novel bisimulation relation based on ordered indexed markings, gen-
eralizing the similar idea in [19].
Definition 21. (OIM-bisimulation) Let N = (S, A, T ) be a P/T net. An OIM-bisimulation
is a relation B ⊆ OIM(N) × OIM(N) × P((S × N) × (S × N)) such that if
((k1 , ≤1 ), (k2 , ≤2 ), β ) ∈ B, then:
• ∀t1 , k10 , ≤01 such that (k1 , ≤1 )Jt1 i(k10 , ≤01 ), (where we assume k100 ∈ k1 •t1 such that k10 =
k100 t1• ), there exist t20 , k20 , ≤02 (where we assume k200 ∈ k2 •t2 such that k20 = k200 t2• ),
and for β 0 defined as ∀(s1 , n1 ) ∈ k10 , ∀(s2 , n2 ) ∈ k20 :
(
0 (s1 , n1 ) ∈ k100 , (s2 , n2 ) ∈ k200 , (s1 , n1 ) β (s2 , n2 ), or
(s1 , n1 ) β (s2 , n2 ) ⇔
(s1 , n1 ) ∈ k10 \ k100 , (s2 , n2 ) ∈ k20 \ k200
the following hold:
- (k2 , ≤2 )Jt2 i(k20 , ≤02 ) where ((k10 , ≤01 ), (k20 , ≤02 ), β 0 ) ∈ B and l(t1 ) = l(t2 );
- ∀(s1 , n1 ) ∈ k1 \ k100 , ∃(s01 , n01 ) ∈ k1 \ k100 , (s02 , n02 ) ∈ k2 \ k200 such that (s1 , n1 ) ≤1
(s01 , n01 ) ∧ (s01 , n01 ) β (s02 , n02 ) and symmetrically ∀(s2 , n2 ) ∈ k2 \ k200 , ∃(s02 , n02 ) ∈
k2 \ k200 , (s01 , n01 ) ∈ k1 \ k100 such that (s2 , n2 ) ≤2 (s02 , n02 ) ∧ (s01 , n01 ) β (s02 , n02 )
• symmetrically, if (k2 , ≤2 ) moves first.
Two markings m1 and m2 of N are OIM-bisimilar, denoted m1 ∼oim m2 , if there exists
an OIM-bisimulation B containing the triple (init(N(k1 )), init(N(k2 ), k1 × k2 ) where,
for i = 1, 2, ki is the initial indexed marking such that mi = α(ki ). 2
Our aim is to relate ∼ f c and ∼oim and the idea is that two tokens are related by β
if and only if the transition generating one of the two is mapped by f to the transition
generating the other one. Next, we show that fully-concurrent bisimilarity and OIM-
bisimilarity coincide on P/T nets.
Theorem 2. (OIM-bisimilarity and FC-bisimilarity coincide) Let N = (S, A, T ) be a
P/T net and m1 , m2 two markings of N. m1 ∼oim m2 if and only if m1 ∼ f c m2 .
Proof. See the preliminary full version of this article [5].
Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets 13
Theorem 3. (FC-bisimilarity is decidable for finite bounded nets) Given N(m1 ) and
N(m2 ) bounded nets, it is decidable to check whether m1 ∼ f c m2 .
Proof. By Theorem 2, we have to check whether m1 ∼oim m2 . There are finitely many
possible sets of triples following Definition 21. Therefore we can check by exhaustive
search whether one of them is an OIM-bisimulation. Full detail in the preliminary full
version of this article [5].
We conclude this section with a remark on the complexity of the decision procedure.
Assume that the considered net has (less than) s places, t transitions and it is h-bounded.
The upper bound for our decision procedure is 2O(hs·log(hs)+log(t)) . Full detail in the
preliminary full version of this article [5]. Note that our exhaustion algorithm has no
worse complexity than other proposed algorithms [15,14].
7 Causal-net Bisimilarity is Decidable
In the same fashion as the preceding section, we now prove that also causal-net bisimi-
larity is decidable.
Definition 22. (OIMC bisimulation) Let N = (S, A, T ) be a P/T net. An OIMC bisim-
ulation is a relation B ⊆ OIM(N) × OIM(N) × P((S × N) × (S × N)) such that if
((k1 , ≤1 ), (k2 , ≤2 ), β ) ∈ B, then:
• | k1 | = | k2 |
• ∀t1 , k10 , ≤01 if (k1 , ≤1 )Jt1 i(k10 , ≤01 ) (where we assume that k100 ∈ k1 •t 0
1 such that k1 =
k100 t1• ), then there exist t2 , k20 , ≤02 (where we assume k200 ∈ k2 •t 0
2 such that k2 =
k200 t2• ), and for β 0 defined as ∀(s1 , n1 ) ∈ k10 , ∀(s2 , n2 ) ∈ k20 :
(
(s1 , n1 ) ∈ k100 , (s2 , n2 ) ∈ k200 , (s1 , n1 ) β (s2 , n2 ) , or
(s1 , n1 ) β 0 (s2 , n2 ) ⇔
(s1 , n1 ) ∈ k10 \ k100 , (s2 , n2 ) ∈ k20 \ k200
the following hold:
- (k1 \ k100 ) and (k2 \ k200 ) are bijectively related by β ,
- (k2 , ≤2 )Jt2 i(k20 , ≤02 ) where ((k10 , ≤01 ), (k20 , ≤02 ), β 0 ) ∈ B and l(t1 ) = l(t2 ).
• symmetrically, if (k2 , ≤2 ) moves first.
Two markings m1 and m2 of N are OIMC bisimilar, denoted m1 ∼oimc m2 , if there exists
an OIMC bisimulation B containing the triple (init(N(k1 )), init(N(k2 ), k1 × k2 ) where,
for i = 1, 2, ki is the closed indexed marking such that mi = α(ki ). 2
Theorem 4. (OIMC-bisimilarity and CN-bisimilarity coincide) Let N = (S, A, T ) be
a P/T net and m1 , m2 two markings of N. m1 ∼oimc m2 if and only if m1 ∼cn m2 .
Proof. See the preliminary full version of this article [5].
Theorem 5. (CN-bisimilarity is decidable for finite bounded nets) Given N(m1 ) and
N(m2 ) bounded nets, it is decidable to check whether m1 ∼cn m2 .
14 A. Cesco and R. Gorrieri
Proof. By Theorem 4 we have to check whether there exists an OIMC-bisimulation B
for the given net N and initial markings m1 , m2 . The proof then follows the same steps
of Theorem 3.
Note that the complexity of this procedure is again 2O(hs·log(hs)+log(t)) .
8 Conclusion and Future Research
We have extended Vogler’s proof technique in [19], based on ordered markings, that
he used to prove decidability of (strong) fully-concurrent bisimilarity for safe nets, to
bounded nets by means of indexed ordered markings. The extension is flexible enough
to be applicable also to other similar equivalences, such as causal-net bisimilarity [9,12].
While decidability of fully-concurrent bisimilarity for bounded nets was already proved
by Montanari and Pistore [15], our result for causal-net bisimilarity is new. However,
the approach of [15] is not defined directly on Petri nets, rather it exploits an encoding of
Petri nets into so-called causal automata, a model of computation designed for handling
dependencies between transitions by means of names. In addition to this, their encod-
ing works modulo isomorphisms, so that, in order to handle correctly the dependency
names, at each step of the construction costly renormalizations are required. Along the
same line, recently history-dependent automata [4,3] have been proposed. They are a
much refined version of causal automata, retaining not only events but also their causal
relations. Moreover, they are equipped with interesting categorical properties such as
having symmetry groups over them, which allow for state reductions. As in the former
work, the latter ones do not work directly on the net and may require minimizations (al-
beit automatic, in the case of HD automata). On the contrary, our construction is very
concrete and works directly on the net. Thus, we conjecture that, even if the worst-case
complexity is roughly the same, our algorithm performs generally better.
Decidability of fully-concurrent bisimilarity for bounded nets using the ordered in-
dexed marking idea was claimed to have been proved by Valero-Ruiz in his PhD thesis
[18]. However, his proof contains many flaws; an accurate analysis of which can be
found in the preliminary version of this paper [5]. Therefore our work can be consid-
ered the first one to have proved it using the ordered indexed marking approach.
A natural question is whether it is possible to decide these equivalences for larger
classes of nets, notably unbounded P/T nets. However, as Esparza observed in [7], all
the behavioral equivalences ranging from interleaving bisimilarity to fully-concurrent
bisimilarity are undecidable on unbounded P/T nets. So, there is no hope to extend our
result about fc-bisimilarity further. Nonetheless, the proof of undecidability by Janc̆ar
[13] does not apply to causal-net bisimilarity, so that the decidability of causal-net
bisimilarity over unbounded P/T nets is open. As a future work, we plan to extend
Vogler’s results in [20] about decidability of weak fully-concurrent bisimilarity on safe
nets with silent moves, to bounded nets with silent moves, by means of our indexed
marking idea.
Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets 15
References
1. Best, E., Devillers, R.: Sequential and concurrent behaviour in petri net theory. Theoretical
Computer Science 55, 87–136 (1987). https://doi.org/10.1016/0304-3975(87)90090-9
2. Best, E., Devillers, R.R., Kiehn, A., Pomello, L.: Concurrent bisimulations in petri nets. Acta
Informatica 28, 231–264 (1991). https://doi.org/10.1007/BF01178506
3. Bruni, R., Montanari, U., Sammartino, M.: A coalgebraic semantics for causality in petri
nets. Journal of Logic and Algebraic Methods in Programming 84(6), 853–883 (2015).
https://doi.org/10.1016/j.jlamp.2015.07.003
4. Bruni, R., Montanari, U., Sammartino, M.: Revisiting causality, coalgebraically. Acta Infor-
matica 52(1), 5–33 (2015). https://doi.org/10.1007/s00236-014-0207-9
5. Cesco, A., Gorrieri, R.: Decidability of two truly concurrent equivalences for finite bounded
petri nets. CoRR (2021), https://arxiv.org/abs/2104.14856
6. Degano, P., Nicola, R.D., Montanari, U.: Partial orderings descriptions and observations of
nondeterministic concurrent processes. Lecture Notes in Computer Science 354, 438–466
(1988). https://doi.org/10.1007/BFb0013030
7. Esparza, J.: Decidability and complexity of petri net problems - an introduction. Lecture
Notes in Computer Science 1491, 374–428 (1996). https://doi.org/10.1007/3-540-65306-
6 20
8. van Glabbeek, R.J.: The individual and collective token interpretations of petri nets. Lecture
Notes in Computer Science 3653, 323–337 (2005). https://doi.org/10.1007/11539452 26
9. van Glabbeek, R.J.: Structure preserving bisimilarity, supporting an operational petri
net semantics of CCSP. Lecture Notes in Computer Science 9360, 99–130 (2015).
https://doi.org/10.1007/978-3-319-23506-6 9
10. van Glabbeek, R.J., Goltz, U.: Refinement of actions and equivalence notions for concurrent
systems. Acta Informatica 37, 229–327 (2001). https://doi.org/10.1007/s002360000041
11. Goltz, U., Reisig, W.: The non-sequential behaviour of petri nets. Information and Control
57, 125–147 (1983). https://doi.org/10.1016/S0019-9958(83)80040-0
12. Gorrieri, R.: A study on team bisimulations for BPP nets. Lecture Notes in Computer Science
12152, 153–175 (2020). https://doi.org/10.1007/978-3-030-51831-8 8
13. Jancar, P.: Undecidability of bisimilarity for petri nets and some related problems. Theoret-
ical Computer Science 148, 281–301 (1995). https://doi.org/10.1016/0304-3975(95)00037-
W
14. Jategaonkar, L., Meyer, A.R.: Deciding true concurrency equivalences on safe, finite
nets. Theoretical Computer Science 154, 107–143 (1996). https://doi.org/10.1016/0304-
3975(95)00132-8
15. Montanari, U., Pistore, M.: Minimal transition systems for history-preserving
bisimulation. Lecture Notes in Computer Science 1200, 413–425 (1997).
https://doi.org/10.1007/BFb0023477
16. Olderog, E.R.: Nets, Terms and Formulas, vol. Cambridge Tracts in
Theoretical Computer Science 23. Cambridge University Press (1991).
https://doi.org/10.1017/CBO9780511526589
17. Rabinovich, A., Trakhtenbrot, B.A.: Behavior structures and nets. Fundamenta Informaticae
11, 357–403 (1988). https://doi.org/10.3233/FI-1988-11404, 4
18. Valero-Ruiz, V.: Decibilidad de problemas sobre redes de Petri temporizadas. Ph.D. the-
sis, Universidad Complutense de Madrid, Madrid (1993), https://eprints.ucm.es/
id/eprint/3439/
19. Vogler, W.: Deciding history preserving bisimilarity. Lecture Notes in Computer Science
510, 495–505 (1991). https://doi.org/10.1007/3-540-54233-7 158
20. Vogler, W.: Generalized om-bisimulation. Information and Computation 118, 38–47 (1995).
https://doi.org/10.1006/inco.1995.1050