Improved Model Checking Techniques for State Space Analysis of Gene Regulatory Networks

Improved Model Checking Techniques for State Space Analysis of Gene Regulatory Networks

Hélio C. Pais (Cadence Research Laboratories, USA and INESC-ID/IST, Portugal), Kenneth L. McMillan (Cadence Research Laboratories, USA), Ellen M. Sentovich (Cadence Research Laboratories, USA), Ana T. Freitas (INESC-ID/IST, Portugal) and Arlindo L. Oliveira (Cadence Research Laboratories, USA)
DOI: 10.4018/978-1-60566-685-3.ch016
OnDemand PDF Download:
No Current Special Offers


A better understanding of the behavior of a cell, as a system, depends on our ability to model and understand the complex regulatory mechanisms that control gene expression. High level, qualitative models of gene regulatory networks can be used to analyze and characterize the behavior of complex systems, and to provide important insights on the behavior of these systems. In this chapter, we describe a number of additional functionalities that, when supported by a symbolic model checker, make it possible to answer important questions about the nature of the state spaces of gene regulatory networks, such as the nature and size of attractors, and the characteristics of the basins of attraction. We illustrate the type of analysis that can be performed by applying an improved model checker to two well studied gene regulatory models, the network that controls the cell cycle in the yeast S. cerevisiae, and the network that regulates formation of the dorsal-ventral boundary in D. melanogaster. The results show that the insights provided by the analysis can be used to understand and improve the models, and to formulate hypotheses that are biologically relevant and that can be confirmed experimentally.
Chapter Preview


The next advances in the field of systems biology are critically dependent on a better understanding of gene regulatory networks, and abstract models are essential in order to improve our understanding of the complex mechanisms underlying gene regulation.

Indeed, the highly complex transcriptional regulation of gene expression in eukaryotes occurs through the coordinated action of multiple transcription factors, and can be understood in detail only if one views the system as a network.

Regrettably, the complex physical and biochemical mechanisms involved in gene regulation make it difficult to identify regulatory mechanisms directly from first principles, and even sophisticated experimental methods are difficult to apply directly to the identification of the parameters of gene regulatory networks. For these reasons, computational approaches that help researchers identify and analyze genetic regulatory networks are essential, and represent a fundamental tool in our quest for the understanding of organisms as biological systems.

Gene regulatory networks, as well as other biological networks, have been modeled and studied using a variety of levels of abstraction. At the more detailed levels, ordinary differential equations (ODE) that relate different concentration levels within the cells have been used to model the dynamics of some small, well understood systems. Less detailed qualitative models have been extensively used to perform analysis of more complex systems [de Jong et al., 2003, Chabrier and Fages, 2003, Li et al., 2004, Garg et al., 2007], and have the advantage that they require less knowledge of the exact parameters governing the dynamics of the system. In qualitative models each of the components of the system (gene, protein, metabolite, etc.) is represented as a variable with a finite domain, and each variable is updated in accordance with a discrete transition function, that specifies its value as a function of the present value of the variables of the system.

Qualitative models have a number of significant advantages over quantitative ones. They can be used to analyze larger systems and, perhaps more importantly, existing tools, such as model checkers, can be used to analyze not only a particular trajectory of the system in state space, but also to characterize the state space as a whole. Understanding the characteristics of the state space can lead to important insights on how these networks have evolved and are wired. One of the problems of using qualitative models is the large number of behaviors that are possible, when one is dealing with complex systems whose dynamics cannot be sufficiently constrained. Model checking techniques have been proposed to deal with this problem.

Verification of biological network properties based on model checking provides a powerful method to analyze models of molecular interaction networks [Shults and Kuipers, 1997]. Using this methodology coerces the user to formulate interesting questions, and to interpret the answers, something that is especially difficult when dealing with very large models. The problem of posing relevant questions is critical in model assessment, in general, but even more so when using model checking. For instance, a property like once the concentration of protein P1 reaches some threshold, the concentration of protein P2 will start to increase only after some reaction R has stopped, corresponds to the CTL formula AG(P1 → ((EFP2)¬E [RUP2 ])).

The next sections describe how a model checker that includes some extra functionality can be used to analyze the characteristics of the state space of a gene regulatory network, and obtain additional insight about the behavior of the biological system.

Key Terms in this Chapter

Gene regulatory networks: A gene regulatory network is a collection of DNA segments in a cell which interact with each other and with other substances in the cell, thereby governing the rates at which genes in the network are transcribed into mRNA

Dorsal Ventral Boundary: Boundary between different cell types at the Drosophila wing

Gene Regulation: The processes that cells and viruses use to turn the information in genes into gene products

Cell Cycle: Is the series of events that take place in a cell leading to its division and duplication (replication).

Model Checking: To algorithmically check whether a simplified model of a system satisfies a given specification

State Transition Graph: A graph consisting of circles to represent states and directed line segments to represent transitions between the states.

Computation Tree Logic: It is a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realized.

Complete Chapter List

Search this Book: