Two resources (submarkings) are called similar if in any marking any one of them can be replaced by another one without affecting the net's behaviour (modulo marking bisimulation). It is known that resource similarity is undecidable for general labelled Petri nets. In this paper we study the properties of resource similarity and resource bisimulation (a subset of complete similarity relation, closed under transition firing) in Petri nets with invisible transitions (where some transitions may be unlabelled and hence invisible for external observer). It is shown that for a proper subclass - p-saturated nets - the weak transfer property of resource bisimulation can be effectively checked.
In this paper we consider an important generalization of labelled Petri nets, where some transitions may be unlabelled and hence invisible for external observer. Quite often when analyzing the system there is a need to abstract from the excessive information about its behavior. For example, it is convenient to hide all transitions, corresponding to the internal actions of the system. The information obtained in this case can be useful, in particular, to detect additional properties of the system in terms of its interaction with the environment.
Place bisimulations in Petri nets with invisible transitions were studied by
C. Autant et al. in [
In this paper we basically apply a similar approach to the resource equivalences. It is shown that, despite their non-trivial infinite structure, resource bisimulations can be effectively computed even in the case of nets with invisible transitions. In particular, it is shown that for a proper subclass — p-saturated nets — the weak transfer property of resource p-bisimulation can be effectively checked. Moreover, we can underapproximate the largest p-bisimulation by a parameterized algorithm.
The paper is organized as follows. Section 2 contains basic definitions. Specifically, in Subsection 2.1 we give some technical notions and lemmata on the properties of additively-transitively closed relations on multisets. Subsection 2.2 contains definitions of Petri nets and bisimulations. Subsections 2.3 and 2.4 give a short review on Petri net resources and resource equivalences (similarity and bisimulation). Section 3 deals with invisible transitions. In Subsections 3.1 and 3.2 we define the straightforward -generalizations of resource equivalences and study their properties. Subsections 3.3 and 3.4 describe the subclass of psaturated nets and the corresponding notion of p-bisimulation. In Subsection 3.5 we present an algorithm, computing the parameterized underapproximation of largest p-bisimulation. Section 4 contains some conclusions. 2 2.1
Let X be a finite set. A multiset m over a set X is a mapping m : X ! Nat, where Nat is the set of natural numbers (including zero), i.e. a multiset may contain several copies of the same element.
For two multisets m; m0 we write m m0 iff 8x 2 X : m(x) m0(x) (the inclusion relation). The sum and the union of two multisets m and m0 are defined as usual: 8x 2 X : m + m0(x) = m(x) + m0(x); m [ m0(x) = max(m(x); m0(x)). By M(X) we denote the set of all finite multisets over X.
Non-negative integer vectors are often used to encode multisets. Actually, the set of all multisets over finite X is a homomorphic image of NatjXj.
A binary relation R Natk Natk is a congruence if it is an equivalence
relation and whenever (v; w) 2 R then (v + u; w + u) 2 R (here ‘+’ denotes
coordinate-wise addition). It was proved by L. Redei [
Let RAT denote the additive-transitive closure (AT-closure) of the relation R M(X) M(X) (the minimal congruence, containing R).
Let B M(X) M(X) be a binary relation on multisets. A relation B0 is called an AT-basis of B iff (B0)AT = BAT . An AT-basis B0 is called minimal iff there is no B00 B0 such that (B00)AT = BAT .
Now we construct a special kind of minimal AT-basis for B: Define a partial order v on the set B M(X) M(X) of pairs of multisets as follows: 1. For loop (i.e. reflexive) pairs let (r1; r1) v (r2; r2) def r1 , r2; 2. For two non-loop pairs, the maximal loop constituents and the addend pairs of nonintersecting multisets are compared separately (r1 + o1; r1 + o01) v (r2 + o2; r2 + o02) def , def o1 \ o01 = ; & o2 \ o02 = ; & r1 , r2 & o1 o2 & o0 1 o0 : 2 3. A loop pair and a non-loop pair are always incomparable.
Let Bs denote the set of all minimal (with respect to v) elements of BAT .
Theorem 1. [
We call Bs the ground basis of B. Obviously, it is finite.
There is also a useful
Lemma 1. [
(r; a1); (a1; a2); : : : ; (ak 1; ak); (ak; s) 2 (Bs)A; where (Bs)A is the additive closure of Bs. 2.2
Let P and T be disjoint sets of places and transitions and let F : (P T ) [ (T P ) ! Nat. Then N = (P; T; F ) is a Petri net. A marking in a Petri net is a function M : P ! Nat, mapping each place to some natural number (possibly zero). Thus a marking may be considered as a multiset over the set of places. Pictorially, P -elements are represented by circles, T -elements by boxes, and the flow relation F by directed arcs. Places may carry tokens represented by filled circles. A current marking M is designated by putting M (p) tokens into each place p 2 P . Tokens residing in a place are often interpreted as resources of some type consumed or produced by a transition firing. A marked Petri net (N; M0) is a Petri net N together with an initial marking M0.
For a transition t 2 T the preset t and the postset t are defined as the multisets over P such that t(p) = F (p; t) and t (p) = F (t; p) for each p 2 P . A transition t 2 T is enabled in a marking M iff 8p 2 P M (p) F (p; t). An enabled transition t may fire yielding a new marking M 0 =def M t + t , i.e. M 0(p) = M (p) F (p; t) + F (t; p) for each p 2 P (denoted M !t M 0).
The transitions may fire in parallel (concurrently), if there are enough tokens for all of them. In particular, the transition may fire in parallel with itself. The concurrent firing of a multiset of transitions is called a parallel step. The precondition and postcondition for a multiset of transitions 2 M(T ) are: =def
X t; t2 =def
X t : t2 Obviously, ( + ) = + ; ( + ) = + :
To observe a net behavior transitions are labelled by special labels representing observable actions or events. Let Act be a set of action names. A labelled Petri net is a tuple N = (P; T; F; l), where (P; T; F ) is a Petri net and l : T ! Act is a labelling function. It can be generalized to sequences: for 2 T s.t.
= t with t 2 T and we have l( ) =def l(t)l( ):
2 M(T ) l( ) =def Pt2 l(t): Here we use not a union but a sum of multisets.
Let N = (P; T; F; l) be a labelled Petri net. We say that a relation R M(P ) M(P ) conforms to the transfer property iff for all (M1; M2) 2 R and t for every step t 2 T , s.t. M1 ! M10 , there exists an imitating step u 2 T , s.t.
u l(t) = l(u), M2 ! M20 and (M10 ; M20 ) 2 R.
A relation R is called a marking bisimulation, if both R and R 1 conform to the transfer property.
For every labelled Petri net there exists the largest marking bisimulation
(denoted by ) and this bisimulation is an equivalence. It was proved by P. Jančar
[
Informally, resources are parts of markings which may or may not provide this
or that kind of net behavior.
Definition 1. [
Resources r and s in N are called similar (denoted r s) iff for every marking R 2 M(P ), r R implies R R r + s.
Thus if two resources are similar, then in every marking each of these resources can be replaced by another without changing the observable system’s behavior. Some examples of similar resources are shown in Fig. 1. p1 p2 - a - a
Figure a) shows a Petri net containing two transitions labeled with the same label a and leading to the same marking p3. Here the resources p1 and p2 are similar, as they lead to a completely identical observable behavior — action a producing a single token in p3. Moreover, all the resources containing the same number of tokens in p1 and p2 are similar.
Figure b) shows a simple net consisting of a single transition. In this case the resource p2 is similar to an empty resource, since it does not affect the behavior of the net (the place p2 is redundant).
Figure c) depicts a cycle consisting of one transition and one place. Note that the set of markings of this net can be divided into two disjoint subsets — empty marking and all the others. With empty marking, the transition can not fire, for all others — it can fire any number of times. Note that for this net the largest marking bisimulation and the resource similarity coincide.
Figure d) shows a more complex network. We have p1 p2 + p3; that is, replacing one token in p1 by two tokens (one in p2 and one in p3) does not affect the observable behavior of the net as a whole.
The similarity relation is an equivalence [
Hence it has a finite ground basis. Unfortunately, from the undecidability of
a stronger relation of place fusion [
We defined a stronger equivalence relation, retaining the observable system’s
behavior:
Definition 2. [
M(P ) is called a re
Note that an AT-closure of a resource similarity is not necessarily a marking bisimulation. The next theorem states some important properties of resource bisimulations.
Theorem 3. [
Therefore B(N ) (as well as any other resource bisimulation) also has a finite ground basis.
The AT-closure of a resource bisimulation is a marking bisimulation, and hence, it conforms to the transfer property. Resource bisimulations satisfy a weak variant of the transfer property, when only ’adjacent’ markings are considered for a transition t:
We say that a relation B M(P ) M(P ) conforms to the weak transfer
property if for all (r; s) 2 B, for each t 2 T , such that t \ r 6= ;, there exists an
imitating transition u 2 T , such that l(t) = l(u) and, writing M1 for t [ r and
M2 for t r + s, we have M1 !t M10 and M2 !u M20 with (M10 ; M20 ) 2 BAT .
Theorem 4. [
Due to this theorem to check whether a given finite relation B is a resource
bisimulation, one needs to verify the weak transfer property for only a finite
number of pairs of resources. In [
In this section we investigate the possibilities of effectively constructing bisimulation-preserving relations for an extended class of systems — Petri nets with invisible transitions.
To distinguish visible and invisible transitions, a special symbol is added to the set of labels: Act = Act [ f g.
Definition 3. A labelled Petri net with invisible transitions is a tuple N = (P; T; F; l), where (P; T; F ) is a Petri net and l : T ! Act is an extended labelling function.
Let ; 0 2 (Act ) be sequences of action labels (with -s). Denote 0 ,def jAct = 0jAct (“equal modulo ”). For example, “ a ” = “a”. = 3.1
-bisimulation Let N = (P; T; F; l) be a labelled Petri net with invisible transitions. We say that a relation R M(P ) M(P ) conforms to the -transfer property iff for all t (M1; M2) 2 R and for every step t 2 T , s.t. M1 ! M10 , there exists an imitating sequence of steps 2 T s.t. l(t) = l( ), M2 ! M20 and (M10 ; M20 ) 2 R.
A relation R is called a marking -bisimulation, if both R and R 1 conform to the -transfer property. The largest -bisimulation is denoted by .
Marking bisimulation is a special case of -bisimulation (for nets with no s). It is a stronger relation. Consider as an example the net at Fig. 2. Markings p1 and p2 are not bisimilar, because at p2 no transition with label a is active. But they are -bisimilar, because the invisible firing of t2 changes the marking from p2 to p1.
p1 k s
p2 The definition of resource similarity can be naturally generalized to the case of nets with invisible transitions: Definition 4. Let N = (P; T; F; l) be a labelled Petri net with invisible transitions. Resources r and s are called -similar (denoted r s) iff for every marking R, r R implies R R r + s.
We can show that resource -similarity has all basic properties of resource similarity: Proposition 2. 1. Resource -similarity is closed under addition and transitivity; hence it has finite AT-basis. 2. Resource -similarity is undecidable.
Definition 5. Let N = (P; T; F; l) be a labelled Petri net with invisible transitions. An equivalence relation B M(P ) M(P ) is called a resource bisimulation if BAT is a marking -bisimulation.
Proposition 3. Let N = (P; T; F; l) be a labelled Petri net with invisible transitions. Then 1. if B M(P ) M(P ) is a resource -bisimulation and (r1; r2) 2 B then r1 r2; 2. if B1; B2 M(P ) M(P ) are resource -bisimulations then B1 [ B2 is a resource -bisimulation; 3. for any N there exists the largest resource -bisimulation (denoted by B (N )), and it is an equivalence.
Proof. The first statement follows directly from the definitions. Note, that there exists a resource -similarity which is not a -bisimulation.
The proof of the second statement is rather long and contains some technical details. It uses the decomposition of a given pair into a transitive chain of pairs, where pairs are constructed as sums of pairs from (B1)AT and (B2)AT .
The third statement is an immediate corollary of the second. The largest resource -bisimulation is the union of all resource -bisimulations for N . M1 = t [ r and M2 = t (M10 ; M20 ) 2 BAT .
Definition 6. We say that a relation B M(P ) M(P ) conforms to the weak -transfer property if for all (r; s) 2 B, t 2 T s.t. t \ r 6= ;, there exists an imitating sequence of transitions 2 T s.t. l(t) = l( ) and, denoting r + s, we have M1 !t M10 and M2 ! M20 with
Th. 4 in the case of Petri nets with invisible transitions works only in one direction: Proposition 4. If the relation conforms to the -transfer property then it conforms to the weak -transfer property; there exist relations, conforming to the weak -transfer property and not conforming to the -transfer property. Proof. ()) Since the weak -transfer property is the -transfer property for a bounded (finite) subset of pairs of resources.
(6() Consider a net at Fig. 3 (this example is taken from [
B = Id(P ) [ f(p1; p2); (p2; p1); (p3; p4); (p4; p3)g:
B conforms to the weak -transfer property. At the same time B is not a resource -bisimulation. Consider markings M1 = p1 + p3 and M2 = p2 + p4. The pair (M1; M2) belongs to the relation BAT , but the markings are not bisimilar, because an action a is possible at M2 (transition t3) and is impossible at M1. p1 t1 p2 m ? τ ? m
mp3 U ? τ
t2 - m?p4
Hence the weak -transfer property can not be used to construct bisimulation.
In the case of systems with invisible transitions it is even more important to
strengthen the considered relations and/or to restrict the considered class of
Petri nets.
There exists a wide and important subclass of Petri nets with invisible
transitions for which resource -bisimulation can be constructed using weak transfer
property — so-called “p-saturated nets”. In p-saturated nets [
=def f 2 T j l( ) 2 Act g: Definition 7. A labelled Petri net with invisible transitions N = (P; T; F; l) is called p-saturated (or simply saturated), if for any sequence of transitions 2 T there exists a parallel step U 2 M(T ) s.t. l(U ) = l( ), U = and U = .
p2 p2 m p1 - τ t1 - m
- a a) not saturated net saturating transition
t3 - a m p1 - τ t1 - m
- a
b) saturated net
In [
M ?? τ t3 ?
WWW
τ t4
saturating
transition
b) rst step of saturation
Definition 8. [
M20 and
Definition 9. [
It is known [
In saturated Petri nets p-bisimulation coincides with -bisimulation [
M1
M2:
Now we are ready to define a resource p-similarity: Definition 10. Let N = (P; T; F; l) be a saturated labelled Petri net with invisible transitions. Resources r and s are called p-similar (denoted r p s) iff for every marking R, r R implies R p R r + s.
p and
in saturated nets we immediately have: Corollary 1. Let N = (P; T; F; l) be a saturated labelled Petri net with invisible transitions, r; s 2 M(P ): Then r p s , r s:
So, in saturated nets it is sufficient to look for p-similarities.
Definition 11. Let N = (P; T; F; l) be a saturated labelled Petri net with invisible transitions. An equivalence relation B M(P ) M(P ) is called a resource p-bisimulation if BAT is a marking p-bisimulation.
In the case of p-relations all basic properties also hold: Proposition 5. 1. Resource p-similarity is closed under addition and transitivity; hence it has finite AT-basis. 2. Resource p-similarity is undecidable. 3. If B M(P ) M(P ) is a resource p-bisimulation and (r1; r2) 2 B then r1 p r2. 4. If B1; B2 M(P ) M(P ) are resource p-bisimulations then B1 [ B2 is a resource p-bisimulation; 5. For any N there exists the largest resource p-bisimulation (denoted by B p(N )), and it is an equivalence. Proof.
1) Immediately from the definition of resource p-similarity. 2) From Cor. 1 and the undecidability of ( ). 3) Immediately from the definitions.
4) The proof is almost the same as in Prop. 3: the only difference is that we consider not an imitating transition but an imitating parallel step.
5) Note that we can take a union of all resource p-bisimulations. Definition 12. Let N = (P; T; F; l) be a saturated labelled Petri net with invisible transitions. We say that a relation B M(P ) M(P ) conforms to the weak p-transfer property if for all (r; s) 2 B, t 2 T s.t. t \ r 6= ;, there exists an imitating parallel step U 2 M(T ) s.t. l(t) = l(U ) and, denoting M1 = t [ r and M2 = t r + s, we have M1 !t M10 and M2 !U M20 with (M10 ; M20 ) 2 BAT .
In saturated nets the weak p-transfer property is a necessary and sufficient condition for its extended version, which guarantees the imitation of a parallel step rather than a single transition: Definition 13. Let N = (P; T; F; l) be a saturated labelled Petri net with invisible transitions. We say that a relation B M(P ) M(P ) conforms to the extended weak p-transfer property if for all (r; s) 2 B and any parallel step V 2 M(T ) s.t. V \ r 6= ;, there exists an imitating parallel step U 2 M(T ) s.t. l(V ) = l(U ) and, denoting M1 = V [ r and M2 = V r + s, we have
V U M1 ! M10 and M2 ! M20 with (M10 ; M20 ) 2 BAT .
Lemma 2. Let N = (P; T; F; l) be a saturated labelled Petri net with invisible transitions. The relation B M(P ) M(P ) conforms to the weak p-transfer property iff it conforms to the extended weak p-transfer property. Proof. (() Since the weak transfer property is a special case of the extended weak transfer property.
()) Assume the converse: the extended property does not hold, so there exists (M1; M2) 2 BAT ; V = ft1; : : : ; tkg 2 M(T ) with M1 !V M10 , s.t. there exists no imitating parallel step U 2 M(T ) with the same visible label l(V ) =
U l(U ) and M2 ! M20 and (M10 ; M20 ) 2 BAT .
Consider the transition firing M1 !t1 M11. From the weak p-transfer property it follows that this transition has an imitating parallel step M2 W!1 M21 such that (M11; M21) 2 BAT .
Note that V = ft1; : : : ; tkg is a parallel step at marking M1, hence after the firing of one of these transitions all other are still enabled. Therefore we can repeat the previous reasoning for the new pair of markings (M11; M21) 2 BAT and transition t2. And continue this until tk:
M1 imitating the firing of parallel step M1 !V M10 . The net is saturated so for any sequence of transitions (note that a parallel step also can be considered as a sequence of transitions) there exists an imitating parallel step with the same U label, precondition and postcondition (M2 ! M20 ) – q.e.d.
Note that, unlike the weak transfer property, the extended weak transfer property can not be effectively checked by the search of resource pairs, since the set of parallel steps is infinite.
Theorem 5. Let N = (P; T; F; l) be a saturated labelled Petri net with invisible transitions. An equivalence relation B M(P ) M(P ) conforms to the weak p-transfer property iff B is a resource p-bisimulation.
Proof. (() Since the weak p-transfer property is the p-transfer property for a bounded (finite) subset of pairs of resources.
()) The proof is similar to the proof of Th. 4, with the additional use of Lm. 2.
Assume the converse: let BAT does not conform to the p-transfer property, t i.e. there exist (M1; M2) 2 BAT ; t 2 T with M1 ! M10 , s.t. there are no imitating U parallel step U 2 M(T ) with l(t) = l(U ), M2 ! M20 and (M10 ; M20 ) 2 BAT .
Consider a pair of markings (M1; M2) 2 BAT . From Lm. 1 this pair can be obtained by a transitive closure of several pairs from BA (additive closure of B): (H1; H2); (H2; H3); : : : ; (Hk 1; Hk) 2 BA, where H1 = M1; Hk = M2.
(H1; H2) = (r1 + r2 + : : : + rl; s1 + s2 + : : : + sl), where (ri; si) 2 B H1 = t [ r1 + F1. Due to the weak transfer property for the pair (r1; s1) t there exists an imitating parallel step V 2 M(T ) s.t. l(t) = l(V ), t [ r1 ! G1 and t r1 + s1 !V G2, where (G1; G2) 2 BAT .
Since t [ r1 H1, we can add the resource F = H1 t [ r1 to preconditions and postconditions: t t [ r1 + F !t G1 + F r1 + s1 + F !V G2 + F
From the reflexivity of B and the additive closure of BAT the new pair of markings is also decomposable by B : (G1 + F; G2 + F ) 2 BAT .
We obtained a new marking H10 = t r1 + s1 + F = H1 r1 + s1. Note that it still contains r2 + : : : + rl. Therefore, we can apply the same reasoning one more time, replacing resource r2 by the bisimilar resource s2, now using Lm. 2 and constructing an imitating parallel step not for a transition but for a parallel step V .
Apply this l 1 times. Using transitive closure of BAT , at the end we obtain a parallel step W that can imitate t at marking H2.
Now proceed to the next pair (H2; H3) and repeat the procedure for the parallel step W . And so on, until the last pair (Hk 1; Hk). Finally we obtain a parallel step U that can imitate t at marking Hk = M2.
Thus, in saturated nets the weak p-transfer property can be used in the construction of resource p-bisimulation. 3.5
As in ordinary Petri nets, in the case of saturated (saturable) nets with invisible transitions there is a way of constructing an approximation of the maximal resource p-bisimulation. If we consider not an infinite set of network resources, but only it’s finite subset, then it will be possible to check the weak p-transfer property.
Let N = (P; T; F; l) be a saturated labelled Petri net with invisible transitions, q 2 Nat — some parameter. By Mq(P ) we denote the set of all resources, containing not more then q tokens in the net: Mq(P ) = fr 2 M(P ) : jrj < qg.
The largest resource p-bisimulation on Mq(P ) is defined as the union of all resource p-bisimulations on Mq(P ). We denote it by B p(N; q). Since Mq(P ) is finite, we can use the weak transfer property to compute B p(N; q). Definition 14. (Underapproximation of largest resource p-bisimulation)
Input: A saturated labelled Petri net with invisible transitions N = (P; T; F; l), parameter q 2 Nat.
Output: Relation B p(N; q).
Step 1: Let C = f(;; ;)g — an empty set of pairs (considered as a relation over Mq(P )).
Step 2: Compute B = (Mq(P ) Mq(P )) n C. Since Mq(P ) is finite the set of pairs B is also finite.
Step 3: Compute Bs — the ground basis of B.
Step 4: Check, whether Bs conforms to the weak p-transfer property: it is sufficient to test all non-reflexive elements of Bs.
If all pairs conforms to the weak p-transfer property then stop and return B — the bisimulation.
Otherwise there are (r; s) 2 Bsnr and t 2 T with t \ r 6= ;, s.t. the firing M1 !t M10 with M1 = t [ r can not be imitated by a parallel step with the same label and with precondition M2 = t r + s. In this case add (r; s) and (s; r) to C and go back to Step 2.
For any marking the set of active parallel steps is finite. Also note that the set Mq(P ) Mq(P ) is finite. Hence the algorithm always stops.
Denote by R = jMq(P )j the size of the set of considered resources.
At the Step 2 we search through the set of all parallel steps with at most one visible label, that can fire at marking M2: Each invisible transition can participate in the parallel step at most jM2j times, since it uses at least one input token.1 There is also at most one visible transition. Hence we have to check at most jT jjM2jjT j multisets of transitions.
The size of marking M2 = t r + s can be evaluated as O(jsj) = O(q): Using our previous estimations of complexity for ground basis calculation (polynomial w.r.t. R) and the complexity of other steps of algorithm (polynomial w.r.t. the size of the net), we obtain the overall complexity of
O(maxfjP j R9; jT j2qjT jjP j R7g):
So in the case of nets with invisible transitions the complexity of the algorithm increased significantly (the linear dependence on jT j was replaced by an exponential one). Such a jump is explained by the transition from sets of transitions to multisets.
Consider an example of calculations (Fig. 6). With q = 1 we found that resource p2 is p-similar to an empty resource (i.e. the place p2 is redundant). Increasing the parameter (q = 2), we obtained one more pair of similar resources p1 p 2p3: 4
The proposed method for finding pairs of similar resources is of particular interest for certain applications. In addition, the use of resource bisimulation allows one to reduce a Petri net with conservation of its behavior. This reduction is 1 Without loss of generality we can assume that a net contains no invisible transitions with empty preconditions, since such transitions are redundant and can always be removed from the net along with places, included in their postconditions. ? m ? τ p1 m ? a t3 q τ t2 ?? mp3 ?? a t5 q = 1 : q = 2 : p2 ≈τ p ∅ p1 ≈τ p 2p3 important when analyzing properties of the Petri net, since the computational complexity of the majority of algorithms used in analysis depends exponentially on the size of the net.
Important open questions concern decidability and complexity of related algorithmic problems. For example, we have already shown that all types of resource similarity (ordinary, -, p-) are undecidable. On the other hand, the problem of B(N ) (and B (N ), and B p(N )) computability is still open. We have introduced only the underapproximations.
Acknowledgment. I would like to express my sincere gratitude to my mentor Irina Lomazova for her support and encouragement.