202 B. Miraglio et al.
Definition 3 (Formula). The setFof formulason a signatureE is induc-
tively defined by:
- any atomic formula of the formab(whereaandbcan be any element of
E∪L) belongs toF.
–ifφandψare elements ofF, then¬φ,φ∧ψ,φ∨ψ,φ⇒ψare also elements
ofF.
Definition 4 (Satisfaction relation). A stateηand a formulaφ∈Fon a
signatureEbeing given, thesatisfaction relationηφis inductively defined by:
–ifφis an atom of the formab, thenηφif and only ifη(a)η(b)where
ηis the extension ofηtoE∪Lby the identity onL.
–ifφis of the formφ 1 ∧φ 2 thenη(φ 1 ∧φ 2 )if and only ifηφ 1 andηφ 2.
We proceed similarly for theother connectives.“ηφ”isread“ηsatisfiesφ.”We use the abbreviationa=bas a shortcut for (ab)∧(ba)andwe
proceed similarly fora<b,a>bandab.
Examples of formulas can beφ≡(I =θ), stating an excessive presence of I
orψ≡(T 4 >TPO), stating that the qualitative level of T 4 is strictly greater
than the one of TPO. The stateη 0 , previously described in Eq. 1 , satisfiesφbut
notψ.
To describe possible evolutions of the system, a set of rules of the following
form is then used:
r:A 1 +···+Am⇒Am+1+···+An when(φ) boost(ψ)Beside its identifierr, each rule includes two sets of entitiesAi. The first one,
for alliin [1,m], constitutes the set ofconsumables, whose level may be reduced
by the application of the rule. The other set, for alliin [m+1,n], represents
the set ofproduceableswhose level may be increased by the application of the
rule. A rule also includes two modulating conditionswhen(φ)andboost(ψ)(φ
andψbeing formulas). Intuitively,φthe role of the guard of the rule andψwill
relax some restriction on the increasing of produceable levels.
Definition 5 (Biological action network).A biological action network on a
signatureE,orE-action network, is a setRof rules of the form:
r:A 1 +···+Am⇒Am+1+···+An when(φ) boost(ψ)where:
- ris an identifier such that there are not two rules inNwith the samer.
- ∀i=1...n,Ai∈E.
- {A 1 ...Am}∩{Am+1...An}=∅.
- φandψare elements ofF.