时序逻辑领域的开拓者
文章来源： | 发布时间：2009-12-09 | 【】 【】
又一位图灵奖得主去世了，他是受人尊敬的时序逻辑领域大师艾米尔• 伯努利（amir pnueli）。今年11月2日，这位1996年度图灵奖得主因脑出血去世，享年68岁，只剩那些熠熠生辉的科技成就留给后人。
艾米尔• 伯努利于1941年出生于以色列的nahalal，在以色列理工学院取得数学学士学位，1967年在魏茨曼学院以一篇关于海洋潮汐计算的毕业论文取得应用数学博士学位。而后伯努利留校任教。
在计算机出现后的最初几十年里，计算机实质上是一个巨大的计算器，数字被录入，计算结果被输出。直到20世纪70年代，科学家们才意识到需要正确地验证这些计算结果。随着电脑变得更强大，软件更先进，多任务和变化的数据核查变得更加困难。因此，程序员不得不考虑到时间推移下系统的行为。在这个契机下，时序逻辑被引入计算科学，这是计算科学发展历史的重要转折点。
时序逻辑也叫时态逻辑（temporal logic），是计算机科学里一个很专业很重要的领域。时序逻辑被用来描述为表现和推理关于时间限定的命题的规则和符号化的任何系统，主要用于形式验证。20世纪60年代arthur prior提出介入的基于模态逻辑的特殊的时间逻辑系统，这一理论后来被艾米尔•伯努利等逻辑学家进一步发展。
后来，pnueli在斯坦福大学和ibm waston研究中心从事博士后的研究工作，从这时开始，他将工作研究方向转移到计算机科学领域。1973年，他创办了特拉维夫大学计算机科学系，并担任第一任院长。1977年，pnueli开创性地把时态逻辑引入计算机科学，他的时态逻辑是非经典逻辑中的一种，研究如何处理含有时间信息的事件的命题和谓词。现在通常称为时序逻辑的计算机系统，就出现在这一年，pnueli在子编程语言与系统验证方面做出的杰出贡献具有里程碑意义。
“pnueli实现了这一逻辑，这是计算机科学的完美契合”，赖斯大学计算工程的摩西教授如是说。1996年度图灵奖颁奖典礼上，该奖项的题词评价pnueli 1977年的论文“引发了对系统的动态行为推理的基本模式转变”。这个很杰出的技术诞生后即在软件工程界引起轰动，掀起了软件工程中的一场革命，目前已成为开发反应式系统和并发式系统时进行规格说明和验证的工具，在芯片、硬件的设计上已经广泛运用。
1981年，pnueli回到魏兹曼成为计算机科学系的教授。1999年，pnueli加入美国纽约大学计算机科学系并出任教授一职。此外，和国外绝大多数教授一样，pnueli并不拘泥于纯学术的研究和教学。pnueli成立了几家软件公司，1971年成立mini-systems，1984年成立adcad。他还和朋友一起在美国马萨诸塞州创办了另一家公司：ilogixinc，pnueli 担任ilogixinc公司的首席科学家。
pnueli为人谦逊随和，与中国的渊源甚深。他和2008年去世的我国著名逻辑和软件学家唐稚松是至交，二人均是时态逻辑方面是业界领跑人。唐稚松教授提出了世界上第一个可执行时序逻辑语言xyz/e。如果说pnueli获1996年图灵奖的最大贡献，是因开创性地将时序逻辑引入计算科学，那么唐稚松则是第一次将这种时序逻辑形式化理论与最新软件技术结合起来，应用该语言将状态转换的控制机制引入到逻辑系统之中的人。pnueli赴美接受图灵奖前夕，在写给唐稚松的信中说：“我完全相信，由于使时态逻辑成为具有‘深远影响’的理念，你应该分享这一荣誉（指图灵奖）中一个很有意义的部分。”
除了图灵奖，pnueli还曾获得奖项无数，其中就包括以色列奖，这是以色列给出美国国家科学院外籍院士的成员的最高荣誉。
（本文来自《程序员》杂志0912期）
