摘要
模型检测技术在实时系统验证中被广泛使用。离散时间区间时序逻辑满足性是可判定的,因而也是可模型检测的。连续时间域时间区间时序逻辑是否可模型检测,则并不清楚。约束时间域到非负实数,证明了其可满足性是不可判定的,但存在该逻辑的可判定子集,并发现了这样的子集。由于模型检测问题可归约为时序逻辑满足性判定问题,因此结果表明,时间区间时序逻辑不可模型检测,但其可判定子集可模型检测。
Model checking is used widely in verification of real-time system.Satisfiability of discrete Timed Interval Temporal Logic is decidable,so is model checking of it.But in dense-time domain,the problem of model checking Timed Interval Temporal Logic is not clear.We prove that Satisfiability of Timed Interval Temporal Logic is un-decidable and we find a subset of Timed Interval Temporal Logic which can be decidable.So,it can be decidable to model checking the subset.
出处
《计算机科学》
CSCD
北大核心
2010年第11期227-229,共3页
Computer Science
基金
国家(863)高技术研究发展计划(No2007AA010408)
河南省重大科技攻关计划(No.092101210104)资助
关键词
时间区间时序逻辑
可满足性判定
表达能力
模型检测
Timed interval temporal logic
Checking the satisfiability
Expressive power
Model checking
