Modeling and Analysis of Gene Regulatory Networks - Modeling in Computational Biology and Biomedicine - page 69

2.3.2.4 Formal Methods

SMBioNet. Given an interaction graph G , the number of asynchronous state graphs
that we can build with the logical method is finite. For instance, 90 different
asynchronous state graphs can be built from the interaction graph of Fig. 2.9 . 2
A natural question is then: How to find, among this finite set of asynchronous
state graphs, those that are coherent with biological observations (or hypothesis)
on the dynamics of the system?
Formal methods are useful to perform automatically such a selection. First, a
temporal logic can be used to translate the dynamical observations into a temporal
formula Φ , which can be handled by a computer. Then, one can use model-checking
algorithms in order to check automatically if a given state graph (a model) satisfies
or not formula Φ . Hence, to solve the question, the following (basic) approach can
be used: enumerate the different asynchronous state graphs, and select those that
satisfy Φ using model-checking techniques .
This enumerative approach has been implemented in a software called
SMB IO N ET [ 8 ]. The temporal logic used is the well known Computational Tree
Logic (CTL) [ 19 ], and the verification step is performed with the model-checker
called N U SMV [ 11 ]. The Computational Tree Logic is briefly presented in the next
paragraph. An illustration, on a real case, of this logic and the enumerative approach
is then given in Sect. 2.3.3 .
But before going further, let us briefly discuss the enumerative approach. The
obvious limitation is that the number of state graphs to enumerate (which increases
exponentially with the number of components) is often too huge to consider
networks with more than ten genes or so. The obvious interest is that temporal logic
and model checking allow us to handle automatically rather complex dynamical
properties, and that the method is exhaustive: all the state graphs associated with G
that are consistent with Φ are reported. (For other applications of formal methods
in the context of gene regulatory networks, see for instance [ 6 , 7 , 13 , 14 ]andthe
references therein.)

Computational Tree Logic. In an asynchronous state graph, a given state has
generally several successors. So without additional information, all the successors
are possible next states: the dynamical description is undeterministic. In other
words, given an initial state x , the possible evolutions of the system are given by
the set of paths starting from x , and these paths may be seen as a tree rooted at x .

2 For the interaction graph of Fig. 2.9 ,wehave b 1 ∈{ 1 , 2 } , t 11 ,t 12 ∈{ 1 ,b 1 } and b 2 = θ 21 =1 .
If b 1 =1 ,then t 11 = t 12 =1 ,andthereare 18 possible instantiations of the parameters K ,
which lead to a set of 18 different asynchronous state graphs. If b 1 =2 there are two cases. First,
if t 11 =1 <t 21 =2 ,thereare 60 possible instantiations of the parameters K , which lead to
aset S of 42 different asynchronous state graphs. Second, if t 11 =2 >t 21 =1 ,thereare 60
possible instantiations of the parameters K , which lead also to a set of 42 different asynchronous
state graphs, but 12 of them are contained in S . Hence, the total number of asynchronous state
graphs is 18 + 42 + 42 − 12 = 90 .