View article

René Thomas’ discrete modelling of gene regulatory networks (GRN) is a well-known approach to study the dynamics resulting from a set of interacting genes. It deals with some parameters which reflect the possible targets of trajectories. Those parameters are a priori unknown, but they may generally be deduced from a well-chosen set of biologically observed trajectories. Besides, it neglects the time delays for a gene to pass from one level of expression to another one. The purpose of this paper is to show that we can account for time delays of increasing or decreasing expression levels of genes in a GRN, while preserving powerful enough computer-aided reasoning capabilities. We designed a more accurate abstraction of GRN where delays are now supposed to be non-null unknown new parameters. We show that such models, together with hybrid model-checking algorithms, make it possible to obtain …