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

Clc Number:

TP3-05

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    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.

    Reference
    Related
    Cited by
Get Citation

杨科,肖美华,钟小妹,占东明.时序逻辑及其表达能力综述[J].华东交通大学学报英文版,2023,40(2):57-70.
Yang Ke, Xiao Meihua, Zhong Xiaomei, Zhan Dongming. Review of Temporal Logic and Its Expressive Power[J]. JOURNAL OF EAST CHINA JIAOTONG UNIVERSTTY,2023,40(2):57-70

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:April 24,2022
  • Revised:
  • Adopted:
  • Online: May 06,2023
  • Published:
Article QR Code