电子学报 ›› 2016, Vol. 44 ›› Issue (6): 1265-1271.DOI: 10.3969/j.issn.0372-2112.2016.06.001

• 学术论文 •    下一篇

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

朱维军, 周清雷, 李永亮   

  1. 郑州大学信息工程学院, 河南郑州 450001
  • 收稿日期:2014-11-15 修回日期:2015-01-27 出版日期:2016-06-25 发布日期:2016-06-25
  • 作者简介:朱维军 男,1976年生于河南郑州,现为郑州大学副教授.主要研究方向:DNA计算、形式化方法.E-mail:zhuweijun76@163.com;周清雷 男,1962年生于河南新乡,现为郑州大学教授、博士生导师.主要研究方向:DNA计算、形式化方法.E-mail:ieqlzhou@zzu.edu.cn
  • 基金资助:

    国家自然科学基金(No.61250007,No.U1204608,No.U1304606,No.61572444);中国博士后科学基金(No.2012M511588,No.2015M572120);河南省高等学校青年骨干教师资助计划项目(No.2014GGJS-001)

Conduct Linear Temporal Logic Model Checking via DNA Molecules

ZHU Wei-jun, ZHOU Qing-lei, LI Yong-liang   

  1. School of Information Engineering, Zhengzhou University, Zhengzhou, Henan 450001, China
  • Received:2014-11-15 Revised:2015-01-27 Online:2016-06-25 Published:2016-06-25

摘要:

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

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

Abstract:

The linear temporal logic (LTL) model checking is widely used in processor design and verification, network protocol verification and security protocol verification.Up to now, this technique can only be realized on the platform of electronic computer.In order to conduct LTL model checking under the circumstance of deoxyribo nucleic acid (DNA), we proposed a method to check the Until constructor via a sticker automaton.We encode a finite state automaton (FSA) which is a model of the formula Until, with a DNA sticker automaton.And we convert a model of a system into its paths, as the input strings of the sticker automaton.We verify whether the system satisfies the formula or not, by using the sticker automaton.In this way, the formula Until can be checked with the double strand DNA molecules.The simulation results show that the method can successfully check the basic temporal formulas.

Key words: model checking, deoxyribo nucleic acid, linear temporal logic, sticker automaton

中图分类号: