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.