**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 [1].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 [3].**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 [4].