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

杨 科，肖美华，钟小妹，占东明，2

（1.华东交通大学软件学院，江西 南昌 330013；2.华中师范大学教育学院，湖北 武汉 430079）

时序逻辑来源于哲学和语言学，由模态逻辑演变而来，是一种特殊模态逻辑。时序逻辑将时间因素引入到模态逻辑中，将模态算子□(必然)解释为“将来永远”,◇(可能)解释为“将来会”，它是由Prior于1955 年首先提出的，以研究时间和时序的逻辑[1]。在过去几十年里，许多逻辑学家和计算机科学家对其进行研究和扩充，衍生出各种不同的时序逻辑，被广泛应用于数学、计算机科学以及人工智能等领域。

早期的形式化方法（20 世纪70 年代前）致力于研究经典一阶逻辑、Hoare 逻辑在串行程序上的描述与验证，该类方法是以逻辑推理为基础的演绎证明。从20 世纪70 年代中期开始，并发程序设计成为理论计算机科学中的研究热点。不同于串行程序，并发程序涉及到不同任务之间的同步以及信息交换，可能会造成数据竞争、死锁、原子性违反等错误[2]，在串行程序分析方法的基础上扩充并发性的推理规则对于并发程序的分析验证并不适用。由于连续运行的系统必然会涉及到时间概念，然而命题逻辑缺乏描述包含连续系统中与时间相关概念的能力。因此以色列科学家伯努利在1977 年提出将时序逻辑作为并发系统的规格说明工具，基于时序逻辑对并发程序性质进行形式化规约和验证。20 世纪80 年代，随着超大规模集成电路、并发分布式系统等技术的迅猛发展，鉴于演绎验证的局限性，对自动化验证技术提出了更高的要求。美国的Clarke和Emerson，法国的Sifakis 和Queille 在1981 年分别独立提出将时序逻辑与状态空间搜索相结合的方法，诞生了模型检测技术[3]。随着模型检测技术的发展，时序逻辑被广泛应用在系统形式化规约与验证中，尤其是上世纪90 年代符号模型检测技术的出现，利用二叉决策图的方式来表示模型的状态迁移关系，使得可验证的系统状态数多达10200，成功应用于超大规模集成电路和大型软件系统的验证中。时序逻辑作为一种描述与验证计算机系统的形式化规约语言，被广泛应用于各类系统的形式化验证。经过40 多年的发展，时序逻辑已经发展成为包括线性时序逻辑、计算树逻辑和区间时序逻辑等众多分支的一门学科。特别是在计算机科学中，时序逻辑作为形式规约语言，已经成为形式化验证程序和并发系统的重要组成部分。

对于一种时序逻辑来说，一般从可满足性、复杂性、表达性3 个方面展开研究[4]。可满足性就是给定一个性质规约公式φ，是否存在一个结构M，该结构恰好是给定公式φ 的模型，或者判定模型M 是否满足公式φ；复杂性就是研究逻辑公式可满足性的复杂度问题；表达性是研究时序逻辑的表达能力，该逻辑公式能够描述哪一种类型的性质。本文着重研究时序逻辑的表达能力问题，介绍各种时序逻辑和分析它们适合对哪些系统进行性质规约，以及不同时序逻辑在表达能力上的优劣。

1 时序逻辑

时序逻辑主要研究状态随时间变化系统的逻辑特性，由于硬件和软件的运行都是随着时间的变化而不断变化，因此时序逻辑特别适合对该类系统模型进行形式化规约，广泛应用在程序验证和硬件验证领域。在对系统形式化验证时，人们通常关心这两种性质：安全性（safety）和活性（liveness）[5]。它们分别表示“坏的事情永远不会发生”和“好的事情最终会发生”。系统的特性用时序逻辑来表示，比如系统是否会发生死锁、程序代码是否会陷入死循环和系统能否在规定时间内对输入信号做出正确响应等。

下面简要介绍时序逻辑属性、属性的可描述性以及表达能力[6]的形式化定义。

定义1 （属性）在一个无穷状态序列δ：δ0，δ1，δ2，…（δ∈Sω）的集合Sω上定义属性p（property，也称之为性质）。一个属性p⊆Sω是所有满足该属性的无穷状态序列δ 的集合，也就是说一个无穷状态序列δ 满足属性p 等价于该序列δ 属于p 所表示的集合，记作δ｜=p⇔δ∈p。

定义2 （属性p 的可描述性）设φ 是一个时序逻辑公式，如果δ∈p iff δ｜=φ 成立，那么属性p 能够用时序逻辑公式φ 来描述。

定义3 （表达能力）在一类模型M 下，语言L2至少具有和语言L1同等的表达能力，记作L1⊆ML2。有如下公式成立：

∀φ1∈L1，∃φ2∈L2，∀M∈M，M｜=φ1iff M｜=φ2

如果有L1⊆ML2和L2⊆ML1成立，我们称在模型M 上语言L1和L2表达能力相同，记作L1≡ML2。如果有L1⊆ML2成立而L1≡ML2不成立，称在模型M 上语言L2的表达能力比L1更强，记作L1⊂ML2。

2 基于离散时间模型的时序逻辑

本节介绍基于离散时间模型的时序逻辑，它们的语义被解释在孤立离散的点上，主要包括LTL，CTL 和CTL*，并对它们之间的区别进行详细分析比较。

2.1 线性时序逻辑LTL

LTL 由Manna 和Pnueli 提出，是一种非常重要的时序逻辑，可以用来描述并发分布式系统的属性，在模型检测中得到广泛使用。LTL 将时间序列设想成一个线性序列δ：s0，s1，s2，…，这是一种经典的时间模型。状态之间按照时间参数严格排序，在状态序列上解释其真值，并且其真值随时间变化而变化，这也是时序逻辑与经典逻辑的主要区别之处。

LTL 采用的时间结构是线性、离散的，其语义模型是通过Kripke 三元组ML=＜S，R，L＞来定义的，其中S 是状态集合，R⊂S×S 是符合完全性约束的变迁关系（即对于任意的状态s∈S，存在状态s'∈S满足（s，s'）∈R，L∶S→2AP是标记函数，用于标记某个状态上所有满足的原子命题集合。

以选举算法为例，对如何使用LTL 描述领导人选举算法需要满足的性质进行阐述。领导人选举算法是分布系统中一类非常重要的算法，目的是在多个服务器中选出一个特殊的节点作为领导人，可以简化服务器之间的协作，有助于容错和节省资源。我们用elected 表示选举发生，num_leader 表示领导人数量，one_leader 表示成功选举出领导人。

性质1：选举结束后，最终会选出一位领导人：◇（num_leader＞0）。

性质2：选举结束后，至多有一位领导人当选：□¬（num_leader＞1）。

性质3：当某个节点被选为领导人之后，将永远成为领导人：∧i□（electedi→one_leader）。

定理1 LTL 的表达能力与一阶谓词逻辑等价，不能表达ω 正则性质[7]。

该定理表明虽然LTL 与一阶谓词逻辑的表达能力等价，但对于两者的可满足性的复杂度却不相同。对于一阶谓词逻辑来说，它的可满足性问题的解决难度是非初等的，也就是说它的复杂度上界是无限增长的，而对于LTL 来说是PSPACE-完全的[8]，这也是LTL 能够得到广泛应用于程序验证、程序综合以及人工智能等领域的一个重要理论支撑[9]。

在显式模型检测中，通常是将软硬件系统用形式化语言建模成模型M，同时利用LTL 公式将系统的属性表示为φ，其核心是判断系统模型的自动机AM与时序逻辑公式φ取反得到的等价自动机Aφ做交运算后的自动机AP是否为空。可以推断出LTL是可以用自动机来表示的，但研究表明LTL 与自动机之间的转换并不是双向的，LTL 的表达能力弱于自动机[10]。

虽然LTL 具有容易理解、表达能力较强的优点，但它的缺点是不能表达ω-正则性质，具备完整的ω-正则语言表达能力对于性质规约语言来说是十分重要的，尤其是对于无限状态系统的形式化验证。因此一些研究对LTL 进行扩充，使得扩展得到的时序逻辑表达能力等价于ω-正则语言[11]。一种方法是将时序逻辑构筑于二阶量词或不动点算子，如Kozen[12]提出了μ 演算，μ 演算在时间模型的基础上加入了不动点算子。通过引入不动点算子使得μ 演算表达性增强，然而付出的代价是其可满足性的判定问题变得复杂，而且不动点算子的嵌套使用令公式难以理解。另外一种方法则是在时序逻辑基础上添加时序算子或者正则表达式，如Wolper[13]提出了ETL，通过在LTL 中加入正则表达式使其表达能力等价于自动机。

2.2 计算树逻辑CTL

CTL[14]的语义模型与LTL 类似，都是通过Kripke 结构来定义的。不同的是，由状态组成的序列∏∶s0，s1，s2，…，sk，…的路径中，从模型的初始状态作为根节点，对于k≥0，都有（sk，sk+1）∈R，模型的未来时刻存在着多种不确定状态。因此，把所有路径展开就形成了树状的拓扑结构，这也是被称为计算树的原因，又因为每个节点存在分支，所以CTL 也被称之为分支时序逻辑（branching temporal logic，BTL）。

CTL 的语义模型是通过Kripke 三元组M=＜S，R，L＞来定义的，其中S 是状态集合，R⊂S×S 是符合完全性约束的变迁关系（即对于任意的状态s∈S,存在状态s'∈S 满足 （s，s'）∈R），L∶S→2AP是标记函数，用于标记某个状态上所有满足的原子命题集合。

为了更好地介绍如何使用CTL 描述相关性质，以多个进程访问共享内存为例进行说明。假设有两个独立进程proc1和proc2访问同一片共享内存，并且要避免它们同时访问，一旦两个进程同时访问临界区，那么就会造成程序崩溃。“entering”状态表示当前某个进程请求访问共享内存，“critical”状态表示当前有某个进程正在访问共享内存。

性质4：两个进程不能同时访问共享内存，即两个进程间存在互斥性（mutual exclusion）。

2.3 计算树逻辑CTL*

针对LTL 与CTL 在在处理计算分支上的不同，Clarke 对CTL 的语法和语义作适当的扩充，设计了兼容上述两种时序逻辑算子的语言CTL*[15]，该语言融合两种时序逻辑于一种语言之中，同时还克服了时序逻辑公式的二义性解释（时序逻辑公式既可以解释成线性的，也可以解释成分支的）。

CTL*的语义与CTL 类似，因此不做过多介绍。LTL 和CTL 存在交集，这部分性质既可以用LTL 公式表示，也可以用CTL 公式来表示。存在只能用LTL 公式表示的性质（如A（FGp））却不存在着相应的CTL 公式，也存在只能用CTL 公式表示的性质（如AG（EFp））却不存在着相应的LTL 公式。这两种性质的结合体A（FGp∨AG（EFp）既不能用LTL 表示，也不能用CTL 表示，只能用这两种时序逻辑的超集CTL*表示。随着CTL*表达能力的增强，CTL*模型检测的复杂度随之提高，CTL*的模型检测问题是PSPACE-完全的。随着待验证系统规模状态增加，CTL* 模型检测中的状态爆炸问题更加突出，在实际验证中会根据具体情况牺牲部分表达能力而选择复杂度较小的LTL 公式或CTL 公式。在表达能力上LTL 公式可以方便地描述路径范围的选择，但在路径量词方面有所缺失，CTL 公式可以精细地描述某个路径，但欠缺对路径范围的选择。

一个逻辑公式的可满足性问题也称为模型检测问题，对于CTL* 有如下结论：

定理2 ①CTL*的模型检测问题是多项式时间完备的；②CTL*的模型检测问题具有NP 难度和co-NP 难度[16]。

CTL*是CTL 和LTL 的超集，表达能力虽然得到了加强，但仍然存在着两个主要缺陷。首先CTL*公式描述的是系统从某一状态s 开始后系统的所有可能发生的行为，并不关注系统是以一种什么样的方式到达状态s 的，换句话说CTL*公式不能描述状态s 之前的系统行为。另外CTL*的缺陷是只能定性地描述系统建立可能发生的行为，但却不能精确地描述该行为发生的确切时间，该类性质对于并发系统中区间相关性质尤为重要[17]。

2.4 LTL 和CTL 的比较

定义4 LTL 公式和CTL 公式的等价性。

如果一个LTL 公式φ 和一个CTL 公式ø 是等价的，记作φ≡ø，那么对于任意迁移系统（transition system，TS）上的原子命题来说，当且仅当下面的式子成立

从公式形式上来看，在LTL 公式上添加全称路径量词得到CTL 公式，这是因为LTL 公式默认包含量词。

然而并不是简单地去掉CTL 公式中的路径量词就得到相应的LTL 公式，例如CTL 公式∀◇∀□a 和LTL 公式◇□a 并不是等价的。LTL 公式◇□a的含义是从某个状态开始，命题a会永远成立，然而CTL 公式∀◇∀□a 的语义解释是对于任意一条路径，最终会到达某个状态s，使得s｜=∀□a，当且仅当对于任意一条路径π＝s0，s1，s2，…∈Path（s）会有状态sj使得sj｜=∀□a 成立，这也意味着状态sj之后的所有可达状态都满足原子命题a。

对于LTL 公式◇□a 来说是满足图1 中状态迁移系统的，初始状态s0满足公式◇□a，从s0出发最终会停留状态s0或者s2，是满足该公式的语义“从某一状态开始a 永远为真”。然而对于CTL 公式∀◇∀□a 来说不满足图2 中的状态迁移系统，该公式在状态s0处不成立，记作s0ω｜≠◇∀□a，这是因为路径s0*，s1，s2ω经过了一个不满足原子命题a 的状态s1，其中s0*表示由状态s0构成的有穷序列，s2ω表示由状态s2构成的无穷序列。

图1 LTL 公式◇□a 的状态迁移系统Fig.1 The state transition system of LTL ◇□a

图2 CTL 公式∀◇∀□a 的计算树展开形式Fig.2 The expansion form of computation tree of Formula CTL formula ∀◇∀□a

另外，许多学者也对LTL 和CTL 的区别进行过系统研究。这两种逻辑使用同一套符号体系，造成语义上的模糊，关于这两种逻辑孰优孰劣，学者们有着不同的争论。两种时序逻辑的公式是一样的，关键在于语义的区别。LTL 以路径作为命题的论断对象，而CTL 以状态作为命题的论断对象。图灵奖得主Lamport 的结论是[18]：LTL 和CTL 一般来说是不能相比的，但在证明并发程序的某些性质时LTL 要优于CTL，而在证明非确定性程序的某些性质时CTL 要优于LTL。Lamport 和Emerson 等曾讨论过LTL 和CTL 的本质区别，及其用于程序验证时功能上的不同。那么它们的不同之处在于语义上的区别，主要体现在下列事实上。

定理3 在LTL 中□p≡→p，但在CTL 中◇p¬≡→p。

其中，→p 的含义表示“有时p 成立”。该定理表明在不同语义模型下，LTL 和CTL 是不等价的，针对这两种不同时序逻辑的表达能力问题，Lamport定义了强等价性。

定义5 给定时序结构M=（S，X，D），其中S 为非空状态集，X 是非空路径集，D 是一个映射。如果对于每条路径a∈X 来说都有（L，M，a）｜=p 成立，则称时序公式p 是在线性语义下M 为真，记作（L，M）→p。类似的，如果对于每个状态t∈S 都有（B，M，t）→p成立，则称时序公式p 在分支意义下M 为真。其中L 表示线性语义，B 表示分支语义。

定义6 令p 和q 表示两个时序公式，C 是由一组时序结构组成的类，如果对C 中的每个时序结构，有如下公式成立

式中：I 和J 是两个语义解释，可以是线性语义L 或分支语义B，则称时序公式p 和q 分别在语义解释I 和J 下，相对于结构类C 是强等价的，记作p=q（I，J，C）。

基于上述定义，可以证明得到如下两个定理。

定理4 存在这样的结构类C，使得CTL 公式◇p 不强等价于任何LTL 公式。

定理5 存在这样的结构类C，使得LTL 公式→◇p 不强等价于任何CTL 公式。

上述定理的证明过程在文献[19]中已经给出，对于上述结论，可以用下面的例子进行说明。设P是一个不确定性程序，则P 的计算路径和计算结果有多种可能性，如果要证明不管P 走哪一条路径，它的计算最终必将终止，那么这个性质用CTL 公式表示为∀◇terminated（P），根据定理4，该公式是无法用LTL 公式表示的，因此在这一点上CTL 是强于LTL 的。另一方面，设Q 是一个并发程序，其中包含许多并发执行的分量，如果要证明Q 对各分量Qi的调度符合公平性原则，即任何一个分量，只要获取无数多次可执行机会，则一定会被执行，该性质可以用LTL 表示为□¬enabled（Qi）∨execute（Qi），根据定理5，该公式是无法用CTL 表示的。因此在这一点上LTL 又强于CTL。对于该结论的可靠性，Emerson 指出Lamport 的强等价性的要求过高，该结论是以某个断言在所有状态或所有路径上为真的前提下进行比较的。

对于这两种时序逻辑的比较，从逻辑的角度看这两种语言各有长短。实际应用于模型检测中，普遍认为对于安全属性如公平性和活性的描述，使用LTL 表示更具有优势。但是从计算的角度来看，实现CTL 模型检测相对简单，LTL 模型检测问题是PSPACE-完全的，而CTL 模型检测时间是线性或多项式的。从模型检测的发展历程来看，在模型检测早期，以SMV 为代表的CTL 模型检测器对硬件、数字电路验证占主导地位。但对于刻画系统性质的规约，使用LTL 更加简洁且容易理解，再加上LTL 模型检测算法有巨大进步，Cadence SMV 和SPIN 这类LTL 模型检测工具得到广泛应用。

对于LTL，CTL 的模型检测，由于两者的语义解释不同造成模型检测方法的不同。在对LTL 公式φ进行模型检测时，模型检测工具会对φ 取反得到有限自动机A¬φ，然后与系统模型的有限自动机AM相乘，验证两个自动机的交集是否为空，若不为空，则表示设计中有不满足属性的行为。而对CTL 公式进行模型检测是以Kripke 结构图的所有状态为根节点进行搜索，如果存在不满足属性的模型，即得到违反属性的反例路径。通过对比这两种不同公式的模型检测方法，可以得出LTL 模型检测可以快速完成对路径上的状态搜索，所需要的状态数比CTL 模型检测更少。

3 连续时间模型的时序逻辑

本节介绍基于连续时间模型的时序逻辑，包括ITL 和PTL，对两种逻辑系统进行分析比较，指出它们的适用范围。

3.1 区间时序逻辑ITL

LTL，CTL 公式的语义在独立的点上被解释，一个点代表一个状态，点之间的关系就代表时序之间的关系，这样的时序关系无法描述正则表达式所表达的性质。由于基于连续时间模型的时序逻辑的表达能力较弱，使得对一些性质的验证无法进行。因此很多关于LTL 的扩展已经被提出，如Kozen 提出了μ 演算[12]，Vardi 提出了ETL[13]。尽管这些时序逻辑具备完全正则语言能力，但仍难以表达一些状态敏感的性质，如原子命题p 在某个具体状态或具体区间上成立，此外如顺序、循环等结构难以表达。

与基于点语义的LTL 不同,系统的时间特征行为可能会出现在一系列时间区间上，那么就需要使用一些连续时间区间, 称之为区间时间模型。Moszkowski 在其博士论文中提出了基于区间语义的ITL[20]，可用于描述区间中的状态及其时序关系的性质。

定理6 ITL 具有正则表达能力，能够方便地表达状态敏感的性质，以及顺序、迭代等行为[20]。

由于ITL 定义在有穷区间范围内, 主要包括chop，next 以及投影符号proj 等时序操作符，因此使得ITL 比LTL 具有更强的表达能力。作为时序逻辑的一个重要分支，现在已经扩展应用在并发软件系统的规约和验证，但ITL 的缺陷在于只能应用于有穷区间。

在ITL 中有两个最具特色的动作算子: 分割算子“；”（chop operator）和投影算子proj（projection operator）。分割算子“；”的作用是把一个有穷区间分割成两个部分，可以表示成p，q，该公式的含义为前一部分性质p 成立，后一部分性质q 成立。投影算子proj 具有可重复行为，P proj Q 把一个有穷区间Q 分割成多份具有相同长度的子区间。投影算子的主要作用是能产生重复操作的结构，可用于描述Loops 循环，例如动作P 每隔时间n 就执行一次可描述为P proj len（n）。

3.2 投影时序逻辑PTL

由于ITL 是定义在有穷区间上的时序逻辑，所以该逻辑的缺陷是无法描述系统中的无穷行为。针对ITL 存在的问题，西安电子科技大学段振华等提出了投影时序逻辑PTL[21]，对ITL 进行扩充到无穷区间范围内，并引入一个全新的投影操作结构（P1，…，Pm）prj Q，从而得到一种描述有穷、无穷模型和时段的逻辑系统。

通过引入投影操作符号（P1，…，Pm）prj Q 将ITL推广到无穷区间范围，与原有的投影结构P prj Q相比，新的投影操作更加灵活易用。PTL 相比ITL 的优势在于：由于扩充了投影算子prj，PTL 可以应用于无穷区间，允许用不同的时间粒度来描述计算的进程，由此可定义顺序、循环等操作。PTL 相比ITL更适合描述并发软件[22-23]。

定理7 PPTL 具备完全正则表达能力，能够对顺序、并行、区间相关以及周期重复的性质进行描述[24-25]。

PTL 的一个命题子集也就是命题投影时序逻辑PPTL（propositional PTL，PPTL)的表达能力等价于Büchi 自动机[26]，因而证明其具有完全正则表达能力。PPTL 不仅能够表达离散时间模型上的时序性质，还可以表达如区间相关性质以及周期性重复的闭包性质，主要使用区间长度算子len（n），分割算子chop，chop star 和投影算子prj 来实现，具体性质如下[4]：

1）区间相关的性质。例如“命题p 在时间长度为n 的区间上成立”可以表示为p∧len（n）；“命题p在第5 个和第10 个时间单元内成立”可以表示为len（5）；◇p∧len（5）。

2）周期重复的性质。例如“命题p 在偶数状态上成立”可以表示为p∧（○2（p∧ε））*。因此对于验证实时系统的性质不仅局限于传统的安全性和活性，即描述性质“事件p 在将来会成立”，还可以通过时间间隔描述对于时间有严格要求的性质，例如性质“事件p 将在一段时间间隔内发生”。

3）顺序、循环、迭代等结构。PPTL 中的分割算子chop 和chop star 可以对该类结构方便地进行描述。

总的来说，相比较其它时序逻辑如LTL，CTL 和ITL，PTL 的表达能力是完全正则的，等价于Büchi自动机，能够表达区间相关的性质以及周期性重复的闭包性质，可描述并发情况以及实时性相关性质。虽然该逻辑的表达能力得到增强，但不可避免地带来更高的模型检测复杂度，减少系统状态空间的方法如偏序规约、限界模型检测以及组合验证等技术被引入到PPTL 模型检测中[28-29]。

4 处理复杂计算特征的时序逻辑

为了处理复杂的计算特征，如实时、随机、混成、开放系统中的行为，许多时序逻辑被相继提出。例如:为了描述随机系统的高度不确定性，通过在计算树逻辑中引入概率建立了概率计算树逻辑以及连续随机逻辑；为了描述实时系统中关于时间敏感的性质，提出了时段演算等一系列逻辑语言；为了处理混成系统中同时包含离散变量和连续变量的复杂行为，提出了微分动态逻辑；为了处理开放系统中多进程间的任意交互以及系统内部与外界环境的交互，计算树逻辑被扩充为交替时序逻辑，下面将对这些时序逻辑变体及其适合描述哪些性质进行概述。

4.1 面向随机系统的时序逻辑

随机系统具有随机不确定性，为了表达这种性质概率时序逻辑被提出。概率属性规约通常采用概率计算树逻辑 （probabilistic computation tree logic，PCTL）[30]和连续随机逻辑（continuous stochastic logic，CSL）[31]等概率时序逻辑描述。其中PCTL 是CTL的概率扩展，应用在离散时间马尔科夫链和马尔科夫决策，CSL 是在CTL 和PCTL 基础上扩展得到，应用在连续时间马尔可夫链, 下面对这两种概率时序逻辑作详细介绍与分析。

PCTL 适用于描述随机不确定系统，能够表达定量性质。这种能力在随机不确定性系统中是非常实用的，在形式化验证中有时并不要求系统性质的绝对正确性，而是保证系统性质在一定程度上的相对正确性。例如，在网络通信过程中经常会发生数据传输失败的情况，因此需要对数据进行重新发送。对如何使用PCTL 表达协议所期望的功能正确性和协议性能为例进行说明。在网络通信过程中，组件A 和B 在发送消息时会有一定几率发送失败，如果发送失败则会接着发送直到消息发送成功。

P＜0.05［X error A］：组件A 发送消息失败的概率小于0.05。

P＜0.05［true U≤kmessage_num≥5］：在经过k 步迁移之后，至少5 条消息被组件A 或B 成功发送的概率小于0.05。

P＞0.9［F＜100 “enabled”］：在经过100 步迁移之后，消息全部发送成功达到稳定状态的概率大于0.9。

CSL 也是由CTL 的概率扩展得到，它是在CTL的基础上添加了两个新的算子：路径概率算子P 和稳定状态算子S，可以用来描述连续时间马尔科夫链的稳态行为，公式S～p（φ）表示一个状态满足φ 的稳态概率～p。CSL 的语法中引入了一个新的公式ø1∪Iø2，其中I 是R 的时间间隔，而PCTL 中操作符∪被离散时间k 约束。因此CSL 与PCTL 的区别在于CSL 能够表达某个自然数区间的行为，而PCTL 是不能的。除了S～p（φ）以外，在CSL 中的状态公式与PCTL 没有区别，它类似于PCTL 中的P～p（φ），表示在满足～p 的概率条件下，将会保持在状态φ很长时间。CSL 适用于描述在连续时间段之内需要满足的性质，例如“在紧急情况下，飞行控制系统中的阀门必须在1 秒之内打开的概率大于99%”,表示为

目前PCTL 和CSL 已经在概率模型检测器PRISM 中得到支持和应用，被用于规约概率系统的期望属性。此外PRISM 通过扩展回报，一个形如的r：S×S→R≥0 回报结构将非负数的回报值添加到状态迁移过程中，可用于分析与回报期望值相关的属性，这是通过扩充R 算子实现的。以分布式系统中的自稳定算法为例进行说明，在分布式环境下往往要求系统具有自稳定性，这就要求自稳定算法在没有外界干预下，经过有限次步骤后从一个杂乱无章的初始状态到达一个稳定状态。对于自稳定算法关于时间消耗的属性，通过一个简单的回报结构time将系统中每一步的状态迁移的回报值设定为1，有如下公式

4.2 面向实时系统的时序逻辑

实时系统是一种能够在有限时间范围内对来自外部输入等做出快速响应的系统，例如控制系统、监测系统、通信系统等。实时系统的部件之间具有并发性，运行通常并不终止，对规定动作的进行和完成时间也有很高的要求。

时段演算适用于对实时系统的实时需求进行刻画[34]，不仅能够像其它实时逻辑描述刻度时间性质和时间边界特性，还可以描述一段时间范围内性质的累积。以燃气燃烧器为例，对如何使用时段演算形式化刻画离散状态系统的实时特性进行说明。我们希望控制煤气燃烧器的点火机制和关闭机制，把煤气泄漏控制在安全阈值之内。需求说明为：在煤气灶使用期间如果对其连续观察超过60 s，那么煤气泄漏的时间不能超过观测时间的1/20。引入b和e 分别表示观测的起始、截止时间，只有当煤气被释放且没有火焰出现的状态被称为煤气泄漏，用布尔函数Leak（t）来表示煤气的泄漏状态，可表示Leak（t）≜Gas（t）∧¬Flame（t）为,那么该安全需求形式化表示为

设计原则2：任何两个泄露时段的时间间隔不能少于30 s。

通过上面的示例可以看出，时段演算继承了ITL 的优点，克服了基于点语义的CTL*及其子集只能描述某个时刻系统状态的性质，能够描述时段累积性质，那么一个状态的前驱序列的性质也可以通过时段演算公式表示，因此时段演算被广泛应用于实时系统的形式化验证当中。虽然时段演算强大的性质表达能力使其对系统规约带来很大的方便性，但与此同时基于时段演算的自动化验证是十分困难的，时段演算没有绝对意义上的完备公理系统，时段演算公式的可满足性与模型检测问题都是不可判定的。目前的做法是针对时间模型做一些限制（如对离散时间域的长度进行限制得到有界离散时间模型）或者限制模态算子的使用来得到其可判定的子集和模型检测子集[35]。

此外，针对实时系统的性质规约与验证，还有许多时序逻辑被相继提出，对它们的研究主要分为两个方向。其中一种是通过在时序逻辑中引入含时间 界 限 的 时 序 算 子 （如□≤tφ，□≤［t1，t2］φ，◇≤tφ，◇≤［t1，t2］φ）来表示实时性质，包括时间计算树逻辑[36]和度量区间时序逻辑[37]等。另外一种是在时序逻辑中引入显式的时钟变量来表示时间约束，代表性的有实时时序逻辑[38]，例如性质“命题p 在时间区间［t1，t2］内成立”可形式化表示为：∀u（t=u∧◇（p∧（u+t1≤t∧t≤u+t2））），其中，t 是全局时钟变量，u 是刚性变量。上述时序逻辑适用于作为实时与混成系统的性质规约语言，对于实时系统通常是利用时间自动机或者混成自动机来建模，模型构建和属性规约分别采用两种不同的语言来描述。针对该方法的局限性李广元提出了面向实时系统的连续时序逻辑[39]，这是LTL 在实时领域的一种扩展，该逻辑语言继承了时序逻辑程序设计语言的优点，既能够表示实时系统的实现与性质规约，又能在统一的语义框架下表示高层的需求规约与低层的实现模型之间不同抽象级别的描述。

4.3 面向混成系统的时序逻辑

混成系统是一种特殊的实时系统，混成系统的研究对象包括嵌入式系统和信息物理融合系统等[40]。该类系统的特征是既有离散的逻辑控制又有连续的时间行为，并且这两部分行为相互交织混杂在同一系统中。混成系统的状态变化既随时间连续变化，也受到离散事件驱动[41]。20 世纪90 年代以来，随着混成系统在工业、航空航天领域得到广泛应用，对该类系统的安全性和可靠性提出了严格要求，保障混成系统的可靠性是目前的研究热点。普通的时段演算主要关注离散状态系统中某类状态在给定观测时间区间（时段）上的积分，而对于混成系统中的连续动态行为缺乏相应的描述机制。Raven 提出了扩展的时段演算（extended duration calculus，EDC），在原有的时段演算基础上引入连续实值函数对混成系统的连续动态行为进行描述，混成系统的模型以及性质被扩展的时段演算公式形式化表示，然后基于时段演算的公理系统和推理规则对混成系统进行推理验证。

由于混成系统的并发性和时间属性使得混成系统的状态空间极为庞大，而且系统中的状态可达性不可判定使得基于模型检测的混成系统形式化验证难以开展。André Platzerti[42]提出了一类描述混成系统属性的规约语言：微分动态逻辑（differential dynamic logic，DDL）家族，该类逻辑是离散一阶动态逻辑的扩展，DDL 在离散一阶动态逻辑的基础上引入了描述连续状态变化的结构，利用混成程序（hybrid program）建模混成系统中状态以及状态变迁，具体为使用离散跳跃集表示混成系统中的离散变迁，使用微分方程组描述系统动态行为中的连续变迁，然后通过控制结构操作符（U，*，∶）将系统的离散和连续行为组合在一起。

DDL 适用于描述混成系统中离散变迁与连续动态行为特征[43]。这表明DDL 可用于描述混成系统中连续变化的物理层和离散变化的控制层之间的相互交互过程，并且相关推理规则已经被提出，能对混成系统的行为特性进行推理验证。基于DDL对混成系统的形式化验证主要是采用定理证明方法，同时结合了组合验证思想，在验证过程中对待验证属性公式进行逐步分解然后独立验证，能够明显克服基于混成自动机、混成Petri 网验证混成系统时面临的状态爆炸问题，提高验证效率并能够保持系统模型特征与变迁结构。

DDL 具有良好的扩展性，基于DDL 的定理证明是在给定的公理和推理规则上进行，为了使DDL具有更强大的证明能力，可以对DDL 的公理系统和推理规则进行扩充。目前在DDL 基础上根据不同的应用情况以及不同的操作模型衍生出许多变体，包括微分代数动态逻辑 （differential-algebraic dynamic logic，DAL），微分时序动态逻辑（differential temporal dynamic logic，dTL），微分代数时序动态逻辑（differential-algebraic temporal dynamic logic，DATL）以及量化微分动态逻辑（quantified differential dynamic logic，QdL）[44-46]。DDL 缺乏描述物理环境中连续动态行为特性的有效方法，同时存在微分方程不可解的情况，针对该问题在一阶动态逻辑的基础上提出了DAL，使用微分不变量技术进行推理验证而不必求解微分方程。为了验证混成系统中的时序属性，将DDL，DAL 分别与时序逻辑相结合得到dTL 和DATL，DATL 将动态逻辑的模态操作符和时序逻辑的时序操作符完美结合在一起，得到形如的逻辑公式，可以同时描述系统的时序行为和非时序行为。为了处理分布式混成系统的形式化验证，基于一阶动态逻辑和量化的微分方程相结合得到QdL。DDL家族之间的关系可以用图3 来说明。

图3 微分动态逻辑家族示意图Fig.3 Schematic diagram of differential dynamic logic family

4.4 面向开放系统的时序逻辑

封闭系统的行为由当前系统所处的状态决定，与外部环境无关，针对封闭系统的模型检测主要采用LTL 或CTL 来描述系统的性质。开放系统的行为不仅由系统当前所处状态决定，同时也受到外部环境的约束[47]。与封闭系统相比，开放系统的外部环境是不确定的，开放系统中不同组件之间的交互会导致难以预测的情况发生，如可观测性以及可控性等。因此，开放系统的形式化验证需要将外部环境的各种不确定情况纳入考虑范围内[48]。Alur 提出了交替时序逻辑（alternating-time temporal logic，ATL）[49]，该逻辑描述的是开放系统与外界环境之间的交互以及内部组件之间的合作与竞争关系，将系统中的各组件之间的交互最终到达的稳定状态规约为开放系统与外界环境之间的博弈结果，所以又被称为博弈逻辑。

ATL 适用于描述开放系统与外界环境之间的交互以及内部组件之间的合作与竞争关系[50]。这表明对于系统行为同时受到内部结构和外部环境输入的开放系统，系统不同组件之间交互后最终达到的状态，可以使用ATL 规约为开放系统与外部环境之间的博弈。以几个简单的例子介绍如何使用ATL来描述开放系统中各个主体之间的合谋与对抗行为，来说明ATL 对于开放系统的表达能力。假设存在参与者集合∑＝｛a，b，c｝，不同的参与者存在着策略使得命题p 成立，同时不同参与者之间存在着合谋与竞争，有如下ATL 公式：

《a》◇p：针对参与者b 和c，参与者a 存在一个获胜策略使得命题p 最终成立。

《b，c》□p：针对参与者a,无论参与者b 和c 如何合谋，永远不能避免系统最终达到一个状态使得命题p 成立。

《a，b》○（p∧¬《c》□p）：针对参与者c，参与者a和b 合谋能够使得下一状态命题p 成立，并且从下一状态开始参与者c 永远不能使命题p 成立。

上述公式形式化地描述了一个开放系统中不同成员之间的合作与对抗行为，这种表达能力对于描述电子商务协议这种开放系统是非常合适且有效的。与传统的安全协议中协议参与方是诚实的相比，电子商务协议中除了可信第三方（trusted third party，TTP）是诚实可信的，其他参与主体都是互不信任且会做出欺骗行为。例如电子支付协议中存在消费者已经收到货物但是却拒不承认的情况，或者消费者与攻击者合谋一起欺骗商家等恶意行为，电子商务协议中的安全威胁不仅仅来自外部环境，更多的是协议参与方之间的合谋与对抗。在基于Dolev-Yao 模型的协议分析过程中，安全协议被当作一个封闭系统进行研究，不能有效地描述协议与外部环境之间的交互。而基于ATL 的电子商务协议安全性分析中，充分考虑了协议主体间的相互博弈，所有协议参与方根据自身利益最大化选择适合自己的策略，根据博弈结果决定自己下一步动作，能够对协议主体间的合谋与对抗行为进行精确地描述。目前实验结果表明ATL 比LTL，CTL 更适合分析电子商务协议这一类开放系统，已经成功发现合同签署协议、公平交换协议中存在不满足公平性等缺陷[51-52]。

此后有许多研究工作对ATL 进行扩展形成了ATL 家族，主要体现在策略表示、与其它逻辑相融合等方面的扩展。ATL 规定每一个路径选择量词《A》必须有一个时序算子相匹配，针对该缺陷提出的ATL*支持这两种算子之间的任意嵌套，因此ATL*的性质表达能力比ATL 更强。ATL中只能对策略进行量化，模糊地表示存在某一策略使得性质φ 成立，但不能明确指出是哪一个策略使得性质φ 成立，针对该问题具体策略交替时序逻辑（ATL with explicit strategies，ATLES）[53]被 提出。为了将行动的实施与其所掌握的知识前提（knowledge precondition）形式化表示，文献[54]将ATL 与认知逻辑（epistemic logic）相结合提出了交替认知时序逻辑（alternating-time temporal epistemic logic，ATEL）。为了解决开放系统的验证过程中没有考虑随机行为的问题，通过引入概率分布到认知模型中来描述系统中的随机性，文献[55]基于ATEL 提出了概率交替时序认知逻辑（probabilistic alternating-time temporal epistemic logic，PATEL），能够对开放系统中的知识前提及其它性质进行定量验证。文献[56]将ATL 与投影时序逻辑PTL 结合提出了交替投影时序逻辑（alternating projection temporal logic，APTL），该逻辑融合了这两种逻辑的优点，不仅可以描述有穷区间、无穷区间内的性质，还可以描述开放系统中与博弈相关的性质。上述ATL 家族之间的关系如图4 所示。

图4 交替时序逻辑家族示意图Fig.4 Schematic diagram of alternating-time temporal logic family

5 时序逻辑未来的研究方向

从时序逻辑的发展趋势来看，今后一段时间时序逻辑的研究工作包括以下几个方面：

1）扩充已有的时序逻辑，使其能够适用于复杂系统的形式化规约。例如，随着大规模集成电路和EDA 技术的发展，片上系统（system on chip）成为嵌入式系统的发展方向，减少片上系统中的设计错误，提高系统的设计可靠性是关键性问题，基于仿真的方法中存在着覆盖率不足、仿真时间过长等问题。信号时序逻辑[57]是在模拟和混合信号电路背景下提出的规约语言，以LTL 为基础同时具有实时和实值约束，可以描述离散和连续系统的实时属性。在量子计算方面，随着量子计算机在计算速度方面有超越经典计算机的绝对优势，量子程序的开发及验证是发挥量子计算机能力的关键因素，目前基于CTL 的量子计算树逻辑 （quantum computation tree logic，QCTL）[58-59]已被提出用于量子程序的性质规约。此外，新的计算模式如大数据、机器学习算法不断涌现，这些计算模式下程序行为与经典的串行与并发程序有显著差异，因此需要扩充或设计新的时序逻辑来描述这些新的计算模式[60-61]。

2）研究不同形式化逻辑系统之间的组合，使得组合后的逻辑能够吸收不同逻辑的特性。例如分离逻辑是对霍尔逻辑的扩展，对于验证具有复杂数据结构的动态内存程序非常实用，但从表达能力来看，分离逻辑并未突破一阶逻辑的范畴，在描述和验证内存的时序性质方面仍有欠缺[62]。时序逻辑虽然能够描述状态随时间变化系统的时序性质，但不能够描述带有指针的程序性质,文献[63-64]提出一种结合分离逻辑和PPTL 的二维(时间和空间)时序逻辑PPTLSL，该逻辑继承了分离逻辑和PPTL 的优势，能够描述指针程序的时序性质。此外，利用until算子描述的性质在LTL 中可以轻松实现，但却不能被PPTL 有效支持。文献[65]将LTL 中的until 算子在有穷区间和无穷区间上重新定义并扩充到PPTL中，提出一种新的统一时序逻辑UTL（unified temporal logic，UTL），该逻辑完美地结合了LTL 和PPTL的特性。

3）时序逻辑的判定问题、模型检测问题和公理化问题。对于时序逻辑而言，除了需要研究它的表达能力之外，还需要研究该逻辑的判定性、模型检测和公理系统。时序逻辑的判定问题即该逻辑的（可满足）判定性及复杂度，该问题在一种新的时序逻辑被提出时是必须考虑的。基于时序逻辑的模型检测即自动化验证系统模型是否满足性质规约的重要手段，设计高效的模型检测算法与开发相关支撑工具是人们追求的目标。公理化问题即基于该逻辑提出相应的公理和推理规则，并保证该公理系统的可靠性和完备性。针对特殊的无穷状态系统的模型检测，结合定理证明技术能够有效缓解系统状态空间的膨胀。

6 结束语

形式化方法是验证安全攸关系统安全性与可靠性的重要手段，时序逻辑作为形式化规约语言，能够描述软硬件系统中基于时间变化的状态迁移，是形式化验证的基础。本文首先介绍基于离散时间模型的LTL，CTL 和CTL*，以及基于连续时间模型的ITL 和PTL，对它们之间的区别进行阐述；然后介绍为了处理复杂计算特征(如随机、实时、混成和开放系统中的行为)而提出的各种时序逻辑；最后指出时序逻辑未来的研究方向。