時序邏輯

由多個觸發器和多個組合邏輯塊組成的網路。常用的有：計數器、複雜的數據流動控制邏輯、運算控制邏輯、指令分析和操作控制邏輯。同步時序邏輯是設計複雜的數字邏輯系統的核心。時序邏輯藉助於狀態寄存器記住它目前所處的狀態。在不同的狀態下，即使所有的輸入都相同，其輸出也不一定相同。

在計算機出現后的最初幾十年裡，計算機實質上是一個巨大的計算器，數字被錄入，計算結果被輸出。直到20世紀70年代，科學家們才意識到需要正確地驗證這些計算結果。隨著電腦變得更強大，軟體更先進，多任務和筆畫的數據核查變得更加困難。因此，程序員不得不考慮到時間推移下系統的行為。在這個契機下，時序邏輯被引入計算科學，這是計算科學發展歷史的重要轉折點。

時序邏輯也叫時態邏輯（temporal logic），是計算機科學里一個很專業很重要的領域。時序邏輯被用來描述為表現和推理關於時間限定的命題的規則和符號化的任何系統，主要用於形式驗證。20世紀60年代Arthur Prior提出介入的基於模態邏輯的特殊的時間邏輯系統，這一理論後來被艾米爾 伯努利等邏輯學家進一步發展。

後來，Pnueli在斯坦福大學和IBM Waston 研究中心從事博士后的研究工作，從這時開始，他將工作研究方向轉移到計算機科學領域。1973年，他創辦了特拉維夫大學計算機科學系，並擔任第一任院長。1977 年，Pnueli開創性地把時態邏輯引入計算機科學，他的時態邏輯是非經典邏輯中的一種，研究如何處理含有時間信息的事件的命題和謂詞。現在通常稱為時序邏輯的計算機系統，就出現在這一年，Pnueli 在子編程語言與系統驗證方面做出的傑出貢獻具有里程碑意義。

“Pnueli實現了這一邏輯，這是計算機科學的完美契合”，賴斯大學計算工程的摩西教授如是說。1996 年度圖靈獎頒獎典禮上，該獎項的題詞評價Pnueli 1977年的論文“引發了對系統的動態行為推理的基本模式轉變”。這個很傑出的技術誕生后即在軟體工程界引起轟動，掀起了軟體工程中的一場革命，目前已成為開發反應式系統和併發式系統時進行規格說明和驗證的工具，在晶元、硬體的設計上已經廣泛運用。

1981年，Pnueli 回到魏茲曼成為計算機科學系的教授。1999年，Pnueli加入美國紐約大學計算機科學系並出任教授一職。此外，和國外絕大多數教授一樣，Pnueli 並不拘泥於純學術的研究和教學。Pnueli 成立了幾家軟體公司，1971年成立Mini-Systems ，1984年成立AdCad。他還和朋友一起在美國馬薩諸塞州創辦了另一家公司：iLogixInc，Pnueli 擔任iLogixInc 公司的首席科學家。

Pnueli為人謙遜隨和，與中國的淵源甚深。他和2008年去世的我國著名邏輯和軟體學家唐稚松是至交，二人均是時態邏輯方面是業界領跑人。唐稚松教授提出了世界上第一個可執行時序邏輯語言XYZ/E。如果說Pnueli獲1996年圖靈獎的最大貢獻，是因開創性地將時序邏輯引入計算科學，那麼唐稚松則是第一次將這種時序邏輯形式化理論與最新軟體技術結合起來，應用該語言將狀態轉換的控制機制引入到邏輯系統之中的人。Pnueli 赴美接受圖靈獎前夕，在寫給唐稚松的信中說：“我完全相信，由於使時態邏輯成為具有‘深遠影響’的理念，你應該分享這一榮譽（指圖靈獎）中一個很有意義的部分。”

除了圖靈獎，Pnueli還曾獲得獎項無數，其中就包括以色列獎，這是以色列給出美國國家科學院外籍院士的成員的最高榮譽。