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, historypreserving bisimilarity) is decidable on finite safe nets. Copyright 2021 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
Truly concurrent equivalences, such as fully-concurrent bisimilarity [
In his seminal paper [
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
bisimilarity and (strong) fully-concurrent bisimilarity. Section 4 introduces indexed markings
and the alternative, individual, token game semantics. Section 5 describes indexed
ordered 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 [
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 fs 2 S m(s) 6= 0g. The set of all multisets over S, denoted by M (S), is ranged over by m. We write s 2 m if m(s) > 0. The multiplicity of s in m is given by the number m(s). The size of m, denoted by jmj, is the number ås2S 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 q . We write m m0 if m(s) m0(s) for all s 2 S. Multiset union is defined as follows: (m m0)(s) = m(s) + m0(s). Multiset difference is defined as follows: (m1 m2)(s) = maxfm1(s) m2(s); 0g. 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 = fs1; : : : ; sng can be represented as k1 s1 k2 s2 : : : kn sn, where k j = m(s j) 0 for j = 1; : : : ; n. 2
short) is a tuple N = (S; A; T ), where
T (M (S) n fq g) A M (S) is the finite set of transitions, ranged over by t (possibly indexed). 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 consumed; l(t) for its label `, and t to denote its post-set m0 of tokens to be produced.
Hence, transition t can be also represented as t l(t) ! t . We also define the flow function flow : (S T ) [ (T S) ! N as follows: for all s 2 S, for all t 2 T , flow(s; t) = t(s) and flow(t; s) = t (s). We will use F to denote the flow relation f(x; y) 2 (S T ) [ (T S) flow(x; y) > 0g. Finally, we define pre-sets and post-sets also for places as follows: s = ft 2 T s 2 t g and s = ft 2 T s 2 tg. 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 labeled 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.
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(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.,
[
We outline some definitions adapted from literature (cf., e.g., [
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. 8b 2 B j bj 3. 8b 2 B m0(b) = 1 ^ jb j 1 (i.e., the places are not branched); (1 if b = 0/
0 otherwise; 4. 8e 2 E e(b) 1 ^ e (b)
1 for all b 2 B (i.e., all the arcs have weight 1).
We denote by Min(C) the set m0, and by Max(C) the set fb 2 B b = 0/ g. A sequence of events s 2 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; E0; m0), we say that C moves in one step to C0 through e, denoted by C[eiC0, if e Max(C), E0 = E [ feg 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 r : B [ E ! S [ T , which is typepreserving, i.e., such that r(B) S and r(E) T , satisfying the following: L = A and l(e) = l(r(e)) for all e 2 E; r(m0) = m0, i.e., m0(s) = jr 1(s) \ m0j; 8e 2 E; r( e) = r(e), i.e., r( e)(s) = jr 1(s) \ ej for all s 2 S; 8e 2 E; r(e ) = r(e) , i.e., r(e )(s) = jr 1(s) \ e j for all s 2 S.
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 e1F e2, where F is the reflexive and transitive closure of F, which is the flow relation for C. Given a process p = (C; r), we denote as p , i.e. given e1; e2 2 E, e1 p 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; ri), for i = 1; 2, be two processes of N(m0). We say that (C1; r1) moves in one step to (C2; r2) through e, denoted by (C1; r1) !e (C2; r2), if C1[eiC2 and r1 r2. If p1 = (C1; r1) and p2 = (C2; r2), we denote the move as p1 e 2
Definition 13. (Causal-net bisimulation) Let N = (S; A; T ) be a finite P/T net. A causalnet bisimulation is a relation R, composed of triples of the form (r1;C; r2), where, for i = 1; 2, (C; ri) is a process of N(m0i ) for some m0i , such that if (r1;C; r2) 2 R then i) 8t1;C0; r10 such that (C; r1) !e (C0; r10), where r10(e) = t1, 9t2; r20 such that (C; r2) !e (C0; r20), where r20(e) = t2, and (r10;C0; r20) 2 R; ii) symmetrically, 8t2;C0; r20 such that (C; r2) !e (C0; r20), where r20(e) = t2, 9t1; r10 such that (C; r1) !e (C0; r10), where r10(e) = t1, and (r10;C0; r20) 2 R.
denoted by m1 cn m2, if there exists a causal-net bisimulation R containing a triple (r10;C0; r20), where C0 contains no events and ri0(Min(C0)) = ri0(Max(C0)) = mi for i = 1; 2. 2
Causal-net bisimilarity, which coincides with structure-preserving bisimilarity [
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 (p1; f ; p2) where, for i = 1; 2, pi = (Ci; ri) is a process of N(m0i) for some m0i and f is an isomorphism between EC1 and EC2 , such that if (p1; f ; p2) 2 R then: i) 8t1; p10 such that p1
e 1. p2 !2 p20 where r20(e2) = t2, 2. f 0 = f [ fe1 7! e2g, 3. (p10; f 0; p0 ) 2 R;
2 ii) symmetrically, if p2 moves first.
e !1 p10, where r10(e1) = t1, there exist e2; t2; p20; f 0 such that
bisimulation R exists, containing a triple (p10; 0/ ; p20) where pi0 = (Ci0; ri0) such that Ci0 contains no events and ri0(Min(Ci0)) = ri0(Max(Ci0)) = mi for i = 1; 2. 2
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 marking is a function k : S ! P f in(N) associating to each place a finite set of natural numbers, such that the associated (de-indexed) marking m is obtained as m(s) = j k(s) j for each s 2 S. In this case, we write a(k) = m. The support set dom(k) is fs 2 S k(s) 6= 0/ g.
An indexed place is a pair (s; i) such that s 2 S and i 2 N. A set of indexed places f(s1; i1); : : : ; (sn; in)g 2 P(S N) is also another way of describing an indexed marking.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 2 K(S) is closed if k(s) = f1; : : : ; j k(s) jg for all s 2 dom(k). If there exists a marked net N(m0) and a closed indexed marking k0 such that a(k0) = m0, we say that k0 is an initial indexed marking of N, and we write N(k0). 2 m(s)
We define the difference between an indexed marking k and a marking m (such that jk(s)j for all s 2 S) as : K(S) ! M (S) ! P(K(S)) k (s k q =fkg m) =(k s)
m fk1; : : : kng m =k1 m [ : : : [ kn
m k s = fk0 k0(s0) = k(s0) if s0 6= s ; or
= k(s) n fng if s0 = s and n 2 k(s)g and the union of an indexed marking k and a marking m as : K(S) ! M (S) ! K(S) k
q = k k s = k0 k (s m) = (k s) m where for all s0 2 S ; k0(s0) is defined as: k0(s0) = (k(s0) k(s) [ fng if s0 6= s if s0 = s; n = min(k(s)) where k(s) = N n k(s) where we use min(H), with H 2 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: 1Being a set, we are sure that 6 9 j1; j2 such that s j1 = s j2 ^ i j1 = i j2 , i.e., each token on a place s has an index different from the index of any other token on s. since it makes no sense to prefer a single possible execution over another, all possible choices for n 2 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 2 K(S) such that m = a(k), we say that a transition t 2 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
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 a(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 f(s1; n1) : : : (si; ni)g where j k j = i. a) s1 1 u
2 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 = f(s1; 1); (s2; 1); (s2; 2); (s2; 3)g. 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: ff(s1; 1); (s2; 2); (s2; 3)g; f(s1; 1); (s2; 1); (s2; 3)g; f(s1; 1); (s2; 1); (s2; 2)gg. Let us choose, for the sake of the argument, that the token deleted by t2 is (s2; 2), i.e. choose k0 = f(s1; 1); (s2; 1); (s2; 3)g. The union k0 t2 easily yields the indexed marking k1 = f(s1; 1); (s2; 1); (s2; 3); (s3; 1)g, 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
generated deleted untouched m[tim0 t t m t kJtik0 k0 n k00 k n k00 k00 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 ff(s2; 1); (s2; 3); (s3; 1)gg, therefore we choose k00 = f(s2; 1); (s2; 3); (s3; 1)g. Since t1 = s2 s2, we show in detail how k00 t1 is computed. First, we apply the definition for union with non-singleton multisets: k00 (s2 s2) = (k00 s2) s2. Then, we compute k00 s2: since the least free index for the place s2 is 2, k00 s2 = f(s2; 1); (s2; 2)(s2; 3); (s3; 1)g. Now we apply again the definition: note that this time the least free index for s2 is 4, and the final result is k2 = f(s2; 1); (s2; 2)(s2; 3); (s2; 4); (s3; 1)g. 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 2 k t such that k0 = k00 t , where a(k) = m and a(k0) = m0.
Definition 17. (Firing sequence with IM) Given a finite net N = (S; A; T ) and an indexed marking k, a firing sequence starting at k is defined inductively as follows: kJeik is a firing sequence (where e denotes an empty sequence of transitions) and if kJs ik0 is a firing sequence and k0Jtik00, then kJstik00 is a firing sequence. The set of reachable indexed markings from k is Jki = fk0 9s : kJs ik0g. Given a net N(k0), we call Jk0i 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) reachable indexed markings is finite.
K(S) of
Proof. Full detail in the preliminary full version of this article [
Vogler [
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
markings are finite objects, Vogler defines OM-bisimulation and shows that it coincides with
fully-concurrent bisimulation. He himself hinted at a possibility [
We adapt his approach by defining a semantics based on ordered indexed markings, 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 indexed marking k 2 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).
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 2 T is enabled 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 2 k t such that k0 = k00 t for all (sh; ih); (s j; i j) 2 k0 ; (sh; ih) 0 (s j; i j) if and only if: 1. (sh; ih); (s j; i j) 2 k00 and (sh; ih) (s j; i j), or 2. (sh; ih); (s j; i j) 2 k0 n k00, or 3. (sh; ih) 2 k00; (s j; i j) 2 k0 n k00 and 9(sl ; il ) 2 k n 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
[
Example 2. Consider again the net in Figure 1 and the first part of the execution of Example 1, i.e. k0Jt2ik1. 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 tokens. Summing up, we have (k0; 0)Jt2i(k1; 1) where
1= 0 nf((si; ni); (s j; n j)) 2 k0 (si; ni) = (s2; 2) _ (s j; n j) = (s2; 2)g [ f((s1; 1); (s3; 1)); ((s2; 1); (s3; 1)); ((s2; 3); (s3; 1)); ((s3; 1); (s3; 1))g. 2
defined inductively as follows: (k; )Jei(k; ) is a firing sequence (where e denotes an empty sequence of transitions) and if (k; )Js i(k0; 0) is a firing sequence and (k0; 0)0Jti(k00; 00), then (k; )Jsti(k00; 00) is a firing sequence.
J(k; )i = f(k0; 0) 9s : (k; )Js i(k0; 0)g.
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 = f(s1; n1) : : : (s j; n j)g 2 IM(N) is finite, because k k. Therefore, Jinit(N)i is finite. 5.1
Given a transition sequence s , there is an operational preorder on tokens obtained by Definition 20, and a preorder derived from the process p obtained from the causal net C corresponding to the transition sequence s . In the following, we introduce some notation for processes and ordered indexed markings, and relate the two. If p = (C; r) is a process of a marked net N(m0) and k0 is the initial indexed marking for N(m0) (i.e. a(k0) = m0 and k0 is closed), we also say that p is a process of N(k0). Moreover, given a process p = (C; r) of a net N(k0) and s a complete transition sequence of C, we write init(N)Jpi(k; ) if init(N)Jr(s )i(k; ).
Theorem 1. Let p = (C; r) a process of N(k0) such that init(N)Jpi(k; ).
Then (k; )Jti(k0; 0) if and only if p !e p0 where r0(e) = t and init(N)Jp0i(k0; 0).
Proof. By induction on the sequence s :e where s is a complete transition sequence of
C. Complete proof in the preliminary full version of this article [
Example 3. In Figure 2(a), the same 5-bounded P/T net N as Figure 1 is depicted, together with its empty process (we omit the representation of its initial marking). Figure 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. k0Jt2ik1Jt1ik2. 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 pi 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 a) b) c) s1 1 u
2
J t 2 i s1 1 1 J t 1 i s1 2 (C0 (C1 (C2 conditions bij are minimal in the causal net C0 and mapped to tokens in the initial indexed 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 2 Min(C1) but b3 62 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 p2 , also (s2; 2) and (s3; 1) are not related by 2. 2 6
We now define a novel bisimulation relation based on ordered indexed markings,
generalizing the similar idea in [
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 ) 2 B, then: 8t1; k10; 01 such that (k1; 1)Jt1i(k10; 01), (where we assume k100 2 k1 t1 such that k10 = k100 t1 ), there exist t20; k20; 02 (where we assume k200 2 k2 t2 such that k20 = k200 t2 ), and for b 0 defined as 8(s1; n1) 2 k10; 8(s2; n2) 2 k20:
Our aim is to relate f c and oim and the idea is that two tokens are related by b 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 OIMbisimilarity coincide on P/T nets.
Theorem 2. (OIM-bisimilarity and FC-bisimilarity coincide) Let N = (S; A; T ) be a
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 [
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 [
In the same fashion as the preceding section, we now prove that also causal-net bisimilarity is decidable.
Definition 22. (OIMC bisimulation) Let N = (S; A; T ) be a P/T net. An OIMC bisimulation is a relation B OIM(N) OIM(N) P((S N) (S N)) such that if ((k1; 1); (k2; 2); b ) 2 B, then: j k1 j = j k2 j 8t1; k10; 01 if (k1; 1)Jt1i(k10; 01) (where we assume that k100 2 k1 k100 t1 ), then there exist t2; k20; 02 (where we assume k200 2 k2 k200 t2 ), and for b 0 defined as 8(s1; n1) 2 k10; 8(s2; n2) 2 k20: t1 such that k10 = t2 such that k20 =
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 [
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
We have extended Vogler’s proof technique in [
Decidability of fully-concurrent bisimilarity for bounded nets using the ordered
indexed marking idea was claimed to have been proved by Valero-Ruiz in his PhD thesis
[
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 [