阿米尔·伯努利
人物简介
阿米尔• 伯努利（Amir Pnueli） ，1941年4月22日出生于以色列。在 斯坦福大学和IBM Waston研究中心从事 博士后的研究工作其间，Pnueli将研究工作方向转移到 计算机科学领域。1999年，Pnueli加入 美国纽约大学 计算机科学系并出任教授。1996年授予Amir Pnueli 图灵奖，以表彰其在计算机科学中引入 时序逻辑的开创性的研究工作，和其在 编程语言和系统验证方面的突出贡献。[1]
相关研究
把 时态逻辑引入计算机科学 1996年度的图灵奖授予了一位以色列学者，著名的以色列魏茨曼学院(Weizmann Institute Of Science，位于圣城 耶路撒冷西北约50 km的 雷霍沃特)应用数学系教授阿米尔·伯努利(Amir Pnueli)，以彰显他把时态逻辑引入计算机科学所做的贡献。 伯努利于1967年在魏茨曼学院获应用数学博士学位，后留校任教。他的主要研究方向是时态 逻辑或叫时序逻辑(temporal logic)。时态逻辑是非 经典逻辑中的一种，它研究如何处理含有时间信息(现在、过去、将来；之前、之后等)的事件的命题和谓词。时态 逻辑体系包含的要素有： 1．基本符号：事件e，关系或谓词r，时间区间i(interval)等。 2．时态谓词： after(e，r)，before(e，r)等。 3．时态事件演算规则：初始规则、终止规则等，如holds(before(e，r))：—terminates(e，r)表终止规则，意为若事件已使谓词r失效，则在e之前且r成立的一段区间中r为真。 4．时态 逻辑运算：时态区间的并、交，时态谓词的与、或、非等。 1977年，伯努利把时态逻辑引入计算机科学，把它作为开发反应式系统(reactive system)和并发式系统(concurrent system)时进行 规格说明(specification)和验证(verification)的工具，取得了极大的成功，在 软件工程界引起轰动，被认为是软件工程中的一场革命。伯努利也因此而声名大振，他曾被 美国斯坦福大学、 哈佛大学等著名高等学府聘为客座教授或进行讲学。 伯努利和他的同事曼纳(Z．Manna)共同开发的时态逻辑系统叫“命题线性时态逻辑系统”(Proposition Linear Temporal 1ogic，缩写PLTL)。PLTL包含可数无穷多个 命题变元， 逻辑联结词“否定”┐，“ 合取”∧，“ 析取”∨，“蕴含” ，“等价”≡；时态算子□，意为“任一时刻”；◇，意为“某一时刻”；○，意为“下一时刻”；μ，意为“直到”。 合式公式（well-formed formula）在PLTL中的定义如下： （1）命题变元P是合式公式； （2）若w、w1和w2是合式公式，则┐w、 w1∧w2、w1∨w2、w1 w2、w1≡w2都是合式公式；□W、◇W、○W和w1μw2也都是合式公式； （3）每个合式公式均可通过有限次应用（1）、（2）获得。 PLTL中包含10条公理和3条推理规则，它们是： 公理1：┐◇w≡□┐w 公理2：□(w1 w2) (□w1 □w2) 公理3：□w w 公理4：○┐w≡┐○w 公理 5：○(w1 w2) (○w1 ○w2) 公理6：□w ○w 公理7：□w ○□w 公理 8：□(w ○w) (w □w) 公理9：(w1μw2) ≡(w2∨(w1∧○(w1μw2))) 公理10： (w1μw2) ◇w2 推理规则1( 重言规则)：若u是命题 重言式(tautology)，则├u 推理规则2( 假言推理规则)：若├u v且├u ，则├v 推理规则3(口引入规则)：若├u，则├□u 应用上述公理和推理规则，经过有穷步骤，可推导出一系列合式公式，即PLTL的定理。 显然，PLTL是对普通 命题逻辑(propositional lohic)的扩充，但这一扩充却意义重大，因为这使系统具有了处理随时间变化而改变其值的动态变元(称为时序或时态变元)的能力。在时态逻辑中，时间的结构可以有线性、分支、离散、连续，基于时间点或时区的这样几种不同情况，可视具体应用背景而定。PLTL采用线性、离散，且与 自然数同构的时间结构。它的 语义解释是一个无穷状态序列σ=S0,S1,S2,…，每个Si都是对命题变元的一个赋值。若令σ（i）=Si,si+1,si+2…，且用σ|=w表示时态公式w在解释σ下为真，则各时态算子的含义如下： σ|=□w当且仅当对任意i≥0，均有σ（i）|=w σ|=◇w 当且仅当存在i≥0，使σ（i）|=w σ|=○w当且仅当σ（i）|=w σ|=w1μw2当且仅当存在i≥0，使 σ（i）|=w2且对任意j(0)≤j<(i)均有σ（j）|=w1 由于程序的行为是一种动态现象，其状态是随着时间的推移而不断改变的，而这种改变又可能反过来影响其外部环境。并发反应式程序的这种持续的动态行为无法用经典逻辑描述，由著名的逻辑学家 霍恩(A．Hom)于1951年提出，因而用他的名字命名的至多包含一个正文字的Hom子句所组成的霍恩逻辑也不能描述。而伯努利的PLTL则凭着它的极强的表达能力，填补了这一空白，成为研究 并发程序尤其是持续不终止的反应式程序(如操作系统， 网络通信协议等)的强有力的形式化工具，可充分表达程序的安全性、活性和事件的优先性等，成为程序规约(specification)、验证(verification)等的有力工具。 值得指出的是，中国科学家在伯努利工作的基础上，将时态逻辑用于计算机科学的研究大大地向前发展了一步。伯努利只把时态逻辑用于程序规约和验证，而我国科学家 唐稚松(中科院院士，软件所研究员)在20世纪70年代末、80年代初把时态逻辑用于软件开发的整个过程，包括需求定义、规约、设计、证实、验证、代码生成和集成，并开发了世界上第一个可执行时态逻辑语言XYZ／E和一组相应的 CASE工具，在国际上引起强烈反响。1979年，时任 美国加州大学伯克利分校计算机科学系主任的 布卢姆(M．Blum， 计算复杂性理论奠基人之一，1995年图灵奖获得者)曾致信唐稚松本人，称：“在美国，很有一些最重要的计算机科学家知道您及您的工作，他们都对您的研究工作作了高度评价”。伯努利本人也同唐稚松建立了联系，并成为朋友。1995年8月，为庆祝唐稚松70寿辰，举办了一个名为“逻辑和软件工程”的国际专题讨论会，伯努利和他的老搭挡曼纳带了一篇新的论文“有时钟的变迁系统”(Clocked Transition System)来北京参加了这个讨论会，并亲自编辑出版了会议论文集(Logic and Software Engineering：International Workshop in Honour Of Chih-Sung Tang，Singapore：World Scientific Pr.，1996)。在论文集的前言中，伯努利高度评价了唐稚松的工作。 伯努利主要从事教学和研究，但也和国外绝大多数教授一样，不限于“纯学术”工作。他和别人一起在美国 马萨诸塞州的布灵顿(Burlington)办了一个公司：i—Logix Inc，他任该公司首席科学家。
研究成果
主要有： 《反应式系统和并发系统的时态逻辑：规约》(The Temporal Verification of Reactive and Concurrent Systems：Specification，Springer，1992) 《反应式系统的时态验证：安全》(Temporal Verification of Reactive Systems：Safety，Springer，1995) 伯努利现任 施普林格出版社(Springer Verlag)著名的系列丛书kecture Notesin Computer Science的编委，也是有关领域的不少杂志如Acta lnformatica、Science Of Computer Programming、Notes On Computer Science的编委。