摘要：线性时序逻辑模型检测被广泛应用于处理器设计与验证、网络协议验证、安全协议验证等领域.然而到目前为止,该技术只能在电子计算的平台上实现.为了以脱氧核糖核酸（Deoxyribo Nucleic Acid,DNA）为载体对线性时序逻辑（Linear Temporal Logic,LTL）实施模型检测,给出了使用粘贴自动机实现Until算子模型检测的方法.首先,使用粘贴自动机对Until公式的有穷状态自动机（Finite State Automata,FSA）模型进行编码;然后,将系统模型转换为粘贴自动机的输入字符串;最后,用粘贴自动机验证系统是否满足公式.仿真实验结果证实,新方法可实现对LTL逻辑时序算子的检测.

关键词：模型检测 脱氧核糖核酸 线性时序逻辑 粘贴自动机 

单位：郑州大学信息工程学院; 河南郑州450001