阿米爾·伯努利檢視原始碼討論檢視歷史

阿米爾·伯努利
出生	1941年4月22日
國籍	以色列
別名	Amir Pnueli
職業	科學 教授
知名於	獲得其應用數學博士學位
知名作品	《反應式系統和並發系統的時態邏輯:規約》

人物生平

阿米爾·伯努利（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的編委。