摘要：目前还没有模型检查的方法自动检测模型是否满足时间区间时序逻辑描述的性质．我们约束时间域到离散时间，证明了离散时间区间时序逻辑的可满足性是可判定的，因而是可模型检查的．提出了时间正则图模型，通过从离散时间区间时序逻辑到时间正则图的构造，提出了基于该逻辑的判定算法，该算法可以推广到其它的时序逻辑模型检查，并优于现有的基于自动机的时序逻辑判定方法．

关键词：模型检查 离散时间区间时序逻辑 时间正则图 可满足性判定 

单位：西安电子科技大学计算机学院; 陕西西安710071; 郑州大学信息工程学院; 河南郑州450052