Detecting Toxicity Pathways with a Formal Framework 209through SE-LTL properties. For instance, we express the fact thatTHactivation
always primes onIrecyclingas long as there is no shortage of blood iodide:
φ 0 ≡G((IB>ε∧app(THactivation)∧app(Irecycling))→¬Irecycling)Literally,φ 0 means that if IBis present in the system, and bothTHactivationand
Irecyclingare applicable, thenIrecyclingdoes not apply. TheGoperator indicates
that the property must be satisfied at every step of the path.
It has also been observed that an excess of detoxifying enzymes quickly leads
to the depletion of T4B:
φ 1 ≡G((Detox =θ∧app(T (^4) destr))→T (^4) destr)
We can also check that the model verifies global biological properties such
as the fact that without any disruption in D 2 functionning, an hypothyroidic
state (i.e.where T4Bis lacking) leads to a state where TSH is in excessive
concentration:
φ 2 ≡G(T4B=ε∧XD2=ε)→F(TSH =θ))
Of course, several paths belonging toRthydo not satisfy the previous prop-
erties. For instance, letπ 1 andπ 2 the portions of path represented in Fig. 2 .In
stateη 12 ofπ 1 , the conditions ofφ 0 are satisfied andIrecyclingshould not be
applied. Therefore,π 1 does not satisfyφ 0 , contrary toπ 2.
As such, if we considerAxthy={φ 0 ,φ 1 ,φ 2 }and the constrained network
Nthy=(Rthy,Axthy), paths includingπ 1 do not belong toNthy.
π 1 =Δεε︸︷︷︸
η 10
THsynth
−−−−−−→ΔΔε︸︷︷︸
η 11
THactivation
−−−−−−−−−→ΔΔΔ︸︷︷︸
η 12
Irecycling
−−−−−−−→ΔεΔ︸︷︷︸
η 13
π 2 =︸︷︷︸εεε
η 20
THsynth
−−−−−−→εΔε︸︷︷︸
η 21
−TH−−−−−−−−activation→εΔΔ
︸︷︷︸
η 22
Irecycling
−−−−−−−→ΔΔΔ︸︷︷︸
η 12
Fig. 2.Possible path segments belonging toRthy. For the sake of simplicity, states
depicted here only contain the levels of respectively IB,T4Band T3B.
Finally, we can use the constrained networkNthyto search for existing path-
ways of toxicity. Indeed, possible disruptions described in Sect. 2 correspond to
sets of paths belonging toNthy. These sets of paths can be identified thanks
to temporal formulas. For example, the inactivation of D 2 by XD2leading to
hyperthyroidism corresponds to paths satisfyingφD2:
φD2≡G(XD2>ε U (D 2 =εU(T3Pit=εU(TSH =θU(T4B=θ)))))