Structural analysis of High-Level Petri Nets is a powerful technique, but it is less supported than in PNs. A symbolic calculus for Symmetric Nets (SNs) has been developed and implemented, which allows one to check structural properties directly on SNs without unfolding: however it is limited to a particular form of composition, restricted to functions that map to sets. To complete the calculus for more general applications the ability to solve the composition of general SN arc expressions in a symbolic way is required. In literature, a few papers show how to solve this operation for a restricted category of SN. In this paper, we formalize the algebraic composition of general SN bag-functions. Some applications are also discussed.
The possibility of checking some properties of PN models on their structure
instead of (or before) generating their state space is a strong point in favour of
the PN formalism. The extension of the structural analysis techniques to High
Level Petri Nets (HLPNs), without resorting to unfolding, has been considered in
the literature and some interesting results have been published [
A contribution in this direction has been proposed in [
Paper organization: Some de nitions and notations are introduced in Sec. 1.1 and 1.2. Sec.s 2 and 3 introduce some useful de nitions and properties, while in Sec. 4 we describe the steps to solve the general composition of SN functions. In Sec. 5 two example applications are illustrated. Sec. 6 concludes the paper and outlines directions for future work. 1.1
A (generalized) bag b over a domain A is a map b : A ! Z. Bag[A] is the set of bags over A. Let a 2 A and b 2 Bag[A]: we write a 2 b if and only if b(a) 6= 0. The set b = fa; a 2 bg is the support of b. The bag with an empty support, is denoted ;A or just ; if its domain is clear from the context. Bags b1; b2 2 Bag[A] are disjoint if and only if b1 \ b2 = ;. A proper bag is a map b : A ! N. The set of proper bags over A is denoted Bag+[A]. The size of b 2 Bag+[A], jbj, is Pa b(a). Bag b is type-set if 8a 2 b b(a) = 1. A bag b 6= ; may be represented as a formal sum Pa2A b(a):a. Let b1; b2 2 Bag[A], k 2 Z. The scalar product k b1 and the sum (di ) b1 b2 are operations in Bag[A] de ned as (k b1)(a) = b1(a) k and b1 b2(a) = b1(a) b2(a), 8a 2 A. Operator + is associative, is associative on Bag[A], not on Bag+[A], + is commutative. ; is the neutral element for +, .
The Cartesian product is de ned as follows. Let b1 2 Bag[A], b2 2 Bag[B]: b1 b2 2 Bag[A B] is b1 b2(ha; bi) = b1(a) b2(b), 8a 2 A; b 2 B. The notation hb1; b2; : : :i is used in place of b1 b2 : : :. The Cartesian product is associative and may be distributed over inner +; : h: : : ; b1 op b2; : : :i, op 2 f+; g = h: : : ; b1; : : :i op h: : : ; b2; : : :i. Finally, h: : : ; k b1; : : :i = k h: : : ; b1; : : :i.
Generalized bags allow to distribute composition over sum or di erence: in our context it simpli es the symbolic treatment of general composition. 1.2
Note: GreatSPN GUI syntax Cij and Xij ++ correspond to Si;j and !Xij, respectively.
Fig. 1. A SN example: Producers and Consumers
The SN formalism belongs to the HLPN class: places and transitions are associated with a color domain C(:) expressing the possible colors of tokens and of the transition instances. Arcs are annotated by expressions, representing functions from C(t) to multisets Bag+[C(p)]; W (p; t) and W +(p; t) denote t input and output arc expressions. The structure of a color annotation is based on the de nition of color classes ( nite not empty sets), which may be partitioned into (static) subclasses or be circularly ordered, and on a restricted set of basic functions: Si; Si;k; Xi; !Xi namely di usion/synchronization (on class Ci or subclass Ci;k), projection Xij and successor !Xij (only for ordered classes). Color domains are de ned as Cartesian products of n classes, where classes may be repeated. The arc expressions are weighted sums of tuples (Cartesian product) of basic functions (see Def. 4). The SN in Fig.1, represents a classical inter process communication example: producer and consumer processes communicating through a bu er (FIFO queue). There are two color classes, C1 (circularly ordered, representing the position of messages in the bu er) and C2 (id of producers/consumers), partitioned into two subclasses C21; C22. The places color domains are C2, C1, C1 C2 (tokens are tuples of one or two elements); some places and one transition in this net have neutral color (as in PNs, e.g. place empty and transition ProduceBurst). The transitions have color domain C2, C1 C2, C1 C22, depending on the projection symbols appearing on their arcs; transition Get has a guard : a predicate restricting the allowed color instances. Arc expressions in Fig.1 are quite simple: hX21i, h!X11i, hX11; X22i, hS2;2i. A guard is a boolean expression whose terms can be either (Xij = Xik)/(!Xij = Xik) or Xij 2 Ci;k. An example of transition instance is Get(pos1; pc1; pc2): it satises the guard (the two colors pc2; pc3 2 C2 belong to the same subclass C22), and the projection X11(pos1; pc2; pc3) = pos1, while X12(pos1; pc2; pc3) = pc2, X22(pos1; pc2; pc3) = pc3, nally !X11(pos1; pc2; pc3) = pos2. A more formal de nition of the SN arc expressions is deferred to Def. 4. Produce burst has only one instance since the functions hS22i on its arcs are constant, mapping on C22.
An incidence matrix can be derived from the SN structure:
N is a P T matrix of functions: C[p; t] = W +(p; t) W (p; t). If a transition instance t(c) enabled in marking mi res, the corresponding state change can be de ned in terms of the incidence matrix as: mj = mi + C[:; t](c). Among the structural analysis techniques that can be applied to SN models those based on the de nition of P and T-semi ows allow to check interesting invariant properties of the model. The general composition proposed in this paper enables such possibility by allowing to compose the functions in C with T or P-indexed vectors of functions to check if they are semi ows, as discussed in Sec. 5. 2
Operators op 2 f+; g on functions mapping to Bags are de ned as follows, in terms of Bag-operations. Let f; h : A ! Bag[D], op 2 f+; g: (f op h)(a) = f (a) op h(a), (k f )(a) = k f (a), 8a 2 A. The constant function mapping to the null bag is denoted A;D (or just ).
Let ffi : A ! Bag[Di]g be a family of functions: the function-tuple hf1; f2; : : :i (or ifi), is a map A ! Bag[D1 D2 : : :]: hf1; f2; : : :i(a) = hf1(a); f2(a); : : :i.
The properties of operations on bags, as well as the type-set notion, apply to bag-functions by considering all function arguments. We call any expression built of bag-functions a bag-expression.
De nition 2 (composition). Let f : A ! Bag[D], h : C ! Bag[A]. Then f h : C ! Bag[D] is f h(c) = f (h(c)), 8c 2 C, where f : Bag[A] ! Bag[D] is the linear extension of f de ned as f (b) = Pa2A b(a) f (a), 8b 2 Bag[A]. We shall use the same symbol for a function and its linear extension. When a function takes a bag as an argument we implicitly refer to its linear extension.
The possibility to distribute composition over a di erence or sum during the symbolic calculus, thanks to generalized bags, is very helpful because a complex composition may be reduced to an algebraic sum of simpler ones.
Bag-expressions may be pre xed by lters and su xed by guards, both expressed as predicates. A [true] guard/ lter is usually omitted. Let p : A ! ftrue; f alseg. A lter or guard [p] is a function A ! Bag[A] such that [p](a) = 1 a if p(a) = true, [p](a) = ; otherwise. Let f : A ! Bag[D], and p0 be a predicate on D. The expressions f [p] and [p0]f stand for f [p] and [p0] f , respectively. The following de nition characterizes an important class of functions. De nition 3 (constant-size function). f : A ! Bag+[D] is constant-size i 9n 2 N+ such that 8a 2 A f (a) 6= ; ) jf (a)j = n.
Hereafter, with f constant-size we mean f f 0[p], with f 0[p] = i p = f alse. The following two general properties of composition concern constant and constant-size functions.
B ! Bag[D] be a constant function so de ned: f (b) = d; 8b 2 B. And let h[g] : A ! Bag[B] be a n constant-size function, where h[g](a) = ; i g(a) = f alse. Then, the composition f h[g] is de ned as follows: 8a 2 A, f h[g] = n f 0[g], where f 0[g] : A ! Bag[D] is such that 8a 2 A; g(a) = true ) f 0(a) = d.
function. Then hf; f 0i h = hf h; f 0i.
Since f and f 0 might be tuples in turn, Property 2 applies (up to a permutation of tuple positions) to any T h, where T := hf1; : : : ; fmi contains some constant components and others non-constant. We may thus reduce such a composition to T 0 h, where T 0 is built of all and only the non-constant components fi of T . In the sequel, we focus on this case.
Let us anticipate the main result presented in this paper by introducing the language used to calculate and express the composition of SN functions. De nition 4 (Language Lc). Let - D = C1e1 C2e2 ::: Cnen ; e 2 N, be any color domain, i.e., a Cartesian product of colour classes ( ei = 0 means that Ci doesn't occur on D). - BiD = nXij ; Si; Si;k; !sXij : D ! Bag[Ci]o; i : 1; : : : ; n; j : 1; : : : ; ei; k : 1; : : : ; jjCijj; s 2 Z; be the set of elementary functions, where !s denotes the s-th modjCij successor on Ci (!sXij !s Xij , !0 = id) 4. - Tj : D ! Bag[D0], Tj = hf1; : : : fli, and 8r : 1; : : : ; l, fr : D ! Bag[Ci], fr = Pm m hm, m 2 Z, hm 2 BiD; fr is said a class-function. - gj0 and gj be SN predicates on D0 and D, respectively, such that all class functions appearing in Tj [gj ] map to proper bags when gj is true.
L c = nE : D ! Bag[D0]; E = X j [gj0 ]Tj [gj ]; 8D; D0o; j 2 Z j Any class-function fr has as implicit guard: the guard of the tuple it belongs to. Theorem 1. Lc is closed under composition.
The properties and lemmas presented in the rest of the paper justify the
claim above5. Before that, let us point out a few interesting facts about Lc.
Lc includes SN arc-functions, where scalars are such that they map to Bag+[D0].
The possibility of pre xing function-tuples with lters makes Lc slightly more
expressive than the language of SN arc-functions, and has recently been included in
the GreatSPN GUI. With respect to the language (L) of SN structural relations
de ned in [
The next important properties of Lc directly follow from the de nition of Lc,
the Cartesian product and lter/guard properties, and the basic predicate
reductions listed in [
Property 4 (type-set equivalence). Any E 2 Lc can be rewritten into E0 2 Lc, E0 E, in which class-functions (therefore, function-tuples) are type-set. Property 5 (constant-size function). Any class-function fr is constant-size when considering its implicit guard. jfrj is the weighted algebraic sum of sizes of elementary terms of fr. A function-tuple not pre xed by a lter is constant-size. Its size is the product of sizes of tuple's components.
For instance, j(S1 X11 X12)j, with the implicit guard X11 6= X12, is equal to jC1j 2. This expression is also type-set.
A function-tuple pre xed by a lter may not be constant-size. An example is [X11 = X12]hS1 X12; S1 X11i: the size of this function-tuple depends on whether the 1st and 2nd element of a color-tuple argument are the same or not, it is jCj 1 when applied to hc; ci and jCj 2 when applied to hc; c0i; c 6= c0. Observe that the projection symbols appearing in the lter refer to the elements of the tuple (X1j is the j-th element of class C1 in the tuple), and should not be confused with the projection symbols appearing within the tuple or the guard. Property 6 (constant-size equivalence). Any E 2 Lc can be rewritten into E0 2 Lc, E0 E, uniquely composed of constant-size terms.
Thus, if needed, we can transform any expression into an equivalent sum of constant-size (and/or type-set) terms. We will return to this in Section 4.1.
When calculating a Cartesian product, we have to take care of possible lters. Since we consider domains ordered by color, we only have to deal with two cases. Property 7 (Lc tuple Cartesian product with lters adaptation).
Let F1; F2 2 Lc, F1 : D ! D0, F1 = [g1]T1; F2 : D ! D00, F2 = [g2]T2, such that D0, D00 are either a) disjoint or b) D0 = Cim, D00 = Cin, n; m 2 N+.
Then hF1; F2i = [g1 ^ g2 ]hT1; T2i, where g2 = g2 in case a), g2 is obtained by replacing each Xij in g2 with Xij+m in case b).
All results we are presenting hold modulo a permutation of tuple elements. 3.1
Lower-case letters f; g; h; p denote class-functions and predicates, if enclosed between angular and square brackets, respectively, otherwise represent any bagexpression (like in Section 2). Upper case F denotes any expression in Lc whereas T any (guarded) function-tuple in Lc. V ar(f ) denotes the set fXjig of variables (projections) appearing in f : if f = [g]f 0[g0] then V ar(f ) = V ar(f 0) [ V ar(g0).
Let X be a non-empty set of typed variables: f (X) denotes a function such that V ar(f ) = X. We may list all function variables, e.g., f (Xij ; Xhw) meaning that V ar(f ) = fXij ; Xhwg. The subset Xi X holds the class-Ci variables. Index restriction r Let D: C1e1 ::: Cnen , f = f (X) : D ! Bag[D0], and e0j = jXj j (by the way, e0j ej ). The index restriction of f is a function f r: C1e01 ::: Cne0n ! Bag[D0], obtained from f by replacing symbols in Xji 2 Xj , in superscript order, e0 with Xj1; : : : ; Xj j , for each j, e0j < ej .
For example, let T = hX11 + 2X13; X13; X22i: C13 C22 ! C12 C2, then T r = hX11 + 2X12; X12; X21i : C12 C2 ! C12 C2.
Let X be a set fXjig, Xji : D ! Cj .
Domain projection By convenience, we assume X ordered, rst by class index then by superscript. We say the tuple X;D : D ! D0 =
Xji2X Xji projection of D (on D0) induced by X. D is omitted when clear from the context. Projection image X Let T 0 = hh1; : : : ; hmi with codomain D. The image of X on T 0 is the subtuple T X0 = i:9Xji2X hi, with the same domain as T 0. We denote by T :0X the residual sub-tuple of T 0. 4
Composing Lc expressions Let T : D ! Bag[D0], T 0 : D00 ! Bag[D], D = C1e1 ::: Cnen , X = V ar(T ) and V ar(T ) 6= ;. Tuple T may have a guard, i.e., T = hf1; : : : ; fni[g]. Solving T T 0 means being able to rewrite this expression into F 2 Lc.
The algorithm to solve composition operates top-down. Each step is described in detail in this section. We proceed by making assumptions more and more stringent on T; T 0, until we get a base form.
Figure 2 outlines the main steps of the composition procedure on an example. At each step some rewriting rule is applied, possibly involving a sub-term (highlighted using under-braces): it is described in the legend along with the reference(s) to the corresponding lemma(s).
We hereafter assume to have preliminarily operated all generic reductions described in Sec.2 (see e.g. the rst step in the example of Fig. 2), thus we let T be hf1; : : : ; fni[g], where 8i V ar(fi) 6= ;, and T 0 = hh1; : : : ; hmi. Property 8. T = T r X .
A rst basic result says that we can solve T T 0 by considering T r and the image of V ar(T ) on T 0.
Lemma 1. Let T = T (X) and T X0 6= T 0. If T :0X is of constant-size k, then: T
T 0[g0] = k T r
T X0 [g0] Lemma 1 is applied twice in Fig. 2; follows a third example (j2S1 X12j = 2jC1j 1): hX11; X11; S1 X13i hS1; 2S1 X11; S1;1+X12i = (2jC1j 1) hX11; X11; S1 X12i hS1; S1;1+X12i Based on Lemma 1 (and Property 6), we focus on tuple compositions where the image of left tuple's variables coincides with the entire right tuple.
A second basic result allows one to distribute a composition over the independent parts of the left operand (up to a permutation of tuple elements). 4
5 6 9
10 composition's result rule short description 1 constant pulled-out of the left tuple 2,8 left tuple restriction and projection on the right tuple 3,6 distribution of composition on independent left sub-tuples 4 reduction (move) of a membership clause of g 5 distribution property, reduction to a simple tuple-pre x 7 elimination of an in-between guard built of inequalities 9 distribution property and composition of a left constant 10 elementary composition 11, 12 basic composition (variable repetitions on the left tuple) reference(s) Property 2 Lemma 1
Lemma 2
see [
Claim 1, Def. 5 Corollary 2, Lemma 5
Property 1 Sect. 4.1 (table)
Property 14 3 12 7 1 2 8 11
Let T = hF1(X1); : : : ; Fh(Xh)i ^ 8i; j; i 6= j; Xi \ Xj = ;, ^T X0 = T 0.
T
T 0 = hF1r
T X01 ; : : : ; Fhr
T X0h i
In other words, one can separately compose independent sub-tuples of T with their images on T 0, whatever form they have. As a consequence, due to color independence, one can partition T (and T 0) in sub-tuples based on color-classes. indeWx einthbearesifcorfeu nfocctiuosnso:nXfujnrcetpiolanc-teuspXlejs, CSiej !replCaice0esanSdi;j h,eSreareftpelracoemsiSti.clWases i assume that monochromatic tuples do not include independent sub-tuples.
Lemma 2 exploits a nice property of linear extension of Cartesian product of bag-functions by which, if an argument is in turn a product of bags, it is possible to evaluate the product-function in a modular way.
In Fig. 2 this Lemma is applied twice; follows another non-trivial example: hX1; X3; S
X2; X2i[X1 6= X3 ^ X2 6= X4] hS; 2S X11; S; S1 + 2X2i = hhX1; X3i[X1 6= X3]; hS
X2; X2i[X2 6= X4]i hS; 2S
X1; S; S1 + 2X2i Le=m:2 hhX1; X2i[X1 6= X2] hS; Si; hS
X1; X1i[X1 6= X2] h2S
X1; S1 + 2X2ii
The two compositions that we ended up with are representatives of the base cases of tuple composition we have to solve. 4.1
We can identify a few base cases of function-tuple composition as a result of Lemma 2 application. One in which the left-hand tuple is a one-variable function and the right tuple is a singleton. The others in which there is an in x predicate (guard/ lter) that cannot be eliminated. The presence of an in x predicate complicates the solution of a composition. Based on properties of lters and lter reduction rules we may reduce such expressions to a particular form. The following statements assume that the right operand of a composition (T 0) is possibly followed by a guard.
Let T 0 = hh1; : : : ; hmi. A tuple-pre x [g]T 0 is simple if and only if 1. g is a conjunction of (in)equalities, such that for each clause (Xi =6=!sXj ) in g: hi is type-set, jhij > 1, and hi =!shj 2. let g= [ g6= be the partition of g in equalities and inequalities (a) if g6= 6= ;, each partition g1 [ g2 of g6= is such that V ar(g1) \ V ar(g2) 6= ; (b) if g= 6= ;, then g= may be partitioned in g=i; : : : ; g=w, w 2 N+, such that 8i; j, i 6= j, V ar(g=i) \ V ar(g=j) = ; 8g=i V ar(g=i) \ V ar(g6=) = fXj g
tuple-pre x and 8i jV ar(g=i) \ V ar(T )j 1.
In other words, if required we may assume that in x predicates are made of (in)equalities between projections which point to equal (modulo-successor) typeset class-functions of T 0 of size > 1. Equalities de ne equivalence classes of projections, one representative of each class must appear in inequalities, and at most one occur on T . In Fig. 2 steps 4 and 5 lead to a form satisfying Def.5; follows another example: Let (jC2j > 1):
X3; X1i[X1 6= X2 ^ X1 2 C2 ^ X1 = X3] hS; S; S + X1i ! X1; X1i[X1 6= X2 ^ X1 = X3] hS2; S2; S2i+ X1; X1i[X1 = X3] hS2; S
S2; S2i + hS2
X1; X1i hX1; S
X1; X1i[X1 2 C2]
Tuples pre xed by a lter matching De nition 5 have an important property. Property 9. A simple tuple-pre x [p]T : D ! Bag[D0] is constant-size. Four base cases have to be considered, they are listed below. 1. T (X1) hhi 2. T (X)[g] T 0, with jXj > 1 and X 3. T (X)[g] T 0, with X V ar(g) 4. T [g] T 0, with V ar(T ) \ V ar(g) = ; V ar(g) Case 1: T (X1) hhi In absence of in x predicates, we can always reduce to one such form due to the distribution property of sum/di . For example: hS
X1 +2X2; X2i hh1; h2i = h(S
X1) hh1i; X1 hh2ii+2jh1j hX1; X1i hh2i Case 1.a: jhj = 1; this is the simplest situation.
Property 10. Let jhj = 1. Then F (X1) hhi is obtained by replacing each occurrence of symbol X1 in F with h.
It directly follows from the de nition of composition.
For example, hS + X1; X1i hh2i, jh2j = 1 ! hS + h2; h2i.
Case 1.b: jhj > 1. The basic compositions are summarized in the following table (omitting tuple notation),the rst one is applied in Fig. 2, step 10: X1
Basic composition rules and some useful identities h = h !sX1 h =!sh S X1 h = jhj S h S !rX1 !rS = S !s!rXi =!s+rXi !r(h1 h2) =!rh1 !rh2 h = jhj S !rh
If T = hf1(X1)i the above basic rules (and property 2) are enough. For example, letting jC1j = 3: h2S X1 !X1i hS X2i ! h4S S + X2 S+!X2i h2S + X2+!X2i. Repetition of a projection in T Let T = hf1(X1); : : : ; fm(X1)i, where (without loss of generality due to Property 4) fi(X1) =!si X1, 8i (symbol !sXi from now on denotes a projection possibly pre xed by the s-th successor). We consider rst an unordered color class, then we generalize. As an example:
h!X1; X1; !X1i hS X2i = [X1 =!X2 ^ X1 = X3]hS !X2; S X2; S !X2i. In some cases may treat the idiom S X1 as a single function for convenience. Here are two situations that are more e ciently processed applying the following properties, although they could be solved applying the previous rules. Without loss of generality, in both cases S X1 is the last element of T . Property 13. Let h be a type-set function.
hX1; : : : ; X1; S X1i hhi = [X1 6= Xm Vi:2:::m 1 X1 = Xi] hh; : : : ; h; Si | {mz } | {mz } If there are no repetitions of X1 then h may be any function.
Property 14. hX1; S
X1i hhi = [X1 6= X2]hh; Si Case 2: T(X)[g] T0; jXj > 1; X Var(g) In this and in the next case we may assume, without loss of generality, that g is composed of (in-)equalities and T = hf1; : : : ; fmi, where fi =!si Xj , 8i. Consider, for example:
hX2; !X2; X3; !2X1i[X1 6= X3 ^ X1 6= !X2] hh1; h2; h3i
This expression doesn't match Lc. However, we can transform the guard in between into a lter pre xing the left tuple through an index substitution, i.e., an injective map : V ar(T ) ! f1 : : : mg associating each Xi to the position of any of its occurrences in T . The picture below illustrates the idea.
hX2; !X2; X3; !2X1i[X1 6= X3 ^ X1 6= !X2]:
The following rule formalizes the move of a clause of a guard g to a lter pre xing T (Xi =6= !kXj Xj =6= ! kXi). 6 if b is any bag, hX1; : : : ; X1i(b) is obtained from [Vi:2:::m X1 = Xi]hb; : : : ; bi by applying the mth root to multiplicities of bag elements
be any two occurrences of variables Xi; Xj , i 6= j, in tuple T .
(i) (j) h: : : ; !rXi; : : : ; !sXj ; : : :i[Xi =6= !kXj ; : : :] | {Tz } ! [X (i) =6= !k+r sX (j)]T [: : :] Corollary 1. Let T [g], with T = hf1; : : : ; fmi and g be a set of (in)equalities. If 8Xi 2 V ar(g) there is fj , fj =!sXi, then 9p T [g] [p]T .
Therefore, if V ar(T ) V ar(g) the reiterated application of Lemma 3 eventually removes the in x guard from T (X)[g] T 0.
Applying Lemma 3 to the last example,we can proceed with Lemma 2. Lem:3
! Lem:2 !
[X4 6=!2X3 ^ X4 6= !2X2]hX2; !X2; X3; !2X1i hh1; h2; h3i [X4 6=!2X3 ^ X4 6= !2X2]hhX1; !X1i hh2i; X1 hh3i; !2X1 hh1ii Case 3: T (X)[g] T 0, X V ar(g) This situation is the most complex one. The reason is that we must project on X = V ar(T ) the application of the lter g on T 0, in a symbolic way.
We assume that g is no further reducible, the composition to solve matches De nition 5 and none of lemmas presented so far applies (in particular Lemma 1, thus TV0 ar(g) = T 0).
Let A V ar(g): we say gA = f(Xi =6=!rXj ) 2 gjXi; Xj 2 Ag the restriction of g to variables A.
A rst simpli cation comes from the fact that we may take out equalities of g. We recall that f r denotes the index-restriction of f .
Property 15. Let [g]T 0 meet De nition 5, g= 6= ;, X0 = X [ V ar(g6=). Then T (X)[g] T 0 = (T [g6=])r
T X00 This nice property stems from the fact that (by De nition 5) T 0 components are equal (modulo successor) and in T only one symbol per equivalence class is used. Here are some examples of application of Property 15. For simplicity, in all the following examples X = fX1; : : : ; Xmg (T = T r). 1) hX1; S
X1i[X1 = X2; X1 = !X3] hS !X2; S !X2; S hX1; S
X1i hS !X2i P ro!p:14 [X1 6= X2]hS !X2; Si 2) hX1; !X2i[X1 6= !X2; X2 = X3] hS !X2; S X2; S
X2i P rop:15
! X2i P rop:15 ! hX1; !X2i[X1 6= !X2] hS !X2; S
X2i Lem:3;Lem:2 [X1 6= X2]hS !X2; S !X2i ! (hX2; X2i[X1 6= X2; X2 6= X4])r
hS1; S1; S1; S1ifX1;X2;X4g hX2; X2i[X1 6= X2; X2 6= X3] hS1; S1; S1i (non-reducible with the available rules) (1) (2) Main sub-case: g = g6= We may therefore assume that g is a non-empty set of inequalities and focus on X [g]T 0.
In general, we gure out that it holds
X
Equation 1 says that, disregarding bag multiplicity, the projection of [g]T 0 on V ar(T ) is included in the restriction of [g] to V ar(T ) which applies to the image of V ar(T ) on T 0. It follows from our assumptions, by which: g ) gX . In the sequel, we characterize particular forms [g]T 0 verifying
X
[g]T 0 = k [gX ]r T X0 ; k 2 N showing that (modulo some rewriting) we can always reduce our expression to such a form. An immediate corollary of (2) is: Corollary 2. Let T = T (X), X tuple-pre x (De nition 5). Then: T (X)[g] T 0 = k T r[gX ]r
T X0 , where k = j[gjX[g]]rTT0jX0 j if j[gX ]rT X0 j 6= 0, otherwise Corollary 2 outlines that we bring a composition to a form where the variables of the left tuple are a super-set of those of the in x predicate.
Consider this simple but interesting case where T [g] : C3 ! C2, T 0 : C ! C3. hX1; X2i[X1 6= X3 ^ X2 6= X3] hS
T g
X1; S
X1S T 0
X1i jCj > 2 In this case condition (2) is not veri ed: for any c 2 C, jCj > 2: fX1;X2g
[g]T 0(c) turns out to be,
X c02C;c06=c (jCj 2) hc0; c0i + (jCj 3)
X c0;c002C;c06=c;c006=c;c06=c00 hc0; c00i
The restriction of g[T 0] to X = fX1; X2g used on the right-hand side of (2), instead, is hS X1; S X1i (in this particular case, gX = fg). As the example suggests, we should distinguish (in g) the case X1 = X2 from the case X1 6= X2.
Since we are assuming that the requirements of De nition 5 are met, we may conveniently study [g]T 0 as a system of inequalities (in case of ordered classes, the successors are all expressed modulo-jCj) among V ar(g) variables, with the implicit constraints Xi 2 hi(c), 8Xi 2 V ar(g), hi being the i-th component of T 0. Thus, [g]T 0(c) is a type-set bag which corresponds to the system's solutions, while X [g]T 0(c) is a bag representing their projection on subset X.
Due to the symmetry of g and to the fact that functions hi are equal (modulo successor), we can abstract from both c and i and consider any hi as a (parametric) set of known size.
We put some conditions on g to ensure that the projection of the inequality system's solutions on X is the parametric multi-set consisting of k instances of the solutions of the sub-system restricted to X, i.e., [gX ]r T X0 .
We consider rst an unordered color-class C. In that case, hi = h, 8i, and we may represent g as an undirected simple graph whose vertices are V ar(g) and whose edges connect vertices corresponding to variables that are required to be di erent by a term of g. Abusing notation, we denote the same way g and the corresponding graph, leaving the context to disambiguate. Thus, we may interpret gX as a (proper) subgraph of g.
A few basic results of graph-colouring theory turn out to be useful for our
purposes (refer to [
P (G; ) can be expressed as a polynomial in , called chromatic polynomial of
G. This is interesting, since it gives us the possibility to express a composition's
result in a parametric way. Computing G is around O(2n), and computing
P (G; ) is at least as complex. [
P (G; ) = P (G xy; ) + P (G + xy; ). { Let G include Kr and G0 be obtained from G by adding a new vertex x which is (uniquely) linked to all vertices of Kr. Then P (G0; ) = P (G; )( r) { Some known polynomials: P (Kr; ) = ( 1) ( r + 1); if G is an empty graph of order n, P (G; ) = n; . . .
Any solution of the inequality system [g]T 0 (g, from now on) corresponds in fact to a -colouring of g with = jhj, therefore, denoting with Sol(g; ) the number of solutions of the inequality system, P (g; ) = Sol(g; ). k = 0, where
= jhij, for any hi in T 0.
Lemma 4. Let [g]T 0 be a simple tuple-pre x, X V ar(g), and gX be a clique. Then, equation (2) holds and (Corollary 2) k = P (PK(jgX; j;) ) if jXj, otherwise It is su cient to observe that for any two distinct -colourings of gX there are (obviously) the same number of -colourings of g that include them. Moreover, we know that Kr = r and g gX .
We are always able to reduce a composition to the condition that meets Lemma 4 by linking non-adjacent vertices of gX . Two such vertices are two unrelated variables Xi; Xj 2 X, therefore we rewrite T [g][T 0] into the equivalent sum T [g ^ Xi 6= Xj ]T 0 + T [g ^ Xi = Xj ]T 0. Note that g ^ Xi = Xj , after symbol replacement and removal of redundant inequalities (according to De nition 5) exactly corresponds to g Xi Xj .
By recursively rewriting and applying variable substitutions accordingly in T we eventually get sub-compositions solvable with the lemmas above. Let us instantiate this simple procedure and Lemma 4 on the last example. hX1; X2i[X1 6= X3 ^ X2 6= X3] hS X1; S X1S; X1i = jCj 1 (> 1) T g T 0 hX1; X2i[X1 6= X3 ^ X2 6= X3 ^ X1 6= X2] T 0 + hX1; X1i[X1 6= X3] T 0 hX1; X2i ( (
What if predicate g of the lter pre xing tuple T 0 is de ned on an ordered class? In theory, the situation is even simpler because we can always rewrite any inequality into a disjunction of equalities: for example, if jCj = 3: X1 6=!X2 X1 =!2X2 _ X1 = X2. So, by expanding T [g]T 0 accordingly we eventually get a solvable form.
This approach, however, may be ine cient and is not parametric. Therefore, we slightly extend the technique based on graph-representation of g to ordered classes. The graph representing g now has as vertices the symbols Symb(g) = f!rXj g occurring in g and as edges, in addition to inequalities in g, those implied by them: for any two symbols !rXj ; !sXj 2 Symb(g), there is a corresponding edge in the graph7. In this case, a -colouring of g doesn't necessarily match a solution of the inequality system, i.e., P (g; ) Sol(g; ),
Due to the circularity of C there are a number of equivalent representations for g. A rst result concerns those cases where g may be expressed in a form such that jV ar(g)j = jSymb(g)j, i.e., for each variable there is one corresponding symbol. In this case the previous results, in particular Lemma 4, still hold. When jV ar(g)j < jSymb(g)j instead, an extension of Lemma 4 is needed. Sol(gX ; ) > 0, otherwise k = 0, where = jhij, for any hi in T 0.
Xi 2 V ar(g)nX any two inequalities between X and Xi use the same symbol !rXi and b) gX is a clique, then equation (2) holds and k = SSool(l(ggX;; )) if We can always rewrite any predicate g so that it meets condition a) of Lemma 5. Condition a) is redundant if jXj = 1.
Observe that for computing Sol(g; ), for any inequality graph g, we can use
similar basic techniques as for the chromatic polynomial. See Fig. 2, step 7 and
[
This section presents two application examples: the symbolic veri cation of
invariants in SN models, and the reduction of nets by agglomeration of transitions,
enabling more e cient qualitative analysis (as in behavior preserving
reductions [
C(y) ! Bag[C([t)]; t 2 T ; y is a T-semi ow if C y = nully. A T-semi ow de nes a (parametric) set of transition instances; given a color c 2 C(y) if all the transition instances in y(c) can re (in any order) starting from marking m, they bring back the model to the same marking m.
Where nully is a P-indexed vector of functions such that nully[p] is a constant function mapping any c 2 C(y) into a constant empty Bag on C(p). In Table 1 two T-semi ows of the producers-consumers SN are listed. Their interpretation is quite simple8: In order to reproduce a marking the pointers rst and last should be increased by one jC1j times, hence the producers should produce jC1j items and put them into the bu er, and the consumers should get jC1j items from the bu er. In T1 the same producer lls completely the bu er and a consumer with the same id of the producer empties it (it represents jC2j invariants in the unfolded net). In T2 any combination of jC1j producers and jC1j consumers (satisfying the invariant guard g0) is possible. The expressions 8 Initialization transition init cannot belong to any T-invariant, while additional invariants involving ProduceBurst exist, but are not included for the sake of space. Transition T1 T2 (Hp: jC1j = 4) (Domain) C2 C28; C1 [g0] Produce (C2) jC1jhX21i hX21i + hX23i + hX25i + hX27i
Put (C1; C2) hSC1 ; X21i Pi3=0h!i X11; X22i+1i Get [g](C1; C22) hSC1 ; X21; X21i Pi3=0h!i X11; X22i+1; X22(i+1)i
End Process (C2) jC1jhX21i hX22i + hX24i + hX26i + hX28i 1) allowing to verify that vectors Tj correspond to parametric T-semi ows are: 8p 2 P; Pt2T C[p; t] Tj [t] = C(p); the function Tj [t] has domain C(Ti) and codomain C(t), so that the domains of the functions to be composed are coherent. Observe that T2 represents 625 T-invariants in the unfolded net when jC1j = 4, jC21j = 1 and jC22j = 2.
Let's check whether the transitions in T1 produce a null change on all places. Producing: W +(Put,Producing) T 1[Put] - W (Produce; Producing) T 1[Produce] = hX21i jC1jhX21i hX21i jC1jhX21i = C1 ( the equations for Wait to insert, Wait to extract and Processing are very similar). bu er: W +(Put; bu er) T 1[Put] W (Get; bu er) T 1[Get] = hX11; X21i hSC1 ; X21i hX11; X21i[g] hSC1 ; X21; X21i = hSC1 ; X21i hSC1 ; X21i = C1;C2 full: W +(Put; full) T 1[Put] W (Get; full) T 1[Get] = hSC i hX11; X21i hSC i[g] hX11; X21; X21i = C (the equation for empty is very similar) rst:W +(Get; rst) T 1[Get] W (Get; rst) T 1[Get] = h!X11i[g] hSC1 ; X21; X21i hX11i[g] hSC1 ; X21; X21i = hSC1 i hSC1 i = C1 (the equation for last is very similar) T2 has color domain C1; C28 where 8 = 2jC1j, completed by guard g0 (see Table1); and similar formulae as for T1 apply to it, let us consider the expressions for just a few places to illustrate the type of composition to be solved. bu er: W +(Put; bu er) T 2[Put] W (Get; bu er) T 2[Get] = hX11; X21i (hX11; X21i[g0] +h!X11; X23i[g0] + h!2X11; X25i[g0] + h!3X11; X27i[g0]) (hX11; X21i[g] (hX11; X21; X22i[g0] + h!X11; X23; X24i[g0] + h!2X11; X25; X26i[g0] + h!3X11; X27; X28i[g0]) = C1;C2 Wait to insert: W +(Produce; Wait to insert) T 2[Produce] W (Put; Wait to insert) T 2[Put] = hX21i (hX21i+hX23i+hX25i+hX27i)[g0] (hX21i (hX11; X21i[g0]+h!X11; X23i[g0]+ h!2X11; X25i[g0] + h!3X11; X27i[g0]) = C2 Observe that in all cases where transition Get is involved we have an in x guard g whose terms check which static sublcass X21 and X22 belong to: it is easily handled both in T1 (where the involved elements of the right tuple are equal) and in T2 (where the T-semi ow guard g0 implies that g is satis ed). Finally, note that depending on the actual binding of the T-psemi ow variables to colors, functions Tj [Produce] and Tj [End Process] map to a Bag+[C2] that may have coe cients greater than one. Hence the composition presented in this paper is required to verify the invariant.
Reduction of transitions. Another application of multiset composition in coloured
PN is structural reduction. For instance, in [
Transitions agglomeration is a useful reduction: it consists of merging causally connected transitions. The aim is to reduce transition instances interleaving, preserving speci c system properties. A number of techniques have been proposed, with di erent properties and applicability conditions. Common to most proposals is this applicability scenario: a set H of transitions put tokens into a place p, leading to a new marking of p from which it is possible to restore its initial state only through the ring of a newly enabled transition t0; in that case, the ring of any transition in H may immediately cause the ring of t0, without interfering with any other transition ring. In this paper, we do not propose a general agglomeration technique for SN, rather, we illustrate how to perform agglomeration by symbolically deriving the arc functions for the new transition. We also provide an intuitive structural condition on SN arc functions, which ensures the applicability of agglomeration in a limited set of cases.
Figure 3(a.1) shows a simple example where the transitions t and t0 can be agglomerated. Figure 3(a.2) depicts a part of the net unfolding connected to the instance h1i of t. It is possible to see that, if p is initially empty, after the ring of instance h1i of t, we can safely re immediately all the newly enabled instances of t0 restoring the p empty state. This is true for any instance hii of t. Figure 3(a.3) is the reduced colored subnet, where the size of class C is a parameter.
The reduced subnet can be obtained without unfolding it: indeed, for this type of agglomeration, the following formula allows to symbolically compute the arc functions of the reduced subnet9:
W (tt0; r) = W (t; r); W +(tt0; q) = W +(t0; q) W (t0; p)t W +(t; p) In W +(tt0; q) the rightmost composition provides the instances of t0 enabled by the ring of an instance of t, through p. Finally composing W +(t0; q) with this result ( ring t0 for all those instances) we obtain a function providing the multiset of tokens to be added in q. For the example of Fig.3(a) W (tt0; r) = hXi, while:
W +(tt0; q) = hS Xi hXit hSi = hS Xi hSi = (jCj 1):hSi jC=j=3 2:hSi
Figure 3(b.1) shows another example of reduction. The formula for the
agglomeration can be also used here. The agglomeration is valid for any jCj 2:
9 W (t0; p)t : C(p) ! Bag[C(t)] denotes the transpose of W (t0; p); the rules to
symbolically compute the transpose of an arc function are de ned in [
For these examples where p is the only input place of t0 and is the only output place of t, we can con dently state that if (1) the instances of transition t0 are not in con ict with each other (a situation called auto-con ict, which can be checked symbolically on the net structure) and (2) if all the tokens put into p by t can be completely consumed by (one or more instances of) t0, then we can aggregate t and t0. To verify the second condition it is su cient to check the following equality: W +(t; p) = W (t0; p) W (t0; p)t W +(t; p). The following property characterizes the form for the input function W (t0; p) which guarantees the agglomeration conditions(s). Let the identity on D be IdeD(d) = 1 d, 8d 2 D. Property 16. Let C(p)0 = W +(t; p)(C(t)) be the (support of the) image of W +(t; p). W +(t; p) = W (t0; p) W (t0; p)t W +(t; p) , 8c 2 C(p)0W (t0; p) W (t0; p)t(c) = 1 c (i.e. the restriction of W (t0; p) W (t0; p)t to C(p)0 is the identity).
Observe that with the assumption that p is the unique intermediate place
between t and t0, this property includes also the condition of no autocon icts
among t0 instances (= W (t0; p)t W (t0; p) Ide, simpli ed formula from [
The condition holds for both the examples discussed above, and this can be checked symbolically exploiting the composition presented in this paper. Finally, let us consider a third example, fully exploiting the composition technique presented in this paper. The subnet schema is the same but for t0, which has one more output place, q0. The arc functions for this example are: W (t; r) = hXi
W +(t; p) = hS !X; S; S
Xi W +(t0; q) = h!X2; X2i[X1 = X3] W (t0; p) = h!X3; X2; X1i
W +(t0; q0) = 2 hX1; X2i[X1 6= X2 ^ X2 6= X3] The arc functions for the agglomerated transition tt0 are ( = jCj with jCj > 2): W (tt0; r) = hXi W +(tt0; q0) = 2(
W +(tt0; q) = (
1)[X1 =!X2]hS; Si 1)hS
X; Xi + 2(
The detailed explanation of the steps leading to the result, involving the
application of Lemmas 1 to 4, is in Appendix A.3 of [
This paper reaches the goal of completing the symbolic manipulation of SN arc functions de ning a procedure for the composition of functions mapping on Bags. This enables a number of applications that couldn't be treated with the operations de ned so far. The implementation of a new version of SNexpression including this kind of composition is ongoing. The approach suggests an extension to the SN formalism itself, to allow lters in arc expressions: this feature is now implemented in the GreatSPN Graphical User Interface. The presented results are often parametric in color class cardinality, possibly with some constraints on cardinality lower bounds.
Future work is devoted to extend the possible applications of the results
presented in this paper, in particular as concerns a generalization of net reduction
methods proposed in literature to a wider class of nets: for instance, we expect
that our proposal may allow to relax some restriction posed in [