时序逻辑的语法语义比较分析

黄 羿，马新强，刘友缘，罗万成

(1.重庆文理学院机器视觉与智能信息系统重点实验室，重庆 永川 402160;

2.贵州大学计算机科学与技术学院，贵州 贵阳 550025;3.贵州科学院，贵州 贵阳 550001)

时序逻辑的语法语义比较分析

黄 羿1，2，3，马新强1，2，3，刘友缘1，罗万成1

(1.重庆文理学院机器视觉与智能信息系统重点实验室，重庆 永川 402160;

2.贵州大学计算机科学与技术学院，贵州 贵阳 550025;3.贵州科学院，贵州 贵阳 550001)

随着信息技术的快速发展，信息和通信技术(ICT)系统被广泛使用，因而其可靠性非常重要.本文采用时序逻辑的形式化方法对ICT系统进行可靠性检测讨论，主要从3种时序逻辑的语法、语义及它们的异同进行比较分析，为ICT的可靠性检测分析提供了理论借鉴.

语法;语义;时序逻辑;可靠性

目前，人们对信息和通信技术(ICT)系统的依赖在快速增长，这些系统正变得越来越复杂.通过Internet和各种嵌入式系统(如智能卡、掌上电脑、移动电话)等大规模的应用，正迅速进入人们的日常生活.人们对嵌入式系统的依赖使得这些系统的可靠运行变得非常重要.这些系统如果在运行过程中出现错误有时会带来金钱上的损失，有时甚至会带来灾难.因此，ICT系统的可靠性在系统设计中是一个关键问题，系统验证技术适用于在更可靠的方式下设计ICT系统［1］.

利用系统验证方式来构建或设计的软件应具有某些特性，而要验证的特性可以是一些基本的属性，属性大多是从系统规范得到的.系统规范描述了系统要做的和不做的，从而构成任何验证活动的基础.一旦系统不满足某个规范的属性则一个缺陷被发现了.一旦系统满足所有的属性就被认为是正确的.在本文中讨论被称为模型检测的验证技术.在这方面也有相关研究，例如:为了保证以Verilog硬件描述语言设计的片上系统的正确性，提出了Verilog程序的符号模型检测方法.该方法依据形式化操作语义将 Verilog程序建模为有限状态机，将设计规范用命题投影时序逻辑公式描述，并采用命题投影时序逻辑符号模型检测工具对程序进行验证，从而证明片上系统满足设计规范［2］.

通过模型检测技术验证系统的可靠性时，应将反应式系统的属性进行形式化描述，考虑到这类系统本身的特点，通常时序逻辑可作为这样的一个形式化描述语言［3］.像在自然语言中的情形一样，形式语言也有语义、语法和实例.语义涉及符号和符号表达式的涵义(当给符号以某种解释时).语法涉及符号表达式的形式结构，不考虑任何对形式语言的解释.形式语言的语义和语法既有联系，又有区分［4］.在这里讨论3种时序逻辑，分别是线性时序逻辑(LTL)、计算树逻辑(CTL)、时序逻辑与行为逻辑的结合(TLA).

1 LTL的语法与语义

LTL即线性时序逻辑，用于对计算进行推理.虽然没有明说，但隐含了整个系统是按着一个路径向前发展演化的，就像一个只有一个线索的故事一样.

1.1 LTL 的语法

定义1 令p是原子命题，LTL中的公式由有限次使用以下规则(1)～(5)形成:

(1)p是公式.

(2)如果Φ是公式，则﹁Φ是公式.

(3)如果Φ和Ψ是公式，则Φ∨Ψ是公式.

(4)如果Φ是公式，则ΧΦ是公式.

(5)如果Φ和Ψ是公式，则Φ∪Ψ是公式.

在定义1中可看出，规则(1)、(2)、(3)与命题逻辑中公式的形成规则相同，但和命题逻辑公式相比LTL公式引入了时序运算符Χ和∪.ΧΦ表示如果Φ在下个时刻成立，则ΧΦ在当前时刻成立.Φ∪Ψ表示在将来某个时刻Ψ成立，Φ在该时刻之前成立.

1.2 LTL 的语义

作者使用Kripke结构这个概念来定义时序公式的含义.

定义2 Kripke结构是一个四元组(S，I，R，Lable).其中

定义3 Kripke结构中的路径是一个无限状态序列s0s1s2…，使得(si，si+1)∈R对∀i，i≥0.

定义4 LTL语义

令p∈AP是原子命题，σ是路径，Φ和Ψ是TLT公式，可满足关系|=定义为:

此外还引入4个辅助算子，F(将来)、G(总是)、W(除非)、R(释放).

图1 LTL实例

1.3 实例

如图1所示的Kripke结构为:线性时序逻辑将时间看作线性的，即每个时刻系统只有一个可能的后继状态，因此，每个时刻只有一个唯一的可能的将来.如果每个时刻可能有多个不同的将来，这样LTL就不能处理，因此引入CTL.

2 CTL的语法与语义

CTL即计算树逻辑，是分支时序逻辑的一种.整个系统的演化也是从某个起始状态开始的，但可以有不同的分支，即未来发展是不确定的.

2.1 CTL 的语法

定义5 令p是原子命题，CTL中的公式分为状态公式和路径公式.状态公式由有限次使用以下规则形成:

(1)p是状态公式.

(2)如果Φ是状态公式，则﹁Φ是状态公式.

(3)如果Φ和Ψ是状态公式，则Φ∨Ψ是状态公式.

(4)如果φ是路径公式，则Εφ和Αφ是状态公式.

路径公式由有限次使用以下规则形成:

(1)如果Φ是状态公式，则ΧΦ是路径公式.

(2)如果Φ和Ψ是状态公式，则Φ∪Ψ是路径公式.

从定义1、2中可以看出，CTL对LTL中的公式区分为状态公式和路径公式.状态公式表示状态的属性，路径公式表示路径的属性.运算符Χ和∪的含义与PLTL相同，但在CTL中是路径运算符号.加上路径量词Ε(对某条路径)或Α(对所有路径)前缀，路径公式转换为状态公式.

2.2 CTL 的语义

CTL公式的解释同样使用Kripke结构来定义，CTL中Kripke结构的定义与LTL中Kripke定义相同.CTL中路径的定义与LTL中路径的定义相同.

定义6 CTL语义定义6与定义4对比可看出，CTL语义中将可满足关系细分为状态公式和路径公式的可满足关系，而LTL语义中的可满足关系仅是CTL路径公式的可满足关系.因此，LTL可看作是CTL的特例.

2.3 实例如图2所示实例的Kripke结构为:

图2 CTL实例

3 TLA语法与语义

TLA是时序逻辑与行为逻辑的结合，用来对并发和反应式离散系统进行形式化和推理.在TLA中，算法被表示为公式.

3.1 TLA 的语法

定义7

通过PLTL、CTL、TLA关于公式的定义不难看出，TLA中谓词中引入了使能断言这一概念，公式里引入了行为、状态函数的概念.一个行为是由变量、下一变量、常量所形成的表达式，其值是布尔值.行为表示的是旧状态和新状态之间的关系.状态函数是由变量、常量形成的算术表达式.使能断言是对每个行为 A，一个状态s下Enabled A为真当且仅当起始于s下能执行一个A步.如果一个行为A表示一个程序的原子操作，则Enabled A在能执行这个操作的那些状态下值为真.

3.2 TLA 的语义

3.3 实例

4 结语

通过LTL、CTL、TLA语法、语义的定义和实例可看出，这三者都用状态代表每个时间点，而无限的状态序列在LTL、CTL中用路径来表示，而在TLA中不怎么使用路径这一概念.在LTL、CTL语义中主要表述路径、状态与公式间的可推导关系，LTL中的推导关系主要反映在某个时间点上，系统是否具有某种性质;或系统是否一直具有某种性质，等等.CTL中推导关系可反映每个时间点上系统满足哪些性质;或者某种性质是否在所有的分支路径上可满足还是只在某条路径上满足等.TLA则是时序逻辑和行为逻辑的结合，这种结合在TLA中的语法、语义的定义和推理规则中都有所反映.TLA的推理规则考虑了行为的影响，除此之外，推理规则还包含简单的时序逻辑推理规则.当然，TLA也比LTL、CTL复杂.通过对3种时序逻辑的语法、语义及它们的异同进行比较分析，为ICT的可靠性检测分析提供了理论借鉴.

下一步的研究主要针对ICT系统的特点应用时序逻辑形式化描述和分析.同时，针对智能信息的可靠性、可信性［5］及安全性分析中能否利用时序逻辑形式化方法进行刻画，都是值得研究的问题.

致谢:感谢贵州大学计算机科学与技术学院龙士工、王以松教授的传道授业解惑.

［1］Katoen JP.Formalmethods and tools group，principles ofmodel checking［M］.2005:15-50.

［2］逄涛，段振华，刘晓芳.Verilog程序的命题投影时序逻辑符号模型检测［J］.西安电子科技大学学报，2014，41(2):98-104.

［3］Lamport L.The temporal logic of actions［J］.ACM Transactions on Programming Languages and Systems 1993，11(1):1-52.

［4］陆钟万.面向计算机科学的数理逻辑(第2版)［M］.北京:科学出版社，2004:1-6.

［5］马新强，黄羿.基于格的可信计算模型［J］.通信学报，2010，31(8A):105-110.

(责任编辑 穆 刚)

Com parative analysis of tem poral logic syntax and semantics

HUANG Yi，MA Xinqiang，LIU Youyuan，LUOWancheng

(1.Key Laboratory of Machine Vision and Intelligent Information System，Chongqing University of Arts and Sciences，Yongchuan Chongqing 402160，China;2.Schoolof Computer Science and Technology，Guizhou University，Guiyang Guizhou 550025，China;3.Guizhou Academ y of Science，Guiyang Guizhou 550001，China)

With the rapid development of information technology，information and communication technology(ICT)systems are widely used in kinds of fields.Therefore，its reliability is of great importance.In this paper，the formalmethod of temporal logic is employed for reliability testing on ICT system.The syntax and semantics of three temporal logics，aswell as their similarities and differences are compared and analyzed，to provide a theoretical reference for reliability testing on ICT system.

syntax;semantics;temporal logic;reliability

TP391

A

1673-8004(2014)05-0116-05

2014-05-29

重庆市前沿与基础研究项目(CSTC2013JCYJA40053);重庆市教委科学技术研究项目(KJ131218、KJ111217、KJ1401112);永川区自然科学基金(重点)项目(YCSTC2013NB8001，YCSTC2013AD2002).

黄羿(1976-)，女，重庆人，贵州大学博士研究生，副教授，主要从事逻辑程序、人工智能方面的研究.