RoVerGeNe: A tool for the Robust Verification of Gene Networks
Grégory Batt and Calin Belta
Center for BioDynamics
Center for Information and Systems Engineering
Boston University
Rovergene is a tool for the analysis of genetic regulatory networks under parameter uncertainty.
Genetic regulatory networks are described by a class of piecewise multiaffine differential equation models, dynamical properties are expressed in linear temporal logic and uncertain parameters are specified by intervals.
The tool addresses two problems:
- robustness analysis: checking whether a dynamical property is satisfied by every parameter in a given set and for every initial state in a given region. The parameter set is then called valid.
- parameter constraint synthesis: searching for valid subsets of a given parameter set.
Rovergene can be used for the analysis of the robustness of dynamical properties of gene networks with respect to parameter variations and for the
tuning of synthetic gene networks.
Rovergene is an implementation of the approach presented in:
- G. Batt and C. Belta(2006)
Model Checking Genetic Regulatory Networks with Applications to Synthetic Biology, CISE technical report 2006-IR-0030. - G. Batt, C. Belta and R. Weiss (2006) Model checking genetic regulatory networks with parameter uncertainty. Submitted. [link]
- G. Batt, C. Belta and R. Weiss (2006) Model checking liveness properties of genetic regulatory networks. Submitted. [link]
Implementation and installation notes:
Rovergene is written in Matlab and uses the toolbox MPT for polyhedral operations, the library matlabBGL for graph operations and the CTL/LTL model checker NuSMV. Rovergene has been developed with Matlab 7.0.1, NuSMV 2.2.4 and Cygwin 6.8.2.0-4. Note that it may not work with previous versions of these tools. It works on Linux and Windows operating systems.
For Linux systems, NuSMV must be installed and the path sets such that NuSMV can be called from the working directory. MPT and matlabBGL are thirdparty packages send with the distribution. Finally, we assume that the folder rovergene_folder/exports is writable. For Windows, in addition to the above requirements, Cygwin must be installed, since NuSMV runs on top of Cygwin. Note that Matlab should then be started from Cygwin, in order that system calls work properly.
Download (latest version 3.0)
Download Rovergene (tgz, zip). If you need any help, please feel free to contact us by email (contact: {batt,cbelta}@bu.edu).
Using the tool:
We illustrate the use of the tool by means of the two-gene network represented below. Note that we assume here a familiarity with the concepts and notations presented in the above-mentioned technical report.
The network is represented by the following pair of piecewise multiaffine differential equations. Note that the production rate parameter of gene a, κa, is an uncertain
parameter.
An expected property of this cross-inhibition network is that the protein concentrations can not remain both high nor both low. This property can be
expressed in temporal logic by the following formula
When running Rovergene, the user should specify the type of analysis (0 for robustness analysis or 1 for parameter constraint synthesis) and the name of the
model file. The models are described in text files that are assumed to be stored as rovergene_folder/models/model_name.txt.
A typical execution is represented here with some comments. For robustness analysis, the result of the analysis is a message saying that the property is satisfied by all parameters in the set or that no conclusions were obtained. For parameter constraint synthesis, the (possibly empty) list of polytopes corresponding to valid sets is displayed (see here again).
Model specifications:
Models are given as text files. The model corresponding to the two gene network is given here. They consists in three parts: description of the state space (number of variable, and for each variable, values that define the partition), description of the differential equations of the variables (specification of production and degradation functions), and description of the dynamical properties (atomic propositions and LTL formula).
In the following, the values that define the partition in the direction of the ith variable xi are called λij. To facilitate parsing, the regulation functions should be given using a prefix notation (ie “+ 2 2” instead of “2 + 2“). The terms are the constant 1, the binary operator * for multiplication (“* a b” means “a*b“), the unary operator - for negation (“- a” means “1-a“) and the ternary operator r used for representing ramp functions. More specifically, with i a variable index, k an array of λ-indices and y an array of reals comprised between 0 and 1, the term r i k y represents the ramp function having xi as a variable and evaluating to yj at point λij, for all j in k. For example, one can check that “r 1 [1 4 5 6] [0 0 1 1]” represents r+(xa,θa3,θa4). Atomic propositions corresponding to xi >λij or xi < λij are represented as {i ‘>’ j} or {i ‘<‘ j}. The LTL formula is expressed using the NuSMV syntax and using prop1, prop2, etc. for atomic propositions. Finally the flag “compute liveness of SCCs” should be set to 1 for a correct evaluation of the liveness properties. In special cases, notably in absence of feedback loops, tighter results may be obtained by turning this flag off.
Application to the tuning and robustness analysis of a synthetic transcriptional cascade:
We have studied the synthetic transcriptional cascade built by Hooshangi et al. (PNAS, 2005). You can download the models corresponding to our analysis of the possibilities to tune the system in which three parameter vary in large intervals, or corresponding to our analyses of the robustness of a modified (i.e. tuned) version of the network, where all uncertain parameters range in intervals corresponding to variations of ±10% or ±20% with respect to their reference values.
Acknowledgments:
We would like to thank Michal Kvasnica (ETHZ, Switzerland) for his help in solving compatibility issues between MPT and Matlab.