精华区文章阅读

发信人: ssos (存在与虚无·戒酒戒网), 信区: Algorithm
标  题: 让时态逻辑“搬家” ——伯努利　　
发信站: 哈工大紫丁香 (2001年08月23日17:16:11 星期四), 站内信件

1996年度的图灵奖授予了一位以色列学者，著名的以色列魏茨曼学院(Weizmann Insti
tute 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年，伯努利把时态逻辑引入计算机科学，把它作为开发反应式系统(reactivesyst
em)和并发式系统 (concurrentsystem)时进行规格说明(specification)和验证(verifi
cation)的工具，取得了极大的成功，在软件工程界引起轰动，被认为是软件工程中的
一场革命。伯努利也因此而声名大振，他曾被斯坦福大学，哈佛大学等著名高等学府聘
为客座教授或进行讲学。
伯努利主要从事教学和研究，但也和国外绝大多数教授一样，不限于“纯学术”工作。
他和别人一起在美国马萨诸塞州的Burlington办了一个公司：iLogixInc，他任该公
司首席科学家。
伯努利和我国科学院院士、著名的逻辑和软件学家唐稚松是朋友和知交。唐稚松曾向伯
努利建议，把 “时态逻辑”当作整个软件开发过程(包括需求、规格说明、设计、证实
、验证、代码生成和集成)的普遍的基础，而不局限于规格说明和验证。伯努利深受启
发并对唐先生的聪明和眼光大为赞叹。1995年8月，为庆祝唐稚松70寿辰，举办了一个
名为“逻辑和软件工程”的国际专题讨论会，伯努利带了一篇新的论文来北京参加了
这个讨论会，并负责编辑出版了会议论文集(Logicand Software Engineering: Intern
ational Workshopin Honour of ChihSung Tang, Singapore: World Scientific Pres
s,1996)。在论文集的前言中，伯努利叙述了他和唐稚松之间的这段交往。
伯努利的代表作如下：
《The Temporal Logic of Reactiveand Concurrent Systems: Specification》(Spri
ngerVerlag,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

--


<<社会契约论>>是一本好书,应当多读几遍
风味的肘子味道不错,我还想再吃它

※ 来源:·哈工大紫丁香 bbs.hit.edu.cn·[FROM: 202.118.230.220]

Algorithm 版 (精华区)