Volume 40 Issue 5
May  2017
Article Contents
Article Navigation >  Journal of University of Electronic Science and Technology of China  > 2011  >  40(5): 753-758

ZHU Wei-jun, DENG Miao-lei, ZHOU Qing-lei, ZHANG Hai-bin. Decision Procedure for Extended Propositional Interval Temporal Logic[J]. Journal of University of Electronic Science and Technology of China, 2011, 40(5): 753-758. doi: 10.3969/j.issn.1001-0548.2011.05.023
Citation: ZHU Wei-jun, DENG Miao-lei, ZHOU Qing-lei, ZHANG Hai-bin. Decision Procedure for Extended Propositional Interval Temporal Logic[J]. Journal of University of Electronic Science and Technology of China, 2011, 40(5): 753-758. doi: 10.3969/j.issn.1001-0548.2011.05.023
shu

Decision Procedure for Extended Propositional Interval Temporal Logic

doi: 10.3969/j.issn.1001-0548.2011.05.023
  • 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

  • Received Date: 2010-01-18
  • Rev Recd Date: 2010-07-06
  • Publish Date: 2011-10-15
  • 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.
  • 加载中
通讯作者: 陈斌, bchen63@163.com
  • 1. 

    沈阳化工大学材料科学与工程学院 沈阳 110142

  1. 本站搜索
  2. 百度学术搜索
  3. 万方数据库搜索
  4. CNKI搜索
Get Citation
PDF
XML

Article Metrics

Article views(3498) PDF downloads(41) Cited by()

Related
Proportional views

Decision Procedure for Extended Propositional Interval Temporal Logic

doi: 10.3969/j.issn.1001-0548.2011.05.023
  • 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
  • Received Date: 2010-01-18
  • Rev Recd Date: 2010-07-06
  • Publish Date: 2011-10-15

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.

ZHU Wei-jun, DENG Miao-lei, ZHOU Qing-lei, ZHANG Hai-bin. Decision Procedure for Extended Propositional Interval Temporal Logic[J]. Journal of University of Electronic Science and Technology of China, 2011, 40(5): 753-758. doi: 10.3969/j.issn.1001-0548.2011.05.023
Citation: ZHU Wei-jun, DENG Miao-lei, ZHOU Qing-lei, ZHANG Hai-bin. Decision Procedure for Extended Propositional Interval Temporal Logic[J]. Journal of University of Electronic Science and Technology of China, 2011, 40(5): 753-758. doi: 10.3969/j.issn.1001-0548.2011.05.023
shu

    HTML

Catalog

    Journal Online

    Author's Notes

    Links

    Copyright © 《电子科技大学学报》编辑部

    Address: Room 350, central building, University of Electronic Science and Technology, No.4, Section 2, Jianshe North Road, Chengdu Tel: 028-83202308,83207559 Email: xuebao@uestc.edu.cn

    本系统由 北京仁和汇智信息技术有限公司 开发 

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return