浅谈时态逻辑在计算机科学中的发展

时态逻辑(又称时序逻辑、时间逻辑)作为描述根据时间限定的命题或推理所使用的任意规则和符号系统，是模态逻辑的一个重要分支。在命题逻辑的基础上，Arthur Norman Prior在上个世纪50年代几乎独自创建了这一现代逻辑的重要分支的基础，对时态逻辑的发展具有里程碑意义，被视为“时态逻辑之父”。从上个世纪80年代开始，在其他学科如：计算机科学、数学、人工智能以及语言学等的发展需要的促进下，时态逻辑获得了新的进一步的发展，从而形成了一些不仅具有理论意义而且也有丰富的实际应用价值的成果。

1 计算机科学中时态逻辑的形式化

在逻辑学中，形式化是指分析、研究思维形式结构的方法。“逻辑学的研究对象是思维的形式和规律，但这里的思维形式并非指的是人们思维过程中，能动地、概括地间接反映现实世界的过程中所使用的那些形式，即具体的概念、判断和推理，而是撇开了它们的具体内容，仅仅抽象出其一般的形式结构的概念、判断和推理，这种逻辑形式通常借助于一定的语言形式来表达。”传统的形式逻辑，是以自然语言为主要表述手段，这种表述接近日常思维实际，却存在歧义、模糊、不够精确的缺点。现代形式逻辑则以人工语言为主要表述手段，引入符号语言表达变项和常项。

在计算机科学领域，形式化方法是一种建立在严格的数学基础上，具有精确数学表达形式和语义的开发方法。这种开发方法试图实现从软件的规范，软件的设计到软件的代码实现自动转换和验证，从而充分保证系统的正确性和可靠性。在软件开发过程中，最初级最原始的描述系统也就是规范的方法是用日常语言，这是一种非形式化方法，但这种描述方法可能存在模糊性、歧义性和层次混乱的缺点。

2 时态逻辑对计算机科学的贡献

时态逻辑不仅可以作为哲学分析的有力工具，还对语言学、数学和计算机科学等其他学科产生了重要的影响，尤其是在计算机科学中。近些年来，软件工程、人工智能发展迅猛，时态逻辑对计算机科学的重要影响逐渐被人们所认知。在计算机出现初期，其功能相当于一个十分庞大的计算器，输入数字后，输出计算结果。直到20世纪70年代，计算机科学家们认为有必要对这些输出的计算结果进行正确性验证，可是由于计算机功能的越发强大，数据具有多任务和多变化的特性，对其进行核查会越发的艰难。因此，计算机科学家们必须去研究在时间的推移下计算机系统的行为这一因素。于是，在这样的背景下，这一理论在20世纪70年代被数学家Amir Pnueli和他的搭档Zohar Manna引入计算机科学中，在计算机科学中得到了迅速的发展。时态逻辑是形式逻辑的一个分支，是经典逻辑的一个简单的扩充，它提供了一个很自然的方式来描述程序中的时态行为。时态逻辑能够以一种简单、自然地方式来支持层次化的规范和验证。

时态逻辑对计算机科学的发展还有一个有用之处是：时态逻辑能够表达程序的两个特性：安全性和存活性。安全性用于描述事件必须不会发生，相当于程序中的约束条件;存活性用来描述事件必须最终会发生，它可以防止程序只满足初始条件及影响其它行为。线性时态逻辑显示任何两个不同的时间点都有先后关系，时间序列成不分叉的线状分布的时态。与“线性时态逻辑”相对，在分支时间时态逻辑中，时间的结构有分支树形的性质，即每一个时刻都有多个后继时刻，时间结构就如同一棵有无数分枝的树，树上的每个时间点都有一个到有限多个后继时间。

3对时态逻辑未来发展的展望

可以预见，时态逻辑在计算机科学中不断而深入的应用，将为时态逻辑乃至整个逻辑学提供一种源动力。时态逻辑未来的一个重要发展方向就是扩充发展，在时态逻辑中加入其它的算子就能组成新的逻辑系统。就时态逻辑目前在计算机科学中的应用来看，虽然己经取得了瞩目成就，但计算机科学家们己经看到，同其它形式系统一样，时态逻辑也有其局限性：一是时态逻辑不能很容易的实现并发程序的规范和验证。设计并发程序是一个艰难的过程，时态逻辑提供了一种方法，这种方法能够准确说明程序该做什么和精确分析程序将做什么。精确的推理对任何形式系统来说都是艰难和费时的，但时态逻辑是据我所知能消除并发程序中因时间依赖而产生的细微误差的唯一方法。二是时态逻辑的表达能力有限，除了适合说明和推理并发程序之外，在其它地方用处不大。

4结语

时态逻辑在哲学上作为非经典逻辑的一个分支，研究涉及时间的人类思维中的方方面面，主要体现的是理论性和全面性。时态逻辑作为计算机形式化的一种工具，只研究和工程实践有关的方面，主要体现的是工具性和实用性。不管是在逻辑学还是在计算机科学，时态逻辑都是一个重要的研究课题，而在时态逻辑中引入其它算子，扩充成表达性更强的系统，近年来兴起的一个新的研究课题，也是它的一个十分重要的发展方向。