支持索引式的PPTL定理证明器的实现
作者:
作者单位:

作者简介:

王小兵(1979-),男,博士,副教授,博士生导师,CCF高级会员,主要研究领域为形式化方法,形式化验证,时序逻辑;李春奕(1996-),女,博士,CCF学生会员,主要研究领域为形式化方法,形式化验证,时序逻辑;寇蒙莎(1998-),女,硕士,CCF学生会员,主要研究领域为形式化方法,形式化验证,定理证明;赵亮(1984-),男,博士,副教授,CCF专业会员,主要研究领域为形式化方法,形式化验证,时序逻辑

通讯作者:

赵亮,E-mail:lzhao@xidian.edu.cn

中图分类号:

TP311

基金项目:

国家自然科学基金(61672403,61972301);陕西省重点研发计划(2020GY-043,2020GY-210)


Implementation of Theorem Prover for PPTL with Indexed Expressions
Author:
Affiliation:

Fund Project:

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

    定理证明是目前主流的形式化验证方法,拥有强大的抽象和逻辑表达能力,且不存在状态空间爆炸问题,可用于有穷和无穷状态系统,但其不能完全自动化,并且要求用户掌握较强的数学知识.含索引式的命题投影时序逻辑(PPTL)是一种具有完全正则表达能力,并且包含LTL的时序逻辑,具有较强的建模和性质描述能力.目前,一个可靠完备的含索引式的PPTL公理系统已被构建,然而基于该公理系统的定理证明尚未得到良好工具的支持,存在证明自动化程度较低以及证明冗长易错的问题.鉴于此,首先设计了支持索引式的PPTL定理证明器的实现框架,包括公理系统的形式化与交互式定理证明;然后,在Coq中形式化定义了含索引式的PPTL公式、公理与推理规则,完成了框架中公理系统的实现;最后,通过两个实例的交互式证明验证了该定理证明器的可用性.

    Abstract:

    Theorem proving is a mainstream formal verification method, with a strong ability of abstraction and logical expression. It does not suffer from state space explosion and can be used to verify finite and infinite systems. Nevertheless, it cannot be fully automated and requires users to have deep mathematical knowledge. Propositional projection temporal logic with indexed expressions is a temporal logic with full regular expressiveness and subsumes LTL, having strong modeling and property describing ability. At present, a sound and complete axiom system for PPTL with indexed expressions is presented while the theorem proving based on it is not yet well supported by tools, which leads to the low automaticity, redundancy, and fallibility of theorem proving. Therefore, firstly, the implementation framework of the theorem prover for PPTL with indexed expressions is designed, including two parts, the formalization of the PPTL axiom system and interactive theorem proving. Then the formulas, axioms, and inference rules are formally defined in Coq, implementing the axiom system of the framework. Finally, the availability of the theorem prover is proved by the interactive proving of two proof examples.

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

王小兵,寇蒙莎,李春奕,赵亮.支持索引式的PPTL定理证明器的实现.软件学报,2022,33(6):2172-2188

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

京公网安备 11040202500063号