BIC: Collaborative Research: Rational Design of Synthetic Gene Networks using Formal Analysis of Hybrid Systems

点击翻译按钮获取中文摘要

AbstractThe nascent field of synthetic biology is focused on creating small synthetic genetic networksinserting them into living cells in order to "program" cellular behavior. Recent prototypes includea toggle switch, an oscillator, logic gates, concentration band detectors, and even a pulsegenerator. Synthetic gene networks are foreseen to have tremendous applications inbiotechnology, medicine, and defense related areas. Such engineered biological devices willengage 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 desiredspecifications. There is currently no formal mechanism to guarantee the behavior of these systemsand to tune their parameters a-priori to satisfy desired performances. The existing tools for formalanalysis cannot handle genetic networks successfully due to nonlinearities, uncertainties, scarceknowledge of kinetic and regulatory parameters, and measurements corrupted by noise. However,the adoption of synthetic gene networks in critical applications such as tissue engineering requiresthat these systems meet strict safety guarantees.In this project, we propose a hybrid systems approach to forward engineer and analyze syntheticgenetic networks. In this framework, interval-based specifications translate to reachabilityanalysis and safety verification, which are the central problems of formal analysis. By exploitingthe particular nonlinearities induced by chemical reactions and cooperative regulations, we firstreduce these infinite dimensional problems to finite searches on graphs by constructing discreteabstractions, and then map them to parameter value intervals. This procedure will allow foranalysis under parameter uncertainty and will provide a provably correct methodology to tune theparameters to achieve desired interval-based properties. We will validate our approach with twoexperimental systems. We will improve the steady state digital response of a transcriptionalcascade and use the optimized cascades to build more robust toggle switches. We will also useformal analysis to fine-tune the dynamic behavior of a pulse generator that incorporates cell-cellcommunication and a feed-forward motif.