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

华东交通大学软件学院

作者简介:

通讯作者:

中图分类号:

基金项目:

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


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

Fund Project:

National Natural Science Foundation of China (61562026, 61962020); Academic and Technical Leaders of Major Disciplines in Jiangxi Province (20172BCB22015); Special Fund Project for Postgraduate Innovation in Jiangxi Province (YC2020-B1141).

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

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

    Abstract:

    . Temporal logic studies 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, many variants of temporal logic 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(Linear Temporal Logic), CTL(Computation Tree Logic) and CTL*,the continuous time model ITL(Interval Temporal Logic) and PTL(Projection Temporal Logic), the expressive power and the differences between them are elaborated in detail; Then, we summarize various temporal logic proposed to describe complex behaviors in random, real-time, hybrid and open systems, points out their characteristics and application scope; Finally, the future research direction of temporal logic is discussed.

    参考文献
    相似文献
    引证文献
引用本文
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2022-04-15
  • 最后修改日期:2022-05-25
  • 录用日期:2022-06-18
  • 在线发布日期: 2023-06-21
  • 出版日期: