摘要
目前还没有模型检查的方法自动检测模型是否满足时间区间时序逻辑描述的性质.我们约束时间域到离散时间,证明了离散时间区间时序逻辑的可满足性是可判定的,因而是可模型检查的.提出了时间正则图模型,通过从离散时间区间时序逻辑到时间正则图的构造,提出了基于该逻辑的判定算法,该算法可以推广到其它的时序逻辑模型检查,并优于现有的基于自动机的时序逻辑判定方法.
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.
出处
《电子学报》
EI
CAS
CSCD
北大核心
2010年第5期1039-1045,共7页
Acta Electronica Sinica
基金
国家863高技术研究发展计划(No.2007AA010408)
河南省重大科技攻关计划(No.092101220104)
陕西省科技攻关计划(No.2009K01-36)
关键词
模型检查
离散时间区间时序逻辑
时间正则图
可满足性判定
model checking
discrete limed interval temporal logic
timed normal form graph
satisfiability checking