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

Clc Number:

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).

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

    Reference
    Related
    Cited by
Get Citation
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:April 15,2022
  • Revised:May 25,2022
  • Adopted:June 18,2022
  • Online: June 21,2023
  • Published:
Article QR Code