离散时间区间时序逻辑模型检查,朱维军,段振华,目前还没有模型检查的方法自动检测时间自动机模型是否满足时间区间时序逻辑描述的性质。我们约束时间域到离散时间,证明了离散时