时序逻辑及其表达能力综述

Review of Temporal Logic and Its Expressive Power

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

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.