阿米尔·伯努利

阿米尔?伯努利(Amir Pnueli) ,1941年4月22日出生于以色列。在斯坦福大学和IBM Waston研究中心从事博士后的研究工作其间,Pnueli将研究工作方向转移到计算机科学领域。1999年,Pnueli加入美国纽约大学计算机科学系并出任教授。1996年授予Amir Pnueli 图灵奖,以表彰其在计算机科学中引入时序逻辑的开创性的研究工作,和其在编程语言和系统验证方面的突出贡献。

阿米尔·伯努利 - 简介

阿米尔·伯努利(Amir Pnueli) ,出生于1941年4月22日于Nahalal,以色列。Amir Pnueli年青时代从以色列Technion - Israel Institute of Technology 技术学院获得其数学学士学位,从以色列Weizmann Institute of Science获得其应用数学博士学位。Pnueli的博士论文工作是关于"Cacluation of Tides in the Ocean"。

在斯坦福大学(www.stanford.edu )和IBM Waston研究中心(www.watson.ibm.com )从事博士后的研究工作其间,Pnueli将研究工作方向转移到计算机科学领域。1981年,Pnueli成为Weizmann Institute计算机科学系的教授。1999年,Pnueli加入美国纽约大学计算机科学系并出任教授。1996年授予Amir Pnueli 图灵奖以表彰其在计算机科学中引入时序逻辑的开创性的研究工作,和其在编程语言和系统验证方面的突出贡献。

阿米尔·伯努利 - 把时态逻辑引入计算机科学

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的编委。

TAGS: 人物 图灵奖获得者
上一页: 艾兹格·迪科斯彻 下一页: 艾伦·纽厄尔
相关名人更多>>
名人图文更多>>
相关名人更多>>
网站首页 | 网站地图 | 电脑版
个人简历网-移动版 m.gerenjianli.com