%0 Journal Article
%T 离散时间区间时序逻辑可满足性的判定
%A 朱维军
%A 张海宾
%A 周清雷
%J 电子学报
%P 1039-1045
%D 2010
%X 目前还没有模型检查的方法自动检测模型是否满足时间区间时序逻辑描述的性质.我们约束时间域到离散时间,证明了离散时间区间时序逻辑的可满足性是可判定的,因而是可模型检查的.提出了时间正则图模型,通过从离散时间区间时序逻辑到时间正则图的构造,提出了基于该逻辑的判定算法,该算法可以推广到其它的时序逻辑模型检查,并优于现有的基于自动机的时序逻辑判定方法.
%K 模型检查
%K 离散时间区间时序逻辑
%K 时间正则图
%K 可满足性判定
%U http://www.ejournal.org.cn/CN/abstract/abstract335.shtml