基于高阶逻辑定理证明的生物电路形式化分析

合成生物学是一门跨学科领域，利用来自电气、控制与计算机系统等既成的工程原理来分析生物系统，如生物电路、酶、通路与控制器。传统上，这些生物系统即基因电路使用纸笔证明与基于计算机的仿真技术进行分析。然而，由于人类易错性、舍入误差以及工具核心中存在的未验证算法等固有局限，这些方法无法提供准确结果。本文提出使用高阶逻辑定理证明作为分析这些系统的补充技术，从而克服上述问题。具体而言，我们提出一个基于高阶逻辑定理证明的框架，以形式化推理合成生物学中使用的基因电路。主要思想是首先使用微分方程对基因电路的连续动力学建模；下一步从其相应的框图表示获得系统的传递函数；最后利用拉普拉斯变换对这些基于微分方程的模型进行基于传递函数的分析。为说明我们所提框架的实际应用，我们形式化分析了蛋白质的激活与抑制表达的基因电路。