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