时间区间时序逻辑的判定性与表达能力

模型检测技术在实时系统验证中被广泛使用。离散时间区间时序逻辑满足性是可判定的，因而也是可模型检测的。连续时间域时间区间时序逻辑是否可模型检测，则并不清楚。约束时间域到非负实数，证明了其可满足性是不可判定的，但存在该逻辑的可判定子集，并发现了这样的子集。由于模型检测问题可归约为时序逻辑满足性判定问题，因此结果表明，时间区间时序逻辑不可模型检测，但其可判定子集可模型检测。