In this paper we propose a method for implementing a full structural model refinement of a (biological) model represented as a (colored) Petri net. We build on the full structural data refinement definition of C. Gratie and Petre, and the type refinement of colored Petri nets introduced by Charles Lakos. Given a (biological) reaction-based model and a desired full structural refinement of it, we propose a general coloring scheme for a colored Petri net implementation of the model and give an algorithm for adding the refinement details in the Petri net model. We then prove that the construction is a type refinement, and that by our choice of color sets the resulting refined colored Petri net implements the full structural refinement of the given model.
Model refinement, the process of adding more details to an existing model, is
an important step in the model building cycle. Many refinement methods have
been proposed for different modeling frameworks and formalisms, e.g., action
systems [
Type refinement of colored Petri nets has been introduced in [
The concept of (full) structural refinement of a reaction network (bio-)model
has been introduced in [
We assume the reader is familiar with (colored) Petri nets, but we recall some of the basic definitions so that the paper is self-contained.
The paper is structured as follows: in Section 2 we present reaction network (also called reaction-based) models and the notions of species refinement and (full) structural refinement of such models, with a discussion on the explosion of the model induced by a refinement, in terms of number of species and reactions that the initial model refines to. In Section 3 we recall some notions and notations for Petri nets and their colored version, give a coloring scheme and discuss how a reaction network model can be implemented as a (colored) Petri net. We continue in Section 4 with proposing a type refinement based on a refinement relation ρ and prove that the chosen type refinement results in a colored Petri net that is the implementation of the full structural ρ−refinement of the initial model. We draw our conclusions and discuss about the model size and successive refinements in Section 5. 2
In systems biology, model refinement comprises two aspects: the structural side
and the quantitative side. The structural side handles the newly introduced
species and presents a methodology for computing the new set of reactions,
while the quantitative side deals with changes in the kinetic constants of the
model and ways of setting the new parameters in such a way that previous data
is used. Quantitative model refinement was introduced in [
A reaction-based model M consists of a finite set of species S = {A1, . . .,Am} and a finite set of reactions R = {r1, . . . , rn} using only species in S . A reaction rj ∈ R can be formulated as a rewriting rule of the form: krj rj : c1,j A1 + . . . + cm,j Am −−→ c01,j A1 + . . . + c0m,j Am, (1) with the meaning that ci,j copies of species Ai are consumed by the reaction and c0i,j copies of species Ai are produced, i = 1..m. Constants c1,j , . . . , cm,j , c01,j , . . . , c0m,j ∈ N are the stoichiometric coefficients of rj and krj ≥ 0 is the kinetic rate constant of reaction rj . We denote by rj− = (c1,j , . . . , cm,j ) the vector of stoichiometric coefficients on the left hand side of the reaction, for the species being consumed in reaction rj , and by rj+ = (c01,j , . . . , c0m,j ) the vector of stoichiometric coefficients on its right hand side, those of species being produced. Without a risk of ambiguity, reaction rj can then be written as rj− −k−r→j rj+. Example 1. A biological system with two irreversible reactions that encode the dimerization of a molecule P can be represented as a reaction-based model M = (S , R) where S = {P, P2} and R = {2P → P2, P2 → 2P }. P represents the monomeric molecule and P2 is the dimer that is formed from two P monomers.
Data refinement is the type of refinement of a model that consists in adding details related to the species of the model, i.e., it replaces a species with several of its subspecies. The subspecies may account for post-translational modifications of macromolecules, or distinguish between possible variants of some trait.
All species are considered to be refined at once, thus each species in an initial
model is replaced by a non-empty set of refined species to yield a refined model,
as dictated by a species refinement relation ρ. This is formalized in Definition 1.
Definition 1 ([
Intuitively, each species A ∈ S is replaced in the refined model with the set of species ρ(A). For the case where ρ(A) is a singleton set, one may consider that species A does not change, even if its refined counterpart is denoted by a different name in S 0; such a refinement of a species is called trivial.
Next we recall the definitions of refinement of a vector (of stoichiometric coefficients), of a reaction, and of a reaction-based model.
Definition 2 ([
X 1≤j≤p A0j∈ρ(Ai)
αj0 = αi, for all 1 ≤ i ≤ m .
We denote by ρ(α) the set of all ρ−refinements of α. 2. Let r : r− → r+ and r0 : r0− → r0+ be two reactions over S and S 0, resp.
We say that r0 is a ρ-refinement of r if
r0− ∈ ρ(r−) and r0+ ∈ ρ(r+) .
We denote by ρ(r) the set of all ρ−refinements of r. Note that ρ(r) = ρ(r−)× ρ(r+). 3. Let M = (S , R) and M 0 = (S 0, R0) be two reaction-based models, and ρ ⊆ S × S 0 a species refinement relation. We say that M 0 is a ρ-structural refinement of M if
R0 ⊆ [ ρ(r) and ρ(r) ∩ R0 6= ? ∀r ∈ R .
r∈R In case R0 = Sr∈R ρ(r), we say M 0 is the full structural ρ-refinement of M , denoted M 0 = Mρ.
Model explosion. Note that a vector of coefficients α0 ∈ NS that respects the sum condition P 1≤j≤p αj0 = αi, for all 1 ≤ i ≤ m can be seen as a way of
A0j∈ρ(Ai) choosing αi elements from a bag containing elements of |ρ(Ai)| types, where the selection may contain several elements of the same type. The total number of different ways in which one may choose k elements from a bag with elements of nthetyspoe-sca(lalesdsummuinltgiseentocuogeffihccioepnite,s nofmeualcthichtyoposeeakre. available) is nk = n+kk−1 , A reaction rj of the form (1) can refine to Q 1≤i≤m |ρc(iA,ji)| · |ρc(0iA,ji)| different reactions. The number stems from the number of possible ways of choosing ci,j (c0i,j , resp.) copies from the possible refinements of a species Ai ∈ S . The number of reactions in a full structural ρ−refinement of a model with n reactions is thus: X
Y 1≤j≤n 1≤i≤m |ρ(Ai)| ci,j · |ρ(Ai)| c0i,j .
Example 2. Consider the reaction-based model M = (S , R) from Example 1. One possible refinement for this model is to consider that molecule P can be in two states: acetylated (P (1)) and non-acetylated(P (0)). Then the dimer P2 could have none (P2(0)), one (P2(1)) or both (P2(2)) of its composing monomers acetylated. Consider a set of species S 0 = {P (0), P (1), P (0), P2(1), P2(2)}. A relation 2 ρ ⊆ S × S 0 that would capture such a refinement is ρ = {(P, P (0)), (P, P (1)), (P2, P (0)), (P2, P2(1)), (P2, P2(2))}. One can easily see that ρ is a refinement rela2 tion, based on Definition 1.
A full structural ρ-refinement of M is the model M 0 = (S 0, R0), where R0 = {2P (0) → P2(0), 2P (0) → P2(1), 2P (0) → P2(2), 2P (1) → P2(0), 2P (1) → P2(1), 2P (1) → P2(2), P (0) + P (1) → P2(0), P (0) + P (1) → P2(1), P (0) + P (1) → P2(2), PPP222(((012))) →→→ 222PPP (((000))),,, PPP222(((012))) →→→ 222PPP (((111))),,, PPP222(((012))) →→→ PPP (((000))) +++ PPP (((111))),,}.
Modeling Biological Systems as (Colored) Petri Nets Many biological models are implemented as Petri nets due to the graphical, intuitive formalism, and the many simulation strategies they offer. We start our discussion over refinement and implementations of models as Petri nets from the standard version of Petri nets. We then continue with colored Petri nets. 3.1
We assume the reader is familiar with the basic notions and notations related
to Petri nets and we refer to [
In order to implement a reaction-based model as a Petri net, one represents
each species via a place, and each reaction via a transition having as pre-places
the places representing the reactants of the reaction, and as post-places the
places representing the products of the reaction, with each arc expression being
the stoichiometry of the represented species in that reaction, see [
P 2
T fw T bw 2
P 2
There exist two ways of defining colored Petri nets, one proposed by Kurt
Jensen in [
Definition 4 ([
Arc expressions may contain variables, which are seen as symbols whose value is determined by the color (mode) of the transition the arc is connected with.
For any colored Petri net with finite color sets there exists a standard Petri
net that is behaviorally equivalent, see [
Definition 5 ([
T ∗ × P ∗ | E((t, p))(c0)(c) > 0}; – f ∗((p, c), (t, c0)) = E((p, t))(c0)(c), ∀((p, c), (t, c0)) ∈ A∗ and
f ∗((t, c0), (p, c)) = E((t, p))(c0)(c), ∀((t, c0), (p, c)) ∈ A∗; – M0∗((p, c)) = M0(p, c).
A colored Petri net representation of a model can be obtained from a standard Petri net implementation of the model by assigning to each place a color set with just one element. We propose here a general coloring scheme that uses record color sets (i.e. a data structure containing a finite collection of fields, each with a name and an associated data type) and can easily be extended to incorporate refinement details by adding new fields. Each place is assigned its own record color set with one field that has exactly one value. Each transition is assigned a color set that is a multiset of color sets of its pre- and post-places, where the multiplicity of each color set is given by the multiplicity of the arc connecting the place and the transition. It is basically a multiset with elements of different types. For example, the color set CS T fw in Figure 2 is a collection of two elements of type CS P and one element of type CS P2. Note that this is not the only possible coloring scheme and moreover it may not be optimal (in terms of number of variables and data structures used), but it is general. One may use integers, records, sets, Cartesian products, or whatever coloring scheme better suits the system being modeled.
A further change that is required when turning a standard Petri net into a colored one is assigning to each arc a with arc function f (a) = k where k ∈ N the expression E(a) = v1 + + . . . + +vk where ++ denotes multiset addition and vi :C(p) are typed variables with i = 1..k, and p is the place of arc a. Intuitively, we use a different variable for each token that may traverse an arc. The total number of variables needed in a model is thus Pa∈A f (a). A further change is in the initial marking, where each place p is assigned the same number of tokens as in the standard network, and all tokens have as color the one color in p’s color set. We call such a colored Petri net the trivial coloring of the initial network.
We denote by C(x) the one color in the color set of a place/transtition x. In order to identify precisely the variables used in the expression of an arc (x, y) ∈ A we denote the variables by vx,y,i, where i = 1..f ((x, y)). We also use the shorthand notation va,i to denote the i-th variable on arc a ∈ A.
N = (P, T, A, f, M0), we call a trivial coloring of N a colored Petri net T (N ) = (P, T, A, Σ, C, E, M, Y, M00 ) such that: – Σ = Sp∈P Cp ∪ St∈T Ct where Ct : {Cp | p ∈ P } → N is a multiset such that:
Ct(Cp) = 0 f ((p, t)) (p, t) 6∈ A and (t, p) 6∈ A (p, t) ∈ A and (t, p) 6∈ A ; f ((t, p)) (p, t) 6∈ A and (t, p) ∈ A f ((p, t)) + f ((t, p)) otherwise – C : P ∪ T → Σ, such that C(x) is a record color set defined as above if x ∈ P and a multiset defined as above if x ∈ T ; – E(a) = ++P1≤i≤f(a) va,i = va,1 + + · · · + +va,f(a), for all a ∈ A, where va,i :
C(p) with p being the place of arc a; – M is the set of markings; – Y is the set of steps; – M00 (p) = M0(p)`C(p), for all p ∈ P .
Example 4. An example of a trivial coloring of the Petri net described in Example 3 is given in Figure 2.
CS P
P
Petri net). We say that a colored Petri net N structurally implements a given reaction-based model M iff N ∗, the unfolding of N , structurally implements model M in the sense of Definition 3.
Proposition 1. The unfolding T (N )∗ of a trivial coloring T (N ) of a standard Petri net N is equivalent to the initial net N (as every color set has exactly one color).
Proposition 2. If a standard Petri net N structurally implements a reactionbased model M , then its trivial coloring T (N ) structurally implements the same model M .
Proof. By Proposition 1, N and T (N )∗ are equivalent, thus the unfolding of T (N ) structurally implements model M and, by Definition 7, T (N ) structurally implements M . 3.3
Refinements of Petri nets have been a subject of interest for many years. In
particular, we are concerned here with the work of Charles Lakos, who has identified
and formalized three types of refinements: type refinement, subnet refinement and
node refinement, see [
We recall now the definition of type refinement of a colored Petri net as it
was proposed in [
Definition 8 ([
A morphism that captures a type refinement is a system morphism, see [
Note that for every refined state or action there exists a corresponding abstract state or action, resp. via the projection from subtype to supertype. Also note that in Definition 8, N denotes the refined network. 4
Full Structural Refinement as Type Refinement of Colored Petri Nets In this section we prove that the full structural refinement of a reaction-based model implemented as a Petri net can be implemented as a type refinement of the trivial coloring of the Petri net. We give a coloring strategy (type refinement) for implementing a full structural data refinement of a model represented as a Petri net, and conclude by proving that our construction indeed implements the required full structural data refinement. 4.1
Intuitively, species refinement implies replacing each species with a non-empty
set of species. This can be done in a colored Petri net by replacing for each place
representing a species its default color set by a new record or enumeration color
set having as many elements as the set of species that its corresponding species
refines to. Or, assuming color sets defined as records, by replacing a single value
field with a new field with as many possible values as the cardinality of the
refined subspecies set. Formally, we need to define a morphism from the refined
colored Petri net to the initial colored Petri net that respects all the properties
of a type refinement, as described in [
ment of a reaction network model). We say that a colored Petri net N structurally implements the full structural refinement of a model M as described by a refinement relation ρ iff the unfolding of N , N ∗, structurally implements the full structural refinement of M , ρ(M ) in the sense of Definition 3.
We describe next a type refinement of a given trivial coloring of a Petri net implementation of a reaction-based model M that captures the full structural data refinement of M as described by a given refinement relation ρ. Algorithm 1 TypeRef function TypeRef(N, ρ) Σ0 ← ?;
. create the new color sets based on the old ones; for all p ∈ P do cs ← C(p); define a new color set cs0 that extends cs with a new field with ρ(δ−1(p)) values; Σ0 ← Σ0 ∪ {cs0};
C0(p) ← cs0; end for for all t ∈ T do
define cs as a multiset cs : {C0(p) | p ∈ P } → N such that cs(C0(p)) = C(t)(C(p)), ∀p ∈ P ; Σ0 ← Σ0 ∪ {cs};
C0(t) ← cs; end for
. re-type the arc expressions: for each variable in an arc expression, create one having as type the new color set of the place that the arc is connected to; the new arc expression is a multiset sum of these variables;
E0 ← ?; for all e ∈ E do p ← the place connected to e; V ← set of variables appearing in e; V 0 ← ?; for all vi ∈ V do define vi0 : C0(p);
V 0 ← V 0 ∪ {vi0} end for e0 ← ++Pv∈V 0 v; . ++P denotes multiset addition; E0 ← E0 ∪ {e0}; end for M0 ← μ{(p, c) | p ∈ P, c ∈ C0(p)}; Y0 ← μ{(t, c) | t ∈ T, c ∈ C0(t)}; M00 is designed such that Pc∈C0(p) | M00(p, c) |=| M0(p, C(p)) |, ∀p ∈ P ; N 0 ← (P, T, A, Σ0, C0, E0, M0, Y0, M00 ); return N 0; end function
Let N = (P , T, A, Σ, C, E, M, Y, M0) be a trivially colored Petri net that implements a reaction-based model M = (S , R) with correspondence function δ. Let ρ ⊆ S × S 0 be a full structural refinement relation that refines model M to model M 0 = (S 0, R0). We build a colored Petri net N 0 = (P , T, A, Σ0, C0, E0, M0, Y0, M00 ) and then show that the construction is a type refinement. Moreover, we show that the resulting network implements the full structural refinement ρ(M ). The procedure takes as input a trivially colored Petri net that implements M , and the refinement function ρ. It then updates the color sets of the network such that the color set of each place is extended with a new field that will account for the new subtypes of the species that the place stands for. Each transition gets as color set a multiset of the color sets of its pre- and postplaces, with multiplicities dictated by the cardinality of each arc expression, just like in the trivial coloring. Note that this means that the refined transition color sets are subtypes of the initial transition color sets, as multisets of subtypes of a color set that is a multiset of supertypes, with identical multiplicities.
Using a distinct variable for each token on every arc is important because it allows for exact identification of each token. One can thus encode all possible combinations of in- and out- tokens for a transition t, i.e. the full set of refinements of the reaction encoded by transition t.
Proposition 3. Given a trivially colored Petri net N that is an implementation of a reaction-based model M , and a full structural refinement relation ρ of M , the colored Petri net N 0 = TypeRef(N, ρ) is a type refinement of the initial network.
Proof. Based on the construction described in Algorithm 1, we detail here the type refinement morphism between the two networks.
Note that N is trivially colored, so all color sets have exactly one color. The projection from any color in a color set of Σ0 onto its corresponding supertype color set is the one color in the supertype color set: ΠC(x)(c) = C(x), for any x ∈ P ∪ T , and any color c ∈ C0(x).
We now describe a morphism Φρ : N 0 → N between the two networks, that is a type morphism. 1. Φρ(x) = x for all x ∈ P ∪ T ∪ A. 2. Φρ(C0)(x) = C(x). By definition of the color sets in N 0, the color set of each place and of each transition in N 0 is a subtype of the color set of the same place/transition in N , i.e. C0(x) <: Φρ(C0)(x). Moreover, for any color c ∈ C0(x) : ΠΦρ(C0)(x)(c) = ΠC(x)(c) = C(x). 3. ∀x ∈ P ∪ T : ∀c ∈ C0(x) : Φρ(1 `(x, c)) = 1 `(x, ΠC(x)(c)) = 1 `(x, C(x)): for every colored place/transition in N 0 with color c, the morphism Φρ returns the same place/transition (because Φρ is the identity on P ∪ T ), having as color the projection of c on the color set of x as given by the morphism Φρ, namely C(x). 4. ∀(p, t) ∈ A : ∀(t, m) ∈ Y0 : Φρ(E0(p, t)) = E(p, t) and the multiset of colored tokens consumed from place p at the firing of transition t in mode m is E0(p, t)(m). By construction of E0, the number of consumed tokens is E(p, t)(C(t)). The projection of every color in C0(p) is C(p), thus we get: Φρ(E−(1`(t, m))(p)) = ΠΦρ(C0)(p)(E0(p, t)(m)) = E(p, t)(C(t)) = = E(p, t)(ΠC(t)(m)) = Φρ(E0)(p, t)(ΠΦρ(C0)(t)(m)). 5. Similarly, ∀(t, p) ∈ A : ∀(t, m) ∈ Y0 : Φρ(E0(t, p)) = E(t, p) and the multiset of colored tokens added to place p at the firing of transition t in mode m is E0(t, p)(m). By construction of E0, the number of produced tokens is E(t, p)(C(t)). The projection of every color in C0(p) is C(p), thus we get: Φρ(E+(1`(t, m))(p)) = ΠΦρ(C0)(p)(E0(t, p)(m)) = E(t, p)(C(t)) = = E(t, p)(ΠC(t)(m)) = Φρ(E0)(t, p)(ΠΦρ(C0)(t)(m)).
Because the morphism Φρ respects all conditions for being a type refinement of a Petri net it follows that Algorithm 1 computes a type refinement of its input Petri net.
Theorem 1. Given a reaction-based model M = (S , R), a structural refinement relation ρ ⊆ S × S 0, and a colored Petri net N = (P, T, A, Σ, C, E, M, Y, M0) that is trivially colored and implements model M with function δ : S ∪R → P ∪ T , the colored Petri net TypeRef(N, ρ) implements the full structural ρrefinement of model M .
Proof. Let N 0 denote the refined colored Petri net TypeRef(N, ρ), and let M 0 = (S 0, R0) denote the full structural ρ-refinement Mρ. By construction of the refined colored Petri net N 0 there exists a type morphism between N 0 and N , as detailed in the proof of Proposition 3.
First, note that N is trivially colored and thus the network is equivalent to its unfolding (see Proposition 1). With a slight abuse of notation, we will use x to denote the unfolded equivalent of a place/transition x ∈ P ∪ T , (x, C(x)).
We show now that the unfolding of N 0 implements the full structural refinement of M . Let N ∗ = {P ∗, T ∗, A∗, f ∗, M0∗} be the unfolding of N 0. The color set of a place p ∈ P 0 has | ρ(δ−1(p)) | elements, where each color represents one refined species S0 ∈ S 0, (δ−1(p), S0) ∈ ρ. The places of N ∗ represent pairs (p, c) such that p ∈ P and c ∈ C0(p). Given that every place p has a symbolic correspondence with one species S = δ−1(p) in S , and the colors of places in N 0 can be thought of as the refinements of S, there exists a one-to-one correspondence between places in P ∗ and species in S 0. Let δρ : S 0 → P ∗, with δρ(S0) = (δ(S), c) ∈ P ∗ where (S, S0) ∈ ρ and no two siblings are mapped to the same value.
δρ can be extended to map also reactions in R0 to (t, m) pairs. The color m of a transition t uniquely identifies its pre- and post-places in the unfolded network, and the arc inscriptions. By definition of the color sets of transitions as multisets over the color sets of neighbouring places, it follows that every possible combination of colored tokens flowing through a transition is captured by a transition color. This means that a transition t in N 0 encodes all possible refinements ρ(r) of the reaction r = δ−1(t) that transition t stands for in N .
A transition (t, m) ∈ T ∗ encodes the reaction
X (p,c)∈•(t,m) f ∗((p, c), (t, m))δρ−1((p, c)) → f ∗((t, m), (p, c))δρ−1((p, c)).
X (p,c)∈(t,m)•
The reaction r0 = δρ−1(t, m) that a transition (t, m) ∈ T ∗ implements in N 0∗ is a ρ-refinement of the reaction r = δ−1(t) that transition t implements in N . This comes from the type refinement conditions 4 and 5 (see Definition 8). The incremental effects of executing a step (t, m) in the refined network equal the incremental effects of executing the step (t, ΠC(t)(m)) in the initial network. The negative incremental effect E− encodes the left hand side of a reaction, and the positive incremental effect E+ encodes the right hand side.
We detail here the negative incremental effect of a step, and relate it to its meaning in the model M 0. E−(1`(t, m)) = P(p,t)∈A p × E((p, t))(m). In the unfolded network N ∗ a transition (t, m) is connected to places via edges ((p, c), (t, m)) ∈ A∗ where f ∗((p, c), (t, m)) = E((p, t))(m)(c). Summing over all unfolded instances of a place in N ∗ yields
X c∈C0(p)
X c∈C0(p) f ∗((p, c), (t, m)) =
E((p, t))(m)(c) =| E((p, t))(m) | .
Note that the arc expressions in N and N 0 are the same, which means that their cardinality is also the same. N implements model M , thus |E((p, t))| = ci,j and |E((t, p))| = c0i,j where ci,j is the stoichiometric coefficient of species Si = δ−1(p) on the left hand side of reaction rj = δ−1(t) and c0i,j is the soichiometric coefficient of Si on the right hand side of rj . Arc multiplicities in N ∗ represent stoichiometries, and for any place p of N 0 its unfolded places {(p, c) | c ∈ C0(p)} represent the sibling species in ρ(δ−1(p)).
A similar argument can be made for the right hand side of a reaction, starting from the positive incremental effect of a step. With both the left and the right hand side of a reaction represented by (t, m) being a ρ-refinement of the left or right, respectively hand side of the reaction δ−1(t), it follows that (t, m) implements a ρ-refinement of the reaction implemented by t. 5
In this paper we have made a connection between the notions of type refinement
of a colored Petri net proposed in [
The size of the refined colored Petri net model We discuss here about the size of the colored Petri net model obtained by refining a given model, in terms of number of places and transitions.
A type refinement of a colored Petri net preserves the structure of the network unchanged, i.e. the number of places and transitions does not change. But the semantics of each place and transition is different, and we will therefore consider the unfolding of the colored Petri net.
Given N = (P , T, A, Σ, C, E, M, Y, M0) a trivial colored Petri net implementation of a reaction-based model M = S , R, a refinement relation ρ ⊆ S × S 0 and a colored Petri net N 0 = (P , T, A, Σ0, C0, E, M0, Y0, M00 ) which is the implementation of the full structural ρ−refinement of M by Algorithm 1 with function δ : S ∪ R → P ∪ T , we discuss the size of the unfolding of N 0, denoted byN ∗.
N has by construction |S | places and |R| transitions. In N 0 by construction each place representing a species S ∈ S has ρ(S) colors, and will therefore unfold to ρ(S) places. The total number of unfolded places is PS∈S |ρ(S)| = |S 0|. The total number of possible colors of a transition depends on the number of colors in the color set of the pre- and post-places of the transition, and on the cardinality of the arc expressions of arcs connected on either end with the transition. A transition t ∈ T will thus unfold to transitions in N ∗, which yields a total number of transitions in N ∗ equal to Y p∈•t |ρ(δ−1(p))|
E((p, t)) X t∈T
Y p∈•t |ρ(δ−1(p))|
E((p, t)) ·
Y p∈t• ·
Y p∈t• |ρ(δ−1(p))| E, ((t, p)) |ρ(δ−1(p))| E, ((t, p)) .
Depending on the refinement function ρ, this number can be much larger than the number of transitions in the colored network N 0, which successfully avoids this explosion in number of places and transitions of the network. Consecutive full structural refinements Very often models go through several steps of refinement, as new information about the modeled system is available, and a more detailed representation is needed. We discuss in this paragraph how subsequent full structural refinements of a model can be implemented using our approach. The problem can be formulated as follows. Given a reactionbased model M = (S , R) and two refinement relations ρ ⊆ S × S 0 and ρ0 ⊆ S 0 × S 00, obtain the full structural ρ0−refinement of the full structural ρ−refinement of M . In our construction, we start from a trivial coloring of a Petri net implementation of a model. This is however not a limitation of the approach, since subsequent refinements can be implemented as one single refinement that is the composition of the two (or more) successive refinements to be implemented.
We conclude that colored Petri nets can be used to implement full structural refinements of reaction-based models. The major advantage of using the colored Petri nets formalism lies in their ability to represent the fully structurally refined system in a compact way, using the same network structure and adding all refinement details in the colors of places and transitions.