A high-level Petri net framework is introduced for the toxic risk assessment in biological and bio-synthetic systems. Unlike empirical techniques mostly used in toxicology or toxicogenomics, we propose a systemic approach consisting of a series of behavioral rules (reactions) that depend on abstract discrete \expression" levels of involved agents (species). We introduce a nite state high-level Petri net model allowing exhaustive veri cation (model-checking) of properties related to equilibrium alteration or appearing of hazardous behaviors. The approach is applied to the study of the impact of the aspartame assimilation into the blood glucose regulation process.
Toxicology [
The main approach used in toxicogenomics employs empirical analysis like in
the identi cation of molecular biomarkers, i.e., indicators of disease or toxicity in
the form of speci c gene expression patterns [
Biological processes are usually given in terms of pathways which are causal chains of the responses to stimuli, this way the deregulation of homeostasis appears as the activation or inhibition of unexpected but existing pathways. Moreover, in the context of toxicogenomics it is crucial to take into account at least two other parameters: the exposure time and the thresholds dosage delimiting the ranges of safe and hazardous e ects.
In this paper, we depict and analyze the mechanistic process of toxicology
using high-level Petri nets. Our work is inspired by the de nition of reaction
systems as given in [
From this model we retain the idea of reactions but we signi cantly change the semantics. The rst change concerns principle 2: species are available at a given discrete abstract level. This is mainly related to the need of expressing toxicants doses. The corresponding discretization is built observing thresholds levels in dose-response curves. The second and more fundamental change regards the introduction of discrete time constraints. Time plays a role in the evolution of species, more precisely, species are associated to a decay time , meaning that their level diminishes with time. This accounts for the presence of a non-speci ed environment that consumes and degrades species, thus allowing to abstract away from reactions that may be neglected in the speci ed context. Each reaction (R; I; P ) is extended with levels for all its reactants and inhibitors. Reactions can take place only if each reactant is present at least at a given level and each involved inhibitor is at a level strictly inferior to the given one. As a result, the level of products of the reaction can be increased or decreased.
Summing up, systems are build out of a series of behavioral reactions among
involved agents or species. We model such systems into high-level Petri nets
and apply it to toxicogenomics problems, namely deregulation of homeostatic
processes. Toxicity questions are expressed using a suitable temporal logic like
CTL [
We apply the modeling and veri cation process on the example of blood glucose regulation in human body showing the maintenance of the homeostasis. In particular, we highlight how the interplay between the assimilation of aspartame and glucose regulation causes the appearance of unwanted behaviors.
Organization of the paper. The paper is organized as follows: Section 2 recalls basic de nitions and notations on high-level Petri nets. Next, Section 3 describes our running example of blood glucose regulation. Section 4 introduces the principles behind reaction networks and presents their high-level Petri net modeling. Then Section 5 shows how to check toxicology properties and nally, Section 7 concludes with some considerations on future work. 2
We recall here the general notations together with some elements of the semantics
of high-level Petri nets [
De nition 1. A high-level Petri net N is a tuple (Q; T; F; L; M0) where:
T is the set of transitions and Q \ T = ;;
L is the labeling function from places Q, transitions T and arcs F to a set of labels de ned as follows:
product of sets of integer values;
values; and 8f 2 F , L(f ) is a tuple of variables and integer values compatible with the adjacent place.
tokens in L(q).
Observe that we are considering a subclass of high-level Petri nets where at most one arc per direction for each pair place/transition is allowed and only one token can ow through. The behavior of high-level Petri nets is de ned as usual: markings are functions from places in Q to multisets of possibly structured tokens in L(q) and a transition t 2 T is enabled at marking M , if there exists an evaluation of all variables in the labeling of t such that the guard L(t) evaluates to true (L (t) = true) and there are enough tokens in all input places q to satisfy the corresponding input arcs, i.e., L ((q; t)) 2 M (q). Then, the ring of t produces the marking M 0: 8q 2 Q; M 0(q) = M (q)
L ((q; t)) + L ((t; q)): with L (f ) = 0 if f 2= F , and + are multiset operators for removal and adding of one element, respectively. We denote it by M [t: iM 0.
By convention, primed version of variables (e.g. x0) are used to annotate output arcs of transitions, their evaluation is possibly computed using unprimed variables (e.g. x and y) appearing on input arcs. With an abuse of notation, singleton markings are denoted without brackets, the same is used in arc annotations. An example of ring is shown in Figure 1. We say that a marking M is reachable from the initial marking M0 if there exists a ring sequence (t1; 1); : : : ; (tn; n) such that M0[t1: 1iM1 : : : Mn 1[tn: niM . q1 q2 7 t 5 x y (a) Before the ring
(b) After the ring
Here we introduce our running example: glucose regulation in human body (Figure 2). In the following, we are always referring to the process under normal circumstances in a healthy body.
Glucose regulation is a homeostatic process: i.e., the rates of glucose in blood (glycemia) must remain stable at what we call the equilibrium state. Glycemia is regulated by two hormones: insulin and glucagon. When glycemia rises (for instance as a result of the digestion of a meal), insulin promotes the storing of glucose in muscles through the glycogenesis process, thus decreasing the blood glucose levels. Conversely, when glycemia is critically low, glucagon stimulates the process of glycogenolysis that increases the blood glucose level by transforming glycogen back into glucose.
We will focus on the assimilation of sweeteners: i.e., sugars or arti cial sweeteners such as aspartame. Whenever we eat something sweet either natural or arti cial, the sweet sensation sends a signal to the brain (through neurotransmitters) that in turns stimulates the production of insulin by pancreas. In the case of sugar, the digestion transforms food into nutrients (i.e., glucose) that glucose level
Food intake
Digestion
Glucagon are absorbed by blood. This way, sugar through digestion increases glucose in blood giving the sensation of satiety. In case the income of glucose produces hyperglycemia, the levels of glucose are promptly equilibrated by the intervention of insulin. Unlike sugar, arti cial sweeteners are not assimilated by the body, hence they do not increase the glucose levels in blood. Nevertheless the insulin produced under the stimuli originated by the sweet sensation, although weak, can still cause the rate of glucose to drop engendering hypoglycemia. In response to that, the brain induces the stimulus of hunger. As a matter of fact this appears as an unwanted/toxic behavior, indeed the assimilation of food (even if it contains aspartame) should calm hunger and induce satiety not the opposite.
This schema suggests that we should consider four levels for glycemia: low, hunger, equilibrium and high. Likewise for insulin we assume three levels: inactive, low and high. All other actors involved in glucose regulation, have only two levels (inactive or active). In the following sections, we will see how to model the glucose metabolism and how to verify the unexpected behaviors of arti cial sweeteners. 4
A reaction network is composed of a set of species S governed by a set of reactions R. We begin by giving some intuitions on their dynamics.
Species in S represent the actors of the modeled system. In the example introduced above, we have concrete species such as aspartame and also more abstract ones representing ratios or concepts like glycemia. Species may have several expression levels. Levels are determined by the observable behavior of species, i.e., they refer to a change in the capability of action of species. In toxicology, they may represent dosages. We assume, for each species s, an arbitrary but nite number Ls of levels, and each s is initialized at a certain level s. For certain species, we assume the presence of a non speci ed environment that acts on them by decreasing gradually their expression levels. This special activity is called decay and is modeled by various durations associated to expression levels. Decay may be unbounded indicating that the level of the species can only change by result of a reaction. It is formalized by a function that associates to each level either ! (unbounded) or its nite duration: s : [0::Ls
1] ! N+ [ f!g: For all species s 2 S we require that s(0) = ! meaning that the duration of the basal level must be unbounded.
The set of involved species is
S = fSugar; Aspartame; Glycemia; Glucagon; Insuling and their expression levels and corresponding decays are: levels Lsugar = f0; 1g Laspartame = f0; 1g Lglycemia = f0; 1; 2; 3g Lglucagon = f0; 1g Linsulin = f0; 1; 2g durations sugar(1) = 2 aspartame(1) = 2 glycemia(1) = 8 glycemia(2) = 8 glycemia(3) = 8 glucagon(1) = 3 insulin(1) = 3 insulin(2) = 3 The levels of glycemia are: 0 corresponding to low, 1 to hunger, 2 to equilibrium and 3 to high. Likewise for insulin we have 0 that corresponds to inactive, 1 to low and 2 to high. All levels for the other species are 0 for inactive and 1 for active.
The evolution of species s 2 S is governed by a set of reactions R, each being of the form: ::= hR ; I ; P i (1) where R (reactants), I (inhibitors) are sets of pairs (s; s) and P (products) is a non empty set of pairs (s; z), where s 2 [0::Ls 1] and z 2 Z. Species can appear at most once in each set R , I and P . They can be present in both R and I but they must occur with di erent levels2. We write s 2 R to denote (s; ) 2 R similarly for I and P and we omit index if it is clear from the context ( = hR; I; P i).
Example 2 (Glucose metabolism { reactions). The set of reactions R = f k = (Rk; Ik; Pk) j k 2 [1::9]g for the glucose metabolism example is: k Reactants Rk Inhibitors Ik 1 (Sugar; 1) 2 (Aspartame; 1) ; ; (Glycemia; 1) 3 ; 4 (Glycemia; 3) ; 5 (Insulin; 2) ; 6 (Insulin; 1);
(Glycemia; 3) ; 7 (Insulin; 1) (Glycemia; 2) 8 (Glucagon; 1) ;
P roducts Pk (Insulin; +1); (Glycemia; +1) (Insulin; +1) (Glucagon; +1) (Insulin; +1) (Glycemia; 1) (Glycemia; 1) (Glycemia; 1) (Glycemia; +1) 1 and 2 represent the assimilation of Sugar and Aspartame, respectively: while Aspartame only increases the level of Insulin, Sugar also increases Glycemia. 3 takes care of hypoglycemia, i.e., a Glycemia level equal to 0 (obtained by 2 Observe that a species can appear in the same reaction as reactant at level r, inhibitor at level i > r and product. using (Glycemia; 1) as inhibitor) engenders the production of Glucagon. On the contrary, hyperglycemia causes the production of Insulin ( 4). The presence of Insulin lowers Glycemia (reactions 5; 6; 7). In particular Insulin level equal to 1 plays a role in the decrease of Glycemia only in case of hyperglycemia 6 or hypoglycemia 7, otherwise the signal is not strong enough and we need Insulin at level 2 to see the e ect on Glycemia ( 5). Last reaction describes the role of Glucagon which if active increases the level of Glycemia.
The dynamics of reaction networks is formalized using high-level Petri nets. We represent the state of a species s as a pair hls; usi, where ls is an integer value storing the current level from zero to Ls 1, and us is a counter storing the interval of time spent at level ls. The system is initialized by setting the level of all species: i.e., each species s is set to h s; 0i where s is the given initial level.
Reaction networks can evolve in two ways: Case 1. Time progression and Decay: Time progresses discretely of one unit at once. It a ects species with nite decay only. More precisely if a species s has unbounded decay at level l ( s(l) = w) then its corresponding tuple ( s; us) remains unchanged. Otherwise, if the species has a nite decay ( s(l) = d), it may stay at level l for d time units. Then, degradation happens as soon as d time units are elapsed and is obtained by decreasing the level to l 1 and by setting us to zero.
Case 2. Reaction: A reaction may happen if and only if all the reactants are available at least at the required level and all the inhibitors are expressed at a level strictly inferior to the required one. The triggering of a reaction results in the update of the level of all its products. Depending on the reaction, levels will be increased (+n) , maintained (0) or decreased (-n).
We assume that each reaction can take place only once per time unit. We now comment on some speci c design choices concerning reactions: the set of reactants and inhibitors R[I is allowed to be empty. This accounts for modeling an environment that is continuously sustaining the production of a species. a species can appear in the same reaction simultaneously as a reactant and an inhibitor. In such a case, we require them to occur with di erent levels: (f(s; )g [ R; f(s; 0)g [ I; P ) where < 0. This means that the reaction can take place only if the level ls of s belongs to the interval ls < 0. In particular, if s has to be present in a reaction exactly at level , s should appear as a reactant at level and as inhibitor at level 0 = + 1; species can appear only once in the set of products P . This implies that a product cannot be increased and decreased in the same reaction.
It is also worth observing that if a species is continuously sustained by some reactions then it remains available in the system at a certain level for a period that could be longer than the corresponding decay time. Example 3 (Glucose metabolism { scenario). Take once again the example of glucose metabolism and observe the behavior of Glycemia in the following scenario: initial state 8 time units elapse, counter at level 3 updates one time unit elapses, Glycemia decays one time unit elapses, counter at level 2 updates reaction 5 decreases Glycemia level 8 time units elapse, counter at level 1 updates one time unit elapses, Glycemia decays one time unit elapses, no e ect since glycemia(0) = ! h3; 0i h3; 8i h2; 0i h2; 1i h1; 0i h1; 8i h0; 0i h0; 0i:
More formally, we now introduce the high-level Petri net modeling. Each species s 2 S is modeled by a single place qs whose type L(qs) is the set of tuples of the form hls; usi, where ls 2 [0::Ls 1] and us 2 [0::maxs], with max s = maxf s(l) j s(l) 6= ! and l 2 [0::Ls 1]g. In order to cope with time aspects we introduce a transition tc (Figure 3(a)) connected to all species that is responsible for time progression and takes care of the decay of concerned species (as described in Case 1 above). Finally, every reaction is modeled with a transition t (Figure 3(b)). To each transition t we associate a special place q that is used to ensure that the same reaction is not executed more than once in the same time unit. More detailed explanations for each type of transition follow De nition 2. qs (a) Clock transition with only one place of each kind (qs for s 2 S and q for 2 R).
its high-level Petri net representation is de ned as tuple (Q; T; F; L; M0) where z; z0; l; l0; u; u0; w; w0 are variables and: Q = fqs j s 2 Sg [ fq j 2 Rg; T = ftcg [ ft j 2 Rg; F = f(q; tc); (tc; q) j q 2 Qg [
f(qs; t ); (t ; qs); (q ; t ); (t ; q ) j
2 R and s 2 R
[ I [ P :
L(q ) = f0; 1g for each 2 R
L(qs) = [0::Ls 1] [0::max s] for each s 2 S L((q ; tc)) = w L((tc; qc)) = 1 L((qs; tc)) = hls; usi L((tc; qs)) = hls0; u0si for each s 2 S L((qs; t )) = hls; usi L((q ; t )) = w
L((t ; qs)) = L((t ; q )) = 0 ( (ls) = ! _ us + 1 (ls)) ! hls0; u0si = hls; us + 1i ( (ls) 6= ! ^ us + 1 > (ls)) ! hls0; u0si = hls 1; 0i : ^
We now comment on the transitions of the high-level Petri net. The result of the ring of a transition is handled by guards (namely transition labels L(tc) and L(t )) together with the evaluation as described after De nition 1. With an abuse of notation, in the following, we refer to evaluated variables without e ectively mentioning the evaluation : i.e., we say that the current value of the token in q is w instead of (w). Input and output arcs between the same place and transition with the same label (read arcs) are denoted in gures with a double-pointed arrow with a single label.
Clock transition tc, depicted in Figure 3(a), takes care of Case 1 above. tc is responsible for the decay of concerned species and the related update of counters us of each species. Moreover tc updates the tokens of all places q to 1, thus reenabling the possibility of performing a reaction .
Next, we describe transitions for reactions, depicted in Figure 3(b). Given a reaction = (R; I; P ) we detail the conditions and the results of ring of t . As described in Case 2 we have: each reactant r 2 R has to be present at least at level r, this is expressed by guard lr r; each inhibitor i 2 I has not to exceed level i, this is guaranteed by guard (li < i); each product p 2 P corresponding to place qp is updated to hlp0; u0pi = hmax(0; min(lp + z; Lp 1)); 0i.
The role of place q is to forbid two consecutive executions of the same reaction in the same time unit. Initially, the marking of q is set to 1 and it becomes 0 when the transition t is red; then clock transition tc sets it to 1 again.
Observe that, because of the semantics of high level Petri nets, reaction may not occur even if all constraints are satis ed. This is interpreted as the action of an hostile (non-speci ed) environment (e.g., reactants are too far from each other to react).
Sugar
Aspartame Glucagon
Glycemia + R 3 8
I +
R + 1
I
R R + 4 5 6 7 + R R
R
R +
2 of product levels by 1. For each reaction transition , we have omitted place q and all arcs in the opposite direction. The numbers inside each transition refers to the corresponding reaction in Example 2.
L(tc) tc hlg; ugi Proposition 1. Given a reaction network (S; R) with initial values s for each species s 2 S: its Petri net representation has a nite structure with jSj + jRj places, jRj + 1 transitions and the number of arcs is bounded by 2(jSj + jRj + ( R j + jI j + jP j + 1); =(R ;I ;P )2R j each place type is a nite set; for each arc (q; t) 2 F there is an arc in opposite direction, i.e., (t; q) 2 F and each arc label is a singleton; the initial marking and all reachable markings have exactly one structured token per place; the number of all reachable markings from the initial one is nite. Proof. Follows by de nition and by induction on the length of a ring sequence. tu
Such a Petri net representation of a reaction network is used to detect and
predict toxic behaviors related to the dynamics of bio-molecular networks. In
order to verify toxicology properties, we resort to temporal logics and model
checking techniques [
We recall here the basic concepts of CTL, provide the formal de nition of
the syntax and give some intuitions on the semantics, formally de ned in [
A CTL formula is de ned as: ' ::= ? j a j :' j ' _ ' j ' ^ ' j ' ! '
EX' j EG' j E('U') j EF' j AG' j AF' where a 2 A is an atomic proposition.
CTL is used to state properties on branching time structures. It uses usual boolean operators, path quanti ers and temporal operators. Path quanti ers can be of two kinds: A' means that ' has to hold on all paths starting from the current state, while E' stands for there exists at least one path starting from the current state where ' holds. We have four temporal operators: X' holds if ' is true at the next state, G' means that ' has to globally hold on the entire subsequent path, F' stands for eventually (or nally ) ' has to hold (at some point on the subsequent path), and '1U'2 means that '1 has to hold at least until at some position '2 holds. In our context atomic formulae are represented by pairs of species and levels: A = f(s; s) j s 2 Sg, for instance (Glucose; 2).
As mentioned in the introduction, we are mainly interested in checking whether the inner equilibrium of an organism (tissue, cell, . . . ) is maintained when administrating drugs or applying stressors. More in detail, toxicology properties can be classi ed into two categories: properties checking for the appearance of particular symptoms, and properties characterizing causal relations between events.
The former class of properties basically consists in verifying reachability of some states, while the latter concerns pathways that highlight sequences of events leading to toxic outcomes. For instance, in the case of glucose regulation, we could verify whether glycemia levels are kept stable and whether they change in case of ingestion of aspartame. More precisely, we could examine the causes and the symptoms of the hypoglycemia induced by the assimilation of aspartame. Hence hypoglycemia is treated as a toxic state.
blood glucose regulation. The following properties can be expressed in CTL: Symptoms: Is it possible to have an anomalous decrease of glucose levels in blood (revealing hypoglycemia)?
EF(Glycemia; 0) Mode-of-action: Recalling that the blood glucose regulation process normally maintains glycemia at equilibrium (level 2), is there an abnormal behavior leading to hypoglycemia?
E(EF(Glycemia; 2) U (EF(Glycemia; 0))) Causality: Does assimilation of sweeteners cause hypoglycemia?
EF[((Sugar; 1) _ (Aspartame; 1)) ^ (Glycemia; 1)] ! AF(Glycemia; 2) For the third formula we show two paths given as sequences of reactions (abstracting away from time transitions), one that satisfy the formula and the other that contradicts it. The rst one corresponds to the assimilation of sugar. As described in Section 3, the digestion of sugar induces an increase of the production of insulin and an augmentation of the blood glucose levels. Nonetheless the levels of insulin produced are not enough to cause the glycemia to drop and the formula is satis ed.
(Sugar; 1); (Aspartame; 0); (Glycemia; 1); (Insulin; 0); (Glucagon; 0) 1 ! (Sugar; 1); (Aspartame; 0); (Glycemia; 2); (Insulin; 1); (Glucagon; 0) Unlike previous path, the assimilation of aspartame causes only an increase of insulin. Unfortunately, this increment is su cient to induce a decrease of blood glucose levels thus contradicting the formula above.
(Sugar; 0); (Aspartame; 1); (Glycemia; 1); (Insulin; 0); (Glucagon; 0) 2 ! (Sugar; 0); (Aspartame; 1); (Glycemia; 1); (Insulin; 1); (Glucagon; 0) 7 ! (Sugar; 0); (Aspartame; 0); (Glycemia; 0); (Insulin; 1); (Glucagon; 0) This illustrates the toxic behavior caused by aspartame described in Section 3. 6
The main application of our work concerns the veri cation of properties of
systems de ned in terms of rules or reactions. From a technical point of view, the
closest related work is on reaction systems [
In a broader sense, our work could also be related to P-systems [
We have introduced a high-level Petri net modeling of reaction networks to address problems related to toxicogenomics. In reaction networks, systems consist of a set of species present in the environment at a given level. Species can degrade with time progression and their presence is governed by a set of rules (reactions). In a reaction, species can have the role of reactants, inhibitors or products. A reaction can take place only if all reactants are available and all inhibitors are not. Depending on the type of reaction, products levels are either increased or decreased. We have shown that properties of biological systems can be expressed in a suitable temporal logic and veri ed on the nite state space of the network. We have illustrated our framework in the modeling of blood glucose regulation.
We are currently investigating how to enrich reactions with response time,
representing the required time for yielding products [
Finally, we have a prototype implemented with Snakes [
Acknowledgments. We would like to thank Michel Malo and the anonymous reviewers for their comments and insightful suggestions. This work was supported by the French project ANR BLANC 0307 01 - SYNBIOTIC.