A major goal in synthetic biology is to design and construct gene networks implementing desired behaviors in living organisms. Such networks are foreseen to have important applications in biotechnology and medicine. However, in addition to experimental limitations, the lack of precise information on parameter values hampers the efficient, rational design of networks.

We propose an approach for the verification of dynamical properties of gene networks in presence of parameter uncertainties. We consider a class of piecewise multiaffine (PMA) differential equation models, dynamical properties expressed in temporal logic, and uncertain parameters given as intervals. Then, we can test whether the dynamical properties are satisfied for every parameter in the given set – the set is then called valid – or search for valid parameter subsets. This applies to network robustness analysis or network tuning. The proposed approach combines discrete abstractions and model checking. Discrete abstractions are used to obtain a discrete representation of the dynamics of the system in the state and parameter spaces. The verification of the dynamical properties of the abstract system is then performed by model checking. Conservative approximations are used that guarantee that the parameter sets returned by the procedure are valid. However, we may fail to identify all valid parameter sets. To achieve efficiency, a hierarchical exploration of parameter space is performed.

The approach has been implemented in a publicly-available tool called RoVerGeNe, and applied to the analysis of three synthetic transcriptional cascades comprising one, two or three repression stages, build in E. coli. Like other regulatory cascades, they present an ultrasensitive response to graded input changes. Based on available experimental data, we developed PMA models of the cascades. Then, we tuned the three-stage cascade to satisfy precise input/output specifications by searching for valid parameter sets. Biologically-relevant constraints involving three key parameters were obtained. The robustness of the proposed tuned network was verified by leaving up to 11 parameters vary in intervals centered at their reference value. We show that the property is robustly satisfied by the tuned network for modest (±10%) but not large (±20%) parameter variations. A similar study for the single-stage cascade indicated that it is probably not biologically-feasible to tune this cascade to meet the same specifications. These case studies demonstrate the capacity of this approach to analyze synthetic gene networks of realistic size and complexity and to provide biologically-meaningful results. Besides synthetic biology applications, natural network robustness could be analyzed similarly.