**
J.-P. Comet, P. Le Gall and G. Bernot
**

LaMI UMR CNRS 8042, Université d'Evry Val d'Essonne Boulevard F. Mitterrand 91025 Evry Cedex

Regulatory networks are found at the core of all biological functions from bio-chemical pathways to gene regulation and cell communication processes. Because of the complexity of the interweaving retroactions, the overall behavior is difficult to grasp and the development of formal methods is needed in order to model and simulate the biological system. R. Thomas and co-workers developped a qualitative approach to model the behavior of biological regulatory networks which is described by a state transition system (called model) depending of some parameters. Because of the absence of knowledge on these parameters, the main modelling activity concentrates on the determination of the valuable values of parameters. It has been already shown that the parameters can be constrained using available biological knowledge on homeostasis, multistationarity or on observed experimental dynamics.In order to reduce again the set of models to be considered, some other experiments could be done. Results allow us to separate the possible set of models into two distinct parts: the set of models coherent with the result of the new experiment and the set of others. We propose to help the biologist to select a "good" experiment, in other words an experiment whose result (whatever the result) is able to reduce the set of models to be taken into account. An experiment consists often to put the system in a particular state (partially specified) and to observe if one or several gene products are present or not. This kind of experiment can be described in a temporal logic, and the experimental result is binary. Model checking can then verify the coherence between a particular model and the experiment expressed in term of temporal logic. Our problem becomes to select a possible experiment (temporal formula) which divides the set of considered models into 2 parts: the models validating the formula and the others.

If the biologist has some intuition on the system, he would like to select a good experiment which will discard a maximal number of undesirable models. At the opposite if all models are supposed to be identically likely, a possible strategy consists in selecting a formula which slices the set of models into two parts of approximately same size. These elementary steps can be iterated until getting a unique model or a small set, manageable by the biologist. Modelling allows one to build a priori all the partitions induced by experiment formulae, and this for all sets of models. It becomes possible to select experiments to be performed in order to minimize the total cost of experiments.

We illustrate this approach in the particular framework of the modelling of the mucus production of Pseudomonas aeruginosa.