Algorithm 版 (精华区)

发信人: Lerry (坐壮:望苗:思汉@贵族 与猫族斗争到底), 信区: Algorithm
标  题: ['96]Amir Pnueli 
发信站: 哈工大紫丁香 (2002年04月26日07:54:21 星期五), 站内信件

[1996]让时态逻辑“搬家” ——伯努利 (吴鹤龄)
(Ref: http://it.sohu.com/itpeople/Pnueli.html
      http://www.acm.org/awards/turing_citations/pnueli.html)
=============================================================================
   1996年度的图灵奖授予了一位以色列学 者，著名的以色列魏茨曼学院(Weizmann
   Institute of Science，位于圣城耶 路撒冷西北约50公里的雷霍沃特)应用数学
   系教授艾米尔·伯努利(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年，伯努利把时态逻辑引入计算机 科学，把它作为开发反应式系
   统(reactivesystem)和并发式系统 (concurrentsystem)时进行规格说
   明(specification)和验证(verification)的工具， 取得了极大的成功，在软件
   工程界引起轰动，被认为是软件工 程中的一场革命。伯努利也因此而声名大振，
   他曾被斯坦福大 学，哈佛大学等著名高等学府聘为客座教授或进行讲学。

   伯努利主要从事教学和研究，但也和国 外绝大多数教授一样，不限于“纯学术”
   工作。他和别人一起在 美国马萨诸塞州的Burlington办了一个公司
   ：i?LogixInc，他任该公 司首席科学家。

   伯努利和我国科学院院士、著名的逻辑 和软件学家唐稚松是朋友和知交。唐稚松
   曾向伯努利建议，把 “时态逻辑”当作整个软件开发过程(包括需求、规格说明
   、设计、 证实、验证、代码生成和集成)的普遍的基础，而不局限于规格说 明和
   验证。伯努利深受启发并对唐先生的聪明和眼光大为赞 叹。1995年8月，为庆祝
   唐稚松70寿辰，举办了一个名为“ □阎M软 件工程”的国际专题讨论会，伯努利
   带了一篇新的论文来北京 参加了这个讨论会，并负责编辑出版了会议论文
   集(Logicand Software Engineering: International Workshopin Honour of
   ChihSung Tang, Singapore: World Scientific Press,1996)。在论文集的前言
   中，伯努利叙述了他和唐稚松 之间的这段交往。

   伯努利的代表作如下：

   《The Temporal Logic of Reactiveand Concurrent Systems: Specification
   》(SpringerVerlag,1992)

   《Temporal Verification of Reactive Systems: Safety》 (Springer
   Verlat, 1995)

   伯努利现任斯普林格出版社著名的系 列丛书“Lecture Notesin Computer
   Science”的编委，也是有关领域的不少 杂志如《Acta In formatica》、
   《Science of Computer Programming》、《Noteson Computer Science》的编委
   。

   伯努利的电子邮箱为：

   amir@wisdom.weizmann.ac.il
=============================================================================
Amir Pnueli

   Citation
          For seminal work introducing temporal logic into computing
          science and for outstanding contributions to program and
          systems verification.
=============================================================================
  
--
当一个女孩儿觉得她不太容易了解那个男人的时候，她会爱他。

※ 来源:·哈工大紫丁香 bbs.hit.edu.cn·[FROM: 218.7.32.75]
※ 修改:·Lerry 於 04月26日07:56:17 修改本文·[FROM: 218.7.32.75]