线性时序逻辑公式Xp模型检测的DNA计算方法  

DNA Computing Methods of LTL Model Checking on Xp

作　　者：韩英杰[1] 朱维军[1] 焦林枫 刘洋[1] 周清雷[1] 

机构地区：[1]郑州大学信息工程学院,郑州450001

出　　处：《小型微型计算机系统》2017年第3期553-558,共6页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(61572444)资助;河南省科技厅基础与前沿技术研究项目(152300410055)资助

摘　　要：突破传统计算框架的DNA计算为模型检测提供了新思路.目前已经实现了LTL公式 Uq的DNA模型检测算法,并在其基础上实现了Gp、Fp模型检测的DNA算法.但是Xp无法用含有U算符的公式来表示,目前也没有关于Xp的DNA模型检测算法.提出Xp的基于DNA计算的模型检测算法,仿真实验结果表明其可行性和正确性,DNA计算框架下的LTL模型检测算法得到了扩充和完善,DNA计算已解决的问题库也进一步丰富了.DNA computing based model checking provides a new way of breaking through the traditional computing framework. Checking methods based on DNA computing of LTL formula pUq have been realized, and based on which G-p and Ap are also done. But Xp can＇t be represented by formula containing U and there is no checking method of Xp. A checking method of Xp via a sticker au- tomaton is proposed, and simulations show its feasibility and validity. LTL model checking algorithms based on DNA computing are extended and the problems that can be dealt with DNA computing are enriched.

关 键 词：模型检测 线性时序逻辑 DNA计算 粘贴自动机 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]