Temporal Logic Analysis of Gene Networks Under Parameter Uncertainty

The lack of precise numerical information for the values of biological parameters severely limits the development and analysis of models of genetic regulatory networks. To deal with this problem, we propose a method for the analysis of genetic regulatory networks under parameter uncertainty. We consider models based on piecewise-multiaffine differential 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 parameter set is then called valid-or to find valid subsets of a given parameter set. The proposed method uses discrete abstractions and model checking and allows for efficient search of the parameter space. However, the abstraction process creates spurious behaviors in the abstract systems, along which time does not progress. Consequently, the verification of liveness properties, expressing that something will eventually happen, and implicitly assuming progress of time, often fails. A solution to this second problem is proposed using the notion of transient regions. This approach has been implemented in a tool for robust verification of gene networks and applied to the tuning of a synthetic network built in E. coli.