Computational Methods in Systems Biology

210 B. Miraglio et al.

π 3 =ΔΔΔΔΔ︸ ︷︷ ︸

η 30

−D−−−−^2 destr→ΔΔΔεΔ

︸ ︷︷ ︸

η 31

−Pit−−−−destr→ΔεΔεΔ

︸ ︷︷ ︸

η 32

TSHsynth

−−−−−−−→ΔεθεΔ︸ ︷︷ ︸

η 33

THsynth

−−−−−−→θεθεΔ︸︷︷︸

η 33

Fig. 3.Possible path segment belonging toRthy. For the sake of simplicity, states
depicted here only contain the levels of respectively T4B,T3Pit,TSH,D 2 and XD2.

π 4 =ΔΔΔΔΔ︸ ︷︷ ︸

η 40

Detoxsynth

−−−−−−−−→ΔΔΔθΔ︸ ︷︷ ︸

η 41

−T−−−−^4 destr→εΔΔθΔ

︸ ︷︷ ︸

η 42

−Pit−−−−destr→εεΔθΔ

︸ ︷︷︸

η 42

TSHsynth

−−−−−−−→εεθθΔ︸︷︷︸

η 43

Fig. 4.Possible path segment belonging toRthy. For the sake of simplicity, states
depicted here only contain the levels of respectively T4B,T3Pit,TSH,DetoxandXHep.

The effect of XHep, namely the trigger of hepatic detoxifying enzymes leading
to decreased levels of T4Band then high levels of TSH can also be expressed
thanks toφHep:

φHep≡G(XHep>ε U (Detox =θU(T4B=εU(TSH =θ))))

Pathπ 3 andπ 4 as depicted in Figs. 3 and 4 , are examples of interesting
trajectories for toxicologists. Indeed, both these paths start in theinitial state
(init) defined as follow: the biological system is considered healthy (all the
endogenous entities atΔ) but contains also an exogenous compound (XD2or
XHepgreater thanε). Then, as an exogenous compound leads the organism
towards pathological states (here respectively a chronic hyperthyroidism and a
thyroid cancer), we can enumerate its possible pathways of tocixity by filtering
paths satisfying temporal formulas (here,init∧FG(T4B= θ)andinit∧
FG(TSH =θ)).

6 Conclusion

We presented a new formal framework able to handle several specificities of
the toxicology domain not taken into account so far. This rule-based model-
ing framework allows for a direct description of equilibrium changes happening
in a biological system. This description does not model the strength differences
between equilibrium rules, which can affect the global behavior of the system. For
this reason, we integrated biological and toxicological knowledge about equilibria
kinetics through formulas expressed in SE-LTL. As demonstrated on a simple
model of the thyroid hormone system, the expressive power of the formalism
enable us to describe equilibrium changes in the organism as well as knowl-
edge about equilibrium kinetics. This knowledge allows then the filtering out of
irrelevant paths from the initial model and the search for toxicity pathways.
In the future, our formalism will be coupled with a SE-LTL model checker
in order to list the most probable toxicity pathways present in a model. Indeed,