让时态逻辑“搬家” ——伯努利 吴鹤龄
1996年度的图灵奖授予了一位以色列学 者，著名的以色列魏茨曼学院(Weizmann Institute of
Science，位于圣城耶 路撒冷西北约50公里的雷霍沃特)应用数学系教授艾米尔·伯努利(Amir Pnueli)，以彰显他把时态逻辑引入计算机科学所做的贡
献。
伯努利于1967年在魏茨曼学院获应用数 学博士学位，后留校任教。他的主要研究方向是时态逻辑或叫 时序逻辑(temporal
logic)。时态逻辑是非经典逻辑中的一种，它研究 如何处理含有时间信息(现在、过去、将来；之前、之后等)的事件
的命题和谓词。时态逻辑体系包含的要素有：
- 基本符号：事件e，关系或谓词r，时间区间i(interval)等。
- 时态谓词：after(e,r),before(e,r)等。
- 时态事件演算规则：初始规则、终止规则等，如holds(before(e,r))： terminates(e,r)表终止规则，意为若事件已使谓词r失效，则在e之前
且r成立以一段区间中r为真。
- 时态逻辑运算：时态区间的并交，时态谓词的与、或、非等。
1977年，伯努利把时态逻辑引入计算机 科学，把它作为开发反应式系统(reactivesystem)和并发式系统
(concurrentsystem)时进行规格说明(specification)和验证(verification)的工具，
取得了极大的成功，在软件工程界引起轰动，被认为是软件工 程中的一场革命。伯努利也因此而声名大振，他曾被斯坦福大
学，哈佛大学等著名高等学府聘为客座教授或进行讲学。
伯努利主要从事教学和研究，但也和国 外绝大多数教授一样，不限于“纯学术”工作。他和别人一起在 美国马萨诸塞州的Burlington办了一个公司：iLogixInc，他任该公
司首席科学家。
伯努利和我国科学院院士、著名的逻辑 和软件学家唐稚松是朋友和知交。唐稚松曾向伯努利建议，把 “时态逻辑”当作整个软件开发过程(包括需求、规格说明、设计、
证实、验证、代码生成和集成)的普遍的基础，而不局限于规格说 明和验证。伯努利深受启发并对唐先生的聪明和眼光大为赞
叹。1995年8月，为庆祝唐稚松70寿辰，举办了一个名为“逻辑和软 件工程”的国际专题讨论会，伯努利带了一篇新的论文来北京
参加了这个讨论会，并负责编辑出版了会议论文集(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
谈谈你对伯努利的感觉
本文由ccw提供
|
