多速率混合系统的模型检查

• 作者: 张海宾 段振华
• 来源期刊: 西安电子科技大学学报（自然科学版）
• 学科: 工学
• 关键词: 模型检查 混合系统 多速率自动机 区间时序逻辑
• 年，卷（期）: 2008,（1）
• 页码范围: 60-64,86
• 页数: 6页
• 分类号: TP301
• 字数: 6457字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-2400.2008.01.011

摘要

研究了初始化的多速率混合系统的模型检查问题,即检验初始化的多速率自动机是否满足某个混合区间时序逻辑公式描述的性质.首先定义了一套转换规则把混合区间时序逻辑公式转化为区间时序逻辑公式.接着定义了初始化的多速率自动机状态空间上的等价关系及其对应的域自动机,并且通过构造域自动机对应的标注有限状态自动机,把初始化的多速率混合系统的模型检查问题等价地转换成了可解的区间时序逻辑的模型检查问题.利用区间时序逻辑的模型检查算法加上上述的转换规则,就可以解决初始化的多速率混合系统的模型检查问题.

作者信息

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