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

合成生物学的新兴领域专注于创造小型合成遗传网络，将它们插入活细胞中，以便对细胞行为进行“编程”。最近的原型包括拨动开关、振荡器、逻辑门、浓度带探测器，甚至还有脉冲发生器。合成基因网络在生物技术、医学和国防相关领域有着巨大的应用前景。这种工程化的生物装置将进行简单的计算和细胞间的通讯，以诊断疾病、修复组织、检测和清理环境污染物，以及制造生物材料。合成生物学的主要挑战是创建和调整符合所需规格的基因网络。目前还没有正式的机制来保证这些系统的行为并先验地调整它们的参数以满足期望的性能。现有的形式分析工具由于非线性、不确定性、缺乏动力学和调控参数的知识以及受噪声干扰的测量而不能成功地处理遗传网络。然而，合成基因网络在组织工程等关键应用中的应用要求这些系统满足严格的安全保证。在这个项目中，我们提出了一种正向工程和分析合成基因网络的混合系统方法。在这个框架中，基于区间的规范转化为可达性分析和安全验证，这是形式分析的中心问题。通过利用化学反应和合作规则引起的特殊非线性，我们首先通过构造离散抽象将这些无限维问题转化为图上的有限搜索，然后将它们映射到参数值区间。该程序将允许在参数不确定的情况下进行分析，并将提供一种可证明是正确的方法来调整参数以获得所需的基于区间的属性。我们将用两个实验系统来验证我们的方法。我们将改进转录级联的稳态数字响应，并使用优化的级联来构建更健壮的触发开关。我们还将使用形式分析来微调脉冲发生器的动态行为，该脉冲发生器结合了细胞-细胞通信和前馈基元。

The 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.