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

Introduction

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 P₁ reaches some threshold, the concentration of protein P₂ will start to increase only after some reaction R has stopped, corresponds to the CTL formula AG(P₁ → ((EFP₂) ∧ ¬E [RUP₂ ])).

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.