212 B. Miraglio et al.
Table 2.TheRthyaction network.Iintake : Ω ⇒ IB
Itransf er :IB ⇒ IT when(TSH>ε∧XI=ε)
TPOsynth : Ω ⇒ TPO when(TSH>ε) boost(TSH =θ)
TPOdestr : TPO ⇒ Ωwhen(TSH =ε∨(TPO =θ∧TSH<θ))
THsynth :IT ⇒ T3B+T4B when(TPO>ε) boost(TPO =θ)
Pitsynth :T4B ⇒ T3Pit when(D 2 >ε) boost(D 2 =θ)
Pitdestr :T3Pit ⇒ Ωwhen(T4B=ε∨D 2 =ε∨(T3Pit=θ∧D 2 <θ))
TSHsynth : Ω ⇒ TSH when(T3Pit<θ) boost(T3Pit=ε)
TSHdestr :TSH ⇒ Ωwhen(T3Pit=θ∨(TSH =θ∧T3Pit>ε))D (^1) synth : Ω ⇒ D 1 when(XD1=ε) boost(T3B=ε)
D (^1) destr :D 1 ⇒ Ωwhen(XD1>ε∨(D 1 =θ∧T3B>ε))
D (^2) synth : Ω ⇒ D 2 when(T3B<θ∧XD2=ε) boost(T3B=ε)
D (^2) destr :D 2 ⇒ Ωwhen(T3B=θ∨XD2>ε∨(D 2 =θ∧T3B>ε))
D (^3) synth : Ω ⇒ D 3 when(T3B>ε) boost(T3B=θ)
D (^3) destr :D 3 ⇒ Ωwhen(T3B=ε∨(D 3 =θ∧T3B<θ))
Detoxsynth : Ω ⇒ Detox boost(XHep>ε)
Detoxdestr : Detox ⇒ Ωwhen(Detox =θ∧XHep=ε)
Irecycling :T4B ⇒ IB when(D 1 >ε)
THactivation :T4B ⇒ T3B when(D 1 =θ∨D 2 >ε) boost(D 2 =θ)
T (^3) destr :T3B ⇒ Ωwhen(D 3 =θ∨Detox =θ∨(T3B=θ∧D 3 >ε))
T (^4) destr :T4B ⇒ Ωwhen(D 3 =θ∨Detox =θ∨(T4B=θ∧D 3 >ε))
References
- Barter, R.A., Klaassen, C.D.: Reduction of thyroid hormone levels and alteration
of thyroid function by four representative UDP-glucuronosyltransferase inducers
in rats. Toxicol. Appl. Pharmacol. 128 (1), 9–17 (1994) - Bernot, G., Comet, J.P., Richard, A., Guespin, J.: Application of formal methods to
biological regulatory networks: extending Thomas’ asynchronous logical approach
with temporal logic. J. Theor. Biol. 229 (3), 339–347 (2004) - Chabrier-Rivier, N., Fages, F., Soliman, S.: The biochemical abstract machine
BIOCHAM. In: Danos, V., Schachter, V. (eds.) CMSB 2004. LNCS, vol. 3082,
pp. 172–191. Springer, Heidelberg (2005). doi:10.1007/978-3-540-25974-9 14 - Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: State/Event-
based software model checking. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) IFM
2004. LNCS, vol. 2999, pp. 128–147. Springer, Heidelberg (2004). doi:10.1007/
978-3-540-24756-2 8 - Danos, V., Feret, J., Fontana, W., Harmer, R., Hayman, J., Krivine, J., Thompson-
Walsh, C., Winskel, G.: Graphs, rewriting and pathway reconstruction for rule-
based models. In: LIPIcs-Leibniz International Proceedings in Informatics, vol 18.
Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2012) - Dentice, M., Salvatore, D.: Local impact of thyroid hormone inactivation deiodi-
nases: the balance of thyroid hormone. J. Endocrinol. 209 (3), 273–282 (2011) - Fages, F., Soliman, S.: Formal cell biology in biocham. In: Bernardo, M., Degano,
P., Zavattaro, G. (eds.) SFM 2008. LNCS, vol. 5016, pp. 54–80. Springer,
Heidelberg (2008). doi:10.1007/978-3-540-68894-5 3