DE NOUVELLES REDUCTIONS COLOREES POUR LA VALIDATION DE LOGICIELS

30/09/2017
Publication e-STA e-STA 2004-3
OAI : oai:www.see.asso.fr:545:2004-3:20046
DOI :

Résumé

DE NOUVELLES REDUCTIONS COLOREES POUR LA VALIDATION DE LOGICIELS

Métriques

16
8
127.65 Ko
 application/pdf
bitcache://aa9eed7f99938ee03cf46d2ef3f0046a056fd967

Licence

Creative Commons Aucune (Tous droits réservés)
<resource  xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
                xmlns="http://datacite.org/schema/kernel-4"
                xsi:schemaLocation="http://datacite.org/schema/kernel-4 http://schema.datacite.org/meta/kernel-4/metadata.xsd">
        <identifier identifierType="DOI">10.23723/545:2004-3/20046</identifier><creators><creator><creatorName>Sami Evangelista</creatorName></creator><creator><creatorName>Serge Haddad</creatorName></creator><creator><creatorName>Jean-François Pradat-Peyre</creatorName></creator></creators><titles>
            <title>DE NOUVELLES REDUCTIONS COLOREES POUR LA VALIDATION DE LOGICIELS</title></titles>
        <publisher>SEE</publisher>
        <publicationYear>2017</publicationYear>
        <resourceType resourceTypeGeneral="Text">Text</resourceType><dates>
	    <date dateType="Created">Sat 30 Sep 2017</date>
	    <date dateType="Updated">Sat 30 Sep 2017</date>
            <date dateType="Submitted">Mon 15 Oct 2018</date>
	</dates>
        <alternateIdentifiers>
	    <alternateIdentifier alternateIdentifierType="bitstream">aa9eed7f99938ee03cf46d2ef3f0046a056fd967</alternateIdentifier>
	</alternateIdentifiers>
        <formats>
	    <format>application/pdf</format>
	</formats>
	<version>34063</version>
        <descriptions>
            <description descriptionType="Abstract"></description>
        </descriptions>
    </resource>
.

DE NOUVELLES RÉDUCTIONS COLORÉES POUR LA VALIDATION DE LOGICIELS NEW COLOURED REDUCTIONS FOR SOFTWARE VALIDATION Sami Evangelista ∗ Serge Haddad ∗∗ Jean-François Pradat-Peyre ∗ ∗ CEDRIC-CNAM Paris 292, rue St Martin, 75003 Paris ∗∗ LAMSADE-CNRS UMR 7024 Université Paris 9 Place de Lattre de Tassigny 75775 Paris Cedex 16 Abstract: Une abstraction structurelle du modèle analysé permet de réduire très efficacement la complexité d’une méthode d’analyse basée sur l’énumération des états accessibles. Nous présentons dans cet article des réductions pertinentes de réseaux colorés construites sur de nouvelles réductions de réseaux de Petri ordinaires. Ces réductions ne font appel qu’à des conditions structurelles ou algébriques. Elles préservent la vivacité du modèle mais aussi toute formule LTL qui n’observe pas les transitions réduites du réseau. L’utilisation conjointe de conditions structurelles et algébriques permet d’élargir significativement le domaine d’application de ces réductions. De plus la définition de ces réductions est paramétrée vis à vis du cardinal des domaines de couleurs. Structural model abstraction is a powerful technique for reducing the complexity of a state based enumeration analysis. We present in this paper accurate reductions for high-level Petri nets based on new ordinary Petri nets reductions. These reductions involve only structural and algebraical conditions. They preserve the liveness of the net and any LTL formula that does not observe the reduced transitions of the net. The mixed use of structural and algebraical conditions significantly enlarges their application area. Furthermore the specification of the transformation is parametric with respect to the cardinalities of coloured domains. Keywords: Software Validation, Reductions, High-level Petri nets 1. INTRODUCTION The use of formal methods in software design may be decomposed in two steps: a modelling stage which must lead to a model as close as possible to the analysed software and a verification stage in- volving properties expression and model checking via adequate algorithms. Two kinds of verification techniques can be used. The state enumeration based methods lead to a complete verification but the analysis is restricted by the combinatory explosion factor. The struc- tural methods are generally efficient but they do not ensure the complete correctness of the mod- elled system. Thus an attractive trade-off would be to first per- form structural abstractions in order to obtain a simplified model on which an enumeration based method can more easily be applied. The model may be abstracted in two ways: data abstraction and operation abstraction. Here we will focus on the latter one which merges consecutive instruc- tions into a virtual atomic one. Such a transforma- tion drastically reduces the combinatory explosion due to the elimination of the intermediate states. In the context of (high-level) Petri nets this ab- straction is called a net reduction. A reduction is characterised by some application conditions, a transformation rule and the properties for which the initial and the reduced models are equivalent. In order to obtain reductions with a broad range of applications while preserving a large set of properties, we base our coloured reductions on new efficient ordinary Petri nets reductions (see Haddad and Pradat-Peyre (2004)) and we use the following approach to extend them to coloured models. We characterise some properties of the coloured functions labelling an arc which ensure that the unfolding of this arc will be appropriate for the conditions involved in ordinary reductions. We exhibit coloured flows which lead to the sat- isfaction of the algebraic conditions of ordinary reductions. We show how the use of composition, inverse and transpose of mappings enables us to handle the transformation of the labelling of arcs in the reduced net. Given a subclass of the Well- formed nets, Chiola et al. (1990), we specify re- ductions at a syntactic level in order to efficiently check the conditions and apply the transforma- tions. We will not describe this part which can be found in Evangelista et al. (2004). Compared to previous works concerning high-level nets re- ductions, Colom et al. (1986), Genrich (1990), Haddad (1990), our new coloured reductions lie on accurate application conditions (since they are based on efficient ordinary Petri nets reductions) and then permit to reduce more realistic models. Moreover, this analysis does not need to fix a value for the parameters of the model (which is not the case for methods that reduce the reachability graph) and can be followed by any other analysis method. The paper is organised as follows. In the next section, we recall the basics of coloured Petri nets with a focus on the coloured functions. In the third section, we first demonstrate that existing reduc- tions do not cover typical patterns of concurrent programming. Then we show how the analysis of coloured functions and coloured invariants helps to accurately characterise behavioural conditions on the net. At last, we formally develop the post- agglomeration. In the fourth section, an example illustrates the power of these new reductions. 2. DEFINITIONS AND NOTATIONS Coloured Petri nets handle tokens that are typed (or coloured) upon non empty finite sets called colour domains; a marking is then a multi-set over a colour domain and we denote Bag(C) the set of multi-sets over C (the related definitions can be found in the appendix). Definition 2.1. A coloured net is a 5-tuple CN = hP, T, C, W+ , W− i with : • P a non empty and finite set of places; • T a non empty and finite set of transitions (disjoint of P); • C is the colour mapping from P S T to ω where ω is a set of finite and non empty sets. An item of C(s) is called a colour of s and C(s) denotes the colour domain of s. • W+ (resp. W− ) is the post (resp. pre) inci- dence mapping that associates to each place p and each transition t a colour mapping form C(t) to Bag(C(p)). We note W = W + −W− . We note  = {•} the domain reduced to the single value • (the neutral token); so, ordinary Petri nets can be viewed as particular coloured Petri nets (the unique and common colour domain is ). Definition 2.2. A marking is a mapping that associates to each place p a value in Bag(C(p)). We note m0 the initial marking of a net. A transition t is fireable for an instance ct ∈ C(t) from a marking m (denoted by m[t, cti) if ∀p ∈ P, m(p) ≥ W− (p, t)(ct) The firing of t, ct from m leads to the mark- ing m0 (m[t, ctim0 ) defined by ∀p ∈ P, m0 (p) = m(p) + W(p, t)(ct). A marking m0 is reach- able from a marking m if there exists a se- quence t1, c1, . . . , tk, ck such that m[t1, c1im1, m1[t2, c2im2, . . . , mk−1[tk, ckim0 . We denote by Reach(CN, m0) the set of all reachable markings from m0. As usual, an infinite sequence is a fir- ing sequence iff all its finite prefixes are firing sequences. To each coloured net corresponds a unique Petri net which is called the underlying Petri net. This net is composed by the set of places, p[cp] where p ∈ P and cp ∈ C(p) and the set of transitions t[ct], t ∈ T, ct ∈ C(t). The pre and the post conditions are defined by the instantiation of colour function. This unfolded net is defined in the appendix. We now introduce the coloured flows and invari- ants. These invariants can be used to characterise specific behaviours like, for instance, mutual ex- clusion. In order to obtain a sound definition of flows, we extend by linearity a function from C to Bag(D) to a function from Bag(C) to Bag(D). Definition 2.3. A flow F, on a domain C(F), is a vector over P, noted as the formal sum F = P p∈P λp.Fp.p, where ∀p ∈ P, λp ∈ Z and Fp a mapping from Bag(C(p)) to Bag(C(F)) such that: ∀t ∈ T, P p∈P λp.Fp ◦ W(p, t) = 0 1 . F induces the invariant: ∀m ∈ Reach(CN, m0), P p∈P λp.Fp(m(p)) = P p∈P λp.Fp(m0(p)) An invariant F is positive if ∀p ∈ P, λp ≥ 0. It is binary if ∀c ∈ C(F), P p∈P λp.Fp(m0(p))(c) = 1. It is a synchronisation invariant if ∀c ∈ C(F), P p∈P λp.Fp(m0(p))(c) = 0. When no confusion is possible (i.e. the initial marking is given), we will not distinguish the flow and its corresponding invariant. We want to analyse the structure of the underlying Petri net using the structure and the functions of the coloured Petri net. This requires to characterise and manipulate coloured functions. The following definition and notations are enough for our pur- poses. Definition 2.4. Let f be a mapping from Bag(C) to Bag(C0 ). • t (f) is the mapping defined from Bag(C0 ) to Bag(C) by t (f)(c0 )(c) = f(c)(c0 ) • f is defined from P(C) to P(C0 ) by f(D) = {c0 ∈ C0 | ∃d ∈ D, f(d)(c0 ) 6= 0} where P(C) denotes the power set of C. Note that the linearity is preserved by this transformation (substituting ∪ to +) and that f may be viewed as a function from C to P(C0 ). Definition 2.5. Let f and g be two linear map- pings from P(C) to P(C0 ). We note f v g if ∀c ∈ Bag(C), f(c) ⊆ g(c). Below we list particular mappings. An orthonor- mal mapping is a colour domain permutation, a unitary mapping produces at most one token per colour, a projection is a canonic mapping from Bag(C × D) to Bag(C), an ortho-projection is the composition of an orthonormal mapping with a projection. f is a quasi-one to one mapping if ∀c 6= d f(c) ∩ f(d) = ∅. f is a quasi-onto map- ping from Bag(C) to Bag(D) if f(C) = D. The complete definitions are given in the appendix. 3. COLOURED AGGLOMERATIONS We suppose in the sequel that the set of transi- tions of the net is partitioned as : T = T0 U H U F. The underlying idea of this decomposition is that the couple (H, F) defines transitions sets that are causally dependent : an occurrence of f ∈ F in a firing sequence may always be related to a previ- ous occurrence of some h ∈ H in this sequence. We have extended two kinds of agglomerations: the pre and the post agglomeration. Informally 1 0 denotes here the null mapping from C(t) to Bag(C(F)) stated, in the pre-agglomeration scheme, firing a transition h ∈ H is only useful for firing any transition of f ∈ F. Thus in the reduced net, the firings of h are postponed until the corresponding firing of f. In the post-agglomeration scheme, the firing of any transition f ∈ F is mainly conditioned by the firing of the transitions of H. Thus, in the reduced net, one fires f immediately after the firing of some h ∈ H. 3.1 An introducing example In the following coloured net (see Fig.1), the tran- p r h q V1 : C < X > < G1(X) > < G2(Y) > f < Y > V2 : C Fig. 1. Updating variables sequentially sition h models the update of a variable modelled by the place V 1: the value X is replaced by the value G1(X) where G1 models a mapping from C to C. Initially, this variable has the value x0. Similarly, the transition f models the update of a second variable modelled by the place V 2. Gener- ally, this model does not have the same behaviour as the one of the model depicted in Fig.2 where r < G2(Y) > < Y > V2 : C hf q V1 : C < X > < G1(X) > Fig. 2. Updating variables atomically the two updates are performed simultaneously. However, there exist many cases for which these two models are equivalent. In particular, as soon as we can prove that either the value of V 1 does not change when q or p are marked or the value of V 2 does not change when p is marked, the two models share a large set of properties. Indeed let us suppose that, in the first model, the value of V 1 does not change when q is marked. The variable V 1 cannot be modified when p is marked. So, we can delay the update of the variable V 1 until we are ready to perform the update of the variable V 2 without modifying the properties of the model. This corresponds to the scheme of the pre-agglomeration: h can be delayed until f is fireable. In the second case, updating V 2 after having waited in state p or updating V 2 just after having updated V 1 is equivalent since value of V 2 cannot change when p is marked. This corresponds to the scheme of the post-agglomeration: f is fireable as soon as h is fired. Nevertheless, whereas these behaviours corre- spond to the scheme of the pre or of the post agglomeration, none of the previously defined re- ductions cover such behaviours. The present work is based on reductions for ordinary Petri nets that we proposed in Haddad and Pradat-Peyre (2004). Such reductions cover a large range of patterns by introducing algebraical conditions whereas the previously defined ones solely lie on structural conditions. However the extension of the condi- tions and the transformation of these reductions to high-level nets require careful analysis of the coloured functions labelling the arcs of the net. Due to the lack of space, we focus in this paper on the post-agglomeration; complete results can be found in Evangelista et al. (2004). 3.2 Exploiting coloured functions and invariants The structure of a coloured net does not necessar- ily reflect the structure of the underlying Petri net since we have to take into account colour mappings. Especially, we need to follow colour transformation using composition or transposition of colour mappings. Let us consider the follow- ing coloured Petri net and suppose that, given a h f p: C Ψ Φ Fig. 3. Colour mapping manipulation illustration colour cf ∈ C(f), we want to compute the colours {ch ∈ C(h)} such that the firing of h for a colour ch may help the firing of f for the instance cf (by producing useful tokens in place p). We have to start from cf and to find the instances of p that are linked to f[cf ]. By definition, this set is Φ(cf ). Then we have to find instances of h that are linked to a place p[cp], cp ∈ Φ(cf ). These instances are the set {ch ∈ C(h), Ψ(ch) ∩ Φ(cf ) 6= ∅}. By definition of the transposition of a function, this set is tΨ(Φ(cf )). Thus, the set of colours we look for is (tΨ ◦ Φ)(cf ). In an opposite way, the set of instances of f that are causally dependent of an instance ch of h, are (Ψ ◦ tΦ)(ch). Let us consider now the following coloured Petri net where p is an ordinary place (see Fig.4).         h p α2 α1 q1 q2 f2 : C2 f1 : C1 Fq2 = t (α2 ◦ AllC2 ) α1 and α2 are unitary one to one mappings ∀m ∈ Reach(CN, m0), Fq1 (m(q1)) + Fq2 (m(q2)) = c Fq1 = t (α1 ◦ AllC1 ) Fig. 4. An invariant controlling f1 and f2 Let us prove that there is always an instance of f1 or of f2 that is fireable when p is marked. • The interpretation of the invariant F is the following one: there is at least one to- ken either in the place q1 or in q2 whose colour is either in the set α1(AllC1 (•)) or in α2(AllC2 (•)). • Since t αi (i=1,2) is an unitary quasi-one to one mapping, each firing instance (fi, ci) re- quires, when αi(ci) 6= 0, in addition to the token in p, exactly a token in the place qi which colour is in the singleton αi(ci). • Combining these two facts, an instance (fi, ci) for some i is always fireable when p is marked. Remark that this reasoning is still valid if we only require that ∀i, Fqi v t (αi ◦ AllCi ). 3.3 Post-agglomeration hypotheses We present the four conditions of the post- agglomeration: the potentially post-agglome- rability, the HF-interchangeability, the F- independence and the F-continuation. The potentially post-agglomerability ensures that in any fireable sequence the number of occur- rences of H is greater or equal than the number of occurrences of F. Definition 3.1. (Hypothesis R1). A coloured net is potentially post-agglomerable (p-post-agglo- merable) if ∃ H ⊂ T, F ⊂ T, p ∈ P such that (1) • p = H, p• = F and m0(p) = 0 (2) ∀f ∈ F, C(f) = C(p) × Cf and W− (p, f) is an ortho-projection from C(p) × Cf to C(p); (3) ∀h ∈ H W+ (p, h) is a unitary quasi-onto mapping such that t (W+ (p, h)) is a quasi- onto mapping The first point ensures that place p models an intermediate state between the firing of a transi- tion in H and the firing of a transition in F. The second one ensures that any firing of a transition f requires exactly one token in p. The last point guarantees that all instances of any firing of h ∈ H produces a token in the place p and that any coloured token of C(p) may be produced by a firing of some transition h ∈ H. The HF-interchangeability hypothesis mainly restricts either the set H or F to be a singleton in order to avoid the case where h ∈ H and f ∈ F are live in the original net whereas the transition hf is not live in the reduced net. Definition 3.2. (Hypothesis R2). A p-post-agglo- merable coloured net is HF-interchangeable if one of these conditions is fulfilled : (1) H = {h} and W + (p, h) is orthonormal (2) F = {f}, C(f) = C(p) (thus W − (p, f) is orthonormal) In the following, we will assume w.l.o.g. that de- pending on the item of the above definition either W+ (p, h) is the identity function and W − (p, f) is a projection or W − (p, f) is the identity function. Indeed applying the reduction called orthonor- malization leads to this situation (see Haddad (1990)). The F-independence hypothesis ensures that when the place p is marked, no transition that can produce tokens useful for the firing of a transition in F can be fired. Definition 3.3. (Hypothesis R3). A p-post-agglo- merable coloured net is F-independent if ∀f ∈ F, ∀q ∈ (• f \ {p}), ∀t ∈ • q \ F, ∃pt ∈ • t, such that (1) there exists a binary coloured positive invari- ant F = P r∈P Fr.r on a domain D (2) let us note φ = t(W+(q, t)) ◦ W−(q, f) ◦ t(W−(p, f)) ψ = t(W−(pt, t)) ◦ t(Fpt ) ◦ Fp then φ v ψ Furthermore, if there exists a binary positive invariant F0 on the domain C(p) such that t F0 p is a quasi-onto mapping then the net is strongly F-independent. These two points ensure that the transitions of • (• f[cf ]) (dashed transitions of figure Fig. 5) are not fireable when the related instance p[cp] of place p is marked. This behaviour is obtained by the use of a binary positive invariant that ensures a mutual exclusion of the place p[cp] with place pt[cpt ] which are pre-conditions of these transitions t. The mapping ψ allows us to highlight the instances of the transition t that are linked to an instance of pt covered by the a positive invariant (in the unfolded net) which covers a given instance of p. The third hypothesis, the F-continuation, means that an excess of occurrences of h ∈ H can always be reduced by subsequent firings of transitions of F (when the place p is marked, a transition of F is necessarily fireable).                         q[...] q[...] q[...] p[..] f[...] f[...] t[...] t[...] t[...] pt[..] Fig. 5. A subset of φ(cp), cp ∈ C(p) Definition 3.4. (Hypothesis R4). A p-post-agglo- merable net is F-continuable if either ∃f ∈ F such that • f = {p} or ∃ Fs ⊂ F such that : (1) ∀f ∈ Fs, • f = {p, pf }, (2) ∀f ∈ Fs, t (W− (pf , f)) is a quasi-one to one mapping, (3) there exists a flow on C(p) with F = X f∈Fs Fpf .pf − λ.Fp.p ∀f ∈ Fs, W− (pf , f) ◦ hXC(p), AllCf i = t Fpf and such that (a) either λ = 0 and F induces a binary positive invariant (b) or λ = 1 and F induces a synchronisation invariant 3.4 Post-agglomeration transformation We define now the transformation associated to the coloured post-agglomeration. The reduced net is the same as the original one except that we merge any transition of H with transitions of F (we form couples (hf)). Definition 3.5. The reduced net (CNr, m0r) obtained from a coloured net (CN, M0) by a coloured post-agglomeration is defined by: • Pr = P and Tr = T \ (H ∪ F) ∪ (H × F); we note hf a new transition (h, f) ∈ H × F. • ∀p0 ∈ Pr, m0r(p0 ) = m0(p0 ) • ∀t ∈ Tr \ (H × F), ∀p0 ∈ Pr, W− r (p0 , t) = W− (p0 , t) and W+ r (p0 , t) = W+ (p0 , t) • ∀hf ∈ (H × F), ∀q ∈ Pr · W− r (q, hf) = max(Γ1, Γ2) · W+ r (q, hf) = Υ + W − r (q, hf)) where when H = {h}, then, C(hf) = C(f) and · Γ1 = W− (q, h) ◦ W− (p, f), · Γ2 = W− (q, f) − W(q, h) ◦ W − (p, f) · Υ = W(q, f) + W(q, h) ◦ W − (p, f) when F = {f}, then C(hf) = C(h) and · Γ1 = W− (q, h) · Γ2 = W− (q, f) ◦ W+ (p, h) − W(q, h) · Υ = W(q, f) ◦ W + (p, h) + W(q, h) This transformation preserves the Petri net live- ness and the properties related to the maximal or infinite sequences (e.g. deadlock, fairness, mutual- exclusion,etc.). The corresponding theorem can be found in the appendix. 3.5 An example The following coloured net (Fig. 6) models the allocation of resources (C2) to processes (C1). When receiving a request from a process X, the server chooses a free resource Y , sends this re- source identity to the process and stores locally (in place Taken) this allocation (ts1). Upon recep- AllC1 AllC2 Att1: C1 Att2: C1 Work: C1xC2 Idle: C1 < X > < X > < X,Y > < X > < X > t1 t2 t3 t4 Lock < X > < X,Y > < X > < X > < X,Y > < Y > < X > Mess2: C1xC2 Ack2: C1 Ack1: C2 Mess1: C1 < X,Y > < X,Y > ts1 ts2 Server < X,Y > < X > Taken: C1xC2 < Y > < Y > Resources: C2 < X > < Y > Fig. 6. Typed resource allocation tion of a resource release request (t3) the server services this request (ts2) when the request cor- responds to an already stored allocation (a token (X,Y) is in the place Taken). Let us describe the reduction process on this net in order to look for possible deadlocks. At first, we delete the implicit places Server and Att2. Then we apply a post-agglomeration of the transition t2 with the transition t3 and a post-agglomeration of the transition ts2 with the transition t4. Note that these agglomerations would be still possi- ble with the reductions of Haddad (1990). But AllC1 Lock AllC2 Att1: C1 Idle: C1 < X > < X > t1 t2 < X > < X > < Y > < X > < Y > ts1 < Y > Ack1: C2 Mess1: C1 < X > Resources: C2 < X,Y > Taken: C1xC2 < X,Y > ts2 < Y > < X,Y > < X,Y > Mess2: C1xC2 Fig. 7. No more standard reductions on the reduced net of Fig.7 no reductions previ- ously defined are applicable. However, the post- agglomeration of h = ts1 with f = t2 around the place p = Ack1 is applicable. Indeed, C(f) = C(p) × C2, W − (p, f) is an ortho-projection, H = {h}, W+ (p, h) is an ortho-projection so the net is p-post agglomerable (but does not verify the HF-interchangeability). The unique transition related to the F-inde- pendency hypothesis is the transition t1 (which may put token in place Att). The flow F = hAllC1i.Lock + hAllC1i.Mess1 + hAllC1i.Ack1 on C1 induces the binary positive invariant: ∀m ∈ Reach(N, m0), m(Lock) + P c∈C1 m(Mess1)(c) + P c∈C2 m(Ack1)(c) = 1. Using notation of the hypothesis conditions, φ = AllC1 and ψ = AllC1. So, φ v ψ and since t (AllC1) = AllC1 is a quasi- onto mapping the net is strongly F-independent. At last, the flow F = hAllC2i.Mess1+hAllC2i.Ack1− hAllC2i.Att1 induces the synchronisation invari- ant ∀m ∈ Reach(N, m0), P c∈C1 m(Mess1)(c) + P c∈C2 m(Ack1)(c) − P c∈C1 m(Att11)(c) = 0 which fulfils the conditions of the F-continuation hypothesis (t2 is fireable as soon as Att1 is marked). Applying this reduction leads to the net depicted Fig.8. Finally the implicit places AllC1 AllC2 Idle: C1 t1 < X > Mess1: C1 < X > < Y > ts1 < X,Y > Taken: C1xC2 Resources: C2 < X > < X,Y > < X,Y > Mess2: C1xC2 < X,Y > < X > < X > Att1: C1 Lock < X > < Y > ts2 Fig. 8. Application of a post-agglomeration Mess2 and Att1 are deleted and then a post- agglomeration of ts1 with ts2 followed by a post- agglomeration of t1 with ts1 produces the net depicted Fig.9 where all the places being implicit may be deleted. As the final net is live, the original AllC1 AllC2 Idle: C1 t1 < Y > < Y > Resources: C2 Lock < X > < X > Fig. 9. A live net one is also live (see Theorem 1 in appendix). 4. CONCLUSION We have presented in this paper new coloured reductions and we have precisely defined one of them: the post-agglomeration. These reductions are based on accurate conditions using linear invariants that cover more realistic concurrent software behaviours (compared to initial condi- tions which were only based on the structure of the model). We are integrating a syntactic ver- sion of these reductions in the Quasar tool, a framework for verifying concurrent programs (see http://quasar.cnam.fr). 5. ACKNOWLEDGMENTS A first version of this paper was published at IFAC Workshop on Discrete Event Systems, WODES’04, 22-24 September 2004. 6. ACKNOWLEDGMENTS REFERENCES C. Chiola, C. Dutheillet, G. Franceschinis, and S. Haddad. On well-formed colored nets and their symbolic reachability graph. In ICATPN, Paris-France, June 1990. J.M. Colom, J. Martinez, and M. Silva. Packages for validating discrete production systems mod- eled with Petri nets. In IMACS-IFAC Sympo- sium, Lille, France, 1986. S. Evangelista, S. Haddad, and J.F. Pradat-Peyre. Coloured Petri nets reductions for concurent software validation. Technical report, CEDRIC, CNAM, Paris, 2004. H.J. Genrich. Equivalence transformations of prt-nets. In Jensen and Rozenberg, editors, High-level Petri Nets, Theory and Application, volume 424, pages 426–453. Springer-Verlag, 1990. S. Haddad. A reduction theory for colored nets. In Jensen and Rozenberg, editors, High-level Petri Nets, Theory and Application, volume 424 of LNCS, pages 399–425. Springer-Verlag, 1990. S. Haddad and J.F. Pradat-Peyre. Efficient reduc- tions for LTL formulae verification. Technical report, CEDRIC, CNAM, Paris, 2004.