The nascent field of synthetic biology is focused on creating small synthetic genetic networks inserting them into living cells in order to "program" cellular behavior. Recent prototypes include a toggle switch, an oscillator, logic gates, concentration band detectors, and even a pulse generator. Synthetic gene networks are foreseen to have tremendous applications in biotechnology, medicine, and defense related areas. Such engineered biological devices will engage in simple computations and cell-cell communications to diagnose diseases, repair tissues, detect and clean up environmental pollutants, and manufacture biomaterials. The main challenge in synthetic biology is creating and tuning gene networks to desired specifications. There is currently no formal mechanism to guarantee the behavior of these systems and to tune their parameters a-priori to satisfy desired performances. The existing tools for formal analysis cannot handle genetic networks successfully due to nonlinearities, uncertainties, scarce knowledge of kinetic and regulatory parameters, and measurements corrupted by noise. However, the adoption of synthetic gene networks in critical applications such as tissue engineering requires that these systems meet strict safety guarantees. In this project, we propose a hybrid systems approach to forward engineer and analyze synthetic genetic networks. In this framework, interval-based specifications translate to reachability analysis and safety verification, which are the central problems of formal analysis. By exploiting the particular nonlinearities induced by chemical reactions and cooperative regulations, we first reduce these infinite dimensional problems to finite searches on graphs by constructing discrete abstractions, and then map them to parameter value intervals. This procedure will allow for analysis under parameter uncertainty and will provide a provably correct methodology to tune the parameters to achieve desired interval-based properties. We will validate our approach with two experimental systems. We will improve the steady state digital response of a transcriptional cascade and use the optimized cascades to build more robust toggle switches. We will also use formal analysis to fine-tune the dynamic behavior of a pulse generator that incorporates cell-cell communication and a feed-forward motif.
