阿米爾·伯努利 - 簡(jiǎn)介

阿米爾·伯努利（Amir Pnueli） ，出生于1941年4月22日于Nahalal，以色列。Amir Pnueli年青時(shí)代從以色列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ì)算機(jī)科學(xué)領(lǐng)域。1981年，Pnueli成為Weizmann Institute計(jì)算機(jī)科學(xué)系的教授。1999年，Pnueli加入美國(guó)紐約大學(xué)計(jì)算機(jī)科學(xué)系并出任教授。1996年授予Amir Pnueli 圖靈獎(jiǎng)以表彰其在計(jì)算機(jī)科學(xué)中引入時(shí)序邏輯的開創(chuàng)性的研究工作，和其在編程語言和系統(tǒng)驗(yàn)證方面的突出貢獻(xiàn)。

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

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

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

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

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

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

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

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

伯努利和他的同事曼納(Z．Manna)共同開發(fā)的時(shí)態(tài)邏輯系統(tǒng)叫“命題線性時(shí)態(tài)邏輯系統(tǒng)”(Proposition Linear Temporal 1ogic，縮寫PLTL)。PLTL包含可數(shù)無窮多個(gè)命題變?cè)�，邏輯�?lián)結(jié)詞“否定”┐，“合取”∧，“析取”∨，“蘊(yùn)含”  ，“等價(jià)”≡；時(shí)態(tài)算子□，意為“任一時(shí)刻”；◇，意為“某一時(shí)刻”；○，意為“下一時(shí)刻”；μ，意為“直到”。合式公式（well-formed formula）在PLTL中的定義如下：

（1）命題變?cè)狿是合式公式；

（2）若w、w1和w2是合式公式，則┐w、 w1∧w2、w1∨w2、w1  w2、w1≡w2都是合式公式；□W、◇W、○W和w1μw2也都是合式公式；

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

σ|=□w當(dāng)且僅當(dāng)對(duì)任意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且對(duì)任意j(0)≤j<(i)均有σ（j）|=w1

由于程序的行為是一種動(dòng)態(tài)現(xiàn)象，其狀態(tài)是隨著時(shí)間的推移而不斷改變的，而這種改變又可能反過來影響其外部環(huán)境。并發(fā)反應(yīng)式程序的這種持續(xù)的動(dòng)態(tài)行為無法用經(jīng)典邏輯描述，由著名的邏輯學(xué)家霍恩(A．Hom)于1951年提出，因而用他的名字命名的至多包含一個(gè)正文字的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)等的有力工具。

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

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

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

主要有：

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

《反應(yīng)式系統(tǒng)的時(shí)態(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的編委。