在命题逻辑的基础上,Arthur Norman Prior在上个世纪50年代创建了模态逻辑的一个分支——时态逻辑。从80年代起,在哲学、计算机科学、人工智能、语言学等诸多交叉学科的推动下,时态逻辑取得了新的发展,形成了一些既具有重大理论意义,又具有实际应用价值的研究成果。比较典型的是在计算机科学中的发展。本文以时态逻辑在计算机科学中的发展为主线,在描述计算机科学中时态逻辑的发展的同时,与哲学中时态逻辑的发展进行对比分析,分别分析了时态逻辑对计算机科学的贡献和计算机科学的发展对时态逻辑本身的影响,并以此为基础,对未来逻辑学与计算机科学的交叉互动做出了初步展望。本文共分五个部分：第一部分,回顾时态逻辑的历史发展。第二部分,描述了一元时态逻辑的十个系统的语言、公理、定理和它们的性质,并分析了各个系统之间的关系,随后简要介绍了二元时态逻辑。第三部分,介绍了时态逻辑在计算机科学下发展的背景和所解决的问题,介绍了两个计算机科学下最重要的系统——命题线性时态逻辑系统和分支时态逻辑系统,并分析了它们之间的关系和适用区别。第四部分,介绍了三个时态逻辑的典型扩充系统,前两个是计算机科学下发展起来的,第三个是通常逻辑学中的扩充。第五部分是一些进一步的讨论,对于时态逻辑在计算机科学中的发展进行了总结和评论,为未来逻辑学与计算机科学的交叉互动做出展望。