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.