Conduct Linear Temporal Logic Model Checking via DNA Molecules

doi:10.3969/j.issn.0372-2112.2016.06.001

您当前的位置：

首页 >

文章列表页 >

Conduct Linear Temporal Logic Model Checking via DNA Molecules

更新时间：2025-07-02

- Conduct Linear Temporal Logic Model Checking via DNA Molecules
- Acta Electronica Sinica Vol. 44, Issue 6, Pages: 1265-1271(2016)
- 作者机构：
  
  郑州大学信息工程学院,河南,郑州,450001
- 作者简介：
- 基金信息：
  
  National Natural Science Foundation of China (No.61250007, No.U1204608, No.U1304606, No.61572444);China Postdoctoral Science Foundation (No.2012M511588, No.2015M572120);Funding Project for Young Backbone Teachers of Universities in Henan Province (No.2014GGJS-001)
- DOI：10.3969/j.issn.0372-2112.2016.06.001
  CLC： TP301TP384
- Published Online：25 June 2016，
  
  Published：2016
- 稿件说明：
移动端阅览
Conduct Linear Temporal Logic Model Checking via DNA Molecules[J]. Acta Electronica Sinica, 2016, 44(6): 1265-1271.
DOI：

Conduct Linear Temporal Logic Model Checking via DNA Molecules[J]. Acta Electronica Sinica, 2016, 44(6): 1265-1271. DOI： 10.3969/j.issn.0372-2112.2016.06.001.

摘要

线性时序逻辑模型检测被广泛应用于处理器设计与验证、网络协议验证、安全协议验证等领域.然而到目前为止

该技术只能在电子计算的平台上实现.为了以脱氧核糖核酸(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.

关键词

Keywords

references

Views

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Research on Interaction Modeling and Mismatch Checking of Time-Aware Web Services

Exact Acceleration of Real-Time Model Checking Based on Parking Cycle

Specification and Verification of Web Service Composition Based on XYZ/ADL

Precisely Detecting Buffer Overflow Vulnerabilities

Model Checking on Clock Domain Crossing Design of System-on-Chip

Related Author

Sheng

WANG Sheng

RONG Mei

ZHANG Guang-quan

WANG Cong-yin

ZHUANG Lei

YIN Chuan-long

ZHU Xue-yang

Related Institution

Shenzhen Tourism CollegeJinan UniversityShenzhenGuangdong 518053China

State Key Laboratory of Computer ScienceChinese Academy of ScienceBeijing 100190China

School of Computer Science and TechnologySoochow UniversitySuzhouJiangsu 215006China

Shenzhen Tourism College,Jinan University

State Key Laboratory of Computer Science,Chinese Academy of Science

⁰