区间时序逻辑的模型检查

• 作者: 张海宾 段振华
• 来源期刊: 西安电子科技大学学报(自然科学版)
• 学科: 工学
• 关键词: 模型检查 时序逻辑 自动机
• 年，卷（期）: 2009,（2）
• 页码范围: 338-342
• 页数: 5页
• 分类号: TP301
• 字数: 4061字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-2400.2009.02.028

摘要

为了检验标注有限状态自动机描述的系统是否满足某个区间时序逻辑公式刻画的性质,定义了一套转换规则.利用这些规则,可以构造一个chop-自动机,该自动机接受的语言恰是所有满足这个区间时序逻辑公式的模型的集合.同时,定义了一套转换规则把一个chop-自动机转换为一个标注有限状态自动机,使得它们接受相同的原子命题序列集.这样,区间时序逻辑的模型检查问题就等价地转换成了很容易解决的两个标注有限状态自动机的语言包含问题.

作者信息

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