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

• 作者: 周清雷 朱维军 李永亮
• 来源期刊: 电子学报
• 学科: 工学
• 关键词: 模型检测 脱氧核糖核酸 线性时序逻辑 粘贴自动机
• 年，卷（期）: 2016,（6）
• 所属期刊栏目: 学术论文
• 页码范围: 1265-1271
• 页数: 7页
• 分类号: TP301|TP384
• 字数: 5084字
• 语种: 中文
• 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逻辑时序算子的检测。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	周清雷	郑州大学信息工程学院	109	475	10.0	16.0
2	李永亮	郑州大学信息工程学院	5	23	3.0	4.0
3	朱维军	郑州大学信息工程学院	46	121	6.0	9.0