=Paper=
{{Paper
|id=Vol-2907/paper8
|storemode=property
|title=General Composition for Symmetric Net Arc Functions with Applications
|pdfUrl=https://ceur-ws.org/Vol-2907/paper8.pdf
|volume=Vol-2907
|authors=Lorenzo Capra,Massimiliano De Pierro,Giuliana Franceschinis
|dblpUrl=https://dblp.org/rec/conf/apn/CapraPF21
}}
==General Composition for Symmetric Net Arc Functions with Applications==
https://ceur-ws.org/Vol-2907/paper8.pdf
General composition for Symmetric Net arc
functions with applications
L. Capra1 , M. De Pierro2 , and G. Franceschinis3
1
Dip. di Informatica, Università di Milano, Italy
2
Dip. di Informatica, Università di Torino, Italy
3
DISIT, Università del Piemonte Orientale, Alessandria, Italy
Abstract. 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 unfold-
ing: 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 ex-
pressions 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 pa-
per, we formalize the algebraic composition of general SN bag-functions.
Some applications are also discussed.
1 Introduction
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 [11,13], however
the applicability of the proposed methods is often limited to particular classes
of HLPNs and not completely supported by software tools.
A contribution in this direction has been proposed in [6,4] for models repre-
sented with the Symmetric Net (SN) formalism: it consists of a symbolic calculus
operating on the arc expressions of the formalism, allowing to derive several in-
teresting structural properties in a symbolic and parametric form; the software
tool SNexpression [7] (http://www.di.unito.it/∼depierro/SNexpression/) im-
plements the results developed so far in this direction. One limitation of such
calculus concerned the composition operator, which could be applied only to the
support of arc expressions (hence to functions mapping to sets): although this
is sufficient for the computation of several symbolic structural relations (e.g.
symbolic structural conflict or causal connection [5]) it is not enough e.g. for
checking some invariant properties based on the definition of P and T-semiflows,
or for applying model reduction by agglomeration of transitions, two techniques
Copyright © 2021 for this paper by its authors. Use permitted under Creative
Commons License Attribution 4.0 International (CC BY 4.0).
136 L. Capra, M. De Pierro, and G. Franceschinis
that have been applied to concurrent programs verification [11]. This paper fills
the gap by defining the theory allowing to symbolically apply the composition
operator to general SN arc functions.
Paper organization: Some definitions and notations are introduced in Sec. 1.1
and 1.2. Sec.s 2 and 3 introduce some useful definitions 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 Generalized Bags: basic definition, notation and properties
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 ∈ A and b ∈ Bag[A]: we write a ∈ b if and only if b(a) 6= 0.
The set b = {a, a ∈ b} 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 ∈ Bag[A]
are disjoint if and only if b1 ∩b2 = ∅. A proper bag is a map b : A → N. The P set of
proper bags over A is denoted Bag + [A]. The size of b ∈ Bag + [A], |b|, is a b(a).
Bag bPis type-set if ∀a ∈ b b(a) = 1. A bag b 6= ∅ may be represented as a formal
sum a∈A b(a).a. Let b1 , b2 ∈ Bag[A], k ∈ Z. The scalar product k · b1 and the
sum (diff) b1 ± b2 are operations in Bag[A] defined as (k · b1 )(a) = b1 (a) · k and
b1 ± b2 (a) = b1 (a) ± b2 (a), ∀a ∈ A. Operator + is associative, − is associative on
Bag[A], not on Bag + [A], + is commutative. ∅ is the neutral element for +,−.
The Cartesian product is defined as follows. Let b1 ∈ Bag[A], b2 ∈ Bag[B]:
b1 ×b2 ∈ Bag[A × B] is b1 ×b2 (ha, bi) = b1 (a)·b2 (b), ∀a ∈ A, b ∈ 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 ∈ {+, −} =
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 difference: in
our context it simplifies the symbolic treatment of general composition.
1.2 A brief introduction to Symmetric Nets
Note: GreatSPN GUI syntax Cij and Xij ++ correspond to Si,j and !Xij , respectively.
Fig. 1. A SN example: Producers and Consumers
Composition of SN arc functions 137
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 definition of color classes (finite not empty sets), which may be parti-
tioned into (static) subclasses or be circularly ordered, and on a restricted set
of basic functions: Si , Si,k , Xi , !Xi namely diffusion/synchronization (on class Ci
or subclass Ci,k ), projection Xij and successor !Xij (only for ordered classes).
Color domains are defined as Cartesian products of n classes, where classes may
be repeated. The arc expressions are weighted sums of tuples (Cartesian prod-
uct) of basic functions (see Def. 4). The SN in Fig.1, represents a classical inter
process communication example: producer and consumer processes communi-
cating through a buffer (FIFO queue). There are two color classes, C1 (circu-
larly ordered, representing the position of messages in the buffer) 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: hX21 i, h!X11 i, hX11 , X22 i, hS2,2 i. A guard
is a boolean expression whose terms can be either (Xij = Xik )/(!Xij = Xik ) or
Xij ∈ Ci,k . An example of transition instance is Get(pos1, pc1, pc2): it satis-
fies the guard (the two colors pc2, pc3 ∈ 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, finally !X11 (pos1, pc2, pc3) = pos2. A more formal defi-
nition of the SN arc expressions is deferred to Def. 4. Produce burst has only one
instance since the functions hS22 i on its arcs are constant, mapping on C22 .
An incidence matrix can be derived from the SN structure:
Definition 1 (Incidence Matrix). The incidence matrix C of a HLPN model
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 fires, the corresponding state change can be
defined 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 definition of P and T-semiflows 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 semiflows, as discussed in Sec. 5.
2 Bag-expressions: general properties of composition
Operators op ∈ {+, −} on functions mapping to Bags are defined as follows, in
terms of Bag-operations. Let f, h : A → Bag[D], op ∈ {+, −}: (f op h)(a) =
138 L. Capra, M. De Pierro, and G. Franceschinis
f (a) op h(a), (k · f )(a) = k · f (a), ∀a ∈ A. The constant function mapping to
the null bag is denoted A,D (or just ).
Let {fi : A → Bag[Di ]} be a family of functions: the function-tuple hf1 , f2 , . . .i
(or ⊗i fi ), 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.
Definition 2 (composition). Let f : A → Bag[D], h : C → Bag[A]. Then
f ◦ h : C → Bag[D] is f ◦ h(c) = f ∗ (h(c)), ∀c ∈P
C, where f ∗ : Bag[A] → Bag[D]
∗
is the linear extension of f defined as f (b) = a∈A b(a) · f (a), ∀b ∈ 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 difference 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 prefixed by filters and suffixed by guards, both ex-
pressed as predicates. A [true] guard/filter is usually omitted. Let p : A →
{true, f alse}. A filter 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 predi-
cate on D. The expressions f [p] and [p0 ]f stand for f ◦[p] and [p0 ]◦f , respectively.
The following definition characterizes an important class of functions.
Definition 3 (constant-size function). f : A → Bag + [D] is constant-size iff
∃n ∈ N+ such that ∀a ∈ A f (a) 6= ∅ ⇒ |f (a)| = n.
Hereafter, with f constant-size we mean f ≡ f 0 [p], with f 0 [p] = iff p =
f alse. The following two general properties of composition concern constant
and constant-size functions.
Property 1 (composition of a constant and a constant-size function). Let f :
B → Bag[D] be a constant function so defined: f (b) = d, ∀b ∈ B. And let h[g] :
A → Bag[B] be a n constant-size function, where h[g](a) = ∅ iff g(a) = f alse.
Then, the composition f ◦ h[g] is defined as follows: ∀a ∈ A, f ◦ h[g] = n · f 0 [g],
where f 0 [g] : A → Bag[D] is such that ∀a ∈ A, g(a) = true ⇒ f 0 (a) = d.
Property 2 (composition of a tuple including a constant). Let f 0 be a constant
function. Then hf, f 0 i ◦ h = hf ◦ h, f 0 i.
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 , . . . , fm i 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.
Composition of SN arc functions 139
3 A language for composition of SN functions
Let us anticipate the main result presented in this paper by introducing the
language used to calculate and express the composition of SN functions.
Definition 4 (Language Lc ). Let
- D = C1e1 × C2e2 × ... × Cnen , e∗ ∈ N, be any color domain, i.e., a Cartesian
product nof colour classes ( ei = 0 means that
o Ci doesn’t occur on D).
j s j
- Bi = Xi , Si , Si,k , ! Xi : D → Bag[Ci ] , i : 1, . . . , n, j : 1, . . . , ei , k :
D
1, . . . , ||Ci ||, s ∈ Z; be the set of elementary functions, where !s denotes the
s-th mod|Ci | successor on Ci (!s Xij ≡ !s ◦ Xij , !0 = id) 4 .
0
- Tj : D P → Bag[D ], Tj = hf1 , . . . flD i, and ∀r : 1, . . . , l, fr : D → Bag[Ci ],
fr = m βm · hm , βm ∈ Z, hm ∈ Bi ; 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.
n X o
Lc = E : D → Bag[D0 ], E = λj [gj0 ]Tj [gj ], ∀D, D0 , λj ∈ 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 prefixing function-tuples with filters makes Lc slightly more ex-
pressive 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
defined in [4,5] and implemented in SNexpression [7] the main difference is that
class-functions belong to SN legacy: Si − Xij is a difference between elementary
functions (often treated as an idiom), not a new symbol; the intersection opera-
tor (though helpful) is not part of the language; scalars are in Z; class-functions
and, consequently, function-tuples are themselves bag-expressions, whereas both
in L and the new GreatSPN GUI [2] they are set-expressions. As long as we re-
strict to expressions mapping to proper bags, however, L and Lc are equivalent.
We use Lc for the sake of convenience/efficiency during the symbolic calculus.
The next important properties of Lc directly follow from the definition of Lc ,
the Cartesian product and filter/guard properties, and the basic predicate reduc-
tions listed in [8], Appendix A.2; these properties ensure that a few assumptions,
prerequisites for the application of the lemmas presented in next section, can al-
ways be met, possibly after the transformation of the involved expressions into
equivalent ones satisfying such assumptions. The proof of all relevant properties
and lemmas of this paper are reported in [8], Appendix A.1.
4
symbols !s Xij , with s 6= 0, and Si,k are mutually exclusive because we assume a color
class is either partitioned or circularly ordered.
5
showing the closure of Lc under all the other operations on bag-expression (sum,
difference, intersection, transpose), though much simpler, is not the focus here.
140 L. Capra, M. De Pierro, and G. Franceschinis
Property 3 (conjunctive form equivalence). Any E ∈ Lc can be rewritten into
E 0 ∈ Lc , E 0 ≡ E, in which the predicates of filters/guards are conjunctive forms
exclusively composed of (in)equality/membership clauses.
Property 4 (type-set equivalence). Any E ∈ Lc can be rewritten into E 0 ∈ Lc ,
E 0 ≡ 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. |fr | is the weighted algebraic sum of sizes of el-
ementary terms of fr . A function-tuple not prefixed by a filter is constant-size.
Its size is the product of sizes of tuple’s components.
For instance, |(S1 − X11 − X12 )|, with the implicit guard X11 6= X12 , is equal to
|C1 | − 2. This expression is also type-set.
A function-tuple prefixed by a filter may not be constant-size. An example
is [X11 = X12 ]hS1 − X12 , S1 − X11 i: 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 |C| − 1 when applied to hc, ci and |C| − 2 when applied to hc, c0 i, c 6= c0 .
Observe that the projection symbols appearing in the filter 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 ∈ Lc can be rewritten into E 0 ∈
Lc , E 0 ≡ 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 filters.
Since we consider domains ordered by color, we only have to deal with two cases.
Property 7 (Lc tuple Cartesian product with filters adaptation).
Let F1 , F2 ∈ 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 ∈ N+ .
Then hF1 , F2 i = [g1 ∧ g2 ∗ ]hT1 , T2 i, 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 Conventions/notations used in the sequel
Lower-case letters f, g, h, p denote class-functions and predicates, if enclosed be-
tween angular and square brackets, respectively, otherwise represent any bag-
expression (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 {Xji } of variables
(projections) appearing in f : if f = [g]f 0 [g 0 ] then V ar(f ) = V ar(f 0 ) ∪ V ar(g 0 ).
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 ) = {Xij , Xhw }. The subset X i ⊆ X holds the class-Ci variables.
Composition of SN arc functions 141
Index restriction r Let D: C1e1 ...×Cnen , f = f (X) : D → Bag[D0 ], and e0j = |X j |
e0 e0
(by the way, e0j ≤ ej ). The index restriction of f is a function f r : C1 1 ... × Cnn →
Bag[D0 ], obtained from f by replacing symbols in Xji ∈ X j , in superscript order,
e0
with Xj1 , . . . , Xj j , for each j, e0j < ej .
For example, let T = hX11 + 2X13 , X13 , X22 i: C1 3 × C2 2 → C1 2 × C2 , then
T = hX11 + 2X12 , X12 , X21 i : C1 2 × C2 → C1 2 × C2 .
r
Let X be a set {Xji }, Xji : D → Cj .
Domain projection Π By convenience, we assume X ordered, first by class index
then by superscript. We say the tuple ΠX,D : D → D0 = ⊗X i ∈X Xji projection
j
of D (on D0 ) induced by X. D is omitted when clear from the context.
Projection image X Let T 0 = hh1 , . . . , hm i with codomain D. The image of X
on T 0 is the subtuple TX
0
= ⊗i:∃X i ∈X hi , with the same domain as T 0 . We denote
j
by T¬X the residual sub-tuple of T 0 .
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 , . . . , fn i[g]. Solving T ◦ T 0
means being able to rewrite this expression into F ∈ 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 exam-
ple. 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 first step in the example of Fig. 2), thus we let
T be hf1 , . . . , fn i[g], where ∀i V ar(fi ) 6= ∅, and T 0 = hh1 , . . . , hm i.
Property 8. T = T r ◦ ΠX .
A first basic result says that we can solve T ◦ T 0 by considering T r and the image
of V ar(T ) on T 0 .
0
Lemma 1. Let T = T (X) and TX 6= T 0 . If T¬X
0
is of constant-size k, then:
T ◦ T 0 [g 0 ] = k · T r ◦ TX
0
[g 0 ]
Lemma 1 is applied twice in Fig. 2; follows a third example (|2S1 −X12 | = 2|C1 |−1):
hX11 , X11 , S1 −X13 i◦hS1 , 2S1 −X11 , S1,1 +X12 i = (2|C1 |−1)·hX11 , X11 , S1 −X12 i◦hS1 , S1,1 +X12 i
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 inde-
pendent parts of the left operand (up to a permutation of tuple elements).
142 L. Capra, M. De Pierro, and G. Franceschinis
1
2
3
4 5
6
8
7
9 10
11
12
composition's result
rule short description reference(s)
1 constant pulled-out of the left tuple Property 2
2,8 left tuple restriction and projection on the right tuple Lemma 1
3,6 distribution of composition on independent left sub-tuples Lemma 2
4 reduction (move) of a membership clause of g see [8], Appendix A.2
5 distribution property, reduction to a simple tuple-prefix Claim 1, Def. 5
7 elimination of an in-between guard built of inequalities Corollary 2, Lemma 5
9 distribution property and composition of a left constant Property 1
10 elementary composition Sect. 4.1 (table)
11, 12 basic composition (variable repetitions on the left tuple) Property 14
Fig. 2. A complete composition example (C1 is a partitioned class, C2 is ordered).
Composition of SN arc functions 143
Lemma 2.
0
Let T = hF1 (X 1 ), . . . , Fh (X h )i ∧ ∀i, j, i 6= j, X i ∩ X j = ∅, ∧TX = T 0.
T ◦ T 0 = hF1 r ◦ TX
0
1
0
, . . . , Fh r ◦ TX i
h
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.
0
We therefore focus on function-tuples Cie → Cie and hereafter omit class
index in basic functions: X j replaces Xij , Sj replaces Si,j , S replaces Si . We
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:
hX 1 , X 3 , S − X 2 , X 2 i[X 1 6= X 3 ∧ X 2 6= X 4 ] ◦ hS, 2S − X11 , S, S1 + 2X2 i =
Lem.2
hhX 1 , X 3 i[X 1 6= X 3 ], hS − X 2 , X 2 i[X 2 6= X 4 ]i ◦ hS, 2S − X 1 , S, S1 + 2X2 i =
1 2 1 2 1 1 1 2 1
hhX , X i[X 6= X ] ◦ hS, Si, hS − X , X i[X 6= X ] ◦ h2S − X , S1 + 2X2 ii
The two compositions that we ended up with are representatives of the base
cases of tuple composition we have to solve.
4.1 Tuple composition’s base cases
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 infix predicate
(guard/filter) that cannot be eliminated. The presence of an infix predicate com-
plicates the solution of a composition. Based on properties of filters and filter
reduction rules we may reduce such expressions to a particular form. The follow-
ing statements assume that the right operand of a composition (T 0 ) is possibly
followed by a guard.
Definition 5 (tuple prefix/composition simple form(s)).
Let T 0 = hh1 , . . . , hm i. A tuple-prefix [g]T 0 is simple if and only if
6=
1. g is a conjunction of (in)equalities, such that for each clause (X i =!s X j ) in
g: hi is type-set, |hi | > 1, and hi =!s hj
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 w
, . . . , g= , w ∈ N+ , such that
i j
∀i, j, i 6= j, V ar(g= ) ∩ V ar(g= ) = ∅
i i
∀g= V ar(g= ) ∩ V ar(g6= ) = {X j }
T [g] ◦ T 0 is a simple form of composition if and only if [g] ◦ T ’ is a simple
i
tuple-prefix and ∀i |V ar(g= ) ∩ V ar(T )| ≤ 1.
144 L. Capra, M. De Pierro, and G. Franceschinis
Claim 1 We can rewrite any composition T [g] ◦ T 0 that cannot be decomposed
according to Lemma 2 in terms matching Definition 5 (see [8], Appendix A.2)
In other words, if required we may assume that infix predicates are made of
(in)equalities between projections which point to equal (modulo-successor) type-
set class-functions of T 0 of size > 1. Equalities define 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 (|C2 | > 1):
hS2 − X 3 , X 1 i[X 1 6= X 2 ∧ X 1 ∈ C2 ∧ X 1 = X 3 ] ◦ hS, S, S + X 1 i →
hS2 − X 1 , X 1 i[X 1 6= X 2 ∧ X 1 = X 3 ] ◦ hS2 , S2 , S2 i+
hS2 − X 1 , X 1 i[X 1 = X 3 ] ◦ hS2 , S − S2 , S2 i + hS2 − X 1 , X 1 i ◦ hX 1 , S − X 1 , X 1 i[X 1 ∈ C2 ]
Tuples prefixed by a filter matching Definition 5 have an important property.
Property 9. A simple tuple-prefix [p]T : D → Bag[D0 ] is constant-size.
Four base cases have to be considered, they are listed below.
1. T (X 1 ) ◦ hhi
2. T (X)[g] ◦ T 0 , with |X| > 1 and X ⊇ V ar(g)
3. T (X)[g] ◦ T 0 , with X ⊂ V ar(g)
4. T [g] ◦ T 0 , with V ar(T ) ∩ V ar(g) = ∅
Case 1: T (X 1 ) ◦ hhi In absence of infix predicates, we can always reduce to
one such form due to the distribution property of sum/diff. For example:
hS −X 1 +2X 2 , X 2 i◦hh1 , h2 i = h(S −X 1 )◦hh1 i, X 1 ◦hh2 ii+2|h1 |·hX 1 , X 1 i◦hh2 i
Case 1.a: |h| = 1; this is the simplest situation.
Property 10. Let |h| = 1. Then F (X 1 ) ◦ hhi is obtained by replacing each occur-
rence of symbol X 1 in F with h.
It directly follows from the definition of composition.
For example, hS + X 1 , X 1 i ◦ hh2 i, |h2 | = 1 −→ hS + h2 , h2 i.
Case 1.b: |h| > 1. The basic compositions are summarized in the following table
(omitting tuple notation),the first one is applied in Fig. 2, step 10:
Basic composition rules and some useful identities
X 1 ◦ h = h !s X 1 ◦ h =!s h S − X 1 ◦ h = |h| · S − h S−!r X 1 ◦ h = |h| · S−!r h
!r S = S !s !r X i =!s+r X i !r (h1 ± h2 ) =!r h1 ±!r h2
If T = hf1 (X 1 )i the above basic rules (and property 2) are enough. For
example, letting |C1 | = 3:
h2S − X 1 −!X 1 i ◦ hS − X 2 i → h4S − S + X 2 − S+!X 2 i ≡ h2S + X 2 +!X 2 i.
Composition of SN arc functions 145
Repetition of a projection in T Let T = hf1 (X 1 ), . . . , fm (X 1 )i, where (without
loss of generality due to Property 4) fi (X 1 ) =!si X 1 , ∀i (symbol !s X i from now
on denotes a projection possibly prefixed by the s-th successor). We consider
first an unordered color class, then we generalize.
Property 11. Let h be type-set. hX 1 , . . . , X 1 i ◦hhi = [ i:2...m X 1 = X i ] hh, . . . , hi
V
| {z } | {z }
m>1 m
6
Here are some non-elementary, type-set class-functions :
S − X 1 ; S − X 1 − X 2 [X 1 6= X 2 ]; Si − X 1 [X 1 ∈ Ci ]; S − X 1 −!X 1 .
We can extend the above outcome to any color class.
Property 12. Let h be type-set.
^
h!r1 X 1 , . . . , !rm X 1 i ◦ hhi = [ X 1 = !(r1 −ri ) X i ]h!r1 h, . . . , !rm hi
i:2...m
As an example:
h!X 1 , X 1 , !X 1 i ◦ hS − X 2 i = [X 1 =!X 2 ∧ X 1 = X 3 ]hS−!X 2 , S − X 2 , S−!X 2 i.
In some cases may treat the idiom S − X 1 as a single function for convenience.
Here are two situations that are more efficiently processed applying the following
properties, although they could be solved applying the previous rules. Without
loss of generality, in both cases S − X 1 is the last element of T .
Property 13. Let h be a type-set function. V
hX 1 , . . . , X 1 , S − X 1 i ◦hhi = [X 1 6= X m i:2...m−1 X 1 = X i ] hh, . . . , h, Si
| {z } | {z }
m m
1
If there are no repetitions of X then h may be any function.
Property 14. hX 1 , S − X 1 i ◦ hhi = [X 1 6= X 2 ]hh, Si
Case 2: T(X)[g] ◦ T0 , |X| > 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 , . . . , fm i, where fi =!si X j , ∀i. Consider, for example:
hX 2 , !X 2 , X 3 , !2 X 1 i[X 1 6= X 3 ∧ X 1 6= !X 2 ] ◦ hh1 , h2 , h3 i
This expression doesn’t match Lc . However, we can transform the guard in
between into a filter prefixing the left tuple through an index substitution, i.e.,
an injective map φ : V ar(T ) → {1 . . . m} associating each X i to the position of
any of its occurrences in T . The picture below illustrates the idea.
hX 2 , !X 2 , X 3 , !2 X 1 i[X 1 6= X 3 ∧ X 1 6= !X 2 ].
The following rule formalizes the move of a clause of a guard g to a filter
6= 6=
prefixing T (X i = !k X j ≡ X j = !−k X i ).
6
if b is any bag, hX 1 , . . . , X 1 i(b) is obtained from [ i:2...m X 1 = X i ]hb, . . . , bi by
V
th
applying the m root to multiplicities of bag elements
146 L. Capra, M. De Pierro, and G. Franceschinis
Lemma 3 (transforming the infix predicate into a filter). Let φ(i), φ(j)
be any two occurrences of variables X i , X j , i 6= j, in tuple T .
φ(i) φ(j)
6= 6=
h. . . , !r X i , . . . , !s X j , . . .i[X i = !k X j , . . .] −→ [X φ(i) = !k+r−s X φ(j) ]T [. . .]
| {z }
T
Corollary 1. Let T [g], with T = hf1 , . . . , fm i and g be a set of (in)equalities.
If ∀X i ∈ V ar(g) there is fj , fj =!s X i , then ∃p T [g] ≡ [p]T .
Therefore, if V ar(T ) ⊇ V ar(g) the reiterated application of Lemma 3 eventually
removes the infix guard from T (X)[g] ◦ T 0 .
Applying Lemma 3 to the last example,we can proceed with Lemma 2.
Lem.3
−→ [X 4 6=!2 X 3 ∧ X 4 6= !2 X 2 ]hX 2 , !X 2 , X 3 , !2 X 1 i ◦ hh1 , h2 , h3 i
Lem.2
−→ [X 4 6=!2 X 3 ∧ X 4 6= !2 X 2 ]hhX 1 , !X 1 i ◦ hh2 i, X 1 ◦ hh3 i, !2 X 1 ◦ hh1 ii
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 filter
g on T 0 , in a symbolic way.
We assume that g is no further reducible, the composition to solve matches
Definition 5 and none of lemmas presented so far applies (in particular Lemma
1, thus TV0 ar(g) = T 0 ).
6=
Let A ⊆ V ar(g): we say gA = {(X i =!r X j ) ∈ g|X i , X j ∈ A} the restriction
of g to variables A.
A first simplification comes from the fact that we may take out equalities of
g. We recall that f r denotes the index-restriction of f .
0
Property 15. Let [g]T 0 meet Definition 5, g= 6= ∅, X = X ∪ V ar(g6= ). Then
T (X)[g] ◦ T 0 = (T [g6= ])r ◦ TX
0
0
This nice property stems from the fact that (by Definition 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 = {X 1 , . . . , X m } (T = T r ).
P rop.15
1) hX 1 , S − X 1 i[X 1 = X 2 , X 1 = !X 3 ] ◦ hS−!X 2 , S−!X 2 , S − X 2 i −→
P rop.14
hX 1 , S − X 1 i ◦ hS−!X 2 i −→ [X 1 6= X 2 ]hS−!X 2 , Si
P rop.15
2) hX 1 , !X 2 i[X 1 6= !X 2 , X 2 = X 3 ] ◦ hS−!X 2 , S − X 2 , S − X 2 i −→
Lem.3,Lem.2
hX 1 , !X 2 i[X 1 6= !X 2 ] ◦ hS−!X 2 , S − X 2 i −→ [X 1 6= X 2 ]hS−!X 2 , S−!X 2 i
P rop.15
3) hX 2 , X 2 i[X 1 6= X 2 , X 2 6= X 4 , X 1 = X 3 ] ◦ hS1 , S1 , S1 , S1 i −→
(hX 2 , X 2 i[X 1 6= X 2 , X 2 6= X 4 ])r ◦ hS1 , S1 , S1 , S1 i{X 1 ,X 2 ,X 4 } ≡
hX 2 , X 2 i[X 1 6= X 2 , X 2 6= X 3 ] ◦ hS1 , S1 , S1 i (non-reducible with the available rules)
Composition of SN arc functions 147
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 figure out that it holds
0
ΠX ◦ [g]T 0 ⊆ [gX ]r TX (1)
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 TX
0
, k∈N (2)
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 ⊂ V ar(g). If (2) holds and [g] ◦ T 0 is a simple
tuple-prefix (Definition 5). Then:
0
T (X)[g] ◦ T 0 = k · T r [gX ]r ◦ TX
0
, where k = |[g|[g]T
r 0
| 0
if |[gX ]r TX |=
6 0, otherwise
X ] TX |
k=0
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 infix predicate.
Consider this simple but interesting case where T [g] : C 3 → C 2 , T 0 : C → C 3 .
hX 1 , X 2 i[X 1 6= X 3 ∧ X 2 6= X 3 ] ◦ hS − X 1 , S − X 1 S − X 1 i |C| > 2
T g T0
In this case condition (2) is not verified: Π{X 1 ,X 2 } ◦ [g]T 0 (c) turns out to be,
for any c ∈ C, |C| > 2:
X X
(|C| − 2) ∗ hc0 , c0 i + (|C| − 3) ∗ hc0 , c00 i
c0 ∈C,c0 6=c c0 ,c00 ∈C,c0 6=c,c00 6=c,c0 6=c00
The restriction of g[T 0 ] to X = {X 1 , X 2 } used on the right-hand side of (2),
instead, is hS − X 1 , S − X 1 i (in this particular case, gX = {}). As the example
suggests, we should distinguish (in g) the case X 1 = X 2 from the case X 1 6= X 2 .
Since we are assuming that the requirements of Definition 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-|C|) among V ar(g) variables, with the
implicit constraints X i ∈ hi (c), ∀X i ∈ 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 (mod-
ulo 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
0
the solutions of the sub-system restricted to X, i.e., [gX ]r TX .
148 L. Capra, M. De Pierro, and G. Franceschinis
We consider first an unordered color-class C. In that case, hi = h, ∀i, 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 different 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 [10] for all the details). Given a graph G = (VG , EG ), where VG
is a non-empty finite set and EG a set of unordered pairs xy, x, y ∈ V (G), x 6= y,
and λ ∈ N, we define a λ-colouring of G as a map ϕ : VG → {1, 2, . . . , λ} that
assigns adjacent vertices of G different values. We are interested in the number
of different λ-colourings of G, denoted P (G, λ). The minimum value of λ such
that G admits a λ-colouring is the chromatic number of G, denoted χG . The
value |V (G)| is the order of G. We say that G is empty if E(G) = ∅, complete (or
clique) if any two vertices are adjacent. A clique of order n is denoted Kn . We
use a few operations on graphs: let x, y be two vertices of G, G · xy, xy ∈ / E(G),
is the graph obtained from G by merging x and y and leaving one occurrence
of possible resulting multiple edges; G − xy, xy ∈ E(G), the graph obtained by
removing edge xy; G + xy, xy ∈ / E(G), the graph obtained by adding edge xy.
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. [10] shows, however, that for large classes of
graphs you can compute P (G, λ) very efficiently, e.g., exploiting their modular
structure. How to compute the chromatic polynomial is out of the scope of the
paper, however, here are a few intuitive properties used in the sequel.
– (Fundamental reduction theorem) let x, y be two non-adjacent vertices of G:
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 λ = |h|, therefore, denoting with Sol(g, λ) the
number of solutions of the inequality system, P (g, λ) = Sol(g, λ).
Lemma 4. Let [g]T 0 be a simple tuple-prefix, X ⊂ V ar(g), and gX be a clique.
P (g,λ)
Then, equation (2) holds and (Corollary 2) k = P (K ,λ) if λ ≥ |X|, otherwise
|X|
k = 0, where λ = |hi |, for any hi in T 0 .
It is sufficient 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 un-
related variables X i , X j ∈ X, therefore we rewrite T ◦ [g][T 0 ] into the equivalent
Composition of SN arc functions 149
sum T ◦[g ∧X i 6= X j ]T 0 +T ◦[g ∧X i = X j ]T 0 . Note that g ∧X i = X j , after sym-
bol replacement and removal of redundant inequalities (according to Definition
5) exactly corresponds to g · X i X j .
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.
hX 1 , X 2 i[X 1 6= X 3 ∧ X 2 6= X 3 ] ◦ hS − X 1 , S − X 1 S, −X 1 i λ = |C| − 1 (> 1)
T g T0
≡ hX , X i[X 6= X ∧ X 6= X ∧ X 6= X ] ◦ T 0 + hX 1 , X 1 i[X 1 6= X 3 ] ◦ T 0
1 2 1 3 2 3 1 2
≡ hX 1 , X 2 i ◦ (λ − 2)[X 1 6= X 2 ]hS − X 1 , S − X 1 i + hX 1 , X 1 i ◦ (λ − 1)hS − X 1 i
≡ (λ − 2)[X 1 6= X 2 ]hS − X 1 , S − X 1 i + (λ − 1)[X 1 = X 2 ]hS − X 1 , S − X 1 i
P (K3 ,λ)
where λ − 2 = P (K2 ,λ)
and λ − 1 = P (K2 ,λ)
P (K1 ,λ)
. Dealing with an ordered class C.
What if predicate g of the filter prefixing tuple T 0 is defined 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 |C| = 3: X 1 6=!X 2 ≡
X 1 =!2 X 2 ∨ X 1 = X 2 . So, by expanding T ◦ [g]T 0 accordingly we eventually get
a solvable form.
This approach, however, may be inefficient 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) =
{!r X j } occurring in g and as edges, in addition to inequalities in g, those implied
by them: for any two symbols !r X j , !s X j ∈ 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 first result concerns those cases where g may be expressed in a form
such that |V ar(g)| = |Symb(g)|, i.e., for each variable there is one corresponding
symbol. In this case the previous results, in particular Lemma 4, still hold. When
|V ar(g)| < |Symb(g)| instead, an extension of Lemma 4 is needed.
Lemma 5. Let [g]T 0 be a simple tuple-prefix and X ⊂ V ar(g). If a) for each
X i ∈ V ar(g)\X any two inequalities between X and X i use the same sym-
Sol(g,λ)
bol !r X i and b) gX is a clique, then equation (2) holds and k = Sol(g if
X ,λ)
0
Sol(gX , λ) > 0, otherwise k = 0, where λ = |hi |, for any hi in T .
We can always rewrite any predicate g so that it meets condition a) of Lemma
5. Condition a) is redundant if |X| = 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
[8], Appendix A.3 for a few examples of application of the last two lemmas.
7
Let succmin and succmax be the smallest and largest successor index in the formula;
we assume that succmax − succmin < |C|, so that for each two symbols !r X j , !s X i ,
and for each c, !r X j (c) 6=!s X j (c); as a consequence we may have consider different
cases, depending on the size of C
150 L. Capra, M. De Pierro, and G. Franceschinis
Case 4: T[g] ◦ T0 , Var(T) ∩ Var(g) = ∅. We may reduce this case to one
solvable with Lemma 1. Indeed, we can express (modulo a tuple permutation)
[g] ◦ T 0 as a Cartesian product h[g]r TV0 ar(g) , T¬V
0 0
ar(g) i, where TV ar(g) is the image
0 r 0
of g on T . If [g] TV ar(g) is simple we can directly use Lemma 1. For instance:
hX 1 i[X 2 6= X 3 ] ◦ hS − X 1 , S, Si → hX 1 i ◦ hS − X 1 , [X 1 6= X 2 ]hS, Sii →
λ(λ − 1) · hS − X 1 i (λ = |C|)
5 Applications
This section presents two application examples: the symbolic verification of in-
variants in SN models, and the reduction of nets by agglomeration of transitions,
enabling more efficient qualitative analysis (as in behavior preserving reduc-
tions [3,11]) and quantitative analysis (e.g. elimination of immediate transitions
in Stochastic SN models, extending the technique defined for GSPNs in [1]).
Verification of P and T-invariants. P and T-semiflows inducing invariant prop-
erties in PNs have been introduced in mid 80s and extended to HLPN in 90s [13].
Algorithms to compute a generating family of P and T-semiflows of PN exist [9]
and are implemented in several tools; they can be applied to the unfolding of an
HLPN model, while the automatic derivation of high-level (symbolic) P or T-
semiflows is still an open problem, unless restrictions are imposed on the HLPN
formalism (as in [12]). Often the modeler is aware of which invariant properties
should satisfy a given model, thus the ability to automatically check whether
a P or T-indexed vector of functions is a P or T-semiflow is interesting. The
symbolic calculus implemented in the SNexpression tool [7], extended with the
composition presented in this paper, allows to implement such automatic check.
Let us illustrate how this can be done on the example net in Fig. 1; for the sake
of space only T-invariants are shown, while P-invariants are discussed in [8].
Definition 6 (T-semiflow of HLPN models).
Let y be a T-indexed vector of functions with color domain C(y), y[t] :
C(y) → Bag[C([t)], t ∈ T ; y is a T-semiflow if C ◦ y = nully . A T-semiflow
defines a (parametric) set of transition instances; given a color c ∈ C(y) if all
the transition instances in y(c) can fire (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 ∈ C(y) into a constant empty Bag on C(p). In Table 1
two T-semiflows of the producers-consumers SN are listed. Their interpretation
is quite simple8 : In order to reproduce a marking the pointers first and last
should be increased by one |C1| times, hence the producers should produce
|C1| items and put them into the buffer, and the consumers should get |C1|
items from the buffer. In T1 the same producer fills completely the buffer and
a consumer with the same id of the producer empties it (it represents |C2|
invariants in the unfolded net). In T2 any combination of |C1| producers and
|C1| consumers (satisfying the invariant guard g 0 ) is possible. The expressions
8
Initialization transition init cannot belong to any T-invariant, while additional in-
variants involving ProduceBurst exist, but are not included for the sake of space.
Composition of SN arc functions 151
Transition T1 T2 (Hp: |C1| = 4)
(Domain) C2 C28 , C1 [g 0 ]
1
Produce (C2 ) |C1 |hX2 i hX2 i + hX23 i + hX25 i + hX27 i
1
1 P3 1 2i+1
Put (C1 , C2 ) hSC1 , X2 i i=0 h!i X1 , X2 i
2 1 1 P 3 1 2i+1 2(i+1)
Get [g](C1 , C2 ) hSC1 , X2 , X2 i i=0 h!i X1 , X2 , X2 i
End Process (C2 ) |C1 |hX21 i hX22 i + hX24 i + hX26 i + hX28 i
W
2(i+1)
p(k) = ki=0 2 2i+1
∈ C2j ; g = p(0); g 0 = p(|C1 | − 1)
V
j=1 X2 ∈ C2j ∧ X2
Table 1. Two T-semiflows of the Producers-Consumers SN
allowing Pto verify that vectors Tj correspond to parametric T-semiflows are:
∀p ∈ P, t∈T 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 |C1 | = 4,
|C21 | = 1 and |C22 | = 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] =
hX21 i◦|C1 |hX21 i−hX21 i◦|C1 |hX21 i = C1 ( the equations for Wait to insert, Wait to extract
and Processing are very similar).
buffer: W + (Put, buffer) ◦ T 1[Put] − W − (Get, buffer) ◦ T 1[Get] = hX11 , X21 i ◦ hSC1 , X21 i −
hX11 , X21 i[g] ◦ hSC1 , X21 , X21 i = hSC1 , X21 i − hSC1 , X21 i = C1 ,C2
full: W + (Put, full) ◦ T 1[Put] − W − (Get, full) ◦ T 1[Get] = hSC• i ◦ hX11 , X21 i − hSC• i[g] ◦
hX11 , X21 , X21 i = C• (the equation for empty is very similar)
first:W + (Get, first) ◦ T 1[Get] − W − (Get, first) ◦ T 1[Get] = h!X11 i[g] ◦ hSC1 , X21 , X21 i −
hX11 i[g] ◦ hSC1 , X21 , X21 i = hSC1 i − hSC1 i = C1 (the equation for last is very similar)
T2 has color domain C1 , C28 where 8 = 2|C1 |, completed by guard g 0 (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.
buffer: W + (Put, buffer) ◦ T 2[Put] − W − (Get, buffer) ◦ T 2[Get] = hX11 , X21 i ◦ (hX11 , X21 i[g 0 ]
+h!X11 , X23 i[g 0 ] + h!2 X11 , X25 i[g 0 ] + h!3 X11 , X27 i[g 0 ])− (hX11 , X21 i[g] ◦ (hX11 , X21 , X22 i[g 0 ] +
h!X11 , X23 , X24 i[g 0 ] + h!2 X11 , X25 , X26 i[g 0 ] + h!3 X11 , X27 , X28 i[g 0 ]) = C1 ,C2
Wait to insert: W + (Produce, Wait to insert) ◦ T 2[Produce] − W − (Put, Wait to insert) ◦
T 2[Put] = hX21 i◦(hX21 i+hX23 i+hX25 i+hX27 i)[g 0 ]− (hX21 i◦(hX11 , X21 i[g 0 ]+h!X11 , X23 i[g 0 ]+
h!2 X11 , X25 i[g 0 ] + h!3 X11 , X27 i[g 0 ]) = C2
Observe that in all cases where transition Get is involved we have an infix 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-semiflow guard g 0 implies that g is satisfied).
Finally, note that depending on the actual binding of the T-psemiflow variables
to colors, functions Tj [Produce] and Tj [End Process] map to a Bag + [C2 ] that
may have coefficients 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 [11] a symbolic reduction technique
(based on the capability to syntactically solve the composition) is applied to
models used for software verification. To allow for a symbolic treatment, the
authors propose Quasi-well formed Nets, a tight restriction of SNs. Moreover,
152 L. Capra, M. De Pierro, and G. Franceschinis
C = {1, 2, 3} r:C C = {1, 2, 3} ordered r :C ⇥C
r:C h1, 3i h1, 1i h1, 2i
r :C ⇥C
h1i
hXi hX 1 , X 2 i
t t h1, 3i h1, 1i h1, 2i
hXi hX 1 , X 2 i
h1i
hSi hX 1 + X 2 i 2
0
p:C h1i h2i h3i
tt
p:C tt0
h3i h1i h2i
hXi h!Xi h1i h! 1 X 1 i+
t0 h1i h2i h3i t0 h3i h2i 2hSi
(|C| 1).hSi
hS Xi h! 1 X 2 i
hS Xi
q:C q:C q:C h3i h1i h2i q:C
h1i h2i h3i
(a.1) (a.2) (a.3) (b.1) (b.2) (b.3)
Fig. 3. Agglomeration: .1 Original SN; .2 Unfolded subnet; .3 Reduced folded net.
the syntactical arc function composition requires further restrictions on the shape
of manageable arc functions.
Transitions agglomeration is a useful reduction: it consists of merging causally
connected transitions. The aim is to reduce transition instances interleaving, pre-
serving specific system properties. A number of techniques have been proposed,
with different properties and applicability conditions. Common to most propos-
als 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 firing of a newly enabled transition t0 ; in that case, the
firing of any transition in H may immediately cause the firing of t0 , without
interfering with any other transition firing. 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 firing of
instance h1i of t, we can safely fire 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 firing of an instance of t, through p. Finally composing W + (t0 , q) with this
result (firing 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:
|C|=3
W + (tt0 , q) = hS − Xi ◦ hXit ◦ hSi = hS − Xi ◦ hSi = (|C| − 1).hSi = 2.hSi
Figure 3(b.1) shows another example of reduction. The formula for the agglom-
eration can be also used here. The agglomeration is valid for any |C| ≥ 2:
9
W − (t0 , p)t : C(p) → Bag[C(t)] denotes the transpose of W − (t0 , p); the rules to sym-
bolically compute the transpose of an arc function are defined in [4].
Composition of SN arc functions 153
W + (tt0 , q) = hS − Xi ◦ h!Xit ◦ hX 1 + X 2 i = hS − Xi ◦ h!−1 Xi ◦ hX 1 + X 2 i =
hS − Xi ◦ h!−1 X 1 +!−1 X 2 i = hS−!−1 X 1 i + hS−!−1 X 2 i = 2.hSi − h!−1 X 1 i − h!−1 X 2 i
For these examples where p is the only input place of t0 and is the only output
place of t, we can confidently state that if (1) the instances of transition t0 are not
in conflict with each other (a situation called auto-conflict, 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 sufficient 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, ∀d ∈ 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) ⇔ ∀c ∈ C(p)0 W − (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 autoconflicts
among t0 instances (= W − (t0 , p)t ◦ W − (t0 , p) − Ide, simplified formula from [5]).
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 tech-
nique presented in this paper. The subnet schema is the same but for t0 , which
has one more output place, q 0 . The arc functions for this example are:
W − (t, r) = hXi W + (t, p) = hS−!X, S, S − Xi W + (t0 , q) = h!X 2 , X 2 i[X 1 = X 3 ]
W − (t0 , p) = h!X 3 , X 2 , X 1 i W + (t0 , q 0 ) = 2 · hX 1 , X 2 i[X 1 6= X 2 ∧ X 2 6= X 3 ]
The arc functions for the agglomerated transition tt0 are (λ = |C| with |C| > 2):
W − (tt0 , r) = hXi W + (tt0 , q) = (λ − 1)[X 1 =!X 2 ]hS, Si
W + (tt0 , q 0 ) = 2(λ − 1)hS − X, Xi + 2(λ − 2)[X 1 6= X 2 ]hS − X, S − Xi
The detailed explanation of the steps leading to the result, involving the ap-
plication of Lemmas 1 to 4, is in Appendix A.3 of [8]. Observe that the result
requires to extend the SN formalism, to allow arc expressions with filters.
6 Conclusions and future work
This paper reaches the goal of completing the symbolic manipulation of SN
arc functions defining a procedure for the composition of functions mapping on
Bags. This enables a number of applications that couldn’t be treated with the
operations defined so far. The implementation of a new version of SNexpression
including this kind of composition is ongoing. The approach suggests an exten-
sion to the SN formalism itself, to allow filters 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 con-
straints on cardinality lower bounds.
154 L. Capra, M. De Pierro, and G. Franceschinis
Future work is devoted to extend the possible applications of the results pre-
sented 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 [11]. Another
interesting topic is the elimination of immediate transitions in Stochastic SNs
(in order to apply analysis algorithms which do not work in presence of im-
mediate transitions): this is a challenging issue since in general it may involve
marking dependent sequences of immediate transition firings triggered by one
timed transition, as in the case of the example in Fig. 1.
References
1. M. Ajmone Marsan, G. Balbo, G. Conte, S. Donatelli, and G. Franceschinis. Mod-
elling with Generalized Stochastic Petri Nets. John Wiley —& Sons Ltd, 1995.
2. E. G. Amparore, G. Balbo, M. Beccuti, S. Donatelli, and G. Franceschinis. 30
years of greatSPN, pages 227–254. Springer London, 2016.
3. G. Balbo and M. Silva, editors. Performance Models for Discrete Event Systems
with Synchronizations: Formalisms and Analysis Techniques. Editorial Kronos,
Zaragoza, Spain, 1998. Available online.
4. L. Capra, M. De Pierro, and G. Franceschinis. A high level language for structural
relations in Well-Formed Nets. In G. Ciardo and P. Darondeau, editors, Int. Conf.
on Applications and Theory of Petri Nets 2005, pages 168–187. Springer, 2005.
5. L. Capra, M. De Pierro, and G. Franceschinis. Computing structural properties
of Symmetric Nets. In Proc. of the 15th International Conference on Quantitative
Evaluation of Systems, QEST 15, Madrid, ES, 2015. IEEE CS.
6. L. Capra, M. De Pierro, and G. Franceschinis. Deriving symbolic and parametric
structural relations in Symmetric Nets: Focus on composition operator. Technical
Report TR-INF-2019-03-01-UNIPMN, DiSIT,UPO, Alessandria, Italy, 2019.
7. L. Capra, M. De Pierro, and G. Franceschinis. SNexpression: A symbolic calculator
for Symmetric Net expressions. In Proceedings PN2020, volume 12152 of LNCS,
pages 381–391, Cham, CH, june 2020. Springer.
8. L. Capra, M. De Pierro, and G. Franceschinis. General composition for sym-
metric net arc functions with applications. Technical Report TR-INF-2021-05-01-
UNIPMN, Computer Science Inst., DiSIT, Univ. del Piemonte Orientale, 2021.
9. J.M. Colom and M. Silva. Convex geometry and semiflows in P/T nets. a compar-
ative study of algorithms for computation of minimal p-semiflows. In Rozenberg
G., editor, Advances in Petri Nets 1990. ICATPN 1989, volume 483 of LNCS.
Springer, Berlin, Heidelberg, 1991.
10. F M Dong, K M Koh, and K L Teo. Chromatic Polynomials and Chromaticity of
Graphs. WORLD SCIENTIFIC, 2005.
11. S. Evangelista, S. Haddad, and J. F. Pradat-Peyre. Syntactical colored Petri nets
reductions. In Automated Technology for Verification and Analysis, pages 202–216,
Berlin, Heidelberg, 2005. Springer.
12. S. Evangelista, C. Pajault, and J. F. Pradat-Peyre. A simple positive flows com-
putation algorithm for a large subclass of colored nets. In FORTE 2007, pages
177–195, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg.
13. K. Jensen. An introduction to the theoretical aspects of coloured Petri nets. In
J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, A Decade of Con-
currency, Reflections and Perspectives, REX School/Symposium, The Netherlands,
June 1-4, 1993, volume 803 of LNCS, pages 230–272. Springer, 1993.