Formal Methods for Modeling Biological Regulatory Networks

International audienceThis chapter presents how the formal methods can be used to analyze biological regulatory networks which are at the core of all biological phenomena as cell differentiation or temperature control. The dynamics of such a system, i.e. its semantics, is often described by an ordinary differential equations system, but has also been abstracted into a discrete formalism due to R. Thomas. This second description is well adapted to state-of-the-art measurement techniques in biology, which often provide qualitative and coarse-grained descriptions of biological regulatory networks. This formalism permits us to design a formal framework for analyzing the dynamics of biological systems. The verification tools, as model checking, can then be used not only to verify if the modeling is coherent with known biological properties, but also to help biologist in the modeling process. Actually, for a given biological regulatory network, a large class of semantics can be automatically built and model checking allows the selection of the semantics which are coherent with the biological requirement, i.e. the temporal specification. This modeling process is illustrated with the well studied genetic regulatory network controling immunity of bacteriophage lambda