10.3969/j.issn.1002-137X.2010.11.053
时间区间时序逻辑的判定性与表达能力
模型检测技术在实时系统验证中被广泛使用.离散时间区间时序逻辑满足性是可判定的,因而也是可模型检测的.连续时间域时间区间时序逻辑是否可模型检测,则并不清楚.约束时间域到非负实数,证明了其可满足性是不可判定的,但存在该逻辑的可判定子集,并发现了这样的子集.由于模型检测问题可归约为时序逻辑满足性判定问题,因此结果表明,时间区间时序逻辑不可模型检测,但其可判定子集可模型检测.
时间区间时序逻辑、可满足性判定、表达能力、模型检测
37
TP301(计算技术、计算机技术)
国家863高技术研究发展计划2007AA010408;河南省重大科技攻关计划092101210104
2011-01-28(万方平台首次上网日期,不代表论文的发表时间)
共3页
227-229