• Research Areas
• Search Publications Database
• Awards
• Affiliated BU Labs and Centers
• Government SponsorsManage Publications

Abstract #2006-IR-0030

Model Checking Genetic Regulatory Networks with Applications to Synthetic Biology - CISE Technical Report
Batt, Gregory and Belta, Calin
September 2006
CISE Technical report, September 2006
Document #: 2006-IR-0030
Keywords: discrete abstraction, model checking, piecewise multiaffine model, parameter uncertainty, liveness verification, synthetic biology, genetic regulatory network

The lack of precise numerical information for the values of biological parameters severely limits the development of models of genetic regulatory networks. To deal with this problem, we developed a method for the analysis of genetic regulatory networks with parameter uncertainty. More precisely, we consider genetic regulatory network models based on piecewise-multiaffine diffierential equations, dynamical properties expressed in temporal logic, and intervals for the values of uncertain parameters. The problem is then either to guarantee that the system satisfies the expected properties for every possible parameter value - the corresponding set of parameter values is then called valid - or to find valid subsets of the given parameter set. The proposed method uses discrete abstractions and model checking and allows to search efficiently the parameter space for valid sets. For the verification of liveness properties, an important class of dynamical properties, an extension of the proposed approach is needed to capture the requirement of progress of time. A solution to this second problem is proposed using the notion of transient sets. This approach has been implemented in a tool for the robust verification of genetic networks (RoVerGeNe) and applied to the tuning of a synthetic genetic regulatory network build in E. coli.