阿米尔·伯努利——把时态逻辑引入计算机科学第一人

    以色列学者AmirPnueli是一位著名的计算机科学家，他从海法以色列理工学院获得了学士学位和数学博士学位。他是以色列著名的魏兹曼学院的应用数学教授。在伯努利在斯坦福大学的博士后研究期间，他转向计算机科学。他的计算机科学专注于时间逻辑和模型检查，尤其是并发系统的公平性。他的论文的主题是“海洋潮汐的计算”。1996年，他因将时间逻辑引入计算机科学而在程序和系统验证领域做出了杰出贡献，从而获得了图灵奖，以表彰他对将时间逻辑引入计算机科学的贡献。
    伯努利出生于英国巴勒斯坦（以色列）的那哈啦，并获得了海法以色列理工学院的数学学士学位和博士学位。来自魏茨曼科学研究所的应用数学。他的论文主题是“海洋潮汐的计算”。在斯坦福大学担任博士后研究员期间，他转到计算机科学专业。他的计算机科学着作侧重于时态逻辑和模型检查，特别是关于并发系统的公平性。
    魏茨曼科学研究学院数学博士。在斯坦福大学做博士后时转而研究计算机科学。
    由于程序的行为是一种动态现象，其状态是随着时间的推移而不断改变的，而这种改变又可能反过来影响其外部环境。并发反应式程序的这种持续的动态行为无法用经典逻辑描述，由著名的逻辑学家霍恩(A．Hom)于1951年提出，因而用他的名字命名的至多包含一个正文字的Hom子句所组成的霍恩逻辑也不能描述。而伯努利的PLTL则凭着它的极强的表达能力，填补了这一空白，成为研究并发程序尤其是持续不终止的反应式程序(如操作系统，网络通信协议等)的强有力的形式化工具，可充分表达程序的安全性、活性和事件的优先性等，成为程序规约(specification)、验证(verification)等的有力工具。
    值得指出的是，中国科学家在伯努利工作的基础上，将时态逻辑用于计算机科学的研究大大地向前发展了一步。伯努利只把时态逻辑用于程序规约和验证，而我国科学家唐稚松(中科院院士，软件所研究员)在20世纪70年代末、80年代初把时态逻辑用于软件开发的整个过程，包括需求定义、规约、设计、证实、验证、代码生成和集成，并开发了世界上第一个可执行时态逻辑语言XYZ/E和一组相应的CASE工具，在国际上引起强烈反响。1979年，时任美国加州大学伯克利分校计算机科学系主任的布卢姆(M．Blum，计算复杂性理论奠基人之一，1995年图灵奖获得者)曾致信唐稚松本人，称：“在美国，很有一些最重要的计算机科学家知道您及您的工作，他们都对您的研究工作作了高度评价”。伯努利本人也同唐稚松建立了联系，并成为朋友。1995年8月，为庆祝唐稚松70寿辰，举办了一个名为“逻辑和软件工程”的国际专题讨论会，伯努利和他的老搭挡曼纳带了一篇新的论文“有时钟的变迁系统”(ClockedTransitionSystem)来北京参加了这个讨论会，并亲自编辑出版了会议论文集(LogicandSoftwareEngineering：InternationalWorkshopinHonourOfChih-SungTang，Singapore：WorldScientificPr.，1996)。在论文集的前言中，伯努利高度评价了唐稚松的工作。