稠密时间区间时序逻辑的可满足性判定

• 作者: 张海宾 段振华
• 来源期刊: 西安电子科技大学学报（自然科学版）
• 学科: 工学
• 关键词: 实时系统 时序逻辑 模型检查 混合系统
• 年，卷（期）: 2007,（3）
• 页码范围: 463-467
• 页数: 5页
• 分类号: TP301
• 字数: 5890字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-2400.2007.03.026

摘要

定义了稠密时间区间时序逻辑(DTITL),它是区间时序逻辑的一种实时扩充.通过定义DTITL无穷状态空间上的具有有限个数等价类的等价关系,把DTITL的连续状态模型离散化为一阶区间时序逻辑模型.定义了一套规则来构造DTITL公式对应的有界整数域上一阶区间时序逻辑子集SFO的公式,从而把DTITL的可满足性判定问题等价地转化成了SFO的判定问题.利用多个命题变量等价表示有界整数,把SFO的可满足性判定问题等价转换为可判定的命题区间时序逻辑的判定问题.解决了DTITL的可满足性判定问题.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张海宾	西安电子科技大学计算机学院	13	35	4.0	5.0
2	段振华	西安电子科技大学计算机学院	47	363	10.0	16.0