行为时序逻辑

行为时序逻辑（The Temporal Logic of Actions）是由莱斯利·兰伯特（Leslie Lamport）发展的用于规范和推理并发自反应系统的时间逻辑。 主要应用于计算机科学，程序验证。

简介行为时序逻辑（The Temporal Logic of Actions）是由莱斯利·兰伯特（Leslie Lamport）发展的用于规范和推理并发自反应系统的时间逻辑。 主要应用于计算机科学，程序验证。1

莱斯利·兰波特莱斯利·兰波特（英语：Leslie Lamport，1941年2月7日－），美国计算机科学家。也是排版系统LaTeX的开发者。

兰波特1941年出生于纽约，是欧洲移民的儿子。 在麻省理工学院获学士学位以后，兰波特到布兰代斯大学攻读数学博士，不久后放弃，到佛蒙特州一所小型文科学校——万宝路学院教授数学。之后到麻省计算机协会做兼职工作，做ILLIAC设计。

1972年获博士学位，继续研究ILLIAC。兰波特最终得出证明，分布系统中的相对次序与观察者有关。

2013年，莱斯利·兰波特获图灵奖。1

计算机科学计算机科学（英语：computer science，有时缩写为CS）是系统性研究信息与计算的理论基础以及它们在计算机系统中如何实现与应用的实用技术的学科。它通常被形容为对那些创造、描述以及转换信息的算法处理的系统研究。计算机科学包含很多分支领域；有些强调特定结果的计算，比如计算机图形学；而有些是探讨计算问题的性质，比如计算复杂性理论；还有一些领域专注于怎样实现计算，比如编程语言理论是研究描述计算的方法，而程序设计是应用特定的编程语言解决特定的计算问题，人机交互则是专注于怎样使计算机和计算变得有用、好用，以及随时随地为人所用。

有时公众会误以为计算机科学就是解决计算机问题的事业（比如信息技术），或者只是与使用计算机的经验有关，如玩游戏、上网或者文字处理。其实计算机科学所关注的，不仅仅是去理解实现类似游戏、浏览器这些软件的程序的性质，更要通过现有的知识创造新的程序或者改进已有的程序。1

本词条内容贡献者为:

王沛 - 副教授、副研究员 - 中国科学院工程热物理研究所