| 扩展命题区间时序逻辑公式可满足性判定算法 |
| |
| 引用本文： | 朱维军,邓淼磊,周清雷,张海宾.扩展命题区间时序逻辑公式可满足性判定算法[J].电子科技大学学报（自然科学版）,2011,40(5):753-758. |
| |
| 作者姓名： | 朱维军 邓淼磊 周清雷 张海宾 |
| |
| 作者单位： | 1.郑州大学信息工程学院 郑州 450001; |
| |
| 基金项目： | 国家863高技术研究发展计划(2007AA010408);国家自然科学基金(61003079);教育部博士点基金(20100203120012);陕西省工业攻关计划(2009K01-36);中央高校基本科研业务费(JY10000903014)。 |
| |
| 摘 要： | 针对扩展命题区间时序逻辑由于缺少验证算法因而不能用于模型检测问题,提出该逻辑的可满足性判定算法.首先,正则形子算法把带星算子或不带星算子的扩展命题区间时序逻辑公式翻译为其正则形公式；然后,正则图子算法根据正则形公式构造公式的正则图模型；最后,判定子算法在正则图上判定公式的可满足性.如果在正则图上直接加上接受条件,即可得...
|
| 关 键 词： | 扩展命题区间时序逻辑 模型检测 正则图 可满足性判定 |
| 收稿时间： | 2010-01-18 |
Decision Procedure for Extended Propositional Interval Temporal Logic |
| |
| Affiliation: | 1.School of Information Engineering,Zhengzhou University Zhengzhou 450001;2.School of Computer Science,Xidian University Xi'an 71007;3.College of Information Science and Technology,Henan University of Technology Zhengzhou 450001 |
| |
| Abstract: | Compared with propositional interval temporal logic (PITL), extended propositional 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. |
| |
| Keywords: | |
|
| 点击此处可从《电子科技大学学报（自然科学版）》浏览原始摘要信息 |
|
点击此处可从《电子科技大学学报（自然科学版）》下载全文 |
|
