阿米爾·伯努利 - 簡介

阿米爾·伯努利（Amir Pnueli） ，出生于1941年4月22日于Nahalal，以色列。Amir Pnueli年青時代從以色列Technion - Israel Institute of Technology 技術(shù)學(xué)院獲得其數(shù)學(xué)學(xué)士學(xué)位，從以色列Weizmann Institute of Science獲得其應(yīng)用數(shù)學(xué)博士學(xué)位。Pnueli的博士論文工作是關(guān)于"Cacluation of Tides in the Ocean"。

在斯坦福大學(xué)(www.stanford.edu )和IBM Waston研究中心(www.watson.ibm.com )從事博士后的研究工作其間，Pnueli將研究工作方向轉(zhuǎn)移到計算機(jī)科學(xué)領(lǐng)域。1981年，Pnueli成為Weizmann Institute計算機(jī)科學(xué)系的教授。1999年，Pnueli加入美國紐約大學(xué)計算機(jī)科學(xué)系并出任教授。1996年授予Amir Pnueli 圖靈獎以表彰其在計算機(jī)科學(xué)中引入時序邏輯的開創(chuàng)性的研究工作，和其在編程語言和系統(tǒng)驗(yàn)證方面的突出貢獻(xiàn)。

阿米爾·伯努利 - 把時態(tài)邏輯引入計算機(jī)科學(xué)

1996年度的圖靈獎授予了一位以色列學(xué)者，著名的以色列魏茨曼學(xué)院(Weizmann Institute Of Science，位于圣城耶路撒冷西北約50 km的雷霍沃特)應(yīng)用數(shù)學(xué)系教授阿米爾·伯努利(Amir Pnueli)，以彰顯他把時態(tài)邏輯引入計算機(jī)科學(xué)所做的貢獻(xiàn)。

伯努利于1967年在魏茨曼學(xué)院獲應(yīng)用數(shù)學(xué)博士學(xué)位，后留校任教。他的主要研究方向是時態(tài)邏輯或叫時序邏輯(temporal logic)。時態(tài)邏輯是非經(jīng)典邏輯中的一種，它研究如何處理含有時間信息(現(xiàn)在、過去、將來；之前、之后等)的事件的命題和謂詞。時態(tài)邏輯體系包含的要素有：

1．基本符號：事件e，關(guān)系或謂詞r，時間區(qū)間i(interval)等。

2．時態(tài)謂詞：after(e，r)，before(e，r)等。

3．時態(tài)事件演算規(guī)則：初始規(guī)則、終止規(guī)則等，如holds(before(e，r))：—terminates(e，r)表終止規(guī)則，意為若事件已使謂詞r失效，則在e之前且r成立的一段區(qū)間中r為真。

4．時態(tài)邏輯運(yùn)算：時態(tài)區(qū)間的并、交，時態(tài)謂詞的與、或、非等。

1977年，伯努利把時態(tài)邏輯引入計算機(jī)科學(xué)，把它作為開發(fā)反應(yīng)式系統(tǒng)(reactive system)和并發(fā)式系統(tǒng)(concurrent system)時進(jìn)行規(guī)格說明(specification)和驗(yàn)證(verification)的工具，取得了極大的成功，在軟件工程界引起轟動，被認(rèn)為是軟件工程中的一場革命。伯努利也因此而聲名大振，他曾被美國斯坦福大學(xué)、哈佛大學(xué)等著名高等學(xué)府聘為客座教授或進(jìn)行講學(xué)。

伯努利和他的同事曼納(Z．Manna)共同開發(fā)的時態(tài)邏輯系統(tǒng)叫“命題線性時態(tài)邏輯系統(tǒng)”(Proposition Linear Temporal 1ogic，縮寫PLTL)。PLTL包含可數(shù)無窮多個命題變元，邏輯聯(lián)結(jié)詞“否定”┐，“合取”∧，“析取”∨，“蘊(yùn)含”  ，“等價”≡；時態(tài)算子□，意為“任一時刻”；◇，意為“某一時刻”；○，意為“下一時刻”；μ，意為“直到”。合式公式（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）每個合式公式均可通過有限次應(yīng)用（1）、（2）獲得。

PLTL中包含10條公理和3條推理規(guī)則，它們是：

公理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

推理規(guī)則1(重言規(guī)則)：若u是命題重言式(tautology)，則├u

推理規(guī)則2(假言推理規(guī)則)：若├u   v且├u ，則├v

推理規(guī)則3(口引入規(guī)則)：若├u，則├□u

應(yīng)用上述公理和推理規(guī)則，經(jīng)過有窮步驟，可推導(dǎo)出一系列合式公式，即PLTL的定理。

顯然，PLTL是對普通命題邏輯(propositional lohic)的擴(kuò)充，但這一擴(kuò)充卻意義重大，因?yàn)檫@使系統(tǒng)具有了處理隨時間變化而改變其值的動態(tài)變元(稱為時序或時態(tài)變元)的能力。在時態(tài)邏輯中，時間的結(jié)構(gòu)可以有線性、分支、離散、連續(xù)，基于時間點(diǎn)或時區(qū)的這樣幾種不同情況，可視具體應(yīng)用背景而定。PLTL采用線性、離散，且與自然數(shù)同構(gòu)的時間結(jié)構(gòu)。它的語義解釋是一個無窮狀態(tài)序列σ=S0,S1,S2,…，每個Si都是對命題變元的一個賦值。若令σ（i）=Si,si+1,si+2…，且用σ|=w表示時態(tài)公式w在解釋σ下為真，則各時態(tài)算子的含義如下：

σ|=□w當(dāng)且僅當(dāng)對任意i≥0，均有σ（i）|=w

σ|=◇w 當(dāng)且僅當(dāng)存在i≥0，使σ（i）|=w

σ|=○w當(dāng)且僅當(dāng)σ（i）|=w

σ|=w1μw2當(dāng)且僅當(dāng)存在i≥0，使 σ（i）|=w2且對任意j(0)≤j<(i)均有σ（j）|=w1

由于程序的行為是一種動態(tài)現(xiàn)象，其狀態(tài)是隨著時間的推移而不斷改變的，而這種改變又可能反過來影響其外部環(huán)境。并發(fā)反應(yīng)式程序的這種持續(xù)的動態(tài)行為無法用經(jīng)典邏輯描述，由著名的邏輯學(xué)家霍恩(A．Hom)于1951年提出，因而用他的名字命名的至多包含一個正文字的Hom子句所組成的霍恩邏輯也不能描述。而伯努利的PLTL則憑著它的極強(qiáng)的表達(dá)能力，填補(bǔ)了這一空白，成為研究并發(fā)程序尤其是持續(xù)不終止的反應(yīng)式程序(如操作系統(tǒng)，網(wǎng)絡(luò)通信協(xié)議等)的強(qiáng)有力的形式化工具，可充分表達(dá)程序的安全性、活性和事件的優(yōu)先性等，成為程序規(guī)約(specification)、驗(yàn)證(verification)等的有力工具。

值得指出的是，中國科學(xué)家在伯努利工作的基礎(chǔ)上，將時態(tài)邏輯用于計算機(jī)科學(xué)的研究大大地向前發(fā)展了一步。伯努利只把時態(tài)邏輯用于程序規(guī)約和驗(yàn)證，而我國科學(xué)家唐稚松(中科院院士，軟件所研究員)在20世紀(jì)70年代末、80年代初把時態(tài)邏輯用于軟件開發(fā)的整個過程，包括需求定義、規(guī)約、設(shè)計、證實(shí)、驗(yàn)證、代碼生成和集成，并開發(fā)了世界上第一個可執(zhí)行時態(tài)邏輯語言XYZ／E和一組相應(yīng)的CASE工具，在國際上引起強(qiáng)烈反響。1979年，時任美國加州大學(xué)伯克利分校計算機(jī)科學(xué)系主任的布盧姆(M．Blum，計算復(fù)雜性理論奠基人之一，1995年圖靈獎獲得者)曾致信唐稚松本人，稱：“在美國，很有一些最重要的計算機(jī)科學(xué)家知道您及您的工作，他們都對您的研究工作作了高度評價”。伯努利本人也同唐稚松建立了聯(lián)系，并成為朋友。1995年8月，為慶祝唐稚松70壽辰，舉辦了一個名為“邏輯和軟件工程”的國際專題討論會，伯努利和他的老搭擋曼納帶了一篇新的論文“有時鐘的變遷系統(tǒng)”(Clocked Transition System)來北京參加了這個討論會，并親自編輯出版了會議論文集(Logic and Software Engineering：International Workshop in Honour Of Chih-Sung Tang，Singapore：World Scientific Pr.，1996)。在論文集的前言中，伯努利高度評價了唐稚松的工作。

伯努利主要從事教學(xué)和研究，但也和國外絕大多數(shù)教授一樣，不限于“純學(xué)術(shù)”工作。他和別人一起在美國馬薩諸塞州的布靈頓(Burlington)辦了一個公司：i—Logix Inc，他任該公司首席科學(xué)家。

阿米爾·伯努利 - 研究成果

主要有：

《反應(yīng)式系統(tǒng)和并發(fā)系統(tǒng)的時態(tài)邏輯：規(guī)約》(The Temporal Verification of Reactive and Concurrent Systems：Specification，Springer，1992)

《反應(yīng)式系統(tǒng)的時態(tài)驗(yàn)證：安全》(Temporal Verification of Reactive Systems：Safety，Springer，1995)

伯努利現(xiàn)任施普林格出版社(Springer Verlag)著名的系列叢書kecture Notesin Computer Science的編委，也是有關(guān)領(lǐng)域的不少雜志如Acta lnformatica、Science Of Computer Programming、Notes On Computer Science的編委。