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

On the Decidability and Expressive Power of Timed Interval Temporal Logic

作　　者：朱维军[1,2] 周清雷[2] 

机构地区：[1]西安电子科技大学计算机学院,西安710071 [2]郑州大学信息工程学院,郑州450052

出　　处：《计算机科学》2010年第11期227-229,共3页Computer Science

基　　金：国家(863)高技术研究发展计划(No2007AA010408);河南省重大科技攻关计划(No.092101210104)资助

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

关 键 词：时间区间时序逻辑 可满足性判定 表达能力 模型检测 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]