阿米爾·伯努利（Amir Pnueli） ，出生於1941年4月22日於Nahalal，以色列。Amir Pnueli年青時代從以色列Technion - Israel Institute of Technology 技術學院獲得其數學學士學位，從以色列Weizmann Institute of Science獲得其套用數學博士學位。Pnueli的博士論文工作是關於"Cacluation of Tides in the Ocean"。
基本介紹
- 中文名：阿米爾?伯努利
- 外文名：Amir Pnueli
- 國籍：以色列
- 出生日期：1941年4月22日
- 職業：科學 教授
- 代表作品：《反應式系統和並發系統的時態邏輯:規約》
人物生平,相關研究,研究成果,
人物生平
阿米爾·伯努利（Amir Pnueli） ACM會士，1941年4月22日出生於以色列。在斯坦 福大學和IBM Waston研究中心從事博士後的研究工作其間，Pnueli將研究工作方向轉移到計算機科學領域。1999年，Pnueli加入美國紐約大學計算機科學系並出任教授。1996年授予Amir Pnueli 圖靈獎，以表彰其在計算機科學中引入時序邏輯的開創性的研究工作，和其在程式語言和系統驗證方面的突出貢獻。
阿米爾·伯努利
阿米爾·伯努利2009年11月2日 逝世
相關研究
把時態邏輯引入計算機科學
阿米爾·伯努利
阿米爾·伯努利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的編委。
