TITLE:

On the use of temporal formal logic to deduce the parameters
of a gene regulatory network model


ABSTRACT:

The discrete modelling of biological regulatory networks developped by René
Thomas in the 70's allows to define a framework where formal logic and tools
from computer science can be applied. Temporal properties, expressed in
Computational Tree Logic, can be automatically and systematically checked
against many hypothetical models.

It is then possible to encode some biological knowledge and to automatically
compute the set of models that are biologically sensible. The chosen temporal
properties can reflect established knowledge about the biological system as
well as hypotheses that motivate the biological research.

In the biological modelling activity, the main difficulty is almost always the
determination of parameter values of the models. Owing to our logical
approach, if the computed set of sensible models is not empty, it exhaustively
describes the sensible parameter values of the models.

Even better: we can manipulate the temporal formulae that formalize the
hypotheses to extract their "observable consequences." This allows us to
derive a set of wet experiments capable to refute (or validate) the
hypotheses.

Our approach is illustrated on the simple mucus production example in
Pseudomonas aeruginosa, a bacteria involved in cystic fibrosis.