Home  > News from Ibis > PhD and Master thesis defenses

Pedro Tiago Gonçalves Monteiro - Towards an integrative approach for the modeling and formal verification of biological regulatory networks

PhD thesis defense at Instituto Superior Tecnico, Lisbon, May 17, 2010, 10 :AM

PhD thesis committee

Joaquim Armando Pires Jorge (president, Instituto Superior Tecnico, Lisbon, Portugal)

Jaco van de Pol (rapporteur, University of Twente, the Netherlands)

Claudine Chaouiya Chantegrel (rapporteur, Université de la Méditerranée, Marseille)

Maria Inês Camarate Lynce de Faria (examinatrice, Instituto Superior Tecnico, Lisbon, Portugal)

Ana Teresa Correia de Freitas (directrice de thèse, Instituto Superior Tecnico, Lisbon, Portugal)

Hidde de Jong (directeur de thèse, INRIA, Grenoble)

Radu Mateescu (directeur de thèse, INRIA, Grenoble)


The study of biological networks has led to the development of increasingly large and detailed models. While whole-cell models are not on the horizon yet, complex networks underlying specific cellular processes have been modeled in detail. The study of these models by means of analysis and simulation tools leads to large amounts of predictions, typically time-courses of the concentration of several dozens of molecular components in a variety of physiological conditions and genetic backgrounds. This raises the question how to make sense of these simulations, that is, how to obtain an understanding of the way in which particular molecular mechanisms control the cellular process under study, and how to identify interesting predictions of novel phenomena that can be confronted with experimental data.

Formal verification techniques based on model-checking provide a powerful technology to keep up with this increase in scale and complexity. The basic idea underlying model checking is to specify dynamical properties of interest as statements in temporal logic, and to use model-checking algorithms to automatically and efficiently verify whether the properties are satisfied or not by the model. The application of model-checking techniques is hampered, however, by several key issues described in this thesis.

First, the systems biology domain brought to the fore a few properties of the network dynamics that are not easily expressed using classical temporal logics, like Computation Tree Logic (CTL) and Linear Time Logic (LTL). On the one hand, questions about multistability are important in the analysis of biological regulatory networks, but difficult (or impossible) to express in LTL. On the other hand, CTL is capable of dealing with branching time, important for multistability and other properties of non-deterministic models, but it does not do a good job when faced with questions about cycles in a Kripke structure. Second, the problem of posing relevant and interesting questions is critical in modeling in general, but even more so in the context of applying model-checking techniques, due to the fact that it is not easy for non-experts to formulate queries in temporal logic. Finally, most of the existing modeling and simulation tools are not capable of applying model-checking techniques in a transparent way. In particular, they do not hide from the user the technical details of the installation of the model checker, the export in a suitable format of the model and the query, the call of the model checker, and the import of the results produced by the model checker (the true/false verdict and witness/counterexample).

In order to address these issues, in this thesis we propose three different approaches to tackle each of the issues. First, we propose a new temporal logic, called Computation Tree Regular Logic (CTRL), powerful enough to capture the biological properties of multistability (branching-time) and oscillations (linear-time). CTRL extends CTL with regular expressions and fairness operators, achieving a good compromise between expressive power, user-friendliness and complexity of model checking. Second, we propose a new pattern system, based on frequently-asked questions posed by modelers in systems biology. Each pattern is a high-level query template formulated in structured natural language rather than temporal logic, providing an automatic translation into temporal logic formulas. Third, we propose a service-oriented architecture capable of integrating modeling and simulation tools with current model-checking tools, providing a common environment for the modeling and the verification of biological regulatory networks. This architecture is generic and modular, capable of integrating different model checkers through the use of a plugin system and permitting the connection from different modeling and simulation tools.

The proposed methods were implemented in a new version of the tool Genetic Network Analyzer (GNA 7.0), through the development of a new verification module. This module provides a graphical user interface capable of helping the user with the specification of biological properties, as well as with the visualization and interpretation of verification results. In order to illustrate the use and applicability of the developed methods, GNA 7.0 has been used for the validation of two complex biological models. The first is a model of the network of regulators controlling the carbon starvation response in the bacterium Escherichia coli. The second is a model of the activation of the 12-spanner H+ drug antiporter encoding gene FLR1 in the presence of the fungicide mancozeb in the eukaryote Saccharomyces cerevisiae. Both models were checked for inconsistencies by confronting the model predictions with available experimental data. The identified inconsistencies were subject to further experiments and/or to model revisions.

Formal verification methods are promising tools for upscaling the analysis of biological regulatory networks. The implementation of the proposed approaches into a single integrative environment provide the modeler with a scalable and automated method for analysis of these networks. This thesis helps lower the obstacles to the use of formal verification technology in biology, opening the way for new perspectives like the exploration of symbolic approaches to further scale the size and complexity of the models, and the definition of diagnostics for the semi-automatic revision of the models.