**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 *i*th variable *x _{i}* are called

**Application to the tuning and robustness analysis of a synthetic transcriptional cascade:**

**Acknowledgments:**

We would like to thank Michal Kvasnica (ETHZ, Switzerland) for his help in solving compatibility issues between MPT and Matlab.