朱维军,周清雷,李永亮

(郑州大学信息工程学院,河南郑州 450001)



以DNA为载体的线性时序逻辑模型检测

朱维军,周清雷,李永亮

(郑州大学信息工程学院,河南郑州 450001)

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

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

1　引言

模型检测由图灵奖得主Clarke教授等人提出[1].它是一种能够自动验证系统是否满足给定性质的形式化核心方法与技术,被广泛地应用于硬件验证[2]、网络协议验证、安全协议验证[3]等领域.在时序逻辑模型检测中,线性时序逻辑[4](Linear Temporal Logic,LTL)、计算树逻辑[5](Computation Tree Logic,CTL)分别被用来描述系统需满足的线性时序性质和分支时序性质,有穷状态自动机(Finite State Automata,FSA)则被用来为系统建模,模型检测算法自动检测模型是否满足需求性质.

脱氧核糖核酸(Deoxyribo Nucleic Acid,DNA)计算以DNA分子为载体,以生物酶和生物操作作为信息处理工具,是一种与电子计算不同的计算模型.1994年,图灵奖得主Adleman教授发表在《Science》上的一篇文章……