Model Checking Genetic Regulatory Networks using GNA and CADP

Organisation:	INRIA Rhône-Alpes (Grenoble, FRANCE)
Functionality:	Model checking of Genetic Regulatory Networks
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Period:	2004
Description:	The GNA (Genetic Network Analyzer) tool allows to model and simulate genetic regulatory networks using piecewise-linear differential equations. GNA produces a graph of qualitative states and transitions between qualitative states, which provides a discrete abstraction of the dynamics of the system. This approach is known as qualitative simulation. 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. To palliate this issue, the qualitative simulator GNA is connected with the verification technologies provided by the CADP toolbox. The connection is performed by the GNA2BCG translator from the graph format produced by GNA to the BCG format of CADP. The resulting BCG graph can be simplified by eliminating instantaneous states using abstraction and reduction modulo branching equivalence, and inspected visually by using the BCG_EDIT tool of CADP. Then, various temporal properties concerning the behavior of the regulatory network (evolution of protein concentrations, reachability of equilibrium states, etc.) can be modeled in regular alternation-free mu-calculus and verified using the EVALUATOR 3.0 model checker.
Conclusions:	By translating the state transition graph produced by GNA into a BCG graph, standard verification technologies become available for analyzing the dynamics of the underlying genetic regulatory network. The regular alternation-free mu-calculus is convenient to express branching-time properties of genetic regulatory networks in a concise way. Moreover, the diagnostic generation and interactive simulation facilities offered by CADP allow to establish a correspondence between verification results and biological data, for instance by characterizing evolutions leading to equilibrium states.
Publications:	[Batt-Bergamini-deJong-et-al-04] Grégory Batt, Damien Bergamini, Hidde de Jong, Hubert Garavel, and Radu Mateescu. "Model Checking Genetic Regulatory Networks using GNA and CADP". In Susanne Graf and Laurent Mounier, editors, Proceedings of the 11th International SPIN Workshop on Model Checking of Software SPIN'2004 (Barcelona, Spain), Lecture Notes in Computer Science vol. 2989, pp. 158-163, April 2004. Available on-line from http://cadp.inria.fr/publications/Batt-Bergamini-deJong-et-al-04.html and from the CADP Web site in PDF or PostScript [Batt-Ropers-deJong-et-al-05-a] Grégory Batt, Delphine Ropers, Hidde de Jong, Johannes Geiselmann, Radu Mateescu, Michel Page, and Dominique Schneider. "Analysis and Verification of Qualitative Models of Genetic Regulatory Networks: A Model-Checking Approach". In Leslie Pack Kaelbling and Alessandro Saffiotti, editors, Proceedings of the 19th International Joint Conference on Artificial Intelligence IJCAI'05 (Edinburgh, Scotland), pp. 370-375, July-August, 2005. Available on-line from http://cadp.inria.fr/publications/Batt-Ropers-deJong-et-al-05-a.html and from the CADP Web site in PDF or PostScript [Batt-Ropers-deJong-et-al-05-b] Grégory Batt, Delphine Ropers, Hidde de Jong, Johannes Geiselmann, Radu Mateescu, Michel Page, and Dominique Schneider. "Validation of Qualitative Models of Genetic Regulatory Networks by Model Checking: Analysis of the Nutritional Stress Response in Escherichia Coli". In Bioinformatics, volume 21, suppl. 1, 2005. Available on-line from http://cadp.inria.fr/publications/Batt-Ropers-deJong-et-al-05-b.html and from the CADP Web site in PDF or PostScript [Mateescu-Monteiro-Dumas-deJong-08] Radu Mateescu, Pedro Tiago Monteiro, Estelle Dumas, and Hidde de Jong. "Computation Tree Regular Logic for Genetic Regulatory Networks" Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis ATVA'08 (Seoul, South Korea), October 2008. Available on-line from http://cadp.inria.fr/publications/Mateescu-Monteiro-Dumas-deJong-08.html and from the CADP Web site in PDF or PostScript [Mateescu-Monteiro-Dumas-deJong-11] Radu Mateescu, Pedro Tiago Monteiro, Estelle Dumas, and Hidde de Jong. "CTRL: Extension of CTL with Regular Expressions and Fairness Operators to Verify Genetic Regulatory Networks". Theoretical Computer Science 412(26):2854-2883, June 2011. Available on-line from http://cadp.inria.fr/publications/Mateescu-Monteiro-Dumas-deJong-11.html and from the CADP Web site in PDF or PostScript
Contact:	Dr. Hidde de Jong INRIA Rhône-Alpes Montbonnot 38334 Saint Ismier Cedex FRANCE Tel: +33 (0)4 76 61 53 35 Fax: +33 (0)4 76 61 54 08 E-mail: Hidde.de-Jong@inria.fr
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page