去年十二月在上海参加IEEE CDC会议时，一位过去留美的同行告诉我Pnueli教授刚去世，还问我是不是对形式化研究仍然有兴趣。我对形式化已很长时间不碰了，但对Pnueli Calculi和Pnueli的Temporal Logic还印象深刻。春节之后，收到国际计算机协会的通讯CACM，整个封面是Pnueli的半身画像和暗红的标题，Amir Pnueli: Ahead of His Time。

Pnueli教授因脑溢血于2009年11月2日突然去世，终年68岁。Pnueli的工作对我早期的研究曾有过很大的影响，谨以此文表示纪念。

生平

Pnueli生于以色列，直到博士的教育也都是在那里完成的，博士论文的题目是“Calculation of Tides in the Ocean”。后赴美国斯坦福大学做博士后，其间对计算机理论产生兴趣，即转行一生从事程序理论研究。回到以色列之后，在特拉维夫大学创办计算机系，后在母校Weizmann Institute of Science任教，同时在纽约大学从事教学和研究。1977年，Pnueli教授发表了题为“The Temporal Logic of Programs”, 将哲学家们用来探索时间在自然语言中的作用之时态逻辑应用于程序行为的分析和验证，还提出了“反应系统（Reactive Systems）”的概念，不但开创了基于时态方法研究分析、验证共发（Concurrent）和反应系统的新领域，推进了模型检测（Model Checking）工作的开展，还彻底改变了之前程序验证（Program Verification）形式化研究一筹莫展、似进死胡同、毫无希望的局面。为此，许多人把Pnueli当作该领域的“拯救者”和“开拓者”。由于这项工作和接下来的一系列的重要成果，Pnueli教授一人于1996年获ACM的图灵奖，其citation说： “For seminal work introducing temporal logic into computing science and for outstanding contributions to program and systems verification”，2000年获以色列的最高奖Israel Prize,，2007年当选ACM Fellow。应指出的是，我国已故的计算机科学家唐稚松先生也是这一领域极有造诣和成就的学者，建立了时序逻辑语言XYZ/E和工具系统XYZ，而且同样是转行，从哲学转到计算机。

影响

         上世纪八十年代中，由于从事关于智能机（Intelligent Machines）的协调理论的研究，我对C.A.R. （Tony）Hoare 的通讯序贯过程（CSP）程序语言十分感兴趣，花了很大的精力去学习研究。但CSP难以描述时序，由此接触到Pnueli的关于Temporal Logic工作，希望能把两者合在一起，建立针对智能机协调过程的Specification和实时执行之理论体系。那时，一看到各种各样的Pnueli运算（Calculus）和自动机（Automata）的漂亮公式心里就激动，觉得自己的博士论文有希望了，对Pnueli和同事们的论文都是一字一句十分用心地去读。可激动之后，发现问题也很大，因为计算机可以完全基于一个结构化的人工逻辑世界，可智能机必须与动态非结构的真实物理世界打交道，时态逻辑的许多约定和假设难以采纳，特别是一旦涉及实际问题，就面临“组合爆炸”或“NP-Hard”等复杂性与决策问题，只能处理所谓的“toy（玩具）问题”。记得读了Pnueli和同事关于Timed Automata（时间化的自动机）之后，特别是看到其已在控制器分析中得到了应用，曾使我一度觉得曙光已经来临，随后意识到接下来将面临的是指数型增长的状态数目而无法实用时，当时的失望和伤心，至今印象深刻。我曾因此想放弃相关研究，并一度回去研究力学问题，还发了三篇论文，幸被导师发现，一顿猛训加鼓励，使我重回智能机和智能控制的研究。最终，我还是放弃了“阳春白雪”的形式化理论，提出了“下里巴人”式、但实用的Petri网Transducer（翻译器），完成了毕业论文，也算是自己对形式语言的探索结果。1991年，当Manna与Pnueli关于Temporal Logic的专著出版之后，我还认真地读完，虽有些新的体会，但因工作的压力已有心却无力再操旧业。今日重忆，当日的失败或因自己年轻思路狭窄而致，但愿此生还有机会回访此问题，再寻新解。

启示

Pnueli教授生性羞涩，为人低调、谦虚、不摆架子，同行学者多有好评。就连他做事拖拖拉拉、还经常迟到的毛病，也被说成最终问题总是解决了，而且还是以“in great depth, in detail, and combined with the great grace of his personality and his deep wisdom”的方式。他能够从极其抽象的理论研究，看出其商业价值，并与同事学生创办了两个公司，成功地开发了Statecharts等产品，还获得2007 的ACM Software System奖，值得我们学习。

显然，Pnueli教授的美国游学经历，对其学术生涯起了极为关键的作用。直到去世，他长期在以美两国同时任职，不但有助于他的研究和创新，也大大加强了其国际上的学术地位和影响。我熟知的许多犹太学者都有类似的经历，不但他们自己在学术获益，同时也以民间交流和外交等形式有效地加强了以色列在国际上的地位，这一事实值得我们深思。我们应鼓励、支持有条件的学者游历于国际之间。无论如何，犹太、日韩学者穿行于以美、欧美之间的经验，特别是上世纪八十年代日本大力鼓励支持其学者赴美高校（尤其是伯克利加大、CMU、MIT等名校）任职，我们应当认真研究，考察其效，适度借鉴

2010年4月始记于长沙黄华机场和CZ 3141，6月草成于旧金山ACM理事会和UA6352。