有穷时间投影时序逻辑的完备公理系统
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

国家自然科学基金(60433010, 60910004, 60873018, 91018010, 61003078, 61003079); 国家重点基础研究发展计划(973)(2010CB328102); 中央高校基本科研业务费专项资金(JY10000903004)


Complete Axiomatization for Projection Temporal Logic with Finite Time
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    为采用定理证明的方法对并发及交互式系统进行验证,研究了有穷论域下有穷时间一阶投影时序逻辑(projection temporal logic,简称PTL)的一个完备公理系统.在介绍PTL 的语法、语义并给出公理系统后,提出了PTL公式的正则形(normal form,简称NF)和正则图(normal form graph,简称NFG).基于NF 给出了NFG 的构造算法,并利用NFG可描述公式模型的性质证明PTL 公式的可满足性判定定理和公理系统的完备性.最后,结合实例展示了PTL及其公理系统在系统验证中的应用.结果表明,基于PTL 的定理证明方法可方便用于并发系统的建模与验证.

    Abstract:

    To verify the properties of concurrent and reactive systems based on the theorem proving approach, a complete axiomatization is formulized over finite domains for first order projection temporal logic (PTL) with finite time. First, the syntax, semantics and the axiomatization of PTL are presented; next, a normal form (NF) and a normal form graph (NFG) of PTL formulas are defined respectively; further, the algorithm for constructing the NFG is formalized upon the NF; moreover, the decision theorem for PTL formulas and the completeness of the axiomatic system have been proven to be based on the property that the NFG can-describe the models of PTL formulas; finally, an example is given to illustrate how to do system verification based on PTL and its axiomatic system, and the results indicate that the PTL based theorem proving approach can be conveniently applied to modeling and verification of concurrent systems.

    参考文献
    相似文献
    引证文献
引用本文

舒新峰,段振华.有穷时间投影时序逻辑的完备公理系统.软件学报,2011,22(3):366-380

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2010-04-06
  • 最后修改日期:2010-06-09
  • 录用日期:
  • 在线发布日期:
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号