1导论
1.1时态由来
现代逻辑另一种更为常见的解决方法是把“小兰去上海”这类句子看成是能够表达命题的完整句子并且拥有真值。这种处理方法由Arthur Prior在上个世纪50年代首先提出，并由此发展成一个独立的逻辑分支——时态逻辑。当然，在时态逻辑中，一个句子如果是现在时态，其真值会不同于其是将来时态或过去时态的。因此，时态逻辑需要某种方法来区别这种仅仅是时态不同的句子，一种简单的方法是在经典逻辑中加两个一元联结词：将来算子F和过去算子P。如果P表示“小兰在上海”那么Fp和Pp则分别表示“小兰将会在上海”和"小兰曾经有一次到过上海”。时态逻辑中，F和P分别表示“将会有这个情况……”和“过去曾有这个情况……”，那么，等价于G，等价于H，其中，G和H分别表示“将来一直有这个情况……”和“过去曾一直有这个情况……”。用这个方法来改写上述论证如下：
1.2论文的研究意义
时态逻辑（又称时序逻辑、时间逻辑）作为描述根据时间限定的命题或推理所使用白勺任意规则和符号系统，是模态逻辑的一个重要分支。在命题逻辑的基础上，ArthurNorman Prior在上个世纪50年代几乎独自创建了这一现代逻辑的重要分支的基础，对时态逻辑的发展具有里程碑意义，被视为"时态逻辑之父”。从上个世纪80年代开始，在其他学科如：计算机科学、数学、人工智能以及语言学等的发展需要的促进下，时态逻辑获得了新的进一步的发展，从而形成了一些不仅具有理论意义而且也有丰富的实际应用价值的成果。在历史上，关于时间的逻辑首先被Aristotle研究过。Aristotle在《解释篇》第九节中讨论过时态与模态在命题间的关系。他认为“P”是一个现在时或过去时的命题，那么，“P”就是一个必然命题，从这一前提出发，Aristotle在本节进而又讨论了应用于现在与过去命题的那种必然性，是否也应用于所有将来命题。其论证如下：“如果一件东西现在是白的，那么，先前说‘它将会是白的’那句话就是正确的”。“如果说一事物‘是’或‘将是’的话总是正确的，那么，它不是或将不是就不是可能的，而如果一事物不能不将发生，那么，就不可能是它将不发生，而如果不可能是它将不发生，那么，它就必定将发生。所以，一切将要发生的，一定必然发生。”中世纪的WilliamOckham或Peter Auriole，也都进行过关于时间逻辑（特别是关于未来可能性问题）的思考。
现代意义上的时态逻辑是由模态逻辑演变而来的，是一种广义模态逻辑。时态逻辑作为形式逻辑学，真正开始得到研究，是在第二次世界大战以后，研究的时间很短，是目前发展中的新领域。Arthur Norman Prior在1957年出版的论文《时间与模态》4中介绍他在时间和模态上的发现，在1967年Prior出版了《过去，现在和未来》5建立了时态逻辑形式演算系统，标志着时态逻辑作为模态逻辑的一个分支学科而诞生。继Prior之后，也有很多的逻辑学家致力于对时态逻辑的研究，并且提出了不同于Prior的时态逻辑系统，值得一提的是Hans Kamp6在1968年提出一种二元时态逻辑——US时态逻辑，其中U代表“until”； S代表“since”，这种逻辑系统比Prior表达性较为成熟的学科。1977年对时态逻辑来说，无疑是非常特殊的一年，就在这一年时态逻辑被数学家Amir Pnueli和他的搭档Zohar Manna引入计算机科学中，在计算机科学中发展迅速。时态逻辑在计算机科学中作为对并发程序（concurrentprogram)进行规范(specification)和验证(verification)的工具，获得了突破性的发展，Amir Pnueli的这一重大成果在当时甚至被认为是计算机科学界的一场革命。他也因此在1996年获得了计算机界的最高奖项一图灵奖。时态逻辑引入计算机科学后，得到了迅速的发展，除了 Pnueli的命题线性时态逻辑系统外，比较重要和典型的还有唐稚松和赵探的XYZ系统，E. A.Emerson 和 E. M.Clarke 的计算树逻辑（Computation Tree Logic), Leslie Lamport 的行为时态逻辑系统（Temporal logic of actions),等等。毫无疑问，不同的目的产生不同的时间实体选择（例如连续、区间和分支），就产生了不同的表达这些信息的时态逻辑系统。同时在工程实践中，有许多方面与时间有关，在时态逻辑系统中加入一些其他的算子扩充后则会使系统语言具有更强的表达能力刻画处理这些信息关系。在众多有关时态逻辑的应用发展中，笔者认为，计算机科学中的时态逻辑发展路线（见图1-1)，尤其值得关注。这不仅是因为其中产生了丰富的研究成果，更是因为计算机及人工智能的发展动向直接关乎时态逻辑本身的未来追求。本文聚焦于时态逻辑在计算机科学中的发展，试图通过研究时态逻辑在应用于计算机科学前后所出现的一些具体变化，反观时态逻辑的本质和重要性，进而对时态逻辑与计算机科学等相关认知科学的交叉融合提出一些初步思考。
2时态逻辑概览
时间作为一个本体论问题，不同的领域有不同的时间性质的阐释，而逻辑学家能够做的事情就是将人们在各个领域中对时间性质所做的种种假设加以形式化的处理、讨论它们的逻辑性质和相互联系。本章首先介绍极小时态逻辑系统L。，分析系统的可靠性、一致性、完全性及其他性质，并在这个系统的基础上，通过加入对时间性质的不同刻画的模态词，构成极小时态逻辑系统L。的不同的变形和扩充，并分别介绍这些系统以及分析了这些系统之间的相互关系。在本章的最后，以Hans Kamp的us时态逻辑为例简要介绍了二元时态逻辑系统的语言和语义。
2.1 A.N.Prior和时态逻辑
Arthur Norman Prior (1914-1969)最伟大的成就毫无疑问是他对现代时态逻辑方面所做的贡献。自20世纪50年代中叶幵始，他几乎独自创建了这一现代逻辑的重要分支的基础，对时态逻辑的发展具有里程碑意义，被视为“时态逻辑之父”。Prior〗二 1914年12月4日出生在新西兰的马斯特顿，他的母亲在他出生后几周就去世/，他的父亲是一名医生并且参加了第一次世界大战。Prior由祖母和姑妈抚养长大，他的祖父和外祖父都是牧师，基督教家庭的成长环境对他后面哲学和逻辑学的工作奠定了重要的基础。Prior的整个教育时代都是在新西兰度过的，一开始他只是位谦虚的数学家为人所知，1946年他幵始在新西兰的坎特伯雷大学教哲学和逻辑。虽然Prior是从1953年正式开始研究时态逻辑，但在1950年他确定了时间和逻辑之间会有某种关联。在1950年到1951年之间，Prior曾撰写一本名叫“逻辑技艺”的书，这本书未曾全部出版，只是以《命题与词项学说》为书名出版了其中的一部分。在这本书的第一章节“命题和句子”中，他分析了 Aristotle关f?时间和时态问题的一些观点。Prior发现，按照古代以及中世纪时期的观点，一个命题可能在这个时候为真，在另一个时候为假。他在文中这样表达：“某人坐着，这个语句或观点为真，只要实际上是坐着的，一旦他站起来，这个语句就为假。”
3计算机科学中的时态逻辑 .........19
3.1为何形式化 .........19
3.2计算机为什么使用时态逻辑 ......... 21
3.3 Amir Pnueli和时态逻辑系统 ......... 23
3.4分支时态逻辑 .........28
3.4.1树形结构 .........28
3.4.2命题分支时态逻辑系统 ......... 28
3.5本章小结 .........30
4时态逻辑的重要扩充 ......... 32
4.1行为时态逻辑 ......... 32
4.2时态认知逻辑 ......... 35
4.3模态时态逻辑 ......... 37
4.4对比与分析 ......... 38
5总结与评论 ......... 40
5.1时态逻辑对计算机科学的贡献 ......... 40
5.2计算机的发展对于时态逻铒的毖响 ......... 40
5.3个人对时态逻辑在两个学科 ......... 41
5.4对时态逻辑未来发展的展望 ......... 42
结论
时态逻辑不仅可以作为哲学分析的有力工具，还对语言学、数学和计算机科学等其他学科产生了重要的影响，尤其是在计算机科学中。近些年来，软件工程、人工智能发展迅猛，时态逻辑对计算机科学的重要影响逐渐被人们所认知。在计算机出现初期，其功能相当于一个十分庞大的计算器，输入数字后，输出计算结果。直到二十世纪七十年代，计算机科学家们认为有必要对这些输出的计算结果的进行正确性验证，可是由于计算机功能的越发强大，数据具有多任务和多变化的特性，对其进行核查会越发的艰难。因此，计算机科学家们必须去研究在时间的推移下计算机系统的行为这一因素。于是，在这样的背景下，这一理论在20世纪70年代被数学家Amir Pnueli和他的搭档Zohar Manna引入计算机科学中33,在计算机科学中得到了迅速的发展。时态逻辑是形式逻辑的一个分支，是经典逻辑的一个简单的扩充，它提供了一个很自然的方式来描述程序中的时态行为。时态逻辑能够以一种简单、自然地方式来支持层次化的规范和验证。时态逻辑对计算机科学的发展还有一个有用之处是：时态逻辑能够表达程序的两个特性：安全性和存活性34。安全性用于描述事件必须不会发生，在相当于程序中的约束条件；存活性用来描述事件必须最终会发生，它可以防止程序只满足初始条件及影响其它行为。
参考文献
[1]冯棉.广义模态逻辑[M].上海_.华东师范大学出版社，1987.
[2]晋荣东.逻辑何为——当代中国逻辑的现代性反思[M].上海：上海古籍出版社，2005.
[3]彭漪涟.逻辑学基础教程[M](修订版）.上海：华东师范大学出版社，2009.
[4]杨文龙等.软件工程[M](第二版）?北京：电子工业出版社，2004.
[5]周北海.模态逻辑导论[M].北京：北京大学出版社，2002.
[6]章清宇，郭世铭，李小五.哲学逻辑研究[M].北京：社会科学文献出版社，2007.
[7]亚里士多德.范畴篇解释篇[M].方书春，译.北京：商务印书馆，1986.
[8]刘冬宁，汤庸.智能主体的信念认知时态子结构逻辑模[J].计算机应用研究，2010，(7).
[9]宁正元，胡山立，赖贤伟.交互时态信念逻辑及其模型检测[J].南京大学学报（自然科学版)，2008, (2).
[10]白金山，李祥.具有自反性质的线性时态逻辑研究[J].汁算机工程与设计，2011，(4).