论文部分内容阅读
针对扩展命题区间时序逻辑由于缺少验证算法因而不能用于模型检测问题，提出该逻辑的可满足性判定算法。首先，正则形子算法把带星算子或不带星算子的扩展命题区间时序逻辑公式翻译为其正则形公式；然后，正则图子算法根据正则形公式构造公式的正则图模型；最后，判定子算法在正则图上判定公式的可满足性。如果在正则图上直接加上接受条件，即可得到公式的自动机模型。新算法的提出为带有星算子的扩展命题区间时序逻辑的模型检测解决了核心方法问题。仿真结果表明，与相关方法相比，基于扩展命题区间时序逻辑的新方法在描述与验证循环结构性质方面具有