计算树逻辑模型检测的DNA计算方法研究

The Computation Tree Logic (CTL, for short) model checking is becoming a research focus in formal methods. In order to improve the efficency of CTL model checking, we will construct a series of molecular biological methods for CTL model checking. We will carry out our research from the following three aspects: (1) using artificial micro operations and logical structures to realize a non-autonomous algorithm for CTL model checking; (2) employing the molecular self assembly technique at nano scale in order to realize an autonomous method for CTL model checking. These studies will breakthrough the lowest bound of complexity of CTL model checking problem by using DNA computing due to its highly parallel computing. Thus, a new pathway for CTL model checking will be opened up. And the library of solved problems by using the DNA computing will be further enriched.

计算树逻辑模型检测是形式化方法研究的一个热点。为了提升该逻辑模型检测的效率，本项目构建计算树逻辑模型检测的分子生物计算方法。我们拟从两个方面开展研究，分别是：人工实验微操作与逻辑结构相结合以实现模型检测计算功能的非自治算法、纳米尺度下分子自组装以实现模型检测计算功能的自治方法。上述这些研究将利用高度并行的DNA计算机制从根本上突破经典计算中该问题的效率限制，从而为计算树逻辑模型检测开拓出一条有别于传统的全新路径，同时进一步丰富DNA计算已解决的问题库。

计算树逻辑（Computation Tree Logic，CTL）模型检测是形式化方法研究的热点，是保证系统正确性的重要手段之一。DNA计算是以生化操作为计算手段的一种生物计算模式，具有巨大信息存储容量、大规模运算并行性和超低能耗等特点，在解决复杂计算问题、信息存储、纳米材料组装及体外体内分析方面有着巨大的应用潜力。开展CTL模型检测的DNA计算方法研究，不仅可以利用DNA计算的强大并行优势解决模型检测状态空间爆炸问题，而且对推动DNA计算机的研发具有重要意义。更重要的是，通过DNA计算研究，以计算思维揭示生命本质和纳米材料特性，在医疗和新材料开发等领域具有重要的应用。. DNA计算框架下的CTL 模型检测问题由图灵奖获得者Emerson教授提出。但只能检测一个基本公式。为提升CTL模型检测的DNA计算方法的检测能力和自治性，提升CTL模型检测的效率，扩展其应用领域，本项目构建了一套计算树逻辑模型检测的分子生物计算方法。一方面研究人工实验微操作与逻辑结构相结合的CTL模型检测的非自治方法；另一方面研究纳米尺度下分子自组装的自治方法；同时，探索了细胞内CTL模型检测的计算方法。. 取得的重要成果包括基于Adleman模型的CTL模型检测的非自治DNA计算方法、基于粘贴自动机的CTL模型检测的分子自组装方法和CTL模型检测的细胞内计算方法。同时将分子自组装的模型检测方法扩展到线性时序逻辑、投影时序逻辑和区间时序逻辑。. 本项目为CTL模型检测开拓了一条全新的研究途径，提出DNA计算机上使用的分子时序逻辑，并在DNA计算机上完成时态逻辑计算，为在DNA计算机上解决CTL模型检测问题提供基本理论并奠定基础。扩充并丰富DNA计算已解决的问题库，推动DNA计算理论的发展，为基于生物分子如RNA、蛋白质计算等的CTL模型检测提供了研究基础。同时，也扩展CTL模型检测的潜在应用领域，为基因疾病的早期诊断和治疗提供了精确的、智能化的手段。