CAJ | 학술논문

针对扩展命题区间时序逻辑由于缺少验证算法因而不能用于模型检测问题,提出该逻辑的可满足性判定算法.首先,正则形子算法把带星算子或不带星算子的扩展命题区间时序逻辑公式翻译为其正则形公式；然后,正则图子算法根据正则形公式构造公式的正则图模型；最后,判定子算法在正则图上判定公式的可满足性.如果在正则图上直接加上接受条件,即可得到公式的自动机模型.新算法的提出为带有星算子的扩展命题区间时序逻辑的模型检测解决了核心方法问题.仿真结果表明,与相关方法相比,基于扩展命题区间时序逻辑的新方法在描述与验证循环结构性质方面具有比较优势.
침대확전명제구간시서라집유우결소험증산법인이불능용우모형검측문제,제출해라집적가만족성판정산법.수선,정칙형자산법파대성산자혹불대성산자적확전명제구간시서라집공식번역위기정칙형공식；연후,정칙도자산법근거정칙형공식구조공식적정칙도모형；최후,판정자산법재정칙도상판정공식적가만족성.여과재정칙도상직접가상접수조건,즉가득도공식적자동궤모형.신산법적제출위대유성산자적확전명제구간시서라집적모형검측해결료핵심방법문제.방진결과표명,여상관방법상비,기우확전명제구간시서라집적신방법재묘술여험증순배결구성질방면구유비교우세.