Analysing Gene Regulatory Networks by both Constraint Programming and Model-Checking

In this article, we propose a formal method to analyse gene regulatory networks (GRN). The dynamics of such systems is often described by an ordinary differential equation system, but has also been abstracted into a discrete transition system. This modeling depends on parameters for which different values are possible. Each instantiation of these parameters defines a possible dynamics and verification tools can be used to select the tuples of values which lead to dynamics consistent with known behaviours. GRN are so complex that their discrete modeling gives a number of possible dynamics exponential in function of the GRN´s size (number of genes and interactions). In this paper, we propose to use constraint programming and CTL formal language to determine the set of all dynamics consistent with the known behavioral properties without enumerating all of them. This approach allows us therefore to minimize the computation time necessary for the research of these parameters.