扩展命题区间时序逻辑公式可满足性判定算法  

Decision Procedure for Extended Propositional Interval Temporal Logic

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

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

出　　处：《电子科技大学学报》2011年第5期753-758,共6页Journal of University of Electronic Science and Technology of China

基　　金：国家863高技术研究发展计划(2007AA010408);国家自然科学基金(61003079);教育部博士点基金(20100203120012);陕西省工业攻关计划(2009K01-36);中央高校基本科研业务费(JY10000903014)

摘　　要：针对扩展命题区间时序逻辑由于缺少验证算法因而不能用于模型检测问题,提出该逻辑的可满足性判定算法。首先,正则形子算法把带星算子或不带星算子的扩展命题区间时序逻辑公式翻译为其正则形公式;然后,正则图子算法根据正则形公式构造公式的正则图模型;最后,判定子算法在正则图上判定公式的可满足性。如果在正则图上直接加上接受条件,即可得到公式的自动机模型。新算法的提出为带有星算子的扩展命题区间时序逻辑的模型检测解决了核心方法问题。仿真结果表明,与相关方法相比,基于扩展命题区间时序逻辑的新方法在描述与验证循环结构性质方面具有比较优势。Compared with propositional interval temporal logic （PITL）, extended propositional interval temporal logic （EPITL） is equipped with inf＇mite models and the chop-star operator additionally. However, there is no algorithm available for model checking EPITL. To this end, we propose an algorithm for EPITL satisfiability checking. The first step is to translate EPITL formulae with or without chop-star operators into their normal forms （NFs）. The second step is to construct normal form graphs （＇NFGs） from the NF formulae. The last step is to check the satisfiability of the EPITL formulae by using the NFGs. Accordingly, we can translate the NFGs into buchi automata. So, the EPITL model checking problem is solved. As shown in the simulation results, our approach is superior to the existing ones based on other logics in terms of specification and verification of some properties of loop structures.

关 键 词：扩展命题区间时序逻辑 模型检测 正则图 可满足性判定 

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