扩展命题区间时序逻辑公式可满足性判定算法

• 作者: 周清雷 张海宾 朱维军 邓淼磊
• 来源期刊: 电子科技大学学报
• 学科: 工学
• 关键词: 扩展命题区间时序逻辑 模型检测 正则图 可满足性判定
• 年，卷（期）: 2011,（5）
• 所属期刊栏目: 计算机工程与应用
• 页码范围: 753-758
• 分类号: TP301
• 字数: 5141字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-0548.2011.05.023

摘要

针对扩展命题区间时序逻辑由于缺少验证算法因而不能用于模型检测问题,提出该逻辑的可满足性判定算法.首先,正则形子算法把带星算子或不带星算子的扩展命题区间时序逻辑公式翻译为其正则形公式；然后,正则图子算法根据正则形公式构造公式的正则图模型；最后,判定子算法在正则图上判定公式的可满足性.如果在正则图上直接加上接受条件,即可得到公式的自动机模型.新算法的提出为带有星算子的扩展命题区间时序逻辑的模型检测解决了核心方法问题.仿真结果表明,与相关方法相比,基于扩展命题区间时序逻辑的新方法在描述与验证循环结构性质方面具有比较优势.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	周清雷	郑州大学信息工程学院	109	475	10.0	16.0
2	张海宾	西安电子科技大学计算机学院	13	35	4.0	5.0
3	朱维军	郑州大学信息工程学院	46	121	6.0	9.0
7	邓淼磊	河南工业大学信息科学与工程学院	29	64	4.0	7.0