基于时间区间时序逻辑的实时系统统一模型检测

• 作者: 乔芃喆 周清雷 张海宾 朱维军
• 来源期刊: 电子科技大学学报
• 学科: 工学
• 关键词: 统一模型检测 实时系统 可满足性判定 时间区间时序逻辑
• 年，卷（期）: 2014,（5）
• 所属期刊栏目: 计算机工程与应用
• 页码范围: 712-716
• 页数: 5页
• 分类号: TP301
• 字数: 4556字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-0548.2014.05.014

摘要

在同一个逻辑框架内无法自动验证实时区间模型的实时区间性质。为此，该文使用一个离散时间区间时序逻辑公式建立实时系统模型，使用另一个离散时间区间时序逻辑公式描述实时系统需要满足的性质，在此基础上，离散时间区间时序逻辑统一模型检测问题即可归约为目前已解决的离散时间区间时序逻辑可满足性判定问题。该文证明了新方法的有效性以及正确性，为区间实时逻辑这一类的模型检测问题提供了方法。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	周清雷	郑州大学信息工程学院	109	475	10.0	16.0
2	张海宾	西安电子科技大学计算机学院	13	35	4.0	5.0
3	朱维军	郑州大学信息工程学院	46	121	6.0	9.0
7	乔芃喆	河南牧业经济学院信息工程系	9	10	2.0	3.0