The study of genetic regulatory networks has received a major impetus from the recent development of high-throughput genomic techniques. This experimental progress calls for the development of appropriate computer tools supporting the analysis of genetic regulatory processes. We have developed a modeling and simulation method, based on piecewise-linear differential equations, that is well-adapted to the qualitative nature of most available biological data. The method has been implemented in the tool Genetic Network Analyzer (GNA), which produces a graph of qualitative states and transitions between qualitative states. The graph provides a discrete abstraction of the dynamics of the system. A bottleneck in the application of the qualitative simulation method is the analysis of the state transition graph, which is usually too large for visual inspection. In this paper, we propose a model-checking approach to perform this task in a systematic and efficient way. In particular, we will connect the qualitative simulator GNA with the verification technologies provided by the CADP toolbox. A dedicated translator has been developed, which converts the state transition graph resulting from qualitative simulation into a form suitable for automated verification. After instantaneous states have been abstracted away by means of branching bisimulation, various properties characterizing the evolution of protein concentrations are checked by encoding them as regular alternation-free mu-calculus. The diagnostics produced by the CADP model checker allow to establish a correspondence between verification results and biological data, for instance by characterizing evolutions leading to equilibrium states. We illustrate the combined use of qualitative simulation and model checking by means of a simple, biologically-inspired example.

Paper

(PDF, 133.5 ko)

Presentation

(PDF, 5.4 Mo)