模型检测由图灵奖得主Clarke教授等人提出,是一种能够自动验证系统是否满足指定性质的技术,并且在系统不满足性质时提供反例,被广泛地应用于硬件验证、网络协议验证、安全协议验证、软件验证等领域,取得了令人瞩目的成果。另一方面,作为一种新的计算载体,DNA具有很高的信息存储密度和强大的并行处理能力,DNA计算为突破经典模型检测算法的效率限制提供了新的思路。2006年,著名的计算机科学家、图灵奖得主Ernest Allen Emerson首次把分子生物计算应用到模型检测领域,提出了一种用DNA分子对计算树逻辑(Computation Tree Logic,CTL)公式进行检测的方法。但是,Emerson教授只给出了一种CTL公式EFp的DNA检测算法,目前尚无其它基于DNA计算的CTL逻辑公式的检测算法,更没有DNA计算方法可以对全部的CTL逻辑公式进行检测。这是本文研究和要解决的问题。Emerson教授的方法存在一些不足之处:一,CTL公式EFp的DNA检测算法使用了DNA限制性内切酶和DNA连接酶,酶切反应和连接反应在同一生化环境中进行,对生化反应的环境要求苛刻,可靠性较低;二,当系统模型不满足公式EFp时,算法不能提供反例;三,只给出了一种CTL公式的检测方法,能够检测的公式类型单一。针对上述三个问题,首先,用带标签的有限状态自动机对系统建立模型;其次,探索合适的编码方式,用DNA分子编码系统模型;再次,经过研究和分析,把对系统模型的验证问题规约为对长度在阈值范围之内的运行的验证问题;然后,通过调用DNA分子的7种基本操作,给出了生成长度在阈值范围之内的运行的算法;最后,给出了4种CTL公式的DNA检测算法。对于公式EFp,新算法的反应试管中只含有一种核酸酶—DNA连接酶,对反应环境要求较低,可靠性较高;并且,当系统模型不满足公式时,新方法能给出反例;此外,新方法给出了另外三种公式的检测算法,能够检测的公式类型更多。新方法有效地弥补了Emerson方法中的不足。