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

doi:10.3969/j.issn.0372-2112.2016.06.001

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

• 学术论文 • 下一篇

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

朱维军, 周清雷, 李永亮

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

收稿日期:2014-11-15 修回日期:2015-01-27 出版日期: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

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

摘要/Abstract

摘要：

线性时序逻辑模型检测被广泛应用于处理器设计与验证、网络协议验证、安全协议验证等领域.然而到目前为止,该技术只能在电子计算的平台上实现.为了以脱氧核糖核酸(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

中图分类号:

TP301
TP384

朱维军, 周清雷, 李永亮. 以DNA为载体的线性时序逻辑模型检测[J]. 电子学报, 2016, 44(6): 1265-1271.

ZHU Wei-jun, ZHOU Qing-lei, LI Yong-liang. Conduct Linear Temporal Logic Model Checking via DNA Molecules[J]. Acta Electronica Sinica, 2016, 44(6): 1265-1271.

参考文献

[1] CLARKE E.Model Checking[M].Massachusetts:MIT Press,1999.
[2] BAMAT J,BAUCH P,BRIM L,et al.Designing fast LTL model checking algorithms for many-core GPUs[J].Journal of Parallel and Distributed Computing,2012,72(9):1083-1097.
[3] CARBONE R.LTL model-checking for security protocols[J].AI Communications,2011,24(3):281-283.
[4] GOTZHEIN R.Temporal logic and applications-a tutorial[J].Computer Networks and ISDN Systems,1992,24(3):203-218.
[5] BENARI M,PNUELI A,MANNA Z.The temporal logic of branching time[J].Acta Informatica,1983,20(3):207-226.
[6] ADLEMAN L.Molecular computation of solutions to combinatorial problems[J].Science,1994,266(5187):1021-1023.
[7] ADLEMAN L.On constructing a molecular computer[J].Discrete Mathematics and Theoretical Computer Science,1995,27:1-21.
[8] ZIMMERMANN K,IGNATOVA Z,PEREZ M.DNA Computing Models[M].Berlin:Springer,2008.
[9] YIN Z X,ZHANG F Y,XU J.A Chinese postman problem based on DNA computing[J].Journal of Chemical Information and Computer Sciences,2002,2(42):222-224.
[10] YIN Z X,ZHANG F Y,XU J.The general form of 0-1 programming problem based on DNA computing[J].Biosystems,2003,70(1):73-79.
[11] PAN L Q,XU J,LIU Y C.A surface-based DNA algorithm for the maximal clique problem[J].Chinese Journal of Electronics,2002,11(4):469-471.
[12] PAN L Q,XU J.A surface-based DNA algorithm for the minimal vertex cover problem[J].Progress in Natural Science,2003,13(1):81-84.
[13] 高琳,许进.图的顶点着色问题的DNA算法[J].电子学报,2003,31(4):494-497. GAO Lin,XU Jin.A DNA algorithm for graph vertex coloring problem[J].Acta Electronica Sinica,2003,31(4):494-497.(in Chinese)
[14] XU J,QIANG X L,ZHANG K,et al.A parallel type of DNA computing model for graph vertex coloring problem[A].2010 IEEE Fifth International Conference on Bio-inspired Computing:Theories and Applications[C].Changsha:IEEE Press,2010.231-235.
[15] YANG J,DONG C,DONG Y,et al.Logic Nanoparticle beacon triggered by the binding induced effect of multiple inputs[J].ACS Applied Material Interfaces,2014,6(16):14486-14492.
[16] ZHANG C,WU L,YANG J,et al.A molecular logical switch beacon controlled by thiolated DNA signals[J].Chemical Communications,2013,49:11308-11310.
[17] ZHANG C,MA J,YANG J.Nanoparticle aggregation logic computing controlled by DNA branch migration[J].Applied Physics Letters,2013,103(9):093-106.
[18] EMERSON E A,HAGER K D,KONIECZKA J H.Molecular model checking[J].International Journal of Foundations of Computer Science,2006,17(04):733-741.

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

Conduct Linear Temporal Logic Model Checking via DNA Molecules

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

[1]	王舜, 杜晔, 韩臻. 基于模块化Abstract-Refine算法框架的软件模型检测方法[J]. 电子学报, 2020, 48(5): 997-1002.
[2]	范艳焕, 李永明. 模糊线性时序逻辑的可实现性[J]. 电子学报, 2018, 46(2): 341-346.
[3]	范艳焕, 李永明, 潘海玉. 不确定型模糊Kripke结构的计算树逻辑模型检测[J]. 电子学报, 2018, 46(1): 152-159.
[4]	梁常建, 李永明. 具有模糊时态的广义可能性线性时序逻辑的模型检测[J]. 电子学报, 2017, 45(12): 2971-2977.
[5]	梁常建, 李永明. 广义可能性计算树逻辑的模型检测问题[J]. 电子学报, 2017, 45(11): 2641-2648.
[6]	林运国, 雷红轩, 李永明. 量子马尔可夫链安全性模型检测[J]. 电子学报, 2014, 42(11): 2191-2197.
[7]	刘志锋, 孙博, 周从华. 概率实时时态认知逻辑模型检测中抽象技术的研究[J]. 电子学报, 2013, 41(7): 1343-1351.
[8]	周从华, 孙博, 刘志锋, 葛云. 概率时态认知逻辑模型检测中三值抽象技术的研究[J]. 电子学报, 2012, 40(10): 2052-2061.
[9]	王曦;徐中伟. 基于启发式SCCs的广义Büchi 自动机判空检测算法[J]. 电子学报, 2012, 40(1): 95-102.
[10]	张广泉;戎玫;朱雪阳;何亚丽;石慧娟. 基于XYZ/ADL的Web服务组合描述与验证[J]. 电子学报, 2011, 39(3A): 86-93.
[11]	尹传龙;庄雷;王从银;. 实时模型检测中基于驻留环的精确加速[J]. 电子学报, 2011, 39(3): 489-493.
[12]	张广泉;戎玫;王 Sheng. 时间感知Web服务交互行为建模与失配检测方法研究[J]. 电子学报, 2011, 39(11): 2568-2575.
[13]	冯毅;易江芳;刘丹;佟冬;程旭. 面向SoC系统芯片中跨时钟域设计的模型检验方法[J]. 电子学报, 2008, 36(5): 886-892.
[14]	王雷;李吉;李博洋. 缓冲区溢出漏洞精确检测方法研究[J]. 电子学报, 2008, 36(11): 2200-2204.
[15]	林惠民, 张文辉. 模型检测:理论、方法与应用[J]. 电子学报, 2002, 30(S1): 1907-1912.