Marked regulatory graphs: a formal framework to simulate biological regulatory networks with simple automata

In the field of biological regulation, models obtained from experimental biology are usually complex networks of induction and repression between genes. Due to the development of high throughput genomic, it is now necessary to treat large scale networks. The challenge is to automatically analyze their behavior. We propose a formal framework to define these biological regulatory networks. Our model is derived from R. Thomas representation, where a biological regulatory network can be seen as a discrete model. We propose a formal definition of such a representation. We separate the static part (description of the systems) from the dynamic part (we develop two semantics, synchronous or asynchronous, to illustrate our method). A software environment to support this framework is also described. This software, developed to be used by biologists, can be used to rapidly obtain a prototype describing the behavior of the system, for product simulations and to automize proofs of properties.