key: cord-0046626-jlnbgyzs
authors: Gorrieri, Roberto
title: A Study on Team Bisimulations for BPP Nets
date: 2020-06-02
journal: Application and Theory of Petri Nets and Concurrency
DOI: 10.1007/978-3-030-51831-8_8
sha: ce77d5fa4c65441e3c77f0d886e49679c9303190
doc_id: 46626
cord_uid: jlnbgyzs

BPP nets, a subclass of finite P/T nets, were equipped in [13] with an efficiently decidable, truly concurrent, behavioral equivalence, called team bisi-milarity. This equivalence is a very intuitive extension of classic bisimulation equivalence (over labeled transition systems) to BPP nets and it is checked in a distributed manner, without building a global model of the overall behavior of the marked BPP net. This paper has three goals. First, we provide BPP nets with various causality-based equivalences, notably a novel one, called causal-net bisimilarity, and (a version of) fully-concurrent bisimilarity [3]. Then, we define a variant equivalence, h-team bisimilarity, coarser than team bisimilarity. Then, we complete the study by comparing them with the causality-based semantics we have introduced: the main results are that team bisimilarity coincides with causal-net bisimilarity, while h-team bisimilarity with fully-concurrent bisimilarity.

A BPP net is a simple type of finite Place/Transition Petri net [18] whose transitions have singleton pre-set. Nonetheless, as a transition can produce more tokens than the only one consumed, there can be infinitely many reachable markings of a BPP net. BPP is the acronym of Basic Parallel Processes [4] , a simple CCS [11, 15] subcalculus (without the restriction operator) whose processes cannot communicate. In [12] a variant of BPP, which requires guarded sum and guarded recursion, is actually shown to represent all and only the BPP nets, up to net isomorphism, and this explains the name of this class of nets.

In a recent paper [13] , we proposed a novel behavioral equivalence for BPP nets, based on a suitable generalization of the concept of bisimulation [15] , originally defined over labeled transition systems (LTSs, for short). A team bisimulation R over the places of an unmarked BPP net is a relation such that if two places s 1 and s 2 are related by R, then if s 1 performs a and reaches the marking m 1 , then s 2 may perform a reaching a marking m 2 such that m 1 and m 2 are element-wise, bijectively related by R (and vice versa if s 2 moves first). Team bisimilarity is the largest team bisimulation over the places of the unmarked BPP net, and then such a relation is lifted to markings by additive closure: if place s 1 is team bisimilar to place s 2 and the marking m 1 is team bisimilar to m 2 (the base case relates the empty marking to itself), then also s 1 ⊕ m 1 is team bisimilar to s 2 ⊕ m 2 , where ⊕ is the operator of multiset union. Note that to check if two markings are team bisimilar we need not to construct an LTS, such as the interleaving marking graph, describing the global behavior of the whole system, but only to find a bijective, team bisimilarity-preserving match among the elements of the two markings. In other words, two distributed systems, each composed of a team of sequential, non-cooperating processes (i.e., the tokens in the BPP net), are equivalent if it is possible to match each sequential component of the first system with one team-bisimilar, sequential component of the other system, as in any sports where two competing (distributed) teams have the same number of (sequential) players.

The complexity of checking whether two markings of equal size are team bisimilar is very low. First, by adapting the optimal algorithm for standard bisimulation equivalence over LTSs [19] , team bisimulation equivalence over places can be computed in O(m · p 2 · log (n + 1)) time, where m is the number of net transitions, p is the size of the largest post-set (i.e., p is the least natural such that |t • | ≤ p for all t) and n is the number of places. Then, checking whether two markings of size k are team bisimilar can be done in O(k 2 ) time. Of course, we proved that team bisimilar markings respect the global behavior; in particular, we proved that team bisimilarity implies interleaving bisimilarity and that team bisimilarity coincides with strong place bisimilarity [1] .

In this paper, we complete the comparison between team bisimilarity on markings and the causal semantics of BPP nets. In particular, we propose a novel coinductive equivalence, called causal-net bisimulation equivalence, inspired by [9] , which is essentially a bisimulation semantics over the causal nets [2, 17] of the BPP net under scrutiny. We prove that team bisimilarity on markings coincides with causal-net bisimilarity, hence proving that our distributed semantics is coherent with the expected causal semantics of BPP nets. Moreover, we adapt the definition of fully-concurrent bisimulation (fc-bisimulation, for short) in [3] , in order to be better suited for our aims. Fc-bisimilarity was inspired by previous notions of equivalence on other models of concurrency, in particular, by history-preserving bisimulation (hpb, for short) [8] . Moreover, we define also a slight strengthening of fc-bisimulation, called state-sensitive fc-bisimulation, which requires additionally that, for each pair of related processes, the current markings have the same size. We also prove that causal-net bisimilarity coincides with state-sensitive fc-bisimilarity. These behavioral causal semantics have been provided for BPP nets, but they can be easily adapted for general P/T nets.

The other main goal of this paper is to show that fc-bisimilarity (hence also hpb) can be characterized for BPP nets in a team-style, by means of h-team bisimulation equivalence. (The prefix h-is used to remind that h-team bisimilarity is connected to hpb.) The essential difference between a team bisimulation and an h-team bisimulation is that the former is a relation on the set of places only, while the latter is a relation on the set composed of the places and the empty marking θ.

The paper is organized as follows. Section 2 introduces the basic definitions about BPP nets and recalls interleaving bisimilarity. Section 3 discusses the causal semantics of BPP nets. First, the novel causal-net bisimulation is introduced, then (state-sensitive) fully-concurrent bisimilarity, as an improvement of the original one [3] , which better suits our aims. Section 4 recalls the main definitions and results about team bisimilarity from [13] ; in this section we also prove a novel result: causal-net bisimilarity coincides with team bisimilarity for BPP nets. Section 5 defines h-team bisimulation equivalence and studies its properties; in particular, we prove that h-team bisimilarity coincides with fc-bisimilarity. Finally, Sect. 6 discusses related literature. 

Multiset union ⊕ is defined as follows: (m ⊕ m )(s) = m(s) + m (s); it is commutative, associative and has θ as neutral element. Multiset difference is defined as follows: (m 1 m 2 )(s) = max{m 1 (s)−m 2 (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 s i we also denote the multiset with s i as its only element. Hence, a multiset m over S = {s 1 , . . . , s n } can be represented as k 1 · s 1 ⊕ k 2 · s 2 ⊕ . . . ⊕ k n · s n , where k j = m(s j ) ≥ 0 for j = 1, . . . , n. Given a transition t = (s, , m), we use the notation:

• • t to denote its pre-set s (which is a single place) of tokens to be consumed; • l(t) for its label , and • t • to denote its post-set m (which is a multiset) of tokens to be produced.

Hence, transition t can be also represented as • t

We also define pre-sets and post-sets for places as follows:

Note that the pre-set (post-set) of a place is a set. 

A multiset over S is called a marking. Given a marking m and a place s, we say that the place s contains m(s) tokens, graphically represented by m(s) bullets inside place s. A BPP net system N (m 0 ) is a tuple (S, A, T, m 0 ), where (S, A, T ) is a BPP net and m 0 is a marking over S, called the initial marking. We also say that N (m 0 ) is a marked net. Note that reach(s) is always a finite set, even if [s is infinite.

Example 1. Figure 1 (a) shows the simplest BPP net representing a semi-counter, i.e., a counter unable to test for zero. Note that the number represented by this semi-counter is the number of tokens which are present in s 2 , i.e., in the place ready to perform dec; hence, Fig. 1 (a) represents a semi-counter holding 0; note also that the number of tokens which can be accumulated in s 2 is unbounded. Indeed, the set of reachable markings for a BPP net can be countably infinite. In (b), a variant semi-counter is outlined, which holds number 2 (i.e., two tokens are ready to perform dec).

Two markings m 1 and m 2 are interleaving bisimilar, denoted by m 1 ∼ int m 2 , if there exists an interleaving bisimulation R such that (m 1 , m 2 ) ∈ R.

Interleaving bisimilarity ∼ int , which is defined as the union of all the interleaving bisimulations, is the largest interleaving bisimulation and also an equivalence relation.

The definition above covers also the case of an interleaving bisimulation between two BPP nets, say, N 1 = (S 1 , A, T 1 ) and N 2 = (S 2 , A, T 2 ) with S 1 ∩ S 2 = ∅, because we may consider just one single BPP net N = (S 1 ∪ S 2 , A, T 1 ∪ T 2 ): An interleaving bisimulation R ⊆ M (S 1 ) × M (S 2 ) is also an interleaving bisimulation on M (S 1 ∪S 2 )×M (S 1 ∪S 2 ). Similar considerations hold for all the bisimulation-like definitions we propose in the following.

Remark 2 (Comparing two marked nets). The definition above of interleaving bisimulation is defined over an unmarked BPP net, i.e., a net without the specification of an initial marking m 0 . Of course, if one desires to compare two marked nets, then it is enough to find an interleaving bisimulation (over the union of the two nets, as discussed in the previous remark), containing the pair composed of the respective initial markings. This approach is followed for all the other bisimulation-like definitions we propose.

Continuing Example 1 about Fig. 1 , it is easy to realize that relation

k = k 1 + k 2 and k, k 1 , k 2 ≥ 0} is an interleaving bisimulation.

We start with the most concrete equivalence definable over BPP nets: isomorphism equivalence. Definition 6 (Isomorphism). Given two BPP nets N 1 = (S 1 , A, T 1 ) and N 2 = (S 2 , A, T 2 ), we say that N 1 and N 2 are isomorphic via f if there exists a type-preserving bijection f : S 1 ∪ T 1 → S 2 ∪ T 2 (i.e., a bijection such that f (S 1 ) = S 2 and f (T 1 ) = T 2 ), satisfying the following condition:

where f is homomorphically extended to markings (i.e., f is applied element-wise to each component of the marking:

Two BPP net systems N 1 (m 1 ) and N 2 (m 2 ) are rooted isomorphic if the isomorphism f ensures, additionally, that f (m 1 ) = m 2 .

In order to define our approach to causality-based semantics for BPP nets, we need some auxiliary definitions, adapting those in, e.g., [3, 9, 10] .

, the arcs of the net do not form any cycle. Note that a BPP causal net, being a BPP net, is finite; since it is acyclic, it represents a finite computation. Note also that any reachable marking of a BPP causal net is a set, i.e., this net is safe; in fact, the initial marking is a set and, assuming by induction that a reachable marking m is a set and enables t, i.e., m[t m , then also m = (m • t) ⊕ t • is a set, because the net is acyclic and because of the condition on the shape of the post-set of t (weights can only be 1).

N(m 0 ) = (S, A, T, m 0 ) satisfying the following conditions: 1. N is acyclic; 2. ∀s ∈ S | • s| ≤ 1 ∧ |s • | ≤ 1 (i.e., the places are not branched); 3. ∀s ∈ S m 0 (s) = 1 if • s = ∅ 0 otherwise; 4. ∀t ∈ T t • (s) ≤ 1 for all s ∈ S (i.e.,

causal net N(m 0 ) = (S, A, T, m 0 ), we can extract the partial order of its events

Two partial orders (T 1 , 1 ) and (T 2 , 2 ) are isomorphic if there is a labelpreserving, order-preserving bijection g : T 1 → T 2 , i.e., a bijection such that l 1 (t) = l 2 (g(t)) and t 1 t if and only if g(t) 2 g(t ).

We also say that g is an event isomorphism between the causal nets N 1 and N 2 if it is an isomorphism between their associated partial orders of events E N1 and E N2 .

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

N = (S, A, T, m 0 ) and N = (S , A, T , m 0 ), we say that N moves in one step to N through t, denoted by N[t N , if • t ∈ Max(N), T = T ∪ {t} and S = S ∪ t • ; in other words, N extends N by one event t.

which is type-preserving, i.e., such that ρ(S) ⊆ S and ρ(T) ⊆ T , satisfying the following: Definition 6) and

N (m 0 ), two of its processes (N 1 , ρ 1 ) and (N 2 , ρ 2 ) are isomorphic via f if N 1 and N 2 are rooted isomorphic via bijection f (seeρ 1 = ρ 2 • f .

Let N (m 0 ) = (S, A, T, m 0 ) be a BPP system and let (N i , ρ i ), for i = 1, 2, be two processes of N (m 0 ). We say that

We would like to define a bisimulation-based equivalence which is coarser than the branching-time semantics of isomorphism of (nondeterministic) occurrence nets (or unfoldings) [5, 7, 16] and finer than the linear-time semantics of isomorphism of causal nets [2, 17] . The proposed novel behavioral equivalence is the following causal-net bisimulation, inspired by [9] . 

Two markings m 1 and m 2 of N are cn-bisimilar (or cn-bisimulation equivalent), denoted by

Let us denote by ∼ cn R = (m 1 , m 2 ) m 1 is cn-bisimilar to m 2 thanks to R . Of course, cn-bisimilarity ∼ cn can be seen as

R is a causal-net bisimulation is the largest causal-net bisimulation by item 4 of the following proposition. Proposition 1. For each BPP net N = (S, A, T ), the following hold:

Proof. Trivial for 1, 2 and 4. For case 3, assume that (ρ 1 , N, Since (N, ρ 2 ) and (N,

Note that (N , ρ 2 ) and (N , ρ 2 ) are isomorphic via f , where f extends f in the obvious way (notably, by mapping transition t to t). As

Example 3. Consider the nets in Fig. 1 . Clearly the net in a) with initial marking s 1 and the net in b) with initial marking s 3 are not isomorphic; however, we can prove that they have isomorphic unfoldings [5, 7, 16] ; moreover, s 1 ∼ cn s 3 , even if the required causal-net bisimulation contains infinitely many triples.

Example 4. Consider the nets in Fig. 2 . Of course, the initial markings s 1 and s 2 do not generate isomorphic unfoldings; however, s 1 ∼ cn s 2 .

Example 5. Look at Fig. 3 . Of course, s 1 ∼ cn s 3 , even if they generate the same causal nets. In fact, s 1 a −→ s 2 might be matched by s 3 either with s 3 a −→ s 4 or with s 3 a −→ s 5 , so that it is necessary that s 2 ∼ cn s 4 or s 2 ∼ cn s 5 ; but this is impossible, because only s 2 can perform both b and c. Moreover, s 6 ∼ cn s 8 as they generate different causal nets.

Behavioral equivalences for distributed systems, usually, observe only the events. Hence, causal-net bisimulation, which also observes the structure of the distributed state, may be considered too concrete an equivalence. We disagree with this view, as the structure of the distributed state is not less observable than the events this distributed system can perform. Among the equivalences not observing the state, the most prominent is fully-concurrent bisimulation (fcbisimulation, for short) [3] . As we think that the definition in [3] is not very practical (as it assumes implicitly a universal quantification over the infinite set of all the possible extensions of the current process), we prefer to offer here an equivalent definition, by considering a universal quantification over the finite set of the net transitions only. We define also a novel, slightly stronger version, called state-sensitive fc-bisimulation equivalence, that we prove to coincide with cn-bisimilarity.

Let N = (S, A, T ) be a BPP net. An fc-bisimulation is a relation R, composed of triples of the form ((N 1 , ρ 1 ), g, (N 2 , ρ 2 )), where, for i = 1, 2, (N i , ρ i ) is a process of N (m 0i ) for some m 0i and g is an event isomorphism between N 1 and N 2 , such that if

, ρ 2 (t 2 ) = t 2 and ρ 2 (Max(N 2 )) = m 2 ; 4. g = g ∪ {(t 1 , t 2 )}, and finally, 5. ((N 1 , ρ 1 ), g , (N 2 , ρ 2 ) ) ∈ R; ii) symmetrically, if ρ 2 (Max(N 2 )) moves first. ((N, ρ), id, (N, ρ) ) ∃m. (N, ρ) is a process of N (m) and id is the identity event isomorphism on N} is an fc-bisimulation; that (ii) the inverse relation R −1 of an fcbisimulation R is an fc-bisimulation; that (iii) the composition

)} of two fc-bisimulations R 1 and R 2 is an fc-bisimulation; and finally, that (iv) the union i∈I R i of a family of fc-bisimulations R i is an fc-bisimulation. Fig. 3 we argued that s 6 cn s 8 ; however, s 6 ∼ fc s 8 , because, even if they do not generate the same causal net, still they generate isomorphic partial orders of events. On the contrary, s 1 fc s 3 because, even if they generate the same causal nets, the two markings have a different branching structure. Note that the deadlock place s 7 and the empty marking θ are fcbisimilar.

An fcbisimulation R is state-sensitive if for each triple ((N 1 , ρ 1 ), g, (N 2 , ρ 2 )) ∈ R, the maximal markings have equal size, i.e., |ρ 1 (Max(N 1 ))| = |ρ 2 (Max(N 2 ))|. Two markings m 1 and m 2 of N are sfc-bisimilar, denoted by m 1 ∼ sf c m 2 , if there exists a state-sensitive fc-bisimulation R containing a triple ((N 0 1 , ρ 0 1 ), g 0 , (N 0 2 , ρ 0 2 )), where N 0 i contains no transitions, g 0 is empty and

Of course, also the above definition is defined coinductively; as we can prove an analogous of Proposition 1, it follows that ∼ sf c is an equivalence relation, too. N, ρ 1 ), id, (N, ρ 2 ) ) (ρ 1 , N, ρ 2 ) ∈ R}, where id is the identity event isomorphism on N, is a state-sensitive fc-bisimulation. Since R contains the triple ((N 0 , ρ 0 1 ), id, (N 0 , ρ 0 2 )), it follows that m 1 ∼ sf c m 2 .

⇐) (Sketch). If m 1 ∼ sf c m 2 , then there exists a state-sensitive fc-bisimulation R containing a triple ((N 0 1 , ρ 0 1 ), g 0 , (N 0 2 , ρ 0 2 )), where N 0 i contains no transitions, g 0 is empty and ρ 0 i (Min(N 0 i )) = ρ 0 i (Max(N 0 i )) = m i for i = 1, 2, with |m 1 | = |m 2 |. Hence, N 0 1 and N 0 2 are isomorphic, where the isomorphism function f 0 is a suitably chosen bijection from Min(N 0 1 ) to Min(N 0 2 ). 1 We build the candidate causal-net bisimulation R inductively, by first including the triple (ρ 0 1 , N 0 1 , ρ 0 2 • f 0 ); hence, if R is a causal-net bisimulation, then m 1 ∼ cn m 2 .

Since ((N 0 1 , ρ 0 1 ), g 0 , (N 0 2 , ρ 0 2 )) ∈ R and R is a state-sensitive fully-concurrent bisimulation, if ρ 0

, ρ 2 (t 2 ) = t 2 and ρ 2 (Max(N 2 )) = m 2 ; 4. g = g 0 ∪ {(t 1 , t 2 )}, and finally, 5. ((N 1 , ρ 1 ), g, (N 2 , ρ 2 )) ∈ R, with |ρ 1 (Max(N 1 ))| = |ρ 2 (Max(N 2 ))|.

It is necessary that the isomorphism f 0 has been chosen in such a way that f 0 ( • t 1 ) = • t 2 . As |ρ 0 1 (Max(N 0 1 ))| = |ρ 0 2 (Max(N 0 2 ))| and |ρ 1 (Max(N 1 ))| = |ρ 2 (Max(N 2 ))|, it is necessary that t 1 and t 2 have the same post-set size; hence, N 1 and N 2 are isomorphic and the bijection f 0 can be extended to bijection f with the pair {(t 1 , t 2 )} and also with a suitably chosen bijection between the post-sets of these two transitions. Hence, we include into R also the triple (ρ 1 , N 1 , ρ 2 • f ). Symmetrically, if ρ 0 2 (N 0 2 ) moves first. By iterating this procedure, we add (possibly unboundedly many) triples to R. It is an easy observation to realize that R is a causal-net bisimulation. 

Proof ⇐). Of course, a state-sensitive fc-bisimulation is also an fc-bisimulation. ⇒). If there are no deadlock places, an fc-bisimulation must be state sensitive. In fact, if two related markings have a different size, then, since no place is a deadlock and the BPP net transitions have singleton pre-set, they would originate different partial orders of events. Proof ⇒). If m 1 ∼ fc m 2 , then there exists an fc-bisimulation R on N containing a triple ((N 0 1 , ρ 0 1 ), g 0 , (N 0 2 , ρ 0 2 )), where N 0 i contains no transitions, g 0 is empty and

} is an fc-bisimulation on d(N ). By Proposition 4, R is actually a state-sensitive fully-concurrent bisimulation on d(N ). Note that R contains the triple ((d(N 0 

is the restriction of ρ i on the places of d(N i ), for i = 1, 2, and g is such that

In this section, we recall the main definitions and results about team bisimulation equivalence, outlined in [13] . We also include one novel, main result: causal-net bisimilarity coincides with team bisimilarity. 

Note that, by definition, two markings are related by R ⊕ only if they have the same size; in fact, the axiom states that the empty marking is related to itself, while the rule, assuming by induction that m 1 and m 2 have the same size, ensures that s 1 ⊕ m 1 and s 2 ⊕ m 2 have the same size. An alternative way to define that two markings m 1 and m 2 are related by R ⊕ is to state that m 1 can be represented as s 1 ⊕ s 2 ⊕ . . . ⊕ s k , m 2 can be represented as s 1 ⊕ s 2 ⊕ . . . ⊕ s k and (s i , s i ) ∈ R for i = 1, . . . , k.

It is possible to prove that if R is an equivalence relation, then its additive closure R ⊕ is also an equivalence relation. Moreover, if R 1 ⊆ R 2 , then R ⊕ 1 ⊆ R ⊕ 2 , i.e., the additive closure is monotonic.

Two places s and s are team bisimilar (or team bisimulation equivalent), denoted s ∼ s , if there exists a team bisimulation R such that (s, s ) ∈ R. The team bisimulation R above is a very simple, finite relation, proving that s 1 and s 3 are team bisimulation equivalent. In Example 2, in order to show that s 1 and s 3 are interleaving bisimilar, we had to introduce a complex relation, with infinitely many pairs. In Example 3 we argued that s 1 ∼ cn s 3 , even if we did not provide any causal-net bisimulation (which would be composed of infinitely many triples). Fig. 2 . Of course, s 1 ∼ s 2 because the finite relation R = {(s 1 , s 2 ), (s 1 , s 3 ), (s 1 , s 4 )} is a team bisimulation. Actually, all the places are pairwise team bisimilar. In Example 4 we argued that s 1 ∼ cn s 2 , but the justifying causal-net bisimulation would contain infinitely many triples. Fig. 4 . It is easy to see that R = {(s 1 , s 4 ), (s 2 , s 5 ), (s 2 , s 6 ), (s 2 , s 7 ), (s 3 , s 8 ), (s 3 , s 9 )} is a team bisimulation. This example shows that team bisimulation is compatible with duplication of behavior and fusion of places.

It is not difficult to prove [13] that (i) the identity relation I S = {(s, s) s ∈ S} is a team bisimulation; that (ii) the inverse relation R −1 = {(s , s) (s, s ) ∈ R} of a team bisimulation R is a team bisimulation; that (iii) the relational composition R 1 • R 2 = {(s, s ) ∃s .(s, s ) ∈ R 1 ∧ (s , s ) ∈ R 2 } of two team bisimulations R 1 and R 2 is a team bisimulation; and, finally, that (iv) the union i∈I R i of team bisimulations R i is a team bisimulation. Remember that s ∼ s if there exists a team bisimulation containing the pair (s, s ). This means that ∼ is the union of all team bisimulations, i.e.,

Hence ∼ is also a team bisimulation, the largest such relation. Moreover, by the property listed above, relation ∼ ⊆ S × S is an equivalence relation.

It is well-known that the optimal algorithm for computing bisimilarity over a finite-state LTS with n states and m transitions has O(m· log n) time complexity [19] ; this very same partition refinement algorithm can be easily adapted also for team bisimilarity over BPP nets; it is enough to start from an initial partition composed of two blocks: S and {θ}, and to consider the little additional cost due to the fact that the reached markings are to be related by the additive closure of the current partition; this extra cost is related to the size of the post-set of the net transitions; if p is the size of the largest post-set of the net transitions, then the time complexity is O(m·p 2 · log (n+1)), where m is the number of the net transitions and n is the number of the net places.

Starting from team bisimulation equivalence ∼, which has been computed over the places of an unmarked BPP net N , we can lift it over the markings of N in a distributed way: m 1 is team bisimulation equivalent to m 2 if these two markings are related by the additive closure of ∼, i.e., if (m 1 , m 2 ) ∈∼ ⊕ , usually denoted by

Remark 6 (Complexity 2). Once ∼ has been computed once and for all for the given net (in O(m · p 2 · log (n + 1)) time), the algorithm in [13] checks whether two markings m 1 and m 2 are team bisimulation equivalent in O(k 2 ) time, where k is the size of the markings. In fact, if ∼ is implemented as an adjacency matrix, then the complexity of checking if two markings m 1 and m 2 (represented as an array of places with multiplicities) are related by ∼ ⊕ is O(k 2 ), because the problem is essentially that of finding for each element s 1 of m 1 a matching, ∼-related element s 2 of m 2 . Moreover, if we want to check whether other two markings of the same net are team bisimilar, we can reuse the already computed ∼ relation, so that the time complexity is again quadratic.

Continuing Example 8 about the semi-counters, the marking s 1 ⊕ 2 · s 2 is team bisimilar to the following markings of the net in (b): s 3 ⊕ 2 · s 5 , or s 3 ⊕ s 5 ⊕ s 6 , or s 3 ⊕ 2 · s 6 , or s 4 ⊕ 2 · s 5 , or s 4 ⊕ s 5 ⊕ s 6 , or s 4 ⊕ 2 · s 6 .

Of course, two markings m 1 and m 2 are not team bisimilar if there is no bijective, team-bisimilar-preserving mapping between them; this is the case when m 1 and m 2 have different size, or if the algorithm in [13] ends with b holding false, i.e., by singling out a place s i in (the residual of) m 1 which has no matching team bisimilar place in (the residual of) m 2 .

The following theorem provides a characterization of team bisimulation equivalence ∼ ⊕ as a suitable bisimulation-like relation over markings. It is interesting to observe that this characterization gives a dynamic interpretation of team bisimulation equivalence, while Definition 18 gives a structural definition of team bisimulation equivalence ∼ ⊕ as the additive closure of ∼. The proof is outlined in [13] . 

By the theorem above, it is clear that ∼ ⊕ is an interleaving bisimulation.

Let N = (S, A, T ) be a BPP net. If m 1 ∼ ⊕ m 2 , then m 1 ∼ int m 2 .

Theorem 3 (Team bisimilarity implies cn-bisimilarity). Let N = (S, A, T ) be a BPP net. If m 1 ∼ ⊕ m 2 , then m 1 ∼ cn m 2 .

Proof. Let R = {(ρ 1 , N, ρ 2 ) (N, ρ 1 ) is a process of N (m 1 ) and (N, ρ 2 ) is a process of N (m 2 ) such that ρ 1 (s) ∼ ρ 2 (s), for all s ∈ Max(N)}. We want to prove that R is a causal-net bisimulation. First, observe that, any triple of the form (ρ 0 1 , N 0 , ρ 0 2 ), where N 0 is a BPP causal net with no transitions, ρ 0 i (Max(N 0 )) = m i and ρ 0 1 (s) ∼ ρ 0 2 (s), for all s ∈ Max(N 0 ), belongs to R and its existence is justified by the hypothesis m 1 ∼ ⊕ m 2 . Note also that if the relation R is a causal-net bisimulation, then this triple ensures that m 1 ∼ cn m 2 . Now assume (ρ 1 , N, ρ 2 ) ∈ R. In order to be a causal-net bisimulation triple, it is necessary that i) ∀t 1 such that ρ 1 (Max(N))[t 1 m 1 , ∃t 2 , m 2 , t, N , ρ 1 , ρ 2 such that 1. Let t 1 be any transition such that ρ 1 (Max(N))[t 1 m 1 and let s 1 = • t 1 . Since by hypothesis we have that ρ 1 (s) ∼ ρ 2 (s), for all s ∈ Max(N), if s 1 = ρ 1 (s ), then there exists s 2 = ρ 2 (s ) such that s 1 ∼ s 2 . Hence, there exists t 2 such that

, so that, by Theorem 2, ρ 2 (Max(N))[t 2 m 2 and m 1 ∼ ⊕ m 2 . Therefore, it is really possible to extend the causal net N to the causal net N through a suitable transition t such that • t = s , as required above, and to extend ρ 1 and ρ 2 to ρ 1 and ρ 2 , respectively, in such a way that ρ 1 (s) ∼ ρ 2 (s), for all s ∈ t • because t • 1 ∼ ⊕ t • 2 . Summing up, for the move t 1 , we have that (ρ 1 , N , ρ 2 ) ∈ R because ρ 1 (s) ∼ ρ 2 (s), for all s ∈ Max(N ), as required. Symmetrically, if ρ 2 (Max(N)) moves first. Proof. By Corollary 2 and Theorem 1, we get the thesis.

Therefore, our characterization of cn-bisimilarity and sfc-bisimilarity, which are, in our opinion, the intuitively correct (strong) causal semantics for BPP nets, is quite appealing because it is based on the very simple technical definition of team bisimulation on the places of the unmarked net, and, moreover, offers a very efficient algorithm to check if two markings are cn-bisimilar (see Remarks 5 and 6).

We provide the definition of h-bisimulation on places for unmarked BPP nets, adapting the definition of team bisimulation on places (cf. Definition 19) . In this definition, the empty marking θ is considered as an additional place, so that the relation is defined not on S, rather on S ∪ {θ}; therefore, the symbols p 1 and p 2 that occur in the definition below can only denote either the empty marking θ or a single place.

• ∀m 1 such that p 1 −→ m 1 , ∃m 2 such that p 2 −→ m 2 and (m 1 , m 2 ) ∈ R ⊕ , • ∀m 2 such that p 2 −→ m 2 , ∃m 1 such that p 1 −→ m 1 and (m 1 , m 2 ) ∈ R ⊕ . p 1 and p 2 are h-team bisimilar (or h-team bisimulation equivalent), denoted p 1 ∼ h p 2 , if there exists an h-team bisimulation R such that (p 1 , p 2 ) ∈ R.

Since a team bisimulation is also an h-team bisimulation, we have that team bisimilarity ∼ implies h-team bisimilarity ∼ h . This implication is strict as illustrated in the following example.

Example 12. Consider the nets in Fig. 3 . It is not difficult to realize that s 6 and s 8 are h-team bisimilar because R = {(s 6 , s 8 ), (s 7 , θ)} is an h-team bisimulation. In fact, s 6 can reach s 7 by performing a, and s 8 can reply by reaching the empty marking θ, and (s 7 , θ) ∈ R. In Example 6 we argued that s 6 ∼ fc s 8 and in fact we will prove that h-team bisimilarity coincide with fc-bisimilarity.

Remark 7 (Additive closure properties). Note that the additive closure of an h-team bisimulation R does not ensure that if two markings are related by R ⊕ , then they must have the same size. For instance, considering the above relation R = {(s 6 , s 8 ), (s 7 , θ)}, we have that, e.g., s 6 ⊕ s 7 R ⊕ s 8 , because θ is the identity for multiset union. However, the other properties of the additive closure described in Sect. 4.1 hold also for these more general place relations.

It is not difficult to prove that, for any BPP net N = (S, A, T ), the following hold:

Hence, ∼ h is also an h-team bisimulation, the largest such relation. Moreover, by the observations above, relation ∼ h ⊆ (S ∪ {θ}) × (S ∪ {θ}) is an equivalence relation.

Starting from h-team bisimulation equivalence ∼ h , which has been computed over the places (and the empty marking) of an unmarked BPP net N , we can lift it over the markings of N in a distributed way: m 1 is h-team bisimulation equivalent to m 2 if these two markings are related by the additive closure of

is an equivalence relation.

Computing ∼ h is not more difficult than computing ∼. The partition refinement algorithm in [19] can be adapted also in this case. It is enough to consider the empty marking θ as an additional, special place which is h-team bisimilar to each deadlock place. Hence, the initial partition considers two sets: one composed of all the deadlock places and θ, the other one with all the non-deadlock places. Therefore, the time complexity is also in this case O(m · p 2 · log (n + 1)), where m is the number of the net transitions, n is the number of the net places and p the size of the largest post-set of the net transitions.

Once ∼ h has been computed once and for all for the given net, the complexity of checking whether two markings m 1 and m 2 are h-team bisimulation equivalent, according to the algorithm in [13] , is O(k 2 ), where k is the size of the largest marking, since the problem is essentially that of finding for each element s 1 (not ∼ h -related to θ) of m 1 a matching, ∼ h -related element s 2 of m 2 (and then checking that all the remaining elements of m 1 and m 2 are ∼ h -related to θ).

In this section, we first show that h-team bisimilarity over a BPP net N coincides with team-bisimilarity over its associated deadlock-free net d(N ). A consequence of this result is that h-team bisimilarity coincides with fc-bisimilarity on BPP nets. 

Team bisimilarity is the most natural, intuitive and simple extension of LTS bisimilarity to BPP nets; it also has a very low complexity, actually lower than any other equivalence for BPP nets. Moreover, it coincides with causal-net bisimilarity and state-sensitive fully-concurrent bisimilarity, hence it corresponds to the intuitively correct bisimulation-based causal semantics for BPP nets. Moreover, it coincides also with structure-preserving bisimilarity, because our causalnet bisimilarity is rather similar to its process-oriented characterization in [9] . From a technical point of view, team bisimulation seems a sort of egg of Columbus: a simple (actually, a bit surprising in its simplicity) solution for a presumedly hard problem. This paper is not only an addition to [13] , where team bisimilarity was originally introduced, but also an extension to a team-style characterization of fully-concurrent bisimilarity, namely h-team bisimilarity. We think that state-sensitive fc-bisimilarity (hence, also team bisimilarity) is more accurate than fc-bisimilarity (hence, h-team bisimilarity) because it is resource-aware, i.e., it is sensitive to the number of resources that are present in the net. This more concrete equivalence is justified in, e.g., the area of information flow security [14] .

Our complexity results for fc-bisimilarity in terms of the equivalent h-team bisimilarity (cf. Remark 8), seem comparable with those in [6] , where, by using an event structure [20] semantics, Fröschle et al. show that history-preserving bisimilarity (hpb, for short) is decidable for the BPP process algebra with guarded summation in O(n 3 · log n) time, where n is the size of the involved BPP terms.

However, this value n is strictly larger than the size of the corresponding BPP net. In fact, in [6] the size of a BPP term p is defined as "the total number of occurrences of symbols (including parentheses)", where p is defined by means of a concrete syntax. E.g., p = (a.0) | (a.0) has size 11, while the net semantics for p generates one place and one transition (and 2 tokens). For a comparison of team bisimilarity with other equivalences for BPP, we refer you to [13] .

In [13] we presented a modal logic characterization of ∼ ⊕ and also a finite axiomatization for the process algebra BPP (with guarded sum and guarded recursion). As a future work, we plan to extend these results to ∼ ⊕ h , hence equipping fc-bisimilarity (and hpb) with a logic characterization and an axiomatic one for the process algebra BPP.

The identity relation I S = {(s, s) s ∈ S} is an h-team bisimulation

R} of an h-team bisimulation R is an h-team bisimulation

the relational composition R 1 • R 2 = {(p, p ) ∃p .(p, p ) ∈ R 1 ∧

R 2 } of two h-team bisimulations R 1 and R 2 is an h-team bisimulation

Strong bisimilarity on nets revisited

Sequential and concurrent behavior in Petri net theory

Concurrent bisimulations in Petri nets

Decidability and decomposition in process algebra

Branching processes of Petri nets

Non-interleaving bisimulation equivalences on basic parallel processes

Petri net models for algebraic theories of concurrency

Equivalence notions for concurrent systems and refinement of actions

Structure preserving bisimilarity, supporting an operational petri net semantics of CCSP

The non-sequential behaviour of Petri nets

Introduction to Concurrency Theory: Transition Systems and CCS. EATCS Texts in Theoretical Computer Science

Process Algebras for Petri Nets: The Alphabetization of Distributed Systems. EATCS Monographs in Theoretical Computer Science

Team bisimilarity, and its associated modal logic, for BPP nets. Acta Informatica

Interleaving vs true concurrency: some instructive security examples

Communication and Concurrency

Petri nets, event structures and domains, part I. Theor

Nets, Terms and Formulas

Petri Net Theory and the Modeling of Systems

Three partition refinement algorithms

Event structures

Acknowledgments. The anonymous referees are thanked for their comments.

Proof. If m 1 ∼ cn m 2 , then there exists a causal-net bisimulation R containing a triple (ρ 0 1 , N 0 , ρ 0 2 ), where N 0 is a BPP causal net which has no transitions andLet us consider a pair (s 1 , s 2 ) ∈ R. Hence, there exist a triple (ρ 1 , N, ρ 2 ) ∈ R and a place s ∈ Max(N) such that s 1 = ρ 1 (s) and s 2 = ρ 2 (s). If s 1 moves, e.g.,Since R is a causal-net bisimulation, ∃t 2 , m 2 , t, N , ρ 1 , ρ 2 such that 1. Note that t is such that • t = s, and so • t 2 = s 2 . This means that m 2 = ρ 2 (Max(N)) s 2 ⊕ m 2 , where m 2 = t • 2 ; in other words, t 2 = s 2 −→ m 2 . Note also that ρ 1 extends ρ 1 by mapping t to t 1 and, similarly, ρ 2 extends ρ 2 by mapping t to t 2 ; in this way,Summing up, for (s 1 , s 2 ) ∈ R, if s 1 −→ m 1 , then s 2 −→ m 2 such that (m 1 , m 2 ) ∈ R ⊕ ; symmetrically, if s 2 moves first. Therefore, R is a team bisimulation.