- 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.
To accelerate the process of refining a model, we seek to optimize the selection of biological experiments to implement in order to converge as quickly as possible to predictive modeling. The task is arduous because of observability constraints (not all system variables are observable) and operability constraints (some initial states can not be chosen). Formal models can help in the selection of the most discriminating experiences.
- 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 first 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. The DyMBioNet modeling environment includes SMBioNet
but adds a simulator and fair model-checking.
We have also developed an approach based on the Hoare logic and the calculation of the lowest precondition to generate the constraints on the values of the parameters. The observed behavior specifications play a role similar to that of the programs in the classical Hoare logic, and the lower precondition characterizes the compatible settings, expressed as constraints on the parameters.
- 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.
Recently, we developed a Hoare logic for these hybrid systems in order to build the constraints on the parameters of the model compatible with the observed traces. Holmes BioNet implements these ideas and uses the constraints solver AbSolute to produce solutions.