时序逻辑及其表达能力综述
作者:
作者单位:

作者简介:

杨科(1993—),男,博士研究生,研究方向为形式化方法,安全协议的形式化分析。E-mail:landexplorer@163.com

通讯作者:

中图分类号:

TP3-05

基金项目:

国家自然科学基金项目(61562026, 61962020);江西省主要学科学术和技术带头人计划项目(20172BCB22015);江西省教育厅科学技术研究项目(GJJ190326);江西省 2020 年度研究生创新专项资金项目(YC2020-B1141)


Review of Temporal Logic and Its Expressive Power
Author:
Affiliation:

Fund Project:

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

    时序逻辑是研究状态随时间变化系统的逻辑特性,在软硬件验证中有着广泛应用,是模型检测的基础。 基于对时间模型的不同描述以及为了处理更加复杂的计算特征,衍生出各种时序逻辑,具有不同的表达能力,正确理解其表达能力对于系统模型的形式化规约尤为重要。 首先,介绍基于离散时间模型的线性时序逻辑 LTL、计算树逻辑 CTL 和 CTL*,以及基于连续时间模型的区间时序逻辑 ITL 和投影时序逻辑 PTL,对它们的表达能力及区别进行了详细阐述;然后,概述为了描述随机、实时、混成、开放系统中的复杂行为而提出的不同时序逻辑,指出它们的特点及适用范围;最后,对时序逻辑的未来研究方向进行展望。

    Abstract:

    Temporal logic involves the logic characteristics of the system whose state changes with time. It is widely used in software and hardware verification and is the basis of model checking. Based on the different descriptions of time models and in order to deal with more complex computational characteristics, different kinds of temporal logics are derived, which have different expressive power. It is particularly important for the formal specification of system models to correctly understand their expressive power. Firstly, this paper introduces the discrete-time model LTL, CTL and CTL*, the continuous time model ITL and PTL, and the expressive power and the differences between them are elaborated in details. Then, various temporal logic proposed to describe random, real-time, hybrid and open-system complex behaviors are summarized, and their characteristics and application scopes are presented. Finally, the future research direction of temporal logic is discussed.

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

杨科,肖美华,钟小妹,占东明.时序逻辑及其表达能力综述[J].华东交通大学学报,2023,40(2):57-70.

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2022-04-24
  • 最后修改日期:
  • 录用日期:
  • 在线发布日期: 2023-05-06
  • 出版日期: