206 B. Miraglio et al.
Definition 9 (Temporal formula).Given anE-action networkR, the setTR
of temporal formulasonRis inductively defined by:
- (A∪R∪{Id})⊂TR
–ifφandψare formulas ofTR, then¬φ,φ∧ψ,φ∨ψ,φ⇒ψ,Xφ,Fφ,Gφ,
φU ψare formulas ofTR.
Definition 10(Temporal formula satisfaction). Given an E-action net-
workRand a path(π≡η 0
r 0
−→η 1
r 1
−→...)∈ΠR, thesatisfaction relation
⊂ΠR×TRis inductively defined by:
- πα(where the atomαbelongs toA)ifandonlyifη 0 α,
- πrwherer∈R∪{Id}if and only ifr=r 0 ,
- πφ∧ψwhere(φ, ψ)∈TR^2 if and only ifπφandπψ, other proposi-
tional logic connectives are treated similarly, - πXφwhereφ∈TRif and only if(η 1
r 1
−→η 2
r 2
−→...)φ, - πGφwhereφ∈TRif and only if for alli∈N,(ηi−r→i ηi+1
ri+1
−−−→...)φ, - πFφwhereφ∈TRif and only if there existsi∈N,(ηi
ri
−→ηi+1
ri+1
−−−→
...)φ,- πφU ψwhere(φ, ψ)∈TR^2 if and only if there existsj∈N,(ηj
rj
−→...)
ψand for all 0 i<j,(ηi
ri
−→...)φ.Furthermore, for allr∈Rof the formr:A 1 +···+Am⇒Am+1+···+
An when(φ)boost(ψ), we noteapp(r) the temporal formula (
∧m
i=1Ai>ε)∧¬ψ
stating thatris applicable at the current state (see Definition 6 ).
In addition, for alle∈E, we note↓ethe temporal formula stating that the
level of the entityedecreases in the next state:
∨
l∈E(e){ε}
(
e=l∧X(
e=decre(l)))
.
We proceed similarly for↑e.
For instance in our running example, the propertyχcharacterizing paths where
an excess of I leads to a future excess of T 3 can be written as:G((I>Δ)⇒F(T 3 >
Δ)) and the formulaξstating that the rulerBis the first applied when T 4 is absent
from the system can be written as:G((T 4 =ε)⇒rB). In this situation, the path
beginning with (η 0
rB
−−→η 1 ), whereη 0 =(Δ, ε, ι, θ)andη 1 =(θ, ε, ι, θ) satisfies
bothχandξ.
Finally, the association of the transition graph of a system with a set of
properties representing the relevant biological pathways is called aconstrained
network. This constrained network is actually a subset of paths from the tran-
sition graph, with each path in this subset satisfying all the SE-LTL biological
properties.
Definition 11(Constrained network).AnE-constrained networkis a cou-
pleN=(R, Ax)whereRis anE-action network andAxis a set of temporal
formulas.
Definition 12(Dynamics of a constrained network). Given an E-
constrained network N =(R, Ax), the dynamics of N is the
subsetΠNofΠRsuch thatπ∈ΠRbelongs toΠN if and only ifπAx.