离散时间区间时序逻辑可满足性的判定

• 作者: 周清雷 张海宾 朱维军
• 来源期刊: 电子学报
• 学科: 工学
• 关键词: 模型检查 离散时间区间时序逻辑 时间正则图 可满足性判定
• 年，卷（期）: 2010,（5）
• 所属期刊栏目: 学术论文
• 页码范围: 1039-1045
• 分类号: TP301
• 字数: 6544字
• 语种: 中文

摘要

目前还没有模型检查的方法自动检测模型是否满足时间区间时序逻辑描述的性质.我们约束时间域到离散时间,证明了离散时间区间时序逻辑的可满足性是可判定的,因而是可模型检查的.提出了时间正则图模型,通过从离散时间区间时序逻辑到时间正则图的构造,提出了基于该逻辑的判定算法,该算法可以推广到其它的时序逻辑模型检查,并优于现有的基于自动机的时序逻辑判定方法.

作者信息

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