- Methodological approach
A model should evolve to reflect the evolution of knowledge about the
biological system it represents. To avoid to repeat the entire
modeling process as soon as a new information contests the model, it
is necessary to handle, at every stage, not only a single model of the
biological system but all possible formalisations consistent with
biological knowledge. Thus, a new knowledge represents only an
additional constraint on the set of models .
In order to refine the model as quickly as possible, we would like to optimize the selection of experiments. The task is complicated by observational constraints (not all internal variables of the systems can be observed) and by operability constraints (some initial states cannot be chosen). The formal models should guide the selection of the more informative experiments. In particular we have shown that under some strong assumptions on experimental constraints, the selection process of experiments leads to a set of models which converges to a set of observationally indistinguishable models.
- Verification of behavioral properties
Verification of behavioral properties is fundamental to verify the
consistency of the built models with respect to known properties. The
group has developped a tool SMBioNet that automatically retrieves,
through intensive model checking, all the settings of a gene
regulatory graph leading to a behaviour consistent with the
knowledge/assumption, expressed via temporal logic formulae, about the
system dynamics. We also developped an approach based on Hoare
Logic and an associated weakest precondition calculus to generate
constraints on parameter values. Specifications of observed behaviours
play a similar role as programs in the classical Hoare logic, and
computed weakest preconditions characterizes the sets of all
compatible parameterizations, expressed as constraints on parameters [2a].
We also develop a hybrid linear logic Hyll (Hybrid Linear Logic) whose goal is to make proof trees directly on the formalised system, avoiding enumeration of all possible parameters. This logic is now supported by coq and λProlog to ease the generation of the proof [2b].
- Relationships between dynamics / structure of interactions.
When modelling a biological system, the generally available knowledge
resides in the structure of the regulatory network (represented by a
graph whose edges are oriented and usually signed). As the different
kinetic parameters that govern the behaviour are usually not known, it
could be interesting to infer as much as possible the dynamics from
the interaction graph. For example, it is now well known (and proven
in many modeling frameworks) that the presence of a positive feedback
loop in the structure is necessary for the existence of several fixed
points. We are currently investigating how to determine an interval
which, according to the structure, bounds the number of fixed points,
and how to distribute the signs on a partially signed graph to
maximize the number of fixed points .
- Chronometric information Chronometric information (which completes the knowledge on the sequence of events by adding temporal information on actions) are often easy to obtain from experiments but rarely used. Chronometric information includes the time required for the system to change state, or the time mandatory to go through a sequence (path) of states and observe the complete transformation. They could be used to constrain the parameterization of models, thus we are developing hybrid formal models for biological systems in which one can formally manipulate such chronometric information .