离散时间区间时序逻辑可满足性的判定  

On the Decidability of Satisfiability of Discrete TITL Formulae

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

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

出　　处：《电子学报》2010年第5期1039-1045,共7页Acta Electronica Sinica

基　　金：国家863高技术研究发展计划(No.2007AA010408);河南省重大科技攻关计划(No.092101220104);陕西省科技攻关计划(No.2009K01-36)

摘　　要：目前还没有模型检查的方法自动检测模型是否满足时间区间时序逻辑描述的性质.我们约束时间域到离散时间,证明了离散时间区间时序逻辑的可满足性是可判定的,因而是可模型检查的.提出了时间正则图模型,通过从离散时间区间时序逻辑到时间正则图的构造,提出了基于该逻辑的判定算法,该算法可以推广到其它的时序逻辑模型检查,并优于现有的基于自动机的时序逻辑判定方法.There is no method available for checking whether a model satisfies a property described by a timed interval temporal logic （TITL） formula. In this paper, we formalize a novel model named timed normal form graph （ TNFG ）. In addition, we give a procedure to construct TNFG from discrete TITL formula, and prove that the satisfiability of discrete TITL is decidable. The new method can be also used for other types of temporal logic and it is superior to the existing approaches.

关 键 词：模型检查 离散时间区间时序逻辑 时间正则图 可满足性判定 

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