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

摘要

针对扩展命题区间时序逻辑由于缺少验证算法因而不能用于模型检测问题,提出该逻辑的可满足性判定算法.首先,正则形子算法把带星算子或不带星算子的扩展命题区间时序逻辑公式翻译为其正则形公式；然后,正则图子算法根据正则形公式构造公式的正则图模型；最后,判定子算法在正则图上判定公式的可满足性.如果在正则图上直接加上接受条件,即可得到公式的自动机模型.新算法的提出为带有星算子的扩展命题区间时序逻辑的模型检测解决了核心方法问题.仿真结果表明,与相关方法相比,基于扩展命题区间时序逻辑的新方法在描述与验证循环结构性质方面具有比较优势.%Compared with prepositional interval temporal logic (PITL), extended prepositional interval temporal logic (EPITL) is equipped with infinite 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.