离散时间区间时序逻辑模型检查[EB/OL]
北京:中国科技论文在线
) 摘要: 目前还没有模型检查的方法自动检测时间自动机模型是否满足时间区间时序逻辑描述的性质
证明了离散时间区间时序逻辑的可满足性是可判定的
通过从离散时间区间时序逻辑到离散时间自动机的构造
该方法可以推广到其它的时序逻辑模型检查
2、 西安电子科技大学计算理论与技术研究所
关键词: 离散时间区间时序逻辑
( 1、 西安电子科技大学计算理论与技术研究所;西安电子科技大学计算机学院;郑州大学信息工程学院
【详情见下载】离散时间区间时序逻辑模型检查[EB/OL]
) 摘要: 目前还没有模型检查的方法自动检测时间自动机模型是否满足时间区间时序逻辑描述的性质
证明了离散时间区间时序逻辑的可满足性是可判定的
通过从离散时间区间时序逻辑到离散时间自动机的构造
2、 西安电子科技大学计算理论与技术研究所
( 1、 西安电子科技大学计算理论与技术研究所;西安电子科技大学计算机学院;郑州大学信息工程学院
【详情见下载】