TITLE:

Using Formal Temporal Logic to Model Biological Regulatory Networks
and to Propose New Wet Experiments.


AUTHORS:

Gilles BERNOT, Jean-Paul COMET, Janine GUESPIN


ABSTRACT:

Based on the discrete definition of biological regulatory networks developped
by René Thomas, we provide a computer science formal approach to treat
temporal properties of biological regulatory networks, expressed in
Computational Tree Logic.

It is then possible to automatically compute all the models whose behaviour
satisfies a set of given temporal properties. The chosen temporal properties
can reflect established knowledge about the model as well as hypotheses which
motivate the biological research.

If the set of computed models is empty, it proves that the biological
hypotheses contradict the current knowledge and they have to be reconsidered.

If at least one model exists then we can manipulate the temporal formulae
which formalize the hypotheses in a computer aided manner, according to some
logical rules. This allows us to derive a set of sensible wet experiments
capable to refute or validate the hypotheses.

Our approach is illustrated on the cytotoxicity example in Pseudomonas
aeruginosa.