%0 Journal Article
%T 时间区间时序逻辑的判定性与表达能力
%A 朱维军
%A 周清雷？
%J 计算机科学
%D 2010
%X 模型检测技术在实时系统验证中被广泛使用。离散时间区间时序逻辑满足性是可判定的，因而也是可模型检测的。连续时间域时间区间时序逻辑是否可模型检测，则并不清楚。约束时间域到非负实数，证明了其可满足性是不可判定的，但存在该逻辑的可判定子集，并发现了这样的子集。由于模型检测问题可归约为时序逻辑满足性判定问题，因此结果表明，时间区间时序逻辑不可模型检测，但其可判定子集可模型检测。
%K 时间区间时序逻辑
%K 可满足性判定
%K 表达能力
%K 模型检测
%U http://www.jsjkx.com/jsjkx/ch/reader/view_abstract.aspx?file_no=101153&flag=1